def Validator.Certificate.constraintUD {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ S1ᵢ K1ᵢ K2ᵢ : ℕ) : Constraint (Unit × Unit × (ℕ × ℕ) × Unit × Unit)

Equations

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

def Validator.Certificate.constraintSD {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ Sᵢ K1ᵢ K2ᵢ : ℕ) : Constraint (Unit × Unit × Unit × ℕ × Unit)

Equations

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

def Validator.Certificate.constraintPG {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ Sᵢ K1ᵢ K2ᵢ K3ᵢ : ℕ) : Constraint (Unit × Unit × Unit × Unit × (ℕ × ℕ) × ((ℕ × Unit) × ℕ × Unit) × ℕ × ℕ × Unit)

Equations

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

def Validator.Certificate.constraintPI {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ S1ᵢ K1ᵢ K2ᵢ K3ᵢ : ℕ) : Constraint (Unit × Unit × Unit × ℕ × ((ℕ × ℕ) × (ℕ × Unit) × ℕ × Unit) × ℕ × Unit)

Equations

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

def Validator.Certificate.constraintRG {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ S1ᵢ K1ᵢ K2ᵢ K3ᵢ : ℕ) : Constraint (Unit × Unit × Unit × (ℕ × (ℕ × ℕ) × (ℕ × Unit) × ℕ × Unit) × ℕ × ℕ × Unit)

Equations

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

def Validator.Certificate.constraintRI {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ Sᵢ K1ᵢ K2ᵢ K3ᵢ : ℕ) : Constraint (Unit × Unit × Unit × Unit × (ℕ × ℕ) × (ℕ × Unit) × (ℕ × Unit) × (ℕ × ℕ) × Unit × Unit)

Equations

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

