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

Equations

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

theorem Validator.Certificate.valid.conclusionDead {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Kᵢ : Fin C.knowledge.size) {Sᵢ : Fin C.states.size} (h : ∃ (K : DeadKnowledge ↑Sᵢ), C.knowledge[Kᵢ]? = some (Knowledge.dead (↑Sᵢ) K)) : conclusion Kᵢ ↔ ProofSystem.Dead pt (⋯.getStates Sᵢ)

theorem Validator.Certificate.valid.conclusionStateSubset {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Kᵢ : Fin C.knowledge.size) {Sᵢ S'ᵢ : Fin C.states.size} (h : ∃ (K : StateSubsetKnowledge ↑Sᵢ ↑S'ᵢ), C.knowledge[Kᵢ]? = some (Knowledge.stateSubset (↑Sᵢ) (↑S'ᵢ) K)) : conclusion Kᵢ ↔ ⋯.getStates Sᵢ ⊆ ⋯.getStates S'ᵢ

theorem Validator.Certificate.valid.conclusionActionSubset {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Kᵢ : Fin C.knowledge.size) {Aᵢ A'ᵢ : Fin C.actions.size} (h : ∃ (K : ActionSubsetKnowledge ↑Aᵢ ↑A'ᵢ), C.knowledge[Kᵢ]? = some (Knowledge.actionSubset (↑Aᵢ) (↑A'ᵢ) K)) : conclusion Kᵢ ↔ ⋯.getActions Aᵢ ⊆ ⋯.getActions A'ᵢ

theorem Validator.Certificate.valid.conclusionUnsolvable {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Kᵢ : Fin C.knowledge.size) (h : ∃ (K : UnsolvableKnowledge), C.knowledge[Kᵢ] = Knowledge.unsolvable K) : conclusion Kᵢ ↔ Unsolvable pt

@[irreducible]

def Validator.Certificate.valid.toDerivation {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Kᵢ : Fin C.knowledge.size) : ProofSystem.Derivation pt (conclusion Kᵢ)

Equations

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

theorem Validator.Certificate.valid.soundness' {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (Kᵢ : Fin C.knowledge.size) : conclusion Kᵢ

theorem Validator.Certificate.valid.soundness {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.valid) (h : C.IsUnsolvable) : Unsolvable pt