structure Constraint (α : Type) : Type

• prop : α → Prop
• verify' : Validator.Result α self.prop
• elimExists : (∃ (a : α), self.prop a) → { a : α // self.prop a ∧ ∀ (a' : α), self.prop a' → a' = a }
• message : Option String

def Constraint.elimExists0 {prop : Unit → Prop} : (∃ (v : Unit), prop v) → { v : Unit // prop v ∧ ∀ (v' : Unit), prop v' → v' = v }

Equations

• Constraint.elimExists0 h' = ⟨(), ⋯⟩

def Constraint.tacticElimExists1_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def Constraint.tacticElimExists2_ : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Constraint.valid {α : Type} (h : Constraint α) : Prop

Equations

• h.valid = ∃ (a : α), h.prop a

def Constraint.verify {α : Type} (h : Constraint α) : Validator.Result α h.prop

Equations

• h.verify = Validator.withErrorMessage h.message h.verify'

def Constraint.seq {α1 α2 : Type} (h1 : Constraint α1) (h2 : α1 → Constraint α2) : Constraint (α1 × α2)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.seq.prop_eq {α1 α2 : Type} {a : α1} {a' : α2} (h : Constraint α1) (h' : α1 → Constraint α2) : (h.seq h').prop (a, a') = (h.prop a ∧ (h' a).prop a')

def Constraint.and {α1 α2 : Type} (h1 : Constraint α1) (h2 : Constraint α2) : Constraint (α1 × α2)

Equations

• One or more equations did not get rendered due to their size.

def Constraint.«term_∧ᶜ_» : Lean.TrailingParserDescr

Equations

• Constraint.«term_∧ᶜ_» = Lean.ParserDescr.trailingNode `Constraint.«term_∧ᶜ_» 70 71 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "∧ᶜ") (Lean.ParserDescr.cat `term 70))

@[simp]

theorem Constraint.and.prop_eq {α1 α2 : Type} {a : α1} {a' : α2} (h : Constraint α1) (h' : Constraint α2) : (h∧ᶜh').prop (a, a') = (h.prop a ∧ h'.prop a')

def Constraint.eqState (h : Constraint ℕ) (Eᵢ : ℕ) : Constraint Unit

Equations

• h.eqState Eᵢ = Constraint.eq✝ h Validator.SetType.States Eᵢ

@[simp]

theorem Constraint.eqState.prop_eq {Sᵢ : ℕ} {a : Unit} (h : Constraint ℕ) : (h.eqState Sᵢ).prop a = h.prop Sᵢ

def Constraint.eqAction (h : Constraint ℕ) (Eᵢ : ℕ) : Constraint Unit

Equations

• h.eqAction Eᵢ = Constraint.eq✝ h Validator.SetType.Actions Eᵢ

@[simp]

theorem Constraint.eqAction.prop_eq {Aᵢ : ℕ} {a : Unit} (h : Constraint ℕ) : (h.eqAction Aᵢ).prop a = h.prop Aᵢ

def Constraint.leftEq (h : Constraint (ℕ × ℕ)) (T : Validator.SetType) (E1ᵢ : ℕ) : Constraint ℕ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.leftEq.prop_eq {T : Validator.SetType} {E1ᵢ E2ᵢ : ℕ} (h : Constraint (ℕ × ℕ)) : (h.leftEq T E1ᵢ).prop E2ᵢ = h.prop (E1ᵢ, E2ᵢ)

def Constraint.leftEqState (h : Constraint (ℕ × ℕ)) (Eᵢ : ℕ) : Constraint ℕ

Equations

• h.leftEqState Eᵢ = h.leftEq Validator.SetType.States Eᵢ

@[simp]

theorem Constraint.leftEqState.prop_eq {S1ᵢ S2ᵢ : ℕ} (h : Constraint (ℕ × ℕ)) : (h.leftEqState S1ᵢ).prop S2ᵢ = h.prop (S1ᵢ, S2ᵢ)

def Constraint.leftEqAction (h : Constraint (ℕ × ℕ)) (Eᵢ : ℕ) : Constraint ℕ

Equations

• h.leftEqAction Eᵢ = h.leftEq Validator.SetType.Actions Eᵢ

@[simp]

theorem Constraint.leftEqAction.prop_eq {A1ᵢ A2ᵢ : ℕ} (h : Constraint (ℕ × ℕ)) : (h.leftEqAction A1ᵢ).prop A2ᵢ = h.prop (A1ᵢ, A2ᵢ)

def Constraint.rightEq (h : Constraint (ℕ × ℕ)) (T : Validator.SetType) (E2ᵢ : ℕ) : Constraint ℕ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.rightEq.prop_eq {T : Validator.SetType} {E1ᵢ E2ᵢ : ℕ} (h : Constraint (ℕ × ℕ)) : (h.rightEq T E2ᵢ).prop E1ᵢ = h.prop (E1ᵢ, E2ᵢ)

def Constraint.rightEqState (h : Constraint (ℕ × ℕ)) (Sᵢ : ℕ) : Constraint ℕ

Equations

• h.rightEqState Sᵢ = h.rightEq Validator.SetType.States Sᵢ

@[simp]

theorem Constraint.rightEqState.prop_eq {Eᵢ Sᵢ : ℕ} (h : Constraint (ℕ × ℕ)) : (h.rightEqState Sᵢ).prop Eᵢ = h.prop (Eᵢ, Sᵢ)

def Constraint.rightEqAction (h : Constraint (ℕ × ℕ)) (Aᵢ : ℕ) : Constraint ℕ

Equations

• h.rightEqAction Aᵢ = h.rightEq Validator.SetType.Actions Aᵢ

@[simp]

theorem Constraint.rightEqAction.prop_eq {Eᵢ Aᵢ : ℕ} (h : Constraint (ℕ × ℕ)) : (h.rightEqAction Aᵢ).prop Eᵢ = h.prop (Eᵢ, Aᵢ)

def Constraint.bothEq (h : Constraint (ℕ × ℕ)) (T1 T2 : Validator.SetType) (E1ᵢ E2ᵢ : ℕ) : Constraint Unit

Equations

• h.bothEq T1 T2 E1ᵢ E2ᵢ = Constraint.eq✝ (h.leftEq T1 E1ᵢ) T2 E2ᵢ

@[simp]

theorem Constraint.bothEq.prop_eq {T1 T2 : Validator.SetType} {Eᵢ E'ᵢ : ℕ} {a : Unit} (h : Constraint (ℕ × ℕ)) : (h.bothEq T1 T2 Eᵢ E'ᵢ).prop a = h.prop (Eᵢ, E'ᵢ)

def Constraint.eqStates (h : Constraint (ℕ × ℕ)) (S1ᵢ S2ᵢ : ℕ) : Constraint Unit

Equations

• h.eqStates S1ᵢ S2ᵢ = h.bothEq Validator.SetType.States Validator.SetType.States S1ᵢ S2ᵢ

@[simp]

theorem Constraint.eqStates.prop_eq {S1ᵢ S2ᵢ : ℕ} {a : Unit} (h : Constraint (ℕ × ℕ)) : (h.eqStates S1ᵢ S2ᵢ).prop a = h.prop (S1ᵢ, S2ᵢ)

def Constraint.eqStateAction (h : Constraint (ℕ × ℕ)) (Sᵢ Aᵢ : ℕ) : Constraint Unit

Equations

• h.eqStateAction Sᵢ Aᵢ = h.bothEq Validator.SetType.States Validator.SetType.Actions Sᵢ Aᵢ

@[simp]

theorem Constraint.eqStateAction.prop_eq {Sᵢ Aᵢ : ℕ} {a : Unit} (h : Constraint (ℕ × ℕ)) : (h.eqStateAction Sᵢ Aᵢ).prop a = h.prop (Sᵢ, Aᵢ)

def Constraint.actionBounds (limit Aᵢ : ℕ) : Constraint Unit

Equations

• Constraint.actionBounds limit Aᵢ = Constraint.bounds✝ Validator.IndexType.ActionSet limit Aᵢ

def Constraint.stateBounds (limit Sᵢ : ℕ) : Constraint Unit

Equations

• Constraint.stateBounds limit Sᵢ = Constraint.bounds✝ Validator.IndexType.StateSet limit Sᵢ

def Constraint.knowledgeBounds (limit Kᵢ : ℕ) : Constraint Unit

Equations

• Constraint.knowledgeBounds limit Kᵢ = Constraint.bounds✝ Validator.IndexType.Knowledge limit Kᵢ

@[simp]

theorem Constraint.knowledgeBounds.prop_eq {limit Kᵢ : ℕ} {a : Unit} : (knowledgeBounds limit Kᵢ).prop a ↔ Kᵢ < limit

def Constraint.actionBounds' {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Aᵢ : ℕ) : Constraint Unit

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.actionBounds'.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Aᵢ : ℕ} {a : Unit} : (actionBounds' C Aᵢ).prop a ↔ Aᵢ < C.actions.size

def Constraint.stateBounds' {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint Unit

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.stateBounds'.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Sᵢ : ℕ} {a : Unit} : (stateBounds' C Sᵢ).prop a ↔ Sᵢ < C.states.size

