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: |
|---|---|---|
| at-dot | ⊦ A.cols = B.rows → (A * B)[m, n] = Σ(A.cols, λ k. A[m, k] * B[k, n]) | An Axiom |
| sum-base | ⊦ Σ(0, nf) = 0 | An Axiom |
| sum-rec | ⊦ Σ(n + 1, nf) = nf(n) + Σ(n, nf) | An Axiom |
| cols-dot | ⊦ A.cols = B.rows → (A * B).cols = B.cols | An Axiom |
| rows-dot | ⊦ A.cols = B.rows → (A * B).rows = A.rows | An Axiom |
| dist | ⊦ i * Σ(n, nf) = Σ(n, λ k. i * nf(k)) | A User Theorem |
| dot-assoc | ⊦ A.cols = B.rows ∧ B.cols = C.rows → (A * B) * C = A * B * C | A User Theorem |
| sum-empty | ⊦ Σ(n, λ k. 0) = 0 | A User Theorem |
| sum-split | ⊦ Σ(n, λ k. nf0(k) + nf1(k)) = Σ(n, nf0) + Σ(n, nf1) | A User Theorem |
| sum-swap | ⊦ Σ(n, λ k0. Σ(m, λ k1. nnf(k0, k1))) = Σ(m, λ k1. Σ(n, λ k0. nnf(k0, k1))) | A User Theorem |