Theorem: LocalRuleUniqueL (Bml/Tableau.lean)

State before:
α : Formula
L R : Finset Formula
C : List TNode
precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
lrApp : LocalRuleApp (L, R) C
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
⊢ ∀ c ∈ C, α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1
Tactic:
intro c c_in
State after:
α : Formula
L R : Finset Formula
C : List TNode
precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
lrApp : LocalRuleApp (L, R) C
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
c_in : c ∈ C
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1

State before:
α : Formula
L R : Finset Formula
C : List TNode
precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
lrApp : LocalRuleApp (L, R) C
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
c_in : c ∈ C
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1
Tactic:
rcases lrApp with ⟨ress', Lcond', Rcond', lr', L_cond_in, R_cond_in⟩
State after:
case mk.intro
α : Formula
L R : Finset Formula
C : List TNode
precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
c_in : c ∈ C
ress' : List SubPair
Lcond' Rcond' : Finset Formula
lr' : LocalRule (Lcond', Rcond') ress'
hC✝ : C = applyLocalRule lr' (L, R)
L_cond_in : Lcond' ⊆ L
R_cond_in : Rcond' ⊆ R
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1

State before:
case mk.intro
α : Formula
L R : Finset Formula
C : List TNode
precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
c_in : c ∈ C
ress' : List SubPair
Lcond' Rcond' : Finset Formula
lr' : LocalRule (Lcond', Rcond') ress'
hC✝ : C = applyLocalRule lr' (L, R)
L_cond_in : Lcond' ⊆ L
R_cond_in : Rcond' ⊆ R
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1
Tactic:
rename_i C_eq
State after:
case mk.intro
α : Formula
L R : Finset Formula
C : List TNode
precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
c_in : c ∈ C
ress' : List SubPair
Lcond' Rcond' : Finset Formula
lr' : LocalRule (Lcond', Rcond') ress'
C_eq : C = applyLocalRule lr' (L, R)
L_cond_in : Lcond' ⊆ L
R_cond_in : Rcond' ⊆ R
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1

State before:
case mk.intro
α : Formula
L R : Finset Formula
C : List TNode
precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
c_in : c ∈ C
ress' : List SubPair
Lcond' Rcond' : Finset Formula
lr' : LocalRule (Lcond', Rcond') ress'
C_eq : C = applyLocalRule lr' (L, R)
L_cond_in : Lcond' ⊆ L
R_cond_in : Rcond' ⊆ R
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1
Tactic:
subst C_eq
State after:
case mk.intro
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
ress' : List SubPair
Lcond' Rcond' : Finset Formula
lr' : LocalRule (Lcond', Rcond') ress'
L_cond_in : Lcond' ⊆ L
R_cond_in : Rcond' ⊆ R
c_in : c ∈ applyLocalRule lr' (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1

State before:
case mk.intro
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
ress' : List SubPair
Lcond' Rcond' : Finset Formula
lr' : LocalRule (Lcond', Rcond') ress'
L_cond_in : Lcond' ⊆ L
R_cond_in : Rcond' ⊆ R
c_in : c ∈ applyLocalRule lr' (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1
Tactic:
cases lr'
State after:
case mk.intro.oneSidedL
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
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.1 ∨ ∃ res ∈ ress, res ⊆ c.1

case mk.intro.oneSidedR
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
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)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1

case mk.intro.LRnegL
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
ϕ✝ : Formula
L_cond_in : {ϕ✝} ⊆ L
R_cond_in : {~ϕ✝} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.LRnegL ϕ✝) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1

case mk.intro.LRnegR
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
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.1 ∨ ∃ res ∈ ress, res ⊆ c.1

