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-01 | ⊦ t _ t0 ≠ K | An Axiom |
| disj-02 | ⊦ t _ t0 ≠ S | An Axiom |
| disj-03 | ⊦ K ≠ S | An Axiom |
| sel-01 | ⊦ (t _ t0) .2 = t0 | An Axiom |
| sel-02 | ⊦ (t _ t0) .1 = t | An Axiom |
| test-01 | ⊦ ¬ ap(S) | An Axiom |
| test-02 | ⊦ ¬ ap(K) | An Axiom |
| test-03 | ⊦ ap(t _ t0) | An Axiom |
| inj | ⊦ t _ t0 = t1 _ t2 ↔ t = t1 ∧ t0 = t2 | An Axiom |
| case | ⊦ t = t .1 _ t .2 ∨ t = K ∨ t = S | An Axiom |
| size-01 | ⊦ #(S) = 0 | An Axiom |
| size-02 | ⊦ #(K) = 0 | An Axiom |
| size-03 | ⊦ #(t _ t0) = (#(t) + #(t0)) +1 | An Axiom |
| ex | ⊦ ap(t) ↔ (∃ t0, t1. t = t0 _ t1) | An Axiom |
| elim | ⊦ ap(t) → (t0 = t .1 ∧ t1 = t .2 ↔ t = t0 _ t1) | An Axiom |
| gen | An Axiom |