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: |
|---|---|---|
| n2s-char | ⊦ n < 10 → n→s(n) = ('0' + '1' + '2' + '3' + '4' + '5' + '6' + '7' + ('8' + '9'))[n] + "" | An Axiom |
| s2n-rec | ⊦ s→n(char ' + char0 ' + str) = s→n(char ') * 10 ^ (# str)+1 + s→n(char0 ' + str) | An Axiom |
| s2n-char | ⊦ s→n(char ') = pos(char, '0' + '1' + '2' + '3' + '4' + '5' + '6' + '7' + ('8' + '9')) | An Axiom |
| n2s-rec | ⊦ 10 ≤ n → n→s(n) = n→s(n / 10) + n→s(n % 10) | An Axiom |
| char0 | ⊦ n→s(0) = "0" | A User Theorem |
| char1 | ⊦ n→s(1) = "1" | A User Theorem |
| char2 | ⊦ n→s(2) = "2" | A User Theorem |
| char3 | ⊦ n→s(3) = "3" | A User Theorem |
| char4 | ⊦ n→s(4) = "4" | A User Theorem |
| char5 | ⊦ n→s(5) = "5" | A User Theorem |
| char6 | ⊦ n→s(6) = "6" | A User Theorem |
| char7 | ⊦ n→s(7) = "7" | A User Theorem |
| char8 | ⊦ n→s(8) = "8" | A User Theorem |
| char9 | ⊦ n→s(9) = "9" | A User Theorem |
| charn0 | ⊦ s→n("0") = 0 | A User Theorem |
| charn1 | ⊦ s→n("1") = 1 | A User Theorem |
| charn2 | ⊦ s→n("2") = 2 | A User Theorem |
| charn3 | ⊦ s→n("3") = 3 | A User Theorem |
| charn4 | ⊦ s→n("4") = 4 | A User Theorem |
| charn5 | ⊦ s→n("5") = 5 | A User Theorem |
| charn6 | ⊦ s→n("6") = 6 | A User Theorem |
| charn7 | ⊦ s→n("7") = 7 | A User Theorem |
| charn8 | ⊦ s→n("8") = 8 | A User Theorem |
| charn9 | ⊦ s→n("9") = 9 | A User Theorem |
| inject-n2s | ⊦ n→s(m) = n→s(n) ↔ m = n | A User Theorem |
| n2s-chars | ⊦ ¬ char ∈ '0' + '1' + '2' + '3' + '4' + '5' + '6' + '7' + ('8' + '9') → ¬ char ∈ s→l(n→s(m)) | A User Theorem |
| n2s-empty | ⊦ n→s(n) ≠ "" | A User Theorem |
| n2s-length | ⊦ m < 10 → # n→s(m) = 1 | A User Theorem |
| n2s-length-01 | ⊦ # n→s(m % 10) = 1 | A User Theorem |
| n2s-length-02 | ⊦ 10 ≤ m ∧ m < 100 → # n→s(m) = 2 | A User Theorem |
| n2s-length-03 | ⊦ 100 ≤ m ∧ m < 1000 → # n→s(m) = 3 | A User Theorem |
| n2s-length-04 | ⊦ 1000 ≤ m ∧ m < 10000 → # n→s(m) = 4 | A User Theorem |
| n2s-length-05 | ⊦ 10000 ≤ m ∧ m < 100000 → # n→s(m) = 5 | A User Theorem |
| n2s-length-06 | ⊦ 100000 ≤ m ∧ m < 1000000 → # n→s(m) = 6 | A User Theorem |
| n2s-length-07 | ⊦ 1000000 ≤ m ∧ m < 10000000 → # n→s(m) = 7 | A User Theorem |
| n2s-length-08 | ⊦ 10000000 ≤ m ∧ m < 100000000 → # n→s(m) = 8 | A User Theorem |
| n2s-length-09 | ⊦ 100000000 ≤ m ∧ m < 1000000000 → # n→s(m) = 9 | A User Theorem |
| n2s-length-10 | ⊦ 1000000000 ≤ m ∧ m < 10000000000 → # n→s(m) = 10 | A User Theorem |
| n2s-s2n-identity | ⊦ s→n(n→s(m)) = m | A User Theorem |
| n2s-zero | ⊦ n→s(n) = "0" ↔ n = 0 | A User Theorem |
| s2n-app | ⊦ str ≠ "" ∧ str0 ≠ "" → s→n(str + str0) = s→n(str) * 10 ^ # str0 + s→n(str0) | A User Theorem |
| s2n-char-01 | # str = 1 ⊦ s→n(str) = pos(str.char1, '0' + '1' + '2' + '3' + '4' + '5' + '6' + '7' + ('8' + '9')) | A User Theorem |
| s2n-num | 1 < # str ⊦ s→n((* str)) = s→n(str.char1 + "") * 10 ^ (# str)-1 + s→n(str.rstring) | A User Theorem |
| s2n-rec-01 | 1 < # str ⊦ s→n(str) = s→n(str.char1 + "") * 10 ^ (# str)-1 + s→n(str.rstring) | A User Theorem |
| s2n-rec-last | ⊦ str ≠ "" → s→n(str + char ') = s→n(str) * 10 + s→n(char ') | A User Theorem |
| test-01 | ⊦ n→s(12345) = "12345" | A User Theorem |
| test-02 | ⊦ s→n("12345") = 12345 | A User Theorem |