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