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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  # vec1 = # vec2, #c mx = # vec1, mx * (vec1 + vec2) ≠ mx * vec1 + mx * vec2 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  # vec1 = # vec2, #c mx = # vec2, mx * (vec1 + vec2) ≠ mx * vec1 + mx * vec2 ⊦

Rule argument

Additional information

Proof step 3 from proof distrmxvecvec (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:

  # vec1 = # vec2, #c mx = # vec2, #(mx * (vec1 + vec2)) ≠ #(mx * vec1 + mx * vec2) ∨ (∃ n. ¬(n < #(mx * (vec1 + vec2)) → (mx * (vec1 + vec2))[n] = (mx * vec1 + mx * vec2)[n])) ⊦

Rule argument

Additional information

Used terms: mx * (vec1 + vec2), mx * vec1 + mx * vec2

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  # vec1 = # vec2, #c mx = # vec2, #(mx * (vec1 + vec2)) ≠ #(mx * vec1) ∨ ¬(n < #(mx * (vec1 + vec2)) → (mx * (vec1 + vec2))[n] = (mx * vec1 + mx * vec2)[n]) ⊦

Rule argument

Additional information

Used simplifier rules: addvec-size: ⊦ #(vec1 + vec2) = # vec1;

Proof step 6 from proof distrmxvecvec (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:

  # vec1 = # vec2, #c mx = # vec2, #c mx = #(vec1 + vec2), #r mx ≠ #(mx * vec1) ∨ ¬(n < #r mx → (mx * (vec1 + vec2))[n] = (mx * vec1 + mx * vec2)[n]) ⊦

Rule argument

Additional information

Used simplifier rules: addvec-size: ⊦ #(vec1 + vec2) = # vec1; Used terms: mx, vec1 + vec2

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

Lemma multmxvec-size

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # vec1 = # vec2, #c mx = # vec2, (mx * (vec1 + vec2))[n] ≠ (mx * vec1 + mx * vec2)[n], n < #r mx ⊦

Rule argument

Additional information

Used simplifier rules: addvec-size: ⊦ #(vec1 + vec2) = # vec1; multmxvec-size: ⊦ #c mx = # vec → #(mx * vec) = #r mx; ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 9 from proof distrmxvecvec (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:

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

Rule argument

Additional information

Used simplifier rules: addvec-size: ⊦ #(vec1 + vec2) = # vec1; Used terms: mx, vec1 + vec2, n

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

Lemma multmxvec-get

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: addvec-size: ⊦ #(vec1 + vec2) = # vec1;

Proof step 12 from proof distrmxvecvec (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:

  # vec1 = # vec2, #c mx = # vec2, Σ(0 to # vec2, λ n0. mx[n, n0] * (vec1 + vec2)[n0]) ≠ (mx * vec1 + mx * vec2)[n], n < #r mx, ¬ n < #(mx * vec1) ⊦

• Proof step 17:

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

Rule argument

Additional information

Used terms: mx * vec1, mx * vec2, n

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

Lemma addmvec-get

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # vec1 = # vec2, #c mx = # vec2, Σ(0 to # vec2, λ n0. mx[n, n0] * (vec1 + vec2)[n0]) ≠ (mx * vec1 + mx * vec2)[n], n < #r mx, #(mx * vec1) < #r mx, #(mx * vec1) ≤ n ⊦

Rule argument

Additional information

Used simplifier rules: fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: mx, vec1

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

Lemma multmxvec-size

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

Used simplifier rules: multmxvec-get: ⊦ #c mx = # vec ∧ r < #r mx → (mx * vec)[r] = Σ(0 to # vec, λ n. mx[r, n] * vec[n]); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

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

Rule argument

Additional information

Used terms: mx, vec1, n

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

Lemma multmxvec-get

Proof step 20 from proof distrmxvecvec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

• Proof step 23:

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

Rule argument

Additional information

Used terms: 0 to # vec2, λ n0. mx[n, n0] * vec1[n0], λ n0. mx[n, n0] * vec2[n0]

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

Lemma sum-add

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 24:

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

• Proof step 25:

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

Rule argument

Additional information

Used terms: 0 to # vec2, λ n0. mx[n, n0] * (vec1 + vec2)[n0], λ n0. mx[n, n0] * vec1[n0] + mx[n, n0] * vec2[n0]

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

Lemma sum-red

Proof step 25 from proof distrmxvecvec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

Rule argument

Additional information

Used simplifier rules: addmvec-get: ⊦ n < # vec1 → (vec1 + vec2)[n] = vec1[n] + vec2[n]; ⊦ 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 26 from proof distrmxvecvec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

Rule argument

Additional information

Used terms: mx[n, n0], vec1[n0], vec2[n0]

Proof step 27 from proof distrmxvecvec (previous step) (back to tree)

A spec-lemma