internlm/Lean-Github huggingface dataset:
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a.right
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (L, R).2
Tactic:
apply proj_does_not_increase_vocab
Proof state after:
case a.right.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (projection (L, R).2)
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a.right.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ℓ ∈ voc (projection (L, R).2)
Tactic:
simp
Proof state after:
case a.right.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
Theorem: diamondproj_does_not_increase_vocab_R
Proof state before:
case a.right.a
φ : Formula
R L : Finset Formula
valid_proj : ~(□φ) ∈ R
ℓ : Char
ℓ_in_proj : ℓ ∈ voc (diamondProjectTNode (Sum.inr φ) (L, R)).1 ∩ voc (diamondProjectTNode (Sum.inr φ) (L, R)).2
ℓ_right : ℓ ∈ vocabOfFormula φ ∨ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
ψ : Formula
ψ_in_proj : ψ ∈ projection R
ℓ_in_ψ : ℓ ∈ vocabOfFormula ψ
⊢ ∃ a ∈ projection R, ℓ ∈ vocabOfFormula a
Tactic:
use ψ
Proof state after:
no goals
Theorem: endNodesOfSimple
Proof state before:
LR : TNode
hyp : Simple LR
⊢ endNodesOf ⟨LR, fromSimple hyp⟩ = [LR]
Tactic:
simp only [endNodesOf]
Proof state after:
no goals
Theorem: lrEndNodes
Proof state before:
LR : TNode
C : List TNode
ruleA : LocalRuleApp LR C
subTabs : (c : TNode) → c ∈ C → LocalTableau c
⊢ endNodesOf ⟨LR, fromRule ruleA subTabs⟩ =
    (List.map
        (fun x =>
          match x with
          | ⟨c, c_in⟩ => endNodesOf ⟨c, subTabs c c_in⟩)
        C.attach).join
Tactic:
simp only [endNodesOf]
Proof state after:
no goals
Theorem: endNodesOfLEQ
Proof state before:
LR Z : TNode
ltLR : LocalTableau LR
⊢ Z ∈ endNodesOf ⟨LR, ltLR⟩ → lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
cases ltLR
Proof state after:
case fromRule
LR Z : TNode
C✝ : List TNode
subTabs✝ : (c : TNode) → c ∈ C✝ → LocalTableau c
ruleA✝ : LocalRuleApp LR C✝
⊢ Z ∈ endNodesOf ⟨LR, fromRule ruleA✝ subTabs✝⟩ → lengthOfTNode Z ≤ lengthOfTNode LR

