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: |
|---|---|---|
| subst-O | ⊦ O[t] = t | An Axiom |
| subst-Cfun | ⊦ (C _ t1)[t] = C[t] _ t1 | An Axiom |
| subst-Carg | ⊦ (t1 _ C)[t] = t1 _ C[t] | An Axiom |
| K-is-only-OK | ⊦ K = C[t] ↔ t = K ∧ C = O | A User Theorem |
| S-is-only-OS | ⊦ S = C[t] ↔ t = S ∧ C = O | A User Theorem |
| ap-in-context-is-ap | ⊦ ap(C[t _ t1]) | A User Theorem |
| not-value | ⊦ ¬ value(C[K _ t _ t0]) | A User Theorem |
| not-value-01 | ⊦ ¬ value(t1 _ C[K _ t _ t0]) | A User Theorem |
| not-value-02 | ⊦ ¬ value(C[S _ t _ t0 _ t1]) | A User Theorem |
| subst-KK-equal | C[K _ v1 _ v2] = C0[K _ v _ v0], value(v1), value(v2), value(v), value(v0), context(C0), context(C) ⊦ C[v1] = C0[v] | A User Theorem |
| subst-SK-equal | C[S _ v3 _ v4 _ v5] = C0[K _ v _ v0], value(v3), value(v4), value(v5), value(v), value(v0), context(C0), context(C) ⊦ C[v3 _ v5 _ (v4 _ v5)] = C0[v] | A User Theorem |
| subst-SS-equal | C[S _ v4 _ v5 _ v6] = C0[S _ v1 _ v2 _ v3], value(v4), value(v5), value(v6), value(v1), value(v2), value(v3), context(C0), context(C) ⊦ C[v4 _ v6 _ (v5 _ v6)] = C0[v1 _ v3 _ (v2 _ v3)] | A User Theorem |
| substap-is-not-K | ⊦ C[t _ t0] ≠ K | A User Theorem |
| substap-is-not-S | ⊦ C[t _ t0] ≠ S | A User Theorem |
| value-context | ⊦ context(C) ∧ value(C[t]) → (¬ value(t) ↔ false) | A User Theorem |