Proof step 1 from proof sum-union (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  Σ(ns1 ∪ ns2, f) ≠ Σ(ns1, f) + Σ(ns2 \ ns1, f) ⊦

Rule argument

Additional information

Proof step 2 from proof sum-union (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  Σ(ns1 ∪ (ns ++ r), f) ≠ Σ(ns1, f) + Σ((ns ++ r) \ ns1, f), ∀ ns1, f. Σ(ns1 ∪ ns, f) = Σ(ns1, f) + Σ(ns \ ns1, f) ⊦

Rule argument

Additional information

Used simplifier rules: sum-base: ⊦ Σ(∅, f) = O; natset generated by ∅, ++;; ⊦ s ∪ ∅ = s; (s) una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[natset] unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[natset] ⊦ ∅ \ s = ∅; (s) ⊦ a + O = a; (s) addassoc: ⊦ (a + b) + c = a + b + c; from specification ring addcom: ⊦ a + b = b + a; from specification ring

Proof step 3 from proof sum-union (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  Σ((ns ∪ ns1) ++ r, f) ≠ Σ(ns1, f) + Σ((ns ++ r) \ ns1, f), ∀ ns1, f. Σ(ns1 ∪ ns, f) = Σ(ns1, f) + Σ(ns \ ns1, f) ⊦

Rule argument

Additional information

Used simplifier rules: unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[natset] una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[natset] ⊦ (s ++ a) ∪ s0 = (s ∪ s0) ++ a; (s)

Proof step 4 from proof sum-union (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 5:

  Σ(ns1 ∪ ns, f) = Σ(ns1, f) + Σ(ns \ ns1, f), Σ((ns ∪ ns1) ++ r, f) ≠ Σ(ns1, f) + Σ((ns ++ r) \ ns1, f) ⊦

Rule argument

Additional information

Used terms: ns1, f

Proof step 5 from proof sum-union (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ a ∈ s → s ++ a = s

• Proof step 7:

  Σ(ns1 ∪ ns, f) = Σ(ns1, f) + Σ(ns \ ns1, f), Σ((ns ∪ ns1) ++ r, f) ≠ Σ(ns1, f) + Σ((ns ++ r) \ ns1, f), ¬ r ∈ ns ∪ ns1 ⊦

• Proof step 12:

  Σ(ns1 ∪ ns, f) = Σ(ns1, f) + Σ(ns \ ns1, f), Σ(ns ∪ ns1, f) ≠ Σ(ns1, f) + Σ((ns ++ r) \ ns1, f), r ∈ ns ∪ ns1 ⊦

Rule argument

Additional information

Used terms: ns ∪ ns1, r

Proof step 6 from proof sum-union (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof sum-union (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  Σ(ns1 ∪ ns, f) = Σ(ns1, f) + Σ(ns \ ns1, f), f(r) + Σ(ns ∪ ns1, f) ≠ Σ(ns1, f) + Σ((ns \ ns1) ++ r, f), ¬ r ∈ ns, ¬ r ∈ ns1 ⊦

Rule argument

Additional information

Used simplifier rules: sum-rec: ⊦ ¬ n ∈ ns → Σ(ns ++ n, f) = f(n) + Σ(ns, f); ⊦ ¬ a ∈ s1 → (s ++ a) \ s1 = (s \ s1) ++ a; (s) unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[natset] una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[natset] ⊦ a ∈ s ∪ s0 ↔ ¬(¬ a ∈ s ∧ ¬ a ∈ s0); (ss)

Proof step 8 from proof sum-union (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ a ∈ s → s ++ a = s

• Proof step 10:

  Σ(ns1 ∪ ns, f) = Σ(ns1, f) + Σ(ns \ ns1, f), f(r) + Σ(ns ∪ ns1, f) ≠ Σ(ns1, f) + Σ((ns \ ns1) ++ r, f), ¬ r ∈ ns \ ns1, ¬ r ∈ ns, ¬ r ∈ ns1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2; (ws) Used terms: ns \ ns1, r

Proof step 9 from proof sum-union (previous step) (back to tree)

A spec-lemma

Proof step 10 from proof sum-union (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  Σ(ns1 ∪ ns, f) = Σ(ns1, f) + Σ(ns \ ns1, f), f(r) + Σ(ns ∪ ns1, f) ≠ Σ(ns1, f) + f(r) + Σ(ns \ ns1, f), ¬ r ∈ ns1, ¬ r ∈ ns ⊦

Rule argument

Additional information

Used simplifier rules: sum-rec: ⊦ ¬ n ∈ ns → Σ(ns ++ n, f) = f(n) + Σ(ns, f); ⊦ a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2; (ws) addassoc: ⊦ (a + b) + c = a + b + c; from specification ring

Proof step 11 from proof sum-union (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[natset] addassoc: ⊦ (a + b) + c = a + b + c; from specification ring addcom: ⊦ a + b = b + a; from specification ring

Proof step 12 from proof sum-union (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  Σ(ns1 ∪ ns, f) = Σ(ns1, f) + Σ(ns \ ns1, f), #(ns ∪ ns1) ≠ 0, Σ(ns ∪ ns1, f) ≠ Σ(ns1, f) + Σ((ns ++ r) \ ns1, f), ns ∪ ns1 ≠ ∅, r ∈ ns ∪ ns1 ⊦

Rule argument

Additional information

Used simplifier rules: size-zero-01: ⊦ s ≠ ∅ → # s ≠ 0; (forward) from specification set-basic[natset] ne-01: ⊦ a ∈ s → s ≠ ∅; (forward) from specification set-basic[natset]

Proof step 13 from proof sum-union (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ a ∈ s → s ++ a = s

Rule argument

Additional information

Used simplifier rules: unc: ⊦ s ∪ s0 = s0 ∪ s; from specification set-union[natset] ⊦ ¬ a ∈ s → (a ∈ s ∪ s0 ↔ a ∈ s0); (s) una: ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1; from specification set-union[natset] ⊦ a ∈ s1 → (s ++ a) \ s1 = s \ s1; (s) Used terms: ns, r

Proof step 14 from proof sum-union (previous step) (back to tree)

A spec-lemma