All variables i have a primed and an unprimed version, represented by 2 * i + 1 and 2 * i respectively.

def Fin.toUnprimed {n : ℕ} : Fin n → Fin (2 * n)

Equations

• i.toUnprimed = ⟨2 * ↑i, ⋯⟩

def Fin.divNat' {n m : ℕ} (i : Fin (m * n)) : Fin n

Equations

• i.divNat' = ⟨↑i / m, ⋯⟩

theorem Fin.toUnprimedStrictMono {n : ℕ} : StrictMono toUnprimed

def Fin.toPrimed {n : ℕ} (i : Fin (2 * n)) (h : Even ↑i) : Fin (2 * n)

Equations

• i.toPrimed h = ⟨↑i + 1, ⋯⟩

@[reducible, inline]

abbrev STRIPS.VarSet.IsUnprimed {n : ℕ} (V : VarSet (2 * n)) : Prop

Equations

• V.IsUnprimed = ∀ i ∈ V, Even ↑i

@[simp]

theorem STRIPS.VarSet.isUnprimed_empty {n : ℕ} : ∅.IsUnprimed

@[simp]

theorem STRIPS.VarSet.isUnprimed_union {n : ℕ} {V V' : VarSet (2 * n)} : (V ∪ V').IsUnprimed ↔ V.IsUnprimed ∧ V'.IsUnprimed

def STRIPS.VarSet.toUnprimed {n : ℕ} (V : VarSet n) : VarSet (2 * n)

Equations

