structure Validator.MODS (n : ℕ) : Type

• vars : STRIPS.VarSet n
• mods : List (Validator.Formula.PartialModel n)
• prop (M : Validator.Formula.PartialModel n) : M ∈ mods self → M.vars = vars self

def Validator.instDecidableEqMODS.decEq {n✝ : ℕ} (x✝ x✝¹ : MODS n✝) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Validator.instDecidableEqMODS {n✝ : ℕ} : DecidableEq (MODS n✝)

Equations

• Validator.instDecidableEqMODS = Validator.instDecidableEqMODS.decEq

@[implicit_reducible]

instance Validator.MODS.instFormula {n : ℕ} : Formula n (MODS n)

Equations

• Validator.MODS.instFormula = { vars := fun (φ : Validator.MODS n) => Validator.MODS.vars✝ φ, models := Validator.MODS.models✝, models_equiv_right := ⋯ }

@[implicit_reducible]

instance Validator.MODS.instTop {n : ℕ} : Formula.Top n (MODS n)

Equations

• Validator.MODS.instTop = { top := { vars := ∅, mods := [Validator.Formula.PartialModel.empty], prop := ⋯ }, models_top := ⋯ }

@[implicit_reducible]

instance Validator.MODS.instBot {n : ℕ} : Formula.Bot n (MODS n)

Equations

• Validator.MODS.instBot = { bot := { vars := ∅, mods := [], prop := ⋯ }, vars_bot := ⋯, models_bot := ⋯ }

@[implicit_reducible]

instance Validator.MODS.instClausalEntailment {n : ℕ} : Formula.ClausalEntailment n (MODS n)

Equations

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

@[implicit_reducible]

instance Validator.MODS.instImplicant {n : ℕ} : Formula.Implicant n (MODS n)

Equations

• Validator.MODS.instImplicant = { entails := fun (δ : Validator.Formula.Cube n) (φ : Validator.MODS n) => sorry, entails_iff := ⋯ }

@[implicit_reducible]

instance Validator.MODS.instBoundedConjuction {n : ℕ} : Formula.BoundedConjuction n (MODS n)

Equations

• Validator.MODS.instBoundedConjuction = { and := fun (φ ψ : Validator.MODS n) => sorry, models_and := ⋯ }

@[implicit_reducible]

instance Validator.MODS.instSententialEntailment {n : ℕ} : Formula.SententialEntailment n (MODS n)

Equations

• Validator.MODS.instSententialEntailment = { entails := fun (φ ψ : Validator.MODS n) => sorry, entails_iff := ⋯ }

@[implicit_reducible]

instance Validator.MODS.instOfPartialModel {n : ℕ} : Formula.OfPartialModel n (MODS n)

Equations

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

@[implicit_reducible]

instance Validator.MODS.instRename {n : ℕ} : Formula.Rename n (MODS n)

Equations

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

@[implicit_reducible]

instance Validator.MODS.instToCNF {n : ℕ} : Formula.ToCNF n (MODS n)

Equations

• Validator.MODS.instToCNF = { toCNF := sorry, models_toCNF := ⋯ }

@[implicit_reducible]

instance Validator.MODS.instToDNF {n : ℕ} : Formula.ToDNF n (MODS n)

Equations

• Validator.MODS.instToDNF = { toDNF := fun (φ : Validator.MODS n) => List.map Validator.Formula.PartialModel.toCube (Validator.MODS.mods✝ φ), models_toDNF := ⋯ }