case fromSimple
LR Z : TNode
isSimple✝ : Simple LR
⊢ Z ∈ endNodesOf ⟨LR, fromSimple isSimple✝⟩ → lengthOfTNode Z ≤ lengthOfTNode LR
Theorem: endNodesOfLEQ
Proof state before:
LR Z : TNode
LR_simp : Simple LR
⊢ Z ∈ endNodesOf ⟨LR, fromSimple LR_simp⟩ → lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
case fromSimple LR_simp => intro Z_endOf_Y; aesop
Proof state after:
no goals
Theorem: endNodesOfLEQ
Proof state before:
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
⊢ Z ∈ endNodesOf ⟨LR, fromRule lrApp subTabs⟩ → lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
intro Z_endOf_LR
Proof state after:
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
Z_endOf_LR : Z ∈ endNodesOf ⟨LR, fromRule lrApp subTabs⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Theorem: endNodesOfLEQ
Proof state before:
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
Z_endOf_LR : Z ∈ endNodesOf ⟨LR, fromRule lrApp subTabs⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
simp at Z_endOf_LR
Proof state after:
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
Z_endOf_LR : ∃ l, (∃ a, ∃ (h : a ∈ altLR), endNodesOf ⟨a, subTabs a ⋯⟩ = l) ∧ Z ∈ l
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Theorem: endNodesOfLEQ
Proof state before:
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
Z_endOf_LR : ∃ l, (∃ a, ∃ (h : a ∈ altLR), endNodesOf ⟨a, subTabs a ⋯⟩ = l) ∧ Z ∈ l
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
rcases Z_endOf_LR with ⟨ZS, ⟨c, c_in_C, endNodes_c_eq_ZS⟩, Z_in_ZS⟩
Proof state after:
case intro.intro.intro.intro
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
ZS : List TNode
Z_in_ZS : Z ∈ ZS
c : TNode
c_in_C : c ∈ altLR
endNodes_c_eq_ZS : endNodesOf ⟨c, subTabs c ⋯⟩ = ZS
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Theorem: endNodesOfLEQ
Proof state before:
case intro.intro.intro.intro
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
ZS : List TNode
Z_in_ZS : Z ∈ ZS
c : TNode
c_in_C : c ∈ altLR
endNodes_c_eq_ZS : endNodesOf ⟨c, subTabs c ⋯⟩ = ZS
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
subst endNodes_c_eq_ZS
Proof state after:
case intro.intro.intro.intro
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Theorem: endNodesOfLEQ
Proof state before:
case intro.intro.intro.intro
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
apply le_of_lt
Proof state after:
case intro.intro.intro.intro.a
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
⊢ lengthOfTNode Z < lengthOfTNode LR
Theorem: endNodesOfLEQ
Proof state before:
case intro.intro.intro.intro.a
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
⊢ lengthOfTNode Z < lengthOfTNode LR
Tactic:
have := localRuleAppDecreasesLength lrApp c c_in_C
Proof state after:
case intro.intro.intro.intro.a
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
this : lengthOfTNode c < lengthOfTNode (LR.1, LR.2)
⊢ lengthOfTNode Z < lengthOfTNode LR
Theorem: endNodesOfLEQ
Proof state before:
case intro.intro.intro.intro.a
LR Z : TNode
altLR : List TNode
subTabs : (c : TNode) → c ∈ altLR → LocalTableau c
lrApp : LocalRuleApp LR altLR
c : TNode
c_in_C : c ∈ altLR
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
this : lengthOfTNode c < lengthOfTNode (LR.1, LR.2)
⊢ lengthOfTNode Z < lengthOfTNode LR
Tactic:
calc
  lengthOfTNode Z ≤ lengthOfTNode c := endNodesOfLEQ Z_in_ZS
  _ < lengthOfTNode LR := this
