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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  a * Σ(ns, f) ≠ Σ(ns, λ n. a * f(n)) ⊦

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  a * Σ(ns0 ++ r, f) ≠ Σ(ns0 ++ r, λ n. a * f(n)), ∀ a, f. a * Σ(ns0, f) = Σ(ns0, λ n. a * f(n)) ⊦

Rule argument

Additional information

Used simplifier rules: sum-base: ⊦ Σ(∅, f) = O; set('a) generated by ∅, ++;; ⊦ a * O = O; (s) multassoc: ⊦ (a * b) * c = a * b * c; from specification ring

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ a ∈ s → s ++ a = s

• Proof step 5:

  a * Σ(ns0 ++ r, f) ≠ Σ(ns0 ++ r, λ n. a * f(n)), ¬ r ∈ ns0, ∀ a, f. a * Σ(ns0, f) = Σ(ns0, λ n. a * f(n)) ⊦

• Proof step 9:

  a * Σ(ns0, f) ≠ Σ(ns0, λ n. a * f(n)), r ∈ ns0, ∀ a, f. a * Σ(ns0, f) = Σ(ns0, λ n. a * f(n)) ⊦

Rule argument

Additional information

Used terms: r, ns0

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  a * (f(r) + Σ(ns0, f)) ≠ a * f(r) + Σ(ns0, λ n. a * f(n)), ¬ r ∈ ns0, ∀ a, f. a * Σ(ns0, f) = Σ(ns0, λ n. a * f(n)) ⊦

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ a * (b + c) = a * b + a * c

• Proof step 8:

  a * f(r) + a * Σ(ns0, f) ≠ a * f(r) + Σ(ns0, λ n. a * f(n)), ¬ r ∈ ns0, ∀ a, f. a * Σ(ns0, f) = Σ(ns0, λ n. a * f(n)) ⊦

Rule argument

Additional information

Used terms: a, f(r), Σ(ns0, f)

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

A spec-lemma

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a, f

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  # ns0 ≠ 0, a * Σ(ns0, f) ≠ Σ(ns0, λ n. a * f(n)), ns0 ≠ ∅, r ∈ ns0, ∀ a, f. a * Σ(ns0, f) = Σ(ns0, λ n. a * f(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 10 from proof sum-multl (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: a, f