internlm/Lean-Github huggingface dataset:
Theorem: localRuleApp.decreases_DM
Proof state before:
case mk
B : List TNode
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✝
hC✝ : B = applyLocalRule rule (L✝, R✝, O✝)
⊢ ∀ Y ∈ B, lt_TNode Y (L✝, R✝, O✝)
Tactic:
rename_i L R ress O B_def
Proof state after:
case mk
B : List TNode
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
B_def : B = applyLocalRule rule (L, R, O)
⊢ ∀ Y ∈ B, lt_TNode Y (L, R, O)
Theorem: localRuleApp.decreases_DM
Proof state before:
case mk
B : List TNode
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
B_def : B = applyLocalRule rule (L, R, O)
⊢ ∀ Y ∈ B, lt_TNode Y (L, R, O)
Tactic:
subst B_def
Proof state after:
case mk
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
⊢ ∀ Y ∈ applyLocalRule rule (L, R, O), lt_TNode Y (L, R, O)
Theorem: localRuleApp.decreases_DM
Proof state before:
case mk
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
⊢ ∀ Y ∈ applyLocalRule rule (L, R, O), lt_TNode Y (L, R, O)
Tactic:
intro RES RES_in
Proof state after:
case mk
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
RES_in : RES ∈ applyLocalRule rule (L, R, O)
⊢ lt_TNode RES (L, R, O)
Theorem: localRuleApp.decreases_DM
Proof state before:
case mk
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
RES_in : RES ∈ applyLocalRule rule (L, R, O)
⊢ lt_TNode RES (L, R, O)
Tactic:
simp [applyLocalRule] at RES_in
Proof state after:
case mk
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
RES_in :
  ∃ a ∈ ress,
    (match a with
      | (Lnew, Rnew, Onew) =>
        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
⊢ lt_TNode RES (L, R, O)
Theorem: localRuleApp.decreases_DM
Proof state before:
case mk
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
RES_in :
  ∃ a ∈ ress,
    (match a with
      | (Lnew, Rnew, Onew) =>
        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
⊢ lt_TNode RES (L, R, O)
Tactic:
rcases RES_in with ⟨⟨Lnew,Rnew,Onew⟩, Y_in_ress, claim⟩
Proof state after:
case mk.intro.mk.mk.intro
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 (Lnew, Rnew, Onew) with
    | (Lnew, Rnew, Onew) =>
      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
⊢ lt_TNode RES (L, R, O)
Theorem: localRuleApp.decreases_DM
Proof state before:
case mk.intro.mk.mk.intro
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 (Lnew, Rnew, Onew) with
    | (Lnew, Rnew, Onew) =>
      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
⊢ lt_TNode RES (L, R, O)
Tactic:
unfold lt_TNode
Proof state after:
case mk.intro.mk.mk.intro
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 (Lnew, Rnew, Onew) with
    | (Lnew, Rnew, Onew) =>
      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
⊢ MultisetLT (node_to_multiset RES) (node_to_multiset (L, R, O))
Theorem: localRuleApp.decreases_DM
Proof state before:
case mk.intro.mk.mk.intro
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 (Lnew, Rnew, Onew) with
    | (Lnew, Rnew, Onew) =>
      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
⊢ MultisetLT (node_to_multiset RES) (node_to_multiset (L, R, O))
Tactic:
simp at claim
Proof state after:
case mk.intro.mk.mk.intro
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
⊢ MultisetLT (node_to_multiset RES) (node_to_multiset (L, R, O))
Theorem: localRuleApp.decreases_DM
Proof state before:
case mk.intro.mk.mk.intro
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
⊢ MultisetLT (node_to_multiset RES) (node_to_multiset (L, R, O))
Tactic:
rw [MultisetLT.iff_MultisetLT']
Proof state after:
case mk.intro.mk.mk.intro
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
⊢ MultisetLT' (node_to_multiset RES) (node_to_multiset (L, R, O))
Theorem: localRuleApp.decreases_DM
Proof state before:
case mk.intro.mk.mk.intro
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
⊢ MultisetLT' (node_to_multiset RES) (node_to_multiset (L, R, O))
Tactic:
unfold MultisetLT'
Proof state after:
case mk.intro.mk.mk.intro
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
⊢ ∃ X Y Z, Y ≠ ∅ ∧ node_to_multiset RES = Z + X ∧ node_to_multiset (L, R, O) = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Theorem: localRuleApp.decreases_DM
Proof state before:
case mk.intro.mk.mk.intro
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
⊢ ∃ X Y Z, Y ≠ ∅ ∧ node_to_multiset RES = Z + X ∧ node_to_multiset (L, R, O) = Z + Y ∧ ∀ x ∈ X, ∃ y ∈ Y, x < y
Tactic:
use node_to_multiset (Lnew, Rnew, Onew)
Proof state after:
case h
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
⊢ ∃ Y Z,
    Y ≠ ∅ ∧
      node_to_multiset RES = Z + node_to_multiset (Lnew, Rnew, Onew) ∧
        node_to_multiset (L, R, O) = Z + Y ∧ ∀ x ∈ node_to_multiset (Lnew, Rnew, Onew), ∃ y ∈ Y, x < y
Theorem: localRuleApp.decreases_DM
Proof state before:
case h
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
⊢ ∃ Y Z,
    Y ≠ ∅ ∧
      node_to_multiset RES = Z + node_to_multiset (Lnew, Rnew, Onew) ∧
        node_to_multiset (L, R, O) = Z + Y ∧ ∀ x ∈ node_to_multiset (Lnew, Rnew, Onew), ∃ y ∈ Y, x < y
Tactic:
use node_to_multiset (Lcond, Rcond, Ocond)
Proof state after:
case h
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
⊢ ∃ Z,
    node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅ ∧
      node_to_multiset RES = Z + node_to_multiset (Lnew, Rnew, Onew) ∧
        node_to_multiset (L, R, O) = Z + node_to_multiset (Lcond, Rcond, Ocond) ∧
          ∀ x ∈ node_to_multiset (Lnew, Rnew, Onew), ∃ y ∈ node_to_multiset (Lcond, Rcond, Ocond), x < y
Theorem: localRuleApp.decreases_DM
Proof state before:
case h
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
⊢ ∃ Z,
    node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅ ∧
      node_to_multiset RES = Z + node_to_multiset (Lnew, Rnew, Onew) ∧
        node_to_multiset (L, R, O) = Z + node_to_multiset (Lcond, Rcond, Ocond) ∧
          ∀ x ∈ node_to_multiset (Lnew, Rnew, Onew), ∃ y ∈ node_to_multiset (Lcond, Rcond, Ocond), x < y
Tactic:
let Z := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
Proof state after:
case h
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
⊢ ∃ Z,
    node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅ ∧
      node_to_multiset RES = Z + node_to_multiset (Lnew, Rnew, Onew) ∧
        node_to_multiset (L, R, O) = Z + node_to_multiset (Lcond, Rcond, Ocond) ∧
          ∀ x ∈ node_to_multiset (Lnew, Rnew, Onew), ∃ y ∈ node_to_multiset (Lcond, Rcond, Ocond), x < y
Theorem: localRuleApp.decreases_DM
Proof state before:
case h
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
⊢ ∃ Z,
    node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅ ∧
      node_to_multiset RES = Z + node_to_multiset (Lnew, Rnew, Onew) ∧
        node_to_multiset (L, R, O) = Z + node_to_multiset (Lcond, Rcond, Ocond) ∧
          ∀ x ∈ node_to_multiset (Lnew, Rnew, Onew), ∃ y ∈ node_to_multiset (Lcond, Rcond, Ocond), x < y
Tactic:
use Z
Proof state after:
case h
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
⊢ node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅ ∧
    node_to_multiset RES = Z + node_to_multiset (Lnew, Rnew, Onew) ∧
      node_to_multiset (L, R, O) = Z + node_to_multiset (Lcond, Rcond, Ocond) ∧
        ∀ x ∈ node_to_multiset (Lnew, Rnew, Onew), ∃ y ∈ node_to_multiset (Lcond, Rcond, Ocond), x < y
Theorem: localRuleApp.decreases_DM
Proof state before:
case h
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
⊢ node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅ ∧
    node_to_multiset RES = Z + node_to_multiset (Lnew, Rnew, Onew) ∧
      node_to_multiset (L, R, O) = Z + node_to_multiset (Lcond, Rcond, Ocond) ∧
        ∀ x ∈ node_to_multiset (Lnew, Rnew, Onew), ∃ y ∈ node_to_multiset (Lcond, Rcond, Ocond), x < y
Tactic:
have Z_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, Onew) := by
  sorry
Proof state after:
case h
L R : List Formula
ress : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress
preconP : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
RES : TNode
Lnew Rnew : List Formula
Onew : Option (NegLoadFormula ⊕ NegLoadFormula)
Y_in_ress : (Lnew, Rnew, Onew) ∈ ress
claim :
  (match Onew with
    | none => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, O)
    | some (Sum.inl (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L.diff Lcond ++ Lnew, R.diff Rcond ++ Rnew, some (Sum.inr (~'χ)))) =
    RES
Z : Multiset Formula := node_to_multiset (L, R, O) - node_to_multiset (Lcond, Rcond, Ocond)
Z_eq : Z = node_to_multiset RES - node_to_multiset (Lnew, Rnew, Onew)
⊢ node_to_multiset (Lcond, Rcond, Ocond) ≠ ∅ ∧
    node_to_multiset RES = Z + node_to_multiset (Lnew, Rnew, Onew) ∧
      node_to_multiset (L, R, O) = Z + node_to_multiset (Lcond, Rcond, Ocond) ∧
        ∀ x ∈ node_to_multiset (Lnew, Rnew, Onew), ∃ y ∈ node_to_multiset (Lcond, Rcond, Ocond), x < y
Theorem: localRuleApp.decreases_DM
Proof state before:
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 = node_to_multiset RES - node_to_multiset (Lnew, Rnew, Onew)
Tactic:
sorry
Proof state after:
no goals