internlm/Lean-Github huggingface dataset:
Theorem: localRuleApp.decreases_DM
Proof 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
Proof 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
Theorem: localRuleApp.decreases_DM
Proof 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
Proof 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
Theorem: localRuleApp.decreases_DM
Proof 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
Proof 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)))
Theorem: localRuleApp.decreases_DM
Proof 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]
Proof 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)))
Theorem: localRuleApp.decreases_DM
Proof 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
Proof 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)))
Theorem: localRuleApp.decreases_DM
Proof 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
Proof 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]))))
Theorem: localRuleApp.decreases_DM
Proof 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
Proof state after:
no goals
Theorem: localRuleApp.decreases_DM
Proof 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
Proof 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)))
Theorem: localRuleApp.decreases_DM
Proof 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
Proof 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]))))
Theorem: localRuleApp.decreases_DM
Proof 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
Proof 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)
Theorem: localRuleApp.decreases_DM
Proof 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
Proof state after:
no goals
Theorem: localRuleApp.decreases_DM
Proof 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
Proof state after:
no goals
Theorem: proj
Proof state before:
g : Formula
A : ℕ
X : List Formula
⊢ g ∈ projection A X ↔ (⌈·A⌉g) ∈ X
Tactic:
induction X
Proof state after:
case nil
g : Formula
A : ℕ
⊢ g ∈ projection A [] ↔ (⌈·A⌉g) ∈ []

case cons
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈ projection A (head✝ :: tail✝) ↔ (⌈·A⌉g) ∈ head✝ :: tail✝
Theorem: proj
Proof state before:
g : Formula
A : ℕ
⊢ g ∈ projection A [] ↔ (⌈·A⌉g) ∈ []
Tactic:
case nil =>
  simp only [projection, formProjection, beq_iff_eq, List.map_nil, List.not_mem_nil, iff_false]
  exact List.count_eq_zero.mp rfl
Proof state after:
no goals
Theorem: proj
Proof state before:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈ projection A (head✝ :: tail✝) ↔ (⌈·A⌉g) ∈ head✝ :: tail✝
Tactic:
case cons =>
  simp only [projection, formProjection, beq_iff_eq, List.map_cons, List.mem_cons]
  rw [List.reduceOption_mem_iff]
  aesop
Proof state after:
no goals
Theorem: proj
Proof state before:
g : Formula
A : ℕ
⊢ g ∈ projection A [] ↔ (⌈·A⌉g) ∈ []
Tactic:
simp only [projection, formProjection, beq_iff_eq, List.map_nil, List.not_mem_nil, iff_false]
Proof state after:
g : Formula
A : ℕ
⊢ g ∉ [].reduceOption
Theorem: proj
Proof state before:
g : Formula
A : ℕ
⊢ g ∉ [].reduceOption
Tactic:
exact List.count_eq_zero.mp rfl
Proof state after:
no goals
Theorem: proj
Proof state before:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈ projection A (head✝ :: tail✝) ↔ (⌈·A⌉g) ∈ head✝ :: tail✝
Tactic:
simp only [projection, formProjection, beq_iff_eq, List.map_cons, List.mem_cons]
Proof state after:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈
      ((match A, head✝ with
          | A, ⌈·B⌉φ => if A = B then some φ else none
          | x, x_1 => none) ::
          List.map
            (fun x =>
              match A, x with
              | A, ⌈·B⌉φ => if A = B then some φ else none
              | x, x_1 => none)
            tail✝).reduceOption ↔
    (⌈·A⌉g) = head✝ ∨ (⌈·A⌉g) ∈ tail✝
Theorem: proj
Proof state before:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ g ∈
      ((match A, head✝ with
          | A, ⌈·B⌉φ => if A = B then some φ else none
          | x, x_1 => none) ::
          List.map
            (fun x =>
              match A, x with
              | A, ⌈·B⌉φ => if A = B then some φ else none
              | x, x_1 => none)
            tail✝).reduceOption ↔
    (⌈·A⌉g) = head✝ ∨ (⌈·A⌉g) ∈ tail✝
Tactic:
rw [List.reduceOption_mem_iff]
Proof state after:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ some g ∈
      (match A, head✝ with
        | A, ⌈·B⌉φ => if A = B then some φ else none
        | x, x_1 => none) ::
        List.map
          (fun x =>
            match A, x with
            | A, ⌈·B⌉φ => if A = B then some φ else none
            | x, x_1 => none)
          tail✝ ↔
    (⌈·A⌉g) = head✝ ∨ (⌈·A⌉g) ∈ tail✝
