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: |
|---|---|---|
| dec-snd | ⊦ i.2 = decode(decode(i).2) | An Axiom |
| dec-fst | ⊦ i.1 = decode(decode(i).1) | An Axiom |
| dec-nat-neg | ⊦ i < 0 → decode(i) = 2 * i→n(i) - 1 | An Axiom |
| dec-nat-pos | ⊦ 0 ≤ i → decode(i) = 2 * i→n(i) | An Axiom |
| dec-int-neg | ⊦ n % 2 ≠ 0 → decode(n) = ~ n→i((n + 1) / 2) | An Axiom |
| dec-int-pos | ⊦ n % 2 = 0 → decode(n) = n→i(n / 2) | An Axiom |
| encode-pair | ⊦ i × j = encode(encode(encode(i), encode(j))) | An Axiom |
| enc-nat-neg | ⊦ n % 2 ≠ 0 → encode(n) = ~ n→i((n + 1) / 2) | An Axiom |
| enc-nat-pos | ⊦ n % 2 = 0 → encode(n) = n→i(n / 2) | An Axiom |
| enc-int-neg | ⊦ i < 0 → encode(i) = 2 * i→n(i) - 1 | An Axiom |
| enc-int-pos | ⊦ 0 ≤ i → encode(i) = 2 * i→n(i) | An Axiom |
| dec-int | ⊦ decode(encode(i)) = i | A User Theorem |
| dec-int-01 | ⊦ encode(decode(i)) = i | A User Theorem |
| dec-nat | ⊦ decode(encode(n)) = n | A User Theorem |
| dec-nat-01 | ⊦ encode(decode(n)) = n | A User Theorem |
| enc-invert | ⊦ i.1 × i.2 = i | A User Theorem |
| enc-zero | ⊦ i × j = 0 ↔ ¬ ¬(i = 0 ∧ j = 0) | A User Theorem |
| enc-zero-01 | ⊦ encode(i) = 0 ↔ i = 0 | A User Theorem |
| enc-zero-02 | ⊦ encode(n) = 0 ↔ n = 0 | A User Theorem |
| exencode | ⊦ ∃ i, j. i × j = i0 | A User Theorem |
| injectivity | ⊦ i × j = i0 × j0 ↔ i = i0 ∧ j = j0 | A User Theorem |
| injectivity-01 | ⊦ encode(m) = encode(n) ↔ m = n | A User Theorem |
| injectivity-02 | ⊦ encode(i) = encode(j) ↔ i = j | A User Theorem |
| sel-fst | ⊦ (i × j).1 = i | A User Theorem |
| sel-snd | ⊦ (i × j).2 = j | A User Theorem |