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)