inductive Validator.SetType : Type

• Actions : SetType
• States : SetType

def Validator.SetType.toIndexType : SetType → IndexType

Equations

• Validator.SetType.Actions.toIndexType = Validator.IndexType.ActionSet
• Validator.SetType.States.toIndexType = Validator.IndexType.StateSet

@[implicit_reducible]

instance Validator.instToStringSetType : ToString SetType

Equations

• Validator.instToStringSetType = { toString := fun (T : Validator.SetType) => toString T.toIndexType }

def Validator.Certificate.validActionSetExpr {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Certificate pt) (Aᵢ : Fin C.actions.size) : Prop

Equations

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

def Validator.Certificate.validStateSetExpr {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Certificate pt) (Sᵢ : Fin C.states.size) : Prop

Equations

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

def Validator.Certificate.verifyActionSetExpr {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Certificate pt) (Aᵢ : Fin C.actions.size) : ResultProp (C.validActionSetExpr Aᵢ)

Equations

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

def Validator.Certificate.verifyStateSetExpr {n : ℕ} {pt : STRIPS.PlanningTask n} (C : Certificate pt) (Sᵢ : Fin C.states.size) : ResultProp (C.validStateSetExpr Sᵢ)

Equations

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

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

• validActions (Aᵢ : Fin C.actions.size) : C.validActionSetExpr Aᵢ
• validStates (Sᵢ : Fin C.states.size) : C.validStateSetExpr Sᵢ

@[reducible, inline]

abbrev Validator.Certificate.validSets.ActionIds {n : ℕ} (pt : STRIPS.PlanningTask n) : Type

Equations

• Validator.Certificate.validSets.ActionIds pt = List (Fin pt.actions'.length)

def Validator.Certificate.validSets.ActionIds.toActions {n : ℕ} {pt : STRIPS.PlanningTask n} (A : ActionIds pt) : STRIPS.Actions n

Equations

• A.toActions = ↑(List.map (fun (x : Fin pt.actions'.length) => pt.actions'[x]) A).toFinset

@[simp]

theorem Validator.Certificate.validSets.ActionIds.mem_toActions {n : ℕ} {pt : STRIPS.PlanningTask n} (A : ActionIds pt) {a : STRIPS.Action n} : a ∈ A.toActions ↔ ∃ i ∈ A, pt.actions'[i] = a

@[irreducible]

def Validator.Certificate.validSets.getActionIds {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Aᵢ : Fin C.actions.size) : ActionIds pt

Equations

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

def Validator.Certificate.validSets.getActions {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Aᵢ : Fin C.actions.size) : STRIPS.Actions n

Equations

• hC.getActions Aᵢ = (hC.getActionIds Aᵢ).toActions

theorem Validator.Certificate.validSets.getActions_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} {hC : C.validSets} {Aᵢ : Fin C.actions.size} : hC.getActions Aᵢ = (hC.getActionIds Aᵢ).toActions

theorem Validator.Certificate.validSets.getActionsAll {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} {hC : C.validSets} (Aᵢ : Fin C.actions.size) (h : C.actions[Aᵢ]? = some ActionSetExpr.all) : hC.getActions Aᵢ = pt.actions

theorem Validator.Certificate.validSets.getActionsUnion {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} {hC : C.validSets} (Aᵢ A'ᵢ A''ᵢ : Fin C.actions.size) (h : C.actions[Aᵢ]? = some (ActionSetExpr.union ↑A'ᵢ ↑A''ᵢ)) : hC.getActions Aᵢ = hC.getActions A'ᵢ ∪ hC.getActions A''ᵢ

@[irreducible]

def Validator.Certificate.validSets.getStates {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) : STRIPS.States n

Equations

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

theorem Validator.Certificate.validSets.getStatesEmpty {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some StateSetExpr.empty) : hC.getStates Sᵢ = ∅

theorem Validator.Certificate.validSets.getStatesInit {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some StateSetExpr.init) : hC.getStates Sᵢ = {pt.init}

theorem Validator.Certificate.validSets.getStatesGoal {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some StateSetExpr.goal) : hC.getStates Sᵢ = pt.goalStates

theorem Validator.Certificate.validSets.getStatesBdd {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) {φ : Formalism.UnprimedVariable pt (BDD (2 * n))} (h : C.states[Sᵢ]? = some (StateSetExpr.bdd φ)) : hC.getStates Sᵢ = (↑φ).toStates

theorem Validator.Certificate.validSets.getStatesHorn {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) {φ : Formalism.UnprimedVariable pt (Horn (2 * n))} (h : C.states[Sᵢ]? = some (StateSetExpr.horn φ)) : hC.getStates Sᵢ = (↑φ).toStates

theorem Validator.Certificate.validSets.getStatesMods {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) {φ : Formalism.UnprimedVariable pt (MODS (2 * n))} (h : C.states[Sᵢ]? = some (StateSetExpr.mods φ)) : hC.getStates Sᵢ = (↑φ).toStates

theorem Validator.Certificate.validSets.getStatesNeg {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ S'ᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some (StateSetExpr.neg ↑S'ᵢ)) : hC.getStates Sᵢ = (hC.getStates S'ᵢ)ᶜ

theorem Validator.Certificate.validSets.getStatesInter {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ S'ᵢ S''ᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some (StateSetExpr.inter ↑S'ᵢ ↑S''ᵢ)) : hC.getStates Sᵢ = hC.getStates S'ᵢ ∩ hC.getStates S''ᵢ

theorem Validator.Certificate.validSets.getStatesUnion {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ S'ᵢ S''ᵢ : Fin C.states.size) (h : C.states[Sᵢ]? = some (StateSetExpr.union ↑S'ᵢ ↑S''ᵢ)) : hC.getStates Sᵢ = hC.getStates S'ᵢ ∪ hC.getStates S''ᵢ

theorem Validator.Certificate.validSets.getStatesProg {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ S'ᵢ : Fin C.states.size) (Aᵢ : Fin C.actions.size) (h : C.states[Sᵢ]? = some (StateSetExpr.progr ↑S'ᵢ ↑Aᵢ)) : hC.getStates Sᵢ = STRIPS.progression (hC.getStates S'ᵢ) (hC.getActions Aᵢ)

theorem Validator.Certificate.validSets.getStatesRegr {n : ℕ} {pt : STRIPS.PlanningTask n} {C : Certificate pt} (hC : C.validSets) (Sᵢ S'ᵢ : Fin C.states.size) (Aᵢ : Fin C.actions.size) (h : C.states[Sᵢ]? = some (StateSetExpr.regr ↑S'ᵢ ↑Aᵢ)) : hC.getStates Sᵢ = STRIPS.regression (hC.getStates S'ᵢ) (hC.getActions Aᵢ)