def Validator.Certificate.constraintUR {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (T : SetType) (Eᵢ E1ᵢ : ℕ) : Constraint (Unit × ℕ)

Equations

• C.constraintUR T Eᵢ E1ᵢ = Constraint.setBounds' C T Eᵢ∧ᶜ(Constraint.isUnion C T E1ᵢ).leftEq T Eᵢ

def Validator.Certificate.constraintUL {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (T : SetType) (Eᵢ E1ᵢ : ℕ) : Constraint (Unit × ℕ)

Equations

• C.constraintUL T Eᵢ E1ᵢ = Constraint.setBounds' C T Eᵢ∧ᶜ(Constraint.isUnion C T E1ᵢ).rightEq T Eᵢ

def Validator.Certificate.constraintIR {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (S1ᵢ Sᵢ : ℕ) : Constraint (Unit × ℕ)

Equations

• C.constraintIR S1ᵢ Sᵢ = Constraint.stateBounds' C Sᵢ∧ᶜ(Constraint.isStateInter C S1ᵢ).leftEqState Sᵢ

def Validator.Certificate.constraintIL {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (S1ᵢ Sᵢ : ℕ) : Constraint (Unit × ℕ)

Equations

• C.constraintIL S1ᵢ Sᵢ = Constraint.stateBounds' C Sᵢ∧ᶜ(Constraint.isStateInter C S1ᵢ).rightEqState Sᵢ

def Validator.Certificate.constraintDI {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (S1ᵢ S2ᵢ : ℕ) : Constraint ((ℕ × ℕ) × (ℕ × ℕ) × (ℕ × ℕ) × Unit × Unit)

Equations

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

def Validator.Certificate.constraintSU {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (T : SetType) (Kᵢ E1ᵢ E''ᵢ K1ᵢ K2ᵢ : ℕ) : Constraint (Unit × Unit × Unit × (ℕ × ℕ) × Unit × Unit)

Equations

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

def Validator.Certificate.constraintSI {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ Sᵢ S1ᵢ K1ᵢ K2ᵢ : ℕ) : Constraint (Unit × Unit × Unit × (ℕ × ℕ) × Unit × Unit)

Equations

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

def Validator.Certificate.constraintST {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (T : SetType) (Kᵢ Eᵢ E''ᵢ K1ᵢ K2ᵢ : ℕ) : Constraint (Unit × Unit × Unit × Unit × ℕ × Unit)

Equations

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

def Validator.Certificate.constraintAT {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ S1ᵢ S'ᵢ K1ᵢ K2ᵢ : ℕ) : Constraint (Unit × Unit × Unit × (ℕ × ℕ) × ℕ × ℕ × Unit)

Equations

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

def Validator.Certificate.constraintAU {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ S1ᵢ S'ᵢ K1ᵢ K2ᵢ : ℕ) : Constraint (Unit × Unit × Unit × (ℕ × ℕ) × (ℕ × ℕ) × (ℕ × Unit) × ℕ × Unit)

Equations

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

def Validator.Certificate.constraintPT {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ S1ᵢ S''ᵢ K1ᵢ K2ᵢ : ℕ) : Constraint (Unit × Unit × Unit × (ℕ × ℕ) × ℕ × ℕ × Unit)

Equations

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

def Validator.Certificate.constraintPU {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ S1ᵢ S''ᵢ K1ᵢ K2ᵢ : ℕ) : Constraint (Unit × Unit × Unit × (ℕ × ℕ) × (ℕ × ℕ) × (ℕ × Unit) × ℕ × Unit)

Equations

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

def Validator.Certificate.constraintPR {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ S1ᵢ S2ᵢ K1ᵢ : ℕ) : Constraint (Unit × (ℕ × ℕ) × ℕ × ℕ × ℕ × Unit)

Equations

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

def Validator.Certificate.constraintRP {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ S1ᵢ S'ᵢ K1ᵢ : ℕ) : Constraint (Unit × Unit × (ℕ × ℕ) × (ℕ × ℕ) × (ℕ × Unit) × Unit)

Equations

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

def Validator.Certificate.constraintCI {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ K1ᵢ : ℕ) : Constraint (Unit × ℕ × Unit)

Equations

• C.constraintCI Kᵢ K1ᵢ = Constraint.knowledgeBounds Kᵢ K1ᵢ∧ᶜ(Constraint.isDeadKnowledge C K1ᵢ).seq fun (SIᵢ : ℕ) => Constraint.isStateInit C SIᵢ

def Validator.Certificate.constraintCG {n : ℕ} {pt : STRIPS n} (C : Certificate pt) (Kᵢ K1ᵢ : ℕ) : Constraint (Unit × ℕ × Unit)

Equations

• C.constraintCG Kᵢ K1ᵢ = Constraint.knowledgeBounds Kᵢ K1ᵢ∧ᶜ(Constraint.isDeadKnowledge C K1ᵢ).seq fun (SGᵢ : ℕ) => Constraint.isStateGoal C SGᵢ

def Validator.Certificate.constraintKnowledge {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Kᵢ : Fin C.knowledge.size) : (α : Type) × Constraint α

Equations

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

def Validator.Certificate.validKnowledge {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Kᵢ : Fin C.knowledge.size) : Prop

Equations

• Validator.Certificate.validKnowledge hC Kᵢ = (Validator.Certificate.constraintKnowledge hC Kᵢ).snd.valid

structure Validator.Certificate.valid {n : ℕ} {pt : STRIPS n} (C : Certificate pt) extends C.validSets : Prop

• validActions (Aᵢ : Fin C.actions.size) : C.validActionSetExpr Aᵢ
• validStates (Sᵢ : Fin C.states.size) : C.validStateSetExpr Sᵢ
• validKnowledge (Kᵢ : Fin C.knowledge.size) : Certificate.validKnowledge ⋯ Kᵢ

theorem Validator.Certificate.valid.actionUnionBounds {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Aᵢ : Fin C.actions.size) {A'ᵢ A''ᵢ : ℕ} (h : C.actions[Aᵢ]? = some (ActionSetExpr.union A'ᵢ A''ᵢ)) : A'ᵢ < C.actions.size ∧ A''ᵢ < C.actions.size

theorem Validator.Certificate.valid.stateUnionBounds {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Sᵢ : Fin C.states.size) {S'ᵢ S''ᵢ : ℕ} (h : C.states[Sᵢ]? = some (StateSetExpr.union S'ᵢ S''ᵢ)) : S'ᵢ < C.states.size ∧ S''ᵢ < C.states.size

theorem Validator.Certificate.valid.stateInterBounds {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Sᵢ : Fin C.states.size) {S'ᵢ S''ᵢ : ℕ} (h : C.states[Sᵢ]? = some (StateSetExpr.inter S'ᵢ S''ᵢ)) : S'ᵢ < C.states.size ∧ S''ᵢ < C.states.size

theorem Validator.Certificate.valid.stateProgrBounds {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Sᵢ : Fin C.states.size) {S'ᵢ Aᵢ : ℕ} (h : C.states[Sᵢ]? = some (StateSetExpr.progr S'ᵢ Aᵢ)) : S'ᵢ < C.states.size ∧ Aᵢ < C.actions.size

theorem Validator.Certificate.valid.deadKnowledgeBound {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Kᵢ : Fin C.knowledge.size) {Sᵢ : ℕ} (h : ∃ (K : DeadKnowledge Sᵢ), C.knowledge[Kᵢ]? = some (Knowledge.dead Sᵢ K)) : Sᵢ < C.states.size

theorem Validator.Certificate.valid.actionSubsetKnowledgeBounds {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Kᵢ : Fin C.knowledge.size) {Aᵢ A'ᵢ : ℕ} (h : ∃ (K : ActionSubsetKnowledge Aᵢ A'ᵢ), C.knowledge[Kᵢ]? = some (Knowledge.actionSubset Aᵢ A'ᵢ K)) : Aᵢ < C.actions.size ∧ A'ᵢ < C.actions.size

theorem Validator.Certificate.valid.stateSubsetKnowledgeBounds {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Kᵢ : Fin C.knowledge.size) {Sᵢ S'ᵢ : ℕ} (h : ∃ (K : StateSubsetKnowledge Sᵢ S'ᵢ), C.knowledge[Kᵢ]? = some (Knowledge.stateSubset Sᵢ S'ᵢ K)) : Sᵢ < C.states.size ∧ S'ᵢ < C.states.size

def Validator.Certificate.verifyAll {k : ℕ} (h : Fin k → (α : Type) × Constraint α) : Result' (∀ (j : Fin k), (h j).snd.valid)

Equations

• Validator.Certificate.verifyAll h = do let __discr ← Validator.Certificate.verifyAll_aux✝ h (Fin.last k) match __discr with | ⟨PUnit.unit, h_1⟩ => pure ⟨(), ⋯⟩

def Validator.Certificate.verifyAll' {k : ℕ} {p : Fin k → Prop} (verify : (i : Fin k) → Result' (p i)) : Result' (∀ (i : Fin k), p i)

Equations

• Validator.Certificate.verifyAll' verify = do let __discr ← Validator.Certificate.verifyAll'_aux✝ verify (Fin.last k) match __discr with | ⟨PUnit.unit, h⟩ => pure ⟨(), ⋯⟩

@[reducible, inline]

abbrev Validator.Certificate.IsUnsolvable {n : ℕ} {pt : STRIPS n} (C : Certificate pt) : Prop

Equations

• C.IsUnsolvable = ∃ (Kᵢ : Fin C.knowledge.size) (K : Validator.UnsolvableKnowledge), C.knowledge[Kᵢ] = Validator.Knowledge.unsolvable K

@[irreducible]

def Validator.Certificate.verifyIsUnsolvable {n : ℕ} {pt : STRIPS n} (C : Certificate pt) : optParam (Fin (C.knowledge.size + 1)) (Fin.last C.knowledge.size) → Result' C.IsUnsolvable

Equations

• C.verifyIsUnsolvable ⟨0, ⋯⟩ = Validator.throwUnvalid "Unsolvability NOT proven"
• C.verifyIsUnsolvable ⟨Kᵢ.succ, h⟩ = match heq : C.knowledge[Kᵢ] with | Validator.Knowledge.unsolvable K => pure ⟨(), ⋯⟩ | x => C.verifyIsUnsolvable ⟨Kᵢ, ⋯⟩

def Validator.Certificate.verify {n : ℕ} {pt : STRIPS n} (C : Certificate pt) : Result' (C.valid ∧ C.IsUnsolvable)

Equations

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