def Validator.Certificate.validSets.getFormalism {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) : List (Fin C.states.size) → StateSetFormalism

Equations

• hC.getFormalism [] = Validator.StateSetFormalism.mods
• hC.getFormalism (Sᵢ :: tail) = match Validator.Certificate.validSets.getFormalism'✝ hC Sᵢ with | none => hC.getFormalism tail | some F => F

def Validator.constraintB1 {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (S1ᵢ S2ᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Validator.constraintB1.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} {hC : C.validSets} {S1ᵢ S2ᵢ : ℕ} {a : Unit} : (constraintB1 hC S1ᵢ S2ᵢ).prop a ↔ S1ᵢ < C.states.size ∧ S2ᵢ < C.states.size ∧ ∃ (hS1ᵢ : S1ᵢ < C.states.size) (hS2ᵢ : S2ᵢ < C.states.size), have R := hC.getFormalism [⟨S1ᵢ, hS1ᵢ⟩, ⟨S2ᵢ, hS2ᵢ⟩]; Formalism.IsLiteralInter pt (StateSetFormalism.type pt R) (hC.getStates ⟨S1ᵢ, hS1ᵢ⟩) ∧ Formalism.IsLiteralUnion pt (StateSetFormalism.type pt R) (hC.getStates ⟨S2ᵢ, hS2ᵢ⟩) ∧ hC.getStates ⟨S1ᵢ, hS1ᵢ⟩ ⊆ hC.getStates ⟨S2ᵢ, hS2ᵢ⟩

def Validator.constraintB2 {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (S1ᵢ S2ᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Validator.constraintB2.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} {hC : C.validSets} {S1ᵢ S2ᵢ : ℕ} {a : Unit} : (constraintB2 hC S1ᵢ S2ᵢ).prop a ↔ S1ᵢ < C.states.size ∧ S2ᵢ < C.states.size ∧ ∃ (hS1ᵢ : S1ᵢ < C.states.size) (hS2ᵢ : S2ᵢ < C.states.size), have R := hC.getFormalism [⟨S1ᵢ, hS1ᵢ⟩, ⟨S2ᵢ, hS2ᵢ⟩]; Formalism.IsProgrInter pt (StateSetFormalism.type pt R) (hC.getStates ⟨S1ᵢ, hS1ᵢ⟩) ∧ Formalism.IsLiteralUnion pt (StateSetFormalism.type pt R) (hC.getStates ⟨S2ᵢ, hS2ᵢ⟩) ∧ hC.getStates ⟨S1ᵢ, hS1ᵢ⟩ ⊆ hC.getStates ⟨S2ᵢ, hS2ᵢ⟩

def Validator.constraintB3 {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (S1ᵢ S2ᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Validator.constraintB3.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} {hC : C.validSets} {S1ᵢ S2ᵢ : ℕ} {a : Unit} : (constraintB3 hC S1ᵢ S2ᵢ).prop a ↔ S1ᵢ < C.states.size ∧ S2ᵢ < C.states.size ∧ ∃ (hS1ᵢ : S1ᵢ < C.states.size) (hS2ᵢ : S2ᵢ < C.states.size), have R := hC.getFormalism [⟨S1ᵢ, hS1ᵢ⟩, ⟨S2ᵢ, hS2ᵢ⟩]; Formalism.IsRegrInter pt (StateSetFormalism.type pt R) (hC.getStates ⟨S1ᵢ, hS1ᵢ⟩) ∧ Formalism.IsLiteralUnion pt (StateSetFormalism.type pt R) (hC.getStates ⟨S2ᵢ, hS2ᵢ⟩) ∧ hC.getStates ⟨S1ᵢ, hS1ᵢ⟩ ⊆ hC.getStates ⟨S2ᵢ, hS2ᵢ⟩

def Validator.constraintB4 {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (S1ᵢ S2ᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Validator.constraintB4.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} {hC : C.validSets} {S1ᵢ S2ᵢ : ℕ} {a : Unit} : (constraintB4 hC S1ᵢ S2ᵢ).prop a ↔ S1ᵢ < C.states.size ∧ S2ᵢ < C.states.size ∧ ∃ (hS1ᵢ : S1ᵢ < C.states.size) (hS2ᵢ : S2ᵢ < C.states.size), have R1 := hC.getFormalism [⟨S1ᵢ, hS1ᵢ⟩]; have R2 := hC.getFormalism [⟨S2ᵢ, hS2ᵢ⟩]; Formalism.IsLiteral pt (StateSetFormalism.type pt R1) (hC.getStates ⟨S1ᵢ, hS1ᵢ⟩) ∧ Formalism.IsLiteral pt (StateSetFormalism.type pt R2) (hC.getStates ⟨S2ᵢ, hS2ᵢ⟩) ∧ hC.getStates ⟨S1ᵢ, hS1ᵢ⟩ ⊆ hC.getStates ⟨S2ᵢ, hS2ᵢ⟩

def Validator.constraintB5 {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (A1ᵢ A2ᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Validator.constraintB5.prop_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} {hC : C.validSets} {A1ᵢ A2ᵢ : ℕ} {u : Unit} : (constraintB5 hC A1ᵢ A2ᵢ).prop u ↔ A1ᵢ < C.actions.size ∧ A2ᵢ < C.actions.size ∧ ∃ (hA1ᵢ : A1ᵢ < C.actions.size) (hA2ᵢ : A2ᵢ < C.actions.size), hC.getActions ⟨A1ᵢ, hA1ᵢ⟩ ⊆ hC.getActions ⟨A2ᵢ, hA2ᵢ⟩