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: |
|---|---|---|
| one-step-red-def | ⊦ t => t' ↔ (∃ C. (∃ v1, v2. t = C[K _ v1 _ v2] ∧ t' = C[v1] ∧ value(v1) ∧ value(v2) ∧ context(C)) ∨ (∃ v1, v2, v3. t = C[S _ v1 _ v2 _ v3] ∧ t' = C[v1 _ v3 _ (v2 _ v3)] ∧ value(v1) ∧ value(v2) ∧ value(v3) ∧ context(C))) | An Axiom |
| it-base | ⊦ (R ^ 0)(t, t') ↔ t = t' | An Axiom |
| it-rec | ⊦ (R ^ (n + 1))(t, t') ↔ (∃ t1. R(t, t1) ∧ (R ^ n)(t1, t')) | An Axiom |
| reduce-def | ⊦ t =>* t' ↔ (∃ n. (=> ^ n)(t, t')) | An Axiom |
| topred-def | ⊦ t =>top t' ↔ (∃ v1, v2. t = K _ v1 _ v2 ∧ t' = v1 ∧ value(v1) ∧ value(v2)) ∨ (∃ v1, v2, v3. t = S _ v1 _ v2 _ v3 ∧ t' = v1 _ v3 _ (v2 _ v3) ∧ value(v1) ∧ value(v2) ∧ value(v3)) | An Axiom |
| irred-def | ⊦ irred(t) ↔ ¬ (∃ t'. t => t') | An Axiom |
| K-does-not-reduce | ⊦ ¬ K => t | A User Theorem |
| K-does-not-top-reduce | ⊦ ¬ K =>top t | A User Theorem |
| K-reduce | ⊦ value(v) ∧ value(v0) → K _ v _ v0 => v | A User Theorem |
| K-top-reduce | ⊦ value(v) ∧ value(v0) → K _ v _ v0 =>top v | A User Theorem |
| S-does-not-reduce | ⊦ ¬ S => t | A User Theorem |
| S-does-not-top-reduce | ⊦ ¬ S =>top t | A User Theorem |
| S-reduce | ⊦ value(v1) ∧ value(v2) ∧ value(v3) → S _ v1 _ v2 _ v3 => v1 _ v3 _ (v2 _ v3) | A User Theorem |
| S-top-reduce | ⊦ value(v1) ∧ value(v2) ∧ value(v3) → S _ v1 _ v2 _ v3 =>top v1 _ v3 _ (v2 _ v3) | A User Theorem |
| fun-reduces-imp-app-reduces | ⊦ t => t' → (¬ t _ t1 => t' _ t1 ↔ false) | A User Theorem |
| fun-value-and-arg-reduces-imp-app-reduces | ⊦ t => t' ∧ value(t1) → (¬ t1 _ t => t1 _ t' ↔ false) | A User Theorem |
| irred-no-step | ⊦ irred(t) → ¬ t => t0 | A User Theorem |
| irred-no-step-01 | ⊦ irred(t1 _ t2) → ¬ t1 => t | A User Theorem |
| irred-no-step-02 | ⊦ irred(t1 _ t2) ∧ value(t1) → ¬ t2 => t | A User Theorem |
| irred-top | ⊦ t1 _ t2 => t' ∧ irred(t2) ∧ value(t1) ∧ irred(t1) → t1 _ t2 =>top t' | A User Theorem |
| irred-top-01 | ⊦ t1 _ t2 => t' ∧ irred(t1) ∧ ¬ value(t1) → t1 _ t2 =>top t' | A User Theorem |
| it-rec-01 | ⊦ n ≠ 0 → ((R ^ n)(t, t') ↔ (∃ t1. R(t, t1) ∧ (R ^ n -1)(t1, t'))) | A User Theorem |
| no-ap-irred | ⊦ ¬ ap(t) → (¬ irred(t) ↔ false) | A User Theorem |
| reduce-no-ap | ⊦ ¬ ap(t) → ¬ t => t' | A User Theorem |
| reduce-topreduce | ⊦ t =>top t1 → (¬ t => t1 ↔ false) | A User Theorem |
| reduce-unique | ⊦ t => t1 ∧ t => t2 → t1 = t2 | A User Theorem |
| reduction-is-reflexive | ⊦ t =>* t | A User Theorem |
| reduction-is-topred-in-ctxt | ⊦ t => t' ↔ (∃ C, t0, t1. context(C) ∧ t = C[t0] ∧ t0 =>top t1 ∧ t' = C[t1]) | A User Theorem |
| topred-unique | ⊦ t =>top t1 ∧ t =>top t2 → t1 = t2 | A User Theorem |