State before:
α : Formula
L R precond : Finset Formula
ress✝ : List (Finset Formula)
α_in_L : α ∈ L
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.1 ∨ ∃ res ∈ ress✝, res ⊆ c.1
Tactic:
case oneSidedL ress orule' =>
  cases orule
  case bot =>
    cases orule'
    all_goals aesop
  case not φ =>
    apply Finset.subset_of_eq at precond_eq
    rw [Finset.subset_singleton_iff'] at precond_eq
    simp_all
    rcases precond_eq with ⟨l,r⟩
    subst l
    cases r
  case neg φ =>
    cases orule'
    case neg φ' =>
      simp_all
      subst c_in
      subst precond_eq
      if φ = φ'
      then simp_all
      else simp_all
    all_goals aesop
  case con φ ψ =>
    cases orule'
    case con φ' ψ' =>
      simp_all
      subst c_in
      subst precond_eq
      if φ = φ' ∧ ψ = ψ'
      then
        apply Or.inr
        refine Finset.insert_subset_iff.mpr ?_
        aesop
      else aesop
    all_goals aesop
  case ncon φ ψ =>
    simp_all
    cases orule'
    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
    all_goals aesop
State after:
no goals

State before:
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
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)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1
Tactic:
case oneSidedR orule' =>
  apply Or.inl
  aesop
State after:
no goals

State before:
case mk.intro.LRnegL
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
c : TNode
ϕ✝ : Formula
L_cond_in : {ϕ✝} ⊆ L
R_cond_in : {~ϕ✝} ⊆ R
c_in : c ∈ applyLocalRule (LocalRule.LRnegL ϕ✝) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1

case mk.intro.LRnegR
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
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.1 ∨ ∃ res ∈ ress, res ⊆ c.1
Tactic:
all_goals simp_all
State after:
no goals

State before:
α : Formula
L R precond : Finset Formula
ress✝ : List (Finset Formula)
α_in_L : α ∈ L
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.1 ∨ ∃ res ∈ ress✝, res ⊆ c.1
Tactic:
cases orule
State after:
case bot
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
precond_eq : {⊥} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

case not
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ✝ : Formula
precond_eq : {φ✝, ~φ✝} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

case neg
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ✝ : Formula
precond_eq : {~~φ✝} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ✝}], res ⊆ c.1

case con
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ✝ ψ✝ : Formula
precond_eq : {φ✝⋀ψ✝} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ✝, ψ✝}], res ⊆ c.1

case ncon
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ✝ ψ✝ : Formula
precond_eq : {~(φ✝⋀ψ✝)} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ [{~φ✝}, {~ψ✝}], res ⊆ c.1

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
precond_eq : {⊥} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1
Tactic:
case bot =>
  cases orule'
  all_goals aesop
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ : Formula
precond_eq : {φ, ~φ} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1
Tactic:
case not φ =>
  apply Finset.subset_of_eq at precond_eq
  rw [Finset.subset_singleton_iff'] at precond_eq
  simp_all
  rcases precond_eq with ⟨l,r⟩
  subst l
  cases r
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ : Formula
precond_eq : {~~φ} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ}], res ⊆ c.1
Tactic:
case neg φ =>
  cases orule'
  case neg φ' =>
    simp_all
    subst c_in
    subst precond_eq
    if φ = φ'
    then simp_all
    else simp_all
  all_goals aesop
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1
Tactic:
case con φ ψ =>
  cases orule'
  case con φ' ψ' =>
    simp_all
    subst c_in
    subst precond_eq
    if φ = φ' ∧ ψ = ψ'
    then
      apply Or.inr
      refine Finset.insert_subset_iff.mpr ?_
      aesop
    else aesop
  all_goals aesop
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ ψ : Formula
precond_eq : {~(φ⋀ψ)} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ [{~φ}, {~ψ}], res ⊆ c.1
Tactic:
case ncon φ ψ =>
  simp_all
  cases orule'
  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
  all_goals aesop
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
precond_eq : {⊥} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1
Tactic:
cases orule'
State after:
case bot
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
precond_eq : {⊥} = {α}
L_cond_in : {⊥} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL OneSidedLocalRule.bot) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

case not
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
precond_eq : {⊥} = {α}
φ✝ : Formula
L_cond_in : {φ✝, ~φ✝} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.not φ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

case neg
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
precond_eq : {⊥} = {α}
φ✝ : Formula
L_cond_in : {~~φ✝} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.neg φ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

