| m0 = m, C4[m0, n] = C2[m0, n] + Σ(k, λ k. A[m, k] * B[k, n]), C3.cols = B.cols, C3.rows = A.rows, C4.cols = B.cols, C4.rows = A.rows, C2.cols = B.cols, C2.rows = A.rows, A.cols = B.rows, n < B.cols, m0 < A.rows, n1 < B.cols, k < B.rows, m < A.rows, ∀ m0, n. m0 < A.rows ∧ n < B.cols → C4[m0, n] = C2[m0, n] + (m0 = m ⊃ Σ(k, λ k. A[m, k] * B[k, n]);0), ∀ m1, n0. m1 < A.rows ∧ n0 < B.cols → C2[m1, n0] = (m1 < m ⊃ Σ(B.rows, λ k. A[m1, k] * B[k, n0]);0), m0 ≠ m ∨ n1 < n, m0 ≠ m ∨ n ≠ n1, ∀ m0, n. m0 < A.rows ∧ n < B.cols → C3[m0, n] = C4[m0, n] + (m0 = m ∧ n < n1 ⊃ A[m, k] * B[k, n];0) ⊦ B.cols = 0, A.rows = 0, B.rows = 0, C3[m0, n] = C4[m0, n] |
C4[m, n] = C2[m, n] + Σ(k, λ k. A[m, k] * B[k, n]), C3.cols = B.cols, C3.rows = A.rows, C4.cols = B.cols, C4.rows = A.rows, C2.cols = B.cols, C2.rows = A.rows, A.cols = B.rows, n1 + 1 < B.cols, n < B.cols, k < B.rows, m < A.rows, n1 < n, n1 < B.cols, ∀ m0, n. m0 < A.rows ∧ n < B.cols → C3[m0, n] = C4[m0, n] + (m0 = m ∧ n < n1 ⊃ A[m, k] * B[k, n];0), ∀ m0, n. m0 < A.rows ∧ n < B.cols → C4[m0, n] = C2[m0, n] + (m0 = m ⊃ Σ(k, λ k. A[m, k] * B[k, n]);0), ∀ m1, n0. m1 < A.rows ∧ n0 < B.cols → C2[m1, n0] = (m1 < m ⊃ Σ(B.rows, λ k. A[m1, k] * B[k, n0]);0) ⊦ B.cols = 0, A.rows = 0, B.rows = 0, C3[m, n] = C4[m, n], n = n1, n = 0
Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic1%succ: ⊦ m +1 = m + 1; from specification nat-basic2%trans-1: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic1%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic1%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic1