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

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

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

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

case h.refine_2.refine_1.h.some.inr.some.inl.none
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
val✝¹ : NegLoadFormula
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
val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, none) ress
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inl val✝)) - node_to_multiset (Lcond, Rcond, none)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match none, some (Sum.inl val✝) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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

case h.refine_2.refine_1.h.some.inr.some.inl.some
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
val✝² : NegLoadFormula
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
val✝¹ : NegLoadFormula
val✝ : NegLoadFormula ⊕ NegLoadFormula
rule : LocalRule (Lcond, Rcond, some val✝) ress
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inl val✝¹)) - node_to_multiset (Lcond, Rcond, some val✝)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match some val✝, some (Sum.inl val✝¹) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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

case h.refine_2.refine_1.h.some.inr.some.inr.none
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
val✝¹ : NegLoadFormula
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
val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, none) ress
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inr val✝)) - node_to_multiset (Lcond, Rcond, none)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match none, some (Sum.inr val✝) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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

case h.refine_2.refine_1.h.some.inr.some.inr.some
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
val✝² : NegLoadFormula
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
val✝¹ : NegLoadFormula
val✝ : NegLoadFormula ⊕ NegLoadFormula
rule : LocalRule (Lcond, Rcond, some val✝) ress
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inr val✝¹)) - node_to_multiset (Lcond, Rcond, some val✝)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match some val✝, some (Sum.inr val✝¹) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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 try (rename_i cond; cases cond)
Proof state after:
case h.refine_2.refine_1.h.none.none.none
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, none) = RES
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 ∧
      match none, none with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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.none.none.some.inl
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, none) = RES
val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inl val✝)) ress
Z : Multiset Formula := node_to_multiset (L, R, none) - node_to_multiset (Lcond, Rcond, some (Sum.inl val✝))
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match some (Sum.inl val✝), none with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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.none.none.some.inr
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, none) = RES
val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inr val✝)) ress
Z : Multiset Formula := node_to_multiset (L, R, none) - node_to_multiset (Lcond, Rcond, some (Sum.inr val✝))
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match some (Sum.inr val✝), none with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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.none.some.inl.none.neg
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
rule : LocalRule (Lcond, Rcond, none) ress
a✝ : LoadFormula
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'a✝))) = RES
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 ∧
      match none, some (Sum.inl (~'a✝)) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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.none.some.inl.some.inl
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
val✝¹ : NegLoadFormula
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl val✝¹)) = RES
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 ∧
      match some (Sum.inl val✝), some (Sum.inl val✝¹) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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.none.some.inl.some.inr
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
val✝¹ : NegLoadFormula
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl val✝¹)) = RES
val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inr val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inl val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inr val✝))
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match some (Sum.inr val✝), some (Sum.inl val✝¹) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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.none.some.inr.none.neg
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
rule : LocalRule (Lcond, Rcond, none) ress
a✝ : LoadFormula
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'a✝))) = RES
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 ∧
      match none, some (Sum.inr (~'a✝)) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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.none.some.inr.some.inl
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
val✝¹ : NegLoadFormula
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr val✝¹)) = RES
val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inl val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inr val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inl val✝))
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match some (Sum.inl val✝), some (Sum.inr val✝¹) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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.none.some.inr.some.inr
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
Y_in_ress : (Lnew, Rnew, none) ∈ ress
val✝¹ : NegLoadFormula
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr val✝¹)) = RES
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 ∧
      match some (Sum.inr val✝), some (Sum.inr val✝¹) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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.none.neg.none.load
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
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)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match none, none with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
a✝¹ : Program
a✝ : Formula
Y_in_ress : (Lnew, Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝))) ∈ ress
claim : (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'(~'⌊a✝¹⌋a✝).1))) = RES
Z_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝)))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inl (~'⌊a✝¹⌋a✝))) ≤ node_to_multiset RES

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

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

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

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

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

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

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

case h.refine_2.refine_1.h.some.inr.some.inl.none.neg
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
val✝ : NegLoadFormula
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
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 ∧
      match none, some (Sum.inl (~'a✝)) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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

case h.refine_2.refine_1.h.some.inr.some.inl.some.inl
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
val✝² : NegLoadFormula
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
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 ∧
      match some (Sum.inl val✝), some (Sum.inl val✝¹) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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

case h.refine_2.refine_1.h.some.inr.some.inl.some.inr
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
val✝² : NegLoadFormula
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
val✝¹ val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inr val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inl val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inr val✝))
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match some (Sum.inr val✝), some (Sum.inl val✝¹) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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

case h.refine_2.refine_1.h.some.inr.some.inr.none.neg
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
val✝ : NegLoadFormula
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
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 ∧
      match none, some (Sum.inr (~'a✝)) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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

case h.refine_2.refine_1.h.some.inr.some.inr.some.inl
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
val✝² : NegLoadFormula
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
val✝¹ val✝ : NegLoadFormula
rule : LocalRule (Lcond, Rcond, some (Sum.inl val✝)) ress
Z : Multiset Formula :=
  node_to_multiset (L, R, some (Sum.inr val✝¹)) - node_to_multiset (Lcond, Rcond, some (Sum.inl val✝))
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match some (Sum.inl val✝), some (Sum.inr val✝¹) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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

case h.refine_2.refine_1.h.some.inr.some.inr.some.inr
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
RES : TNode
Lnew Rnew : List Formula
val✝² : NegLoadFormula
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
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 ∧
      match some (Sum.inr val✝), some (Sum.inr val✝¹) with
      | none, x => True
      | some val, none => False
      | some f, some g => f = g
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