case con
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
precond_eq : {⊥} = {α}
φ✝ ψ✝ : Formula
L_cond_in : {φ✝⋀ψ✝} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.con φ✝ ψ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

case ncon
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
precond_eq : {⊥} = {α}
φ✝ ψ✝ : Formula
L_cond_in : {~(φ✝⋀ψ✝)} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

State before:
case bot
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
precond_eq : {⊥} = {α}
L_cond_in : {⊥} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL OneSidedLocalRule.bot) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

case not
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
precond_eq : {⊥} = {α}
φ✝ : Formula
L_cond_in : {φ✝, ~φ✝} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.not φ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

case neg
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
precond_eq : {⊥} = {α}
φ✝ : Formula
L_cond_in : {~~φ✝} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.neg φ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

case con
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
precond_eq : {⊥} = {α}
φ✝ ψ✝ : Formula
L_cond_in : {φ✝⋀ψ✝} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.con φ✝ ψ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

case ncon
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
precond_eq : {⊥} = {α}
φ✝ ψ✝ : Formula
L_cond_in : {~(φ✝⋀ψ✝)} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1
Tactic:
all_goals aesop
State after:
no goals

State before:
case ncon
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
precond_eq : {⊥} = {α}
φ✝ ψ✝ : Formula
L_cond_in : {~(φ✝⋀ψ✝)} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1
Tactic:
aesop
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ : Formula
precond_eq : {φ, ~φ} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1
Tactic:
apply Finset.subset_of_eq at precond_eq
State after:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ : Formula
precond_eq : {φ, ~φ} ⊆ {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ : Formula
precond_eq : {φ, ~φ} ⊆ {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1
Tactic:
rw [Finset.subset_singleton_iff'] at precond_eq
State after:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ : Formula
precond_eq : ∀ b ∈ {φ, ~φ}, b = α
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ : Formula
precond_eq : ∀ b ∈ {φ, ~φ}, b = α
⊢ α ∈ c.1 ∨ ∃ res ∈ ∅, res ⊆ c.1
Tactic:
simp_all
State after:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress
φ : Formula
c_in : ∃ a ∈ ress, (L \ Lcond' ∪ a, R) = c
precond_eq : φ = α ∧ ~φ = α
⊢ α ∈ c.1

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress
φ : Formula
c_in : ∃ a ∈ ress, (L \ Lcond' ∪ a, R) = c
precond_eq : φ = α ∧ ~φ = α
⊢ α ∈ c.1
Tactic:
rcases precond_eq with ⟨l,r⟩
State after:
case intro
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress
φ : Formula
c_in : ∃ a ∈ ress, (L \ Lcond' ∪ a, R) = c
l : φ = α
r : ~φ = α
⊢ α ∈ c.1

State before:
case intro
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress
φ : Formula
c_in : ∃ a ∈ ress, (L \ Lcond' ∪ a, R) = c
l : φ = α
r : ~φ = α
⊢ α ∈ c.1
Tactic:
subst l
State after:
case intro
L R : Finset Formula
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress
φ : Formula
c_in : ∃ a ∈ ress, (L \ Lcond' ∪ a, R) = c
α_in_L : φ ∈ L
r : ~φ = φ
⊢ φ ∈ c.1

State before:
case intro
L R : Finset Formula
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress
φ : Formula
c_in : ∃ a ∈ ress, (L \ Lcond' ∪ a, R) = c
α_in_L : φ ∈ L
r : ~φ = φ
⊢ φ ∈ c.1
Tactic:
cases r
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ : Formula
precond_eq : {~~φ} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ}], res ⊆ c.1
Tactic:
cases orule'
State after:
case bot
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ : Formula
precond_eq : {~~φ} = {α}
L_cond_in : {⊥} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL OneSidedLocalRule.bot) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ}], res ⊆ c.1

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

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

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

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

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ : Formula
precond_eq : {~~φ} = {α}
φ' : Formula
L_cond_in : {~~φ'} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.neg φ')) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ}], res ⊆ c.1
Tactic:
case neg φ' =>
  simp_all
  subst c_in
  subst precond_eq
  if φ = φ'
  then simp_all
  else simp_all
State after:
no goals

State before:
case bot
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ : Formula
precond_eq : {~~φ} = {α}
L_cond_in : {⊥} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL OneSidedLocalRule.bot) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ}], res ⊆ c.1

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

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

