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