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: |
|---|---|---|
| sub-base | ⊦ m - 0 = m | An Axiom |
| sub-rec | ⊦ m - n +1 = (m - n)-1 | An Axiom |
| le-def | ⊦ m ≤ n ↔ ¬ n < m | An Axiom |
| gr-def | ⊦ m > n ↔ n < m | An Axiom |
| ge-def | ⊦ m ≥ n ↔ ¬ m < n | An Axiom |
| add | ⊦ n ≤ m → ((m - n) + n0 = m ↔ n = n0) | A User Theorem |
| add-01 | ⊦ n ≤ m → m + n0 - n = (m - n) + n0 | A User Theorem |
| add-02 | ⊦ 1 + m + m ≤ n + n ↔ m < n | A User Theorem |
| add-03 | ⊦ n ≤ n0 → m + n0 - n = m + (n0 - n) | A User Theorem |
| add-le-right2-ls | m ≤ m0 + n0, n0 < n1 ⊦ m < m0 + n1 | A User Theorem |
| add-ls-right2-le | m < m0 + n0, n0 ≤ n1 ⊦ m < m0 + n1 | A User Theorem |
| add-num-01 | n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n) | A User Theorem |
| add-num-02 | n0 < n ⊦ m + (* n) = m0 + (* n0) ↔ m + (n - n0) = m0 | A User Theorem |
| add-num-03 | n < n0 ⊦ (* n) ≠ m0 + (* n0) | A User Theorem |
| add-num-04 | n0 < n ⊦ (* n) = m0 + (* n0) ↔ n - n0 = m0 | A User Theorem |
| add-sub-less | ⊦ m ≤ n ∧ n0 ≤ m → (n - m) + n0 = n - (m - n0) | A User Theorem |
| anti | ⊦ m ≤ n → (n ≤ m ↔ m = n) | A User Theorem |
| cancel-01 | ⊦ m + n - n + n1 = m - n1 | A User Theorem |
| elim-pred-c | n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1 | A User Theorem |
| elim-sub | n ≤ m ⊦ n0 = m - n ↔ m = n0 + n | A User Theorem |
| eq | ⊦ m = n + 1 → ¬ m ≤ n | A User Theorem |
| eq-01 | ⊦ m + n - m = n | A User Theorem |
| eq-02 | n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1 | A User Theorem |
| eq-03 | ⊦ m + 1 = n → n - m = 1 | A User Theorem |
| eq-add2n-1-eq-le | ⊦ n = n0 + n1 + 1 ∧ n0 + n1 = m0 + m1 → (n < m0 ↔ false) | A User Theorem |
| eq-pred | ⊦ m = m0 ∧ m0 = n + 1 → m - n - 1 = 0 | A User Theorem |
| eq-pred-01 | ⊦ m = n + 1 → m - n - 1 = 0 | A User Theorem |
| eqle-one | ⊦ m = n + 1 ∧ n < n0 → m ≤ n0 | A User Theorem |
| fle | ⊦ m < n ∧ n ≤ n0 → m < n0 | A User Theorem |
| fle-01 | ⊦ m ≤ n ∧ n < n0 → m < n0 | A User Theorem |
| ge | ⊦ n ≥ m ↔ m ≤ n | A User Theorem |
| l-num-01 | n < n0 ⊦ m + (* n) < m0 + (* n0) ↔ m < m0 + (n0 - n) | A User Theorem |
| l-num-02 | n0 < n ⊦ m + (* n) < m0 + (* n0) ↔ m + (n - n0) < m0 | A User Theorem |
| l-num-03 | n < n0 ⊦ (* n) < m0 + (* n0) | A User Theorem |
| l-num-04 | n0 < n ⊦ (* n) < m0 + (* n0) ↔ n - n0 < m0 | A User Theorem |
| l-num-05 | n < n0 ⊦ m + (* n) < (* n0) ↔ m < n0 - n | A User Theorem |
| l-num-06 | n0 < n ⊦ ¬ m + (* n) < (* n0) | A User Theorem |
| le | n ≤ m ⊦ (m - n) + m0 ≤ n0 ↔ m + m0 ≤ n0 + n | A User Theorem |
| le-add | ⊦ m + m0 ≤ m ↔ m0 = 0 | A User Theorem |
| le-add-01 | ⊦ n < m ∧ n0 < m0 → (¬ ¬ m + m0 ≤ n + n0 ↔ false) | A User Theorem |
| le-add-02 | ⊦ n < m ∧ n0 < m0 → (¬ ¬ m + m0 ≤ n + n0 + 1 ↔ false) | A User Theorem |
| le-addex | ⊦ m ≤ n ↔ (∃ n0. m + n0 = n) | A User Theorem |
| le-ls-simp | ⊦ m ≤ n → (n < m ↔ false) | A User Theorem |
| le-num-01 | n < n0 ⊦ m + (* n) ≤ m0 + (* n0) ↔ m ≤ m0 + (n0 - n) | A User Theorem |
| le-num-02 | n0 < n ⊦ m + (* n) ≤ m0 + (* n0) ↔ m + (n - n0) ≤ m0 | A User Theorem |
| le-num-03 | n < n0 ⊦ (* n) ≤ m0 + (* n0) | A User Theorem |
| le-num-04 | n0 < n ⊦ (* n) ≤ m0 + (* n0) ↔ n - n0 ≤ m0 | A User Theorem |
| le-num-05 | n < n0 ⊦ m + (* n) ≤ (* n0) ↔ m ≤ n0 - n | A User Theorem |
| le-num-06 | n0 < n ⊦ ¬ m + (* n) ≤ (* n0) | A User Theorem |
| le-one | ⊦ m ≤ n + 1 ∧ n < n0 → m ≤ n0 | A User Theorem |
| le-rec | ⊦ n ≠ 0 → (m ≤ n ↔ m = n ∨ m < n) | A User Theorem |
| le-sum | ⊦ n ≤ n0 ∧ n1 ≤ m → n + n1 ≤ n0 + m | A User Theorem |
| lels | ⊦ ¬ m < n ↔ n ≤ m | A User Theorem |
| lels-01 | ⊦ ¬ m ≤ n ↔ n < m | A User Theorem |
| lels-02 | ⊦ m ≠ n → (m ≤ n ↔ m < n) | A User Theorem |
| lels-03 | ⊦ m < n → m ≤ n | A User Theorem |
| lels-04 | ⊦ n + m ≤ m0 → ¬ n0 + m0 < m | A User Theorem |
| lep | ⊦ m ≤ m + n | A User Theorem |
| lep-01 | ⊦ m + n ≤ m ↔ n = 0 | A User Theorem |
| lep-02 | ⊦ m + n ≤ m + n0 ↔ n ≤ n0 | A User Theorem |
| lepr | ⊦ m ≠ 0 → ¬ m ≤ m - 1 | A User Theorem |
| leprf | ⊦ m ≤ m - 1 → m = 0 | A User Theorem |
| ler | ⊦ m ≤ m | A User Theorem |
| les | ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1) | A User Theorem |
| less | n ≤ m, n1 < n ⊦ (m - n) + n0 + n1 < m + n0 | A User Theorem |
| less-01 | n ≤ m, n1 ≤ n ⊦ (m - n) + n0 + n1 ≤ m + n0 | A User Theorem |
| less-02 | n ≤ m, n0 < n ⊦ (m - n) + n0 < m | A User Theorem |
| less-03 | ⊦ m - n0 < m - n1 ∧ n0 ≤ m ∧ n1 ≤ m → n1 < n0 | A User Theorem |
| let | ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1 | A User Theorem |
| lez | ⊦ 0 ≤ m | A User Theorem |
| lez-01 | ⊦ m ≤ 0 ↔ m = 0 | A User Theorem |
| ls | n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n | A User Theorem |
| ls-01 | n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0 | A User Theorem |
| ls-02 | n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n | A User Theorem |
| ls-03 | n0 ≤ n ⊦ n - n0 ≤ m ↔ n ≤ m + n0 | A User Theorem |
| ls-04 | ⊦ n ≤ m ∧ n0 ≤ m → (m - n < m - n0 ↔ n0 < n) | A User Theorem |
| ls-05 | ⊦ n < m → 0 < m - n | A User Theorem |
| ls-06 | ⊦ n ≤ m → (m - n < m ↔ n ≠ 0) | A User Theorem |
| ls-07 | n ≤ m, n0 ≤ m ⊦ m - n < m - n0 ↔ n0 < n | A User Theorem |
| ls-add-not | ⊦ m ≤ m0 ∧ n ≤ n0 → ¬ m0 + n0 + n1 < m + n | A User Theorem |
| ls-add-not-01 | ⊦ m ≤ m0 ∧ n ≤ n0 → ¬ m0 + n0 < m + n | A User Theorem |
| ls-add-not-02 | ⊦ m ≤ m0 ∧ n ≤ n0 ∧ m1 ≤ n1 → ¬ m0 + n0 + n1 + n2 < m + n + m1 | A User Theorem |
| ls-add-not-03 | ⊦ m ≤ m0 ∧ n ≤ n0 ∧ m1 ≤ n1 → ¬ m0 + n0 + n1 < m + n + m1 | A User Theorem |
| ls-le-simp | ⊦ m < n → (n ≤ m ↔ false) | A User Theorem |
| ls-pred | ⊦ n + 1 < m → m - n - 1 < m | A User Theorem |
| neq-01 | ⊦ m0 ≤ m ∧ n + m ≤ n0 → n0 + 1 ≠ n + m0 | A User Theorem |
| neq-add1 | ⊦ n0 = n1 + n2 → (n2 = n0 + 1 ↔ false) | A User Theorem |
| not-zero | 0 < n ⊦ (* n) ≤ m → m ≠ 0 | A User Theorem |
| num-01 | ⊦ n + 1 - 1 = n | A User Theorem |
| num-02 | n ≠ 0 ⊦ (n - 1) + 1 = n | A User Theorem |
| one-01 | ⊦ m ≠ 0 → (m + n ≤ 1 ↔ m = 1 ∧ n = 0) | A User Theorem |
| one-02 | ⊦ m ≠ 0 → (m ≤ 1 ↔ m = 1) | A User Theorem |
| pls | m ≤ m0, n < n0 ⊦ m + n < m0 + n0 | A User Theorem |
| pred | ⊦ n < m → m - 1 - n = m - n - 1 | A User Theorem |
| pred-01 | ⊦ n < m → (m - n - 1) + 1 = m - n | A User Theorem |
| pred-02 | m ≠ 0, n ≠ 0, n ≤ m ⊦ m - 1 - (n - 1) = m - n | A User Theorem |
| pred-03 | ⊦ n -1 = n - 1 | A User Theorem |
| prop | n < m ⊦ m - 1 - n = m - n + 1 | A User Theorem |
| prop-01 | n ≤ m ⊦ (m - n) + n = m | A User Theorem |
| prop-02 | n ≤ m ⊦ (m - n) + 1 = m + 1 - n | A User Theorem |
| prop-04 | ⊦ m < m - n → m < n | A User Theorem |
| prop-05 | m ≤ n ⊦ (n - m) + n0 = n + n0 - m | A User Theorem |
| prop-06 | m ≠ 0, m ≤ n + 1 ⊦ n + 1 - m = n - (m - 1) | A User Theorem |
| prop-07 | ⊦ n < m → (m - n) + n = m | A User Theorem |
| rax | ⊦ m - n + 1 = m - n - 1 | A User Theorem |
| rec | n ≤ m ⊦ m + 1 - n = (m - n) + 1 | A User Theorem |
| shift | ⊦ m - n - n0 = m - n0 - n | A User Theorem |
| shift-01 | ⊦ m - n - n0 = m - n + n0 | A User Theorem |
| sub-add | ⊦ n ≤ n0 → (m + (n0 - n)) + n = m + n0 | A User Theorem |
| sub-add-01 | ⊦ n0 ≤ n ∧ n ≤ m + n0 → m - (n - n0) = m + n0 - n | A User Theorem |
| sub-le-rew | m0 ≤ m, n0 ≤ n ⊦ m - m0 ≤ n - n0 ↔ m + n0 ≤ n + m0 | A User Theorem |
| sub-ls | ⊦ ¬ n + (m - n) < m | A User Theorem |
| sub-ls-rew | m0 < m, n0 < n ⊦ m - m0 < n - n0 ↔ m + n0 < n + m0 | A User Theorem |
| sub-same | ⊦ n ≤ m → m - (m - n) = n | A User Theorem |
| sub-succ | ⊦ m0 ≤ n ∧ n ≤ m → m - (n - m0) = (m - n) + m0 | A User Theorem |
| succ | ⊦ n + 1 - n = 1 | A User Theorem |
| succ-01 | ⊦ m + 1 ≤ n ↔ m < n | A User Theorem |
| succ-02 | ⊦ m < n + 1 ↔ m ≤ n | A User Theorem |
| succ-04 | n ≤ m ⊦ m + 1 - n - 1 = m - n | A User Theorem |
| succ-05 | ⊦ n + 1 < m → m - n - 1 ≠ 0 | A User Theorem |
| trans-le-le | m ≤ n, n ≤ n0 ⊦ m ≤ n0 | A User Theorem |
| trans-le-ls | m ≤ n, n < n0 ⊦ m < n0 | A User Theorem |
| trans-ls-le | m < n, n ≤ n0 ⊦ m < n0 | A User Theorem |
| zero | ⊦ m - m = 0 | A User Theorem |
| zero-01 | ⊦ n < m → m - n ≠ 0 | A User Theorem |
| zero-02 | ⊦ m ≤ n → (n - m = 0 ↔ n = m) | A User Theorem |