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: |
|---|---|---|
| add-fin | ⊦ ⌜m + n⌝ = ⌜m⌝ + ⌜n⌝ | An Axiom |
| add-inf1 | ⊦ ∞ + ⌜m⌝ = ∞ | An Axiom |
| add-inf2 | ⊦ ⌜m⌝ + ∞ = ∞ | An Axiom |
| add-inf | ⊦ ∞ + ∞ = ∞ | An Axiom |
| less-fin | ⊦ ⌜m⌝ < ⌜n⌝ ↔ m < n | An Axiom |
| less-inf2 | ⊦ ⌜m⌝ < ∞ | An Axiom |
| less-inf1 | ⊦ ¬ ∞ < n∞ | An Axiom |
| min-def | ⊦ min(n∞, n∞0) = (n∞ < n∞0 ⊃ n∞;n∞0) | An Axiom |
| add-all-inf | ⊦ n∞ + ∞ = ∞ | A User Theorem |
| add-all-zero | ⊦ n∞ + ⌜0⌝ = n∞ | A User Theorem |
| add-assoc | ⊦ (n∞ + n∞1) + n∞2 = n∞ + n∞1 + n∞2 | A User Theorem |
| add-cancel-01 | ⊦ ⌜n⌝ + n∞1 = ⌜n⌝ + n∞2 ↔ n∞1 = n∞2 | A User Theorem |
| add-cancel-02 | ⊦ n∞1 = n∞1 + n∞2 ↔ ¬ ¬(n∞1 = ∞ ∨ n∞2 = ⌜0⌝ ) | A User Theorem |
| add-cancel-03 | ⊦ ⌜n⌝ + n∞ = ⌜n⌝ ↔ n∞ = ⌜0⌝ | A User Theorem |
| add-cancel-num-01 | ⊦ m ≤ n → (⌜(* n)⌝ = ⌜(* m)⌝ + n∞2 ↔ ⌜n - m⌝ = n∞2) | A User Theorem |
| add-cancel-num-02 | ⊦ n < m → (⌜(* n)⌝ = ⌜(* m)⌝ + n∞2 ↔ false) | A User Theorem |
| add-cancel-num-03 | ⊦ m ≤ n → (⌜(* n)⌝ + n∞1 = ⌜(* m)⌝ + n∞2 ↔ ⌜n - m⌝ + n∞1 = n∞2) | A User Theorem |
| add-cancel-num-04 | ⊦ n < m → (⌜(* n)⌝ + n∞1 = ⌜(* m)⌝ + n∞2 ↔ n∞1 = ⌜m - n⌝ + n∞2) | A User Theorem |
| add-comm | ⊦ n∞1 + n∞2 = n∞2 + n∞1 | A User Theorem |
| add-inf-01 | ⊦ n∞ + n∞1 = ∞ ↔ n∞ = ∞ ∨ n∞1 = ∞ | A User Theorem |
| add-inf-02 | ⊦ ⌜n⌝ + n∞1 = ∞ ↔ n∞1 = ∞ | A User Theorem |
| add-less | ⊦ n∞1 < n∞ + n∞1 ↔ ¬ ¬(n∞ ≠ ⌜0⌝ ∧ n∞1 ≠ ∞) | A User Theorem |
| add-less-fin-01 | ⊦ ⌜n⌝ < n∞ + ⌜n⌝ ↔ n∞ ≠ ⌜0⌝ | A User Theorem |
| add-ls-cancel-01 | ⊦ ⌜n⌝ + n∞1 < ⌜n⌝ + n∞2 ↔ n∞1 < n∞2 | A User Theorem |
| add-ls-cancel-num-01 | ⊦ m ≤ n → (⌜(* n)⌝ < ⌜(* m)⌝ + n∞2 ↔ ⌜n - m⌝ < n∞2) | A User Theorem |
| add-ls-cancel-num-02 | ⊦ m ≤ n → (⌜(* n)⌝ + n∞1 < ⌜(* m)⌝ + n∞2 ↔ ⌜n - m⌝ + n∞1 < n∞2) | A User Theorem |
| add-ls-cancel-num-03 | ⊦ m ≤ n → (⌜(* m)⌝ + n∞2 < ⌜(* n)⌝ ↔ n∞2 < ⌜n - m⌝ ) | A User Theorem |
| add-ls-cancel-num-04 | ⊦ m ≤ n → (⌜(* m)⌝ + n∞2 < ⌜(* n)⌝ + n∞1 ↔ n∞2 < ⌜n - m⌝ + n∞1) | A User Theorem |
| add-not-less | ⊦ ¬ n∞ + n∞1 < n∞1 | A User Theorem |
| addeqinf-cancel | ⊦ ⌜m⌝ + n∞ = ∞ ↔ n∞ = ∞ | A User Theorem |
| eq-natinf-to-nat-2-1 | ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n + m = n0 | A User Theorem |
| eq-natinf-to-nat-2-2 | ⊦ ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ + ⌜n1⌝ ↔ n + m = n0 + n1 | A User Theorem |
| eq-natinf-to-nat-3-1 | ⊦ ⌜n1⌝ + ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ ↔ n1 + n + m = n0 | A User Theorem |
| eq-natinf-to-nat-3-2 | ⊦ ⌜n1⌝ + ⌜n⌝ + ⌜m⌝ = ⌜n0⌝ + ⌜n2⌝ ↔ n1 + n + m = n0 + n2 | A User Theorem |
| eq-natinf-to-nat-3-3 | ⊦ ⌜n1⌝ + ⌜n⌝ + ⌜m⌝ = ⌜n2⌝ + ⌜n0⌝ + ⌜n2⌝ ↔ n1 + n + m = n2 + n0 + n2 | A User Theorem |
| eqls-ls-notls | ⊦ n∞ = n∞0 + ⌜1⌝ ∧ ⌜n⌝ < n∞0 → (¬ ⌜n⌝ < n∞ ↔ false) | A User Theorem |
| eqls-succ | ⊦ n∞0 + ⌜1⌝ = n∞ → (⌜n⌝ + ⌜1⌝ < n∞ ↔ ⌜n⌝ < n∞0) | A User Theorem |
| eqsucc-ls | ⊦ n∞0 + ⌜1⌝ = n∞ → (¬ n∞0 < n∞ ↔ n∞0 = ∞) | A User Theorem |
| eqsucc-notls | ⊦ n∞0 + ⌜1⌝ = n∞ → (n∞ < n∞0 ↔ false) | A User Theorem |
| eqsum-notless | ⊦ n∞ = ⌜n⌝ + ⌜m⌝ → (¬ ⌜n1⌝ + ⌜m⌝ < n∞ ↔ ¬ n1 < n) | A User Theorem |
| inf-inseq-reduce | ⊦ n∞ = ⌜m⌝ + ⌜n0⌝ → (⌜n⌝ < n∞ ↔ n < m + n0) | A User Theorem |
| inf-less | ⊦ n∞ < ∞ ↔ n∞ ≠ ∞ | A User Theorem |
| lele-refl | ⊦ ¬ n∞1 < n∞ → (¬ n∞ < n∞1 ↔ n∞ = n∞1) | A User Theorem |
| lele-trans | ⊦ ¬ n∞1 < n∞ ∧ ¬ n∞2 < n∞1 → ¬ n∞2 < n∞ | A User Theorem |
| lels-trans | ⊦ ¬ n∞1 < n∞ ∧ n∞1 < n∞2 → n∞ < n∞2 | A User Theorem |
| leq-notgradd | ⊦ m ≤ n → (⌜n⌝ + n∞0 < ⌜m⌝ ↔ false) | A User Theorem |
| less-less-leftsucc | ⊦ n∞ < n∞0 → (¬ n∞ + ⌜1⌝ < n∞0 ↔ ¬ ¬(n∞ + ⌜1⌝ = n∞0 ∧ n∞ ≠ ∞)) | A User Theorem |
| less-notgeqinf | ⊦ m < n → (⌜n⌝ + n∞ < ⌜m⌝ ↔ false) | A User Theorem |
| less-succ-leq | ⊦ ⌜n⌝ < ⌜1⌝ + n∞ ↔ ¬ n∞ < ⌜n⌝ | A User Theorem |
| ls-irref | ⊦ ¬ n∞ < n∞ | A User Theorem |
| ls-le | ⊦ n∞ < n∞0 → ¬ n∞0 < n∞ | A User Theorem |
| ls-lsadd | ⊦ m < n → ⌜m⌝ < ⌜n⌝ + n∞0 | A User Theorem |
| ls-natinf-to-nat-1-2 | ⊦ ⌜n⌝ < ⌜m⌝ + ⌜n0⌝ ↔ n < m + n0 | A User Theorem |
| ls-natinf-to-nat-1-3 | ⊦ ⌜n1⌝ < ⌜n0⌝ + ⌜n⌝ + ⌜m⌝ ↔ n1 < n0 + n + m | A User Theorem |
| ls-natinf-to-nat-2-1 | ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n + m < n0 | A User Theorem |
| ls-natinf-to-nat-2-2 | ⊦ ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ + ⌜n1⌝ ↔ n + m < n0 + n1 | A User Theorem |
| ls-natinf-to-nat-2-3 | ⊦ ⌜n1⌝ + ⌜n⌝ < ⌜n0⌝ + ⌜n2⌝ + ⌜m⌝ ↔ n1 + n < n0 + n2 + m | A User Theorem |
| ls-natinf-to-nat-3-1 | ⊦ ⌜n1⌝ + ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ ↔ n1 + n + m < n0 | A User Theorem |
| ls-natinf-to-nat-3-2 | ⊦ ⌜n1⌝ + ⌜n⌝ + ⌜m⌝ < ⌜n0⌝ + ⌜n2⌝ ↔ n1 + n + m < n0 + n2 | A User Theorem |
| ls-natinf-to-nat-3-3 | ⊦ ⌜n1⌝ + ⌜n⌝ + ⌜m⌝ < ⌜n2⌝ + ⌜n0⌝ + ⌜n2⌝ ↔ n1 + n + m < n2 + n0 + n2 | A User Theorem |
| ls-notlssucc | ⊦ ⌜m⌝ < n∞ → (¬ ⌜m⌝ + ⌜1⌝ < n∞ ↔ ⌜m⌝ + ⌜1⌝ = n∞) | A User Theorem |
| ls-one | ⊦ n∞ < ⌜1⌝ ↔ n∞ = ⌜0⌝ | A User Theorem |
| ls-succ | ⊦ n∞ < ⌜n + 1⌝ ↔ ¬ ⌜n⌝ < n∞ | A User Theorem |
| ls-succ-01 | ⊦ n∞ < ⌜n⌝ + ⌜1⌝ ↔ ¬ ⌜n⌝ < n∞ | A User Theorem |
| ls-trans | ⊦ n∞ < n∞1 ∧ n∞1 < n∞2 → n∞ < n∞2 | A User Theorem |
| lsle-trans | ⊦ n∞ < n∞1 ∧ ¬ n∞2 < n∞1 → n∞ < n∞2 | A User Theorem |
| min-inf1 | ⊦ min(∞, n∞) = n∞ | A User Theorem |
| min-inf2 | ⊦ min(n∞, ∞) = n∞ | A User Theorem |
| not-less-zero | ⊦ ¬ n∞ < ⌜0⌝ | A User Theorem |
| num-add | ⊦ ⌜(* n)⌝ + ⌜(* m)⌝ = ⌜n + m⌝ | A User Theorem |
| onels-neqzero | ⊦ ⌜1⌝ < n∞ ↔ ¬ ¬(n∞ ≠ ⌜0⌝ ∧ n∞ ≠ ⌜1⌝ ) | A User Theorem |
| prime-add-fin | n∞ ≠ ∞ ⊦ (⌜m⌝ + n∞).n = m + n∞.n | A User Theorem |
| rem-seln-on-add | ⊦ n∞ = ⌜m⌝ + ⌜n⌝ → n∞.n = m + n | A User Theorem |
| sum-notinf | ⊦ n∞ = ⌜m⌝ + ⌜n⌝ → (n∞ = ∞ ↔ false) | A User Theorem |
| sum-zero | ⊦ n∞ + n∞1 = ⌜0⌝ ↔ n∞ = ⌜0⌝ ∧ n∞1 = ⌜0⌝ | A User Theorem |
| sum-zero-fin | ⊦ ⌜n⌝ + n∞ = ⌜0⌝ ↔ n∞ = ⌜0⌝ ∧ n = 0 | A User Theorem |
| zerols-neqzero | ⊦ ⌜0⌝ < n∞ ↔ n∞ ≠ ⌜0⌝ | A User Theorem |