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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

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

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

Rule argument

Additional information

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

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

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

Rule argument

Additional information

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

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

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

Rule argument

Additional information

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

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

Lemma multvecmx-size

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

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

Rule argument

Additional information

Used simplifier rules: addmx-rowno: ⊦ #r(mx1 + mx2) = #r mx1; multvecmx-size: ⊦ #r mx = # vec → #(vec * mx) = #c mx; addmx-colno: ⊦ #c(mx1 + mx2) = #c 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 distrvecmxmx (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:

  # vec = #r mx2, #c mx1 = #c mx2, #r mx1 = #r mx2, #r(mx1 + mx2) = # vec, Σ(0 to # vec, λ n0. vec(n0) * (mx1 + mx2)(n0, n)) ≠ (vec * mx1 + vec * mx2)(n), n < #c mx2, n < #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: vec, mx1 + mx2, n

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

Lemma multvecmx-get

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

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

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

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

• Proof step 17:

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

Rule argument

Additional information

Used terms: vec * mx1, vec * mx2, n

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

Lemma addmvec-get

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

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

Proof step 15 from proof distrvecmxmx (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: lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m.+1 < n0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → ¬ n < m; (s) Used terms: vec, mx1

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

Lemma multvecmx-size

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

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

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

Proof step 18 from proof distrvecmxmx (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:

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

Rule argument

Additional information

Used terms: vec, mx1, n

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

Lemma multvecmx-get

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

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

Rule argument

Additional information

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

Proof step 21 from proof distrvecmxmx (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:

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

Rule argument

Additional information

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

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

Lemma sum-add

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

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

Rule argument

Additional information

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

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

Lemma sum-red

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 27:

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

• Proof step 28:

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

Rule argument

Additional information

Used terms: mx1, mx2, n0, n

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

Lemma addmx-get

Proof step 28 from proof distrvecmxmx (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 30:

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

Rule argument

Additional information

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

Proof step 30 from proof distrvecmxmx (previous step) (back to tree)

A spec-lemma