Proof step 1 from proof distrmxmx-l (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof distrmxmx-l (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Proof step 3 from proof distrmxmx-l (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ 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 5:

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

Rule argument

Additional information

Used terms: (mx1 + mx2) * mx, mx1 * mx + mx2 * mx

Proof step 4 from proof distrmxmx-l (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof distrmxmx-l (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

Proof step 6 from proof distrmxmx-l (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

Used simplifier rules: addmx-colno: ⊦ #c(mx1 + mx2) = #c mx1; Used terms: mx1 + mx2, mx

Proof step 7 from proof distrmxmx-l (previous step) (back to tree)

Lemma multmx-rowno

Proof step 8 from proof distrmxmx-l (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

Used simplifier rules: addmx-colno: ⊦ #c(mx1 + mx2) = #c mx1; addmx-rowno: ⊦ #r(mx1 + mx2) = #r mx1;

Proof step 9 from proof distrmxmx-l (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

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

Rule argument

Additional information

Used simplifier rules: addmx-colno: ⊦ #c(mx1 + mx2) = #c mx1; Used terms: mx1 + mx2, mx

Proof step 10 from proof distrmxmx-l (previous step) (back to tree)

Lemma multmx-colno

Proof step 11 from proof distrmxmx-l (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: addmx-colno: ⊦ #c(mx1 + mx2) = #c mx1; ⊦ 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

Proof step 12 from proof distrmxmx-l (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ #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 14:

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

Rule argument

Additional information

Used simplifier rules: addmx-colno: ⊦ #c(mx1 + mx2) = #c mx1; addmx-rowno: ⊦ #r(mx1 + mx2) = #r mx1; ⊦ m < n ↔ ¬ n ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ ¬ n < n; (s) Used terms: mx1 + mx2, mx, r, c

Proof step 13 from proof distrmxmx-l (previous step) (back to tree)

Lemma multmx-get

Proof step 14 from proof distrmxmx-l (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: addmx-colno: ⊦ #c(mx1 + mx2) = #c mx1; addmx-rowno: ⊦ #r(mx1 + mx2) = #r mx1;

Proof step 15 from proof distrmxmx-l (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ r < #r mx1 ∧ c < #c mx1 → (mx1 + mx2)[r, c] = mx1[r, c] + mx2[r, c]

• Proof step 17:

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

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 ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ ¬ n < n; (s) Used terms: mx1 * mx, mx2 * mx, r, c

Proof step 16 from proof distrmxmx-l (previous step) (back to tree)

Lemma addmx-get

Proof step 17 from proof distrmxmx-l (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

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

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; 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]);

Proof step 18 from proof distrmxmx-l (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

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

Rule argument

Additional information

Used terms: 0 to #r mx, λ n. mx1[r, n] * mx[n, c], λ n. mx2[r, n] * mx[n, c]

Proof step 19 from proof distrmxmx-l (previous step) (back to tree)

Lemma sum-add

Proof step 20 from proof distrmxmx-l (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

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

Rule argument

Additional information

Used terms: 0 to #r mx, λ n. (mx1 + mx2)[r, n] * mx[n, c], λ n. mx1[r, n] * mx[n, c] + mx2[r, n] * mx[n, c]

Proof step 21 from proof distrmxmx-l (previous step) (back to tree)

Lemma sum-red

Proof step 22 from proof distrmxmx-l (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Used simplifier rules: ⊦ 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 23 from proof distrmxmx-l (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ r < #r mx1 ∧ c < #c mx1 → (mx1 + mx2)[r, c] = mx1[r, c] + mx2[r, c]

• Proof step 25:

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

Rule argument

Additional information

Used terms: mx1, mx2, r, n

Proof step 24 from proof distrmxmx-l (previous step) (back to tree)

Lemma addmx-get

Proof step 25 from proof distrmxmx-l (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

Proof step 26 from proof distrmxmx-l (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

Used terms: mx1[r, n], mx2[r, n], mx[n, c]

Proof step 27 from proof distrmxmx-l (previous step) (back to tree)

A spec-lemma