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: |
|---|---|---|
| decl-01 | An Axiom | |
| decl-03 | An Axiom | |
| decl-04 | An Axiom | |
| SII-def | ⊦ SII = S _ I _ I | An Axiom |
| I-def | ⊦ I = S _ K _ K | An Axiom |
| RED-complete | t =>* t' ∧ irred(t') ⊦ 〈RED(t; t0)〉 t0 = t' | A User Theorem |
| RED-correct | 〈RED(t; t')〉 t' = t1 ⊦ t =>* t1 ∧ irred(t1) | A User Theorem |
| RED-iff-reduce | ⊦ 〈RED(t; t0)〉 t0 = t' ↔ t =>* t' ∧ irred(t') | A User Theorem |
| RED1-lem | ⊦ 〈RED1(t; tn)〉 (tn = none ⊃ irred(t); t => tn .t) | A User Theorem |
| SII-loops | ⊦ ¬ 〈RED(SII _ SII; t0)〉 true | A User Theorem |
| TOPRED-lem | ⊦ 〈TOPRED(t; tn)〉 (tn = none ⊃ ¬ (∃ t0. t =>top t0); t =>top tn .t) | A User Theorem |
| kappa-RED1 | 〈RED1(t; tn)〉 tn = tn0, 〈RED1(t; tn): n 〉 tn = tn1 ⊦ tn0 = tn1 | A User Theorem |
| kappa-TOPRED | 〈TOPRED(t; tn)〉 tn = tn0, 〈TOPRED(t; tn): n 〉 tn = tn1 ⊦ tn0 = tn1 | A User Theorem |
| ks-RED | ⊦ 〈RED(ks(n); t)〉 ((even(n) → t = K) ∧ (odd(n) → t = K _ K)) | A User Theorem |
| ks-RED1 | ⊦ 〈RED1(ks(n); tn)〉 ((tn = none → n ≤ 1) ∧ (tn ≠ none → ¬ n ≤ 1 ∧ tn = some(ks(n - 2)))) | A User Theorem |
| ks-TOPRED | ⊦ 〈TOPRED(ks(n); tn)〉 (tn ≠ none → n = 2 ∧ tn = some(K)) | A User Theorem |
| termination-RED | ¬ hasS(t) ⊦ 〈RED(t; t')〉 true | A User Theorem |
| termination-RED1 | ¬ hasS(t) ⊦ 〈RED1(t; tn)〉 (tn ≠ none → ¬ hasS(tn) ∧ #(tn) < #(t)) | A User Theorem |
| termination-TOPRED | ¬ hasS(t) ⊦ 〈TOPRED(t; tn)〉 (tn ≠ none → ¬ hasS(tn) ∧ #(tn) < #(t)) | A User Theorem |