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: |
|---|---|---|
| encode-def | ⊦ encode(m, n) = ((m + n) * (m + n + 1)) / 2 + n | An Axiom |
| dec-fst | ⊦ m.1 = maxenc(m) - m.2 | An Axiom |
| dec-snd | ⊦ m.2 = m - (maxenc(m) * (maxenc(m) + 1)) / 2 | An Axiom |
| maxi-start | ⊦ maxenc(n) = maxenc(0, n) | An Axiom |
| maxi-rec | ⊦ ((m + 1) * (m + 2)) / 2 ≤ n → maxenc(m, n) = maxenc(m + 1, n) | An Axiom |
| maxi-found | ⊦ ¬ ((m + 1) * (m + 2)) / 2 ≤ n → maxenc(m, n) = m | An Axiom |
| enc-invert | ⊦ encode(m.1, m.2) = m | A User Theorem |
| encode-zero | ⊦ encode(m, n) = 0 ↔ m = 0 ∧ n = 0 | A User Theorem |
| encode-zero-01 | ⊦ encode(0, 0) = 0 | A User Theorem |
| exencode | ⊦ ∃ m, n. encode(m, n) = n0 | A User Theorem |
| fst-def | ⊦ encode(m, n).1 = m | A User Theorem |
| fst-ls | ⊦ m.1 ≤ m | A User Theorem |
| fst-ls-01 | ⊦ m.1 < m ↔ m ≠ 0 ∧ m ≠ 1 | A User Theorem |
| fst-nle | m0 ≠ 0, m0 ≠ 1 ⊦ n + m * (* m0) ≤ m.1 ↔ m = 0 ∧ n = 0 | A User Theorem |
| fst-one | ⊦ 1.1 = 1 | A User Theorem |
| fst-zero | ⊦ 0.1 = 0 | A User Theorem |
| injectivity | ⊦ encode(m, n) = encode(m0, n0) ↔ m = m0 ∧ n = n0 | A User Theorem |
| max-bigger | ⊦ m ≤ maxenc(m, n) | A User Theorem |
| max-def | ⊦ (n * (n + 1)) / 2 ≤ m ∧ m < ((n + 1) * (n + 2)) / 2 ∧ (m0 * (m0 + 1)) / 2 ≤ m → maxenc(m0, m) = n | A User Theorem |
| max-def-01 | ⊦ (n * (n + 1)) / 2 ≤ m ∧ m < ((n + 1) * (n + 2)) / 2 → maxenc(m) = n | A User Theorem |
| max-le | ⊦ maxenc(m) ≤ m | A User Theorem |
| max-nls | ⊦ ¬ m < (maxenc(m) * maxenc(m) + maxenc(m)) / 2 | A User Theorem |
| max-one | ⊦ maxenc(1) = 1 | A User Theorem |
| max-rev | ⊦ maxenc(m0, m) = n ∧ (m0 * (m0 + 1)) / 2 ≤ m → (n * (n + 1)) / 2 ≤ m ∧ m < ((n + 1) * (n + 2)) / 2 | A User Theorem |
| max-rev-01 | ⊦ maxenc(m) = n → (n * (n + 1)) / 2 ≤ m ∧ m < ((n + 1) * (n + 2)) / 2 | A User Theorem |
| max-size | ⊦ (maxenc(m) * (maxenc(m) + 1)) / 2 ≤ m ∧ m < ((maxenc(m) + 1) * (maxenc(m) + 2)) / 2 | A User Theorem |
| max-size-01 | ⊦ maxenc(m) * (maxenc(m) + 1) ≤ 2 * m ∧ 2 * m < (maxenc(m) + 1) * (maxenc(m) + 2) | A User Theorem |
| max-snd-le | ⊦ m.2 ≤ maxenc(m) | A User Theorem |
| max-snd-nle | ⊦ m ≠ 0 ∧ m ≠ 1 → ¬ m + m.2 ≤ maxenc(m) | A User Theorem |
| max-snd-nls | ⊦ ¬ maxenc(m) < m.2 | A User Theorem |
| max-square | ⊦ maxenc(((m + n) * (m + n + 1)) / 2 + n) = m + n | A User Theorem |
| max-two | ⊦ maxenc(2) = 1 | A User Theorem |
| max-zero | ⊦ maxenc(m) = 0 ↔ m = 0 | A User Theorem |
| max-zero-01 | ⊦ maxenc(m) = 1 ↔ m = 1 ∨ m = 2 | A User Theorem |
| max-zero-02 | ⊦ maxenc(0) = 0 | A User Theorem |
| snd-def | ⊦ encode(m, n).2 = n | A User Theorem |
| snd-eq | ⊦ m.2 = m ↔ m = 0 | A User Theorem |
| snd-le | ⊦ m.2 ≤ m | A User Theorem |
| snd-ls | ⊦ m.2 < m ↔ m ≠ 0 | A User Theorem |
| snd-nle | m0 ≠ 0 ⊦ n + m * (* m0) ≤ m.2 ↔ m = 0 ∧ n = 0 | A User Theorem |
| snd-one | ⊦ 1.2 = 0 | A User Theorem |
| snd-zero | ⊦ 0.2 = 0 | A User Theorem |