inductive Validator.StateSetFormalism : Type

• bdd : StateSetFormalism
• horn : StateSetFormalism
• mods : StateSetFormalism

@[implicit_reducible]

instance Validator.instDecidableEqStateSetFormalism : DecidableEq StateSetFormalism

Equations

• Validator.instDecidableEqStateSetFormalism x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Validator.StateSetFormalism.instToString : ToString StateSetFormalism

Equations

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

@[reducible, inline]

abbrev Validator.StateSetFormalism.type {n : ℕ} : STRIPS.PlanningTask n → StateSetFormalism → Type

Equations

• Validator.StateSetFormalism.type x✝ Validator.StateSetFormalism.bdd = Validator.BDD (2 * n)
• Validator.StateSetFormalism.type x✝ Validator.StateSetFormalism.horn = Validator.Horn (2 * n)
• Validator.StateSetFormalism.type x✝ Validator.StateSetFormalism.mods = Validator.MODS (2 * n)

@[implicit_reducible]

instance Validator.StateSetFormalism.BDD.instFormalism {n : ℕ} {pt : STRIPS.PlanningTask n} : Formalism pt (BDD (2 * n))

Equations

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

@[implicit_reducible]

instance Validator.StateSetFormalism.Horn.instFormalism {n : ℕ} {pt : STRIPS.PlanningTask n} : Formalism pt (Horn (2 * n))

Equations

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

@[implicit_reducible]

instance Validator.StateSetFormalism.MODS.instFormalism {n : ℕ} {pt : STRIPS.PlanningTask n} : Formalism pt (MODS (2 * n))

Equations

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

@[implicit_reducible]

instance Validator.StateSetFormalism.instFormalismType {n : ℕ} {pt : STRIPS.PlanningTask n} {R : StateSetFormalism} : Formalism pt (type pt R)

Equations

• Validator.StateSetFormalism.instFormalismType = Validator.StateSetFormalism.BDD.instFormalism
• Validator.StateSetFormalism.instFormalismType = Validator.StateSetFormalism.Horn.instFormalism
• Validator.StateSetFormalism.instFormalismType = Validator.StateSetFormalism.MODS.instFormalism

@[implicit_reducible]

instance Validator.StateSetFormalism.instBotHMulNatOfNatType {n : ℕ} {pt : STRIPS.PlanningTask n} {R : StateSetFormalism} : Formula.Bot (2 * n) (type pt R)

Equations

• Validator.StateSetFormalism.instBotHMulNatOfNatType = Validator.BDD.instBot
• Validator.StateSetFormalism.instBotHMulNatOfNatType = Validator.Horn.instBot
• Validator.StateSetFormalism.instBotHMulNatOfNatType = Validator.MODS.instBot

@[implicit_reducible]

instance Validator.StateSetFormalism.instClausalEntailmentHMulNatOfNatType {n : ℕ} {pt : STRIPS.PlanningTask n} {R : StateSetFormalism} : Formula.ClausalEntailment (2 * n) (type pt R)

Equations

• Validator.StateSetFormalism.instClausalEntailmentHMulNatOfNatType = Validator.BDD.instClausalEntailment
• Validator.StateSetFormalism.instClausalEntailmentHMulNatOfNatType = Validator.Horn.instClausalEntailment
• Validator.StateSetFormalism.instClausalEntailmentHMulNatOfNatType = Validator.MODS.instClausalEntailment

@[implicit_reducible]

instance Validator.StateSetFormalism.instImplicantHMulNatOfNatType {n : ℕ} {pt : STRIPS.PlanningTask n} {R : StateSetFormalism} : Formula.Implicant (2 * n) (type pt R)

Equations

• Validator.StateSetFormalism.instImplicantHMulNatOfNatType = Validator.BDD.instImplicant
• Validator.StateSetFormalism.instImplicantHMulNatOfNatType = Validator.Horn.instImplicant
• Validator.StateSetFormalism.instImplicantHMulNatOfNatType = Validator.MODS.instImplicant

@[implicit_reducible]

instance Validator.StateSetFormalism.instOfPartialModelHMulNatOfNatType {n : ℕ} {pt : STRIPS.PlanningTask n} {R : StateSetFormalism} : Formula.OfPartialModel (2 * n) (type pt R)

Equations

• Validator.StateSetFormalism.instOfPartialModelHMulNatOfNatType = Validator.BDD.instOfPartialModel
• Validator.StateSetFormalism.instOfPartialModelHMulNatOfNatType = Validator.Horn.instOfPartialModel
• Validator.StateSetFormalism.instOfPartialModelHMulNatOfNatType = Validator.MODS.instOfPartialModel