case ncon
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ : Formula
precond_eq : {~~φ} = {α}
φ✝ ψ✝ : Formula
L_cond_in : {~(φ✝⋀ψ✝)} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ}], res ⊆ c.1
Tactic:
all_goals aesop
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ : Formula
precond_eq : {~~φ} = {α}
φ' : Formula
L_cond_in : {~~φ'} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.neg φ')) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ}], res ⊆ c.1
Tactic:
simp_all
State after:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ φ' : Formula
precond_eq : ~~φ = α
L_cond_in : ~~φ' ∈ L
c_in : c = (insert φ' (L.erase (~~φ')), R)
⊢ (α = φ' ∨ ¬α = ~~φ') ∨ φ = φ' ∨ ¬φ = ~~φ' ∧ φ ∈ L

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ φ' : Formula
precond_eq : ~~φ = α
L_cond_in : ~~φ' ∈ L
c_in : c = (insert φ' (L.erase (~~φ')), R)
⊢ (α = φ' ∨ ¬α = ~~φ') ∨ φ = φ' ∨ ¬φ = ~~φ' ∧ φ ∈ L
Tactic:
subst c_in
State after:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
φ φ' : Formula
precond_eq : ~~φ = α
L_cond_in : ~~φ' ∈ L
⊢ (α = φ' ∨ ¬α = ~~φ') ∨ φ = φ' ∨ ¬φ = ~~φ' ∧ φ ∈ L

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
φ φ' : Formula
precond_eq : ~~φ = α
L_cond_in : ~~φ' ∈ L
⊢ (α = φ' ∨ ¬α = ~~φ') ∨ φ = φ' ∨ ¬φ = ~~φ' ∧ φ ∈ L
Tactic:
subst precond_eq
State after:
L R : Finset Formula
φ φ' : Formula
L_cond_in : ~~φ' ∈ L
α_in_L : ~~φ ∈ L
⊢ (~~φ = φ' ∨ ¬~~φ = ~~φ') ∨ φ = φ' ∨ ¬φ = ~~φ' ∧ φ ∈ L

State before:
L R : Finset Formula
φ φ' : Formula
L_cond_in : ~~φ' ∈ L
α_in_L : ~~φ ∈ L
⊢ (~~φ = φ' ∨ ¬~~φ = ~~φ') ∨ φ = φ' ∨ ¬φ = ~~φ' ∧ φ ∈ L
Tactic:
if φ = φ'
then simp_all
else simp_all
State after:
no goals

State before:
L R : Finset Formula
φ φ' : Formula
L_cond_in : ~~φ' ∈ L
α_in_L : ~~φ ∈ L
h✝ : φ = φ'
⊢ (~~φ = φ' ∨ ¬~~φ = ~~φ') ∨ φ = φ' ∨ ¬φ = ~~φ' ∧ φ ∈ L
Tactic:
simp_all
State after:
no goals

State before:
L R : Finset Formula
φ φ' : Formula
L_cond_in : ~~φ' ∈ L
α_in_L : ~~φ ∈ L
h✝ : ¬φ = φ'
⊢ (~~φ = φ' ∨ ¬~~φ = ~~φ') ∨ φ = φ' ∨ ¬φ = ~~φ' ∧ φ ∈ L
Tactic:
simp_all
State after:
no goals

State before:
case ncon
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ : Formula
precond_eq : {~~φ} = {α}
φ✝ ψ✝ : Formula
L_cond_in : {~(φ✝⋀ψ✝)} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ}], res ⊆ c.1
Tactic:
aesop
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1
Tactic:
cases orule'
State after:
case bot
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
L_cond_in : {⊥} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL OneSidedLocalRule.bot) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1

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

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

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

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

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ' ψ' : Formula
L_cond_in : {φ'⋀ψ'} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.con φ' ψ')) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1
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
State after:
no goals