@[reducible, inline]

abbrev Constraint.setBounds' {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (S : Validator.SetType) : ℕ → Constraint Unit

Equations

• Constraint.setBounds' C Validator.SetType.Actions x✝ = Constraint.actionBounds' C x✝
• Constraint.setBounds' C Validator.SetType.States x✝ = Constraint.stateBounds' C x✝

def Constraint.isActionAll {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Aᵢ : ℕ) : Constraint Unit

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isActionAll.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Aᵢ : ℕ} {a : Unit} : (isActionAll C Aᵢ).prop a ↔ Aᵢ < C.actions.size ∧ C.actions[Aᵢ]? = some Validator.ActionSetExpr.all

def Constraint.isActionUnion {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Aᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isActionUnion.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Aᵢ A'ᵢ A''ᵢ : ℕ} : (isActionUnion C Aᵢ).prop (A'ᵢ, A''ᵢ) ↔ Aᵢ < C.actions.size ∧ C.actions[Aᵢ]? = some (Validator.ActionSetExpr.union A'ᵢ A''ᵢ)

def Constraint.isStateEmpty {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint Unit

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isStateEmpty.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Sᵢ : ℕ} {a : Unit} : (isStateEmpty C Sᵢ).prop a ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some Validator.StateSetExpr.empty

def Constraint.isStateInit {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint Unit

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isStateInit.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Sᵢ : ℕ} {a : Unit} : (isStateInit C Sᵢ).prop a ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some Validator.StateSetExpr.init

def Constraint.isStateGoal {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint Unit

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isStateGoal.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Sᵢ : ℕ} {a : Unit} : (isStateGoal C Sᵢ).prop a ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some Validator.StateSetExpr.goal

def Constraint.isStateNeg {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint ℕ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isStateNeg.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Sᵢ S'ᵢ : ℕ} : (isStateNeg C Sᵢ).prop S'ᵢ ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some (Validator.StateSetExpr.neg S'ᵢ)

def Constraint.isStateInter {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isStateInter.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Sᵢ S'ᵢ S''ᵢ : ℕ} : (isStateInter C Sᵢ).prop (S'ᵢ, S''ᵢ) ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some (Validator.StateSetExpr.inter S'ᵢ S''ᵢ)

def Constraint.isStateUnion {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isStateUnion.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Sᵢ S'ᵢ S''ᵢ : ℕ} : (isStateUnion C Sᵢ).prop (S'ᵢ, S''ᵢ) ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some (Validator.StateSetExpr.union S'ᵢ S''ᵢ)

def Constraint.isStateProgr {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isStateProgr.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Sᵢ S'ᵢ Aᵢ : ℕ} : (isStateProgr C Sᵢ).prop (S'ᵢ, Aᵢ) ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some (Validator.StateSetExpr.progr S'ᵢ Aᵢ)

def Constraint.isStateRegr {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Sᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isStateRegr.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Sᵢ S'ᵢ Aᵢ : ℕ} : (isStateRegr C Sᵢ).prop (S'ᵢ, Aᵢ) ↔ Sᵢ < C.states.size ∧ C.states[Sᵢ]? = some (Validator.StateSetExpr.regr S'ᵢ Aᵢ)

@[reducible, inline]

abbrev Constraint.isUnion {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) : Validator.SetType → ℕ → Constraint (ℕ × ℕ)

Equations

• Constraint.isUnion C Validator.SetType.Actions = Constraint.isActionUnion C
• Constraint.isUnion C Validator.SetType.States = Constraint.isStateUnion C

def Constraint.isDeadKnowledge {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Kᵢ : ℕ) : Constraint ℕ

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isDeadKnowledge.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Kᵢ Sᵢ : ℕ} : (isDeadKnowledge C Kᵢ).prop Sᵢ = ∃ (K : Validator.DeadKnowledge Sᵢ), C.knowledge[Kᵢ]? = some (Validator.Knowledge.dead Sᵢ K)

def Constraint.isActionSubsetKnowledge {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Kᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isActionSubsetKnowledge.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Kᵢ Aᵢ A'ᵢ : ℕ} : (isActionSubsetKnowledge C Kᵢ).prop (Aᵢ, A'ᵢ) = ∃ (K : Validator.ActionSubsetKnowledge Aᵢ A'ᵢ), C.knowledge[Kᵢ]? = some (Validator.Knowledge.actionSubset Aᵢ A'ᵢ K)

def Constraint.isStateSubsetKnowledge {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) (Kᵢ : ℕ) : Constraint (ℕ × ℕ)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Constraint.isStateSubsetKnowledge.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Validator.Certificate pt} {Kᵢ Sᵢ S'ᵢ : ℕ} : (isStateSubsetKnowledge C Kᵢ).prop (Sᵢ, S'ᵢ) = ∃ (K : Validator.StateSubsetKnowledge Sᵢ S'ᵢ), C.knowledge[Kᵢ]? = some (Validator.Knowledge.stateSubset Sᵢ S'ᵢ K)

@[reducible, inline]

abbrev Constraint.isSubsetKnowledge {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Validator.Certificate pt) : Validator.SetType → ℕ → Constraint (ℕ × ℕ)

Equations

• Constraint.isSubsetKnowledge C Validator.SetType.Actions = Constraint.isActionSubsetKnowledge C
• Constraint.isSubsetKnowledge C Validator.SetType.States = Constraint.isStateSubsetKnowledge C