@[implicit_reducible]

instance Validator.StateSetFormalism.instRenameHMulNatOfNatType {n : ℕ} {pt : STRIPS.PlanningTask n} {R : StateSetFormalism} : Formula.Rename (2 * n) (type pt R)

Equations

• Validator.StateSetFormalism.instRenameHMulNatOfNatType = Validator.BDD.instRename
• Validator.StateSetFormalism.instRenameHMulNatOfNatType = Validator.Horn.instRename
• Validator.StateSetFormalism.instRenameHMulNatOfNatType = Validator.MODS.instRename

@[reducible, inline]

abbrev Validator.StateSetFormalism.UnprimedVariable' {n : ℕ} (pt : STRIPS.PlanningTask n) (R : StateSetFormalism) : Type

Equations

• Validator.StateSetFormalism.UnprimedVariable' pt R = Validator.Formalism.UnprimedVariable pt (Validator.StateSetFormalism.type pt R)

@[reducible, inline]

abbrev Validator.StateSetFormalism.UnprimedLiteral' {n : ℕ} (pt : STRIPS.PlanningTask n) (R : StateSetFormalism) : Type

Equations

• Validator.StateSetFormalism.UnprimedLiteral' pt R = Validator.Formalism.UnprimedLiteral pt (Validator.StateSetFormalism.type pt R)

@[reducible, inline]

abbrev Validator.StateSetFormalism.Variables' {n : ℕ} (pt : STRIPS.PlanningTask n) (R : StateSetFormalism) : Type

Equations

• Validator.StateSetFormalism.Variables' pt R = Validator.Formalism.Variables pt (Validator.StateSetFormalism.type pt R)

@[reducible, inline]

abbrev Validator.StateSetFormalism.UnprimedVariables' {n : ℕ} (pt : STRIPS.PlanningTask n) (R : StateSetFormalism) : Type

Equations

• Validator.StateSetFormalism.UnprimedVariables' pt R = Validator.Formalism.UnprimedVariables pt (Validator.StateSetFormalism.type pt R)

@[reducible, inline]

abbrev Validator.StateSetFormalism.UnprimedLiterals' {n : ℕ} (pt : STRIPS.PlanningTask n) (R : StateSetFormalism) : Type

Equations

• Validator.StateSetFormalism.UnprimedLiterals' pt R = Validator.Formalism.UnprimedLiterals pt (Validator.StateSetFormalism.type pt R)

def Validator.StateSetFormalism.mkEmpty {n : ℕ} (pt : STRIPS.PlanningTask n) (R : StateSetFormalism) : UnprimedVariable' pt R

Equations

• Validator.StateSetFormalism.mkEmpty pt R = ⟨Validator.Formula.Bot.bot (2 * n), ⋯⟩

@[simp]

theorem Validator.StateSetFormalism.toStates_mkEmpty {n : ℕ} (pt : STRIPS.PlanningTask n) (R : StateSetFormalism) : (↑(mkEmpty pt R)).toStates = ∅

def Validator.StateSetFormalism.mkInit {n : ℕ} (pt : STRIPS.PlanningTask n) (R : StateSetFormalism) : UnprimedVariable' pt R

Equations

• Validator.StateSetFormalism.mkInit pt R = ⟨Validator.Formula.OfPartialModel.ofPartialModel { pos := pt.init'.toUnprimed, neg := pt.init'ᶜ.toUnprimed, disjoint := ⋯ }, ⋯⟩

@[simp]

theorem Validator.StateSetFormalism.toStates_mkInit {n : ℕ} (pt : STRIPS.PlanningTask n) (R : StateSetFormalism) : (↑(mkInit pt R)).toStates = {pt.init}

def Validator.StateSetFormalism.mkGoal {n : ℕ} (pt : STRIPS.PlanningTask n) (R : StateSetFormalism) : UnprimedVariable' pt R

Equations

• Validator.StateSetFormalism.mkGoal pt R = Validator.Formalism.UnprimedVariable.ofVarSet (Validator.StateSetFormalism.type pt R) pt.goal'

@[simp]

theorem Validator.StateSetFormalism.toStates_mkGoal {n : ℕ} (pt : STRIPS.PlanningTask n) (R : StateSetFormalism) : (↑(mkGoal pt R)).toStates = pt.goalStates