Proof step 1 from proof toMatrix-add (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof toMatrix-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ mx1 = mx2 ↔ #r mx1 = #r mx2 ∧ #c mx1 = #c mx2 ∧ (∀ r, c. r < #r mx1 ∧ c < #c mx1 → mx1[r, c] = mx2[r, c])

• Proof step 4:

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

Rule argument

Additional information

Used terms: spmx[r × c, a].toMatrix(m, n), spmx.toMatrix(m, n) + mkmatrix(m, n, O)[r, c, a]

Proof step 3 from proof toMatrix-add (previous step) (back to tree)

A spec-lemma

Proof step 4 from proof toMatrix-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (r0 × c0 ∈ spmx[r × c, a] ⊃ spmx[r × c, a][r0 × c0];O) ≠ (spmx.toMatrix(m, n) + mkmatrix(m, n, O)[r, c, a])[r0, c0], c0 < n, r0 < m, c < n, r < m, ¬ r × c ∈ spmx ⊦

Rule argument

Additional information

Used simplifier rules: toMatrix-rowno: ⊦ #r spmx.toMatrix(r, c) = r; toMatrix-colno: ⊦ #c spmx.toMatrix(r, c) = c; toMatrix-get: ⊦ m < r ∧ n < c → spmx.toMatrix(r, c)[m, n] = (m × n ∈ spmx ⊃ spmx[m × n];O); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ #c(mx1 + mx2) = #c mx1; (s) ⊦ #r(mx1 + mx2) = #r mx1; (s)

Proof step 5 from proof toMatrix-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

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

• Proof step 7:

  (r0 × c0 ∈ spmx[r × c, a] ⊃ spmx[r × c, a][r0 × c0];O) ≠ spmx.toMatrix(m, n)[r0, c0] + mkmatrix(m, n, O)[r, c, a][r0, c0], r < m, c < n, r0 < m, c0 < n, r0 < #r spmx.toMatrix(m, n), c0 < #c spmx.toMatrix(m, n), ¬ r × c ∈ spmx ⊦

Rule argument

Additional information

Used simplifier rules: toMatrix-rowno: ⊦ #r spmx.toMatrix(r, c) = r; toMatrix-colno: ⊦ #c spmx.toMatrix(r, c) = c; Used terms: spmx.toMatrix(m, n), mkmatrix(m, n, O)[r, c, a], r0, c0

Proof step 6 from proof toMatrix-add (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof toMatrix-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  (r0 × c0 ∈ spmx[r × c, a] ⊃ spmx[r × c, a][r0 × c0];O) ≠ (r0 × c0 ∈ spmx ⊃ spmx[r0 × c0];O) + mkmatrix(m, n, O)[r, c, a][r0, c0], c < n, r < m, c0 < n, r0 < m, ¬ r × c ∈ spmx ⊦

Rule argument

Additional information

Used simplifier rules: toMatrix-get: ⊦ m < r ∧ n < c → spmx.toMatrix(r, c)[m, n] = (m × n ∈ spmx ⊃ spmx[m × n];O); toMatrix-colno: ⊦ #c spmx.toMatrix(r, c) = c; toMatrix-rowno: ⊦ #r spmx.toMatrix(r, c) = r;

Proof step 8 from proof toMatrix-add (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  spmx[r × c, a][r0 × c0] ≠ (r0 × c0 ∈ spmx ⊃ spmx[r0 × c0];O) + mkmatrix(m, n, O)[r, c, a][r0, c0], r0 < m, c0 < n, r < m, c < n, r0 × c0 ∈ spmx[r × c, a], ¬ r × c ∈ spmx ⊦

• Proof step 16:

  O ≠ (r0 × c0 ∈ spmx ⊃ spmx[r0 × c0];O) + mkmatrix(m, n, O)[r, c, a][r0, c0], r0 < m, c0 < n, r < m, c < n, ¬ r0 × c0 ∈ spmx[r × c, a], ¬ r × c ∈ spmx ⊦

Rule argument

Additional information

Proof step 9 from proof toMatrix-add (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 10:

  spmx[r × c, a][r0 × c0] ≠ spmx[r0 × c0] + mkmatrix(m, n, O)[r, c, a][r0, c0], c < n, r < m, c0 < n, r0 < m, r0 × c0 ∈ spmx[r × c, a], r0 × c0 ∈ spmx, ¬ r × c ∈ spmx ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ a + O = a; (s) addassoc: ⊦ (a + b) + c = a + b + c; from specification ring addcom: ⊦ a + b = b + a; from specification ring ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st; (ws) ⊦ n × n0 = n1 × n2 ↔ n = n1 ∧ n0 = n2; (ws) lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ a = b → st[b, d][a] = d; (s) ⊦ #r mkmatrix(r, c, a) = r; (s) ⊦ #c mkmatrix(r, c, a) = c; (s) r < #r mx, c < #c mx ⊦ mx[r, c, a][r, c] = a; (s)

Proof step 10 from proof toMatrix-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  spmx[r0 × c0] ≠ spmx[r0 × c0] + mkmatrix(m, n, O)[r, c, a][r0, c0], r0 < m, c0 < n, r < m, c < n, r0 × c0 ∈ spmx, r0 × c0 ∈ spmx[r × c, a], ¬ r × c ∈ spmx ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ b ∈ st ∧ ¬ a ∈ st → st[a, d][b] = st[b]; (s)

Proof step 11 from proof toMatrix-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

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

• Proof step 13:

  c = c0, spmx[r0 × c0] ≠ spmx[r0 × c0] + mkmatrix(m, n, O)[r, c, a][r0, c0], c < n, r < m, c0 < n, r0 < m, r0 × c0 ∈ spmx[r × c, a], r0 × c0 ∈ spmx, ¬ r × c ∈ spmx ⊦

Rule argument

Additional information

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

Proof step 12 from proof toMatrix-add (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof toMatrix-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  spmx[r0 × c0] ≠ spmx[r0 × c0] + mkmatrix(m, n, O)[r, c0, a][r0, c0], r0 < m, r < m, c0 < n, r0 × c0 ∈ spmx, r0 × c0 ∈ spmx[r × c0, a], ¬ r × c0 ∈ spmx ⊦

Rule argument

Additional information

Proof step 14 from proof toMatrix-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

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

Rule argument

Additional information

Used simplifier rules: ⊦ r < r0 ∧ c < c0 → mkmatrix(r0, c0, a)[r, c] = a; (s) ⊦ a + O = a; (s) addassoc: ⊦ (a + b) + c = a + b + c; from specification ring addcom: ⊦ a + b = b + a; from specification ring ⊦ ¬ a ∈ st → st[a] = ∅[a]; (s) ⊦ #r mkmatrix(r, c, a) = r; (s) ⊦ #c mkmatrix(r, c, a) = c; (s) r < #r mx, c < #c mx ⊦ mx[r, c, a][r, c] = a; (s) Used terms: c0, r, c0, r0, mkmatrix(m, n, O), a

Proof step 15 from proof toMatrix-add (previous step) (back to tree)

A spec-lemma

Proof step 16 from proof toMatrix-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  O ≠ mkmatrix(m, n, O)[r, c, a][r0, c0], r0 × c0 ≠ r × c, c < n, r < m, c0 < n, r0 < m, ¬ r × c ∈ spmx, ¬ r0 × c0 ∈ spmx ⊦

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) ⊦ a ∈ st[b, d] ↔ a = b ∨ a ∈ st; (ws)

Proof step 17 from proof toMatrix-add (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

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

Rule argument

Additional information

Used simplifier rules: ⊦ r < r0 ∧ c < c0 → mkmatrix(r0, c0, a)[r, c] = a; (s) ⊦ n × n0 = n1 × n2 ↔ n = n1 ∧ n0 = n2; (ws) ⊦ r ≠ r0 → mx[r, c, a][r0, c0] = mx[r0, c0]; (s) Used terms: c0, r0, c, r, mkmatrix(m, n, O), a

Proof step 18 from proof toMatrix-add (previous step) (back to tree)

A spec-lemma