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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Proof step 3 from proof distrmxmx-r (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 = #c mx2, #c mx = #r mx2, #r mx1 = #r mx2, #r(mx * (mx1 + mx2)) ≠ #r(mx * mx1 + mx * mx2) ∨ #c(mx * (mx1 + mx2)) ≠ #c(mx * mx1 + mx * mx2) ∨ (∃ r, c. ¬(r < #r(mx * (mx1 + mx2)) ∧ c < #c(mx * (mx1 + mx2)) → (mx * (mx1 + mx2))[r, c] = (mx * mx1 + mx * mx2)[r, c])) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

Proof step 6 from proof distrmxmx-r (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 = #c mx2, #c mx = #r mx2, #c mx = #r(mx1 + mx2), #r mx1 = #r mx2, #r mx ≠ #r(mx * mx1) ∨ #c(mx * (mx1 + mx2)) ≠ #c(mx * mx1) ∨ ¬(r < #r mx ∧ c < #c(mx * (mx1 + mx2)) → (mx * (mx1 + mx2))[r, c] = (mx * mx1 + mx * mx2)[r, c]) ⊦

Rule argument

Additional information

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

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

Lemma multmx-rowno

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  #c mx = #r mx2, #c mx1 = #c mx2, #r mx1 = #r mx2, #c(mx * (mx1 + mx2)) ≠ #c mx2 ∨ ¬(r < #r mx ∧ c < #c(mx * (mx1 + mx2)) → (mx * (mx1 + mx2))[r, c] = (mx * mx1 + mx * mx2)[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; multmx-colno: ⊦ #c mx1 = #r mx2 → #c(mx1 * mx2) = #c mx2;

Proof step 9 from proof distrmxmx-r (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 = #c mx2, #c mx = #r mx2, #c mx = #r(mx1 + mx2), #r mx1 = #r mx2, #c(mx1 + mx2) ≠ #c mx2 ∨ ¬(r < #r mx ∧ c < #c(mx1 + mx2) → (mx * (mx1 + mx2))[r, c] = (mx * mx1 + mx * mx2)[r, c]) ⊦

Rule argument

Additional information

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

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

Lemma multmx-colno

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: addmx-rowno: ⊦ #r(mx1 + mx2) = #r mx1; addmx-colno: ⊦ #c(mx1 + mx2) = #c mx1; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic

Proof step 12 from proof distrmxmx-r (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 mx1 = #c mx2, #c mx = #r mx2, #c mx = #r(mx1 + mx2), #r mx1 = #r mx2, Σ(0 to #c mx, λ n. mx[r, n] * (mx1 + mx2)[n, c]) ≠ (mx * mx1 + mx * mx2)[r, c], c < #c mx2, r < #r mx, c < #c(mx1 + mx2) ⊦

Rule argument

Additional information

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

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

Lemma multmx-get

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

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

Proof step 15 from proof distrmxmx-r (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 = #c mx2, #c mx = #r mx2, #r mx1 = #r mx2, Σ(0 to #r mx2, λ n. mx[r, n] * (mx1 + mx2)[n, c]) ≠ (mx * mx1 + mx * mx2)[r, c], r < #r mx, c < #c mx2 ⊦ r < #r(mx * mx1) ∧ c < #c(mx * mx1)

• Proof step 19:

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

Rule argument

Additional information

Used terms: mx * mx1, mx * mx2, r, c

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

Lemma addmx-get

Proof step 17 from proof distrmxmx-r (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(mx1 * mx2) = #r mx1

Rule argument

Additional information

Used simplifier rules: 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: mx, mx1

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

Lemma multmx-rowno

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

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

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) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 20 from proof distrmxmx-r (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 mx = #r mx2, #c mx1 = #c mx2, #c mx = #r mx1, #r mx1 = #r mx2, Σ(0 to #r mx2, λ n. mx[r, n] * (mx1 + mx2)[n, c]) ≠ Σ(0 to #c mx, λ n. mx[r, n] * mx1[n, c]) + Σ(0 to #r mx2, λ n. mx[r, n] * mx2[n, c]), c < #c(mx * mx1), r < #r(mx * mx1), c < #c mx2, r < #r mx, c < #c mx1 ⊦

Rule argument

Additional information

Used terms: mx, mx1, r, c

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

Lemma multmx-get

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

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 distrmxmx-r (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

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

Rule argument

Additional information

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

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

Lemma sum-add

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 26:

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

• Proof step 27:

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

Rule argument

Additional information

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

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

Lemma sum-red

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  #c mx = #r mx1, #c mx1 = #c mx2, #r mx2 = #r mx1, mx[r, n] * (mx1 + mx2)[n, c] ≠ mx[r, n] * mx1[n, c] + mx[r, n] * mx2[n, c], Σ(0 to #r mx1, λ n. mx[r, n] * (mx1 + mx2)[n, c]) ≠ Σ(0 to #r mx1, λ n. mx[r, n] * mx1[n, c] + mx[r, n] * mx2[n, c]), n < #r mx1, r < #r mx, c < #c 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 28 from proof distrmxmx-r (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

• Proof step 30:

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

Rule argument

Additional information

Used simplifier rules: ⊦ 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, n, c

Proof step 29 from proof distrmxmx-r (previous step) (back to tree)

Lemma addmx-get

Proof step 30 from proof distrmxmx-r (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

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

Rule argument

Additional information

Proof step 31 from proof distrmxmx-r (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

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

Rule argument

Additional information

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

Proof step 32 from proof distrmxmx-r (previous step) (back to tree)

A spec-lemma