Proof step 1 from proof mult-assoc (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  #c mx1 = #r mx2, #c mx2 = #r mx3, (mx1 * mx2) * mx3 ≠ mx1 * mx2 * mx3 ⊦

Rule argument

Additional information

Proof step 2 from proof mult-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ mx1 = mx2 ↔ #r mx1 = #r mx2 ∧ #c mx1 = #c mx2 ∧ (∀ r, c. r < #r mx1 ∧ c < #c mx1 → mx1[r, c] = mx2[r, c])

• Proof step 4:

  #c mx2 = #r mx3, #c mx1 = #r mx2, #r((mx1 * mx2) * mx3) ≠ #r(mx1 * mx2 * mx3) ∨ #c((mx1 * mx2) * mx3) ≠ #c(mx1 * mx2 * mx3) ∨ (∃ r, c. ¬(r < #r((mx1 * mx2) * mx3) ∧ c < #c((mx1 * mx2) * mx3) → ((mx1 * mx2) * mx3)[r, c] = (mx1 * mx2 * mx3)[r, c])) ⊦

Rule argument

Additional information

Used terms: (mx1 * mx2) * mx3, mx1 * mx2 * mx3

Proof step 3 from proof mult-assoc (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof mult-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  #c mx1 = #r mx2, #c mx2 = #r mx3, #r((mx1 * mx2) * mx3) ≠ #r(mx1 * mx2 * mx3) ∨ #c((mx1 * mx2) * mx3) ≠ #c(mx1 * mx2 * mx3) ∨ ¬(r < #r((mx1 * mx2) * mx3) ∧ c < #c((mx1 * mx2) * mx3) → ((mx1 * mx2) * mx3)[r, c] = (mx1 * mx2 * mx3)[r, c]) ⊦

Rule argument

Additional information

Proof step 5 from proof mult-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1

• Proof step 7:

  #c mx2 = #r mx3, #c mx1 = #r mx2, #c mx1 = #r(mx2 * mx3), #r((mx1 * mx2) * mx3) ≠ #r mx1 ∨ #c((mx1 * mx2) * mx3) ≠ #c(mx1 * mx2 * mx3) ∨ ¬(r < #r((mx1 * mx2) * mx3) ∧ c < #c((mx1 * mx2) * mx3) → ((mx1 * mx2) * mx3)[r, c] = (mx1 * mx2 * mx3)[r, c]) ⊦

Rule argument

Additional information

Used simplifier rules: multmx-rowno: ⊦ #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1; Used terms: mx1, mx2 * mx3

Proof step 6 from proof mult-assoc (previous step) (back to tree)

Lemma multmx-rowno

Proof step 7 from proof mult-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  #c mx2 = #r mx3, #c mx1 = #r mx2, #r((mx1 * mx2) * mx3) ≠ #r mx1 ∨ #c((mx1 * mx2) * mx3) ≠ #c(mx1 * mx2 * mx3) ∨ ¬(r < #r((mx1 * mx2) * mx3) ∧ c < #c((mx1 * mx2) * mx3) → ((mx1 * mx2) * mx3)[r, c] = (mx1 * mx2 * mx3)[r, c]) ⊦

Rule argument

Additional information

Used simplifier rules: multmx-rowno: ⊦ #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1;

Proof step 8 from proof mult-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1

• Proof step 10:

  #c mx1 = #r mx2, #c mx2 = #r mx3, #c(mx1 * mx2) = #r mx3, #r(mx1 * mx2) ≠ #r mx1 ∨ #c((mx1 * mx2) * mx3) ≠ #c(mx1 * mx2 * mx3) ∨ ¬(r < #r(mx1 * mx2) ∧ c < #c((mx1 * mx2) * mx3) → ((mx1 * mx2) * mx3)[r, c] = (mx1 * mx2 * mx3)[r, c]) ⊦

Rule argument

Additional information

Used simplifier rules: multmx-colno: ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2; Used terms: mx1 * mx2, mx3

Proof step 9 from proof mult-assoc (previous step) (back to tree)

Lemma multmx-rowno

Proof step 10 from proof mult-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  #c mx1 = #r mx2, #c mx2 = #r mx3, #c((mx1 * mx2) * mx3) ≠ #c(mx1 * mx2 * mx3) ∨ ¬(r < #r mx1 ∧ c < #c((mx1 * mx2) * mx3) → ((mx1 * mx2) * mx3)[r, c] = (mx1 * mx2 * mx3)[r, c]) ⊦

Rule argument

Additional information

Used simplifier rules: multmx-colno: ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2; multmx-rowno: ⊦ #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1;

Proof step 11 from proof mult-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2

• Proof step 13:

  #c mx2 = #r mx3, #c mx1 = #r mx2, #c(mx1 * mx2) = #r mx3, #c mx3 ≠ #c(mx1 * mx2 * mx3) ∨ ¬(r < #r mx1 ∧ c < #c mx3 → ((mx1 * mx2) * mx3)[r, c] = (mx1 * mx2 * mx3)[r, c]) ⊦

Rule argument

Additional information

Used simplifier rules: multmx-colno: ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2; Used terms: mx1 * mx2, mx3

Proof step 12 from proof mult-assoc (previous step) (back to tree)

Lemma multmx-colno

Proof step 13 from proof mult-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  #c mx1 = #r mx2, #c mx2 = #r mx3, #c mx3 ≠ #c(mx1 * mx2 * mx3) ∨ ¬(r < #r mx1 ∧ c < #c mx3 → ((mx1 * mx2) * mx3)[r, c] = (mx1 * mx2 * mx3)[r, c]) ⊦

Rule argument

Additional information

Used simplifier rules: multmx-colno: ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2;

Proof step 14 from proof mult-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2

• Proof step 16:

  #c mx2 = #r mx3, #c mx1 = #r mx2, #c mx1 = #r(mx2 * mx3), #c mx3 ≠ #c(mx2 * mx3) ∨ ¬(r < #r mx1 ∧ c < #c mx3 → ((mx1 * mx2) * mx3)[r, c] = (mx1 * mx2 * mx3)[r, c]) ⊦

Rule argument

Additional information

Used simplifier rules: multmx-rowno: ⊦ #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1; Used terms: mx1, mx2 * mx3

Proof step 15 from proof mult-assoc (previous step) (back to tree)

Lemma multmx-colno

Proof step 16 from proof mult-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  #c mx1 = #r mx2, #c mx2 = #r mx3, ((mx1 * mx2) * mx3)[r, c] ≠ (mx1 * mx2 * mx3)[r, c], c < #c mx3, r < #r mx1 ⊦

Rule argument

Additional information

Used simplifier rules: multmx-rowno: ⊦ #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1; multmx-colno: ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 17 from proof mult-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ #c mx1 = #r mx2 ∧ r < #r mx1 ∧ c < #c mx2 → (mx1 * mx2)[r, c] = Σ(0 to #c mx1, λ n. mx1[r, n] * mx2[n, c])

• Proof step 19:

  #c mx2 = #r mx3, #c mx1 = #r mx2, #c(mx1 * mx2) = #r mx3, Σ(0 to #c(mx1 * mx2), λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ (mx1 * mx2 * mx3)[r, c], r < #r mx1, r < #r(mx1 * mx2), c < #c mx3 ⊦

Rule argument

Additional information

Used simplifier rules: multmx-colno: ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2; multmx-rowno: ⊦ #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1; Used terms: mx1 * mx2, mx3, r, c

Proof step 18 from proof mult-assoc (previous step) (back to tree)

Lemma multmx-get

Proof step 19 from proof mult-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  #c mx1 = #r mx2, #c mx2 = #r mx3, Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ (mx1 * mx2 * mx3)[r, c], c < #c mx3, r < #r mx1 ⊦

Rule argument

Additional information

Used simplifier rules: multmx-colno: ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2; multmx-rowno: ⊦ #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1;

Proof step 20 from proof mult-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ #c mx1 = #r mx2 ∧ r < #r mx1 ∧ c < #c mx2 → (mx1 * mx2)[r, c] = Σ(0 to #c mx1, λ n. mx1[r, n] * mx2[n, c])

• Proof step 22:

  #c mx2 = #r mx3, #c mx1 = #r mx2, #c mx1 = #r(mx2 * mx3), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #c mx1, λ n. mx1[r, n] * (mx2 * mx3)[n, c]), c < #c mx3, r < #r mx1, c < #c(mx2 * mx3) ⊦

Rule argument

Additional information

Used simplifier rules: multmx-rowno: ⊦ #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1; multmx-colno: ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2; Used terms: mx1, mx2 * mx3, r, c

Proof step 21 from proof mult-assoc (previous step) (back to tree)

Lemma multmx-get

Proof step 22 from proof mult-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  #c mx2 = #r mx3, #c mx1 = #r mx2, Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx2, λ n. mx1[r, n] * (mx2 * mx3)[n, c]), r < #r mx1, c < #c mx3 ⊦

Rule argument

Additional information

Used simplifier rules: multmx-rowno: ⊦ #c mx1 = #r mx2 → #r(mx1 * mx2) = #r mx1; multmx-colno: ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2;

Proof step 23 from proof mult-assoc (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 24:

  #c mx1 = #r mx2, #c mx2 = #r mx3, Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) = Σ(0 to #r mx3, λ n. Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c])), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx2, λ n. mx1[r, n] * (mx2 * mx3)[n, c]), c < #c mx3, r < #r mx1 ⊦

• Proof step 31:

  #c mx1 = #r mx2, #c mx2 = #r mx3, Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx3, λ n. Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c])), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx2, λ n. mx1[r, n] * (mx2 * mx3)[n, c]), c < #c mx3, r < #r mx1 ⊦

Rule argument

Additional information

Used formulas: Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) = Σ(0 to #r mx3, λ n. Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c]))

Proof step 24 from proof mult-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 25:

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

• Proof step 26:

  #c mx2 = #r mx3, #c mx1 = #r mx2, Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) = Σ(0 to #r mx2, λ n. Σ(0 to #r mx3, λ m. mx1[r, n] * mx2[n, m] * mx3[m, c])), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx2, λ n. mx1[r, n] * (mx2 * mx3)[n, c]), r < #r mx1, c < #c mx3 ⊦

Rule argument

Additional information

Used simplifier rules: multassoc: ⊦ (a * b) * c = a * b * c; from specification ring Used terms: 0 to #r mx3, 0 to #r mx2, λ r0, r1. mx1[r, r1] * mx2[r1, r0] * mx3[r0, c]

Proof step 25 from proof mult-assoc (previous step) (back to tree)

Lemma sum-switch

Proof step 26 from proof mult-assoc (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 27:

  ⊦ (∀ n. n ∈ ns → f1(n) = f2(n)) → Σ(ns, f1) = Σ(ns, f2)

• Proof step 28:

  #c mx1 = #r mx2, #c mx2 = #r mx3, Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) = Σ(0 to #r mx2, λ n. Σ(0 to #r mx3, λ m. mx1[r, n] * mx2[n, m] * mx3[m, c])), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx2, λ n. mx1[r, n] * (mx2 * mx3)[n, c]), c < #c mx3, r < #r mx1, (∀ n. n ∈ 0 to #r mx2 → Σ(0 to #r mx3, λ m. mx1[r, n] * mx2[n, m] * mx3[m, c]) = mx1[r, n] * (mx2 * mx3)[n, c]) → Σ(0 to #r mx2, λ n. Σ(0 to #r mx3, λ m. mx1[r, n] * mx2[n, m] * mx3[m, c])) = Σ(0 to #r mx2, λ n. mx1[r, n] * (mx2 * mx3)[n, c]) ⊦

Rule argument

Additional information

Used terms: 0 to #r mx2, λ n. Σ(0 to #r mx3, λ m. mx1[r, n] * mx2[n, m] * mx3[m, c]), λ n. mx1[r, n] * (mx2 * mx3)[n, c]

Proof step 27 from proof mult-assoc (previous step) (back to tree)

Lemma sum-red

Proof step 28 from proof mult-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

  #c mx2 = #r mx3, #c mx1 = #r mx2, Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) = Σ(0 to #r mx2, λ n. Σ(0 to #r mx3, λ m. mx1[r, n] * mx2[n, m] * mx3[m, c])), Σ(0 to #r mx3, λ m. mx1[r, n] * mx2[n, m] * mx3[m, c]) ≠ mx1[r, n] * Σ(0 to #r mx3, λ n0. mx2[n, n0] * mx3[n0, c]), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx2, λ n. mx1[r, n] * (mx2 * mx3)[n, c]), n < #r mx2, r < #r mx1, c < #c mx3 ⊦

Rule argument

Additional information

Used simplifier rules: multmx-get: ⊦ #c mx1 = #r mx2 ∧ r < #r mx1 ∧ c < #c mx2 → (mx1 * mx2)[r, c] = Σ(0 to #c mx1, λ n. mx1[r, n] * mx2[n, c]); ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ 0 ≤ m; (s) ⊦ n0 ∈ m to n ↔ m ≤ n0 ∧ n0 < n; (s)

Proof step 29 from proof mult-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

Used simplifier rules: multassoc: ⊦ (a * b) * c = a * b * c; from specification ring Used terms: mx1[r, n], 0 to #r mx3, λ n0. mx2[n, n0] * mx3[n0, c]

Proof step 30 from proof mult-assoc (previous step) (back to tree)

Lemma sum-multl

Proof step 31 from proof mult-assoc (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 32:

  ⊦ (∀ n. n ∈ ns → f1(n) = f2(n)) → Σ(ns, f1) = Σ(ns, f2)

• Proof step 33:

  #c mx2 = #r mx3, #c mx1 = #r mx2, Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx3, λ n. Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c])), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx2, λ n. mx1[r, n] * (mx2 * mx3)[n, c]), r < #r mx1, c < #c mx3, (∀ n. n ∈ 0 to #r mx3 → (mx1 * mx2)[r, n] * mx3[n, c] = Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c])) → Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) = Σ(0 to #r mx3, λ n. Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c])) ⊦

Rule argument

Additional information

Used terms: 0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c], λ n. Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c])

Proof step 32 from proof mult-assoc (previous step) (back to tree)

Lemma sum-red

Proof step 33 from proof mult-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  #c mx2 = #r mx3, #c mx1 = #r mx2, Σ(0 to #r mx2, λ n0. mx1[r, n0] * mx2[n0, n]) * mx3[n, c] ≠ Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c]), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx2, λ n. mx1[r, n] * (mx2 * mx3)[n, c]), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx3, λ n. Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c])), n < #r mx3, r < #r mx1, c < #c mx3 ⊦

Rule argument

Additional information

Used simplifier rules: multmx-get: ⊦ #c mx1 = #r mx2 ∧ r < #r mx1 ∧ c < #c mx2 → (mx1 * mx2)[r, c] = Σ(0 to #c mx1, λ n. mx1[r, n] * mx2[n, c]); ⊦ m < n → n ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ 0 ≤ m; (s) ⊦ n0 ∈ m to n ↔ m ≤ n0 ∧ n0 < n; (s)

Proof step 34 from proof mult-assoc (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 35:

  ⊦ (∀ n. n ∈ ns → f1(n) = f2(n)) → Σ(ns, f1) = Σ(ns, f2)

• Proof step 36:

  #c mx1 = #r mx2, #c mx2 = #r mx3, Σ(0 to #r mx2, λ n0. mx1[r, n0] * mx2[n0, n]) * mx3[n, c] ≠ Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c]), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx2, λ n. mx1[r, n] * (mx2 * mx3)[n, c]), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx3, λ n. Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c])), c < #c mx3, r < #r mx1, n < #r mx3, (∀ n. n ∈ 0 to #r mx3 → Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c]) = (mx1 * mx2)[r, n] * mx3[n, c]) → Σ(0 to #r mx3, λ n. Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c])) = Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ⊦

Rule argument

Additional information

Used terms: 0 to #r mx3, λ n. Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c]), λ n. (mx1 * mx2)[r, n] * mx3[n, c]

Proof step 35 from proof mult-assoc (previous step) (back to tree)

Lemma sum-red

Proof step 36 from proof mult-assoc (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 37:

  #c mx1 = #r mx2, #c mx2 = #r mx3, Σ(0 to #r mx2, λ n0. mx1[r, n0] * mx2[n0, n]) * mx3[n, c] ≠ Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c]), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx3, λ n. Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n] * mx3[n, c])), Σ(0 to #r mx3, λ n. (mx1 * mx2)[r, n] * mx3[n, c]) ≠ Σ(0 to #r mx2, λ n. mx1[r, n] * (mx2 * mx3)[n, c]), Σ(0 to #r mx2, λ m. mx1[r, m] * mx2[m, n0] * mx3[n0, c]) ≠ Σ(0 to #r mx2, λ n. mx1[r, n] * mx2[n, n0]) * mx3[n0, c], n0 < #r mx3, c < #c mx3, r < #r mx1, n < #r mx3 ⊦

Rule argument

Additional information

Used simplifier rules: multmx-get: ⊦ #c mx1 = #r mx2 ∧ r < #r mx1 ∧ c < #c mx2 → (mx1 * mx2)[r, c] = Σ(0 to #c mx1, λ n. mx1[r, n] * mx2[n, c]); lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ 0 ≤ m; (s) ⊦ n0 ∈ m to n ↔ m ≤ n0 ∧ n0 < n; (s)

Proof step 37 from proof mult-assoc (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 38:

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

Rule argument

Additional information

Used simplifier rules: multassoc: ⊦ (a * b) * c = a * b * c; from specification ring Used terms: 0 to #r mx2, λ n. mx1[r, n] * mx2[n, n0], mx3[n0, c]

Proof step 38 from proof mult-assoc (previous step) (back to tree)

Lemma sum-multr