Theorem: proj
Proof state before:
g : Formula
A : ℕ
head✝ : Formula
tail✝ : List Formula
tail_ih✝ : g ∈ projection A tail✝ ↔ (⌈·A⌉g) ∈ tail✝
⊢ some g ∈
      (match A, head✝ with
        | A, ⌈·B⌉φ => if A = B then some φ else none
        | x, x_1 => none) ::
        List.map
          (fun x =>
            match A, x with
            | A, ⌈·B⌉φ => if A = B then some φ else none
            | x, x_1 => none)
          tail✝ ↔
    (⌈·A⌉g) = head✝ ∨ (⌈·A⌉g) ∈ tail✝
Tactic:
aesop
Proof state after:
no goals
Theorem: vocOfNeg
Proof state before:
ϕ : Formula
⊢ vocabOfFormula (~ϕ) = vocabOfFormula ϕ
Tactic:
constructor
Proof state after:
no goals
Theorem: vocElem_subs_vocSet
Proof state before:
ϕ : Formula
X : Finset Formula
⊢ ϕ ∈ X → vocabOfFormula ϕ ⊆ vocabOfSetFormula X
Tactic:
induction X using Finset.induction_on
Proof state after:
case empty
ϕ : Formula
⊢ ϕ ∈ ∅ → vocabOfFormula ϕ ⊆ vocabOfSetFormula ∅

case insert
ϕ a✝² : Formula
s✝ : Finset Formula
a✝¹ : a✝² ∉ s✝
a✝ : ϕ ∈ s✝ → vocabOfFormula ϕ ⊆ vocabOfSetFormula s✝
⊢ ϕ ∈ insert a✝² s✝ → vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert a✝² s✝)
Theorem: vocElem_subs_vocSet
Proof state before:
ϕ : Formula
⊢ ϕ ∈ ∅ → vocabOfFormula ϕ ⊆ vocabOfSetFormula ∅
Tactic:
case empty =>
  intro phi_in_X;
  cases phi_in_X
Proof state after:
no goals
Theorem: vocElem_subs_vocSet
Proof state before:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula S
⊢ ϕ ∈ insert ψ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert ψ S)
Tactic:
case insert ψ S _ _ =>
  intro psi_in_insert
  simp at *
  intro a aIn
  aesop
Proof state after:
no goals
Theorem: vocElem_subs_vocSet
Proof state before:
ϕ : Formula
⊢ ϕ ∈ ∅ → vocabOfFormula ϕ ⊆ vocabOfSetFormula ∅
Tactic:
intro phi_in_X
Proof state after:
ϕ : Formula
phi_in_X : ϕ ∈ ∅
⊢ vocabOfFormula ϕ ⊆ vocabOfSetFormula ∅
Theorem: vocElem_subs_vocSet
Proof state before:
ϕ : Formula
phi_in_X : ϕ ∈ ∅
⊢ vocabOfFormula ϕ ⊆ vocabOfSetFormula ∅
Tactic:
cases phi_in_X
Proof state after:
no goals
Theorem: vocElem_subs_vocSet
Proof state before:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula S
⊢ ϕ ∈ insert ψ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert ψ S)
Tactic:
intro psi_in_insert
Proof state after:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula S
psi_in_insert : ϕ ∈ insert ψ S
⊢ vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert ψ S)
Theorem: vocElem_subs_vocSet
Proof state before:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ vocabOfSetFormula S
psi_in_insert : ϕ ∈ insert ψ S
⊢ vocabOfFormula ϕ ⊆ vocabOfSetFormula (insert ψ S)
Tactic:
simp at *
Proof state after:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ S.biUnion vocabOfFormula
psi_in_insert : ϕ = ψ ∨ ϕ ∈ S
⊢ vocabOfFormula ϕ ⊆ vocabOfFormula ψ ∪ S.biUnion vocabOfFormula
Theorem: vocElem_subs_vocSet
Proof state before:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ S.biUnion vocabOfFormula
psi_in_insert : ϕ = ψ ∨ ϕ ∈ S
⊢ vocabOfFormula ϕ ⊆ vocabOfFormula ψ ∪ S.biUnion vocabOfFormula
Tactic:
intro a aIn
Proof state after:
ϕ ψ : Formula
S : Finset Formula
a✝¹ : ψ ∉ S
a✝ : ϕ ∈ S → vocabOfFormula ϕ ⊆ S.biUnion vocabOfFormula
psi_in_insert : ϕ = ψ ∨ ϕ ∈ S
a : Char
aIn : a ∈ vocabOfFormula ϕ
⊢ a ∈ vocabOfFormula ψ ∪ S.biUnion vocabOfFormula