inductive Validator.StateSetFormalism : Type

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

instance Validator.instDecidableEqStateSetFormalism : DecidableEq StateSetFormalism

Equations

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

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 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)

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

Equations

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

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

Equations

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

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

Equations

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

def Validator.StateSetFormalism.mkBDD {n : ℕ} (pt : STRIPS n) : Formalism.UnprimedVariable pt (BDD (2 * n))

Equations

• Validator.StateSetFormalism.mkBDD pt = ⟨{ vars := Validator.VarSet'.unprimedVars n }, ⋯⟩

instance Validator.StateSetFormalism.instFormalismType {n : ℕ} {pt : STRIPS 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

instance Validator.StateSetFormalism.instBotHMulNatOfNatType {n : ℕ} {pt : STRIPS 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

instance Validator.StateSetFormalism.instClausalEntailmentHMulNatOfNatType {n : ℕ} {pt : STRIPS 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

instance Validator.StateSetFormalism.instImplicantHMulNatOfNatType {n : ℕ} {pt : STRIPS 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

instance Validator.StateSetFormalism.instSententialEntailmentHMulNatOfNatType {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} : Formula.SententialEntailment (2 * n) (type pt R)

Equations

• Validator.StateSetFormalism.instSententialEntailmentHMulNatOfNatType = Validator.BDD.instSententialEntailment
• Validator.StateSetFormalism.instSententialEntailmentHMulNatOfNatType = Validator.Horn.instSententialEntailment
• Validator.StateSetFormalism.instSententialEntailmentHMulNatOfNatType = Validator.MODS.instSententialEntailment

instance Validator.StateSetFormalism.instOfPartialModelHMulNatOfNatType {n : ℕ} {pt : STRIPS 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

instance Validator.StateSetFormalism.instRenameHMulNatOfNatType {n : ℕ} {pt : STRIPS 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 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 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 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 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 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 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 n) (R : StateSetFormalism) : (↑(mkEmpty pt R)).toStates = ∅

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

Equations

• Validator.StateSetFormalism.mkInit pt R = ⟨Validator.Formula.OfPartialModel.ofPartialModel (Validator.VarSet'.unprimedVars n) (BitVec.cast ⋯ pt.init'), ⋯⟩

@[simp]

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

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

Equations

• Validator.StateSetFormalism.mkGoal pt R = ⟨Validator.Formula.OfPartialModel.ofPartialModel pt.goal'.toUnprimed (BitVec.allOnes (↑pt.goal'.toUnprimed).length), ⋯⟩

@[simp]

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