Proof state after:
no goals
Theorem: endNodesOfLEQ
Proof state before:
LR Z : TNode
LR_simp : Simple LR
⊢ Z ∈ endNodesOf ⟨LR, fromSimple LR_simp⟩ → lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
intro Z_endOf_Y
Proof state after:
LR Z : TNode
LR_simp : Simple LR
Z_endOf_Y : Z ∈ endNodesOf ⟨LR, fromSimple LR_simp⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Theorem: endNodesOfLEQ
Proof state before:
LR Z : TNode
LR_simp : Simple LR
Z_endOf_Y : Z ∈ endNodesOf ⟨LR, fromSimple LR_simp⟩
⊢ lengthOfTNode Z ≤ lengthOfTNode LR
Tactic:
aesop
Proof state after:
no goals
Theorem: endNodesOfLocalRuleLT
Proof state before:
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
⊢ Z ∈ endNodesOf ⟨LR, fromRule lrApp subTabs⟩ → lengthOfTNode Z < lengthOfTNode LR
Tactic:
intro Z_endOf_LR
Proof state after:
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
Z_endOf_LR : Z ∈ endNodesOf ⟨LR, fromRule lrApp subTabs⟩
⊢ lengthOfTNode Z < lengthOfTNode LR
Theorem: endNodesOfLocalRuleLT
Proof state before:
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
Z_endOf_LR : Z ∈ endNodesOf ⟨LR, fromRule lrApp subTabs⟩
⊢ lengthOfTNode Z < lengthOfTNode LR
Tactic:
simp at Z_endOf_LR
Proof state after:
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
Z_endOf_LR : ∃ l, (∃ a, ∃ (h : a ∈ a✝), endNodesOf ⟨a, subTabs a ⋯⟩ = l) ∧ Z ∈ l
⊢ lengthOfTNode Z < lengthOfTNode LR
Theorem: endNodesOfLocalRuleLT
Proof state before:
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
Z_endOf_LR : ∃ l, (∃ a, ∃ (h : a ∈ a✝), endNodesOf ⟨a, subTabs a ⋯⟩ = l) ∧ Z ∈ l
⊢ lengthOfTNode Z < lengthOfTNode LR
Tactic:
rcases Z_endOf_LR with ⟨ZS, ⟨c, c_in_C, endNodes_c_eq_ZS⟩, Z_in_ZS⟩
Proof state after:
case intro.intro.intro.intro
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
ZS : List TNode
Z_in_ZS : Z ∈ ZS
c : TNode
c_in_C : c ∈ a✝
endNodes_c_eq_ZS : endNodesOf ⟨c, subTabs c ⋯⟩ = ZS
⊢ lengthOfTNode Z < lengthOfTNode LR
Theorem: endNodesOfLocalRuleLT
Proof state before:
case intro.intro.intro.intro
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
ZS : List TNode
Z_in_ZS : Z ∈ ZS
c : TNode
c_in_C : c ∈ a✝
endNodes_c_eq_ZS : endNodesOf ⟨c, subTabs c ⋯⟩ = ZS
⊢ lengthOfTNode Z < lengthOfTNode LR
Tactic:
subst endNodes_c_eq_ZS
Proof state after:
case intro.intro.intro.intro
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
c : TNode
c_in_C : c ∈ a✝
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
⊢ lengthOfTNode Z < lengthOfTNode LR
Theorem: endNodesOfLocalRuleLT
Proof state before:
case intro.intro.intro.intro
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
c : TNode
c_in_C : c ∈ a✝
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
⊢ lengthOfTNode Z < lengthOfTNode LR
Tactic:
have := localRuleAppDecreasesLength lrApp c c_in_C
Proof state after:
case intro.intro.intro.intro
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
c : TNode
c_in_C : c ∈ a✝
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
this : lengthOfTNode c < lengthOfTNode (LR.1, LR.2)
⊢ lengthOfTNode Z < lengthOfTNode LR
Theorem: endNodesOfLocalRuleLT
Proof state before:
case intro.intro.intro.intro
Z LR : TNode
a✝ : List TNode
lrApp : LocalRuleApp LR a✝
subTabs : (c : TNode) → c ∈ a✝ → LocalTableau c
c : TNode
c_in_C : c ∈ a✝
Z_in_ZS : Z ∈ endNodesOf ⟨c, subTabs c ⋯⟩
this : lengthOfTNode c < lengthOfTNode (LR.1, LR.2)
⊢ lengthOfTNode Z < lengthOfTNode LR
Tactic:
calc
  lengthOfTNode Z ≤ lengthOfTNode c := endNodesOfLEQ Z_in_ZS
  _ < lengthOfTNode LR := this
Proof state after:
no goals
Theorem: existsLocalTableauFor
Proof state before:
LR : TNode
⊢ Nonempty (LocalTableau LR)
Tactic:
cases em ¬(∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2)
Proof 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)
Theorem: existsLocalTableauFor
Proof 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
Proof state after:
no goals
Theorem: existsLocalTableauFor
Proof 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)
Proof state after:
no goals
Theorem: existsLocalTableauFor
Proof state before:
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
Tactic:
constructor
Proof state after:
case val
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ LocalTableau LR
Theorem: existsLocalTableauFor
Proof 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
Proof state after:
case val.isSimple
LR : TNode
canApplyRule : ¬∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Simple LR
Theorem: existsLocalTableauFor
Proof 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
Proof 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
Theorem: existsLocalTableauFor
Proof 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
Proof 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
Theorem: existsLocalTableauFor
Proof 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
Proof state after:
no goals
Theorem: existsLocalTableauFor
Proof 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
Proof state after:
LR : TNode
canApplyRule : ∃ Lcond Rcond C, Nonempty (LocalRule (Lcond, Rcond) C) ∧ Lcond ⊆ LR.1 ∧ Rcond ⊆ LR.2
⊢ Nonempty (LocalTableau LR)
Theorem: existsLocalTableauFor
Proof 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⟩
Proof 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)
Theorem: existsLocalTableauFor
Proof 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
Proof 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)
Theorem: existsLocalTableauFor
Proof 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
Proof 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
Theorem: existsLocalTableauFor
Proof 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
Proof 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
Theorem: existsLocalTableauFor
Proof 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⟩
Proof 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
Theorem: existsLocalTableauFor
Proof 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)
Proof 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
Theorem: existsLocalTableauFor
Proof 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
Proof 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
Theorem: existsLocalTableauFor
Proof 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
Proof 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
Theorem: existsLocalTableauFor
Proof 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⟩
Proof 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
Theorem: existsLocalTableauFor
Proof 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
Proof 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