Local Tableaux (Section 3)

Tableau Nodes

@[reducible, inline]

abbrev Olf : Type

In nodes we optionally have a negated loaded formula on the left or right.

Equations

• Olf = Option (NegLoadFormula ⊕ NegLoadFormula)

def Olf.voc : Olf → Vocab

Equations

• Olf.voc none = ∅
• Olf.voc (some (Sum.inl nlf)) = nlf.voc
• Olf.voc (some (Sum.inr nlf)) = nlf.voc

def Sequent : Type

A tableau node is labelled with two lists of formulas and an Olf.

Equations

• Sequent = (List Formula × List Formula × Olf)

instance instSequentDecidableEq : DecidableEq Sequent

Equations

• instSequentDecidableEq a b = instDecidableEqProd a b

instance instSequentRepr : Repr Sequent

Equations

• instSequentRepr = instReprProdOfReprTuple

def Sequent.setEqTo : Sequent → Sequent → Prop

Two Sequents are set-equal when their components are finset-equal. That is, we do not care about the order of the lists, but we do care about the side of the formula and what formual is loaded. Hint: use List.toFinset.ext_iff with this.

Equations

• Sequent.setEqTo (L, R, O) (L', R', O') = (L.toFinset = L'.toFinset ∧ R.toFinset = R'.toFinset ∧ O = O')

def Sequent.toFinset : Sequent → Finset Formula

Equations

• Sequent.toFinset (L, R, O) = L.toFinset ∪ R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset

def Sequent.L : Sequent → List Formula

Equations

• Sequent.L (L, R, O) = L

def Sequent.R : Sequent → List Formula

Equations

• Sequent.R (L, R, O) = R

def Sequent.O : Sequent → Olf

Equations

• Sequent.O (L, R, O) = O

def Sequent.isLoaded : Sequent → Bool

Equations

• Sequent.isLoaded (fst, fst_1, none) = decide False
• Sequent.isLoaded (fst, fst_1, some val) = decide True

def Sequent.isFree (Γ : Sequent) : Bool

Equations

• Γ.isFree = decide ¬Γ.isLoaded = true

@[simp]

theorem Sequent.none_isFree (L R : List Formula) : Sequent.isFree (L, R, none) = true

@[simp]

theorem Sequent.some_not_isFree (L R : List Formula) (olf : NegLoadFormula ⊕ NegLoadFormula) : ¬Sequent.isFree (L, R, some olf) = true

theorem setEqTo_isLoaded_iff {X Y : Sequent} (h : X.setEqTo Y) : X.isLoaded = Y.isLoaded

Semantics of a Sequent

instance modelCanSemImplySequent {W : Type} : vDash (KripkeModel W × W) Sequent

Equations

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

instance modelCanSemImplyLLO {W : Type} : vDash (KripkeModel W × W) (List Formula × List Formula × Olf)

Equations

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

instance instSequentHasSat : HasSat Sequent

Equations

• instSequentHasSat = { satisfiable := fun (Δ : Sequent) => ∃ (W : Type) (M : KripkeModel W) (w : W), (M, w)⊨Δ }

theorem tautImp_iff_SequentUnsat {φ ψ : Formula} {X : Sequent} : X = ([φ], [~ψ], none) → (φ⊨ψ ↔ ¬HasSat.satisfiable X)

theorem vDash_setEqTo_iff {W : Type} {X Y : Sequent} (h : X.setEqTo Y) (M : KripkeModel W) (w : W) : (M, w)⊨X ↔ (M, w)⊨Y

Different kinds of formulas as elements of Sequent

instance instMembershipFormulaSequent : Membership Formula Sequent

Equations

• instMembershipFormulaSequent = { mem := fun (X : Sequent) (φ : Formula) => φ ∈ X.L ∨ φ ∈ X.R }

def NegLoadFormula.mem_Sequent (X : Sequent) (nlf : NegLoadFormula) : Prop

Equations

• NegLoadFormula.mem_Sequent X nlf = (X.O = some (Sum.inl nlf) ∨ X.O = some (Sum.inr nlf))

instance instDecidableMem_SequentMkListFormulaProdOlf {L R : List Formula} {O : Olf} {nlf : NegLoadFormula} : Decidable (NegLoadFormula.mem_Sequent (L, R, O) nlf)

Equations

• instDecidableMem_SequentMkListFormulaProdOlf = if h : O = some (Sum.inl nlf) then isTrue ⋯ else if h2 : O = some (Sum.inr nlf) then isTrue ⋯ else isFalse ⋯

def Sequent.without (LRO : Sequent) (naf : AnyNegFormula) : Sequent

Equations

• Sequent.without (L, R, O) (~''(AnyFormula.normal f)) = (L \ {~f}, R \ {~f}, O)
• Sequent.without (L, R, O) (~''(AnyFormula.loaded lf)) = if NegLoadFormula.mem_Sequent (L, R, O) (~'lf) then (L, R, none) else (L, R, O)

instance instMembershipNegLoadFormulaSequent : Membership NegLoadFormula Sequent

Equations

• instMembershipNegLoadFormulaSequent = { mem := NegLoadFormula.mem_Sequent }

def AnyNegFormula.mem_Sequent (X : Sequent) (anf : AnyNegFormula) : Prop

Equations

• AnyNegFormula.mem_Sequent x✝ (~''(AnyFormula.normal φ)) = ((~φ) ∈ x✝)
• AnyNegFormula.mem_Sequent x✝ (~''(AnyFormula.loaded χ)) = NegLoadFormula.mem_Sequent x✝ (~'χ)

instance instMembershipAnyNegFormulaSequent : Membership AnyNegFormula Sequent

Equations

• instMembershipAnyNegFormulaSequent = { mem := AnyNegFormula.mem_Sequent }

Local Tableaux

def closed : Finset Formula → Prop

A set is closed iff it contains ⊥ or contains a formula and its negation.

Equations

• closed X = (⊥ ∈ X ∨ ∃ f ∈ X, (~f) ∈ X)

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

• 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 α φ)

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

Equations

• instDecidableEqOneSidedLocalRule = decEqOneSidedLocalRule✝

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

Equations

• instReprOneSidedLocalRule = { reprPrec := reprOneSidedLocalRule✝ }

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

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

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

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

Equations

• instDecidableEqLoadRule = decEqLoadRule✝

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

Equations

• instReprLoadRule = { reprPrec := reprLoadRule✝ }

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.

inductive LocalRule : Sequent → List Sequent → Type

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

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

Equations

• instReprLocalRule = { reprPrec := reprLocalRule✝ }

instance Option.instHasSubsetOption {α : Type u_1} : HasSubset (Option α)

Equations

• Option.instHasSubsetOption = { Subset := fun (o1 o2 : Option α) => match o1, o2 with | none, x => True | some val, none => False | some f, some g => f = g }

@[simp]

theorem Option.some_subseteq {α : Type u_1} {x : α} {O : Option α} : some x ⊆ O ↔ some x = O

instance Option.insHasSdiff {α : Type u_1} [DecidableEq α] : SDiff (Option α)

Instance that is used to say (O : Olf) \ (O' : Olf).

Equations

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

def Option.overwrite {α : Type u_1} : Option α → Option α → Option α

Equations

• x✝.overwrite none = x✝
• x✝.overwrite (some x_3) = some x_3

def Olf.change (oldO Ocond newO : Olf) : Olf

Equations

• oldO.change Ocond newO = Option.overwrite (oldO \ Ocond) newO

@[simp]

theorem Olf.change_none_none {oldO : Olf} : oldO.change none none = oldO

@[simp]

theorem Olf.change_some_some_none {wnlf : NegLoadFormula ⊕ NegLoadFormula} : Olf.change (some wnlf) (some wnlf) none = none

@[simp]

theorem Olf.change_some {oldO whatever : Olf} {wnlf : NegLoadFormula ⊕ NegLoadFormula} : oldO.change whatever (some wnlf) = some wnlf

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

inductive LocalRuleApp : Sequent → List Sequent → Type

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

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

def isBasicForm : Formula → Bool

Equations

• isBasicForm Formula.bottom = decide True
• isBasicForm (~Formula.bottom) = decide True
• isBasicForm (·a) = decide True
• isBasicForm (~·a) = decide True
• isBasicForm (⌈·a⌉a_1) = decide True
• isBasicForm (~⌈·a⌉a_1) = decide True
• isBasicForm x✝ = decide False

def isBasicSet : Finset Formula → Bool

Equations

• isBasicSet x✝ = decide (∀ P ∈ x✝, isBasicForm P = true)

def isBasic : Sequent → Bool

A sequent is basic iff it only contains ⊥, ¬⊥, p, ¬p, [A]_ or ¬[A]_ formulas.

Equations

• isBasic (L, R, O) = decide (∀ f ∈ L ++ R ++ (Option.map (Sum.elim negUnload negUnload) O).toList, isBasicForm f = true)

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} : isBasic X = true → LocalTableau X

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 : 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) (φ : α) : List.count φ L = List.count φ (L.diff M) + List.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 LocalRule.Decreases {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✝]

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) }

Helper functions, relating end nodes and children

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