State before:
case bot
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
L_cond_in : {⊥} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL OneSidedLocalRule.bot) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1

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

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

case ncon
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ ψ✝ : Formula
L_cond_in : {~(φ✝⋀ψ✝)} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1
Tactic:
all_goals aesop
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ' ψ' : Formula
L_cond_in : {φ'⋀ψ'} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.con φ' ψ')) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1
Tactic:
simp_all
State after:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ φ' ψ' : Formula
precond_eq : φ⋀ψ = α
L_cond_in : φ'⋀ψ' ∈ L
c_in : c = (insert φ' (insert ψ' (L.erase (φ'⋀ψ'))), R)
⊢ (α = φ' ∨ α = ψ' ∨ ¬α = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ φ' ψ' : Formula
precond_eq : φ⋀ψ = α
L_cond_in : φ'⋀ψ' ∈ L
c_in : c = (insert φ' (insert ψ' (L.erase (φ'⋀ψ'))), R)
⊢ (α = φ' ∨ α = ψ' ∨ ¬α = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))
Tactic:
subst c_in
State after:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
φ ψ φ' ψ' : Formula
precond_eq : φ⋀ψ = α
L_cond_in : φ'⋀ψ' ∈ L
⊢ (α = φ' ∨ α = ψ' ∨ ¬α = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
φ ψ φ' ψ' : Formula
precond_eq : φ⋀ψ = α
L_cond_in : φ'⋀ψ' ∈ L
⊢ (α = φ' ∨ α = ψ' ∨ ¬α = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))
Tactic:
subst precond_eq
State after:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : φ'⋀ψ' ∈ L
α_in_L : φ⋀ψ ∈ L
⊢ (φ⋀ψ = φ' ∨ φ⋀ψ = ψ' ∨ ¬φ⋀ψ = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))

State before:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : φ'⋀ψ' ∈ L
α_in_L : φ⋀ψ ∈ L
⊢ (φ⋀ψ = φ' ∨ φ⋀ψ = ψ' ∨ ¬φ⋀ψ = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))
Tactic:
if φ = φ' ∧ ψ = ψ'
then
  apply Or.inr
  refine Finset.insert_subset_iff.mpr ?_
  aesop
else aesop
State after:
no goals

State before:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : φ'⋀ψ' ∈ L
α_in_L : φ⋀ψ ∈ L
h✝ : φ = φ' ∧ ψ = ψ'
⊢ (φ⋀ψ = φ' ∨ φ⋀ψ = ψ' ∨ ¬φ⋀ψ = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))
Tactic:
apply Or.inr
State after:
case h
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : φ'⋀ψ' ∈ L
α_in_L : φ⋀ψ ∈ L
h✝ : φ = φ' ∧ ψ = ψ'
⊢ {φ, ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))

State before:
case h
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : φ'⋀ψ' ∈ L
α_in_L : φ⋀ψ ∈ L
h✝ : φ = φ' ∧ ψ = ψ'
⊢ {φ, ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))
Tactic:
refine Finset.insert_subset_iff.mpr ?_
State after:
case h
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : φ'⋀ψ' ∈ L
α_in_L : φ⋀ψ ∈ L
h✝ : φ = φ' ∧ ψ = ψ'
⊢ φ ∈ insert φ' (insert ψ' (L.erase (φ'⋀ψ'))) ∧ {ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))

State before:
case h
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : φ'⋀ψ' ∈ L
α_in_L : φ⋀ψ ∈ L
h✝ : φ = φ' ∧ ψ = ψ'
⊢ φ ∈ insert φ' (insert ψ' (L.erase (φ'⋀ψ'))) ∧ {ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))
Tactic:
aesop
State after:
no goals

