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: |
|---|---|---|
| disj | ⊦ ⌜m⌝ ≠ ∞ | An Axiom |
| sel | ⊦ ⌜m⌝ .n = m | An Axiom |
| inj | ⊦ ⌜m⌝ = ⌜m0⌝ ↔ m = m0 | An Axiom |
| case | ⊦ n∞ = ⌜n∞.n⌝ ∨ n∞ = ∞ | An Axiom |
| elim | ⊦ n∞ ≠ ∞ → (n = n∞.n ↔ n∞ = ⌜n⌝ ) | An Axiom |
| gen | natinf freely generated by ∞, ⌜ ⌝; | An Axiom |
| fin-inject-embed | n∞ ≠ ∞ ⊦ ⌜n∞.n⌝ = n∞ | A User Theorem |
| notinf-fin | ⊦ n∞ ≠ ∞ ↔ (∃ n. n∞ = ⌜n⌝ ) | A User Theorem |
| notinf-fin-sym | ⊦ ∞ ≠ n∞ ↔ (∃ n. n∞ = ⌜n⌝ ) | A User Theorem |