Proof step 1 from proof main-lemma (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  y[r, y[r] + spmx[r × c] * x[c]] + (spmx -- (r × c)).toMatrix(# y, # x) * x ≠ y + spmx.toMatrix(# y, # x) * x, c < # x, r < # y, r × c ∈ spmx ⊦

Rule argument

Additional information

Proof step 2 from proof main-lemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ a ∈ st ↔ (∃ d, st0. st = st0[a, d] ∧ ¬ a ∈ st0)

• Proof step 4:

  y[r, y[r] + spmx[r × c] * x[c]] + (spmx -- (r × c)).toMatrix(# y, # x) * x ≠ y + spmx.toMatrix(# y, # x) * x, r < # y, c < # x, ∃ d, st0. spmx = st0[r × c, d] ∧ ¬ r × c ∈ st0 ⊦

Rule argument

Additional information

Used terms: r × c, spmx

Proof step 3 from proof main-lemma (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof main-lemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x ≠ y + spmx0[r × c, a].toMatrix(# y, # x) * x, r < # y, c < # x, ¬ r × c ∈ spmx0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ ¬ a ∈ st → st -- a = st; (s) ⊦ st[a, d] -- a = st -- a; (s) ⊦ a = b → st[b, d][a] = d; (s)

Proof step 5 from proof main-lemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ r < m ∧ c < n ∧ ¬ r × c ∈ spmx → spmx[r × c, a].toMatrix(m, n) = spmx.toMatrix(m, n) + mkmatrix(m, n, O)[r, c, a]

• Proof step 7:

  y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x ≠ y + (spmx0.toMatrix(# y, # x) + mkmatrix(# y, # x, O)[r, c, a]) * x, r < # y, c < # x, ¬ r × c ∈ spmx0 ⊦

Rule argument

Additional information

Used terms: # x, # y, spmx0, c, r, a

Proof step 6 from proof main-lemma (previous step) (back to tree)

Lemma toMatrix-add

Proof step 7 from proof main-lemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ #r mx1 = #r mx2 ∧ #c mx1 = #c mx2 ∧ #c mx1 = # vec → (mx1 + mx2) * vec = mx1 * vec + mx2 * vec

• Proof step 9:

  #c spmx0.toMatrix(# y, # x) = #c mkmatrix(# y, # x, O)[r, c, a], #c spmx0.toMatrix(# y, # x) = # x, #r spmx0.toMatrix(# y, # x) = #r mkmatrix(# y, # x, O)[r, c, a], y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x ≠ y + spmx0.toMatrix(# y, # x) * x + mkmatrix(# y, # x, O)[r, c, a] * x, c < # x, r < # y, ¬ r × c ∈ spmx0 ⊦

Rule argument

Additional information

Used simplifier rules: toMatrix-rowno: ⊦ #r spmx.toMatrix(r, c) = r; toMatrix-colno: ⊦ #c spmx.toMatrix(r, c) = c; ⊦ #r mx[r, c, a] = #r mx; (s) ⊦ #r mkmatrix(r, c, a) = r; (s) ⊦ #c mx[r, c, a] = #c mx; (s) ⊦ #c mkmatrix(r, c, a) = c; (s) Used terms: spmx0.toMatrix(# y, # x), mkmatrix(# y, # x, O)[r, c, a], x

Proof step 8 from proof main-lemma (previous step) (back to tree)

A spec-lemma

Proof step 9 from proof main-lemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x ≠ y + spmx0.toMatrix(# y, # x) * x + mkmatrix(# y, # x, O)[r, c, a] * x, r < # y, c < # x, ¬ r × c ∈ spmx0 ⊦

Rule argument

Additional information

Used simplifier rules: toMatrix-rowno: ⊦ #r spmx.toMatrix(r, c) = r; toMatrix-colno: ⊦ #c spmx.toMatrix(r, c) = c; ⊦ #c mkmatrix(r, c, a) = c; (s) ⊦ #c mx[r, c, a] = #c mx; (s) ⊦ #r mkmatrix(r, c, a) = r; (s) ⊦ #r mx[r, c, a] = #r mx; (s)

Proof step 10 from proof main-lemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 11:

  ⊦ ar1 = ar2 ↔ # ar1 = # ar2 ∧ (∀ n. n < # ar1 → ar1[n] = ar2[n])

• Proof step 12:

  c < # x, r < # y, ¬ r × c ∈ spmx0, #(y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x) ≠ #(y + spmx0.toMatrix(# y, # x) * x + mkmatrix(# y, # x, O)[r, c, a] * x) ∨ (∃ n. ¬ ( n < #(y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x) → (y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x)[n] = (y + spmx0.toMatrix(# y, # x) * x + mkmatrix(# y, # x, O)[r, c, a] * x)[n])) ⊦

Rule argument

Additional information

Used terms: y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x, y + spmx0.toMatrix(# y, # x) * x + mkmatrix(# y, # x, O)[r, c, a] * x

Proof step 11 from proof main-lemma (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof main-lemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  (y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x)[n] ≠ y[n] + (spmx0.toMatrix(# y, # x) * x + mkmatrix(# y, # x, O)[r, c, a] * x)[n], r < # y, c < # x, n < # y, ¬ r × c ∈ spmx0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ n < # vec1 → (vec1 + vec2)[n] = vec1[n] + vec2[n]; (s) ⊦ # ar[n, a] = # ar; (s) ⊦ #(vec1 + vec2) = # vec1; (s)

Proof step 13 from proof main-lemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  ⊦ n < # vec1 → (vec1 + vec2)[n] = vec1[n] + vec2[n]

• Proof step 15:

  (y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x)[n] ≠ y[n] + (spmx0.toMatrix(# y, # x) * x + mkmatrix(# y, # x, O)[r, c, a] * x)[n], n < # y, c < # x, r < # y, ¬ n < #(spmx0.toMatrix(# y, # x) * x), ¬ r × c ∈ spmx0 ⊦

• Proof step 18:

  (y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x)[n] ≠ y[n] + (spmx0.toMatrix(# y, # x) * x)[n] + (mkmatrix(# y, # x, O)[r, c, a] * x)[n], n < # y, c < # x, r < # y, n < #(spmx0.toMatrix(# y, # x) * x), ¬ r × c ∈ spmx0 ⊦

Rule argument

Additional information

Used terms: spmx0.toMatrix(# y, # x) * x, mkmatrix(# y, # x, O)[r, c, a] * x, n

Proof step 14 from proof main-lemma (previous step) (back to tree)

A spec-lemma

Proof step 15 from proof main-lemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  (y[r, y[r] + a * x[c]] + spmx0.toMatrix(# y, # x) * x)[n] ≠ y[n] + (spmx0.toMatrix(# y, # x) * x + mkmatrix(# y, # x, O)[r, c, a] * x)[n], r < # y, c < # x, n < # y, #(spmx0.toMatrix(# y, # x) * x) < # y, #(spmx0.toMatrix(# y, # x) * x) ≤ n, ¬ r × c ∈ spmx0 ⊦

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 16 from proof main-lemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

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

Rule argument

Additional information

Used simplifier rules: toMatrix-colno: ⊦ #c spmx.toMatrix(r, c) = c; toMatrix-colno: ⊦ #c spmx.toMatrix(r, c) = c; toMatrix-rowno: ⊦ #r spmx.toMatrix(r, c) = r; ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: spmx0.toMatrix(# y, # x), x

Proof step 17 from proof main-lemma (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof main-lemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ n < # vec1 → (vec1 + vec2)[n] = vec1[n] + vec2[n]

• Proof step 20:

  y[r, y[r] + a * x[c]][n] + (spmx0.toMatrix(# y, # x) * x)[n] ≠ y[n] + (spmx0.toMatrix(# y, # x) * x)[n] + (mkmatrix(# y, # x, O)[r, c, a] * x)[n], n < #(spmx0.toMatrix(# y, # x) * x), r < # y, c < # x, n < # y, n < # y[r, y[r] + a * x[c]], ¬ r × c ∈ spmx0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # ar[n, a] = # ar; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s) Used terms: y[r, y[r] + a * x[c]], spmx0.toMatrix(# y, # x) * x, n

Proof step 19 from proof main-lemma (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof main-lemma (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 21:

  y[r, y[r] + a * x[c]][n] + (spmx0.toMatrix(# y, # x) * x)[n] ≠ y[n] + (spmx0.toMatrix(# y, # x) * x)[n] + (mkmatrix(# y, # x, O)[r, c, a] * x)[n], n < #(spmx0.toMatrix(# y, # x) * x), r < # y, c < # x, n < # y, ¬ r × c ∈ spmx0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ # ar[n, a] = # ar; (s)

Proof step 21 from proof main-lemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ r < m ∧ c < # vec ∧ n < m → (mkmatrix(m, # vec, O)[r, c, a] * vec)[n] = (n = r ⊃ a * vec[c];O)

• Proof step 23:

  y[r, y[r] + a * x[c]][n] + (spmx0.toMatrix(# y, # x) * x)[n] ≠ y[n] + (spmx0.toMatrix(# y, # x) * x)[n] + (n = r ⊃ a * x[c];O), n < #(spmx0.toMatrix(# y, # x) * x), r < # y, c < # x, n < # y, ¬ r × c ∈ spmx0 ⊦

Rule argument

Additional information

Used terms: x, n, # y, c, r, a

Proof step 22 from proof main-lemma (previous step) (back to tree)

A spec-lemma

Proof step 23 from proof main-lemma (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ m ≠ n → ar[n, a][m] = ar[m]

Rule argument

Additional information

Used simplifier rules: ⊦ a + O = a; (s) addcom: ⊦ a + b = b + a; from specification ring addassoc: ⊦ (a + b) + c = a + b + c; from specification ring ⊦ m < # ar → ar[m, a][m] = a; (s) Used terms: y, r, y[r] + a * x[c], n

Proof step 24 from proof main-lemma (previous step) (back to tree)

A spec-lemma