Theorem: loadedDiamondPaths (Pdl/Soundness.lean)

State before:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
h : some tabΔ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
M : KripkeModel W
v : W
φ : AnyFormula
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) Δ
v_X : (M, v)⊨Δ
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
let ⟨L,R,O⟩ := Δ
State after:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
h : some tabΔ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
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)
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

State before:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
h : some tabΔ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
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)
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
let ⟨ΔNode, ΔHist, ΔTab⟩ := tabΔ
State after:
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

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

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)
Δ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
Tactic:
case mrkL =>
  simp at negLoad_in
  cases negLoad_in
  case inl hyp => subst hyp; sorry
  all_goals sorry
State after:
no goals

State before:
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 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
Tactic:
all_goals sorry
State after:
no goals

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)
Δ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
Tactic:
simp at negLoad_in
State after:
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 :
  O =
      some
        (Sum.inl
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ)) ∨
    O =
      some
        (Sum.inr
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ))
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

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 :
  O =
      some
        (Sum.inl
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ)) ∨
    O =
      some
        (Sum.inr
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ))
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
Tactic:
cases negLoad_in
State after:
case inl
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)
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_Δ
h✝ :
  O =
    some
      (Sum.inl
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

case inr
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)
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_Δ
h✝ :
  O =
    some
      (Sum.inr
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

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)
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_Δ
hyp :
  O =
    some
      (Sum.inl
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
case inl hyp => subst hyp; sorry
State after:
no goals

State before:
case inr
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)
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_Δ
h✝ :
  O =
    some
      (Sum.inr
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
all_goals sorry
State after:
no goals

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)
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_Δ
hyp :
  O =
    some
      (Sum.inl
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
subst hyp
State after:
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
Δ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_Δ
v_X :
  (M, v)⊨(L, R,
      some
        (Sum.inl
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ)))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst

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
Δ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_Δ
v_X :
  (M, v)⊨(L, R,
      some
        (Sum.inl
          (match α, φ with
          | α, Sum.inl φ => ~'⌊α⌋φ
          | α, Sum.inr χ => ~'⌊α⌋χ)))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
sorry
State after:
no goals

State before:
case inr
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)
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_Δ
h✝ :
  O =
    some
      (Sum.inr
        (match α, φ with
        | α, Sum.inl φ => ~'⌊α⌋φ
        | α, Sum.inr χ => ~'⌊α⌋χ))
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
sorry
State after:
no goals

State before:
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
Tactic:
sorry
State after:
no goals