Local Lemmas for Soundness (part of Section 6)

theorem atomicLocalLoadedDiamond (α : Program) {X : Sequent} (ltab : LocalTableau X) (α_atom : α.isAtomic) (ξ : AnyFormula) {side : Side} (negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side X) (Y : Sequent) : Y ∈ endNodesOf ltab → (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side Y

Helper for loadedDiamondPaths. If α is atomic, and ~''(⌊α⌋ξ) is in X, then for any local tableau ltab for X, the same loaded diamond must still be in all endNodesOf ltab, on the same side.

@[simp]

theorem next_exists_avoid_def_l {Y : Sequent} {B : List Sequent} (next : (Y : Sequent) → Y ∈ B → LocalTableau Y) : (∃ (l : List Sequent), (∃ (a : Sequent) (h : a ∈ B), endNodesOf (next a h) = l) ∧ Y ∈ l) ↔ ∃ (Z : Sequent) (Z_in : Z ∈ B), Y ∈ endNodesOf (next Z Z_in)

theorem lra_preserves_free {X : Sequent} {B : List Sequent} {Z : Sequent} (lra : LocalRuleApp X B) (Z_in : Z ∈ B) (X_free : X.isFree = true) : Z.isFree = true

theorem endNodesOf_free_are_free {X Y : Sequent} (ltX : LocalTableau X) (h : X.isFree = true) (Y_in : Y ∈ endNodesOf ltX) : Y.isFree = true

theorem localLoadedDiamondList (αs : List Program) {X : Sequent} (ltab : LocalTableau X) {W : Type} {M : KripkeModel W} {v w : W} (v_αs_w : relateSeq M αs v w) (v_t : (M, v)⊨X) (φ : Formula) {side : Side} (negLoad_in : (~''(AnyFormula.loadBoxes αs (AnyFormula.normal φ))).in_side side X) (no_other_loading : (X.without (~''(AnyFormula.loadBoxes αs (AnyFormula.normal φ)))).isFree = true) (w_nξ : (M, w)⊨~''(AnyFormula.normal φ)) : ∃ Y ∈ endNodesOf ltab, (M, v)⊨Y ∧ (Y.isFree = true ∨ ∃ (F : List Formula) (γ : List Program), (~''(AnyFormula.loadBoxes γ (AnyFormula.normal φ))).in_side side Y ∧ relateSeq M γ v w ∧ distance_list M v w γ = distance_list M v w αs ∧ (M, v)⊨F ∧ (F, γ) ∈ Hl αs ∧ (Y.without (~''(AnyFormula.loadBoxes γ (AnyFormula.normal φ)))).isFree = true)

Helper to deal with local tableau in loadedDiamondPaths. Takes a list of programs and φ, i.e. we want access to all loaded boxes.