Local Tableaux (Section 3)

One-sided local rules

inductive OneSidedLocalRule : List Formula → List (List Formula) → Type

Local rules replace a given set of formulas by other sets, one for each branch. The list of resulting branches can be empty, representing that the given set is closed. In the Haskell prover this is done in "ruleFor" in the Logic.PDL.Prove.Tree module.

• bot : OneSidedLocalRule [⊥] ∅
• not (φ : Formula) : OneSidedLocalRule [φ, ~φ] ∅
• neg (φ : Formula) : OneSidedLocalRule [~~φ] [[φ]]
• con (φ ψ : Formula) : OneSidedLocalRule [φ⋀ψ] [[φ, ψ]]
• nCo (φ ψ : Formula) : OneSidedLocalRule [~(φ⋀ψ)] [[~φ], [~ψ]]
• box (α : Program) (φ : Formula) (notAtom : ¬α.isAtomic) : OneSidedLocalRule [⌈α⌉φ] (unfoldBox α φ)
• dia (α : Program) (φ : Formula) (notAtom : ¬α.isAtomic) : OneSidedLocalRule [~⌈α⌉φ] (unfoldDiamond α φ)

def instDecidableEqOneSidedLocalRule.decEq {a✝ : List Formula} {a✝¹ : List (List Formula)} (x✝ x✝¹ : OneSidedLocalRule a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqOneSidedLocalRule.decEq OneSidedLocalRule.bot OneSidedLocalRule.bot = isTrue instDecidableEqOneSidedLocalRule.decEq._proof_1
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.not a_2) (OneSidedLocalRule.not a_2) = isTrue ⋯
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.neg a_2) (OneSidedLocalRule.neg a_2) = isTrue ⋯
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.con a_2 a_3) (OneSidedLocalRule.con a_2 a_3) = isTrue ⋯
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.nCo a_2 a_3) (OneSidedLocalRule.nCo a_2 a_3) = isTrue ⋯
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.box a_2 a_3 a_4) (OneSidedLocalRule.box a_2 a_3 b) = ⋯ ▸ isTrue ⋯
• instDecidableEqOneSidedLocalRule.decEq (OneSidedLocalRule.dia a_2 a_3 a_4) (OneSidedLocalRule.dia a_2 a_3 b) = ⋯ ▸ isTrue ⋯

instance instDecidableEqOneSidedLocalRule {a✝ : List Formula} {a✝¹ : List (List Formula)} : DecidableEq (OneSidedLocalRule a✝ a✝¹)

Equations

• instDecidableEqOneSidedLocalRule = instDecidableEqOneSidedLocalRule.decEq

instance instReprOneSidedLocalRule {a✝ : List Formula} {a✝¹ : List (List Formula)} : Repr (OneSidedLocalRule a✝ a✝¹)

Equations

• instReprOneSidedLocalRule = { reprPrec := instReprOneSidedLocalRule.repr }

def instReprOneSidedLocalRule.repr {a✝ : List Formula} {a✝¹ : List (List Formula)} : OneSidedLocalRule a✝ a✝¹ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprOneSidedLocalRule.repr OneSidedLocalRule.bot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "OneSidedLocalRule.bot")).group prec✝

theorem oneSidedLocalRuleTruth {X : List Formula} {B : List (List Formula)} (lr : OneSidedLocalRule X B) : Con X≡discon B

Loaded Rules

inductive LoadRule : NegLoadFormula → List (List Formula × Option NegLoadFormula) → Type

The loaded diamond rule, given by unfoldDiamondLoaded. In MB page 19 these were multiple rules ¬u, ¬; ¬* and ¬?. It replaces the loaded formula by up to one loaded formula and a list of normal formulas. It's a bit annoying to need the rule twice here due to the definition of LoadFormula and the extra definition of unfoldDiamondLoaded'.

