Theorem: existsLocalTableauFor (Bml/Tableau.lean)

State before:
LR : TNode
⊢ Nonempty (LocalTableau LR)
Tactic:
cases em ¬(∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2)
State after:
case inl
LR : TNode
h✝ : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)

case inr
LR : TNode
h✝ : ¬¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)

State before:
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
Tactic:
case inl canApplyRule =>
  constructor
  apply LocalTableau.fromSimple
  by_contra hyp
  have := notSimpleThenLocalRule hyp
  aesop
State after:
no goals

State before:
LR : TNode
canApplyRule : ¬¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
Tactic:
case inr canApplyRule =>
  rw [not_not] at canApplyRule
  rcases canApplyRule with ⟨LCond, RCond, C, lr_exists, preconL, preconR⟩
  cases' lr_exists with lr
  constructor
  apply LocalTableau.fromRule
  apply LocalRuleApp.mk C LCond RCond lr ⟨preconL, preconR⟩
  use applyLocalRule lr (LR.1, LR.2)
  rfl
  intro c c_in
  let ruleA := @LocalRuleApp.mk LR.1 LR.2 (applyLocalRule lr (LR.1, LR.2)) _ LCond RCond lr rfl ⟨preconL, preconR⟩
  have := localRuleAppDecreasesLength ruleA c c_in
  apply Classical.choice (existsLocalTableauFor c)
State after:
no goals

State before:
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
Tactic:
constructor
State after:
case val
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ LocalTableau LR

State before:
case val
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ LocalTableau LR
Tactic:
apply LocalTableau.fromSimple
State after:
case val.isSimple
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Simple LR

State before:
case val.isSimple
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Simple LR
Tactic:
by_contra hyp
State after:
case val.isSimple
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
hyp : ¬Simple LR
⊢ False

State before:
case val.isSimple
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
hyp : ¬Simple LR
⊢ False
Tactic:
have := notSimpleThenLocalRule hyp
State after:
case val.isSimple
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
hyp : ¬Simple LR
this : ∃ Lcond Rcond ress x, Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ False

State before:
case val.isSimple
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
hyp : ¬Simple LR
this : ∃ Lcond Rcond ress x, Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ False
Tactic:
aesop
State after:
no goals

State before:
LR : TNode
canApplyRule : ¬¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
Tactic:
rw [not_not] at canApplyRule
State after:
LR : TNode
canApplyRule : ∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)

State before:
LR : TNode
canApplyRule : ∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
Tactic:
rcases canApplyRule with ⟨LCond, RCond, C, lr_exists, preconL, preconR⟩
State after:
case intro.intro.intro.intro.intro
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
lr_exists : Nonempty (LocalRule (LCond, RCond) C)
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)

State before:
case intro.intro.intro.intro.intro
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
lr_exists : Nonempty (LocalRule (LCond, RCond) C)
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
Tactic:
cases' lr_exists with lr
State after:
case intro.intro.intro.intro.intro.intro
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ Nonempty (LocalTableau LR)

State before:
case intro.intro.intro.intro.intro.intro
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ Nonempty (LocalTableau LR)
Tactic:
constructor
State after:
case intro.intro.intro.intro.intro.intro.val
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ LocalTableau LR

State before:
case intro.intro.intro.intro.intro.intro.val
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ LocalTableau LR
Tactic:
apply LocalTableau.fromRule
State after:
case intro.intro.intro.intro.intro.intro.val.ruleA
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ LocalRuleApp LR ?intro.intro.intro.intro.intro.intro.val.C

case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ (c : TNode) → c ∈ ?intro.intro.intro.intro.intro.intro.val.C → LocalTableau c

case intro.intro.intro.intro.intro.intro.val.C
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ List TNode

State before:
case intro.intro.intro.intro.intro.intro.val.ruleA
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ LocalRuleApp LR ?intro.intro.intro.intro.intro.intro.val.C

case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ (c : TNode) → c ∈ ?intro.intro.intro.intro.intro.intro.val.C → LocalTableau c

