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: |
|---|---|---|
| hasS-none | ⊦ ¬ hasS(none) | An Axiom |
| hasS-some | ⊦ hasS(some(t)) ↔ hasS(t) | An Axiom |
| hasS-K | ⊦ ¬ hasS(K) | An Axiom |
| hasS-S | ⊦ hasS(S) | An Axiom |
| hasS-A | ⊦ hasS(t _ t0) ↔ hasS(t) ∨ hasS(t0) | An Axiom |
| size-some | ⊦ #(some(t)) = #(t) | An Axiom |
| size-none | ⊦ #(none) = 0 | An Axiom |
| ks-rec | ⊦ ks(n + 1) = ks(n) _ K | An Axiom |
| ks-zero | ⊦ ks(0) = K | An Axiom |
| ks-K | ⊦ ks(n) = K _ t1 _ t2 ↔ t1 = K ∧ t2 = K ∧ n = 2 | A User Theorem |
| ks-K-01 | ⊦ ks(n) = K _ t1 ↔ t1 = K ∧ n = 1 | A User Theorem |
| ks-K-02 | ⊦ ks(n) = K ↔ n = 0 | A User Theorem |
| ks-not-S | ⊦ ks(n) ≠ S _ t1 _ t2 _ t3 | A User Theorem |
| ks-not-S-01 | ⊦ ks(n) ≠ S _ t1 _ t2 | A User Theorem |
| ks-not-S-02 | ⊦ ks(n) ≠ S | A User Theorem |
| ks-not-hasS | ⊦ ¬ hasS(ks(n)) | A User Theorem |
| ks-rec-01 | ⊦ n ≠ 0 → ks(n) = ks(n -1) _ K | A User Theorem |