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: |
|---|---|---|
| val-K | ⊦ value(K) | An Axiom |
| val-S | ⊦ value(S) | An Axiom |
| val-K-ap | ⊦ value(K _ t) ↔ value(t) | An Axiom |
| val-S-ap | ⊦ value(S _ t) ↔ value(t) | An Axiom |
| val-other-ap | ⊦ t1 ≠ K ∧ t1 ≠ S → (value(t1 _ t2) ↔ ¬ ¬ (ap(t1) ∧ t1 .1 = S ∧ value(t2) ∧ value(t1 .2))) | An Axiom |
| value | ⊦ value(S _ K _ K) | A User Theorem |
| value-01 | ⊦ value(S _ (S _ K _ K) _ (S _ K _ K)) | A User Theorem |
| value-02 | ⊦ ¬ value(S _ K _ K _ (S _ (S _ K _ K) _ (S _ K _ K))) | A User Theorem |
| value-03 | ⊦ ¬ value(K _ (S _ (S _ K _ K) _ (S _ K _ K)) _ (K _ (S _ (S _ K _ K) _ (S _ K _ K)))) | A User Theorem |
| value-04 | ⊦ ¬ value(S _ K _ K _ (K _ (S _ (S _ K _ K) _ (S _ K _ K)) _ (K _ (S _ (S _ K _ K) _ (S _ K _ K))))) | A User Theorem |