Theorem: LocalRule.cond_non_empty (Pdl/LocalTableau.lean)

State before:
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
X : List TNode
rule : LocalRule (Lcond, Rcond, Ocond) X
⊢ node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅
Tactic:
cases rule
State after:
case oneSidedL
Lcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
⊢ node_to_multiset (Lcond, ∅, none) ≠ ∅

case oneSidedR
Rcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
⊢ node_to_multiset (∅, Rcond, none) ≠ ∅

case LRnegL
ϕ✝ : Formula
⊢ node_to_multiset ([ϕ✝], [~ϕ✝], none) ≠ ∅

case LRnegR
ϕ✝ : Formula
⊢ node_to_multiset ([~ϕ✝], [ϕ✝], none) ≠ ∅

case loadedL
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))) ≠ ∅

case loadedR
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))) ≠ ∅

State before:
case oneSidedL
Lcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
⊢ node_to_multiset (Lcond, ∅, none) ≠ ∅

case oneSidedR
Rcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
⊢ node_to_multiset (∅, Rcond, none) ≠ ∅

case LRnegL
ϕ✝ : Formula
⊢ node_to_multiset ([ϕ✝], [~ϕ✝], none) ≠ ∅

case LRnegR
ϕ✝ : Formula
⊢ node_to_multiset ([~ϕ✝], [ϕ✝], none) ≠ ∅

case loadedL
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inl (~'χ✝))) ≠ ∅

case loadedR
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))) ≠ ∅
Tactic:
all_goals simp [node_to_multiset]
State after:
case oneSidedL
Lcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
⊢ ¬Lcond = []

case oneSidedR
Rcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
⊢ ¬Rcond = []

State before:
Lcond : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule Lcond ress✝
⊢ ¬Lcond = []
Tactic:
case oneSidedL _ orule => cases orule <;> simp
State after:
no goals

State before:
Rcond : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule Rcond ress✝
⊢ ¬Rcond = []
Tactic:
case oneSidedR _ orule => cases orule <;> simp
State after:
no goals

State before:
case loadedR
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
⊢ node_to_multiset (∅, ∅, some (Sum.inr (~'χ✝))) ≠ ∅
Tactic:
simp [node_to_multiset]
State after:
no goals

State before:
Lcond : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule Lcond ress✝
⊢ ¬Lcond = []
Tactic:
cases orule <;> simp
State after:
no goals

State before:
Rcond : List Formula
ress✝ : List (List Formula)
orule : OneSidedLocalRule Rcond ress✝
⊢ ¬Rcond = []
Tactic:
cases orule <;> simp
State after:
no goals