Proof step 1 from proof distrmxmxvec (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof distrmxmxvec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Proof step 3 from proof distrmxmxvec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1(n) = ar2(n))

• Proof step 5:

  #c mx1 = # vec, #c mx2 = # vec, #r mx1 = #r mx2, #((mx1 + mx2) * vec) ≠ #(mx1 * vec + mx2 * vec) ∨ (∃ n. ¬(n < #((mx1 + mx2) * vec) → ((mx1 + mx2) * vec)(n) = (mx1 * vec + mx2 * vec)(n))) ⊦

Rule argument

Additional information

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

Proof step 4 from proof distrmxmxvec (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof distrmxmxvec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  #c mx2 = # vec, #c mx1 = # vec, #r mx1 = #r mx2, #((mx1 + mx2) * vec) ≠ #r mx2 ∨ ¬(n < #((mx1 + mx2) * vec) → ((mx1 + mx2) * vec)(n) = (mx1 * vec + mx2 * vec)(n)) ⊦

Rule argument

Additional information

Used simplifier rules: addvec-size: ⊦ #(vec1 + vec2) = # vec1; multmxvec-size: ⊦ #c mx = # vec → #(mx * vec) = #r mx;

Proof step 6 from proof distrmxmxvec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

  ⊦ #c mx = # vec → #(mx * vec) = #r mx

• Proof step 8:

  #c mx1 = # vec, #c mx2 = # vec, #c(mx1 + mx2) = # vec, #r mx1 = #r mx2, #r(mx1 + mx2) ≠ #r mx2 ∨ ¬(n < #r(mx1 + mx2) → ((mx1 + mx2) * vec)(n) = (mx1 * vec + mx2 * vec)(n)) ⊦

Rule argument

Additional information

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

Proof step 7 from proof distrmxmxvec (previous step) (back to tree)

Lemma multmxvec-size

Proof step 8 from proof distrmxmxvec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  #c mx1 = # vec, #c mx2 = # vec, #r mx1 = #r mx2, ((mx1 + mx2) * vec)(n) ≠ (mx1 * vec + mx2 * vec)(n), n < #r mx2 ⊦

Rule argument

Additional information

Used simplifier rules: addmx-colno: ⊦ #c(mx1 + mx2) = #c mx1; addmx-rowno: ⊦ #r(mx1 + mx2) = #r 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 9 from proof distrmxmxvec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ #c mx = # vec ∧ r < #r mx → (mx * vec)(r) = Σ(0 to # vec, λ n. mx(r, n) * vec(n))

• Proof step 11:

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

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, vec, n

Proof step 10 from proof distrmxmxvec (previous step) (back to tree)

Lemma multmxvec-get

Proof step 11 from proof distrmxmxvec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  #c mx2 = # vec, #c mx1 = # vec, #r mx1 = #r mx2, Σ(0 to # vec, λ n0. (mx1 + mx2)(n, n0) * vec(n0)) ≠ (mx1 * vec + mx2 * vec)(n), n < #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 12 from proof distrmxmxvec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ n < # vec1 → (vec1 + vec2)(n) = vec1(n) + vec2(n)

• Proof step 14:

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

Rule argument

Additional information

Used simplifier rules: multmxvec-size: ⊦ #c mx = # vec → #(mx * vec) = #r mx; ⊦ 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 * vec, mx2 * vec, n

Proof step 13 from proof distrmxmxvec (previous step) (back to tree)

Lemma addmvec-get

Proof step 14 from proof distrmxmxvec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: multmxvec-size: ⊦ #c mx = # vec → #(mx * vec) = #r mx; multmxvec-get: ⊦ #c mx = # vec ∧ r < #r mx → (mx * vec)(r) = Σ(0 to # vec, λ n. mx(r, n) * vec(n));

Proof step 15 from proof distrmxmxvec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

• Proof step 17:

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

Rule argument

Additional information

Used terms: 0 to # vec, λ n0. mx1(n, n0) * vec(n0), λ n0. mx2(n, n0) * vec(n0)

Proof step 16 from proof distrmxmxvec (previous step) (back to tree)

Lemma sum-add

Proof step 17 from proof distrmxmxvec (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 18:

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

• Proof step 19:

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

Rule argument

Additional information

Used terms: 0 to # vec, λ n0. (mx1 + mx2)(n, n0) * vec(n0), λ n0. mx1(n, n0) * vec(n0) + mx2(n, n0) * vec(n0)

Proof step 18 from proof distrmxmxvec (previous step) (back to tree)

Lemma sum-red

Proof step 19 from proof distrmxmxvec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  #c mx2 = # vec, #c mx1 = # vec, #r mx1 = #r mx2, (mx1 + mx2)(n, n0) * vec(n0) ≠ mx1(n, n0) * vec(n0) + mx2(n, n0) * vec(n0), Σ(0 to # vec, λ n0. (mx1 + mx2)(n, n0) * vec(n0)) ≠ Σ(0 to # vec, λ n0. mx1(n, n0) * vec(n0) + mx2(n, n0) * vec(n0)), n0 < # vec, n < #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 20 from proof distrmxmxvec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

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

• Proof step 22:

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

Rule argument

Additional information

Used terms: mx1, mx2, n, n0

Proof step 21 from proof distrmxmxvec (previous step) (back to tree)

Lemma addmx-get

Proof step 22 from proof distrmxmxvec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

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

Rule argument

Additional information

Proof step 23 from proof distrmxmxvec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

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

Rule argument

Additional information

Used terms: mx1(n, n0), mx2(n, n0), vec(n0)

Proof step 24 from proof distrmxmxvec (previous step) (back to tree)

A spec-lemma