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

User applied rule call right

And obtained the following new goals

• Proof step 2:

  spmx = spmx0, okspmx(spmx0, r, # x) ⊦ ⟪y := mkvector(r); while spmx ≠ ∅ do {/* _:invariant y + spmx.toMatrix(r, # x) * x = (spmx`).toMatrix(r, # x) * x ∧ spmx ⊆ spmx` ∧ # y = r wfbound # spmx; */; choose np with np ∈ spmx in {y[np.r] := y[np.r] + spmx[np] * x[np.c]; spmx := spmx -- np}}⟫ (y = spmx0.toMatrix(r, # x) * x)

Rule argument

Additional information

Used simplifier rules: MULT: ⊦ ;

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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 3:

  spmx = spmx0, y = mkvector(r), okspmx(spmx0, r, # x) ⊦ ⟪while spmx ≠ ∅ do {/* _:invariant y + spmx.toMatrix(r, # x) * x = (spmx`).toMatrix(r, # x) * x ∧ spmx ⊆ spmx` ∧ # y = r wfbound # spmx; */; choose np with np ∈ spmx in {y[np.r] := y[np.r] + spmx[np] * x[np.c]; spmx := spmx -- np}}⟫ (y = spmx0.toMatrix(r, # x) * x)

Rule argument

Additional information

Proof step 3 from proof correct (previous step) (back to tree)

Heuristic annotation applied rule annotation right

And obtained the following new goals

• Proof step 4:

  spmx = spmx0, y = mkvector(r), okspmx(spmx0, r, # x) ⊦ y + spmx.toMatrix(r, # x) * x = spmx.toMatrix(r, # x) * x ∧ spmx ⊆ spmx ∧ # y = r

• Proof step 9:

  # y = r, y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x, spmx = spmx1, spmx2 = spmx0, y0 = mkvector(r), spmx ≠ ∅, okspmx(spmx0, r, # x), spmx ⊆ spmx2 ⊦ ⟪choose np with np ∈ spmx in {y[np.r] := y[np.r] + spmx[np] * x[np.c]; spmx := spmx -- np}⟫ ((y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x ∧ spmx ⊆ spmx2 ∧ # y = r) ∧ # spmx < # spmx1)

• Proof step 34:

  # y = r, y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x, spmx = ∅, spmx2 = spmx0, y0 = mkvector(r), y ≠ spmx0.toMatrix(r, # x) * x, okspmx(spmx0, r, # x), spmx ⊆ spmx2 ⊦

Rule argument

Additional information

Used formulas: y + spmx.toMatrix(r, # x) * x = (spmx`).toMatrix(r, # x) * x ∧ spmx ⊆ spmx` ∧ # y = r, # spmx = # spmx

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  mkvector(r) + spmx0.toMatrix(r, # x) * x ≠ spmx0.toMatrix(r, # x) * x, okspmx(spmx0, r, # x) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ # mkvector(n) = n; (s) ⊦ st ⊆ st; (s)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ # x = n → mkvector(n) + x = x

• Proof step 7:

  #(spmx0.toMatrix(r, # x) * x) ≠ r, mkvector(r) + spmx0.toMatrix(r, # x) * x ≠ spmx0.toMatrix(r, # x) * x, okspmx(spmx0, r, # x) ⊦

Rule argument

Additional information

Used terms: r, spmx0.toMatrix(r, # x) * x

Proof step 6 from proof correct (previous step) (back to tree)

Lemma addzero

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ #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; Used terms: spmx0.toMatrix(r, # x), x

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

A spec-lemma

Proof step 9 from proof correct (previous step) (back to tree)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 10:

  # y = r, y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x, spmx = spmx1, spmx2 = spmx0, y0 = mkvector(r), spmx ≠ ∅, okspmx(spmx0, r, # x), np ∈ spmx, spmx ⊆ spmx2 ⊦ ⟪y[np.r] := y[np.r] + spmx[np] * x[np.c]; spmx := spmx -- np⟫ ((y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x ∧ spmx ⊆ spmx2 ∧ # y = r) ∧ # spmx < # spmx1)

• Proof step 28:

  # y = r, y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x, spmx = spmx1, spmx2 = spmx0, y0 = mkvector(r), spmx ≠ ∅, okspmx(spmx0, r, # x), spmx ⊆ spmx2, ∀ np. ¬ np ∈ spmx ⊦ ⟪abort⟫ ((y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x ∧ spmx ⊆ spmx2 ∧ # y = r) ∧ # spmx < # spmx1)

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 11:

  # y1 = r, y1 + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x, spmx = spmx1, spmx2 = spmx0, y = y1[np.r, y1[np.r] + spmx[np] * x[np.c]], y0 = mkvector(r), spmx ≠ ∅, np.r < # y1, np.c < # x, okspmx(spmx0, r, # x), np ∈ spmx, spmx ⊆ spmx2 ⊦ ⟪spmx := spmx -- np⟫ ((y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x ∧ spmx ⊆ spmx2 ∧ # y = r) ∧ # spmx < # spmx1)

• Proof step 14:

  # y = r, y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x, spmx = spmx1, spmx2 = spmx0, y0 = mkvector(r), spmx ≠ ∅, np.r < # y, okspmx(spmx0, r, # x), np ∈ spmx, spmx ⊆ spmx2, ¬ np.c < # x ⊦ ⟪throw ]⟫ ⟪spmx := spmx -- np⟫ ((y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x ∧ spmx ⊆ spmx2 ∧ # y = r) ∧ # spmx < # spmx1)

• Proof step 21:

  # y = r, y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x, spmx = spmx1, spmx2 = spmx0, y0 = mkvector(r), spmx ≠ ∅, okspmx(spmx0, r, # x), np ∈ spmx, spmx ⊆ spmx2, ¬ np.r < # y ⊦ ⟪throw ]⟫ ⟪spmx := spmx -- np⟫ ((y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x ∧ spmx ⊆ spmx2 ∧ # y = r) ∧ # spmx < # spmx1)

Rule argument

Additional information

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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 12:

  # y1 = r, y1 + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x, spmx = spmx1, spmx2 = spmx0, y = y1[np.r, y1[np.r] + spmx[np] * x[np.c]], y0 = mkvector(r), spmx ≠ ∅, np.c < # x, np.r < # y1, okspmx(spmx0, r, # x), np ∈ spmx, spmx ⊆ spmx2 ⊦ (y + (spmx -- np).toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x ∧ spmx -- np ⊆ spmx2 ∧ # y = r) ∧ #(spmx -- np) < # spmx1

Rule argument

Additional information

Proof step 12 from proof correct (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  y1 + spmx1.toMatrix(# y1, # x) * x = spmx0.toMatrix(# y1, # x) * x, y1[np.r, y1[np.r] + spmx1[np] * x[np.c]] + (spmx1 -- np).toMatrix(# y1, # x) * x ≠ spmx0.toMatrix(# y1, # x) * x, spmx1 ≠ ∅, np.c < # x, np.r < # y1, okspmx(spmx0, # y1, # x), np ∈ spmx1, spmx1 ⊆ spmx0 ⊦

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 ⊦ ¬ n < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ # st = 0 ↔ st = ∅; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ n -1 = n - 1; (s) ⊦ a ∈ st → #(st -- a) = (# st)-1; (s) ⊦ # ar[n, a] = # ar; (s) ⊦ st ⊆ st0 → (st -- a ⊆ st0 ↔ true); (ss)

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

Heuristic elimination applied rule apply elim lemma

And closed the goal!

Rule argument

Additional information

Used simplifier rules: main-lemma: ⊦ r × c ∈ spmx ∧ c < # x ∧ r < # y → y[r, y[r] + spmx[r × c] * x[c]] + (spmx -- (r × c)).toMatrix(# y, # x) * x = y + spmx.toMatrix(# y, # x) * x; multassoc: ⊦ (a * b) * c = a * b * c; from specification ring addassoc: ⊦ (a + b) + c = a + b + c; from specification ring addcom: ⊦ a + b = b + a; from specification ring ⊦ r = np.r ∧ c = np.c ↔ np = r × c; (elim) Used terms: np, r, c

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

Heuristic symbolic execution applied rule throw right

And obtained the following new goals

• Proof step 15:

  # y = r, y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x, spmx = spmx1, spmx2 = spmx0, y0 = mkvector(r), spmx ≠ ∅, np.r < # y, okspmx(spmx0, r, # x), np ∈ spmx, spmx ⊆ spmx2, ¬ np.c < # x ⊦

Rule argument

Additional information

Proof step 15 from proof correct (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  y + spmx.toMatrix(# y, # x) * x = spmx0.toMatrix(# y, # x) * x, spmx ≠ ∅, np.r < # y, okspmx(spmx0, # y, # x), np ∈ spmx, # x ≤ np.c, spmx ⊆ spmx0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n ↔ ¬ n ≤ m; (ss)

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

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 17:

  y + spmx.toMatrix(# y, # x) * x = spmx0.toMatrix(# y, # x) * x, np = r × c, spmx ≠ ∅, r < # y, okspmx(spmx0, # y, # x), np ∈ spmx, # x ≤ c, spmx ⊆ spmx0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r = np.r ∧ c = np.c ↔ np = r × c; (elim) Used terms: np, r, c

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  y + spmx.toMatrix(# y, # x) * x = spmx0.toMatrix(# y, # x) * x, spmx ≠ ∅, r < # y, okspmx(spmx0, # y, # x), r × c ∈ spmx, # x ≤ c, spmx ⊆ spmx0 ⊦

Rule argument

Additional information

Proof step 18 from proof correct (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ okspmx(spmx, r, c) ↔ (∀ np. np ∈ spmx → np.r < r ∧ np.c < c)

• Proof step 20:

  y + spmx.toMatrix(# y, # x) * x = spmx0.toMatrix(# y, # x) * x, spmx ≠ ∅, r < # y, r × c ∈ spmx, # x ≤ c, spmx ⊆ spmx0, ∀ np. np ∈ spmx0 → np.r < # y ∧ np.c < # x ⊦

Rule argument

Additional information

Used terms: spmx0, # y, # x

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

Lemma okspmx-def

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (n × n0).r = n; (s) ⊦ (n × n0).c = n0; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ b ∈ st ∧ ¬ b ∈ st0 → ¬ st ⊆ st0; (s) Used terms: r × c

Proof step 21 from proof correct (previous step) (back to tree)

Heuristic symbolic execution applied rule throw right

And obtained the following new goals

• Proof step 22:

  # y = r, y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x, spmx = spmx1, spmx2 = spmx0, y0 = mkvector(r), spmx ≠ ∅, okspmx(spmx0, r, # x), np ∈ spmx, spmx ⊆ spmx2, ¬ np.r < # y ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  y + spmx.toMatrix(# y, # x) * x = spmx0.toMatrix(# y, # x) * x, spmx ≠ ∅, okspmx(spmx0, # y, # x), np ∈ spmx, # y ≤ np.r, spmx ⊆ spmx0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 23 from proof correct (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 24:

  y + spmx.toMatrix(# y, # x) * x = spmx0.toMatrix(# y, # x) * x, np = r × c, spmx ≠ ∅, okspmx(spmx0, # y, # x), np ∈ spmx, # y ≤ r, spmx ⊆ spmx0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r = np.r ∧ c = np.c ↔ np = r × c; (elim) Used terms: np, r, c

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 25:

  y + spmx.toMatrix(# y, # x) * x = spmx0.toMatrix(# y, # x) * x, spmx ≠ ∅, okspmx(spmx0, # y, # x), r × c ∈ spmx, # y ≤ r, spmx ⊆ spmx0 ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  ⊦ okspmx(spmx, r, c) ↔ (∀ np. np ∈ spmx → np.r < r ∧ np.c < c)

• Proof step 27:

  y + spmx.toMatrix(# y, # x) * x = spmx0.toMatrix(# y, # x) * x, spmx ≠ ∅, r × c ∈ spmx, # y ≤ r, spmx ⊆ spmx0, ∀ np. np ∈ spmx0 → np.r < # y ∧ np.c < # x ⊦

Rule argument

Additional information

Used terms: spmx0, # y, # x

Proof step 26 from proof correct (previous step) (back to tree)

Lemma okspmx-def

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

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (n × n0).r = n; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ b ∈ st ∧ ¬ b ∈ st0 → ¬ st ⊆ st0; (s) Used terms: r × c

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

Heuristic symbolic execution applied rule abort right

And obtained the following new goals

• Proof step 29:

  # y = r, y + spmx.toMatrix(r, # x) * x = spmx2.toMatrix(r, # x) * x, spmx = spmx1, spmx2 = spmx0, y0 = mkvector(r), spmx ≠ ∅, okspmx(spmx0, r, # x), spmx ⊆ spmx2, ∀ np. ¬ np ∈ spmx ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 30:

  y + spmx.toMatrix(# y, # x) * x = spmx0.toMatrix(# y, # x) * x, spmx ≠ ∅, okspmx(spmx0, # y, # x), spmx ⊆ spmx0, ∀ np. ¬ np ∈ spmx ⊦

Rule argument

Additional information

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ st1 = st2 ↔ (∀ a. (a ∈ st1 ↔ a ∈ st2) ∧ st1[a] = st2[a])

• Proof step 32:

  y + spmx.toMatrix(# y, # x) * x = spmx0.toMatrix(# y, # x) * x, okspmx(spmx0, # y, # x), spmx ⊆ spmx0, ∀ np. ¬ np ∈ spmx, ∃ np. ¬((np ∈ spmx ↔ np ∈ ∅) ∧ spmx[np] = ∅[np]) ⊦

Rule argument

Additional information

Used terms: spmx, ∅

Proof step 31 from proof correct (previous step) (back to tree)

A spec-lemma

Proof step 32 from proof correct (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 33:

  y + spmx.toMatrix(# y, # x) * x = spmx0.toMatrix(# y, # x) * x, okspmx(spmx0, # y, # x), np ∈ spmx, spmx ⊆ spmx0, ∀ np. ¬ np ∈ spmx ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ a ∈ st → st[a] = ∅[a]; (s) ⊦ ¬ a ∈ ∅; (s)

Proof step 33 from proof correct (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: np

Proof step 34 from proof correct (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 35:

  y + mkvector(# y) = spmx0.toMatrix(# y, # x) * x, y ≠ spmx0.toMatrix(# y, # x) * x, okspmx(spmx0, # y, # x) ⊦

Rule argument

Additional information

Used simplifier rules: multzero: ⊦ # x = n → ∅.toMatrix(m, n) * x = mkvector(m); ⊦ ∅ ⊆ st; (s)

Proof step 35 from proof correct (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 36:

  ⊦ # vec1 = # vec2 → vec1 + vec2 = vec2 + vec1

Rule argument

Additional information

Used simplifier rules: addzero: ⊦ # x = n → mkvector(n) + x = x; ⊦ # mkvector(n) = n; (s) Used terms: y, mkvector(# y)

Proof step 36 from proof correct (previous step) (back to tree)

A spec-lemma