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: |
|---|---|---|
| sum-empty | ⊦ Σ [] = 0 | An Axiom |
| sum-rec | ⊦ Σ(n ' + nats) = n + Σ nats | An Axiom |
| prod-empty | ⊦ Π [] = 1 | An Axiom |
| prod-rec | ⊦ Π(n ' + nats) = n * Π nats | An Axiom |
| prod-app | ⊦ Π(nats + nats0) = Π nats * Π nats0 | A User Theorem |
| prod-eq-one | ⊦ Π nats = 1 ∧ m < # nats → nats[m] = 1 | A User Theorem |
| prod-eq-one-01 | ⊦ Π nats = 1 ∧ m ∈ nats → m = 1 | A User Theorem |
| prod-eq-zero | ⊦ Π nats = 0 ↔ 0 ∈ nats | A User Theorem |
| prod-last | ⊦ Π(nats + m ') = m * Π nats | A User Theorem |
| prod-one | ⊦ Π n ' = n | A User Theorem |
| sum-append | ⊦ Σ(nats + nats0) = Σ nats + Σ nats0 | A User Theorem |
| sum-listlength-one | ⊦ Σ n ' = n | A User Theorem |
| sum-zero | ⊦ Σ 0 ' = 0 | A User Theorem |