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, ⋯⟩

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 Validator.VarSet'.IsUnprimed {n : ℕ} (V : VarSet' (2 * n)) : Prop

Equations

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

@[simp]

theorem Validator.VarSet'.isUnprimed_empty {n : ℕ} : empty.IsUnprimed

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

Equations

• V.toUnprimed = ⟨List.map Fin.toUnprimed ↑V, ⋯⟩

@[simp]

theorem Validator.VarSet'.toUnprimed_mem_toUnprimed_iff {n : ℕ} {V : VarSet' n} {i : Fin n} : i.toUnprimed ∈ ↑V.toUnprimed ↔ i ∈ ↑V

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

def Validator.VarSet'.unprimedVars (n : ℕ) : VarSet' (2 * n)

Equations

• Validator.VarSet'.unprimedVars n = ⟨List.ofFn Fin.toUnprimed, ⋯⟩

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

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

Equations

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

def Validator.Formula.Model.toPrimed {n : ℕ} (V : 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 / 2, ⋯⟩ ∈ ↑V then M ⟨↑i + 1, ⋯⟩ else M i

theorem Validator.Formula.Model.toPrimed_eq {n : ℕ} (V : 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 / 2, ⋯⟩ ∈ ↑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 ∈ ↑(VarSet'.unprimedVars n), M i = M' i

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

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

• vars (φ : R) : 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) : States n
• toStates_eq (φ : R) : toStates pt φ = Formula.Model.unprimedState '' Formula.models φ

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

Equations

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

@[reducible, inline]

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

Equations

• Validator.Formalism.Variable pt R = R

def Validator.Formalism.Variable.models {n : ℕ} {pt : STRIPS 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 n} {R : Type} [Formalism pt R] : Variable pt R → VarSet' (2 * n)

Equations

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

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

Equations

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

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

instance Validator.Formalism.Variable.instMembershipFinHMulNatOfNat {n : ℕ} {pt : STRIPS 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 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 n} (R : Type) [Formalism pt R] [h : Formula.OfPartialModel (2 * n) R] (V : VarSet' n) (pos : Bool := true) : UnprimedVariable pt R

Equations

• Validator.Formalism.UnprimedVariable.ofVarset' R V pos = ⟨Validator.Formula.OfPartialModel.ofPartialModel V.toUnprimed (BitVec.fill (↑V.toUnprimed).length pos), ⋯⟩

@[simp]

theorem Validator.Formalism.UnprimedVariable.toUnprimed_mem_vars_ofVarSet' {n : ℕ} {pt : STRIPS n} {R : Type} [Formalism pt R] [h : Formula.OfPartialModel (2 * n) R] {V : VarSet' n} {pos : Bool} {i : Fin n} : i.toUnprimed ∈ ↑(↑(ofVarset' R V pos)).vars ↔ i ∈ ↑V

@[simp]

theorem Validator.Formalism.UnprimedVariable.mem_models_ofVarSet' {n : ℕ} {pt : STRIPS n} {R : Type} [Formalism pt R] [h : Formula.OfPartialModel (2 * n) R] {V : 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 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 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)

@[irreducible]

def Validator.Formalism.UnprimedVariable.toPrimedAux {n : ℕ} (oldVars : List (Fin (2 * n))) (h : ∀ i ∈ oldVars, Even ↑i) (toRename : List (Fin n)) : List (Fin (2 * n))

Equations

• One or more equations did not get rendered due to their size.
• Validator.Formalism.UnprimedVariable.toPrimedAux [] h_2 toRename = []
• Validator.Formalism.UnprimedVariable.toPrimedAux oldVars h [] = oldVars

theorem Validator.Formalism.UnprimedVariable.toPrimedAux_eq {n : ℕ} {oldVars : VarSet' (2 * n)} {h : ∀ i ∈ ↑oldVars, Even ↑i} {toRename : VarSet' n} : toPrimedAux (↑oldVars) h ↑toRename = List.map (fun (x : { x : Fin (2 * n) // x ∈ ↑oldVars }) => match x with | ⟨i, hi⟩ => if i ∈ ↑toRename.toUnprimed then have hi := ⋯; ⟨↑i + 1, hi⟩ else i) (↑oldVars).attach

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

Make all unprimed vars in x corresponding to the vars in V primed. TODO : clarify the difference between all kinds of variables.

Equations

• x.toPrimedOld V = Validator.Formula.RenamingOld.rename ↑x ⟨Validator.Formalism.UnprimedVariable.toPrimedAux ↑(↑x).vars ⋯ ↑V, ⋯⟩ ⋯

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

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

Make all unprimed vars in x corresponding to the vars in V primed. TODO : clarify the difference between all kinds of variables.

Equations

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

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

@[reducible, inline]

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

Equations

• Validator.Formalism.Literal pt R = (Validator.Formalism.Variable pt R × Bool)

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

Equations

• Validator.Formalism.Literal.models (X, true) = X.models
• Validator.Formalism.Literal.models (X, false) = X.modelsᶜ

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

Equations

• Validator.Formalism.Literal.toStates (X, true) = X.toStates
• Validator.Formalism.Literal.toStates (X, false) = X.toStatesᶜ

@[reducible, inline]

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

Equations

• Validator.Formalism.UnprimedLiteral pt R = (Validator.Formalism.UnprimedVariable pt R × Bool)

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

Equations

• Validator.Formalism.UnprimedLiteral.val (x_1, b) = (↑x_1, b)

def Validator.Formalism.UnprimedLiteral.pos {n : ℕ} {pt : STRIPS n} {R : Type} [Formalism pt R] (x : UnprimedVariable pt R) : UnprimedLiteral pt R

Equations

• Validator.Formalism.UnprimedLiteral.pos x = (x, true)

@[simp]

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

def Validator.Formalism.UnprimedLiteral.neg {n : ℕ} {pt : STRIPS n} {R : Type} [Formalism pt R] (x : UnprimedVariable pt R) : UnprimedLiteral pt R

Equations

• Validator.Formalism.UnprimedLiteral.neg x = (x, false)

@[simp]

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

theorem Validator.Formalism.UnprimedLiteral.toStates_eq {n : ℕ} {pt : STRIPS 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 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 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 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 n} {R : Type} [F : Formalism pt R] (X : Variables pt R) : States n

Equations

• X.inter = {s : Validator.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 n} {R : Type} [Formalism pt R] {X : Variables pt R} (s : 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 n} {R : Type} [F : Formalism pt R] : inter [] = Set.univ

@[simp]

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

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

Equations

• X.union = {s : Validator.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 n} {R : Type} [Formalism pt R] {X : Variables pt R} (s : 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 n} {R : Type} [F : Formalism pt R] : union [] = ∅

@[simp]

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

@[reducible, inline]

abbrev Validator.Formalism.UnprimedVariables {n : ℕ} (pt : STRIPS 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 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 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 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 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 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 n} {R : Type} [F : Formalism pt R] {X : UnprimedVariables pt R} {s : State n} : s ∈ X.val.inter ↔ ∀ x ∈ X, s ∈ (↑x).toStates

@[simp]

theorem Validator.Formalism.UnprimedVariables.inter_variables_append {n : ℕ} {pt : STRIPS 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 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 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 n} {R : Type} [F : Formalism pt R] [Formula.Rename (2 * n) R] (X : UnprimedVariables pt R) (V : 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 n} {R : Type} [F : Formalism pt R] [Formula.Rename (2 * n) R] {X : UnprimedVariables pt R} {V : VarSet' n} {s : 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 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 n} {R : Type} [Formalism pt R] (X : Variables pt R) : Literals pt R

Equations

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

instance Validator.Formalism.Literals.instAppend {n : ℕ} {pt : STRIPS 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_pos {n : ℕ} {pt : STRIPS 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 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 n} {R : Type} [Formalism pt R] (L : Literals pt R) : States n

Equations

• L.union = {s : Validator.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 n} {R : Type} [Formalism pt R] {ls : Literals pt R} {s : 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 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 n} {R : Type} [Formalism pt R] (L : Literals pt R) : States n

Equations

• L.inter = {s : Validator.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 n} {R : Type} [Formalism pt R] {L : Literals pt R} {s : 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 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 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 n} {R : Type} [Formalism pt R] : UnprimedLiterals pt R

Equations

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

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

Equations

• Validator.Formalism.UnprimedLiterals.single (X, true) = ([X], [])
• Validator.Formalism.UnprimedLiterals.single (X, false) = ([], [X])

@[simp]

theorem Validator.Formalism.UnprimedLiterals.union_single {n : ℕ} {pt : STRIPS 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 n} {R : Type} [Formalism pt R] {l : UnprimedLiteral pt R} : (single l).val.inter = l.val.toStates

instance Validator.Formalism.UnprimedLiterals.instAppend {n : ℕ} {pt : STRIPS 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.val_append {n : ℕ} {pt : STRIPS 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 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 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 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 n) (R : Type) [Formalism pt R] : States n → Prop

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

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

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

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

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

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

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

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

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

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

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

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

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