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: |
|---|---|---|
| Pot2-zero | ⊦ 2^ 0 = 1 | An Axiom |
| Pot2-succ | ⊦ 2^ n +1 = 2 * 2^ n | An Axiom |
| Log2def | ⊦ 2^ m ≤ n ∧ n < 2^ m +1 → log2 n = m | An Axiom |
| Logdef | ⊦ m ^ n0 ≤ n ∧ n < m ^ n0 +1 → log(m, n) = n0 | An Axiom |
| Pot-succ | ⊦ n ^ m +1 = n ^ m * n | An Axiom |
| Pot-zero | ⊦ n ^ 0 = 1 | An Axiom |
| 2-pot-mod | ⊦ m ≠ 0 → 2 ^ m % 2 = 0 | A User Theorem |
| 2-pot-mod-01 | ⊦ 2 ^ m ≠ 1 → 2 ^ m % 2 = 0 | A User Theorem |
| add | ⊦ m ^ (n + n0) = m ^ n * m ^ n0 | A User Theorem |
| div-eq-zero | m0 ≠ 0 ⊦ n0 / m0 = 0 ↔ n0 < m0 | A User Theorem |
| inj | ⊦ 2^ n = 2^ m ↔ n = m | A User Theorem |
| inj-02 | ⊦ 2^ n = 2 * 2^ m ↔ n = m + 1 | A User Theorem |
| ladd | m ≠ 0 ⊦ ¬ log2(m + n) < log2 m | A User Theorem |
| ladd-01 | n ≠ 0 ⊦ m = n + n0 → ¬ log2 m < log2 n | A User Theorem |
| lemma-ax2 | ⊦ 2^(n + 1) = 2 * 2^ n | A User Theorem |
| lls | ⊦ n ≠ 0 → ¬ n < 2^ log2 n | A User Theorem |
| lls-01 | ⊦ n < 2^(log2 n + 1) | A User Theorem |
| lls-02 | n ≠ 0 ⊦ log2 m < log2 n → m < n | A User Theorem |
| lone | ⊦ log2 1 = 0 | A User Theorem |
| lpot | ⊦ log2 2^ n = n | A User Theorem |
| lsucc-01 | ⊦ n ≠ 0 → log2(2 * n + 1) = log2 n + 1 | A User Theorem |
| ltwo-03 | ⊦ n ≠ 0 → log2(2 * n) = log2 n + 1 | A User Theorem |
| ltwo-04 | ⊦ log2 2 = 1 | A User Theorem |
| ltwo-05 | ⊦ n < 2 * 2^ log2 n | A User Theorem |
| lzer | ⊦ log2(m + 1) = 0 ↔ m = 0 | A User Theorem |
| mult | ⊦ (m * m0) ^ n = m ^ n * m0 ^ n | A User Theorem |
| one | ⊦ 2^ m = 1 ↔ m = 0 | A User Theorem |
| one-01 | ⊦ 2^ 1 = 2 | A User Theorem |
| one-01-01 | ⊦ m ^ 1 = m | A User Theorem |
| one-02 | ⊦ 0 ^ 1 = 0 | A User Theorem |
| pot-01 | n ≠ 0 ⊦ 2 * 2^ n -1 = 2^ n | A User Theorem |
| pot-mon | 1 < m ⊦ m ^ n < m ^ n0 ↔ n < n0 | A User Theorem |
| pot-two | ⊦ m ^ 2 = m * m | A User Theorem |
| pot-zero | ⊦ m ≠ 0 → m ^ n ≠ 0 | A User Theorem |
| pot-zero-01 | ⊦ n ≠ 0 → 0 ^ n = 0 | A User Theorem |
| pot2-add | ⊦ 2^(m + n) = 2^ m * 2^ n | A User Theorem |
| pot2-def | ⊦ 2^ m = 2 ^ m | A User Theorem |
| potex | n ≠ 0 ⊦ ∃ m. 2^ m ≤ n ∧ n < 2^(m + 1) | A User Theorem |
| potmon | ⊦ 2^ m < 2^ n ↔ m < n | A User Theorem |
| potmonleq | ⊦ 2^ m ≤ 2^ n ↔ m ≤ n | A User Theorem |
| power-of-2 | ⊦ 2 ^ m ≠ 1 → 2 * 2 ^ m / 2 = 2 ^ m | A User Theorem |
| power-of-2-01 | ⊦ 2 ^ m ≠ 1 → 4 * 2 ^ m / 2 * n = 2 * n * 2 ^ m | A User Theorem |
| rec | ⊦ 2^(n + 1) = 2^ n + 2^ n | A User Theorem |
| rec-01 | ⊦ n ^ (m + 1) = n ^ m * n | A User Theorem |
| succ-02 | ⊦ 2 * 2^ m = 2^(m + 1) | A User Theorem |
| succ-03 | ⊦ 2^ m = 2 * n + 1 ↔ m = 0 ∧ n = 0 | A User Theorem |
| two | ⊦ m ^ (2 * n) = m ^ n * m ^ n | A User Theorem |
| two-pot-zero | ⊦ 2 ^ n ≠ 0 | A User Theorem |
| zero | ⊦ 2^ n ≠ 0 | A User Theorem |
| zero-01 | ⊦ 0 ^ n = 0 ↔ n ≠ 0 | A User Theorem |