Theorem: loadedDiamondPaths
Proof state before:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔNode : TNode
ΔHist : LoadHistory
ΔTab : ClosedTableau ΔHist ΔNode
h : some ⟨ΔNode, ⟨ΔHist, ΔTab⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
cases ΔTab
Proof state after:
case loc
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔNode : TNode
ΔHist : LoadHistory
lt✝ : LocalTableau ΔNode
a✝ : (Y : TNode) → Y ∈ endNodesOf lt✝ → ClosedTableau ΔHist Y
h : some ⟨ΔNode, ⟨ΔHist, ClosedTableau.loc lt✝ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

case mrkL
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

case mrkR
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
R✝ L✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ R✝
a✝ : ClosedTableau ([], []) (L✝, R✝.erase (~⌈α✝⌉φ✝), some (Sum.inr (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkR a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

case atmL
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
L✝ R✝ : List Formula
A✝ : ℕ
X✝ : TNode
χ✝ : LoadFormula
a✝¹ : isBasic X✝ = true
a✝ : ClosedTableau ([], []) (projection A✝ L✝, projection A✝ R✝, some (Sum.inl (~'χ✝)))
h :
  some ⟨(L✝, R✝, some (Sum.inl (~'⌊·A✝⌋χ✝))), ⟨ΔHist, ClosedTableau.atmL a✝¹ a✝⟩⟩ =
    tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

case atmL'
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
L✝ R✝ : List Formula
A✝ : ℕ
X✝ : TNode
φ✝ : Formula
a✝¹ : isBasic X✝ = true
a✝ :
  ClosedTableau (record ΔHist (L✝, R✝, some (Sum.inl (~'⌊·A✝⌋φ✝)))) (projection A✝ L✝ ++ [~φ✝], projection A✝ R✝, none)
h :
  some ⟨(L✝, R✝, some (Sum.inl (~'⌊·A✝⌋φ✝))), ⟨ΔHist, ClosedTableau.atmL' a✝¹ a✝⟩⟩ =
    tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

case atmR
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
L✝ R✝ : List Formula
A✝ : ℕ
X✝ : TNode
χ✝ : LoadFormula
a✝¹ : isBasic X✝ = true
a✝ : ClosedTableau ([], []) (projection A✝ L✝, projection A✝ R✝, some (Sum.inr (~'χ✝)))
h :
  some ⟨(L✝, R✝, some (Sum.inr (~'⌊·A✝⌋χ✝))), ⟨ΔHist, ClosedTableau.atmR a✝¹ a✝⟩⟩ =
    tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

case atmR'
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
L✝ R✝ : List Formula
A✝ : ℕ
X✝ : TNode
φ✝ : Formula
a✝¹ : isBasic X✝ = true
a✝ :
  ClosedTableau (record ΔHist (L✝, R✝, some (Sum.inl (~'⌊·A✝⌋φ✝)))) (projection A✝ L✝, projection A✝ R✝ ++ [~φ✝], none)
h :
  some ⟨(L✝, R✝, some (Sum.inl (~'⌊·A✝⌋φ✝))), ⟨ΔHist, ClosedTableau.atmR' a✝¹ a✝⟩⟩ =
    tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

case rep
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔNode : TNode
ΔHist : LoadHistory
rep✝ : condSixRepeat ΔNode ΔHist
h : some ⟨ΔNode, ⟨ΔHist, ClosedTableau.rep rep✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst