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: |
|---|---|---|
| hex-def | ⊦ hex(str) = hexint(hexstring(str)) | An Axiom |
| hexstring-empty | ⊦ hexstring("") = [] | An Axiom |
| hexstring-rec | ⊦ hexstring(char + str) = hexchar(char) + hexstring(str) | An Axiom |
| hexint-empty | ⊦ hexint([]) = 0 | An Axiom |
| hexint-rec | ⊦ hexint(i ' + ints) = i * 16 ^ n→i(# ints) + hexint(ints) | An Axiom |
| hexchar0 | ⊦ hexchar('0') = 0 | An Axiom |
| hexchar1 | ⊦ hexchar('1') = 1 | An Axiom |
| hexchar2 | ⊦ hexchar('2') = 2 | An Axiom |
| hexchar3 | ⊦ hexchar('3') = 3 | An Axiom |
| hexchar4 | ⊦ hexchar('4') = 4 | An Axiom |
| hexchar5 | ⊦ hexchar('5') = 5 | An Axiom |
| hexchar6 | ⊦ hexchar('6') = 6 | An Axiom |
| hexchar7 | ⊦ hexchar('7') = 7 | An Axiom |
| hexchar8 | ⊦ hexchar('8') = 8 | An Axiom |
| hexchar9 | ⊦ hexchar('9') = 9 | An Axiom |
| hexchara | ⊦ hexchar('a') = 10 | An Axiom |
| hexcharb | ⊦ hexchar('b') = 11 | An Axiom |
| hexcharc | ⊦ hexchar('c') = 12 | An Axiom |
| hexchard | ⊦ hexchar('d') = 13 | An Axiom |
| hexchare | ⊦ hexchar('e') = 14 | An Axiom |
| hexcharf | ⊦ hexchar('f') = 15 | An Axiom |
| hexcharA | ⊦ hexchar('A') = 10 | An Axiom |
| hexcharB | ⊦ hexchar('B') = 11 | An Axiom |
| hexcharC | ⊦ hexchar('C') = 12 | An Axiom |
| hexcharD | ⊦ hexchar('D') = 13 | An Axiom |
| hexcharE | ⊦ hexchar('E') = 14 | An Axiom |
| hexcharF | ⊦ hexchar('F') = 15 | An Axiom |
| hexbyte | ⊦ hexbyte(str) = i2b(hex(str)) | An Axiom |
| hex-empty | ⊦ hex("") = 0 | A User Theorem |
| hex-rec | ⊦ str ≠ "" → hex(str) = hexchar(str.char1) * 16 ^ (n→i(# str) - 1) + hex(str.rstring) | A User Theorem |
| hexbyte-byte | # str = 2 ⊦ hexbyte((* str)) = i2b(hexchar(str.char1) * 16 + hexchar(str.rstring.char1)) | A User Theorem |
| hexstring-length | ⊦ # hexstring(str) = # str | A User Theorem |
| hexstring-rec-01 | ⊦ hexstring(char ' + str) = hexchar(char) + hexstring(str) | A User Theorem |
| numhex-rec | str ≠ "" ⊦ hex((* str)) = hexchar(str.char1) * 16 ^ (n→i(# str) - 1) + hex(str.rstring) | A User Theorem |
| test-01 | ⊦ hex("9F15") = 40725 | A User Theorem |