internlm/Lean-Github huggingface dataset:
Theorem: LocalRuleUniqueR
Proof state before:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
Rcond' : Finset Formula
R_cond_in : Rcond' ⊆ R
ress : List (Finset Formula)
L_cond_in : ∅ ⊆ L
orule' : OneSidedLocalRule Rcond' ress
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR orule') (L, R)
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2
Tactic:
cases orule'
Proof state after:
case bot
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
R_cond_in : {⊥} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR OneSidedLocalRule.bot) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2

case not
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ : Formula
R_cond_in : {φ✝, ~φ✝} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.not φ✝)) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2

case neg
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ : Formula
R_cond_in : {~~φ✝} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.neg φ✝)) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2

case con
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ ψ✝ : Formula
R_cond_in : {φ✝⋀ψ✝} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.con φ✝ ψ✝)) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2

case ncon
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ ψ✝ : Formula
R_cond_in : {~(φ✝⋀ψ✝)} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2
Theorem: LocalRuleUniqueR
Proof state before:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ' ψ' : Formula
R_cond_in : {φ'⋀ψ'} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.con φ' ψ')) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2
Tactic:
case con φ' ψ' =>
  simp_all
  subst c_in
  subst precond_eq
  if φ = φ' ∧ ψ = ψ'
  then
    apply Or.inr
    refine Finset.insert_subset_iff.mpr ?_
    aesop
  else aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
case bot
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
R_cond_in : {⊥} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR OneSidedLocalRule.bot) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2

case not
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ : Formula
R_cond_in : {φ✝, ~φ✝} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.not φ✝)) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2

case neg
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ : Formula
R_cond_in : {~~φ✝} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.neg φ✝)) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2

