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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  Σ(ns1, λ m. Σ(ns2, λ n. g(m, n))) ≠ Σ(ns2, λ n. Σ(ns1, λ m. g(m, n))) ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  Σ(∅, λ m. Σ(ns2, λ n. g(m, n))) ≠ Σ(ns2, λ n. Σ(∅, λ m. g(m, n))) ⊦

• Proof step 7:

  Σ(ns ++ r, λ m. Σ(ns2, λ n. g(m, n))) ≠ Σ(ns2, λ n. Σ(ns ++ r, λ m. g(m, n))), ∀ ns2, g. Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) = Σ(ns2, λ n. Σ(ns, λ m. g(m, n))) ⊦

Rule argument

Additional information

Used simplifier rules: set('a) generated by ∅, ++;;

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  O ≠ Σ(ns2, λ n. O) ⊦

Rule argument

Additional information

Used simplifier rules: sum-base: ⊦ Σ(∅, f) = O;

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

User applied rule structural induction

And obtained the following new goals

• Proof step 5:

  O = Σ(ns, λ n. O), O ≠ Σ(ns ++ r, λ n. O) ⊦

Rule argument

Additional information

Used simplifier rules: sum-base: ⊦ Σ(∅, f) = O; set('a) generated by ∅, ++;;

Proof step 5 from proof sum-switch (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

Rule argument

Additional information

Used simplifier rules: sum-rec: ⊦ ¬ n ∈ ns → Σ(ns ++ n, f) = f(n) + Σ(ns, f); ⊦ a + O = a; (s) addassoc: ⊦ (a + b) + c = a + b + c; from specification ring addcom: ⊦ a + b = b + a; from specification ring Used terms: r, ns

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ a ∈ s → s ++ a = s

• Proof step 9:

  Σ(ns ++ r, λ m. Σ(ns2, λ n. g(m, n))) ≠ Σ(ns2, λ n. Σ(ns ++ r, λ m. g(m, n))), ¬ r ∈ ns, ∀ ns2, g. Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) = Σ(ns2, λ n. Σ(ns, λ m. g(m, n))) ⊦

• Proof step 14:

  Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) ≠ Σ(ns2, λ n. Σ(ns, λ m. g(m, n))), r ∈ ns, ∀ ns2, g. Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) = Σ(ns2, λ n. Σ(ns, λ m. g(m, n))) ⊦

Rule argument

Additional information

Used terms: r, ns

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  Σ(ns2, λ n. g(r, n)) + Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) ≠ Σ(ns2, λ n. g(r, n) + Σ(ns, λ m. g(m, n))), ¬ r ∈ ns, ∀ ns2, g. Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) = Σ(ns2, λ n. Σ(ns, λ m. g(m, n))) ⊦

Rule argument

Additional information

Used simplifier rules: sum-rec: ⊦ ¬ n ∈ ns → Σ(ns ++ n, f) = f(n) + Σ(ns, f);

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 11:

  ⊦ Σ(ns, f1) + Σ(ns, f2) = Σ(ns, λ n. f1(n) + f2(n))

• Proof step 12:

  Σ(ns2, λ r0. g(r, r0)) + Σ(ns2, λ n0. Σ(ns, λ m. g(m, n0))) = Σ(ns2, λ n. g(r, n) + Σ(ns, λ m. g(m, n))), Σ(ns2, λ n. g(r, n)) + Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) ≠ Σ(ns2, λ n. g(r, n) + Σ(ns, λ m. g(m, n))), ¬ r ∈ ns, ∀ ns2, g. Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) = Σ(ns2, λ n. Σ(ns, λ m. g(m, n))) ⊦

Rule argument

Additional information

Used terms: ns2, λ r0. g(r, r0), λ n0. Σ(ns, λ m. g(m, n0))

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

Lemma sum-add

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

User applied rule subst equation

And obtained the following new goals

• Proof step 13:

  Σ(ns2, λ n. g(r, n)) + Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) ≠ Σ(ns2, λ r0. g(r, r0)) + Σ(ns2, λ n0. Σ(ns, λ m. g(m, n0))), ¬ r ∈ ns, ∀ ns2, g. Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) = Σ(ns2, λ n. Σ(ns, λ m. g(m, n))) ⊦

Rule argument

Additional information

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: ns2, g

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # ns ≠ 0, ns ≠ ∅, Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) ≠ Σ(ns2, λ n. Σ(ns, λ m. g(m, n))), r ∈ ns, ∀ ns2, g. Σ(ns, λ m. Σ(ns2, λ n. g(m, n))) = Σ(ns2, λ n. Σ(ns, λ m. g(m, n))) ⊦

Rule argument

Additional information

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

Proof step 15 from proof sum-switch (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: ns2, g