Theorem: localRuleApp.decreases_DM
Proof state before:
case h
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
Z_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, Onew)
⊢ node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅ ∧
    node_to_multiset RES = Z + node_to_multiset (Lnew, Rnew, Onew) ∧
      node_to_multiset (L, R, O) = Z + node_to_multiset (Lcond, Rcond, Ocond) ∧
        ∀ x ∈ node_to_multiset (Lnew, Rnew, Onew), ∃ y ∈ node_to_multiset (Lcond, Rcond, Ocond), x < y
Tactic:
split_ands
Proof state after:
case h.refine_1
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
Z_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, Onew)
⊢ node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅

case h.refine_2.refine_1
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
Z_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, Onew)
⊢ node_to_multiset RES = Z + node_to_multiset (Lnew, Rnew, Onew)

case h.refine_2.refine_2.refine_1
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
Z_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, Onew)
⊢ node_to_multiset (L, R, O) = Z + node_to_multiset (Lcond, Rcond, Ocond)

case h.refine_2.refine_2.refine_2
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
Z_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, Onew)
⊢ ∀ x ∈ node_to_multiset (Lnew, Rnew, Onew), ∃ y ∈ node_to_multiset (Lcond, Rcond, Ocond), x < y