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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Proof step 3 from proof distrvevecmx (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, #r mx = # vec2, #((vec1 + vec2) * mx) ≠ #(vec1 * mx + vec2 * mx) ∨ (∃ n. ¬(n < #((vec1 + vec2) * mx) → ((vec1 + vec2) * mx)(n) = (vec1 * mx + vec2 * mx)(n))) ⊦

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 7:

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

• Proof step 8:

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

Rule argument

Additional information

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

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

Lemma multvecmx-size

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

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

Proof step 9 from proof distrvevecmx (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

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

Rule argument

Additional information

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

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

Lemma multvecmx-get

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

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

Proof step 12 from proof distrvevecmx (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, #r mx = # vec2, Σ(0 to # vec2, λ n0. (vec1 + vec2)(n0) * mx(n0, n)) ≠ (vec1 * mx + vec2 * mx)(n), n < #c mx, ¬ n < #(vec1 * mx) ⊦

• Proof step 17:

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

Rule argument

Additional information

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

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

Lemma addmvec-get

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  # vec1 = # vec2, #r mx = # vec2, Σ(0 to # vec2, λ n0. (vec1 + vec2)(n0) * mx(n0, n)) ≠ (vec1 * mx + vec2 * mx)(n), n < #c mx, #(vec1 * mx) < #c mx, #(vec1 * mx) ≤ 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 distrvevecmx (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

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

Rule argument

Additional information

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

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

Lemma multvecmx-size

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

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

• Proof step 20:

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

Rule argument

Additional information

Used terms: vec1, mx, n

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

Lemma multvecmx-get

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

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

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

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

• Proof step 23:

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

Rule argument

Additional information

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

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

Lemma multvecmx-get

Proof step 23 from proof distrvevecmx (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:

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

Rule argument

Additional information

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

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

Lemma sum-add

Proof step 25 from proof distrvevecmx (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:

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

Rule argument

Additional information

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

Proof step 26 from proof distrvevecmx (previous step) (back to tree)

Lemma sum-red

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  # vec1 = # vec2, #r mx = # vec2, (vec1(n0) + vec2(n0)) * mx(n0, n) ≠ vec1(n0) * mx(n0, n) + vec2(n0) * mx(n0, n), Σ(0 to # vec2, λ n0. (vec1 + vec2)(n0) * mx(n0, n)) ≠ Σ(0 to # vec2, λ n0. vec1(n0) * mx(n0, n) + vec2(n0) * mx(n0, n)), n0 < # vec2, n < #c 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 28 from proof distrvevecmx (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Used terms: vec1(n0), vec2(n0), mx(n0, n)

Proof step 29 from proof distrvevecmx (previous step) (back to tree)

A spec-lemma