Theorem: localRuleApp.decreases_DM
Proof state before:
case h.refine_2.refine_1.h.none
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
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
Y_in_ress : (Lnew, Rnew, none) ∈ ress
claim :
  (match none 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_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, none)
⊢ node_to_multiset (Lnew, Rnew, none) ≤ node_to_multiset RES

case h.refine_2.refine_1.h.some.inl
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
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
val✝ : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inl val✝)) ∈ ress
claim :
  (match some (Sum.inl val✝) 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_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, some (Sum.inl val✝))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inl val✝)) ≤ node_to_multiset RES

case h.refine_2.refine_1.h.some.inr
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
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
val✝ : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inr val✝)) ∈ ress
claim :
  (match some (Sum.inr val✝) 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_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, some (Sum.inr val✝))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inr val✝)) ≤ node_to_multiset RES
Tactic:
all_goals simp_all
Proof state after:
case h.refine_2.refine_1.h.none
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
RES : TNode
Lnew Rnew : List Formula
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, O with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
Y_in_ress : (Lnew, Rnew, none) ∈ ress
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O) = RES
Z_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, none)
⊢ node_to_multiset (Lnew, Rnew, none) ≤ node_to_multiset RES

case h.refine_2.refine_1.h.some.inl
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
RES : TNode
Lnew Rnew : List Formula
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
val✝ : NegLoadFormula
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, O with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
Y_in_ress : (Lnew, Rnew, some (Sum.inl val✝)) ∈ ress
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'val✝.1))) = RES
Z_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, some (Sum.inl val✝))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inl val✝)) ≤ node_to_multiset RES

case h.refine_2.refine_1.h.some.inr
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
RES : TNode
Lnew Rnew : List Formula
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
val✝ : NegLoadFormula
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, O with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
Y_in_ress : (Lnew, Rnew, some (Sum.inr val✝)) ∈ ress
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'val✝.1))) = RES
Z_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, some (Sum.inr val✝))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inr val✝)) ≤ node_to_multiset RES