Theorem: localRuleApp.decreases_DM (Pdl/LocalTableau.lean)

State before:
case h.refine_2.refine_1.h.some
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 ⊕ NegLoadFormula
Y_in_ress : (Lnew, Rnew, some val✝) ∈ ress
claim :
  (match some 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 val✝)
⊢ node_to_multiset (Lnew, Rnew, some val✝) ≤ node_to_multiset RES
Tactic:
try (rename_i f; cases f)
State after:
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

State before:
case h.refine_2.refine_1.h.some
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 ⊕ NegLoadFormula
Y_in_ress : (Lnew, Rnew, some val✝) ∈ ress
claim :
  (match some 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 val✝)
⊢ node_to_multiset (Lnew, Rnew, some val✝) ≤ node_to_multiset RES
Tactic:
(rename_i f; cases f)
State after:
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

State before:
case h.refine_2.refine_1.h.some
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 ⊕ NegLoadFormula
Y_in_ress : (Lnew, Rnew, some val✝) ∈ ress
claim :
  (match some 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 val✝)
⊢ node_to_multiset (Lnew, Rnew, some val✝) ≤ node_to_multiset RES
Tactic:
rename_i f
State after:
case h.refine_2.refine_1.h.some
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)
f : NegLoadFormula ⊕ NegLoadFormula
Y_in_ress : (Lnew, Rnew, some f) ∈ ress
claim :
  (match some f 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 f)
⊢ node_to_multiset (Lnew, Rnew, some f) ≤ node_to_multiset RES

State before:
case h.refine_2.refine_1.h.some
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)
f : NegLoadFormula ⊕ NegLoadFormula
Y_in_ress : (Lnew, Rnew, some f) ∈ ress
claim :
  (match some f 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 f)
⊢ node_to_multiset (Lnew, Rnew, some f) ≤ node_to_multiset RES
Tactic:
cases f
State after:
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

State before:
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:
simp_all
State after:
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

State before:
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
Tactic:
cases O
State after:
case h.refine_2.refine_1.h.some.inr.none
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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
Z : Multiset Formula := node_to_multiset (L, R, none) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, 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 val✝))
⊢ node_to_multiset (Lnew, Rnew, some (Sum.inr val✝)) ≤ node_to_multiset RES

case h.refine_2.refine_1.h.some.inr.some
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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 ⊕ NegLoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some val✝) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, some 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

State before:
case h.refine_2.refine_1.h.some.inr.some
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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 ⊕ NegLoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some val✝) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, some 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:
try (rename_i cond; cases cond)
State after:
case h.refine_2.refine_1.h.some.inr.some.inl
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inl val✝)) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, 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
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inr val✝)) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, 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

State before:
case h.refine_2.refine_1.h.some.inr.some
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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 ⊕ NegLoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some val✝) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, some 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:
(rename_i cond; cases cond)
State after:
case h.refine_2.refine_1.h.some.inr.some.inl
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inl val✝)) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, 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
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inr val✝)) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, 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

State before:
case h.refine_2.refine_1.h.some.inr.some
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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 ⊕ NegLoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some val✝) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, some 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:
rename_i cond
State after:
case h.refine_2.refine_1.h.some.inr.some
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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
cond : NegLoadFormula ⊕ NegLoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some cond) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, some cond 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

State before:
case h.refine_2.refine_1.h.some.inr.some
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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
cond : NegLoadFormula ⊕ NegLoadFormula
Z : Multiset Formula := node_to_multiset (L, R, some cond) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, some cond 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:
cases cond
State after:
case h.refine_2.refine_1.h.some.inr.some.inl
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inl val✝)) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, 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
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inr val✝)) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, 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

State before:
case h.refine_2.refine_1.h.some.inr.some.inr
L R : List Formula
ress : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
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
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inr val✝)) - node_to_multiset (Lcond, Rcond, Ocond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match Ocond, 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:
cases Ocond
State after:
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

State before:
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:
try (rename_i cond; cases cond)
State after:
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

State before:
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:
(rename_i cond; cases cond)
State after:
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

State before:
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:
rename_i cond
State after:
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
cond : NegLoadFormula ⊕ NegLoadFormula
rule : LocalRule (Lcond, Rcond, some cond) ress
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inr val✝)) - node_to_multiset (Lcond, Rcond, some cond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match some cond, 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

State before:
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
cond : NegLoadFormula ⊕ NegLoadFormula
rule : LocalRule (Lcond, Rcond, some cond) ress
Z : Multiset Formula := node_to_multiset (L, R, some (Sum.inr val✝)) - node_to_multiset (Lcond, Rcond, some cond)
preconP :
  Lcond.Sublist L ∧
    Rcond.Sublist R ∧
      match some cond, 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:
cases cond
State after:
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

State before:
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
Tactic:
try simp_all
State after:
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 ∧ val✝ = val✝¹
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

State before:
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
Tactic:
simp_all
State after:
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 ∧ val✝ = val✝¹
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

State before:
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 ∧ val✝ = val✝¹
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:
subst claim
State after:
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)))

State before:
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:
simp [node_to_multiset]
State after:
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✝²))
⊢ (Lnew ++ Rnew).Subperm (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ Rnew)))

State before:
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✝²))
⊢ (Lnew ++ Rnew).Subperm (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ Rnew)))
Tactic:
try apply List.Sublist.subperm
State after:
case h.refine_2.refine_1.h.some.inr.some.inr.some.inr.s
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✝²))
⊢ (Lnew ++ Rnew).Sublist (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ Rnew)))

State before:
case h.refine_2.refine_1.h.none.some.inr.some.inr.s
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)
⊢ (Lnew ++ Rnew).Sublist (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ Rnew)) ++ [~unload val✝¹.1])
Tactic:
try simp_all
State after:
case h.refine_2.refine_1.h.none.some.inr.some.inr.s
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)
⊢ (Lnew ++ Rnew).Sublist (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ (Rnew ++ [~unload val✝¹.1]))))

State before:
case h.refine_2.refine_1.h.some.inr.some.inr.some.inr.s
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✝²))
⊢ (Lnew ++ Rnew).Sublist (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ Rnew)))
Tactic:
sorry
State after:
no goals

State before:
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✝²))
⊢ (Lnew ++ Rnew).Subperm (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ Rnew)))
Tactic:
apply List.Sublist.subperm
State after:
case h.refine_2.refine_1.h.some.inr.some.inr.some.inr.s
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✝²))
⊢ (Lnew ++ Rnew).Sublist (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ Rnew)))

State before:
case h.refine_2.refine_1.h.none.some.inr.some.inr.s
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)
⊢ (Lnew ++ Rnew).Sublist (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ Rnew)) ++ [~unload val✝¹.1])
Tactic:
simp_all
State after:
case h.refine_2.refine_1.h.none.some.inr.some.inr.s
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)
⊢ (Lnew ++ Rnew).Sublist (L.diff Lcond ++ (Lnew ++ (R.diff Rcond ++ (Rnew ++ [~unload val✝¹.1]))))

State before:
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)
Tactic:
apply Multiset.sub_add_of_subset_eq
State after:
case h.refine_2.refine_2.refine_1.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 (L, R, O)

State before:
case h.refine_2.refine_2.refine_1.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 (L, R, O)
Tactic:
exact preconP_to_submultiset preconP
State after:
no goals

State before:
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
Tactic:
exact LocalRule.Decreases rule _ Y_in_ress
State after:
no goals