This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| multiply | multiply(A, B; C) {C := A.rows × B.cols; let m = 0 in while m < C.rows do {/* (correctness invariant: m ≤ C.rows ∧ 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 < C.cols ⊃ Σ(B.rows, λ k. A[m0, k] * B[k, n0]);0)) wfbound: C.rows - m) */; let k = 0 in while k < B.rows do {/* (correctness invariant: k ≤ B.rows ∧ 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 < C.cols ⊃ Σ(k, λ k. A[m0, k] * B[k, n0]);0)) wfbound: B.rows - k) */; 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}; m := m + 1} } | An Axiom |
| correctness | A.cols = B.rows ⊦ ⟨multiply(A, B; C)⟩ (C = A * B) | A User Theorem |
| prove-ext | ⊦ A ≠ B ↔ ¬(A.rows = B.rows ∧ A.cols = B.cols ∧ (∀ m, n. m < A.rows ∧ n < A.cols → A[m, n] = B[m, n])) | A User Theorem |