Proof step 1 from proof singletonmxvec-get-sum-aux (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  Σ(0 to n1, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) ≠ (n = r ∧ c < n1 ⊃ a * vec[c];O), n < m, c < # vec, r < m, n1 ≤ # vec ⊦

Rule argument

Additional information

Proof step 2 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  Σ(0 to n0 +1, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) ≠ (n = r ∧ c < n0 +1 ⊃ a * vec[c];O), r < m, c < # vec, n < m, n0 +1 ≤ # vec, ∀ m, vec, r, c, a, n. ¬ ( Σ(0 to n0, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) ≠ (n = r ∧ c < n0 ⊃ a * vec[c];O) ∧ n < m ∧ c < # vec ∧ r < m ∧ n0 ≤ # vec) ⊦

Rule argument

Additional information

Used simplifier rules: sum-base: ⊦ Σ(∅, f) = O; nat freely generated by 0, +1;; ⊦ n to n = ∅; (s) ⊦ ¬ n < 0; (s)

Proof step 3 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  Σ(0 to n0 + 1, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) ≠ (n = r ∧ ¬ n0 < c ⊃ a * vec[c];O), n0 < # vec, r < m, c < # vec, n < m, ∀ m0, vec0, r0, c0, a0, n1. Σ(0 to n0, λ n0. (mkmatrix(m0, # vec0, O)[r0, c0 := a0])[n1, n0] * vec0[n0]) = (n1 = r0 ∧ c0 < n0 ⊃ a0 * vec0[c0];O) ∨ ¬ n1 < m0 ∨ ¬ c0 < # vec0 ∨ ¬ r0 < m0 ∨ ¬ n0 ≤ # vec0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s) ⊦ m +1 = m + 1; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s)

Proof step 4 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ m to n = (m < n ⊃ (m < n ⊃ (m to n - 1) ++ (n - 1);∅);∅)

• Proof step 6:

  Σ((0 < n0 + 1 ⊃ (0 < n0 + 1 ⊃ (0 to n0 + 1 - 1) ++ (n0 + 1 - 1);∅);∅), λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) ≠ (n = r ∧ ¬ n0 < c ⊃ a * vec[c];O), n < m, c < # vec, r < m, n0 < # vec, ∀ m0, vec0, r0, c0, a0, n1. Σ(0 to n0, λ n0. (mkmatrix(m0, # vec0, O)[r0, c0 := a0])[n1, n0] * vec0[n0]) = (n1 = r0 ∧ c0 < n0 ⊃ a0 * vec0[c0];O) ∨ ¬ n1 < m0 ∨ ¬ c0 < # vec0 ∨ ¬ r0 < m0 ∨ ¬ n0 ≤ # vec0 ⊦

Rule argument

Additional information

Used terms: 0, n0 + 1

Proof step 5 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

A spec-lemma

Proof step 6 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  Σ((0 to n0) ++ n0, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) ≠ (n = r ∧ ¬ n0 < c ⊃ a * vec[c];O), n0 < # vec, r < m, c < # vec, n < m, ∀ m0, vec0, r0, c0, a0, n1. Σ(0 to n0, λ n0. (mkmatrix(m0, # vec0, O)[r0, c0 := a0])[n1, n0] * vec0[n0]) = (n1 = r0 ∧ c0 < n0 ⊃ a0 * vec0[c0];O) ∨ ¬ n1 < m0 ∨ ¬ c0 < # vec0 ∨ ¬ r0 < m0 ∨ ¬ n0 ≤ # vec0 ⊦

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n + 0 = n; (s) ⊦ n ≤ m → m + n0 - n = (m - n) + n0; (s) ⊦ m + 1 ≠ 0; (s) ⊦ 0 < m ↔ m ≠ 0; (s)

Proof step 7 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ a ∈ s → s ++ a = s

• Proof step 9:

  Σ((0 to n0) ++ n0, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) ≠ (n = r ∧ ¬ n0 < c ⊃ a * vec[c];O), n < m, c < # vec, r < m, n0 < # vec, ¬ n0 ∈ 0 to n0, ∀ m0, vec0, r0, c0, a0, n1. Σ(0 to n0, λ n0. (mkmatrix(m0, # vec0, O)[r0, c0 := a0])[n1, n0] * vec0[n0]) = (n1 = r0 ∧ c0 < n0 ⊃ a0 * vec0[c0];O) ∨ ¬ n1 < m0 ∨ ¬ c0 < # vec0 ∨ ¬ r0 < m0 ∨ ¬ n0 ≤ # vec0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n0 ∈ m to n ↔ m ≤ n0 ∧ n0 < n; (s) ⊦ 0 ≤ m; (s) ⊦ ¬ n < n; (s) Used terms: n0, 0 to n0

Proof step 8 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0] + Σ(0 to n0, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) ≠ (n = r ∧ ¬ n0 < c ⊃ a * vec[c];O), n0 < # vec, r < m, c < # vec, n < m, ∀ m0, vec0, r0, c0, a0, n1. Σ(0 to n0, λ n0. (mkmatrix(m0, # vec0, O)[r0, c0 := a0])[n1, n0] * vec0[n0]) = (n1 = r0 ∧ c0 < n0 ⊃ a0 * vec0[c0];O) ∨ ¬ n1 < m0 ∨ ¬ c0 < # vec0 ∨ ¬ r0 < m0 ∨ ¬ n0 ≤ # vec0 ⊦

Rule argument

Additional information

Used simplifier rules: sum-rec: ⊦ ¬ n ∈ ns → Σ(ns ++ n, f) = f(n) + Σ(ns, f); ⊦ ¬ n < n; (s) ⊦ 0 ≤ m; (s) ⊦ n0 ∈ m to n ↔ m ≤ n0 ∧ n0 < n; (s)

Proof step 10 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 11:

  (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0] + Σ(0 to n0, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) ≠ (n = r ∧ ¬ n0 < c ⊃ a * vec[c];O), n < m, c < # vec, r < m, n0 < # vec, Σ(0 to n0, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) = (n = r ∧ c < n0 ⊃ a * vec[c];O) ∨ ¬ n < m ∨ ¬ c < # vec ∨ ¬ r < m ∨ ¬ n0 ≤ # vec ⊦

Rule argument

Additional information

Used terms: m, vec, r, c, a, n

Proof step 11 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  Σ(0 to n0, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) = (n = r ∧ c < n0 ⊃ a * vec[c];O), (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0] + (n = r ∧ c < n0 ⊃ a * vec[c];O) ≠ (n = r ∧ ¬ n0 < c ⊃ a * vec[c];O), n0 < # vec, r < m, c < # vec, n < m ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s)

Proof step 12 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  c ≠ c0 ⊦ (mx[r, c := a])[r0, c0] = mx[r0, c0]

• Proof step 14:

  c = n0, Σ(0 to n0, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) = (n = r ∧ c < n0 ⊃ a * vec[c];O), (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0] + (n = r ∧ c < n0 ⊃ a * vec[c];O) ≠ (n = r ∧ ¬ n0 < c ⊃ a * vec[c];O), n < m, c < # vec, r < m, n0 < # vec ⊦

• Proof step 17:

  Σ(0 to n0, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) = (n = r ∧ c < n0 ⊃ a * vec[c];O), mkmatrix(m, # vec, O)[n, n0] * vec[n0] + (n = r ∧ c < n0 ⊃ a * vec[c];O) ≠ (n = r ∧ ¬ n0 < c ⊃ a * vec[c];O), c ≠ n0, n < m, c < # vec, r < m, n0 < # vec ⊦

Rule argument

Additional information

Used terms: n0, mkmatrix(m, # vec, O), a, n, c, r

Proof step 13 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  Σ(0 to n0, λ n1. (mkmatrix(m, # vec, O)[r, n0 := a])[n, n1] * vec[n1]) = O, (mkmatrix(m, # vec, O)[r, n0 := a])[n, n0] * vec[n0] ≠ (n = r ⊃ a * vec[n0];O), r < m, n0 < # vec, n < m ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ n < n; (s) addcom: ⊦ a + b = b + a; from specification ring addassoc: ⊦ (a + b) + c = a + b + c; from specification ring ⊦ a + O = a; (s)

Proof step 15 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  r ≠ r0 ⊦ (mx[(* r0), c0 := a])[(* r), c] = mx[r, c]

Rule argument

Additional information

Used simplifier rules: ⊦ r ≠ r0 → (mx[r, c := a])[r0, c0] = mx[r0, c0]; (s) ⊦ r < r0 ∧ c < c0 → mkmatrix(r0, c0, a)[r, c] = a; (s) ⊦ O * a = O; (s) multassoc: ⊦ (a * b) * c = a * b * c; from specification ring ⊦ #r mkmatrix(r, c, a) = (c = 0 ⊃ 0;r); (s) ⊦ #c mkmatrix(r, c, a) = (r = 0 ⊃ 0;c); (s) ⊦ m < n → n ≠ 0; (s) r < #r mx, c < #c mx ⊦ (mx[r, c := a])[r, c] = a; (s) Used terms: n0, mkmatrix(m, # vec, O), a, r, n0, n

Proof step 16 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  Σ(0 to n0, λ n0. (mkmatrix(m, # vec, O)[r, c := a])[n, n0] * vec[n0]) = (n = r ∧ c < n0 ⊃ a * vec[c];O), (n = r ∧ c < n0 ⊃ a * vec[c];O) ≠ (n = r ∧ ¬ n0 < c ⊃ a * vec[c];O), c ≠ n0, n0 < # vec, r < m, c < # vec, n < m ⊦

Rule argument

Additional information

Used simplifier rules: addcom: ⊦ a + b = b + a; from specification ring addassoc: ⊦ (a + b) + c = a + b + c; from specification ring ⊦ a + O = a; (s) multassoc: ⊦ (a * b) * c = a * b * c; from specification ring ⊦ O * a = O; (s) ⊦ r < r0 ∧ c < c0 → mkmatrix(r0, c0, a)[r, c] = a; (s)

Proof step 18 from proof singletonmxvec-get-sum-aux (previous step) (back to tree)

User applied rule case distinction

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ m ≠ n → (m < n ↔ ¬ n < m); (ss) ⊦ m < n → ¬ n < m; (s)