Theorem: localRuleApp.decreases_DM
Proof state before:
case h.refine_2.refine_1.h.none.none.none
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
rule : LocalRule (Lcond, Rcond, none) ress
Z : Multiset Formula := node_to_multiset (L, R, none) - node_to_multiset (Lcond, Rcond, none)
preconP : Lcond.Sublist L ∧ Rcond.Sublist R
Z_eq : Z = node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, none) - node_to_multiset (Lnew, Rnew, none)
⊢ node_to_multiset (Lnew, Rnew, none) ≤ node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, none)

case h.refine_2.refine_1.h.none.some.inl.none.neg
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
rule : LocalRule (Lcond, Rcond, none) ress
a✝ : LoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inl (~'a✝))) - node_to_multiset (Lcond, Rcond, none)
preconP : Lcond.Sublist L ∧ Rcond.Sublist R
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'a✝))) -
      node_to_multiset (Lnew, Rnew, none)
⊢ node_to_multiset (Lnew, Rnew, none) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'a✝)))

case h.refine_2.refine_1.h.none.some.inl.some.inl
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
val✝¹ val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inl val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inl val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inl val✝))
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ val✝ = val✝¹
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl val✝¹)) -
      node_to_multiset (Lnew, Rnew, none)
⊢ node_to_multiset (Lnew, Rnew, none) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl val✝¹))

case h.refine_2.refine_1.h.none.some.inr.none.neg
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
rule : LocalRule (Lcond, Rcond, none) ress
a✝ : LoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inr (~'a✝))) - node_to_multiset (Lcond, Rcond, none)
preconP : Lcond.Sublist L ∧ Rcond.Sublist R
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'a✝))) -
      node_to_multiset (Lnew, Rnew, none)
⊢ node_to_multiset (Lnew, Rnew, none) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'a✝)))

case h.refine_2.refine_1.h.none.some.inr.some.inr
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
val✝¹ val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inr val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inr val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inr val✝))
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ val✝ = val✝¹
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr val✝¹)) -
      node_to_multiset (Lnew, Rnew, none)
⊢ node_to_multiset (Lnew, Rnew, none) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr val✝¹))

case h.refine_2.refine_1.h.some.inl.none.neg.none.load
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
rule : LocalRule (Lcond, Rcond, none) ress
Z : Multiset Formula := node_to_multiset (L, R, none) - node_to_multiset (Lcond, Rcond, none)
a✝¹ : Program
a✝ : Formula
preconP : Lcond.Sublist L ∧ Rcond.Sublist R
Y_in_ress : (Lnew, Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝))) ∈ ress
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝)))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝))) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝)))

case h.refine_2.refine_1.h.some.inl.none.neg.none.box
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
rule : LocalRule (Lcond, Rcond, none) ress
Z : Multiset Formula := node_to_multiset (L, R, none) - node_to_multiset (Lcond, Rcond, none)
a✝¹ : Program
a✝ : LoadFormula
preconP : Lcond.Sublist L ∧ Rcond.Sublist R
Y_in_ress : (Lnew, Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝))) ∈ ress
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝)))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝))) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝)))

case h.refine_2.refine_1.h.some.inl.some.inl.none.neg
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
val✝ : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inl val✝)) ∈ ress
rule : LocalRule (Lcond, Rcond, none) ress
a✝ : LoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inl (~'a✝))) - node_to_multiset (Lcond, Rcond, none)
preconP : Lcond.Sublist L ∧ Rcond.Sublist R
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'val✝.1))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inl val✝))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inl val✝)) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'val✝.1)))

case h.refine_2.refine_1.h.some.inl.some.inl.some.inl
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
val✝² : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inl val✝²)) ∈ ress
val✝¹ val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inl val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inl val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inl val✝))
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ val✝ = val✝¹
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'val✝².1))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inl val✝²))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inl val✝²)) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'val✝².1)))