case intro.intro.intro.intro.intro.intro.val.C
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ List TNode
Tactic:
apply LocalRuleApp.mk C LCond RCond lr ⟨preconL, preconR⟩
State after:
case intro.intro.intro.intro.intro.intro.val.C
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ List TNode

LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ ?intro.intro.intro.intro.intro.intro.val.C = applyLocalRule lr (LR.1, LR.2)

case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ (c : TNode) → c ∈ ?intro.intro.intro.intro.intro.intro.val.C → LocalTableau c

case intro.intro.intro.intro.intro.intro.val.C
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ List TNode

State before:
case intro.intro.intro.intro.intro.intro.val.C
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ List TNode

LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ ?intro.intro.intro.intro.intro.intro.val.C = applyLocalRule lr (LR.1, LR.2)

case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ (c : TNode) → c ∈ ?intro.intro.intro.intro.intro.intro.val.C → LocalTableau c

case intro.intro.intro.intro.intro.intro.val.C
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ List TNode
Tactic:
use applyLocalRule lr (LR.1, LR.2)
State after:
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ applyLocalRule lr (LR.1, LR.2) = applyLocalRule lr (LR.1, LR.2)

case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ (c : TNode) → c ∈ applyLocalRule lr (LR.1, LR.2) → LocalTableau c

State before:
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ applyLocalRule lr (LR.1, LR.2) = applyLocalRule lr (LR.1, LR.2)

case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ (c : TNode) → c ∈ applyLocalRule lr (LR.1, LR.2) → LocalTableau c
Tactic:
rfl
State after:
case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ (c : TNode) → c ∈ applyLocalRule lr (LR.1, LR.2) → LocalTableau c

State before:
case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
⊢ (c : TNode) → c ∈ applyLocalRule lr (LR.1, LR.2) → LocalTableau c
Tactic:
intro c c_in
State after:
case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
c : TNode
c_in : c ∈ applyLocalRule lr (LR.1, LR.2)
⊢ LocalTableau c

State before:
case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
c : TNode
c_in : c ∈ applyLocalRule lr (LR.1, LR.2)
⊢ LocalTableau c
Tactic:
let ruleA := @LocalRuleApp.mk LR.1 LR.2 (applyLocalRule lr (LR.1, LR.2)) _ LCond RCond lr rfl ⟨preconL, preconR⟩
State after:
case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
c : TNode
c_in : c ∈ applyLocalRule lr (LR.1, LR.2)
ruleA : LocalRuleApp (LR.1, LR.2) (applyLocalRule lr (LR.1, LR.2)) := LocalRuleApp.mk C LCond RCond lr ⋯
⊢ LocalTableau c

State before:
case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
c : TNode
c_in : c ∈ applyLocalRule lr (LR.1, LR.2)
ruleA : LocalRuleApp (LR.1, LR.2) (applyLocalRule lr (LR.1, LR.2)) := LocalRuleApp.mk C LCond RCond lr ⋯
⊢ LocalTableau c
Tactic:
have := localRuleAppDecreasesLength ruleA c c_in
State after:
case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
c : TNode
c_in : c ∈ applyLocalRule lr (LR.1, LR.2)
ruleA : LocalRuleApp (LR.1, LR.2) (applyLocalRule lr (LR.1, LR.2)) := LocalRuleApp.mk C LCond RCond lr ⋯
this : lengthOfTNode c < lengthOfTNode (LR.1, LR.2)
⊢ LocalTableau c

State before:
case intro.intro.intro.intro.intro.intro.val.subTabs
LR : TNode
LCond RCond : Finset Formula
C : List SubPair
preconL : LCond ⊆ LR.1
preconR : RCond ⊆ LR.2
lr : LocalRule (LCond, RCond) C
c : TNode
c_in : c ∈ applyLocalRule lr (LR.1, LR.2)
ruleA : LocalRuleApp (LR.1, LR.2) (applyLocalRule lr (LR.1, LR.2)) := LocalRuleApp.mk C LCond RCond lr ⋯
this : lengthOfTNode c < lengthOfTNode (LR.1, LR.2)
⊢ LocalTableau c
Tactic:
apply Classical.choice (existsLocalTableauFor c)
State after:
no goals