| A.cols = B.rows, m2 = 0, C1 = A.rows × B.cols, m ≤ C2.rows, C2.rows = A.rows, C2.cols = B.cols, ∀ m0, n0. m0 < C2.rows ∧ n0 < C2.cols → C2[m0, n0] = C1[m0, n0] + (m0 < m ∧ n0 < C2.cols ⊃ Σ(B.rows, λ k. A[m0, k] * B[k, n0]);0), C2 = C0, m = m1, m < C2.rows, k1 = 0, k ≤ B.rows, C.rows = A.rows, C.cols = B.cols, ∀ m0, n0. m0 < C.rows ∧ n0 < C.cols → C[m0, n0] = C2[m0, n0] + (m0 = m ∧ n0 < C.cols ⊃ Σ(k, λ k. A[m0, k] * B[k, n0]);0), k = k0, k < B.rows ⊦ ⟨let n = 0 in while n < C.cols do {/* (correctness invariant: n ≤ C.cols ∧ C.rows = A.rows ∧ C.cols = B.cols ∧ (∀ m0, n0. m0 < C.rows ∧ n0 < C.cols → C[m0, n0] = (C`)[m0, n0] + (m0 = m ∧ n0 < n ⊃ A[m0, k] * B[k, n0];0)) wfbound: C.cols - n) */; C[m, n] := C[m, n] + A[m, k] * B[k, n]; n := n + 1}⟩ ⟨k := k + 1⟩ ( ( k ≤ B.rows ∧ C.rows = A.rows ∧ C.cols = B.cols ∧ (∀ m0, n0. m0 < C.rows ∧ n0 < C.cols → C[m0, n0] = C2[m0, n0] + (m0 = m ∧ n0 < C.cols ⊃ Σ(k, λ k. A[m0, k] * B[k, n0]);0))) ∧ B.rows - k < B.rows - k0) |
A.cols = B.rows, m2 = 0, C1 = A.rows × B.cols, m ≤ C2.rows, C2.rows = A.rows, C2.cols = B.cols, ∀ m0, n0. m0 < C2.rows ∧ n0 < C2.cols → C2[m0, n0] = C1[m0, n0] + (m0 < m ∧ n0 < C2.cols ⊃ Σ(B.rows, λ k. A[m0, k] * B[k, n0]);0), C2 = C0, m = m1, m < C2.rows, k1 = 0, k ≤ B.rows, C.rows = A.rows, C.cols = B.cols, ∀ m0, n0. m0 < C.rows ∧ n0 < C.cols → C[m0, n0] = C2[m0, n0] + (m0 = m ∧ n0 < C.cols ⊃ Σ(k, λ k. A[m0, k] * B[k, n0]);0), k = k0, k < B.rows, n = 0 ⊦ ⟨while n < C.cols do {/* (correctness invariant: n ≤ C.cols ∧ C.rows = A.rows ∧ C.cols = B.cols ∧ (∀ m0, n0. m0 < C.rows ∧ n0 < C.cols → C[m0, n0] = (C`)[m0, n0] + (m0 = m ∧ n0 < n ⊃ A[m0, k] * B[k, n0];0)) wfbound: C.cols - n) */; C[m, n] := C[m, n] + A[m, k] * B[k, n]; n := n + 1}⟩ ⟨k := k + 1⟩ ( ( k ≤ B.rows ∧ C.rows = A.rows ∧ C.cols = B.cols ∧ (∀ m0, n0. m0 < C.rows ∧ n0 < C.cols → C[m0, n0] = C2[m0, n0] + (m0 = m ∧ n0 < C.cols ⊃ Σ(k, λ k. A[m0, k] * B[k, n0]);0))) ∧ B.rows - k < B.rows - k0)