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: |
|---|---|---|
| int2bytes | ⊦ int2bytes(i) = bits2bytes(int2bits(i)) | An Axiom |
| bits2bytes-base | ⊦ # bits ≤ 8 → bits2bytes(bits) = i2b(bits2int(bits)) ' | An Axiom |
| bits2bytes-rec | ⊦ 8 < # bits → bits2bytes(bits) = bits2bytes(firstn(# bits - 8, bits)) + i2b(bits2int(lastn(8, bits))) | An Axiom |
| bytes2int | ⊦ bytes2int(bytes) = bits2int(bytes2bits(bytes)) | An Axiom |
| bytes2bits-empty | ⊦ bytes2bits([]) = [] | An Axiom |
| bytes2bits-rec | ⊦ bytes2bits(by ' + bytes) = byte2bits(by) + bytes2bits(bytes) | An Axiom |
| byte2bits | ⊦ byte2bits(by) = fillsgn(8, int2bits(b2i(by))) | An Axiom |
| fix-longer | ⊦ # bytes ≥ n → fix(n, bytes) = lastn(n, bytes) | An Axiom |
| fix-neg | ⊦ # bytes < n ∧ bytes2int(bytes) < 0 → fix(n, bytes) = mklist(i2b(~1), n - # bytes) + bytes | An Axiom |
| fix-pos | ⊦ # bytes < n ∧ 0 ≤ bytes2int(bytes) → fix(n, bytes) = mklist(i2b(0), n - # bytes) + bytes | An Axiom |
| fillsgn-neg | ⊦ # bytes < n ∧ bytes2int(bytes) < 0 → fillsgn(n, bytes) = mklist(i2b(~1), n - # bytes) + bytes | An Axiom |
| fillsgn-pos | ⊦ # bytes < n ∧ 0 ≤ bytes2int(bytes) → fillsgn(n, bytes) = mklist(i2b(0), n - # bytes) + bytes | An Axiom |
| fillsgn-longer | ⊦ # bytes ≥ n → fillsgn(n, bytes) = bytes | An Axiom |
| band-65535-neg | ⊦ bytes2int(bytes) < 0 ∧ # bytes ≤ 2 ∧ bytes ≠ [] → band(bytes2int(bytes), 65535) = (bytes2int(bytes) + 1) + 65535 | A User Theorem |
| band-65535-pos | ⊦ 0 ≤ bytes2int(bytes) ∧ # bytes ≤ 2 ∧ bytes ≠ [] → band(bytes2int(bytes), 65535) = bytes2int(bytes) | A User Theorem |
| bits2bits-in | ⊦ bits ≠ [] → (boolvar ∈ bytes2bits(bits2bytes(bits)) ↔ boolvar ∈ bits) | A User Theorem |
| bits2bits-inj | ⊦ # bits % 8 = 0 ∧ bits ≠ [] → bytes2bits(bits2bytes(bits)) = bits | A User Theorem |
| bits2bits-sgn | ⊦ bits ≠ [] → sgn(bytes2bits(bits2bytes(bits))) = sgn(bits) | A User Theorem |
| bits2bytes-2pot | ⊦ # bits2bytes(true ' + mklist(false, 7 + 8 * n)) = n + 1 | A User Theorem |
| bits2bytes-app | ⊦ # bits0 % 8 = 0 ∧ bits ≠ [] ∧ bits0 ≠ [] → bits2bytes(bits + bits0) = bits2bytes(bits) + bits2bytes(bits0) | A User Theorem |
| bits2bytes-empty | ⊦ bits2bytes(bits) ≠ [] | A User Theorem |
| bits2bytes-fill | ⊦ bits ≠ [] ∧ # bits % 8 = n ∧ n ≠ 0 → bits2bytes(bits) = bits2bytes(mklist(bits.first, 8 - n) + bits) | A User Theorem |
| bits2bytes-len | ⊦ bits ≠ [] → # bits2bytes(bits) = (# bits - 1) / 8 + 1 | A User Theorem |
| bits2bytes-len-01 | ⊦ # bits % 8 = 0 ∧ bits ≠ [] → # bits2bytes(bits) = # bits / 8 | A User Theorem |
| bits2bytes-len-02 | ⊦ # bits % 8 ≠ 0 → # bits2bytes(bits) = # bits / 8 + 1 | A User Theorem |
| bits2bytes-mklist | ⊦ n % 8 = 0 ∧ n ≠ 0 → bits2bytes(mklist(false, n)) = mklist(i2b(0), n / 8) | A User Theorem |
| bits2bytes-mklist-01 | ⊦ n % 8 ≠ 0 → bits2bytes(mklist(false, n)) = mklist(i2b(0), n / 8 + 1) | A User Theorem |
| bits2bytes-mklist-02 | ⊦ n % 8 = 0 ∧ n ≠ 0 → bits2bytes(mklist(true, n)) = mklist(i2b(~1), n / 8) | A User Theorem |
| bits2bytes-mklist-03 | ⊦ n % 8 ≠ 0 → bits2bytes(mklist(true, n)) = mklist(i2b(~1), n / 8 + 1) | A User Theorem |
| bits2bytes-rec-01 | ⊦ # bits % 8 ≠ 0 ∧ 8 < # bits → bits2bytes(bits) = bits2bytes(firstn(# bits % 8, bits)) + bits2bytes(restn(# bits % 8, bits)) | A User Theorem |
| bits2bytes-rec-02 | ⊦ # bits % 8 = 0 ∧ 8 < # bits → bits2bytes(bits) = bits2bytes(firstn(8, bits)) + bits2bytes(restn(8, bits)) | A User Theorem |
| bits2bytes-true | ⊦ bits2bytes(true ') = i2b(~1) ' | A User Theorem |
| bits2int-2pot | ⊦ ¬ true ∈ bits → bytes2int(bits2bytes(true ' + bits)) = ~(2 ^ n→i(# bits)) | A User Theorem |
| bits2int-neg | ⊦ bits ≠ [] → (bytes2int(bits2bytes(bits)) < 0 ↔ bits.first) | A User Theorem |
| bits2int-pos | ⊦ bits ≠ [] → (0 ≤ bytes2int(bits2bytes(bits)) ↔ ¬ bits.first) | A User Theorem |
| bits2int-zero-ls | ⊦ bytes ≠ [] → (bits2int(bytes2bits(bytes)) < 0 ↔ b2i(bytes.first) < 0) | A User Theorem |
| byte2bits-empty | ⊦ byte2bits(by) ≠ [] | A User Theorem |
| byte2bits-first | ⊦ byte2bits(by).first ↔ b2i(by) < 0 | A User Theorem |
| byte2bits-length | ⊦ # byte2bits(by) = 8 | A User Theorem |
| byte2bits-mone | ⊦ byte2bits(i2b(~1)) = mklist(true, 8) | A User Theorem |
| byte2bits-val | ⊦ bits2uint(byte2bits(by)) = band(b2i(by), 255) | A User Theorem |
| byte2bits-value | ⊦ bits2int(byte2bits(by)) = b2i(by) | A User Theorem |
| byte2bits-zero | ⊦ byte2bits(i2b(0)) = mklist(false, 8) | A User Theorem |
| byte2bits8 | ⊦ # bits = 8 → byte2bits(i2b(bits2int(bits))) = bits | A User Theorem |
| bytes2bits-append | ⊦ bytes2bits(bytes + bytes0) = bytes2bits(bytes) + bytes2bits(bytes0) | A User Theorem |
| bytes2bits-empty-01 | ⊦ bytes2bits(bytes) = [] ↔ bytes = [] | A User Theorem |
| bytes2bits-length | ⊦ # bytes2bits(bytes) = i→n(8) * # bytes | A User Theorem |
| bytes2bits-mklist | ⊦ bytes2bits(mklist(i2b(0), n)) = mklist(false, 8 * n) | A User Theorem |
| bytes2bits-mklist-01 | ⊦ bytes2bits(mklist(i2b(~1), n)) = mklist(true, 8 * n) | A User Theorem |
| bytes2bits-nle | ⊦ ¬ 2 ^ (8 * n→i(# bytes)) ≤ bits2uint(bytes2bits(bytes)) | A User Theorem |
| bytes2bits-nls | bytes ≠ [] ⊦ ¬ 2 ^ (8 * n→i(# bytes)) + bits2int(bytes2bits(bytes)) < 0 | A User Theorem |
| bytes2bits-one | ⊦ bytes2bits(by ') = byte2bits(by) | A User Theorem |
| bytes2bytes | ⊦ bytes ≠ [] → int2bytes(bytes2int(bytes)) = bits2bytes(sgn(bytes2bits(bytes))) | A User Theorem |
| bytes2bytes-fillsgn | ⊦ # bytes = n ∧ bytes ≠ [] → fillsgn(n, int2bytes(bytes2int(bytes))) = bytes | A User Theorem |
| bytes2bytes-first-neg | ⊦ b2i(int2bytes(bytes2int(by ' + bytes)).first) < 0 ↔ b2i(by) < 0 | A User Theorem |
| bytes2bytes-first-pos | ⊦ 0 ≤ b2i(int2bytes(bytes2int(by ' + bytes)).first) ↔ 0 ≤ b2i(by) | A User Theorem |
| bytes2bytes-fix | ⊦ bytes ≠ [] → fix(# bytes, int2bytes(bytes2int(bytes))) = bytes | A User Theorem |
| bytes2bytes-identity | ⊦ # bytes = # int2bytes(bytes2int(bytes)) → int2bytes(bytes2int(bytes)) = bytes | A User Theorem |
| bytes2bytes-identity-01 | ⊦ # bytes ≤ # int2bytes(bytes2int(bytes)) ∧ bytes ≠ [] → int2bytes(bytes2int(bytes)) = bytes | A User Theorem |
| bytes2bytes-length | ⊦ bytes ≠ [] → # int2bytes(bytes2int(bytes)) ≤ # bytes | A User Theorem |
| bytes2bytes-mone | 1 < # bytes, b2i(bytes.first) = ~1, 0 ≤ b2i(bytes.rest.first) ⊦ int2bytes(bytes2int(bytes)) = bytes | A User Theorem |
| bytes2bytes-other | bytes ≠ [], b2i(bytes.first) ≠ 0, b2i(bytes.first) ≠ ~1 ⊦ int2bytes(bytes2int(bytes)) = bytes | A User Theorem |
| bytes2bytes-zero | 1 < # bytes, b2i(bytes.first) = 0, b2i(bytes.rest.first) < 0 ⊦ int2bytes(bytes2int(bytes)) = bytes | A User Theorem |
| bytes2int-011x | ⊦ bytes2int(i2b(0) ' + mklist(i2b(~1), n)) = 2 ^ (8 * n→i(n)) - 1 | A User Theorem |
| bytes2int-011x-01 | ⊦ bytes2int(i2b(127) ' + mklist(i2b(~1), n)) = 2 ^ (8 * (1 + n→i(n)) - 1) - 1 | A User Theorem |
| bytes2int-011x-02 | ⊦ bytes2int(i2b(~2) ' + mklist(i2b(~1), n)) = ~(2 ^ (8 * n→i(n)) + 1) | A User Theorem |
| bytes2int-100x | ⊦ bytes2int(i2b(0) ' + i2b(~128) ' + mklist(i2b(0), n)) = 2 ^ (8 * (1 + n→i(n)) - 1) | A User Theorem |
| bytes2int-100x-01 | ⊦ bytes2int(i2b(1) ' + mklist(i2b(0), n)) = 2 ^ (8 * n→i(n)) | A User Theorem |
| bytes2int-100x-02 | ⊦ bytes2int(i2b(~128) ' + mklist(i2b(0), n)) = ~(2 ^ (8 * (1 + n→i(n)) - 1)) | A User Theorem |
| bytes2int-100x-03 | ⊦ bytes2int(i2b(~1) ' + mklist(i2b(0), n)) = ~(2 ^ (8 * n→i(n))) | A User Theorem |
| bytes2int-1011x | ⊦ bytes2int(i2b(~1) ' + i2b(127) ' + mklist(i2b(~1), n)) = ~(2 ^ (8 * (n→i(n) + 1) - 1) + 1) | A User Theorem |
| bytes2int-2-le-32767 | ⊦ ¬ 32767 < bytes2int(by ' + by1 ') | A User Theorem |
| bytes2int-append | bytes ≠ [], bytes0 ≠ [] ⊦ bytes2int(bytes + bytes0) = bytes2int(bytes) * 256 ^ n→i(# bytes0) + band(bytes2int(bytes0), 256 ^ n→i(# bytes0) - 1) | A User Theorem |
| bytes2int-diff | ⊦ # bytes0 = # bytes ∧ bytes0 ≠ bytes → bytes2int(bytes0) ≠ bytes2int(bytes) | A User Theorem |
| bytes2int-fillsgn-zero | ⊦ fillsgn(n, i2b(0) ') ≠ bytes ∧ bytes ≠ [] ∧ n = # bytes → bytes2int(bytes) ≠ 0 | A User Theorem |
| bytes2int-first-gez | ⊦ 0 ≤ b2i(int2bytes(i).first) ↔ 0 ≤ i | A User Theorem |
| bytes2int-first-lez | ⊦ b2i(int2bytes(i).first) < 0 ↔ i < 0 | A User Theorem |
| bytes2int-first-neq | ⊦ 0 ≤ bytes2int(by ' + bytes) → ¬ b2i(by) < 0 | A User Theorem |
| bytes2int-first-pos | ⊦ ¬ 0 ≤ bytes2int(by + bytes) → ¬ 0 ≤ b2i(by) | A User Theorem |
| bytes2int-first-pos-01 | ⊦ ¬ 0 ≤ bytes2int(by ' + bytes) → ¬ 0 ≤ b2i(by) | A User Theorem |
| bytes2int-ge-zero | ⊦ 0 ≤ bytes2int(by ' + bytes) ↔ 0 ≤ b2i(by) | A User Theorem |
| bytes2int-ge-zero-01 | ⊦ ¬ 0 ≤ bytes2int(i2b(~1) ' + bytes) | A User Theorem |
| bytes2int-i2b | ⊦ bytes ≠ [] → i2b(bytes2int(bytes)) = bytes.last | A User Theorem |
| bytes2int-int2bytes-len-eq | ⊦ # bytes = # int2bytes(bytes2int(bytes)) → bytes = int2bytes(bytes2int(bytes)) | A User Theorem |
| bytes2int-le-zero | ⊦ bytes2int(i2b(0) ' + bytes) ≤ 0 ↔ bytes2int(i2b(0) ' + bytes) = 0 | A User Theorem |
| bytes2int-leading-zero | ⊦ 0 ≤ b2i(by) → bytes2int(i2b(0) ' + by ') = b2i(by) | A User Theorem |
| bytes2int-len-one-01 | ⊦ 0 ≤ bytes2int(bytes) ∧ # bytes ≠ 1 ∧ bytes ≠ [] ∧ bytes.first ≠ i2b(0) → ¬ bytes2int(bytes) < 128 | A User Theorem |
| bytes2int-len-one-02 | ⊦ 0 ≤ bytes2int(bytes) ∧ # bytes ≠ 1 ∧ bytes ≠ [] ∧ bytes.first = i2b(0) ∧ b2i(bytes.rest.first) < 0 → ¬ bytes2int(bytes) < 128 | A User Theorem |
| bytes2int-mklist-mones | ⊦ n ≠ 0 → bytes2int(mklist(i2b(~1), n)) = ~1 | A User Theorem |
| bytes2int-mklist-mones-01 | ⊦ b2i(bytes.first) < 0 ∧ bytes ≠ [] → bytes2int(mklist(i2b(~1), n) + bytes) = bytes2int(bytes) | A User Theorem |
| bytes2int-mklist-zeros | ⊦ bytes2int(mklist(i2b(0), n)) = 0 | A User Theorem |
| bytes2int-mklist-zeros-01 | ⊦ 0 ≤ b2i(bytes.first) ∧ bytes ≠ [] → bytes2int(mklist(i2b(0), n) + bytes) = bytes2int(bytes) | A User Theorem |
| bytes2int-mone | ⊦ b2i(by) < 0 → bytes2int(i2b(~1) ' + by ' + bytes) = bytes2int(by ' + bytes) | A User Theorem |
| bytes2int-neg | ⊦ bytes ≠ [] → (bytes2int(bytes) < 0 ↔ b2i(bytes.first) < 0) | A User Theorem |
| bytes2int-neg-01 | ⊦ bytes2int(by ' + bytes) < 0 ↔ b2i(by) < 0 | A User Theorem |
| bytes2int-one | ⊦ bytes2int(by ') = b2i(by) | A User Theorem |
| bytes2int-pos | ⊦ 0 ≤ bytes2int(bytes) ↔ bytes = [] ∨ 0 ≤ b2i(bytes.first) | A User Theorem |
| bytes2int-range | bytes ≠ [] ⊦ ~(2 ^ n→i(# bytes * 8 - 1)) ≤ bytes2int(bytes) ∧ bytes2int(bytes) < 2 ^ n→i(# bytes * 8 - 1) | A User Theorem |
| bytes2int-rec | ⊦ bytes ≠ [] → bytes2int(bytes + by ') = bytes2int(bytes) * 256 + band(b2i(by), 255) | A User Theorem |
| bytes2int-rec-01 | ⊦ 1 < # bytes → bytes2int(bytes) = bytes2int(bytes.butlast) * 256 + band(b2i(bytes.last), 255) | A User Theorem |
| bytes2int-rec-bor | ⊦ bytes ≠ [] → bytes2int(bytes + by ') = bor(bytes2int(bytes) * 256, band(b2i(by), 255)) | A User Theorem |
| bytes2int-rec-first-zero | ⊦ bytes ≠ [] → bytes2int(i2b(0) ' + by ' + bytes) = band(b2i(by), 255) * 256 ^ n→i(# bytes) + bytes2int(i2b(0) ' + bytes) | A User Theorem |
| bytes2int-same | ⊦ bytes2int(bytes) = bytes2int(bytes0) ∧ int2bytes(bytes2int(bytes)) = bytes ∧ int2bytes(bytes2int(bytes0)) = bytes0 → bytes = bytes0 | A User Theorem |
| bytes2int-size | ⊦ b2i(by) < 0 → bytes2int(i2b(0) ' + by ' + bytes) < 2 ^ ((n→i(# bytes) + 1) * 8) | A User Theorem |
| bytes2int-size-01 | ⊦ b2i(by) < 0 → 2 ^ ((n→i(# bytes) + 1) * 8 - 1) ≤ bytes2int(i2b(0) ' + by ' + bytes) | A User Theorem |
| bytes2int-size-02 | ⊦ 0 < b2i(by) → bytes2int(by ' + bytes) < 2 ^ ((n→i(# bytes) + 1) * 8 - 1) | A User Theorem |
| bytes2int-size-03 | ⊦ 0 < b2i(by) → 2 ^ (n→i(# bytes) * 8) ≤ bytes2int(by ' + bytes) | A User Theorem |
| bytes2int-size-04 | ⊦ b2i(by) < 0 → ~(2 ^ ((n→i(# bytes) + 1) * 8 - 1)) ≤ bytes2int(by ' + bytes) | A User Theorem |
| bytes2int-size-05 | ⊦ 0 ≤ b2i(by) → ~(2 ^ ((n→i(# bytes) + 1) * 8)) ≤ bytes2int(i2b(~1) ' + by ' + bytes) | A User Theorem |
| bytes2int-size-06 | ⊦ b2i(by) < 0 ∧ b2i(by) ≠ ~1 → bytes2int(by ' + bytes) < ~(2 ^ (8 * n→i(# bytes))) | A User Theorem |
| bytes2int-size-07 | ⊦ 0 ≤ b2i(by) → bytes2int(i2b(~1) ' + by ' + bytes) < ~(2 ^ (8 * (n→i(# bytes) + 1) - 1)) | A User Theorem |
| bytes2int-size-val | ⊦ ∃ by, bytes. b2i(by) < 0 ∧ bytes2int(i2b(0) ' + by ' + bytes) = 2 ^ ((n→i(# bytes) + 1) * 8) - 1 | A User Theorem |
| bytes2int-size-val-01 | ⊦ ∃ by, bytes. b2i(by) < 0 ∧ 2 ^ ((n→i(# bytes) + 1) * 8 - 1) = bytes2int(i2b(0) ' + by ' + bytes) | A User Theorem |
| bytes2int-size-val-02 | ⊦ ∃ by, bytes. 0 < b2i(by) ∧ bytes2int(by ' + bytes) = 2 ^ ((n→i(# bytes) + 1) * 8 - 1) - 1 | A User Theorem |
| bytes2int-size-val-03 | ⊦ ∃ by, bytes. 0 < b2i(by) ∧ bytes2int(by ' + bytes) = 2 ^ (n→i(# bytes) * 8) | A User Theorem |
| bytes2int-size-val-04 | ⊦ ∃ by, bytes. b2i(by) < 0 ∧ ~(2 ^ ((n→i(# bytes) + 1) * 8 - 1)) = bytes2int(by ' + bytes) | A User Theorem |
| bytes2int-size-val-05 | ⊦ ∃ by, bytes. 0 ≤ b2i(by) ∧ ~(2 ^ ((n→i(# bytes) + 1) * 8)) = bytes2int(i2b(~1) ' + by ' + bytes) | A User Theorem |
| bytes2int-size-val-06 | ⊦ ∃ by, bytes. b2i(by) < 0 ∧ b2i(by) ≠ ~1 ∧ bytes2int(by ' + bytes) = ~(2 ^ (8 * n→i(# bytes)) + 1) | A User Theorem |
| bytes2int-size-val-07 | ⊦ ∃ by, bytes. 0 ≤ b2i(by) ∧ bytes2int(i2b(~1) ' + by ' + bytes) = ~(2 ^ (8 * (n→i(# bytes) + 1) - 1) + 1) | A User Theorem |
| bytes2int-zero | ⊦ bytes2int(i2b(0) ') = 0 | A User Theorem |
| bytes2int-zero-01 | ⊦ bytes2int(i2b(0) ' + i2b(0) ') = 0 | A User Theorem |
| bytes2int-zero-02 | ⊦ bytes2int(i2b(0) ' + i2b(0) ' + bytes) = bytes2int(i2b(0) ' + bytes) | A User Theorem |
| bytes2int-zero-03 | ⊦ by ≠ i2b(0) ∧ by ∈ bytes → bytes2int(bytes) ≠ 0 | A User Theorem |
| bytes2int-zero-04 | ⊦ 0 ≤ b2i(by) → bytes2int(i2b(0) ' + by ' + bytes) = bytes2int(by ' + bytes) | A User Theorem |
| bytes2int-zero-05 | ⊦ 0 ≤ n ∧ n < # bytes ∧ bytes2int(bytes) = 0 → bytes[n] = i2b(0) | A User Theorem |
| bytes2int-zero-06 | ⊦ bytes ≠ [] → (bytes2int(bytes) = 0 ↔ (∀ by. by ∈ bytes → b2i(by) = 0)) | A User Theorem |
| fillsgn-butlast | ⊦ 1 < # bytes → fillsgn(n, bytes.butlast) = fillsgn(n + 1, bytes).butlast | A User Theorem |
| fillsgn-empty | ⊦ fillsgn(n, bytes) = [] ↔ n = 0 ∧ bytes = [] | A User Theorem |
| fillsgn-fix | ⊦ # bytes < n → fillsgn(n, bytes) = fix(n, bytes) | A User Theorem |
| fillsgn-len-short | ⊦ # fillsgn(2, int2bytes(s2i(sho))) = 2 | A User Theorem |
| fillsgn-length | ⊦ bytes ≠ [] → n ≤ # fillsgn(n, bytes) | A User Theorem |
| fillsgn-length-01 | ⊦ # bytes < n → # fillsgn(n, bytes) = n | A User Theorem |
| fillsgn-length-02 | ⊦ # bytes ≤ n → # fillsgn(n, bytes) = n | A User Theorem |
| fillsgn-length-03 | ⊦ # fillsgn(# bytes, bytes) = # bytes | A User Theorem |
| fillsgn-not-empty | ⊦ fillsgn(n, int2bytes(i)) ≠ [] | A User Theorem |
| fillsgn-rec | ⊦ # bytes < n ∧ bytes ≠ [] → fillsgn(n, bytes) = (b2i(bytes.first) < 0 ⊃ i2b(~1);i2b(0)) ' + fillsgn(n -1, bytes) | A User Theorem |
| fillsgn-short | ⊦ bytes ≠ [] → (fillsgn(2, int2bytes(bytes2int(bytes))) = bytes ↔ 2 ≤ # bytes ∧ (2 < # bytes → int2bytes(bytes2int(bytes)) = bytes)) | A User Theorem |
| fix-bits2bytes | ⊦ bits ≠ [] ∧ n ≠ 0 ∧ # bits ≤ 8 * (n - 1) → fix(n, bits2bytes(bits)) = bits2bytes(fillsgn(n * 8, bits)) | A User Theorem |
| fix-bits2bytes-01 | ⊦ bits ≠ [] ∧ n ≠ 0 ∧ # bits ≤ 8 * n → fix(n, bits2bytes(bits)) = bits2bytes(fillsgn(n * 8, bits)) | A User Theorem |
| fix-butlast | ⊦ 1 < # bytes ∧ n ≠ 0 → fix(n, bytes.butlast) = fix(n + 1, bytes).butlast | A User Theorem |
| fix-butlast-longer | ⊦ 1 < # bytes ∧ # bytes < n → fix(n, bytes.butlast) = fix(n, bytes).first + fix(n, bytes).butlast | A User Theorem |
| fix-empty | ⊦ fix(n, bytes) = [] ↔ n = 0 | A User Theorem |
| fix-fillsgn | ⊦ # bytes < n → fix(n, bytes) = fillsgn(n, bytes) | A User Theorem |
| fix-last | ⊦ bytes ≠ [] ∧ n ≠ 0 → fix(n, bytes).last = bytes.last | A User Theorem |
| fix-length | ⊦ # fix(n, bytes) = n | A User Theorem |
| fix-length-01 | ⊦ # bytes = n → fix(n, bytes) = bytes | A User Theorem |
| fix-neg-le | ⊦ # bytes ≤ n ∧ bytes2int(bytes) < 0 → fix(n, bytes) = mklist(i2b(~1), n - # bytes) + bytes | A User Theorem |
| fix-one | ⊦ fix(1, by ') = by ' | A User Theorem |
| fix-one-01 | ⊦ fix(1, int2bytes(i)) = int2bytes(i).last ' | A User Theorem |
| fix-pos-le | ⊦ # bytes ≤ n ∧ 0 ≤ bytes2int(bytes) → fix(n, bytes) = mklist(i2b(0), n - # bytes) + bytes | A User Theorem |
| fix-rec-neg | ⊦ b2i(bytes.first) < 0 ∧ # bytes < n ∧ bytes ≠ [] → fix(n, bytes) = i2b(~1) ' + fix(n -1, bytes) | A User Theorem |
| fix-rec-pos | ⊦ 0 ≤ b2i(bytes.first) ∧ # bytes < n ∧ bytes ≠ [] → fix(n, bytes) = i2b(0) ' + fix(n -1, bytes) | A User Theorem |
| fix-two | ⊦ fix(2, i2b(0) ') = i2b(0) ' + i2b(0) ' | A User Theorem |
| fix-two-01 | ⊦ fix(2, by ' + by0 ') = by ' + by0 ' | A User Theorem |
| fix-two-02 | ⊦ fix(2, by ' + by0 ' + by1 ') = by0 ' + by1 ' | A User Theorem |
| fix-two-03 | ⊦ fix(2, bytes).rest.butlast = [] | A User Theorem |
| fix-two-04 | ⊦ fix(2, bytes).rest ≠ [] | A User Theorem |
| fix-value | ⊦ # bytes ≤ n ∧ bytes ≠ [] → bytes2int(fix(n, bytes)) = bytes2int(bytes) | A User Theorem |
| fix2rest-last | ⊦ bytes ≠ [] → fix(2, bytes).rest = bytes.last ' | A User Theorem |
| getInt-theorem | ⊦ bor(bor(bor(b2i(by3) i<< 24, band(b2i(by2), 255) i<< 16), band(b2i(by1), 255) i<< 8), band(b2i(by0), 255)) = bytes2int(by3 ' + by2 ' + by1 ' + by0 ') | A User Theorem |
| int2bytes-butlast | ⊦ i < ~128 ∨ 128 ≤ i → int2bytes(i).butlast = int2bytes(i >> 8) | A User Theorem |
| int2bytes-byte | ~128 ≤ i, i < 128 ⊦ int2bytes((* i)) = i2b(i) ' | A User Theorem |
| int2bytes-byte-01 | ⊦ int2bytes(b2i(by)) = by ' | A User Theorem |
| int2bytes-byte-neg | ⊦ ~256 < i ∧ i < ~128 → int2bytes(i) = i2b(~1) ' + i2b(i) ' | A User Theorem |
| int2bytes-bytes2int-length | ⊦ # int2bytes(bytes2int(bytes)) = # bytes → int2bytes(bytes2int(bytes)) = bytes | A User Theorem |
| int2bytes-bytes2int-length-01 | ⊦ n ≠ 0 ∧ # bytes = n → ¬ n < # int2bytes(bytes2int(bytes)) | A User Theorem |
| int2bytes-empty | ⊦ int2bytes(i) ≠ [] | A User Theorem |
| int2bytes-fillsgn-rec | ⊦ 1 < # int2bytes(i) ∧ # int2bytes(i) ≤ n → fillsgn(n, int2bytes(i)) = fillsgn(n -1, int2bytes(i >> 8)) + i2b(i) | A User Theorem |
| int2bytes-first | ⊦ 0 ≤ i → (b2i(int2bytes(i).first) ≤ 0 ↔ b2i(int2bytes(i).first) = 0) | A User Theorem |
| int2bytes-first-neg | ⊦ i < 0 → b2i(int2bytes(i).first) < 0 | A User Theorem |
| int2bytes-first-neg-01 | ⊦ i < 0 → int2bytes(i) ≠ i2b(0) ' + bytes | A User Theorem |
| int2bytes-first-zerobyte | ⊦ 0 ≤ i → (int2bytes(i).first = i2b(0) ↔ n→i(# int2bits(i)) % 8 = 1) | A User Theorem |
| int2bytes-first-zerobyte-01 | ⊦ 0 ≤ j → (int2bytes(j).first = i2b(0) ↔ (∃ i. 0 ≤ i ∧ 2 ^ (8 * i - 1) ≤ j ∧ j < 2 ^ (8 * i))) | A User Theorem |
| int2bytes-index-rightshift | ⊦ 0 ≤ j ∧ j < n→i(# int2bytes(i)) → int2bytes(i)[i→n(j)] = i2b(i >> 8 * (n→i(# int2bytes(i)) - j + 1)) | A User Theorem |
| int2bytes-index-rightshift-01 | ⊦ 0 ≤ n ∧ n < # int2bytes(i) → int2bytes(i)[n] = i2b(i >> 8 * (n→i(# int2bytes(i)) - n→i(n) + 1)) | A User Theorem |
| int2bytes-index-rightshift-02 | ⊦ 0 < i1 ∧ i1 ≤ n→i(# int2bytes(i)) ∧ i1 ≤ 4 → int2bytes(i)[i→n(n→i(# int2bytes(i)) - i1)] = i2b(i i>> 8 * (i1 - 1)) | A User Theorem |
| int2bytes-last | 0 ≤ i, i < 128 ⊦ int2bytes((* i)).last = i2b(i) | A User Theorem |
| int2bytes-last-01 | ⊦ int2bytes(i).last = i2b(i) | A User Theorem |
| int2bytes-le127 | 0 ≤ i, i ≤ 127 ⊦ int2bytes(i) = i2b(i) ' | A User Theorem |
| int2bytes-le255 | 127 < i, i ≤ 255 ⊦ int2bytes(i) = i2b(0) ' + i2b(i - 256) ' | A User Theorem |
| int2bytes-leading-zeros | ⊦ int2bytes(i) ≠ i2b(0) ' + i2b(0) ' + bytes | A User Theorem |
| int2bytes-len-adjust | ⊦ # int2bits(i) % 8 ≠ 0 → # int2bytes(i) = # int2bits(i) / 8 + 1 | A User Theorem |
| int2bytes-len-def | ⊦ # int2bytes(i) = (# int2bits(i))-1 / 8 + 1 | A User Theorem |
| int2bytes-len-eq-neg | ⊦ i < 0 ∧ int2bytes(i).first ≠ i2b(~1) → (# int2bytes(i) = n ↔ ~(2 ^ (8 * n→i(n))) ≤ i ∧ i < ~(2 ^ (8 * (n→i(n) - 1))) ∧ n ≠ 0) | A User Theorem |
| int2bytes-len-eq-neg-01 | ⊦ int2bytes(i).first = i2b(~1) → (# int2bytes(i) = n ↔ ~(2 ^ (8 * n→i(n) - 1)) ≤ i ∧ i < ~(2 ^ (8 * (n→i(n) - 1) - 1)) ∧ n ≠ 0) | A User Theorem |
| int2bytes-len-eq-pos | ⊦ 0 ≤ i ∧ int2bytes(i).first = i2b(0) → (# int2bytes(i) = n ↔ 2 ^ ((n→i(n) - 1) * 8 - 1) ≤ i ∧ i < 2 ^ ((n→i(n) - 1) * 8) ∧ 0 < n) | A User Theorem |
| int2bytes-len-fits | ⊦ # int2bits(i) % 8 = 0 → # int2bytes(i) = # int2bits(i) / 8 | A User Theorem |
| int2bytes-len-le | ⊦ 0 ≤ i ∧ int2bytes(i).first ≠ i2b(0) → (n ≤ # int2bytes(i) ↔ 2 ^ ((n→i(n) - 1) * 8) ≤ i) | A User Theorem |
| int2bytes-len-le-01 | ⊦ 0 ≤ i ∧ int2bytes(i).first = i2b(0) → (n ≤ # int2bytes(i) ↔ 2 ^ ((n→i(n) - 1) * 8 - 1) ≤ i) | A User Theorem |
| int2bytes-len-le-neg | ⊦ i < 0 ∧ int2bytes(i).first ≠ i2b(~1) → (n ≤ # int2bytes(i) ↔ i < ~(2 ^ (8 * (n→i(n) - 1)))) | A User Theorem |
| int2bytes-len-le-neg-01 | ⊦ int2bytes(i).first = i2b(~1) → (n ≤ # int2bytes(i) ↔ i < ~(2 ^ (8 * (n→i(n) - 1) - 1))) | A User Theorem |
| int2bytes-len-le-neg-02 | ⊦ i < 0 ∧ int2bytes(i).first ≠ i2b(~1) → (# int2bytes(i) ≤ n ↔ ~(2 ^ (8 * n→i(n))) ≤ i) | A User Theorem |
| int2bytes-len-le-neg-03 | ⊦ int2bytes(i).first = i2b(~1) → (# int2bytes(i) ≤ n ↔ ~(2 ^ (8 * n→i(n) - 1)) ≤ i) | A User Theorem |
| int2bytes-len-le-upper | ⊦ 0 ≤ i ∧ int2bytes(i).first = i2b(0) → (# int2bytes(i) ≤ n ↔ i < 2 ^ (n→i(n) * 8 - 1)) | A User Theorem |
| int2bytes-len-ls | ⊦ 0 ≤ i ∧ int2bytes(i).first ≠ i2b(0) → (n < # int2bytes(i) ↔ 2 ^ (n→i(n) * 8) ≤ i) | A User Theorem |
| int2bytes-len-ls-01 | ⊦ 0 ≤ i ∧ int2bytes(i).first = i2b(0) → (n < # int2bytes(i) ↔ 2 ^ (n→i(n) * 8)-1 ≤ i) | A User Theorem |
| int2bytes-len-ls-03 | ⊦ 0 ≤ i ∧ int2bytes(i).first ≠ i2b(0) → (# int2bytes(i) < n ↔ i < 2 ^ ((n→i(n) - 1) * 8)) | A User Theorem |
| int2bytes-len-ls-04 | ⊦ 0 ≤ i ∧ int2bytes(i).first = i2b(0) → (# int2bytes(i) < n ↔ i < 2 ^ ((n→i(n) - 1) * 8 - 1)) | A User Theorem |
| int2bytes-len-ls-neg | ⊦ i < 0 ∧ int2bytes(i).first ≠ i2b(~1) → (n < # int2bytes(i) ↔ i < ~(2 ^ (8 * n→i(n)))) | A User Theorem |
| int2bytes-len-ls-neg-01 | ⊦ int2bytes(i).first = i2b(~1) → (n < # int2bytes(i) ↔ i < ~(2 ^ (8 * n→i(n) - 1))) | A User Theorem |
| int2bytes-len-ls-neg-02 | ⊦ i < 0 ∧ int2bytes(i).first ≠ i2b(~1) → (# int2bytes(i) < n ↔ ~(2 ^ (8 * (n→i(n) - 1))) ≤ i) | A User Theorem |
| int2bytes-len-ls-neg-03 | ⊦ int2bytes(i).first = i2b(~1) → (# int2bytes(i) < n ↔ ~(2 ^ (8 * (n→i(n) - 1) - 1)) ≤ i) | A User Theorem |
| int2bytes-len-ls-upper | ⊦ 0 ≤ i ∧ int2bytes(i).first ≠ i2b(0) → (# int2bytes(i) ≤ n ↔ i < 2 ^ (n→i(n) * 8)) | A User Theorem |
| int2bytes-len-neg | ~(2 ^ (8 * (i + 1) - 1)) ≤ j, j ≤ ~(2 ^ (8 * i)), 0 ≤ i ⊦ # int2bytes(j) = i→n(i + 1) | A User Theorem |
| int2bytes-len-neg-01 | ~(2 ^ (8 * (i + 1))) < j, j < ~(2 ^ (8 * (i + 1) - 1)), 0 ≤ i ⊦ # int2bytes(j) = i→n(i + 2) | A User Theorem |
| int2bytes-len-neg256 | ⊦ ~256 ≤ i ∧ i < ~128 → # int2bytes(i) = 2 | A User Theorem |
| int2bytes-len-one | ⊦ int2bytes(i) = by ' ↔ i = b2i(by) | A User Theorem |
| int2bytes-len-one-01 | ⊦ # int2bytes(i) = 1 ↔ int2bytes(i) = i2b(i) ' | A User Theorem |
| int2bytes-len-pos | 0 ≤ i, 2 ^ (8 * i) ≤ j, j < 2 ^ (8 * (i + 1) - 1) ⊦ # int2bytes(j) = i→n(i + 1) | A User Theorem |
| int2bytes-len-pos-01 | 0 ≤ i, 2 ^ (8 * (i + 1) - 1) ≤ j, j < 2 ^ (8 * (i + 1)) ⊦ # int2bytes(j) = i→n(i + 2) | A User Theorem |
| int2bytes-minus-256 | ⊦ int2bytes(~256) = i2b(~1) ' + i2b(0) ' | A User Theorem |
| int2bytes-minus-256-01 | ⊦ i = ~256 → int2bytes(i) = i2b(~1) ' + i2b(0) | A User Theorem |
| int2bytes-minus-one | ⊦ int2bytes(i) = i2b(~1) ' ↔ i = ~1 | A User Theorem |
| int2bytes-not-neg | ⊦ 0 ≤ i ∧ b2i(bytes.first) < 0 → int2bytes(i) ≠ bytes | A User Theorem |
| int2bytes-not-neg-01 | ⊦ 0 ≤ i → int2bytes(i) ≠ i2b(~1) ' + bytes | A User Theorem |
| int2bytes-one | ⊦ # int2bytes(i) = 1 → ~128 ≤ i ∧ i ≤ 127 | A User Theorem |
| int2bytes-one-01 | ⊦ ¬ i ≤ 127 → # int2bytes(i) ≠ 1 | A User Theorem |
| int2bytes-one-02 | ⊦ ¬ ~128 ≤ i → # int2bytes(i) ≠ 1 | A User Theorem |
| int2bytes-rec-case | ⊦ int2bytes(i) = (~128 ≤ i ∧ i < 128 ⊃ i2b(i) ' ;(128 ≤ i ∧ i < 256 ⊃ i2b(0) ' + i2b(i - 256) ' ;(~256 < i ∧ i < ~128 ⊃ i2b(~1) ' + i2b(i) ' ;(i < ~256 ∧ i % 256 = 0 ⊃ int2bytes(i / 256) + int2bytes(i % 256).last ' ;(i < ~256 ∧ i % 256 ≠ 0 ⊃ int2bytes(i / 256 - 1) + int2bytes(i % 256).last ';int2bytes(i / 256) + int2bytes(i % 256).last ') ) ) ) ) | A User Theorem |
| int2bytes-rec-neg-01 | j < ~(2 ^ (i * 8)), 0 < i, j % 2 ^ (i * 8) = 0 ⊦ int2bytes(j) = int2bytes(j / 2 ^ (i * 8)) + fix(i→n(i + 1), int2bytes(j % 2 ^ (i * 8))).rest | A User Theorem |
| int2bytes-rec-neg-02 | j < ~(2 ^ (i * 8)), 0 < i, j % 2 ^ (i * 8) ≠ 0 ⊦ int2bytes(j) = int2bytes(j / 2 ^ (i * 8) - 1) + fix(i→n(i + 1), int2bytes(j % 2 ^ (i * 8))).rest | A User Theorem |
| int2bytes-rec-neg-03 | j < ~(2 ^ (i * 8)), 0 < i ⊦ int2bytes(j) = int2bytes((j - (2 ^ (i * 8) - 1)) / 2 ^ (i * 8)) + fix(i→n(i + 1), int2bytes(j % 2 ^ (i * 8))).rest | A User Theorem |
| int2bytes-rec-neg-04 | j < ~(2 ^ (i * 8 - 1)), 0 < i, j % 2 ^ (i * 8) = 0 ⊦ int2bytes(j) = int2bytes(j / 2 ^ (i * 8)) + fix(i→n(i + 1), int2bytes(j % 2 ^ (i * 8))).rest | A User Theorem |
| int2bytes-rec-neg-05 | j < ~(2 ^ (i * 8 - 1)), 0 < i, j % 2 ^ (i * 8) ≠ 0 ⊦ int2bytes(j) = int2bytes(j / 2 ^ (i * 8) - 1) + fix(i→n(i + 1), int2bytes(j % 2 ^ (i * 8))).rest | A User Theorem |
| int2bytes-rec-neg-06 | j < ~(2 ^ (i * 8 - 1)), 0 < i ⊦ int2bytes(j) = int2bytes((j - (2 ^ (i * 8) - 1)) / 2 ^ (i * 8)) + fix(i→n(i + 1), int2bytes(j % 2 ^ (i * 8))).rest | A User Theorem |
| int2bytes-rec-neg-256 | ⊦ i < ~256 ∧ i % 256 = 0 → int2bytes(i) = int2bytes(i / 256) + int2bytes(i % 256).last ' | A User Theorem |
| int2bytes-rec-neg-256-01 | ⊦ i < ~256 ∧ i % 256 ≠ 0 → int2bytes(i) = int2bytes(i / 256 - 1) + int2bytes(i % 256).last ' | A User Theorem |
| int2bytes-rec-pos | 255 < i ⊦ int2bytes(i) = int2bytes(i / 256) + int2bytes(i % 256).last ' | A User Theorem |
| int2bytes-rec-pos-01 | 255 < i, i % 256 = 0 ⊦ int2bytes(i) = int2bytes(i / 256) + i2b(0) ' | A User Theorem |
| int2bytes-rec-pos-02 | 255 < i, i % 256 < 128 ⊦ int2bytes(i) = int2bytes(i / 256) + int2bytes(i % 256) | A User Theorem |
| int2bytes-rec-pos-03 | 255 < i, 128 ≤ i % 256 ⊦ int2bytes(i) = int2bytes(i / 256) + int2bytes(i % 256).rest | A User Theorem |
| int2bytes-rec-pos-04 | 256 ≤ i ⊦ int2bytes(i) = int2bytes(i / 256) + fix(i→n(2), int2bytes(i % 256)).rest | A User Theorem |
| int2bytes-rec-pos-any | 2 ^ (i * 8) ≤ j, 0 < i ⊦ int2bytes(j) = int2bytes(j / 2 ^ (i * 8)) + fix(i→n(i + 1), int2bytes(j % 2 ^ (i * 8))).rest | A User Theorem |
| int2bytes-rec-shift | ⊦ i < ~128 ∨ 128 ≤ i → int2bytes(i) = int2bytes(i >> 8) + i2b(i) | A User Theorem |
| int2bytes-rec255-neg | ⊦ i < ~ 128 → int2bytes(i) = int2bytes((i - 255) / 256) + int2bytes(i % 256).last ' | A User Theorem |
| int2bytes-zero | ⊦ int2bytes(i) = i2b(0) ' ↔ i = 0 | A User Theorem |
| int2int | ⊦ bytes2int(int2bytes(i)) = i | A User Theorem |
| int2int-fillsgn | ⊦ bytes2int(fillsgn(n, int2bytes(i))) = i | A User Theorem |
| int2int-pos | ⊦ 0 ≤ i → bytes2int(int2bytes(i)) = i | A User Theorem |
| intrightshift-8 | ⊦ 1 < # int2bytes(i) → i i>> 8 = bytes2int(int2bytes(i).butlast) | A User Theorem |
| no-leading-zero | ⊦ int2bytes(bytes2int(bytes)) = bytes ∧ 1 < # bytes ∧ bytes.first = i2b(0) → b2i(bytes.rest.first) < 0 | A User Theorem |
| no-leading-zero-01 | ⊦ 0 ≤ b2i(by) → int2bytes(i) ≠ i2b(0) ' + by ' + bytes | A User Theorem |
| no-leading-zero-02 | ⊦ bytes ≠ [] ∧ bytes.first ≠ i2b(0) ∧ bytes.first ≠ i2b(~1) → int2bytes(bytes2int(bytes)) = bytes | A User Theorem |
| no-leading-zero-03 | ⊦ 2 ≤ # bytes ∧ bytes.first = i2b(0) ∧ b2i(bytes.rest.first) < 0 → int2bytes(bytes2int(bytes)) = bytes | A User Theorem |
| no-leading-zero-04 | ⊦ b2i(by) < 0 → int2bytes(i) ≠ i2b(~1) ' + by ' + bytes | A User Theorem |
| no-leading-zeros | ⊦ int2bytes(bytes2int(bytes)) = bytes ∧ 1 < # bytes → ¬(bytes.first = i2b(0) ∧ bytes.rest.first = i2b(0)) | A User Theorem |
| rightshift-8 | ⊦ 1 < # int2bytes(i) → i >> 8 = bytes2int(int2bytes(i).butlast) | A User Theorem |
| rightshift-8-01 | ⊦ i→n(j) < # int2bytes(i) → i >> 8 * j = bytes2int(firstn(# int2bytes(i) - i→n(j), int2bytes(i))) | A User Theorem |
| rightshift-8-01-01 | ⊦ i >> 8 * j = bytes2int(firstn(# int2bytes(i), fillsgn(i→n(j) + # int2bytes(i), int2bytes(i)))) | A User Theorem |
| rightshift-8-02 | ⊦ i >> 8 = bytes2int(fillsgn(2, int2bytes(i)).butlast) | A User Theorem |
| setInt-theorem | ⊦ ¬(by = i2b(i i>> 24) ∧ by0 = i2b(i i>> 16) ∧ by1 = i2b(i i>> 8) ∧ by2 = i2b(i)) → fillsgn(4, int2bytes(i)) ≠ by ' + by0 ' + by1 ' + by2 ' | A User Theorem |
| setShort-theorem | ⊦ ¬(by0 = i2b(s2i(sho)) ∧ by = i2b(s2i(sho) i>> 8)) → fillsgn(2, int2bytes(s2i(sho))) ≠ by ' + by0 ' | A User Theorem |
| setShort-theorem-01 | ⊦ fillsgn(2, int2bytes(s2i(sho))) = i2b(s2i(sho) i>> 8) + i2b(s2i(sho)) | A User Theorem |
| setShortInt-theorem | ⊦ i ∈short → fillsgn(2, int2bytes(i)) = i2b(i i>> 8) ' + i2b(i) | A User Theorem |
| short-2bytes | ⊦ s2i(i2s(bytes2int(by ' + by0 '))) = bytes2int(by ' + by0 ') | A User Theorem |
| short-2bytes-01 | ⊦ ¬ 65536 ≤ bytes2int(by ' + by0 ') + s2i(sho) | A User Theorem |
| short-2bytes-02 | ⊦ 0 ≤ i → ¬ 32768 + i < bytes2int(by ' + by0 ') | A User Theorem |
| short-2bytes-03 | ⊦ ¬ 32768 < bytes2int(by ' + by0 ') | A User Theorem |