case ncon
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ ψ✝ : Formula
R_cond_in : {~(φ✝⋀ψ✝)} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2
Tactic:
all_goals aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ' ψ' : Formula
R_cond_in : {φ'⋀ψ'} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.con φ' ψ')) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2
Tactic:
simp_all
Proof state after:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ φ' ψ' : Formula
precond_eq : φ⋀ψ = α
R_cond_in : φ'⋀ψ' ∈ R
c_in : c = (L, insert φ' (insert ψ' (R.erase (φ'⋀ψ'))))
⊢ (α = φ' ∨ α = ψ' ∨ ¬α = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Theorem: LocalRuleUniqueR
Proof state before:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ φ' ψ' : Formula
precond_eq : φ⋀ψ = α
R_cond_in : φ'⋀ψ' ∈ R
c_in : c = (L, insert φ' (insert ψ' (R.erase (φ'⋀ψ'))))
⊢ (α = φ' ∨ α = ψ' ∨ ¬α = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Tactic:
subst c_in
Proof state after:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
φ ψ φ' ψ' : Formula
precond_eq : φ⋀ψ = α
R_cond_in : φ'⋀ψ' ∈ R
⊢ (α = φ' ∨ α = ψ' ∨ ¬α = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Theorem: LocalRuleUniqueR
Proof state before:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
φ ψ φ' ψ' : Formula
precond_eq : φ⋀ψ = α
R_cond_in : φ'⋀ψ' ∈ R
⊢ (α = φ' ∨ α = ψ' ∨ ¬α = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Tactic:
subst precond_eq
Proof state after:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : φ'⋀ψ' ∈ R
α_in_R : φ⋀ψ ∈ R
⊢ (φ⋀ψ = φ' ∨ φ⋀ψ = ψ' ∨ ¬φ⋀ψ = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : φ'⋀ψ' ∈ R
α_in_R : φ⋀ψ ∈ R
⊢ (φ⋀ψ = φ' ∨ φ⋀ψ = ψ' ∨ ¬φ⋀ψ = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Tactic:
if φ = φ' ∧ ψ = ψ'
then
  apply Or.inr
  refine Finset.insert_subset_iff.mpr ?_
  aesop
else aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : φ'⋀ψ' ∈ R
α_in_R : φ⋀ψ ∈ R
h✝ : φ = φ' ∧ ψ = ψ'
⊢ (φ⋀ψ = φ' ∨ φ⋀ψ = ψ' ∨ ¬φ⋀ψ = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Tactic:
apply Or.inr
Proof state after:
case h
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : φ'⋀ψ' ∈ R
α_in_R : φ⋀ψ ∈ R
h✝ : φ = φ' ∧ ψ = ψ'
⊢ {φ, ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Theorem: LocalRuleUniqueR
Proof state before:
case h
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : φ'⋀ψ' ∈ R
α_in_R : φ⋀ψ ∈ R
h✝ : φ = φ' ∧ ψ = ψ'
⊢ {φ, ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Tactic:
refine Finset.insert_subset_iff.mpr ?_
Proof state after:
case h
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : φ'⋀ψ' ∈ R
α_in_R : φ⋀ψ ∈ R
h✝ : φ = φ' ∧ ψ = ψ'
⊢ φ ∈ insert φ' (insert ψ' (R.erase (φ'⋀ψ'))) ∧ {ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Theorem: LocalRuleUniqueR
Proof state before:
case h
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : φ'⋀ψ' ∈ R
α_in_R : φ⋀ψ ∈ R
h✝ : φ = φ' ∧ ψ = ψ'
⊢ φ ∈ insert φ' (insert ψ' (R.erase (φ'⋀ψ'))) ∧ {ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Tactic:
aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : φ'⋀ψ' ∈ R
α_in_R : φ⋀ψ ∈ R
h✝ : ¬(φ = φ' ∧ ψ = ψ')
⊢ (φ⋀ψ = φ' ∨ φ⋀ψ = ψ' ∨ ¬φ⋀ψ = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (R.erase (φ'⋀ψ')))
Tactic:
aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
case ncon
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
L_cond_in : ∅ ⊆ L
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ ψ✝ : Formula
R_cond_in : {~(φ✝⋀ψ✝)} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.2
Tactic:
aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
Rcond' : Finset Formula
R_cond_in : Rcond' ⊆ R
ress : List (Finset Formula)
L_cond_in : ∅ ⊆ L
orule' : OneSidedLocalRule Rcond' ress
c_in : c ∈ applyLocalRule (LocalRule.oneSidedR orule') (L, R)
φ ψ : Formula
precond_eq : {~(φ⋀ψ)} = {α}
⊢ α ∈ c.2 ∨ ∃ res ∈ [{~φ}, {~ψ}], res ⊆ c.2
Tactic:
simp_all
Proof state after:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
Rcond' : Finset Formula
R_cond_in : Rcond' ⊆ R
ress : List (Finset Formula)
orule' : OneSidedLocalRule Rcond' ress
φ ψ : Formula
c_in : ∃ a ∈ ress, (L, R \ Rcond' ∪ a) = c
precond_eq : ~(φ⋀ψ) = α
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Theorem: LocalRuleUniqueR
Proof state before:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
Rcond' : Finset Formula
R_cond_in : Rcond' ⊆ R
ress : List (Finset Formula)
orule' : OneSidedLocalRule Rcond' ress
φ ψ : Formula
c_in : ∃ a ∈ ress, (L, R \ Rcond' ∪ a) = c
precond_eq : ~(φ⋀ψ) = α
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Tactic:
cases orule'
Proof state after:
case bot
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
R_cond_in : {⊥} ⊆ R
c_in : ∃ a ∈ ∅, (L, R \ {⊥} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case not
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ : Formula
R_cond_in : {φ✝, ~φ✝} ⊆ R
c_in : ∃ a ∈ ∅, (L, R \ {φ✝, ~φ✝} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case neg
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ : Formula
R_cond_in : {~~φ✝} ⊆ R
c_in : ∃ a ∈ [{φ✝}], (L, R \ {~~φ✝} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case con
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ ψ✝ : Formula
R_cond_in : {φ✝⋀ψ✝} ⊆ R
c_in : ∃ a ∈ [{φ✝, ψ✝}], (L, R \ {φ✝⋀ψ✝} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case ncon
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ ψ✝ : Formula
R_cond_in : {~(φ✝⋀ψ✝)} ⊆ R
c_in : ∃ a ∈ [{~φ✝}, {~ψ✝}], (L, R \ {~(φ✝⋀ψ✝)} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Theorem: LocalRuleUniqueR
Proof state before:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
c_in : ∃ a ∈ [{~φ'}, {~ψ'}], (L, R \ {~(φ'⋀ψ')} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Tactic:
case ncon φ' ψ' =>
  simp at c_in
  subst precond_eq
  cases c_in
  case inl c_eq =>
    subst c_eq
    if φ = φ'
    then simp_all
    else aesop
  case inr c_eq =>
    subst c_eq
    if ψ = ψ'
    then simp_all
    else aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
case bot
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
R_cond_in : {⊥} ⊆ R
c_in : ∃ a ∈ ∅, (L, R \ {⊥} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case not
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ : Formula
R_cond_in : {φ✝, ~φ✝} ⊆ R
c_in : ∃ a ∈ ∅, (L, R \ {φ✝, ~φ✝} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case neg
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ : Formula
R_cond_in : {~~φ✝} ⊆ R
c_in : ∃ a ∈ [{φ✝}], (L, R \ {~~φ✝} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case con
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ ψ✝ : Formula
R_cond_in : {φ✝⋀ψ✝} ⊆ R
c_in : ∃ a ∈ [{φ✝, ψ✝}], (L, R \ {φ✝⋀ψ✝} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Tactic:
all_goals aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
c_in : ∃ a ∈ [{~φ'}, {~ψ'}], (L, R \ {~(φ'⋀ψ')} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Tactic:
simp at c_in
Proof state after:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
c_in : (L, insert (~φ') (R.erase (~(φ'⋀ψ')))) = c ∨ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Theorem: LocalRuleUniqueR
Proof state before:
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
c_in : (L, insert (~φ') (R.erase (~(φ'⋀ψ')))) = c ∨ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Tactic:
subst precond_eq
Proof state after:
R L : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
c_in : (L, insert (~φ') (R.erase (~(φ'⋀ψ')))) = c ∨ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))) = c
α_in_R : ~(φ⋀ψ) ∈ R
⊢ ~(φ⋀ψ) ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
c_in : (L, insert (~φ') (R.erase (~(φ'⋀ψ')))) = c ∨ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))) = c
α_in_R : ~(φ⋀ψ) ∈ R
⊢ ~(φ⋀ψ) ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Tactic:
cases c_in
Proof state after:
case inl
R L : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
h✝ : (L, insert (~φ') (R.erase (~(φ'⋀ψ')))) = c
⊢ ~(φ⋀ψ) ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2

case inr
R L : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
h✝ : (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))) = c
⊢ ~(φ⋀ψ) ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
c_eq : (L, insert (~φ') (R.erase (~(φ'⋀ψ')))) = c
⊢ ~(φ⋀ψ) ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Tactic:
case inl c_eq =>
  subst c_eq
  if φ = φ'
  then simp_all
  else aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
c_eq : (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))) = c
⊢ ~(φ⋀ψ) ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Tactic:
case inr c_eq =>
  subst c_eq
  if ψ = ψ'
  then simp_all
  else aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
c_eq : (L, insert (~φ') (R.erase (~(φ'⋀ψ')))) = c
⊢ ~(φ⋀ψ) ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Tactic:
subst c_eq
Proof state after:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
⊢ ~(φ⋀ψ) ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2 ∨
    ~φ ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2 ∨ ~ψ ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
⊢ ~(φ⋀ψ) ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2 ∨
    ~φ ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2 ∨ ~ψ ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2
Tactic:
if φ = φ'
then simp_all
else aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
h✝ : φ = φ'
⊢ ~(φ⋀ψ) ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2 ∨
    ~φ ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2 ∨ ~ψ ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2
Tactic:
simp_all
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
h✝ : ¬φ = φ'
⊢ ~(φ⋀ψ) ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2 ∨
    ~φ ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2 ∨ ~ψ ∈ (L, insert (~φ') (R.erase (~(φ'⋀ψ')))).2
Tactic:
aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
c_eq : (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))) = c
⊢ ~(φ⋀ψ) ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Tactic:
subst c_eq
Proof state after:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
⊢ ~(φ⋀ψ) ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2 ∨
    ~φ ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2 ∨ ~ψ ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
⊢ ~(φ⋀ψ) ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2 ∨
    ~φ ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2 ∨ ~ψ ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2
Tactic:
if ψ = ψ'
then simp_all
else aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
h✝ : ψ = ψ'
⊢ ~(φ⋀ψ) ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2 ∨
    ~φ ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2 ∨ ~ψ ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2
Tactic:
simp_all
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
R L : Finset Formula
φ ψ φ' ψ' : Formula
R_cond_in : {~(φ'⋀ψ')} ⊆ R
α_in_R : ~(φ⋀ψ) ∈ R
h✝ : ¬ψ = ψ'
⊢ ~(φ⋀ψ) ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2 ∨
    ~φ ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2 ∨ ~ψ ∈ (L, insert (~ψ') (R.erase (~(φ'⋀ψ')))).2
Tactic:
aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
case con
α : Formula
R L : Finset Formula
α_in_R : α ∈ R
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ ψ✝ : Formula
R_cond_in : {φ✝⋀ψ✝} ⊆ R
c_in : ∃ a ∈ [{φ✝, ψ✝}], (L, R \ {φ✝⋀ψ✝} ∪ a) = c
⊢ α ∈ c.2 ∨ ~φ ∈ c.2 ∨ ~ψ ∈ c.2
Tactic:
aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
α : Formula
R L precond : Finset Formula
ress : List (Finset Formula)
α_in_R : α ∈ R
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress✝ : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress✝
R_cond_in : ∅ ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL orule') (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ ress, res ⊆ c.2
Tactic:
apply Or.inl
Proof state after:
case h
α : Formula
R L precond : Finset Formula
ress : List (Finset Formula)
α_in_R : α ∈ R
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress✝ : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress✝
R_cond_in : ∅ ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL orule') (L, R)
⊢ α ∈ c.2
Theorem: LocalRuleUniqueR
Proof state before:
case h
α : Formula
R L precond : Finset Formula
ress : List (Finset Formula)
α_in_R : α ∈ R
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress✝ : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress✝
R_cond_in : ∅ ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL orule') (L, R)
⊢ α ∈ c.2
Tactic:
aesop
Proof state after:
no goals
Theorem: LocalRuleUniqueR
Proof state before:
case mk.intro.LRnegR
α : Formula
R L precond : Finset Formula
ress : List (Finset Formula)
α_in_R : α ∈ R
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
ϕ✝ : Formula
L_cond_in : {~ϕ✝} ⊆ L
R_cond_in : {ϕ✝} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.LRnegR ϕ✝) (L, R)
⊢ α ∈ c.2 ∨ ∃ res ∈ ress, res ⊆ c.2
Tactic:
simp_all
Proof state after:
no goals
Theorem: notSimpleThenLocalRule
Proof state before:
L R : Finset Formula
⊢ ¬Simple (L, R) → ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R
Tactic:
intro not_simple
Proof state after:
L R : Finset Formula
not_simple : ¬Simple (L, R)
⊢ ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R
Theorem: notSimpleThenLocalRule
Proof state before:
L R : Finset Formula
not_simple : ¬Simple (L, R)
⊢ ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R
Tactic:
let ⟨C, ruleA⟩ := notSimpleToRuleApp not_simple
Proof state after:
L R : Finset Formula
not_simple : ¬Simple (L, R)
C : List TNode
ruleA : LocalRuleApp (L, R) C
⊢ ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R
Theorem: notSimpleThenLocalRule
Proof state before:
L R : Finset Formula
not_simple : ¬Simple (L, R)
C : List TNode
ruleA : LocalRuleApp (L, R) C
⊢ ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R
Tactic:
match ruleA with
| @LocalRuleApp.mk _ _ _ ress Lcond Rcond rule _ pp => exact ⟨Lcond, Rcond, ress, rule, pp⟩
Proof state after:
no goals
Theorem: notSimpleThenLocalRule
Proof state before:
L R : Finset Formula
not_simple : ¬Simple (L, R)
C : List TNode
ruleA : LocalRuleApp (L, R) C
ress : List SubPair
Lcond Rcond : Finset Formula
rule : LocalRule (Lcond, Rcond) ress
hC✝ : C = applyLocalRule rule (L, R)
pp : Lcond ⊆ L ∧ Rcond ⊆ R
⊢ ∃ Lcond Rcond ress x, Lcond ⊆ L ∧ Rcond ⊆ R
Tactic:
exact ⟨Lcond, Rcond, ress, rule, pp⟩
Proof state after:
no goals
Theorem: conDecreasesLength
Proof state before:
φ ψ : Formula
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ
Tactic:
cases' em (φ = ψ) with heq hneq
Proof state after:
case inl
φ ψ : Formula
heq : φ = ψ
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ

case inr
φ ψ : Formula
hneq : ¬φ = ψ
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ
Theorem: conDecreasesLength
Proof state before:
case inl
φ ψ : Formula
heq : φ = ψ
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ
Tactic:
simp [heq] at *
Proof state after:
no goals
Theorem: conDecreasesLength
Proof state before:
case inr
φ ψ : Formula
hneq : ¬φ = ψ
⊢ ∑ x ∈ {φ, ψ}, lengthOfFormula x < 1 + lengthOfFormula φ + lengthOfFormula ψ
Tactic:
simp [Finset.sum_pair hneq]
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
⊢ ∀ res ∈ ress, lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
Tactic:
intro res in_ress
Proof state after:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
in_ress : res ∈ ress
⊢ lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
Theorem: localRuleDecreasesLengthSide
Proof state before:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
in_ress : res ∈ ress
⊢ lengthOf res.1 < lengthOf Lcond ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf Rcond ∧ res.1 = ∅
Tactic:
cases rule <;>
( first
  | ( rename_i rule
      cases rule
      <;> (simp at *; try rw [in_ress])
      case neg φ => simp [←Nat.add_assoc]
      case con φ ψ => simp; exact conDecreasesLength
      case ncon φ ψ =>
        cases' in_ress with case_phi case_psi
        <;> ( first
            | simp [case_psi]
            | ( simp [case_phi]
                rw [Nat.add_comm 1 (lengthOfFormula φ), Nat.add_assoc]
                aesop)))
  | all_goals aesop)
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~ϕ✝} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {ϕ✝} ∧ res.1 = ∅
Tactic:
first
| ( rename_i rule
    cases rule
    <;> (simp at *; try rw [in_ress])
    case neg φ => simp [←Nat.add_assoc]
    case con φ ψ => simp; exact conDecreasesLength
    case ncon φ ψ =>
      cases' in_ress with case_phi case_psi
      <;> ( first
          | simp [case_psi]
          | ( simp [case_phi]
              rw [Nat.add_comm 1 (lengthOfFormula φ), Nat.add_assoc]
              aesop)))
| all_goals aesop
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~ϕ✝} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {ϕ✝} ∧ res.1 = ∅
Tactic:
( rename_i rule
  cases rule
  <;> (simp at *; try rw [in_ress])
  case neg φ => simp [←Nat.add_assoc]
  case con φ ψ => simp; exact conDecreasesLength
  case ncon φ ψ =>
    cases' in_ress with case_phi case_psi
    <;> ( first
        | simp [case_psi]
        | ( simp [case_phi]
            rw [Nat.add_comm 1 (lengthOfFormula φ), Nat.add_assoc]
            aesop)))
Proof state after:
no goals
Theorem: localRuleDecreasesLengthSide
Proof state before:
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~ϕ✝} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {ϕ✝} ∧ res.1 = ∅
Tactic:
rename_i rule
Proof state after:
case LRnegR
res : SubPair
rule : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~rule} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {rule} ∧ res.1 = ∅
Theorem: localRuleDecreasesLengthSide
Proof state before:
case LRnegR
res : SubPair
rule : Formula
in_ress : res ∈ ∅
⊢ lengthOf res.1 < lengthOf {~rule} ∧ res.2 = ∅ ∨ lengthOf res.2 < lengthOf {rule} ∧ res.1 = ∅
Tactic:
cases rule
<;> (simp at *; try rw [in_ress])
Proof state after:
no goals