Theorem: localRuleNoOverlap (Bml/Tableau.lean)

State before:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
⊢ ∀ res ∈ ress, Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
Tactic:
intro res in_ress
State after:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
in_ress : res ∈ ress
⊢ Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅

State before:
Lcond Rcond : Finset Formula
ress : List SubPair
rule : LocalRule (Lcond, Rcond) ress
res : SubPair
in_ress : res ∈ ress
⊢ Lcond ∩ res.1 = ∅ ∧ Rcond ∩ res.2 = ∅
Tactic:
cases rule <;>
( rename_i rule
  cases rule
  all_goals aesop)
State after:
no goals

State before:
case LRnegR
res : SubPair
ϕ✝ : Formula
in_ress : res ∈ ∅
⊢ {~ϕ✝} ∩ res.1 = ∅ ∧ {ϕ✝} ∩ res.2 = ∅
Tactic:
rename_i rule
State after:
case LRnegR
res : SubPair
rule : Formula
in_ress : res ∈ ∅
⊢ {~rule} ∩ res.1 = ∅ ∧ {rule} ∩ res.2 = ∅

State before:
case LRnegR
res : SubPair
rule : Formula
in_ress : res ∈ ∅
⊢ {~rule} ∩ res.1 = ∅ ∧ {rule} ∩ res.2 = ∅
Tactic:
cases rule
State after:
case LRnegR.bottom
res : SubPair
in_ress : res ∈ ∅
⊢ {~bottom} ∩ res.1 = ∅ ∧ {bottom} ∩ res.2 = ∅

case LRnegR.atom_prop
res : SubPair
in_ress : res ∈ ∅
a✝ : Char
⊢ {~·a✝} ∩ res.1 = ∅ ∧ {·a✝} ∩ res.2 = ∅

case LRnegR.neg
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~~a✝} ∩ res.1 = ∅ ∧ {~a✝} ∩ res.2 = ∅

case LRnegR.And
res : SubPair
in_ress : res ∈ ∅
a✝¹ a✝ : Formula
⊢ {~(a✝¹⋀a✝)} ∩ res.1 = ∅ ∧ {a✝¹⋀a✝} ∩ res.2 = ∅

case LRnegR.box
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~(□a✝)} ∩ res.1 = ∅ ∧ {□a✝} ∩ res.2 = ∅

State before:
case LRnegR.bottom
res : SubPair
in_ress : res ∈ ∅
⊢ {~bottom} ∩ res.1 = ∅ ∧ {bottom} ∩ res.2 = ∅

case LRnegR.atom_prop
res : SubPair
in_ress : res ∈ ∅
a✝ : Char
⊢ {~·a✝} ∩ res.1 = ∅ ∧ {·a✝} ∩ res.2 = ∅

case LRnegR.neg
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~~a✝} ∩ res.1 = ∅ ∧ {~a✝} ∩ res.2 = ∅

case LRnegR.And
res : SubPair
in_ress : res ∈ ∅
a✝¹ a✝ : Formula
⊢ {~(a✝¹⋀a✝)} ∩ res.1 = ∅ ∧ {a✝¹⋀a✝} ∩ res.2 = ∅

case LRnegR.box
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~(□a✝)} ∩ res.1 = ∅ ∧ {□a✝} ∩ res.2 = ∅
Tactic:
all_goals aesop
State after:
no goals

State before:
case LRnegR.box
res : SubPair
in_ress : res ∈ ∅
a✝ : Formula
⊢ {~(□a✝)} ∩ res.1 = ∅ ∧ {□a✝} ∩ res.2 = ∅
Tactic:
aesop
State after:
no goals