• dia {α : Program} {χ : LoadFormula} (notAtom : ¬α.isAtomic) : LoadRule (~'⌊α⌋AnyFormula.loaded χ) (unfoldDiamondLoaded α χ)
• dia' {α : Program} {φ : Formula} (notAtom : ¬α.isAtomic) : LoadRule (~'⌊α⌋AnyFormula.normal φ) (unfoldDiamondLoaded' α φ)

def instDecidableEqLoadRule.decEq {a✝ : NegLoadFormula} {a✝¹ : List (List Formula × Option NegLoadFormula)} (x✝ x✝¹ : LoadRule a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqLoadRule.decEq (LoadRule.dia a_4) (LoadRule.dia b) = ⋯ ▸ isTrue ⋯
• instDecidableEqLoadRule.decEq (LoadRule.dia' a_4) (LoadRule.dia' b) = ⋯ ▸ isTrue ⋯

instance instDecidableEqLoadRule {a✝ : NegLoadFormula} {a✝¹ : List (List Formula × Option NegLoadFormula)} : DecidableEq (LoadRule a✝ a✝¹)

Equations

• instDecidableEqLoadRule = instDecidableEqLoadRule.decEq

instance instReprLoadRule {a✝ : NegLoadFormula} {a✝¹ : List (List Formula × Option NegLoadFormula)} : Repr (LoadRule a✝ a✝¹)

Equations

• instReprLoadRule = { reprPrec := instReprLoadRule.repr }

def instReprLoadRule.repr {a✝ : NegLoadFormula} {a✝¹ : List (List Formula × Option NegLoadFormula)} : LoadRule a✝ a✝¹ → ℕ → Std.Format

Equations

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

def LoadRule.unload {χ : LoadFormula} {B : List (List Formula × Option NegLoadFormula)} : LoadRule (~'χ) B → OneSidedLocalRule [~χ.unload] (List.map pairUnload B)

Given a LoadRule application, define the equivalent unloaded rule application. This allows re-using oneSidedLocalRuleTruth to prove loadRuleTruth.

Equations

• (LoadRule.dia notAtom).unload = ⋯ ▸ OneSidedLocalRule.dia α χ_2.unload notAtom
• (LoadRule.dia' notAtom).unload = ⋯ ▸ OneSidedLocalRule.dia α φ notAtom

theorem loadRuleTruth {χ : LoadFormula} {B : List (List Formula × Option NegLoadFormula)} (lr : LoadRule (~'χ) B) : ~χ.unload≡dis (List.map (Con ∘ pairUnload) B)

The loaded unfold rule is sound and invertible. In the notes this is part of localRuleTruth.

Local Rules

inductive LocalRule : Sequent → List Sequent → Type

A local rule is a OneSidedLocalRule, a left-right contradiction, or a LoadRule. Note that formulas can be in four places: left, right, loaded left, loaded right.

We do not have neg/contradiction rules between loaded and unloaded formulas (i.e. between ({unload χ}, ∅, some (Sum.inl ~χ)) and (∅, {unload χ}, some (Sum.inr ~χ))) because in any such case we could also close the tableau before or without loading.

The YS_def arguments in non-terminal rules enables deriving DecidableEq for LocalRule.

• oneSidedL {precond : List Formula} {ress : List (List Formula)} {YS : List (List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula))} (orule : OneSidedLocalRule precond ress) (YS_def : YS = List.map (fun (res : List Formula) => (res, ∅, none)) ress) : LocalRule (precond, ∅, none) YS
• oneSidedR {precond : List Formula} {ress : List (List Formula)} {YS : List (List Formula × List Formula × Option (NegLoadFormula ⊕ NegLoadFormula))} (orule : OneSidedLocalRule precond ress) (YS_def : YS = List.map (fun (res : List Formula) => (∅, res, none)) ress) : LocalRule (∅, precond, none) YS
• LRnegL (ϕ : Formula) : LocalRule ([ϕ], [~ϕ], none) ∅
• LRnegR (ϕ : Formula) : LocalRule ([~ϕ], [ϕ], none) ∅
• loadedL {ress : List (List Formula × Option NegLoadFormula)} {YS : List Sequent} (χ : LoadFormula) (lrule : LoadRule (~'χ) ress) (YS_def : YS = List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (X, ∅, Option.map Sum.inl o)) ress) : LocalRule (∅, ∅, some (Sum.inl (~'χ))) YS
• loadedR {ress : List (List Formula × Option NegLoadFormula)} {YS : List Sequent} (χ : LoadFormula) (lrule : LoadRule (~'χ) ress) (YS_def : YS = List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (∅, X, Option.map Sum.inr o)) ress) : LocalRule (∅, ∅, some (Sum.inr (~'χ))) YS

instance instReprLocalRule {a✝ : Sequent} {a✝¹ : List Sequent} : Repr (LocalRule a✝ a✝¹)

Equations

• instReprLocalRule = { reprPrec := instReprLocalRule.repr }

def instReprLocalRule.repr {a✝ : Sequent} {a✝¹ : List Sequent} : LocalRule a✝ a✝¹ → ℕ → Std.Format

Equations

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

instance instDecidableEqLocalRule {a✝ : Sequent} {a✝¹ : List Sequent} : DecidableEq (LocalRule a✝ a✝¹)

Equations

• instDecidableEqLocalRule = instDecidableEqLocalRule.decEq

def instDecidableEqLocalRule.decEq {a✝ : Sequent} {a✝¹ : List Sequent} (x✝ x✝¹ : LocalRule a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqLocalRule.decEq (LocalRule.oneSidedL orule YS_def) (LocalRule.oneSidedR orule_1 YS_def_1) = isFalse ⋯
• instDecidableEqLocalRule.decEq (LocalRule.oneSidedR orule YS_def) (LocalRule.oneSidedL orule_1 YS_def_1) = isFalse ⋯
• instDecidableEqLocalRule.decEq (LocalRule.LRnegL a_2) (LocalRule.LRnegL a_2) = isTrue ⋯
• instDecidableEqLocalRule.decEq (LocalRule.LRnegR a_2) (LocalRule.LRnegR a_2) = isTrue ⋯

def applyLocalRule {Lcond Rcond : List Formula} {Ocond : Olf} {ress : List Sequent} : LocalRule (Lcond, Rcond, Ocond) ress → Sequent → List Sequent

Equations

• applyLocalRule x✝ (L, R, O) = List.map (fun (x : Sequent) => match x with | (Lnew, Rnew, Onew) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O.change Ocond Onew)) ress

theorem oneSidedL_preserves_right {LRO : Sequent} {Lcond : List Formula} (Lpreproof : Lcond ⊆ LRO.L) {Lres : List (List Formula)} (orule : OneSidedLocalRule Lcond Lres) {YS : List Sequent} (YS_def : YS = List.map (fun (res : List Formula) => (res, ∅, none)) Lres) (c : Sequent) : c ∈ applyLocalRule (LocalRule.oneSidedL orule YS_def) LRO → c.right = LRO.right

theorem oneSidedR_preserves_left {LRO : Sequent} {Rcond : List Formula} (Rpreproof : Rcond ⊆ LRO.R) {Rres : List (List Formula)} (orule : OneSidedLocalRule Rcond Rres) {YS : List Sequent} (YS_def : YS = List.map (fun (res : List Formula) => (∅, res, none)) Rres) (c : Sequent) : c ∈ applyLocalRule (LocalRule.oneSidedR orule YS_def) LRO → c.left = LRO.left

theorem oneSidedL_sat_down (LRO : Sequent) {Lcond : List Formula} (Lpreproof : Lcond ⊆ LRO.L) {Lres : List (List Formula)} (orule : OneSidedLocalRule Lcond Lres) {YS : List Sequent} (YS_def : YS = List.map (fun (res : List Formula) => (res, ∅, none)) Lres) {X : List Formula} (LX_sat : HasSat.satisfiable (LRO.left ∪ X)) : ∃ c ∈ applyLocalRule (LocalRule.oneSidedL orule YS_def) LRO, HasSat.satisfiable (c.left ∪ X)

theorem oneSidedR_sat_down (LRO : Sequent) {Rcond : List Formula} (Rpreproof : Rcond ⊆ LRO.R) {Rres : List (List Formula)} (orule : OneSidedLocalRule Rcond Rres) {YS : List Sequent} (YS_def : YS = List.map (fun (res : List Formula) => (∅, res, none)) Rres) {X : List Formula} (RX_sat : HasSat.satisfiable (LRO.right ∪ X)) : ∃ c ∈ applyLocalRule (LocalRule.oneSidedR orule YS_def) LRO, HasSat.satisfiable (c.right ∪ X)

theorem loadedL_preserves_right {LRO : Sequent} (χ : LoadFormula) (Opreproof : LRO.O = some (Sum.inl (~'χ))) {ress : List (List Formula × Option NegLoadFormula)} (lrule : LoadRule (~'χ) ress) {YS : List Sequent} (YS_def : YS = List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (X, ∅, Option.map Sum.inl o)) ress) (c : Sequent) : c ∈ applyLocalRule (LocalRule.loadedL χ lrule YS_def) LRO → c.right = LRO.right

Applying a LoadRule on the left will leave the right unchanged.

theorem loadedR_preserves_left {LRO : Sequent} (χ : LoadFormula) (Opreproof : LRO.O = some (Sum.inr (~'χ))) {ress : List (List Formula × Option NegLoadFormula)} (lrule : LoadRule (~'χ) ress) {YS : List Sequent} (YS_def : YS = List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (∅, X, Option.map Sum.inr o)) ress) (c : Sequent) : c ∈ applyLocalRule (LocalRule.loadedR χ lrule YS_def) LRO → c.left = LRO.left

Applying a LoadRule on the right will leave the left unchanged.

theorem loadedL_sat_down (LRO : Sequent) (χ : LoadFormula) (Opreproof : LRO.O = some (Sum.inl (~'χ))) {ress : List (List Formula × Option NegLoadFormula)} (lrule : LoadRule (~'χ) ress) {YS : List Sequent} (YS_def : YS = List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (X, ∅, Option.map Sum.inl o)) ress) {X : List Formula} (LX_sat : HasSat.satisfiable (LRO.left ∪ X)) : ∃ c ∈ applyLocalRule (LocalRule.loadedL χ lrule YS_def) LRO, HasSat.satisfiable (c.left ∪ X)

Applying a LoadRule on the left preserves satisfiability of the left, even together with any other list of formulas as context.

theorem loadedR_sat_down (LRO : Sequent) (χ : LoadFormula) (Opreproof : LRO.O = some (Sum.inr (~'χ))) {ress : List (List Formula × Option NegLoadFormula)} (lrule : LoadRule (~'χ) ress) {YS : List Sequent} (YS_def : YS = List.map (fun (x : List Formula × Option NegLoadFormula) => match x with | (X, o) => (∅, X, Option.map Sum.inr o)) ress) {X : List Formula} (RX_sat : HasSat.satisfiable (LRO.right ∪ X)) : ∃ c ∈ applyLocalRule (LocalRule.loadedR χ lrule YS_def) LRO, HasSat.satisfiable (c.right ∪ X)

Applying a LoadRule on the right preserves satisfiability of the right, even together with any other list of formulas as context.

inductive LocalRuleApp : Sequent → List Sequent → Type

A local rule application going from ⟨L,R,O⟩ to C consists of a local rule lr replacing ⟨Lcond, Rcond, Ocond⟩ by ress and proofs that ⟨Lcond, Rcond, Ocond⟩ is a subsequent of ⟨L,R,O⟩ and that C are the results of applying lr to ⟨L,R,O⟩.

• mk {L R : List Formula} {C ress : List Sequent} {O : Olf} (Lcond Rcond : List Formula) (Ocond : Olf) (lr : LocalRule (Lcond, Rcond, Ocond) ress) {hC : C = applyLocalRule lr (L, R, O)} (preconditionProof : Lcond.Subperm L ∧ Rcond.Subperm R ∧ Ocond ⊆ O) : LocalRuleApp (L, R, O) C

def instDecidableEqLocalRuleApp.decEq {a✝ : Sequent} {a✝¹ : List Sequent} (x✝ x✝¹ : LocalRuleApp a✝ a✝¹) : Decidable (x✝ = x✝¹)

Equations

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

instance instDecidableEqLocalRuleApp {a✝ : Sequent} {a✝¹ : List Sequent} : DecidableEq (LocalRuleApp a✝ a✝¹)

Equations

• instDecidableEqLocalRuleApp = instDecidableEqLocalRuleApp.decEq

theorem localRuleTruth {X : Sequent} {C : List Sequent} (lrA : LocalRuleApp X C) {W : Type} (M : KripkeModel W) (w : W) : (M, w)⊨X ↔ ∃ Ci ∈ C, (M, w)⊨Ci

instance instDecidableBasic {X : Sequent} : Decidable X.basic

Equations

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

inductive LocalTableau (X : Sequent) : Type

Local tableau for X, maximal by definition.

• byLocalRule {X : Sequent} {B : List Sequent} : LocalRuleApp X B → (next : (Y : Sequent) → Y ∈ B → LocalTableau Y) → LocalTableau X
• sim {X : Sequent} : X.basic → LocalTableau X

instance LocalTableau.instDecidableEq {X : Sequent} {lt1 lt2 : LocalTableau X} : Decidable (lt1 = lt2)

Equations

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

theorem nonbasic_of_localRuleApp {X : Sequent} {B : List Sequent} (lrA : LocalRuleApp X B) : ¬X.basic

If we can apply a local rule to a sequent then it cannot be basic.

Termination of LocalTableau

theorem testsOfProgram_sizeOf_lt (α : Program) (τ : Formula) : τ ∈ testsOfProgram α → sizeOf τ < sizeOf α

@[irreducible]

def lmOfFormula (f : Formula) : ℕ

The local measure we use together with D-M to show that LocalTableau are finite.

Equations

• lmOfFormula Formula.bottom = 0
• lmOfFormula (·a) = 0
• lmOfFormula (φ⋀ψ) = 1 + lmOfFormula φ + lmOfFormula ψ
• lmOfFormula (⌈·a⌉a_1) = 0
• lmOfFormula (⌈α⌉φ) = 1 + lmOfFormula φ + (List.map (fun (τ : { x : Formula // x ∈ testsOfProgram α }) => lmOfFormula (~↑τ)) (testsOfProgram α).attach).sum
• lmOfFormula (~Formula.bottom) = 0
• lmOfFormula (~·a) = 0
• lmOfFormula (~~φ) = 1 + lmOfFormula φ
• lmOfFormula (~(φ⋀ψ)) = 1 + lmOfFormula (~φ) + lmOfFormula (~ψ)
• lmOfFormula (~⌈·a⌉a_1) = 0
• lmOfFormula (~⌈α⌉φ) = 1 + lmOfFormula (~φ) + (List.map (fun (τ : { x : Formula // x ∈ testsOfProgram α }) => lmOfFormula ↑τ) (testsOfProgram α).attach).sum

theorem lmOfFormula_lt_box_of_nonAtom {φ : Formula} {α : Program} (h : ¬α.isAtomic) : lmOfFormula (~φ) < lmOfFormula (~⌈α⌉φ)

instance Formula.WellFoundedLT : _root_.WellFoundedLT Formula

instance Formula.instPreorderFormula : Preorder Formula

Equations

• Formula.instPreorderFormula = Preorder.lift lmOfFormula

def node_to_multiset : Sequent → Multiset Formula

Equations

• node_to_multiset (L, R, none) = ↑L + ↑R
• node_to_multiset (L, R, some (Sum.inl (~'χ))) = ↑L + ↑R + ↑[~χ.unload]
• node_to_multiset (L, R, some (Sum.inr (~'χ))) = ↑L + ↑R + ↑[~χ.unload]

def Olf.toForm : Olf → Multiset Formula

Equations

• Olf.toForm none = ∅
• Olf.toForm (some (Sum.inl (~'χ))) = {~χ.unload}
• Olf.toForm (some (Sum.inr (~'χ))) = {~χ.unload}

theorem node_to_multiset_eq {L R : List Formula} {O : Olf} : node_to_multiset (L, R, O) = ↑L + ↑R + O.toForm

theorem node_to_multiset_eq_of_three_eq {L L' R R' : List Formula} {O O' : Olf} (hL : L = L') (hR : R = R') (hO : O = O') : node_to_multiset (L, R, O) = node_to_multiset (L', R', O')

If each three parts are the same then node_to_multiset is the same.

theorem List.Subperm.append {α : Type u_1} {l₁ l₂ r₁ r₂ : List α} : l₁.Subperm l₂ → r₁.Subperm r₂ → (l₁ ++ r₁).Subperm (l₂ ++ r₂)

theorem preconP_to_submultiset {Lcond L Rcond R : List Formula} {Ocond O : Olf} (preconditionProof : Lcond.Subperm L ∧ Rcond.Subperm R ∧ Ocond ⊆ O) : node_to_multiset (Lcond, Rcond, Ocond) ≤ node_to_multiset (L, R, O)

theorem Multiset.sub_of_le {α : Type u_1} [DecidableEq α] {M N X Y : Multiset α} (h : N ≤ M) : M - N + Y = X ↔ M + Y = X + N

theorem Multiset_diff_append_of_le {α : Type u_1} [DecidableEq α] {R Rcond Rnew : List α} : ↑(R.diff Rcond ++ Rnew) = ↑R - ↑Rcond + ↑Rnew

theorem List.Perm_diff_append_of_Subperm {α : Type u_1} [DecidableEq α] {L M : List α} (h : M.Subperm L) : L.Perm (L.diff M ++ M)

theorem List.count_eq_diff_of_subperm {α : Type u_1} [DecidableEq α] {L M : List α} (h : M.Subperm L) (φ : α) : count φ L = count φ (L.diff M) + count φ M

theorem node_to_multiset_of_precon {L R Lcond Rcond Lnew Rnew : List Formula} {O Ocond Onew : Olf} (precon : Lcond.Subperm L ∧ Rcond.Subperm R ∧ Ocond ⊆ O) (O_extracon : O ≠ none → Ocond = none → Onew = none) : node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond) + node_to_multiset (Lnew, Rnew, Onew) = node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O.change Ocond Onew)

Applying node_to_multiset before or after applyLocalRule gives the same.

def lt_Sequent (X Y : Sequent) : Prop

Equations

• lt_Sequent X Y = (node_to_multiset X).IsDershowitzMannaLT (node_to_multiset Y)

instance instWellFoundedRelationSequent : WellFoundedRelation Sequent

Equations

• instWellFoundedRelationSequent = { rel := lt_Sequent, wf := instWellFoundedRelationSequent._proof_1 }

theorem LocalRule.cond_non_empty {Lcond Rcond : List Formula} {Ocond : Olf} {X : List Sequent} (rule : LocalRule (Lcond, Rcond, Ocond) X) : node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅

theorem Multiset.sub_add_of_subset_eq {α : Type u_1} {X : Multiset α} [DecidableEq α] {M : Multiset α} (h : X ≤ M) : M = M - X + X

theorem unfoldBox.decreases_lmOf_nonAtomic {ψ : Formula} {α : Program} {φ : Formula} {X : List Formula} (α_non_atomic : ¬α.isAtomic) (X_in : X ∈ unfoldBox α φ) (ψ_in_X : ψ ∈ X) : lmOfFormula ψ < lmOfFormula (⌈α⌉φ)

theorem lmOfFormula.le_union_left (α β : Program) (φ : Formula) : lmOfFormula (~⌈α⌉φ) ≤ lmOfFormula (~⌈α⋓β⌉φ)

theorem lmOfFormula.le_union_right (α β : Program) (φ : Formula) : lmOfFormula (~⌈β⌉φ) ≤ lmOfFormula (~⌈α⋓β⌉φ)

theorem H_goes_down (α : Program) (φ : Formula) {Fs : List Formula} {δ : List Program} (in_H : (Fs, δ) ∈ H α) {ψ : Formula} (in_Fs : ψ ∈ Fs) : lmOfFormula ψ < lmOfFormula (~⌈α⌉φ)

theorem unfoldDiamond.decreases_lmOf_nonAtomic {ψ : Formula} {α : Program} {φ : Formula} {X : List Formula} (α_non_atomic : ¬α.isAtomic) (X_in : X ∈ unfoldDiamond α φ) (ψ_in_X : ψ ∈ X) : lmOfFormula ψ < lmOfFormula (~⌈α⌉φ)

theorem LocalRuleDecreases {X : Sequent} {ress : List Sequent} (rule : LocalRule X ress) (Y : Sequent) : Y ∈ ress → ∀ y ∈ node_to_multiset Y, ∃ x ∈ node_to_multiset X, y < x

def MultisetLT' {α : Type u_1} [Preorder α] (M N : Multiset α) : Prop

Equations

• MultisetLT' M N = ∃ (X : Multiset α) (Y : Multiset α) (Z : Multiset α), Y ≠ ∅ ∧ M = Z + X ∧ N = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y

theorem MultisetDMLT.iff_MultisetLT' {α : Type u_1} [Preorder α] {M N : Multiset α} : M.IsDershowitzMannaLT N ↔ MultisetLT' M N

theorem localRuleApp.decreases_DM {X : Sequent} {B : List Sequent} (lrA : LocalRuleApp X B) (Y : Sequent) : Y ∈ B → lt_Sequent Y X

@[irreducible]

def endNodesOf {X : Sequent} : LocalTableau X → List Sequent

Equations

• endNodesOf (LocalTableau.byLocalRule _lr next) = (List.map (fun (x : { x : Sequent // x ∈ B }) => match x with | ⟨Y, h⟩ => endNodesOf (next Y h)) B.attach).flatten
• endNodesOf (LocalTableau.sim a) = [x✝]

Helper functions, relating end nodes and children

noncomputable def endNode_to_endNodeOfChildNonComp {X : Sequent} {a✝ : List Sequent} {subTabs : (Y : Sequent) → Y ∈ a✝ → LocalTableau Y} {E : Sequent} (lrA : LocalRuleApp X a✝) (E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)) : { x : Sequent // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }

Equations

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

theorem endNodeIsEndNodeOfChild {X : Sequent} {a✝ : List Sequent} {subTabs : (Y : Sequent) → Y ∈ a✝ → LocalTableau Y} {E : Sequent} (lrA : LocalRuleApp X a✝) (E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)) : ∃ (Y : Sequent) (h : Y ∈ a✝), E ∈ endNodesOf (subTabs Y h)

theorem endNodeOfChild_to_endNode {X Y : Sequent} {ltX : LocalTableau X} {C : List Sequent} (lrA : LocalRuleApp X C) (subTabs : (Y : Sequent) → Y ∈ C → LocalTableau Y) (h : ltX = LocalTableau.byLocalRule lrA subTabs) (Y_in : Y ∈ C) {Z : Sequent} (Z_in : Z ∈ endNodesOf (subTabs Y Y_in)) : Z ∈ endNodesOf ltX

Overall Soundness and Invertibility of LocalTableau

theorem localTableauTruth {X : Sequent} (lt : LocalTableau X) {W : Type} (M : KripkeModel W) (w : W) : (M, w)⊨X ↔ ∃ Y ∈ endNodesOf lt, (M, w)⊨Y

theorem localTableauSat {X : Sequent} (lt : LocalTableau X) : HasSat.satisfiable X ↔ ∃ Y ∈ endNodesOf lt, HasSat.satisfiable Y

Local Tableaux make progress

These lemmas are used to show soundness, in particular loadedDiamondPaths.

theorem endNodesOf_basic {X Z : Sequent} {ltZ : LocalTableau Z} : X ∈ endNodesOf ltZ → X.basic

End nodes of any local tableau are basic.

theorem endNodesOf_nonbasic_lt_Sequent {X Y : Sequent} (lt : LocalTableau X) (X_nonbas : ¬X.basic) : Y ∈ endNodesOf lt → lt_Sequent Y X

If X is not basic, then all end nodes Y of a local tableau lt for X are strictly lower than X according to the DM-ordering of their multisets.

theorem non_eq_of_ltSequent {X Y : Sequent} : lt_Sequent X Y → X ≠ Y

If a sequent is lower according the DM-ordering, then it is different.

theorem endNodesOf_nonbasic_non_eq {X Y : Sequent} (lt : LocalTableau X) (X_nonbas : ¬X.basic) : Y ∈ endNodesOf lt → Y ≠ X

If X is not basic, then for all end nodes Y of a local tableau lt for X we have that Y ≠ X.

theorem IsDershowitzMannaLT.irrefl {α : Type u_1} [Preorder α] [WellFoundedLT α] (X : Multiset α) : ¬X.IsDershowitzMannaLT X

theorem non_multisetEqTo_of_ltSequent {X Y : Sequent} : lt_Sequent X Y → ¬X.multisetEqTo Y

If a sequent is lower according to the DM-ordering, then they are multiset-different. (The analogue with finset instead of multiset does not hold.)