@[irreducible]

def Validator.Certificate.validSets.get_formalism' {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (Sᵢ : Fin C.states.size) : Option StateSetFormalism

Returns none if the formula is constant

Equations

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

def Validator.Certificate.validSets.get_formalism {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) : List (Fin C.states.size) → StateSetFormalism

Equations

• hC.get_formalism [] = Validator.StateSetFormalism.mods
• hC.get_formalism (Sᵢ :: tail) = match hC.get_formalism' Sᵢ with | none => hC.get_formalism tail | some F => F

def Validator.Certificate.validSets.throwIncompatibleFormalism {α : outParam Type} {p : α → Prop} (R R' : StateSetFormalism) (Sᵢ : ℕ) : Result α p

Equations

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

def Validator.Certificate.validSets.get_variable {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (R : StateSetFormalism) (Sᵢ : Fin C.states.size) : Result (StateSetFormalism.UnprimedVariable' pt R) fun (x : StateSetFormalism.UnprimedVariable' pt R) => hC.getStates Sᵢ = (↑x).toStates ∧ Formalism.IsVariable pt (StateSetFormalism.type pt R) (hC.getStates Sᵢ)

Equations

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

def Validator.Certificate.validSets.get_literal {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (R : StateSetFormalism) (Sᵢ : Fin C.states.size) : Result (StateSetFormalism.UnprimedLiteral' pt R) fun (l : StateSetFormalism.UnprimedLiteral' pt R) => hC.getStates Sᵢ = (Formalism.UnprimedLiteral.val l).toStates ∧ Formalism.IsLiteral pt (StateSetFormalism.type pt R) (hC.getStates Sᵢ)

Equations

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

@[irreducible]

def Validator.Certificate.validSets.get_union_literals {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (R : StateSetFormalism) (Sᵢ : Fin C.states.size) : Result (StateSetFormalism.UnprimedLiterals' pt R) fun (L : StateSetFormalism.UnprimedLiterals' pt R) => hC.getStates Sᵢ = (Formalism.UnprimedLiterals.val L).union ∧ Formalism.IsLiteralUnion pt (StateSetFormalism.type pt R) (hC.getStates Sᵢ)

Equations

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

@[irreducible]

def Validator.Certificate.validSets.get_inter_literals {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (R : StateSetFormalism) (Sᵢ : Fin C.states.size) : Result (StateSetFormalism.UnprimedLiterals' pt R) fun (L : StateSetFormalism.UnprimedLiterals' pt R) => hC.getStates Sᵢ = (Formalism.UnprimedLiterals.val L).inter ∧ Formalism.IsLiteralInter pt (StateSetFormalism.type pt R) (hC.getStates Sᵢ)

Equations

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

@[irreducible]

def Validator.Certificate.validSets.get_inter_variables {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (R : StateSetFormalism) (Sᵢ : Fin C.states.size) : Result (StateSetFormalism.UnprimedVariables' pt R) fun (X : StateSetFormalism.UnprimedVariables' pt R) => hC.getStates Sᵢ = (Formalism.UnprimedVariables.val X).inter ∧ Formalism.IsVariableInter pt (StateSetFormalism.type pt R) (hC.getStates Sᵢ)

Equations

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

def Validator.Certificate.validSets.get_progression_variables {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (R : StateSetFormalism) (Sᵢ : Fin C.states.size) : Result (StateSetFormalism.UnprimedVariables' pt R × ActionIds pt) fun (x : StateSetFormalism.UnprimedVariables' pt R × ActionIds pt) => match x with | (X, A) => hC.getStates Sᵢ = pt.progression (Formalism.UnprimedVariables.val X).inter A.toActions ∧ Formalism.IsVariableInter pt (StateSetFormalism.type pt R) (Formalism.UnprimedVariables.val X).inter

Equations

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

def Validator.Certificate.validSets.get_progression_inter {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (R : StateSetFormalism) (Sᵢ : Fin C.states.size) : Result (StateSetFormalism.UnprimedVariables' pt R × ActionIds pt × StateSetFormalism.UnprimedLiterals' pt R) fun (x : StateSetFormalism.UnprimedVariables' pt R × ActionIds pt × StateSetFormalism.UnprimedLiterals' pt R) => match x with | (X, A, L) => hC.getStates Sᵢ = pt.progression (Formalism.UnprimedVariables.val X).inter A.toActions ∩ (Formalism.UnprimedLiterals.val L).inter ∧ Formalism.IsProgrInter pt (StateSetFormalism.type pt R) (hC.getStates Sᵢ)

Equations

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

def Validator.Certificate.validSets.get_regression_variables {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (R : StateSetFormalism) (Sᵢ : Fin C.states.size) : Result (StateSetFormalism.UnprimedVariables' pt R × ActionIds pt) fun (x : StateSetFormalism.UnprimedVariables' pt R × ActionIds pt) => match x with | (X, A) => hC.getStates Sᵢ = pt.regression (Formalism.UnprimedVariables.val X).inter A.toActions ∧ Formalism.IsVariableInter pt (StateSetFormalism.type pt R) (Formalism.UnprimedVariables.val X).inter

Equations

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

def Validator.Certificate.validSets.get_regression_inter {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (R : StateSetFormalism) (Sᵢ : Fin C.states.size) : Result (StateSetFormalism.UnprimedVariables' pt R × ActionIds pt × StateSetFormalism.UnprimedLiterals' pt R) fun (x : StateSetFormalism.UnprimedVariables' pt R × ActionIds pt × StateSetFormalism.UnprimedLiterals' pt R) => match x with | (X, A, L) => hC.getStates Sᵢ = pt.regression (Formalism.UnprimedVariables.val X).inter A.toActions ∩ (Formalism.UnprimedLiterals.val L).inter ∧ Formalism.IsRegrInter pt (StateSetFormalism.type pt R) (hC.getStates Sᵢ)

Equations

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

def Validator.Formalism.check_variables_subset1 {n : ℕ} {pt : STRIPS n} {R : Type} [F : Formalism pt R] [h1 : Formula.SententialEntailment (2 * n) R] [h2 : Formula.BoundedConjuction (2 * n) R] [Formula.Top (2 * n) R] [h3 : Formula.BoundedDisjunction (2 * n) R] [Formula.Bot (2 * n) R] (X1 : Variables pt R) (X2 : UnprimedVariables pt R) : Bool

Equations

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

theorem Validator.Formalism.check_variables_subset1_correct {n : ℕ} {pt : STRIPS n} {R : Type} [F : Formalism pt R] [h1 : Formula.SententialEntailment (2 * n) R] [h2 : Formula.BoundedConjuction (2 * n) R] [Formula.Top (2 * n) R] [h3 : Formula.BoundedDisjunction (2 * n) R] [Formula.Bot (2 * n) R] (X1 : Variables pt R) (X2 : UnprimedVariables pt R) : check_variables_subset1 X1 X2 = true ↔ X1.inter ⊆ X2.val.union

def Validator.Formalism.check_variables_subset2 {n : ℕ} {pt : STRIPS n} {R : Type} [F : Formalism pt R] [h1 : Formula.ClausalEntailment (2 * n) R] [h2 : Formula.BoundedConjuction (2 * n) R] [Formula.Top (2 * n) R] [h3 : Formula.ToCNF (2 * n) R] (X1 : Variables pt R) (X2 : UnprimedVariables pt R) : Bool

Equations

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

theorem Validator.Formalism.check_variables_subset2_correct {n : ℕ} {pt : STRIPS n} {R : Type} [F : Formalism pt R] [h1 : Formula.ClausalEntailment (2 * n) R] [h2 : Formula.BoundedConjuction (2 * n) R] [Formula.Top (2 * n) R] [h3 : Formula.ToCNF (2 * n) R] (X1 : Variables pt R) (X2 : UnprimedVariables pt R) : check_variables_subset2 X1 X2 = true ↔ X1.inter ⊆ X2.val.union

def Validator.Formalism.check_variables_subset3 {n : ℕ} {pt : STRIPS n} {R : Type} [F : Formalism pt R] [h1 : Formula.Implicant (2 * n) R] [h2 : Formula.BoundedDisjunction (2 * n) R] [Formula.Bot (2 * n) R] [h3 : Formula.ToDNF (2 * n) R] (X1 : Variables pt R) (X2 : UnprimedVariables pt R) : Bool

Equations

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

theorem Validator.Formalism.check_variables_subset3_correct {n : ℕ} {pt : STRIPS n} {R : Type} [F : Formalism pt R] [h1 : Formula.Implicant (2 * n) R] [h2 : Formula.BoundedDisjunction (2 * n) R] [Formula.Bot (2 * n) R] [h3 : Formula.ToDNF (2 * n) R] (X1 : Variables pt R) (X2 : UnprimedVariables pt R) : check_variables_subset3 X1 X2 = true ↔ X1.inter ⊆ X2.val.union

def Validator.Formalism.check_variable_subset_pos_pos_1 {n : ℕ} {pt : STRIPS n} {R1 R2 : Type} [Formalism pt R1] [Formalism pt R2] [h1 : Formula.ToDNF (2 * n) R1] [h2 : Formula.Implicant (2 * n) R2] (x1 : UnprimedVariable pt R1) (x2 : UnprimedVariable pt R2) : Result' ((↑x1).toStates ⊆ (↑x2).toStates)

Equations

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

def Validator.Formalism.check_variable_subset_pos_pos_2 {n : ℕ} {pt : STRIPS n} {R1 R2 : Type} [Formalism pt R1] [Formalism pt R2] [h1 : Formula.ClausalEntailment (2 * n) R1] [h2 : Formula.ToCNF (2 * n) R2] (x1 : UnprimedVariable pt R1) (x2 : UnprimedVariable pt R2) : Result' ((↑x1).toStates ⊆ (↑x2).toStates)

Equations

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

def Validator.Formalism.check_variable_subset_pos_neg_1 {n : ℕ} {pt : STRIPS n} {R1 R2 : Type} [Formalism pt R1] [Formalism pt R2] [h1 : Formula.ToDNF (2 * n) R1] [h2 : Formula.ClausalEntailment (2 * n) R2] (x1 : UnprimedVariable pt R1) (x2 : UnprimedVariable pt R2) : Result' ((↑x1).toStates ⊆ (↑x2).toStatesᶜ)

Equations

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

def Validator.Formalism.check_variable_subset_pos_neg_2 {n : ℕ} {pt : STRIPS n} {R1 R2 : Type} [Formalism pt R1] [Formalism pt R2] [h1 : Formula.ClausalEntailment (2 * n) R1] [h2 : Formula.ToDNF (2 * n) R2] (x1 : UnprimedVariable pt R1) (x2 : UnprimedVariable pt R2) : Result' ((↑x1).toStates ⊆ (↑x2).toStatesᶜ)

Equations

• Validator.Formalism.check_variable_subset_pos_neg_2 x1 x2 = do let __discr ← Validator.Formalism.check_variable_subset_pos_neg_1 x2 x1 match __discr with | ⟨PUnit.unit, h⟩ => pure ⟨(), ⋯⟩

def Validator.Formalism.check_variable_subset_neg_pos_1 {n : ℕ} {pt : STRIPS n} {R1 R2 : Type} [Formalism pt R1] [Formalism pt R2] [h1 : Formula.ToCNF (2 * n) R1] [h2 : Formula.Implicant (2 * n) R2] (x1 : UnprimedVariable pt R1) (x2 : UnprimedVariable pt R2) : Result' ((↑x1).toStatesᶜ ⊆ (↑x2).toStates)

Equations

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

def Validator.Formalism.check_variable_subset_neg_pos_2 {n : ℕ} {pt : STRIPS n} {R1 R2 : Type} [Formalism pt R1] [Formalism pt R2] [h1 : Formula.Implicant (2 * n) R1] [h2 : Formula.ToCNF (2 * n) R2] (x1 : UnprimedVariable pt R1) (x2 : UnprimedVariable pt R2) : Result' ((↑x1).toStatesᶜ ⊆ (↑x2).toStates)

Equations

• Validator.Formalism.check_variable_subset_neg_pos_2 x1 x2 = do let __discr ← Validator.Formalism.check_variable_subset_neg_pos_1 x2 x1 match __discr with | ⟨PUnit.unit, h⟩ => pure ⟨(), ⋯⟩

def Validator.StateSetFormalism.check_variables_subset {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (X1 : Variables' pt R) (X2 : UnprimedVariables' pt R) : Bool

Equations

• Validator.StateSetFormalism.bdd.check_variables_subset X1_2 X2_2 = Validator.Formalism.check_variables_subset1 X1_2 X2_2
• Validator.StateSetFormalism.horn.check_variables_subset X1_2 X2_2 = Validator.Formalism.check_variables_subset2 X1_2 X2_2
• Validator.StateSetFormalism.mods.check_variables_subset X1_2 X2_2 = Validator.Formalism.check_variables_subset2 X1_2 X2_2

theorem Validator.StateSetFormalism.check_variables_subset_correct {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (X1 : Variables' pt R) (X2 : UnprimedVariables' pt R) : R.check_variables_subset X1 X2 = true ↔ Formalism.Variables.inter X1 ⊆ (Formalism.UnprimedVariables.val X2).union

def Validator.StateSetFormalism.checkB1 {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (L1 L2 : UnprimedLiterals' pt R) : Bool

Equations

• R.checkB1 L1 L2 = R.check_variables_subset (L1.1 ++ L2.2).val (L2.1 ++ L1.2)

theorem Validator.StateSetFormalism.checkB1_correct {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) {L1 L2 : UnprimedLiterals' pt R} : R.checkB1 L1 L2 = true ↔ (Formalism.UnprimedLiterals.val L1).inter ⊆ (Formalism.UnprimedLiterals.val L2).union

def Validator.StateSetFormalism.preVariable {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (aᵢ : Fin (List.length pt.actions')) : UnprimedVariable' pt R

Equations

• R.preVariable aᵢ = Validator.Formalism.UnprimedVariable.ofVarset' (Validator.StateSetFormalism.type pt R) pt.actions'[aᵢ].pre'

@[simp]

theorem Validator.StateSetFormalism.mem_models_preVariable {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {aᵢ : Fin (List.length pt.actions')} {M : Formula.Model (2 * n)} : M ∈ (↑(R.preVariable aᵢ)).models ↔ pt.actions'[aᵢ].pre ⊆ M.unprimedState

@[simp]

theorem Validator.StateSetFormalism.mem_toStates_preVariable {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {aᵢ : Fin (List.length pt.actions')} {s : State n} : s ∈ (↑(R.preVariable aᵢ)).toStates ↔ pt.actions'[aᵢ].pre ⊆ s

def Validator.StateSetFormalism.addVariable {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (aᵢ : Fin (List.length pt.actions')) : UnprimedVariable' pt R

Equations

• R.addVariable aᵢ = Validator.Formalism.UnprimedVariable.ofVarset' (Validator.StateSetFormalism.type pt R) pt.actions'[aᵢ].add'

@[simp]

theorem Validator.StateSetFormalism.mem_models_addVariable {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {aᵢ : Fin (List.length pt.actions')} {M : Formula.Model (2 * n)} : M ∈ (↑(R.addVariable aᵢ)).models ↔ pt.actions'[aᵢ].add ⊆ M.unprimedState

@[simp]

theorem Validator.StateSetFormalism.mem_toStates_addVariable {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {aᵢ : Fin (List.length pt.actions')} {s : State n} : s ∈ (↑(R.addVariable aᵢ)).toStates ↔ pt.actions'[aᵢ].add ⊆ s

def Validator.StateSetFormalism.delVariable {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (aᵢ : Fin (List.length pt.actions')) : UnprimedVariable' pt R

Equations

• R.delVariable aᵢ = Validator.Formalism.UnprimedVariable.ofVarset' (Validator.StateSetFormalism.type pt R) (pt.actions'[aᵢ].del'.diff pt.actions'[aᵢ].add') false

@[simp]

theorem Validator.StateSetFormalism.mem_models_delVariable {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {aᵢ : Fin (List.length pt.actions')} {M : Formula.Model (2 * n)} : M ∈ (↑(R.delVariable aᵢ)).models ↔ pt.actions'[aᵢ].del \ pt.actions'[aᵢ].add ⊆ M.unprimedStateᶜ

@[simp]

theorem Validator.StateSetFormalism.mem_toStates_delVariable {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {aᵢ : Fin (List.length pt.actions')} {s : State n} : s ∈ (↑(R.delVariable aᵢ)).toStates ↔ pt.actions'[aᵢ].del \ pt.actions'[aᵢ].add ⊆ sᶜ

def Validator.StateSetFormalism.preVariables {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (aᵢ : Fin (List.length pt.actions')) : UnprimedVariables' pt R

Equations

• R.preVariables aᵢ = [R.preVariable aᵢ]

@[simp]

theorem Validator.StateSetFormalism.mem_preVariables {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {aᵢ : Fin (List.length pt.actions')} {x : Formalism.UnprimedVariable pt (type pt R)} : x ∈ R.preVariables aᵢ ↔ x = R.preVariable aᵢ

def Validator.StateSetFormalism.effectVariables {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (aᵢ : Fin (List.length pt.actions')) : UnprimedVariables' pt R

Equations

• R.effectVariables aᵢ = [R.addVariable aᵢ, R.delVariable aᵢ]

@[simp]

theorem Validator.StateSetFormalism.mem_effectVariables {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {aᵢ : Fin (List.length pt.actions')} {x : Formalism.UnprimedVariable pt (type pt R)} : x ∈ R.effectVariables aᵢ ↔ x = R.addVariable aᵢ ∨ x = R.delVariable aᵢ

def Validator.StateSetFormalism.effectVarSet' {n : ℕ} {pt : STRIPS n} (aᵢ : Fin (List.length pt.actions')) : VarSet' n

Equations

• Validator.StateSetFormalism.effectVarSet' aᵢ = pt.actions'[aᵢ].add'.union pt.actions'[aᵢ].del'

@[simp]

theorem Validator.StateSetFormalism.mem_effectVarSet' {n : ℕ} {pt : STRIPS n} {aᵢ : Fin (List.length pt.actions')} {i : Fin n} : i ∈ ↑(effectVarSet' aᵢ) ↔ i ∈ pt.actions'[aᵢ].add ∨ i ∈ pt.actions'[aᵢ].del

def Validator.StateSetFormalism.checkB2' {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (aᵢ : Fin (List.length pt.actions')) (X0 X1 X2 : UnprimedVariables' pt R) : Bool

Equations

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

theorem Validator.StateSetFormalism.checkB2'_correct {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {aᵢ : Fin (List.length pt.actions')} {X0 X1 X2 : UnprimedVariables' pt R} : R.checkB2' aᵢ X0 X1 X2 = true ↔ pt.progression' (Formalism.UnprimedVariables.val X0).inter pt.actions'[aᵢ] ∩ (Formalism.UnprimedVariables.val X1).inter ⊆ (Formalism.UnprimedVariables.val X2).union

def Validator.StateSetFormalism.checkB2 {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (X : UnprimedVariables' pt R) (A : Certificate.validSets.ActionIds pt) (L1 L2 : UnprimedLiterals' pt R) : Bool

Equations

• R.checkB2 X A L1 L2 = List.all A fun (aᵢ : Fin (List.length pt.actions')) => R.checkB2' aᵢ X (L1.1 ++ L2.2) (L2.1 ++ L1.2)

theorem Validator.StateSetFormalism.checkB2_correct {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {X : UnprimedVariables' pt R} {A : Certificate.validSets.ActionIds pt} {L1 L2 : UnprimedLiterals' pt R} : R.checkB2 X A L1 L2 = true ↔ pt.progression (Formalism.UnprimedVariables.val X).inter A.toActions ∩ (Formalism.UnprimedLiterals.val L1).inter ⊆ (Formalism.UnprimedLiterals.val L2).union

def Validator.StateSetFormalism.checkB3' {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (aᵢ : Fin (List.length pt.actions')) (X0 X1 X2 : UnprimedVariables' pt R) : Bool

Equations

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

theorem Validator.StateSetFormalism.checkB3'_correct {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {aᵢ : Fin (List.length pt.actions')} {X0 X1 X2 : UnprimedVariables' pt R} : R.checkB3' aᵢ X0 X1 X2 = true ↔ pt.regression' (Formalism.UnprimedVariables.val X0).inter pt.actions'[aᵢ] ∩ (Formalism.UnprimedVariables.val X1).inter ⊆ (Formalism.UnprimedVariables.val X2).union

def Validator.StateSetFormalism.checkB3 {n : ℕ} {pt : STRIPS n} (R : StateSetFormalism) (X : UnprimedVariables' pt R) (A : Certificate.validSets.ActionIds pt) (L1 L2 : UnprimedLiterals' pt R) : Bool

Equations

• R.checkB3 X A L1 L2 = List.all A fun (aᵢ : Fin (List.length pt.actions')) => R.checkB3' aᵢ X (L1.1 ++ L2.2) (L2.1 ++ L1.2)

theorem Validator.StateSetFormalism.checkB3_correct {n : ℕ} {pt : STRIPS n} {R : StateSetFormalism} {X : UnprimedVariables' pt R} {A : Certificate.validSets.ActionIds pt} {L1 L2 : UnprimedLiterals' pt R} : R.checkB3 X A L1 L2 = true ↔ pt.regression (Formalism.UnprimedVariables.val X).inter A.toActions ∩ (Formalism.UnprimedLiterals.val L1).inter ⊆ (Formalism.UnprimedLiterals.val L2).union

def Validator.StateSetFormalism.throwUnsuportedB4 {α : outParam Type} {p : α → Prop} (R1 R2 : StateSetFormalism) : Result α p

Equations

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

@[irreducible]

def Validator.StateSetFormalism.checkB4 {n : ℕ} {pt : STRIPS n} (R1 R2 : StateSetFormalism) (l1 : UnprimedLiteral' pt R1) (l2 : UnprimedLiteral' pt R2) : Result' ((Formalism.UnprimedLiteral.val l1).toStates ⊆ (Formalism.UnprimedLiteral.val l2).toStates)

Equations

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

def Validator.constraintB1 {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (S1ᵢ S2ᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Validator.constraintB1.prop_eq {n : ℕ} {pt : STRIPS n} {C : Certificate pt} {hC : C.validSets} {S1ᵢ S2ᵢ : ℕ} {a : Unit} : (constraintB1 hC S1ᵢ S2ᵢ).prop a ↔ S1ᵢ < C.states.size ∧ S2ᵢ < C.states.size ∧ ∃ (hS1ᵢ : S1ᵢ < C.states.size) (hS2ᵢ : S2ᵢ < C.states.size), have R := hC.get_formalism [⟨S1ᵢ, hS1ᵢ⟩, ⟨S2ᵢ, hS2ᵢ⟩]; Formalism.IsLiteralInter pt (StateSetFormalism.type pt R) (hC.getStates ⟨S1ᵢ, hS1ᵢ⟩) ∧ Formalism.IsLiteralUnion pt (StateSetFormalism.type pt R) (hC.getStates ⟨S2ᵢ, hS2ᵢ⟩) ∧ hC.getStates ⟨S1ᵢ, hS1ᵢ⟩ ⊆ hC.getStates ⟨S2ᵢ, hS2ᵢ⟩

def Validator.constraintB2 {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (S1ᵢ S2ᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Validator.constraintB2.prop_eq {n : ℕ} {pt : STRIPS n} {C : Certificate pt} {hC : C.validSets} {S1ᵢ S2ᵢ : ℕ} {a : Unit} : (constraintB2 hC S1ᵢ S2ᵢ).prop a ↔ S1ᵢ < C.states.size ∧ S2ᵢ < C.states.size ∧ ∃ (hS1ᵢ : S1ᵢ < C.states.size) (hS2ᵢ : S2ᵢ < C.states.size), have R := hC.get_formalism [⟨S1ᵢ, hS1ᵢ⟩, ⟨S2ᵢ, hS2ᵢ⟩]; Formalism.IsProgrInter pt (StateSetFormalism.type pt R) (hC.getStates ⟨S1ᵢ, hS1ᵢ⟩) ∧ Formalism.IsLiteralUnion pt (StateSetFormalism.type pt R) (hC.getStates ⟨S2ᵢ, hS2ᵢ⟩) ∧ hC.getStates ⟨S1ᵢ, hS1ᵢ⟩ ⊆ hC.getStates ⟨S2ᵢ, hS2ᵢ⟩

def Validator.constraintB3 {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (S1ᵢ S2ᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Validator.constraintB3.prop_eq {n : ℕ} {pt : STRIPS n} {C : Certificate pt} {hC : C.validSets} {S1ᵢ S2ᵢ : ℕ} {a : Unit} : (constraintB3 hC S1ᵢ S2ᵢ).prop a ↔ S1ᵢ < C.states.size ∧ S2ᵢ < C.states.size ∧ ∃ (hS1ᵢ : S1ᵢ < C.states.size) (hS2ᵢ : S2ᵢ < C.states.size), have R := hC.get_formalism [⟨S1ᵢ, hS1ᵢ⟩, ⟨S2ᵢ, hS2ᵢ⟩]; Formalism.IsRegrInter pt (StateSetFormalism.type pt R) (hC.getStates ⟨S1ᵢ, hS1ᵢ⟩) ∧ Formalism.IsLiteralUnion pt (StateSetFormalism.type pt R) (hC.getStates ⟨S2ᵢ, hS2ᵢ⟩) ∧ hC.getStates ⟨S1ᵢ, hS1ᵢ⟩ ⊆ hC.getStates ⟨S2ᵢ, hS2ᵢ⟩

def Validator.constraintB4 {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (S1ᵢ S2ᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Validator.constraintB4.prop_eq {n : ℕ} {pt : STRIPS n} {C : Certificate pt} {hC : C.validSets} {S1ᵢ S2ᵢ : ℕ} {a : Unit} : (constraintB4 hC S1ᵢ S2ᵢ).prop a ↔ S1ᵢ < C.states.size ∧ S2ᵢ < C.states.size ∧ ∃ (hS1ᵢ : S1ᵢ < C.states.size) (hS2ᵢ : S2ᵢ < C.states.size), have R1 := hC.get_formalism [⟨S1ᵢ, hS1ᵢ⟩]; have R2 := hC.get_formalism [⟨S2ᵢ, hS2ᵢ⟩]; Formalism.IsLiteral pt (StateSetFormalism.type pt R1) (hC.getStates ⟨S1ᵢ, hS1ᵢ⟩) ∧ Formalism.IsLiteral pt (StateSetFormalism.type pt R2) (hC.getStates ⟨S2ᵢ, hS2ᵢ⟩) ∧ hC.getStates ⟨S1ᵢ, hS1ᵢ⟩ ⊆ hC.getStates ⟨S2ᵢ, hS2ᵢ⟩

def Validator.constraintB5 {n : ℕ} {pt : STRIPS n} {C : Certificate pt} (hC : C.validSets) (A1ᵢ A2ᵢ : ℕ) : Constraint Unit

Equations

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

@[simp]

theorem Validator.constraintB5.prop_eq {n : ℕ} {pt : STRIPS n} {C : Certificate pt} {hC : C.validSets} {A1ᵢ A2ᵢ : ℕ} {u : Unit} : (constraintB5 hC A1ᵢ A2ᵢ).prop u ↔ A1ᵢ < C.actions.size ∧ A2ᵢ < C.actions.size ∧ ∃ (hA1ᵢ : A1ᵢ < C.actions.size) (hA2ᵢ : A2ᵢ < C.actions.size), hC.getActions ⟨A1ᵢ, hA1ᵢ⟩ ⊆ hC.getActions ⟨A2ᵢ, hA2ᵢ⟩