State before:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : φ'⋀ψ' ∈ L
α_in_L : φ⋀ψ ∈ L
h✝ : ¬(φ = φ' ∧ ψ = ψ')
⊢ (φ⋀ψ = φ' ∨ φ⋀ψ = ψ' ∨ ¬φ⋀ψ = φ'⋀ψ') ∨ {φ, ψ} ⊆ insert φ' (insert ψ' (L.erase (φ'⋀ψ')))
Tactic:
aesop
State after:
no goals

State before:
case ncon
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
R_cond_in : ∅ ⊆ R
φ ψ : Formula
precond_eq : {φ⋀ψ} = {α}
φ✝ ψ✝ : Formula
L_cond_in : {~(φ✝⋀ψ✝)} ⊆ L
c_in : c ∈ applyLocalRule (LocalRule.oneSidedL (OneSidedLocalRule.ncon φ✝ ψ✝)) (L, R)
⊢ α ∈ c.1 ∨ ∃ res ∈ [{φ, ψ}], res ⊆ c.1
Tactic:
aesop
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
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)
φ ψ : Formula
precond_eq : {~(φ⋀ψ)} = {α}
⊢ α ∈ c.1 ∨ ∃ res ∈ [{~φ}, {~ψ}], res ⊆ c.1
Tactic:
simp_all
State after:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress
φ ψ : Formula
c_in : ∃ a ∈ ress, (L \ Lcond' ∪ a, R) = c
precond_eq : ~(φ⋀ψ) = α
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
Lcond' : Finset Formula
L_cond_in : Lcond' ⊆ L
ress : List (Finset Formula)
orule' : OneSidedLocalRule Lcond' ress
φ ψ : Formula
c_in : ∃ a ∈ ress, (L \ Lcond' ∪ a, R) = c
precond_eq : ~(φ⋀ψ) = α
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
Tactic:
cases orule'
State after:
case bot
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
L_cond_in : {⊥} ⊆ L
c_in : ∃ a ∈ ∅, (L \ {⊥} ∪ a, R) = c
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1

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

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

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

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

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
c_in : ∃ a ∈ [{~φ'}, {~ψ'}], (L \ {~(φ'⋀ψ')} ∪ a, R) = c
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
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
State after:
no goals

State before:
case bot
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
L_cond_in : {⊥} ⊆ L
c_in : ∃ a ∈ ∅, (L \ {⊥} ∪ a, R) = c
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1

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

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

case con
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ ψ✝ : Formula
L_cond_in : {φ✝⋀ψ✝} ⊆ L
c_in : ∃ a ∈ [{φ✝, ψ✝}], (L \ {φ✝⋀ψ✝} ∪ a, R) = c
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
Tactic:
all_goals aesop
State after:
no goals

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
c_in : ∃ a ∈ [{~φ'}, {~ψ'}], (L \ {~(φ'⋀ψ')} ∪ a, R) = c
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
Tactic:
simp at c_in
State after:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
c_in : (insert (~φ') (L.erase (~(φ'⋀ψ'))), R) = c ∨ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R) = c
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1

State before:
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
c_in : (insert (~φ') (L.erase (~(φ'⋀ψ'))), R) = c ∨ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R) = c
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
Tactic:
subst precond_eq
State after:
L R : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
c_in : (insert (~φ') (L.erase (~(φ'⋀ψ'))), R) = c ∨ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R) = c
α_in_L : ~(φ⋀ψ) ∈ L
⊢ ~(φ⋀ψ) ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1

State before:
L R : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
c_in : (insert (~φ') (L.erase (~(φ'⋀ψ'))), R) = c ∨ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R) = c
α_in_L : ~(φ⋀ψ) ∈ L
⊢ ~(φ⋀ψ) ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
Tactic:
cases c_in
State after:
case inl
L R : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
h✝ : (insert (~φ') (L.erase (~(φ'⋀ψ'))), R) = c
⊢ ~(φ⋀ψ) ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1

case inr
L R : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
h✝ : (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R) = c
⊢ ~(φ⋀ψ) ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1

State before:
L R : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
c_eq : (insert (~φ') (L.erase (~(φ'⋀ψ'))), R) = c
⊢ ~(φ⋀ψ) ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
Tactic:
case inl c_eq =>
  subst c_eq
  if φ = φ'
  then simp_all
  else aesop
State after:
no goals

State before:
L R : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
c_eq : (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R) = c
⊢ ~(φ⋀ψ) ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
Tactic:
case inr c_eq =>
  subst c_eq
  if ψ = ψ'
  then simp_all
  else aesop
State after:
no goals

State before:
L R : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
c_eq : (insert (~φ') (L.erase (~(φ'⋀ψ'))), R) = c
⊢ ~(φ⋀ψ) ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
Tactic:
subst c_eq
State after:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
⊢ ~(φ⋀ψ) ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1 ∨
    ~φ ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1 ∨ ~ψ ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1

State before:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
⊢ ~(φ⋀ψ) ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1 ∨
    ~φ ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1 ∨ ~ψ ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1
Tactic:
if φ = φ'
then simp_all
else aesop
State after:
no goals

State before:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
h✝ : φ = φ'
⊢ ~(φ⋀ψ) ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1 ∨
    ~φ ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1 ∨ ~ψ ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1
Tactic:
simp_all
State after:
no goals

State before:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
h✝ : ¬φ = φ'
⊢ ~(φ⋀ψ) ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1 ∨
    ~φ ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1 ∨ ~ψ ∈ (insert (~φ') (L.erase (~(φ'⋀ψ'))), R).1
Tactic:
aesop
State after:
no goals

State before:
L R : Finset Formula
c : TNode
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
c_eq : (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R) = c
⊢ ~(φ⋀ψ) ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
Tactic:
subst c_eq
State after:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
⊢ ~(φ⋀ψ) ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1 ∨
    ~φ ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1 ∨ ~ψ ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1

State before:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
⊢ ~(φ⋀ψ) ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1 ∨
    ~φ ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1 ∨ ~ψ ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1
Tactic:
if ψ = ψ'
then simp_all
else aesop
State after:
no goals

State before:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
h✝ : ψ = ψ'
⊢ ~(φ⋀ψ) ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1 ∨
    ~φ ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1 ∨ ~ψ ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1
Tactic:
simp_all
State after:
no goals

State before:
L R : Finset Formula
φ ψ φ' ψ' : Formula
L_cond_in : {~(φ'⋀ψ')} ⊆ L
α_in_L : ~(φ⋀ψ) ∈ L
h✝ : ¬ψ = ψ'
⊢ ~(φ⋀ψ) ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1 ∨
    ~φ ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1 ∨ ~ψ ∈ (insert (~ψ') (L.erase (~(φ'⋀ψ'))), R).1
Tactic:
aesop
State after:
no goals

State before:
case con
α : Formula
L R : Finset Formula
α_in_L : α ∈ L
c : TNode
φ ψ : Formula
precond_eq : ~(φ⋀ψ) = α
φ✝ ψ✝ : Formula
L_cond_in : {φ✝⋀ψ✝} ⊆ L
c_in : ∃ a ∈ [{φ✝, ψ✝}], (L \ {φ✝⋀ψ✝} ∪ a, R) = c
⊢ α ∈ c.1 ∨ ~φ ∈ c.1 ∨ ~ψ ∈ c.1
Tactic:
aesop
State after:
no goals

State before:
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
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)
⊢ α ∈ c.1 ∨ ∃ res ∈ ress, res ⊆ c.1
Tactic:
apply Or.inl
State after:
case h
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
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)
⊢ α ∈ c.1

State before:
case h
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
orule : OneSidedLocalRule precond ress
precond_eq : precond = {α}
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)
⊢ α ∈ c.1
Tactic:
aesop
State after:
no goals

State before:
case mk.intro.LRnegR
α : Formula
L R precond : Finset Formula
ress : List (Finset Formula)
α_in_L : α ∈ L
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.1 ∨ ∃ res ∈ ress, res ⊆ c.1
Tactic:
simp_all
State after:
no goals