case h.refine_2.refine_1.h.some.inl.some.inr.none.neg
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
val✝ : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inl val✝)) ∈ ress
rule : LocalRule (Lcond, Rcond, none) ress
a✝ : LoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inr (~'a✝))) - node_to_multiset (Lcond, Rcond, none)
preconP : Lcond.Sublist L ∧ Rcond.Sublist R
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'val✝.1))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inl val✝))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inl val✝)) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'val✝.1)))

case h.refine_2.refine_1.h.some.inl.some.inr.some.inr
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
val✝² : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inl val✝²)) ∈ ress
val✝¹ val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inr val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inr val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inr val✝))
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ val✝ = val✝¹
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'val✝².1))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inl val✝²))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inl val✝²)) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'val✝².1)))

case h.refine_2.refine_1.h.some.inr.none.neg.none.load
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
rule : LocalRule (Lcond, Rcond, none) ress
Z : Multiset Formula := node_to_multiset (L, R, none) - node_to_multiset (Lcond, Rcond, none)
a✝¹ : Program
a✝ : Formula
preconP : Lcond.Sublist L ∧ Rcond.Sublist R
Y_in_ress : (Lnew, Rnew, some (Sum.inr (~'⌊a✝¹⌋a✝))) ∈ ress
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'⌊a✝¹⌋a✝))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inr (~'⌊a✝¹⌋a✝)))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inr (~'⌊a✝¹⌋a✝))) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'⌊a✝¹⌋a✝)))

case h.refine_2.refine_1.h.some.inr.none.neg.none.box
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
rule : LocalRule (Lcond, Rcond, none) ress
Z : Multiset Formula := node_to_multiset (L, R, none) - node_to_multiset (Lcond, Rcond, none)
a✝¹ : Program
a✝ : LoadFormula
preconP : Lcond.Sublist L ∧ Rcond.Sublist R
Y_in_ress : (Lnew, Rnew, some (Sum.inr (~'⌊a✝¹⌋a✝))) ∈ ress
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'⌊a✝¹⌋a✝))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inr (~'⌊a✝¹⌋a✝)))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inr (~'⌊a✝¹⌋a✝))) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'⌊a✝¹⌋a✝)))

case h.refine_2.refine_1.h.some.inr.some.inl.none.neg
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
val✝ : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inr val✝)) ∈ ress
rule : LocalRule (Lcond, Rcond, none) ress
a✝ : LoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inl (~'a✝))) - node_to_multiset (Lcond, Rcond, none)
preconP : Lcond.Sublist L ∧ Rcond.Sublist R
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'val✝.1))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inr val✝))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inr val✝)) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'val✝.1)))

case h.refine_2.refine_1.h.some.inr.some.inl.some.inl
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
val✝² : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inr val✝²)) ∈ ress
val✝¹ val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inl val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inl val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inl val✝))
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ val✝ = val✝¹
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'val✝².1))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inr val✝²))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inr val✝²)) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'val✝².1)))

case h.refine_2.refine_1.h.some.inr.some.inr.none.neg
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
val✝ : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inr val✝)) ∈ ress
rule : LocalRule (Lcond, Rcond, none) ress
a✝ : LoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inr (~'a✝))) - node_to_multiset (Lcond, Rcond, none)
preconP : Lcond.Sublist L ∧ Rcond.Sublist R
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'val✝.1))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inr val✝))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inr val✝)) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'val✝.1)))

case h.refine_2.refine_1.h.some.inr.some.inr.some.inr
L R : List Formula
ress : List TNode
Lcond Rcond Lnew Rnew : List Formula
val✝² : NegLoadFormula
Y_in_ress : (Lnew, Rnew, some (Sum.inr val✝²)) ∈ ress
val✝¹ val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inr val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inr val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inr val✝))
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ val✝ = val✝¹
Z_eq :
  Z =
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'val✝².1))) -
      node_to_multiset (Lnew, Rnew, some (Sum.inr val✝²))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inr val✝²)) ≤
    node_to_multiset (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'val✝².1)))
Tactic:
all_goals
  simp [node_to_multiset]
  try apply List.Sublist.subperm
  try simp_all
  sorry
Proof state after:
no goals