• V.toUnprimed = STRIPS.VarSet.ofFn fun (i : Fin (2 * n)) => decide (Even ↑i ∧ i.divNat' ∈ V)

theorem STRIPS.VarSet.mem_toUnprimed {n : ℕ} {V : VarSet n} {i : Fin (2 * n)} : i ∈ V.toUnprimed ↔ Even ↑i ∧ i.divNat' ∈ V

@[simp]

theorem STRIPS.VarSet.toUnprimed_mem_toUnprimed_iff {n : ℕ} {V : VarSet n} {i : Fin n} : i.toUnprimed ∈ V.toUnprimed ↔ i ∈ V

theorem STRIPS.VarSet.isUnprimed_toUnprimed {n : ℕ} {V : VarSet n} : V.toUnprimed.IsUnprimed

def STRIPS.VarSet.unprimedVars (n : ℕ) : VarSet (2 * n)

Equations

• STRIPS.VarSet.unprimedVars n = STRIPS.VarSet.ofFn fun (i : Fin (2 * n)) => decide (Even ↑i)

theorem STRIPS.VarSet.mem_unprimedVars {n : ℕ} {i : Fin (2 * n)} : i ∈ unprimedVars n ↔ Even ↑i

theorem STRIPS.VarSet.isUnprimed_unprimedVars {n : ℕ} : (unprimedVars n).IsUnprimed

theorem STRIPS.VarSet.toUnprimed_mem_unprimedVars {n : ℕ} {i : Fin n} : i.toUnprimed ∈ unprimedVars n

def Validator.Formula.Model.unprimedState {n : ℕ} (M : Model (2 * n)) : STRIPS.State n

Equations

• M.unprimedState = {i : Fin n | M i.toUnprimed}

def Validator.Formula.Model.toPrimed {n : ℕ} (V : STRIPS.VarSet n) (M : Model (2 * n)) : Model (2 * n)

Swap the primed and unprimed versions of the variables in V and replace the other primed variables with their even version.

Equations

• Validator.Formula.Model.toPrimed V M i = if h : ¬Even ↑i then M ⟨↑i - 1, ⋯⟩ else if i.divNat' ∈ V then M ⟨↑i + 1, ⋯⟩ else M i

theorem Validator.Formula.Model.toPrimed_eq {n : ℕ} (V : STRIPS.VarSet n) (M : Model (2 * n)) : toPrimed V M = fun (i : Fin (2 * n)) => if h : ¬Even ↑i then M ⟨↑i - 1, ⋯⟩ else if i.divNat' ∈ V then M ⟨↑i + 1, ⋯⟩ else M i

theorem Validator.Formula.Model.unprimedState_eq_iff_unprimedVars {n : ℕ} {M M' : Model (2 * n)} : M.unprimedState = M'.unprimedState ↔ ∀ i ∈ STRIPS.VarSet.unprimedVars n, M i = M' i

theorem Validator.Formula.Model.exists_model_of_state {n : ℕ} (s : STRIPS.State n) : ∃ (M : Model (2 * n)), s = M.unprimedState

class Validator.Formalism {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) extends Validator.Formula (2 * n) R : Type

• vars (φ : R) : STRIPS.VarSet (2 * n)
• models (φ : R) : Models (2 * n)
• models_equiv_right (φ : R) (M M' : Model (2 * n)) : (∀ i ∈ vars φ, M i = M' i) → M ∈ models φ → M' ∈ models φ
• toStates (φ : R) : STRIPS.States n
• toStates_eq (φ : R) : toStates pt φ = Formula.Model.unprimedState '' Formula.models φ

@[implicit_reducible]

instance Validator.instFormalismStates {n : ℕ} {pt : STRIPS.PlanningTask n} : Formalism pt (STRIPS.States n)

Equations

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

@[reducible, inline]

abbrev Validator.Formalism.Variable {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : Type

Equations

• Validator.Formalism.Variable pt R = R

def Validator.Formalism.Variable.models {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : Variable pt R → Formula.Models (2 * n)

Equations

• Validator.Formalism.Variable.models = Validator.Formula.models

@[reducible, inline]

abbrev Validator.Formalism.Variable.vars {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : Variable pt R → STRIPS.VarSet (2 * n)

Equations

• Validator.Formalism.Variable.vars = Validator.Formula.vars

def Validator.Formalism.Variable.toStates {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : Variable pt R → STRIPS.States n

Equations

• Validator.Formalism.Variable.toStates = Validator.Formalism.toStates pt

theorem Validator.Formalism.Variable.toStates_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {x : Variable pt R} : x.toStates = Formula.Model.unprimedState '' x.models

@[implicit_reducible]

instance Validator.Formalism.Variable.instMembershipFinHMulNatOfNat {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [F : Formalism pt R] : Membership (Fin (2 * n)) (Variable pt R)

Equations

• Validator.Formalism.Variable.instMembershipFinHMulNatOfNat = { mem := fun (x : Validator.Formalism.Variable pt R) (i : Fin (2 * n)) => i ∈ x.vars }

@[reducible, inline]

abbrev Validator.Formalism.UnprimedVariable {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [F : Formalism pt R] : Type

Equations

• Validator.Formalism.UnprimedVariable pt R = { x : Validator.Formalism.Variable pt R // x.vars.IsUnprimed }

def Validator.Formalism.UnprimedVariable.ofVarSet {n : ℕ} {pt : STRIPS.PlanningTask n} (R : Type) [Formalism pt R] [h : Formula.OfPartialModel (2 * n) R] (V : STRIPS.VarSet n) (pos : Bool := true) : UnprimedVariable pt R

Equations

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

@[simp]

theorem Validator.Formalism.UnprimedVariable.mem_vars_ofVarSet {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] [h : Formula.OfPartialModel (2 * n) R] {V : STRIPS.VarSet n} {pos : Bool} {i : Fin (2 * n)} : i ∈ (↑(ofVarSet R V pos)).vars ↔ Even ↑i ∧ i.divNat' ∈ V

@[simp]

theorem Validator.Formalism.UnprimedVariable.mem_models_ofVarSet {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] [h : Formula.OfPartialModel (2 * n) R] {V : STRIPS.VarSet n} {pos : Bool} {M : Formula.Model (2 * n)} : M ∈ (↑(ofVarSet R V pos)).models ↔ ∀ i ∈ V, i ∈ M.unprimedState ↔ pos = true

theorem Validator.Formalism.UnprimedVariable.mem_models_of_eq_toState {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {x : UnprimedVariable pt R} {M M' : Formula.Model (2 * n)} : M.unprimedState = M'.unprimedState → M ∈ (↑x).models → M' ∈ (↑x).models

theorem Validator.Formalism.UnprimedVariable.mem_models_iff_of_eq_unprimedState {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {x : Variable pt R} {M M' : Formula.Model (2 * n)} : x.vars.IsUnprimed → M.unprimedState = M'.unprimedState → (M ∈ x.models ↔ M' ∈ x.models)

def Validator.Formalism.UnprimedVariable.toPrimed {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] [Formula.Rename (2 * n) R] (x : UnprimedVariable pt R) (V : STRIPS.VarSet n) : Variable pt R

Equations

• x.toPrimed V = Validator.Formula.Rename.rename ↑x { rename := fun (i : Fin (2 * n)) => if h : Even ↑i ∧ i.divNat' ∈ V then i.toPrimed ⋯ else i, mono := ⋯ } ⋯

theorem Validator.Formalism.UnprimedVariable.mem_models_toPrimed_iff {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] [Formula.Rename (2 * n) R] {x : UnprimedVariable pt R} {V : STRIPS.VarSet n} {M : Formula.Model (2 * n)} : M ∈ (x.toPrimed V).models ↔ Formula.Model.toPrimed V M ∈ (↑x).models

inductive Validator.Formalism.Literal {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : Type

• pos {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : Variable pt R → Literal pt R
• neg {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : Variable pt R → Literal pt R

def Validator.Formalism.Literal.models {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : Literal pt R → Formula.Models (2 * n)

Equations

• (Validator.Formalism.Literal.pos X).models = X.models
• (Validator.Formalism.Literal.neg X).models = X.modelsᶜ

def Validator.Formalism.Literal.toStates {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : Literal pt R → STRIPS.States n

Equations

• (Validator.Formalism.Literal.pos X).toStates = X.toStates
• (Validator.Formalism.Literal.neg X).toStates = X.toStatesᶜ

@[simp]

theorem Validator.Formalism.Literal.models_pos {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {x : Variable pt R} : (pos x).models = x.models

@[simp]

theorem Validator.Formalism.Literal.models_neg {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {x : Variable pt R} : (neg x).models = x.modelsᶜ

@[simp]

theorem Validator.Formalism.Literal.toStates_pos {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {X : Variable pt R} : (pos X).toStates = X.toStates

@[simp]

theorem Validator.Formalism.Literal.toStates_neg {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {X : Variable pt R} : (neg X).toStates = X.toStatesᶜ

inductive Validator.Formalism.UnprimedLiteral {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : Type

• pos {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : UnprimedVariable pt R → UnprimedLiteral pt R
• neg {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : UnprimedVariable pt R → UnprimedLiteral pt R

def Validator.Formalism.UnprimedLiteral.val {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : UnprimedLiteral pt R → Literal pt R

Equations

• (Validator.Formalism.UnprimedLiteral.pos x_1).val = Validator.Formalism.Literal.pos ↑x_1
• (Validator.Formalism.UnprimedLiteral.neg x_1).val = Validator.Formalism.Literal.neg ↑x_1

@[simp]

theorem Validator.Formalism.UnprimedLiteral.val_pos {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {x : UnprimedVariable pt R} : (pos x).val = Literal.pos ↑x

@[simp]

theorem Validator.Formalism.UnprimedLiteral.val_neg {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {x : UnprimedVariable pt R} : (neg x).val = Literal.neg ↑x

theorem Validator.Formalism.UnprimedLiteral.toStates_eq {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {l : UnprimedLiteral pt R} : l.val.toStates = Formula.Model.unprimedState '' l.val.models

theorem Validator.Formalism.UnprimedLiteral.subset_states_iff_subset_models {n : ℕ} {pt : STRIPS.PlanningTask n} {R1 R2 : Type} [Formalism pt R1] [Formalism pt R2] (l1 : UnprimedLiteral pt R1) (l2 : UnprimedLiteral pt R2) : l1.val.toStates ⊆ l2.val.toStates ↔ l1.val.models ⊆ l2.val.models

@[reducible, inline]

abbrev Validator.Formalism.Variables {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : Type

Equations

• Validator.Formalism.Variables pt R = List (Validator.Formalism.Variable pt R)

def Validator.Formalism.Variables.single {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : Variable pt R → Variables pt R

Equations

• Validator.Formalism.Variables.single = List.singleton

def Validator.Formalism.Variables.inter {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [F : Formalism pt R] (X : Variables pt R) : STRIPS.States n

Equations

• X.inter = {s : STRIPS.State n | ∃ (M : Validator.Formula.Model (2 * n)), M.unprimedState = s ∧ ∀ x ∈ X, M ∈ x.models}

theorem Validator.Formalism.Variables.mem_inter {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {X : Variables pt R} (s : STRIPS.State n) : s ∈ X.inter ↔ ∃ (M : Formula.Model (2 * n)), M.unprimedState = s ∧ ∀ x ∈ X, M ∈ x.models

@[simp]

theorem Validator.Formalism.Variables.inter_empty {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [F : Formalism pt R] : inter [] = Set.univ

@[simp]

theorem Validator.Formalism.Variables.inter_single {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {x : Variable pt R} : (single x).inter = x.toStates

def Validator.Formalism.Variables.union {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [F : Formalism pt R] (X : Variables pt R) : STRIPS.States n

Equations

• X.union = {s : STRIPS.State n | ∃ (M : Validator.Formula.Model (2 * n)), M.unprimedState = s ∧ ∃ x ∈ X, M ∈ x.models}

theorem Validator.Formalism.Variables.mem_union {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {X : Variables pt R} (s : STRIPS.State n) : s ∈ X.union ↔ ∃ (M : Formula.Model (2 * n)), M.unprimedState = s ∧ ∃ x ∈ X, M ∈ x.models

@[simp]

theorem Validator.Formalism.Variables.union_empty {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [F : Formalism pt R] : union [] = ∅

@[simp]

theorem Validator.Formalism.Variables.union_single {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {x : Variable pt R} : (single x).union = x.toStates

@[reducible, inline]

abbrev Validator.Formalism.UnprimedVariables {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : Type

Equations

• Validator.Formalism.UnprimedVariables pt R = List (Validator.Formalism.UnprimedVariable pt R)

def Validator.Formalism.UnprimedVariables.val {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : UnprimedVariables pt R → Variables pt R

Equations

• X.val = do let a ← X pure ↑a

def Validator.Formalism.UnprimedVariables.single {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : UnprimedVariable pt R → UnprimedVariables pt R

Equations

• Validator.Formalism.UnprimedVariables.single = List.singleton

@[simp]

theorem Validator.Formalism.UnprimedVariables.val_single {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {x : UnprimedVariable pt R} : (single x).val = Variables.single ↑x

theorem Validator.Formalism.UnprimedVariables.val_append {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {L1 L2 : UnprimedVariables pt R} : (L1 ++ L2).val = L1.val ++ L2.val

@[simp]

theorem Validator.Formalism.UnprimedVariables.union_append {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {X1 X2 : UnprimedVariables pt R} : (X1 ++ X2).val.union = X1.val.union ∪ X2.val.union

@[simp]

theorem Validator.Formalism.UnprimedVariables.mem_inter {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [F : Formalism pt R] {X : UnprimedVariables pt R} {s : STRIPS.State n} : s ∈ X.val.inter ↔ ∀ x ∈ X, s ∈ (↑x).toStates

@[simp]

theorem Validator.Formalism.UnprimedVariables.inter_variables_append {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {X1 : Variables pt R} {X2 : UnprimedVariables pt R} : (X1 ++ X2.val).inter = X1.inter ∩ X2.val.inter

@[simp]

theorem Validator.Formalism.UnprimedVariables.inter_append {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {X1 X2 : UnprimedVariables pt R} : (X1 ++ X2).val.inter = X1.val.inter ∩ X2.val.inter

theorem Validator.Formalism.UnprimedVariables.inter_subset_union_iff_models {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [F : Formalism pt R] (X1 : Variables pt R) (X2 : UnprimedVariables pt R) : X1.inter ⊆ X2.val.union ↔ ∀ (M : Formula.Model (2 * n)), (∀ x ∈ X1, M ∈ Formula.models x) → ∃ x ∈ X2, M ∈ (↑x).models

def Validator.Formalism.UnprimedVariables.toPrimed {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [F : Formalism pt R] [Formula.Rename (2 * n) R] (X : UnprimedVariables pt R) (V : STRIPS.VarSet n) : Variables pt R

Equations

• X.toPrimed V = List.map (fun (x : Validator.Formalism.UnprimedVariable pt R) => x.toPrimed V) X

theorem Validator.Formalism.UnprimedVariables.mem_inter_toPrimed {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [F : Formalism pt R] [Formula.Rename (2 * n) R] {X : UnprimedVariables pt R} {V : STRIPS.VarSet n} {s : STRIPS.State n} : s ∈ (X.toPrimed V).inter ↔ ∃ s' ∈ X.val.inter, ∀ i ∉ V, i ∈ s' ↔ i ∈ s

@[reducible, inline]

abbrev Validator.Formalism.Literals {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : Type

Equations

• Validator.Formalism.Literals pt R = (Validator.Formalism.Variables pt R × Validator.Formalism.Variables pt R)

def Validator.Formalism.Literals.pos {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] (X : Variables pt R) : Literals pt R

Equations

• Validator.Formalism.Literals.pos X = (X, [])

@[implicit_reducible]

instance Validator.Formalism.Literals.instAppend {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : Append (Literals pt R)

Equations

• Validator.Formalism.Literals.instAppend = { append := fun (L1 L2 : Validator.Formalism.Literals pt R) => (L1.1 ++ L2.1, L1.2 ++ L2.2) }

@[simp]

theorem Validator.Formalism.Literals.append_def {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] (L1 L2 : Literals pt R) : L1 ++ L2 = (L1.1 ++ L2.1, L1.2 ++ L2.2)

@[simp]

theorem Validator.Formalism.Literals.append_pos {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {L1 L2 : Literals pt R} : (L1 ++ L2).1 = L1.1 ++ L2.1

@[simp]

theorem Validator.Formalism.Literals.append_neg {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {L1 L2 : Literals pt R} : (L1 ++ L2).2 = L1.2 ++ L2.2

def Validator.Formalism.Literals.union {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] (L : Literals pt R) : STRIPS.States n

Equations

• L.union = {s : STRIPS.State n | ∃ (M : Validator.Formula.Model (2 * n)), M.unprimedState = s ∧ ((∃ x ∈ L.1, M ∈ x.models) ∨ ∃ x ∈ L.2, M ∉ x.models)}

@[simp]

theorem Validator.Formalism.Literals.mem_union {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {ls : Literals pt R} {s : STRIPS.State n} : s ∈ ls.union ↔ ∃ (M : Formula.Model (2 * n)), M.unprimedState = s ∧ ((∃ x ∈ ls.1, M ∈ x.models) ∨ ∃ x ∈ ls.2, M ∉ x.models)

@[simp]

theorem Validator.Formalism.Literals.union_append {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {L1 L2 : Literals pt R} : (L1 ++ L2).union = L1.union ∪ L2.union

def Validator.Formalism.Literals.inter {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] (L : Literals pt R) : STRIPS.States n

Equations

• L.inter = {s : STRIPS.State n | ∃ (M : Validator.Formula.Model (2 * n)), M.unprimedState = s ∧ (∀ x ∈ L.1, M ∈ x.models) ∧ ∀ x ∈ L.2, M ∉ x.models}

@[simp]

theorem Validator.Formalism.Literals.mem_inter {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {L : Literals pt R} {s : STRIPS.State n} : s ∈ L.inter ↔ ∃ (M : Formula.Model (2 * n)), M.unprimedState = s ∧ (∀ x ∈ L.1, M ∈ x.models) ∧ ∀ x ∈ L.2, M ∉ x.models

@[reducible, inline]

abbrev Validator.Formalism.UnprimedLiterals {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : Type

Equations

• Validator.Formalism.UnprimedLiterals pt R = (Validator.Formalism.UnprimedVariables pt R × Validator.Formalism.UnprimedVariables pt R)

def Validator.Formalism.UnprimedLiterals.val {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : UnprimedLiterals pt R → Literals pt R

Equations

• Validator.Formalism.UnprimedLiterals.val (X, X') = (do let a ← X pure ↑a, do let a ← X' pure ↑a)

@[reducible, inline]

abbrev Validator.Formalism.UnprimedLiterals.empty {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : UnprimedLiterals pt R

Equations

• Validator.Formalism.UnprimedLiterals.empty = ([], [])

def Validator.Formalism.UnprimedLiterals.single {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : UnprimedLiteral pt R → UnprimedLiterals pt R

Equations

• Validator.Formalism.UnprimedLiterals.single (Validator.Formalism.UnprimedLiteral.pos x_1) = ([x_1], [])
• Validator.Formalism.UnprimedLiterals.single (Validator.Formalism.UnprimedLiteral.neg x_1) = ([], [x_1])

@[simp]

theorem Validator.Formalism.UnprimedLiterals.union_single {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {l : UnprimedLiteral pt R} : (single l).val.union = l.val.toStates

@[simp]

theorem Validator.Formalism.UnprimedLiterals.inter_single {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {l : UnprimedLiteral pt R} : (single l).val.inter = l.val.toStates

@[implicit_reducible]

instance Validator.Formalism.UnprimedLiterals.instAppend {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : Append (UnprimedLiterals pt R)

Equations

• Validator.Formalism.UnprimedLiterals.instAppend = { append := fun (L1 L2 : Validator.Formalism.UnprimedLiterals pt R) => (L1.1 ++ L2.1, L1.2 ++ L2.2) }

@[simp]

theorem Validator.Formalism.UnprimedLiterals.append_def {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] (L1 L2 : UnprimedLiterals pt R) : L1 ++ L2 = (L1.1 ++ L2.1, L1.2 ++ L2.2)

@[simp]

theorem Validator.Formalism.UnprimedLiterals.val_append {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {L1 L2 : UnprimedLiterals pt R} : (L1 ++ L2).val = L1.val ++ L2.val

@[simp]

theorem Validator.Formalism.UnprimedLiterals.union_val {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {L : UnprimedLiterals pt R} : L.val.union = L.1.val.union ∪ L.2.val.interᶜ

@[simp]

theorem Validator.Formalism.UnprimedLiterals.inter_val {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {L : UnprimedLiterals pt R} : L.val.inter = L.1.val.inter ∩ L.2.val.unionᶜ

@[simp]

theorem Validator.Formalism.UnprimedLiterals.inter_append {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {L1 L2 : UnprimedLiterals pt R} : (L1.val ++ L2.val).inter = L1.val.inter ∩ L2.val.inter

Note that this is not true for primed variables

inductive Validator.Formalism.IsVariable {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : STRIPS.States n → Prop

• empty {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : IsVariable pt R ∅
• init {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : IsVariable pt R {pt.init}
• goal {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] : IsVariable pt R pt.goalStates
• explicit {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] (φ : R) : IsVariable pt R (toStates pt φ)

inductive Validator.Formalism.IsLiteral {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : STRIPS.States n → Prop

• pos {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S : STRIPS.States n} : IsVariable pt R S → IsLiteral pt R S
• neg {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S : STRIPS.States n} : IsVariable pt R S → IsLiteral pt R Sᶜ

inductive Validator.Formalism.IsLiteralUnion {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : STRIPS.States n → Prop

• single {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S : STRIPS.States n} : IsLiteral pt R S → IsLiteralUnion pt R S
• union {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S S' : STRIPS.States n} : IsLiteralUnion pt R S → IsLiteralUnion pt R S' → IsLiteralUnion pt R (S ∪ S')

inductive Validator.Formalism.IsVariableInter {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : STRIPS.States n → Prop

• single {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S : STRIPS.States n} : IsVariable pt R S → IsVariableInter pt R S
• inter {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S S' : STRIPS.States n} : IsVariableInter pt R S → IsVariableInter pt R S' → IsVariableInter pt R (S ∩ S')

inductive Validator.Formalism.IsLiteralInter {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : STRIPS.States n → Prop

• single {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S : STRIPS.States n} : IsLiteral pt R S → IsLiteralInter pt R S
• inter {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S S' : STRIPS.States n} : IsLiteralInter pt R S → IsLiteralInter pt R S' → IsLiteralInter pt R (S ∩ S')

inductive Validator.Formalism.IsProgrInter {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : STRIPS.States n → Prop

• empty {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S : STRIPS.States n} {A : STRIPS.Actions n} : IsVariableInter pt R S → IsProgrInter pt R (STRIPS.progression S A)
• inter {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S S' : STRIPS.States n} {A : STRIPS.Actions n} : IsVariableInter pt R S → IsLiteralInter pt R S' → IsProgrInter pt R (STRIPS.progression S A ∩ S')

inductive Validator.Formalism.IsRegrInter {n : ℕ} (pt : STRIPS.PlanningTask n) (R : Type) [Formalism pt R] : STRIPS.States n → Prop

• empty {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S : STRIPS.States n} {A : STRIPS.Actions n} : IsVariableInter pt R S → IsRegrInter pt R (STRIPS.regression S A)
• inter {n : ℕ} {pt : STRIPS.PlanningTask n} {R : Type} [Formalism pt R] {S S' : STRIPS.States n} {A : STRIPS.Actions n} : IsVariableInter pt R S → IsLiteralInter pt R S' → IsRegrInter pt R (STRIPS.regression S A ∩ S')