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: |
|---|---|---|
| ibi | ⊦ i2b(b2i(by)) = by | An Axiom |
| isi | ⊦ i2s(s2i(sho)) = sho | An Axiom |
| sis-in | ⊦ i ∈short → s2i(i2s(i)) = i | An Axiom |
| bib-in | ⊦ i ∈byte → b2i(i2b(i)) = i | An Axiom |
| inshort | ⊦ i ∈short ↔ ~32768 ≤ i ∧ i ≤ 32767 | An Axiom |
| inbyte | ⊦ i ∈byte ↔ ~128 ≤ i ∧ i ≤ 127 | An Axiom |
| short2byte | ⊦ s2b(sho) = i2b(s2i(sho)) | An Axiom |
| byte2short | ⊦ b2s(by) = i2s(b2i(by)) | An Axiom |
| int2short-out | ⊦ ¬ i ∈short → i2s(i) = i2s(bits2int(lastn(16, int2bits(i)))) | An Axiom |
| int2byte-out | ⊦ ¬ i ∈byte → i2b(i) = i2b(bits2int(lastn(8, int2bits(i)))) | An Axiom |
| short2int-in | ⊦ s2i(sho) ∈short | An Axiom |
| byte2int-in | ⊦ b2i(by) ∈byte | An Axiom |
| zero-short | ⊦ 0s = i2s(0) | An Axiom |
| zero-byte | ⊦ 0b = i2b(0) | An Axiom |
| short2bint | ⊦ s2bi(sho) = i2bi(s2i(sho)) | An Axiom |
| byte2bint | ⊦ b2bi(by) = i2bi(b2i(by)) | An Axiom |
| int2bint-out | ⊦ ¬ i ∈bint → i2bi(i) = i2bi(bits2int(lastn(32, int2bits(i)))) | An Axiom |
| biibi-in | ⊦ i ∈bint → bi2i(i2bi(i)) = i | An Axiom |
| bint2int-in | ⊦ bi2i(bi) ∈bint | An Axiom |
| ibii | ⊦ i2bi(bi2i(bi)) = bi | An Axiom |
| inbint | ⊦ i ∈bint ↔ ~2147483648 ≤ i ∧ i ≤ 2147483647 | An Axiom |
| zero-bint | ⊦ 0bi = i2bi(0) | An Axiom |
| int2long-out | ⊦ ¬ i ∈long → i2l(i) = i2l(bits2int(lastn(64, int2bits(i)))) | An Axiom |
| lib-in | ⊦ i ∈long → l2i(i2l(i)) = i | An Axiom |
| long2int-in | ⊦ l2i(lo) ∈long | An Axiom |
| ili | ⊦ i2l(l2i(lo)) = lo | An Axiom |
| inlong | ⊦ i ∈long ↔ ~(2 ^ 63) ≤ i ∧ i ≤ 2 ^ 63 - 1 | An Axiom |
| zero-long | ⊦ 0l = i2l(0) | An Axiom |
| unsigned-short | ⊦ us2i(sho) = bits2int(false ' + fillsgn(16, int2bits(s2i(sho)))) | An Axiom |
| unsigned-byte | ⊦ ub2i(by) = bits2int(false ' + fillsgn(8, int2bits(b2i(by)))) | An Axiom |
| shortOverflow | ⊦ shortOverflow(i) ↔ ¬ i ∈short | An Axiom |
| Byte-and-range | ⊦ 0 ≤ band(b2i(by), 255) ∧ band(b2i(by), 255) < 256 | A User Theorem |
| b2i-i2b-same | ⊦ b2i(by) = i → by = i2b(i) | A User Theorem |
| band-011x | ⊦ abs(band(255, b2i(by))) = band(255, b2i(by)) | A User Theorem |
| band-011x-01 | ⊦ 0 < b2i(by) → ¬ 128 ≤ band(255, b2i(by)) | A User Theorem |
| band-bib | ⊦ i ∈byte ∧ j ∈byte → b2i(i2b(band(i, j))) = band(i, j) | A User Theorem |
| band-ff | ⊦ band(b2i(by), 255) = ub2i(by) | A User Theorem |
| band-sis | ⊦ i ∈short ∧ j ∈short → s2i(i2s(band(i, j))) = band(i, j) | A User Theorem |
| bcompl-bib | ⊦ i ∈byte → b2i(i2b(bcompl(i))) = bcompl(i) | A User Theorem |
| bcompl-sis | ⊦ i ∈short → s2i(i2s(bcompl(i))) = bcompl(i) | A User Theorem |
| bib-64 | ⊦ b2i(i2b(64)) = 64 | A User Theorem |
| bib-bitlength | ⊦ # int2bits(i) ≤ 8 → b2i(i2b(i)) = i | A User Theorem |
| bib-in-01 | ⊦ ~128 ≤ i ∧ i ≤ 127 → b2i(i2b(i)) = i | A User Theorem |
| bib-lower | ⊦ ~256 < i ∧ i < ~128 → b2i(i2b(i)) = i + 256 | A User Theorem |
| bib-ls-same | ⊦ i < b2i(i2b(i)) ↔ i < ~128 | A User Theorem |
| bib-ls-same-01 | ⊦ b2i(i2b(i)) < i ↔ 128 ≤ i | A User Theorem |
| bib-neg-high | ⊦ i < 0 ∧ ~128 ≤ i % 256 → b2i(i2b(i)) = i % 256 | A User Theorem |
| bib-neg-low | ⊦ i < 0 ∧ i % 256 < ~128 → b2i(i2b(i)) = i % 256 + 256 | A User Theorem |
| bib-on-bits | ⊦ b2i(i2b(i)) = bits2int(lastn(8, fillsgn(8, int2bits(i)))) | A User Theorem |
| bib-pos-high | ⊦ 0 ≤ i ∧ 127 < i % 256 → b2i(i2b(i)) = i % 256 - 256 | A User Theorem |
| bib-pos-low | ⊦ 0 ≤ i ∧ i % 256 ≤ 127 → b2i(i2b(i)) = i % 256 | A User Theorem |
| bib-upper | ⊦ 127 < i ∧ i < 256 → b2i(i2b(i)) = i - 256 | A User Theorem |
| bint-2pot31 | ⊦ bi2i(i2bi(2147483648)) = ~2147483648 | A User Theorem |
| bint-and-011x-bits2unit | ⊦ i ∈bint → (bits2uint(fillsgn(32, int2bits(i))) ≠ band(4294967295, i) ↔ false) | A User Theorem |
| bint-band-011x | ⊦ i ∈bint ∧ 0 ≤ i → band(4294967295, i) = i | A User Theorem |
| bint-band-011x-neg | ⊦ i ∈bint ∧ i < 0 → band(4294967295, i) = i + 4294967296 | A User Theorem |
| bint-band-and-nlsz | ⊦ ¬ band(4294967295, i) + band(4294967295, j) < 0 | A User Theorem |
| bint-band-one | ⊦ band(j, 1) ∈bint | A User Theorem |
| bint-band-one-01 | ⊦ bi2i(i2bi(band(j, 1))) = band(j, 1) | A User Theorem |
| bint-band-zero | ⊦ i ∈bint → (band(4294967295, i) = 0 ↔ i = 0) | A User Theorem |
| bint-byte | ⊦ bi2i(i2bi(b2i(by))) = b2i(by) | A User Theorem |
| bint-carry | ⊦ 0 ≤ i0 ∧ i0 ≤ 1 → ((i0 + band(4294967295, i) + band(4294967295, j)) l>>> 32)∈bint | A User Theorem |
| bint-carry-01 | ⊦ ((band(4294967295, i) + band(4294967295, j)) l>>> 32)∈bint | A User Theorem |
| bint-div2 | ⊦ 0 < j0 ∧ j0 ≤ j ∧ j ∈bint → (j0 / 2)∈bint | A User Theorem |
| bint-div2-01 | ⊦ 0 < j0 ∧ j0 ≤ j ∧ j ∈bint → bi2i(i2bi(j0 / 2)) = j0 / 2 | A User Theorem |
| bint-eq | ⊦ bi2i(i2bi(i)) ≠ bi2i(i2bi(j)) → i2bi(i) ≠ i2bi(j) | A User Theorem |
| bint-equal | ⊦ bi2i(bi) = i → (i2bi(i) ≠ bi ↔ false) | A User Theorem |
| bint-fillsgn-len | ⊦ i ∈bint → # fillsgn(32, int2bits(i)) = 32 | A User Theorem |
| bint-is-cast | ⊦ bi2i(i2bi(i)) = cast(32, i) | A User Theorem |
| bint-is-cast-01 | ⊦ i2bi(i) = i2bi(cast(32, i)) | A User Theorem |
| bint-mod | ⊦ j ∈bint ∧ j ≠ 0 → (i % j)∈bint | A User Theorem |
| bint-mult2 | ⊦ 0 < j0 ∧ j0 * 2 ≤ j ∧ j ∈bint → bi2i(i2bi(j0)) = j0 | A User Theorem |
| bint-num | 2147483648 ≤ i ⊦ ¬ (* i) ∈bint | A User Theorem |
| bint-num-01 | i < ~2147483648 ⊦ ¬ (* i) ∈bint | A User Theorem |
| bint-num-02 | j ≤ ~2147483648 ⊦ i < (* j) → ¬ i ∈bint | A User Theorem |
| bint-num-03 | 2147483648 ≤ j ⊦ (* j) ≤ i → ¬ i ∈bint | A User Theorem |
| bint-num-04 | ~2147483648 ≤ i, i < 2147483648 ⊦ (* i) ∈bint | A User Theorem |
| bint-num-in | ~2147483648 ≤ i, i < 2147483648 ⊦ bi2i(i2bi((* i))) = i | A User Theorem |
| bint-pred | ⊦ 0 < i ∧ i ∈bint → bi2i(i2bi(i - 1)) = i - 1 | A User Theorem |
| bint-pred-01 | ⊦ 0 < i ∧ i ∈bint → (¬ (i - 1)∈bint ↔ false) | A User Theorem |
| bint-pred-02 | ⊦ 0 ≤ i ∧ i ∈bint → bi2i(i2bi(i - 1)) = i - 1 | A User Theorem |
| bint-short | ⊦ bi2i(i2bi(s2i(sho))) = s2i(sho) | A User Theorem |
| bint-succ-notin | ⊦ i ∈bint ∧ ¬ (i + 1)∈bint → bi2i(i2bi(1 + i)) = ~(2 ^ 31) | A User Theorem |
| bint-trans-pos | ⊦ j ∈bint ∧ 0 < i ∧ i ≤ j → (¬ i ∈bint ↔ false) | A User Theorem |
| bint-trans-pos-01 | ⊦ j ∈bint ∧ 0 ≤ i ∧ i ≤ j → (¬ i ∈bint ↔ false) | A User Theorem |
| bint-trans-pos-02 | ⊦ j ∈bint ∧ 0 ≤ i ∧ i < j → (¬ i ∈bint ↔ false) | A User Theorem |
| bint-trans-pos-03 | ⊦ j ∈bint ∧ 0 < i ∧ i < j → (¬ i ∈bint ↔ false) | A User Theorem |
| bint-trans-pos-04 | ⊦ 0 < j0 ∧ j0 ≤ j ∧ j ∈bint → j0 ∈bint | A User Theorem |
| bint-unsigned | ⊦ 2 ^ 31 ≤ i ∧ i < 2 ^ 32 → i2bi(i) = i2bi(i - 2 ^ 32) | A User Theorem |
| bint-unsigned-01 | ⊦ 2 ^ 31 ≤ i ∧ i < 2 ^ 32 → bi2i(i2bi(i)) = i - 2 ^ 32 | A User Theorem |
| bor-bib | ⊦ i ∈byte ∧ j ∈byte → b2i(i2b(bor(i, j))) = bor(i, j) | A User Theorem |
| bor-sis | ⊦ i ∈short ∧ j ∈short → s2i(i2s(bor(i, j))) = bor(i, j) | A User Theorem |
| byte | ⊦ b2i(i2b(0)) = 0 | A User Theorem |
| byte-01 | ⊦ b2i(i2b(~(1 + 1 + 1 + 1))) = ~(1 + 1 + 1 + 1) | A User Theorem |
| byte-011x-ib | ⊦ i2b(band(255, b2i(by))) = by | A User Theorem |
| byte-011x-neg | ⊦ b2i(by) < 0 → band(b2i(by), 255) = b2i(by) + 256 | A User Theorem |
| byte-011x-pos | ⊦ 0 ≤ b2i(by) → band(b2i(by), 255) = b2i(by) | A User Theorem |
| byte-011x-pos-01 | ⊦ 0 ≤ i ∧ i < 128 → (band(b2i(by), 255) = i ↔ b2i(by) = i) | A User Theorem |
| byte-011x-pos-02 | 0 ≤ i, i < 128 ⊦ band(b2i(by), 255) = (* i) ↔ b2i(by) = i | A User Theorem |
| byte-011x-unsgn | ⊦ 0 ≤ i ∧ i < 256 → band(255, b2i(i2b(i))) = i | A User Theorem |
| byte-02 | ⊦ b2i(i2b(~(1 + 1 + 1 + 1 + 1))) = ~(1 + 1 + 1 + 1 + 1) | A User Theorem |
| byte-03 | ⊦ b2i(i2b(~ 1)) = ~ 1 | A User Theorem |
| byte-04 | ⊦ b2i(i2b(1 + 1)) = 1 + 1 | A User Theorem |
| byte-127 | ⊦ 126 < b2i(by) ↔ b2i(by) = 127 | A User Theorem |
| byte-add-256 | ⊦ i2b(i + 256) = i2b(i) | A User Theorem |
| byte-add-256-01 | ⊦ i2b(~(i + 256)) = i2b(~ i) | A User Theorem |
| byte-and-255 | ⊦ band(255, b2i(by)) ≤ 0 ↔ by = i2b(0) | A User Theorem |
| byte-and-le-256 | ⊦ ¬ 256 ≤ band(b2i(by), 255) | A User Theorem |
| byte-and-lsz | ⊦ ¬ band(b2i(by), 255) < 0 | A User Theorem |
| byte-bitlength | ⊦ # int2bits(b2i(by)) ≤ 8 | A User Theorem |
| byte-bitlength-01 | ⊦ 8 < n → ¬ n ≤ # int2bits(b2i(by)) | A User Theorem |
| byte-equal | ⊦ b2i(byi) = b2i(byj) ↔ byi = byj | A User Theorem |
| byte-equal-01 | ⊦ b2i(by) = i → (i2b(i) ≠ by ↔ false) | A User Theorem |
| byte-gr-127 | ⊦ ¬ 127 < b2i(by) | A User Theorem |
| byte-in | ⊦ 0 ≤ i ∧ i ≤ 127 → b2i(i2b(i)) = i | A User Theorem |
| byte-is-cast | ⊦ b2i(i2b(i)) = cast(8, i) | A User Theorem |
| byte-is-cast-01 | ⊦ i2b(i) = i2b(cast(8, i)) | A User Theorem |
| byte-law-add | ⊦ i2b(i + j) = i2b(b2i(i2b(i)) + b2i(i2b(j))) | A User Theorem |
| byte-law-add-one | ⊦ i2b(i + j) = i2b(b2i(i2b(i)) + j) | A User Theorem |
| byte-law-add-pos | ⊦ 0 ≤ i ∧ 0 ≤ j → i2b(i + j) = i2b(b2i(i2b(i)) + j) | A User Theorem |
| byte-law-and-one | ⊦ i2b(band(i, j)) = i2b(band(b2i(i2b(i)), j)) | A User Theorem |
| byte-law-compl | ⊦ i2b(bcompl(i)) = i2b(bcompl(b2i(i2b(i)))) | A User Theorem |
| byte-law-div-not | ⊦ (i = 256 ∧ j = 64 → i2b(i / j) ≠ i2b(b2i(i2b(i)) / j)) ∧ (i = ~128 ∧ j = 128 → i2b(i / j) ≠ i2b(i / b2i(i2b(j)))) ∧ (i = 256 ∧ j = 128 → i2b(i / j) ≠ i2b(b2i(i2b(i)) / b2i(i2b(j)))) ∧ (i = 258 ∧ j = 43 → i2b(i % j) ≠ i2b(b2i(i2b(i)) % j)) ∧ (i = 1 ∧ j = 255 → i2b(i % j) ≠ i2b(i % b2i(i2b(j)))) ∧ (i = 509 ∧ j = 255 → i2b(i % j) ≠ i2b(b2i(i2b(i)) % b2i(i2b(j)))) | A User Theorem |
| byte-law-leftshift | ⊦ i2b(i i<< j) = i2b(b2i(i2b(i)) i<< j) | A User Theorem |
| byte-law-ls-not | ⊦ (i = 127 ∧ j = 128 → ¬(i < j → b2i(i2b(i)) < b2i(i2b(j)))) ∧ (i = 128 ∧ j = 1 → ¬(b2i(i2b(i)) < b2i(i2b(j)) → i < j)) ∧ (i = 255 ∧ j = ~1 → ¬(b2i(i2b(i)) = b2i(i2b(j)) → i = j)) | A User Theorem |
| byte-law-mult | ⊦ i2b(i * j) = i2b(b2i(i2b(i)) * b2i(i2b(j))) | A User Theorem |
| byte-law-mult-one | ⊦ i2b(i * j) = i2b(b2i(i2b(i)) * j) | A User Theorem |
| byte-law-neg | ⊦ i2b(~ i) = i2b(~ b2i(i2b(i))) | A User Theorem |
| byte-law-righthift-not | ⊦ (i = 128 ∧ j = 1 → i2b(i i>> j) ≠ i2b(b2i(i2b(i)) i>> j)) ∧ (i = 128 ∧ j = 1 → i2b(i i>>> j) ≠ i2b(b2i(i2b(i)) i>>> j)) | A User Theorem |
| byte-law-sub | ⊦ i2b(i - j) = i2b(b2i(i2b(i)) - b2i(i2b(j))) | A User Theorem |
| byte-law-sub-one | ⊦ i2b(i - j) = i2b(b2i(i2b(i)) - j) | A User Theorem |
| byte-law-sub-one-01 | ⊦ i2b(i - j) = i2b(i - b2i(i2b(j))) | A User Theorem |
| byte-le | ⊦ b2i(by) ≤ 127 | A User Theorem |
| byte-le-256 | ⊦ ¬ 256 ≤ b2i(by) | A User Theorem |
| byte-len | ⊦ ¬ 8 < # int2bits(b2i(by)) | A User Theorem |
| byte-length | b2i(by) ≠ ~128 ⊦ # int2bits(b2i(by)) ≤ 8 | A User Theorem |
| byte-ls-127 | ⊦ b2i(by) < ~127 ↔ b2i(by) = ~128 | A User Theorem |
| byte-ls-256 | ⊦ ¬ b2i(by) < ~256 | A User Theorem |
| byte-min | ⊦ b2i(by) ≤ ~128 ↔ b2i(by) = ~128 | A User Theorem |
| byte-mod-100x | ⊦ b2i(by) % 256 = b2i(by) | A User Theorem |
| byte-mod-100x-01 | ⊦ (b2i(by) + 1) % 256 = b2i(by) + 1 | A User Theorem |
| byte-mult | ⊦ i2b(i * 256) = i2b(0) | A User Theorem |
| byte-mult-01 | ⊦ i2b(~(i * 256)) = i2b(0) | A User Theorem |
| byte-mult-256 | ⊦ i2b(i * 256 + j) = i2b(j) | A User Theorem |
| byte-mult-256-01 | ⊦ i2b(~(i * 256 + j)) = i2b(~ j) | A User Theorem |
| byte-mult-neg | ⊦ i < 0 ∧ j < 0 → i2b(i * 256 + j) = i2b(j) | A User Theorem |
| byte-mult-pos | ⊦ 0 ≤ i ∧ 0 ≤ j → i2b(i * 256 + j) = i2b(j) | A User Theorem |
| byte-neq | i < ~128 ⊦ (* i) ≠ b2i(by) | A User Theorem |
| byte-nge | i ≥ 128 ⊦ ¬ (* i) ≤ b2i(by) | A User Theorem |
| byte-ngr | i ≥ 127 ⊦ ¬ (* i) < b2i(by) | A User Theorem |
| byte-ngr-01 | ⊦ ¬ 128 < abs(b2i(by)) | A User Theorem |
| byte-nle | ⊦ ¬ 256 ≤ abs(b2i(by)) | A User Theorem |
| byte-nle-01 | ⊦ ¬ 256 ≤ abs(b2i(by) + 1) | A User Theorem |
| byte-nle-02 | i < ~128 ⊦ ¬ b2i(by) ≤ (* i) | A User Theorem |
| byte-nls | ⊦ ¬ b2i(by) < ~128 | A User Theorem |
| byte-nls-01 | i ≤ ~128 ⊦ ¬ b2i(by) < (* i) | A User Theorem |
| byte-nls-02 | ⊦ 128 ≤ i → ¬ i + b2i(by) < 0 | A User Theorem |
| byte-not-max | ⊦ 126 < b2i(by) ∧ 0 < i → ¬ b2i(by) + i < 128 | A User Theorem |
| byte-range | ⊦ ~128 ≤ b2i(by) ∧ b2i(by) ≤ 127 | A User Theorem |
| byte-short-neq | ⊦ i2b(i) ≠ i2b(j) → i2s(i) ≠ i2s(j) | A User Theorem |
| byte-sis | ⊦ i2b(s2i(i2s(i))) = i2b(i) | A User Theorem |
| byte-size | ⊦ ¬ 128 < 2 ^ (n→i(# int2bits(b2i(by))) - 1) | A User Theorem |
| byte-size-01 | ⊦ ¬ 32768 < 2 ^ (n→i(# int2bits(b2i(by))) - 1) | A User Theorem |
| byte-succ | i < 127 ⊦ 0 ≤ b2i(by) ∧ b2i(by) ≤ (* i) → b2i(i2b(b2i(by) + 1)) = b2i(by) + 1 | A User Theorem |
| byte-unsigned | ⊦ 128 ≤ i ∧ i < 256 → i2b(i) = i2b(i - 256) | A User Theorem |
| cast-b2i | ⊦ cast(8, b2i(by)) = b2i(by) | A User Theorem |
| cast-b2i-01 | ⊦ 8 ≤ i → cast(i, b2i(by)) = b2i(by) | A User Theorem |
| div-inshort | ⊦ s2i(sho1) ≠ 0 → ((s2i(sho0) / s2i(sho1))∈short ↔ ¬(s2i(sho1) = ~1 ∧ s2i(sho0) = ~32768)) | A User Theorem |
| ex256 | ⊦ j = j / 256 * 256 + j % 256 | A User Theorem |
| fits-law-add | ⊦ b2i(by1) + b2i(by2) = s2i(i2s(b2i(by1) + b2i(by2))) | A User Theorem |
| fits-law-band | ⊦ band(b2i(by1), b2i(by2)) = b2i(i2b(band(b2i(by1), b2i(by2)))) | A User Theorem |
| fits-law-band-01 | ⊦ band(s2i(sho1), b2i(by2)) = s2i(i2s(band(s2i(sho1), b2i(by2)))) | A User Theorem |
| fits-law-band-02 | ⊦ band(s2i(sho1), s2i(sho2)) = s2i(i2s(band(s2i(sho1), s2i(sho2)))) | A User Theorem |
| fits-law-bor | ⊦ bor(b2i(by1), b2i(by2)) = b2i(i2b(bor(b2i(by1), b2i(by2)))) | A User Theorem |
| fits-law-bor-01 | ⊦ bor(s2i(sho1), b2i(by2)) = s2i(i2s(bor(s2i(sho1), b2i(by2)))) | A User Theorem |
| fits-law-bor-02 | ⊦ bor(s2i(sho1), s2i(sho2)) = s2i(i2s(bor(s2i(sho1), s2i(sho2)))) | A User Theorem |
| fits-law-bxor | ⊦ bxor(b2i(by1), b2i(by2)) = b2i(i2b(bxor(b2i(by1), b2i(by2)))) | A User Theorem |
| fits-law-bxor-01 | ⊦ bxor(s2i(sho1), b2i(by2)) = s2i(i2s(bxor(s2i(sho1), b2i(by2)))) | A User Theorem |
| fits-law-bxor-02 | ⊦ bxor(s2i(sho1), s2i(sho2)) = s2i(i2s(bxor(s2i(sho1), s2i(sho2)))) | A User Theorem |
| fits-law-compl | ⊦ bcompl(b2i(by)) = b2i(i2b(bcompl(b2i(by)))) | A User Theorem |
| fits-law-compl-01 | ⊦ bcompl(s2i(sho)) = s2i(i2s(bcompl(s2i(sho)))) | A User Theorem |
| fits-law-div | ⊦ i ≠ 0 → b2i(by1) / i = s2i(i2s(b2i(by1) / i)) | A User Theorem |
| fits-law-div-stronger | ⊦ i ≠ ~1 ∧ i ≠ 0 → b2i(by1) / i = b2i(i2b(b2i(by1) / i)) | A User Theorem |
| fits-law-mod | b2i(by1) ≠ 0 ⊦ i % b2i(by1) = b2i(i2b(i % b2i(by1))) | A User Theorem |
| fits-law-mod-01 | s2i(sho) ≠ 0 ⊦ i % s2i(sho) = s2i(i2s(i % s2i(sho))) | A User Theorem |
| fits-law-mul | ⊦ b2i(by1) * b2i(by2) = s2i(i2s(b2i(by1) * b2i(by2))) | A User Theorem |
| fits-law-neg | ⊦ ~ b2i(by) = s2i(i2s(~ b2i(by))) | A User Theorem |
| fits-law-shr | ⊦ b2i(by) i>> i = b2i(i2b(b2i(by) i>> i)) | A User Theorem |
| fits-law-shr-01 | ⊦ s2i(sho) i>> i = s2i(i2s(s2i(sho) i>> i)) | A User Theorem |
| fits-law-sub | ⊦ b2i(by1) - b2i(by2) = s2i(i2s(b2i(by1) - b2i(by2))) | A User Theorem |
| getShort-isi | ⊦ s2i(i2s(bor(b2i(byi) i<< 8, band(b2i(byj), 255)))) = bor(b2i(byi) i<< 8, band(b2i(byj), 255)) | A User Theorem |
| getsetShort-theorem | ⊦ j ∈short → bor(b2i(i2b(j i>> 8)) i<< 8, band(255, b2i(i2b(j)))) = j | A User Theorem |
| i2b-equal | ⊦ i2b(i) = i2b(j) ↔ b2i(i2b(i)) = b2i(i2b(j)) | A User Theorem |
| i2b-noteq | ⊦ i2b(i) ≠ i2b(j) → i ≠ j | A User Theorem |
| inbyte-bib | ⊦ i ∈byte ↔ b2i(i2b(i)) = i | A User Theorem |
| inshort-01 | ⊦ 0 ≤ s2i(sho) ∧ s2i(sho) < s2i(shoi) → (s2i(sho) + 1)∈short | A User Theorem |
| inshort-byte | ⊦ b2i(by) ∈short | A User Theorem |
| inshort-le-num | 32768 ≤ i ⊦ s2i(sho0) ≤ (* i) | A User Theorem |
| inshort-mult | ⊦ s2i(sho) ≠ 0 ∧ s2i(sho) ≠ 1 → ¬ (s2i(sho) * ~32768)∈short | A User Theorem |
| inshort-neg | ⊦ s2i(sho) ≠ ~32768 → (~ s2i(sho))∈short | A User Theorem |
| inshort-num | ⊦ (* i) ∈short ↔ ¬ ¬(~32768 ≤ i ∧ i < 32768) | A User Theorem |
| inshort-sis | ⊦ i ∈short ↔ s2i(i2s(i)) = i | A User Theorem |
| issi-ubyte | ⊦ s2i(i2s(ub2i(by))) = ub2i(by) | A User Theorem |
| l2i-bint | ⊦ i ∈bint → l2i(i2l(i)) = i | A User Theorem |
| lil-carry | ⊦ 0 ≤ i ∧ i ≤ 1 → l2i(i2l(i + band(4294967295, j) + band(4294967295, j0))) = i + band(4294967295, j) + band(4294967295, j0) | A User Theorem |
| lil-num | ~9223372036854775808 ≤ i, i < 9223372036854775808 ⊦ l2i(i2l((* i))) = i | A User Theorem |
| long-automatic | ⊦ i2l((* i)) = i2l((* j)) ↔ (0 ≤ i ∧ i % 18446744073709551616 ≤ 9223372036854775807 ⊃ i % 18446744073709551616 ;(0 ≤ i ∧ 9223372036854775807 < i % 18446744073709551616 ⊃ i % 18446744073709551616 - 18446744073709551616 ;(i < 0 ∧ i % 18446744073709551616 < ~9223372036854775808 ⊃ i % 18446744073709551616 + 18446744073709551616 ;(i < 0 ∧ ~9223372036854775808 ≤ i % 18446744073709551616 ⊃ i % 18446744073709551616;i) ) ) ) = (0 ≤ j ∧ j % 18446744073709551616 ≤ 9223372036854775807 ⊃ j % 18446744073709551616 ;(0 ≤ j ∧ 9223372036854775807 < j % 18446744073709551616 ⊃ j % 18446744073709551616 - 18446744073709551616 ;(j < 0 ∧ j % 18446744073709551616 < ~9223372036854775808 ⊃ j % 18446744073709551616 + 18446744073709551616 ;(j < 0 ∧ ~9223372036854775808 ≤ j % 18446744073709551616 ⊃ j % 18446744073709551616;j) ) ) ) | A User Theorem |
| long-automatic-01 | ⊦ i2l(~9223372036854775809) = i2l(9223372036854775807) | A User Theorem |
| long-automatic-02 | ⊦ i2l(18446744073709551614) = i2l(~2) | A User Theorem |
| long-automatic-03 | ⊦ i2l(85070591730234615847396907784232501249) = i2l(1) | A User Theorem |
| long-band-11x | ⊦ l2i(i2l(band(4294967295, i))) = band(4294967295, i) | A User Theorem |
| long-band-add | ⊦ l2i(i2l(band(4294967295, i) + band(4294967295, j))) = band(4294967295, i) + band(4294967295, j) | A User Theorem |
| long-eq | ⊦ i2l(i) = i2l(j) ↔ cast(64, i) = cast(64, j) | A User Theorem |
| long-eq-01 | ⊦ l2i(i2l(i)) ≠ l2i(i2l(j)) → i2l(i) ≠ i2l(j) | A User Theorem |
| long-is-cast | ⊦ l2i(i2l(i)) = cast(64, i) | A User Theorem |
| long-is-cast-01 | ⊦ i2l(i) = i2l(cast(64, i)) | A User Theorem |
| long-min | ⊦ ¬ l2i(lo) < ~9223372036854775808 | A User Theorem |
| long-min-01 | ⊦ i ≤ ~9223372036854775808 → ¬ l2i(lo) < i | A User Theorem |
| long-mod-neg-high | j < 0, ~(2 ^ (64 - 1)) ≤ j % 2 ^ 64 ⊦ l2i(i2l((* j))) = j % 2 ^ 64 | A User Theorem |
| long-mod-neg-low | j < 0, j % 2 ^ 64 < ~(2 ^ (64 - 1)) ⊦ l2i(i2l((* j))) = j % 2 ^ 64 + 2 ^ 64 | A User Theorem |
| long-mod-pos-high | 0 ≤ j, 2 ^ (64 - 1) - 1 < j % 2 ^ 64 ⊦ l2i(i2l((* j))) = j % 2 ^ 64 - 2 ^ 64 | A User Theorem |
| long-mod-pos-low | 0 ≤ j, j % 2 ^ 64 ≤ 2 ^ (64 - 1) - 1 ⊦ l2i(i2l((* j))) = j % 2 ^ 64 | A User Theorem |
| long-on-bits | ⊦ l2i(i2l(i)) = bits2int(lastn(64, fillsgn(64, int2bits(i)))) | A User Theorem |
| long-shiftzero-in | ⊦ (l2i(lo) l>>> j)∈long | A User Theorem |
| long-shzr | ⊦ l2i(i2l(l2i(lo) l>>> j)) = l2i(lo) l>>> j | A User Theorem |
| longin-mod | ⊦ i ∈long ∧ j ≠ 0 → (i % j)∈long | A User Theorem |
| longin-mult | ⊦ i ∈bint → (i * i)∈long | A User Theorem |
| longin-mult-01 | ⊦ i ∈bint ∧ j ∈bint → (i * j)∈long | A User Theorem |
| longin-mult-mod | ⊦ i ∈bint ∧ j ∈bint ∧ j0 ≠ 0 → ((i * j) % j0)∈long | A User Theorem |
| longin-mult-mod-01 | ⊦ i ∈bint ∧ j ≠ 0 → ((i * i) % j)∈long | A User Theorem |
| mfive | ⊦ i + 1 + 1 + 1 + 1 + 1 = 0 → s2i(i2s(i + 1 + 1)) = i + 1 + 1 | A User Theorem |
| minus-five | ⊦ i + 1 + 1 + 1 + 1 + 1 = 0 → b2i(i2b(i)) = i | A User Theorem |
| minus-five-01 | ⊦ i + 1 + 1 + 1 + 1 + 1 = 0 → b2i(i2b(i + 1)) = i + 1 | A User Theorem |
| minus-four | ⊦ i + 1 + 1 + 1 + 1 = 0 → s2i(i2s(i + 1)) = i + 1 | A User Theorem |
| minus-four-01 | ⊦ i + 1 + 1 + 1 + 1 = 0 → b2i(i2b(i + 1)) = i + 1 | A User Theorem |
| minus-four-02 | ⊦ i + 1 + 1 + 1 + 1 = 0 → b2i(i2b(i)) = i | A User Theorem |
| minus-three | ⊦ i + 1 + 1 + 1 = 0 → s2i(i2s(i)) = ~(1 + 1 + 1) | A User Theorem |
| minus-three-01 | ⊦ i + 1 + 1 + 1 = 0 → s2i(i2s(i + 1)) = ~(1 + 1) | A User Theorem |
| minus-two | ⊦ i + 1 + 1 = 0 → s2i(i2s(i)) = ~(1 + 1) | A User Theorem |
| mod-inshort | ⊦ s2i(sho1) ≠ 0 → (s2i(sho0) % s2i(sho1))∈short | A User Theorem |
| mthree | ⊦ i + 1 + 1 + 1 = 0 → b2i(i2b(i)) = ~(1 + 1 + 1) | A User Theorem |
| mthree-01 | ⊦ i + 1 + 1 + 1 = 0 → b2i(i2b(~ i)) = 1 + 1 + 1 | A User Theorem |
| mtwo | ⊦ i + 1 + 1 = 0 → b2i(i2b(i)) = ~(1 + 1) | A User Theorem |
| notequal | ~128 ≤ i, i ≤ 127, ~128 ≤ j, j ≤ 127, i ≠ j ⊦ i2b((* i)) ≠ i2b((* j)) | A User Theorem |
| notequal-01 | ~32768 ≤ i, i ≤ 32767, ~32768 ≤ j, j ≤ 32767, i ≠ j ⊦ i2s((* i)) ≠ i2s((* j)) | A User Theorem |
| num-i2b-equal | ~128 ≤ i, i ≤ 127, ~128 ≤ j, j ≤ 127 ⊦ i2b((* i)) = i2b((* j)) ↔ i = j | A User Theorem |
| num-i2b-neg | i < ~128 ⊦ i2b((* i)) = i2b(bits2int(lastn(8, int2bits(i)))) | A User Theorem |
| num-i2b-pos | 127 < i ⊦ i2b((* i)) = i2b(bits2int(lastn(8, int2bits(i)))) | A User Theorem |
| num-i2bi-neg | i < ~2147483648 ⊦ i2bi((* i)) = i2bi(bits2int(lastn(32, int2bits(i)))) | A User Theorem |
| num-i2bi-pos | 2147483647 < i ⊦ i2bi((* i)) = i2bi(bits2int(lastn(32, int2bits(i)))) | A User Theorem |
| num-i2l-neg | i < ~9223372036854775808 ⊦ i2l((* i)) = i2l(bits2int(lastn(64, int2bits(i)))) | A User Theorem |
| num-i2l-pos | 9223372036854775807 < i ⊦ i2l((* i)) = i2l(bits2int(lastn(64, int2bits(i)))) | A User Theorem |
| num-i2s-neg | i < ~32768 ⊦ i2s((* i)) = i2s(bits2int(lastn(16, int2bits(i)))) | A User Theorem |
| num-i2s-pos | 32767 < i ⊦ i2s((* i)) = i2s(bits2int(lastn(16, int2bits(i)))) | A User Theorem |
| num-ibbi | ~128 ≤ i, i ≤ 127 ⊦ b2i(i2b((* i))) = i | A User Theorem |
| num-illi | ~9223372036854775808 ≤ i, i ≤ 9223372036854775807 ⊦ l2i(i2l((* i))) = i | A User Theorem |
| num-issi | ~32768 ≤ i, i ≤ 32767 ⊦ s2i(i2s((* i))) = i | A User Theorem |
| out-test-01 | ⊦ b2i(i2b(128)) = ~128 | A User Theorem |
| out-test-02 | ⊦ b2i(i2b(~129)) = 127 | A User Theorem |
| out-test-03 | ⊦ b2i(i2b(123)) = 123 | A User Theorem |
| out-test-04 | ⊦ b2i(i2b(~126)) = ~126 | A User Theorem |
| out-test-05 | ⊦ b2i(i2b(~511)) = 1 | A User Theorem |
| out-test-06 | ⊦ b2i(i2b(~512)) = 0 | A User Theorem |
| out-test-07 | ⊦ b2i(i2b(511)) = ~1 | A User Theorem |
| out-test-08 | ⊦ b2i(i2b(512)) = 0 | A User Theorem |
| s144 | ⊦ s2i(i2s(144)) = 144 | A User Theorem |
| s2i-switch | ⊦ ~32768 ≤ i ∧ i < 32768 → (s2i(sho) = i ↔ sho = i2s(i)) | A User Theorem |
| shiftright-byte-8-neg | ⊦ b2i(by) < 0 → b2i(by) >> 8 = ~1 | A User Theorem |
| shiftright-byte-8-neg-01 | ⊦ b2i(by) < 0 ∧ 8 ≤ j → b2i(by) >> j = ~1 | A User Theorem |
| shiftright-byte-8-pos | ⊦ 0 ≤ b2i(by) → b2i(by) >> 8 = 0 | A User Theorem |
| shiftright-byte-8-pos-01 | ⊦ 0 ≤ b2i(by) ∧ 8 ≤ j → b2i(by) >> j = 0 | A User Theorem |
| short-011x-neg | ⊦ s2i(sho) < 0 → band(s2i(sho), 65535) = s2i(sho) + 65536 | A User Theorem |
| short-011x-pos | ⊦ 0 ≤ s2i(sho) → band(s2i(sho), 65535) = s2i(sho) | A User Theorem |
| short-32767 | ⊦ 32766 < s2i(sho) ↔ s2i(sho) = 32767 | A User Theorem |
| short-add-max | ⊦ ¬ 65536 ≤ s2i(sho) + s2i(sho0) | A User Theorem |
| short-add-max-01 | ⊦ s2i(sho1) < 0 → ¬ 32767 < s2i(sho0) + s2i(sho1) | A User Theorem |
| short-add-min | ⊦ s2i(sho0) + s2i(sho1) ≤ ~65536 ↔ s2i(sho0) = ~32768 ∧ s2i(sho1) = ~32768 | A User Theorem |
| short-add-min-01 | ⊦ s2i(sho0) + s2i(sho1) = ~65536 ↔ s2i(sho0) = ~32768 ∧ s2i(sho1) = ~32768 | A User Theorem |
| short-add-min-02 | ⊦ 0 ≤ s2i(sho0) → ¬ s2i(sho0) + s2i(sho1) < ~32768 | A User Theorem |
| short-add-min-03 | ⊦ ¬ s2i(sho) + s2i(sho0) < ~65536 | A User Theorem |
| short-add-pos | ⊦ s2i(sho) + s2i(sho0) ≤ 32767 ∧ 0 ≤ s2i(sho) ∧ 0 ≤ s2i(sho0) → s2i(i2s(s2i(sho) + s2i(sho0))) = s2i(sho) + s2i(sho0) | A User Theorem |
| short-add-pos-01 | ⊦ s2i(sho) + s2i(sho0) ≤ 32767 ∧ 0 < s2i(sho) ∧ 0 ≤ s2i(sho0) → s2i(i2s(s2i(sho) + s2i(sho0))) = s2i(sho) + s2i(sho0) | A User Theorem |
| short-add-pos-02 | ⊦ s2i(sho) + s2i(sho0) ≤ 32767 ∧ 0 < s2i(sho) ∧ 0 < s2i(sho0) → s2i(i2s(s2i(sho) + s2i(sho0))) = s2i(sho) + s2i(sho0) | A User Theorem |
| short-add2 | ⊦ i ≤ 32767 → ¬ 65536 ≤ i + s2i(sho0) | A User Theorem |
| short-byte | ⊦ s2i(i2s(b2i(by))) = b2i(by) | A User Theorem |
| short-div-max | ⊦ ¬ 32767 < s2i(sho) / 256 | A User Theorem |
| short-div-max-01 | ⊦ 0 < j → ¬ 65536 ≤ s2i(sho) / j | A User Theorem |
| short-div-ngr | ⊦ j ≠ 0 → ¬ 65536 ≤ s2i(sho) / j | A User Theorem |
| short-div256 | ⊦ ¬ 256 < s2i(sho) / 256 | A User Theorem |
| short-equal | ⊦ s2i(shoi) = s2i(shoj) ↔ shoi = shoj | A User Theorem |
| short-ge | ⊦ 32767 ≤ s2i(sho) ↔ s2i(sho) = 32767 | A User Theorem |
| short-in | ⊦ 0 ≤ i ∧ i ≤ 32767 → s2i(i2s(i)) = i | A User Theorem |
| short-inj | ⊦ i2s(i) = i2s(j) ↔ s2i(i2s(i)) = s2i(i2s(j)) | A User Theorem |
| short-inrange | ⊦ ~32768 ≤ i ∧ i < 32768 → s2i(i2s(i)) = i | A User Theorem |
| short-is-cast | ⊦ s2i(i2s(i)) = cast(16, i) | A User Theorem |
| short-is-cast-01 | ⊦ i2s(i) = i2s(cast(16, i)) | A User Theorem |
| short-larger | ⊦ 32768 ≤ i → i2s(i) = i2s(i - 2 ^ 16) | A User Theorem |
| short-law-add | ⊦ s2i(i2s(j + j0)) = s2i(i2s(s2i(i2s(j)) + s2i(i2s(j0)))) | A User Theorem |
| short-law-add-one | ⊦ s2i(i2s(j + j0)) = s2i(i2s(s2i(i2s(j)) + j0)) | A User Theorem |
| short-law-and-one | ⊦ s2i(i2s(band(j, j0))) = s2i(i2s(band(s2i(i2s(j)), j0))) | A User Theorem |
| short-law-compl | ⊦ i2s(bcompl(i)) = i2s(bcompl(s2i(i2s(i)))) | A User Theorem |
| short-law-div-not | ⊦ (i = 2 ^ 16 ∧ j = 2 ^ 14 → i2s(i / j) ≠ i2s(s2i(i2s(i)) / j)) ∧ (i = ~(2 ^ 15) ∧ j = 2 ^ 15 → i2s(i / j) ≠ i2s(i / s2i(i2s(j)))) ∧ (i = 2 ^ 16 ∧ j = 2 ^ 15 → i2s(i / j) ≠ i2s(s2i(i2s(i)) / s2i(i2s(j)))) ∧ (i = 2 ^ 16 + 2 ∧ j = 331 → i2s(i % j) ≠ i2s(s2i(i2s(i)) % j)) ∧ (i = 1 ∧ j = 2 ^ 16 - 1 → i2s(i % j) ≠ i2s(i % s2i(i2s(j)))) ∧ (i = 2 * 2 ^ 16 - 1 ∧ j = 2 ^ 16 - 1 → i2s(i % j) ≠ i2s(s2i(i2s(i)) % s2i(i2s(j)))) | A User Theorem |
| short-law-leftshift | ⊦ i2s(i i<< j) = i2s(s2i(i2s(i)) i<< j) | A User Theorem |
| short-law-ls-not | ⊦ (i = 32767 ∧ j = 32768 → ¬(i < j → s2i(i2s(i)) < s2i(i2s(j)))) ∧ (i = 32768 ∧ j = 1 → ¬(s2i(i2s(i)) < s2i(i2s(j)) → i < j)) ∧ (i = 65535 ∧ j = ~1 → ¬(s2i(i2s(i)) = s2i(i2s(j)) → i = j)) | A User Theorem |
| short-law-mult | ⊦ s2i(i2s(j * j0)) = s2i(i2s(s2i(i2s(j)) * s2i(i2s(j0)))) | A User Theorem |
| short-law-mult-one | ⊦ s2i(i2s(j * j0)) = s2i(i2s(s2i(i2s(j)) * j0)) | A User Theorem |
| short-law-neg | ⊦ i2s(~ i) = i2s(~ s2i(i2s(i))) | A User Theorem |
| short-law-or-one | ⊦ s2i(i2s(bor(j, j0))) = s2i(i2s(bor(s2i(i2s(j)), j0))) | A User Theorem |
| short-law-righthift-not | ⊦ (i = 32768 ∧ j = 1 → i2s(i i>> j) ≠ i2s(s2i(i2s(i)) i>> j)) ∧ (i = 32768 ∧ j = 1 → i2s(i i>>> j) ≠ i2s(s2i(i2s(i)) i>>> j)) | A User Theorem |
| short-law-shift-snd-l | ⊦ i i<< j = i i<< s2i(i2s(j)) | A User Theorem |
| short-law-shift-snd-r | ⊦ i i>> j = i i>> s2i(i2s(j)) | A User Theorem |
| short-law-shift-snd-rz | ⊦ i i>>> j = i i>>> s2i(i2s(j)) | A User Theorem |
| short-law-sub | ⊦ s2i(i2s(j - j0)) = s2i(i2s(s2i(i2s(j)) - s2i(i2s(j0)))) | A User Theorem |
| short-law-sub-one | ⊦ s2i(i2s(j - j0)) = s2i(i2s(s2i(i2s(j)) - j0)) | A User Theorem |
| short-law-sub-one-01 | ⊦ s2i(i2s(j - j0)) = s2i(i2s(j - s2i(i2s(j0)))) | A User Theorem |
| short-law-xor-one | ⊦ s2i(i2s(bxor(j, j0))) = s2i(i2s(bxor(s2i(i2s(j)), j0))) | A User Theorem |
| short-ls | ⊦ s2i(sho) < ~32767 ↔ s2i(sho) = ~32768 | A User Theorem |
| short-mask | ⊦ ¬ band(65535, s2i(sho)) < 0 | A User Theorem |
| short-max | ⊦ ¬ 65536 ≤ s2i(sho) | A User Theorem |
| short-max-01 | ⊦ ¬ 32768 ≤ s2i(sho) | A User Theorem |
| short-max-02 | ⊦ 0 < i → ¬ i + 32767 < s2i(sho) | A User Theorem |
| short-max-03 | ⊦ 0 ≤ i → ¬ i + 32767 < s2i(sho) | A User Theorem |
| short-max-04 | ⊦ 0 ≤ i → ¬ 32768 + i < s2i(sho) | A User Theorem |
| short-max-05 | ⊦ 0 < i → ¬ 32768 + i < s2i(sho) | A User Theorem |
| short-max-06 | ⊦ 32767 ≤ i → ¬ i < s2i(sho) | A User Theorem |
| short-max-07 | ⊦ 32768 ≤ i → ¬ i ≤ s2i(sho) | A User Theorem |
| short-max-08 | ⊦ s2i(sho) ≠ 65535 | A User Theorem |
| short-max-09 | ⊦ s2i(sho) ≠ 65536 | A User Theorem |
| short-max-10 | ⊦ 32767 < i → s2i(sho) ≠ i | A User Theorem |
| short-max-11 | ⊦ 65536 * i + s2i(sho) < 32768 ↔ i ≤ 0 | A User Theorem |
| short-min | ⊦ ~32768 ≤ s2i(sho) | A User Theorem |
| short-min-01 | ⊦ ¬ s2i(sho) < ~32768 | A User Theorem |
| short-min-02 | ⊦ i ≤ ~32768 → ¬ s2i(sho) < i | A User Theorem |
| short-min-03 | ⊦ s2i(sho) ≤ ~32768 ↔ s2i(sho) = ~32768 | A User Theorem |
| short-mod | ⊦ s2i(sho) % 65536 = s2i(sho) | A User Theorem |
| short-mod-01 | i ≠ 0 ⊦ s2i(i2s(s2i(sho) % i)) = s2i(sho) % i | A User Theorem |
| short-mod-add | ⊦ 0 ≤ s2i(sho) → (s2i(sho) + s2i(sho0)) % 65536 = s2i(sho) + s2i(sho0) | A User Theorem |
| short-mod-add-01 | ⊦ 0 ≤ s2i(sho) + s2i(sho0) → (s2i(sho) + s2i(sho0)) % 65536 = s2i(sho) + s2i(sho0) | A User Theorem |
| short-mod-add-02 | ⊦ 0 < s2i(sho) + s2i(sho0) → (s2i(sho) + s2i(sho0)) % 65536 = s2i(sho) + s2i(sho0) | A User Theorem |
| short-mod-max | ⊦ s2i(sho0) + s2i(sho1) ≠ ~65536 → (s2i(sho0) + s2i(sho1)) % 65536 = s2i(sho0) + s2i(sho1) | A User Theorem |
| short-mod-ngr | ⊦ s2i(sho0) ≠ 0 → ¬ 65536 ≤ s2i(sho) % s2i(sho0) | A User Theorem |
| short-mult-65536 | ⊦ i2s(i * 65536 + j) = i2s(j) | A User Theorem |
| short-mult-65536-01 | ⊦ i2s(j) = i2s(i * 65536 + j) | A User Theorem |
| short-neq | ⊦ s2i(sho) ≠ ~65536 | A User Theorem |
| short-neq-01 | ⊦ s2i(sho) + 65536 * i = 0 ↔ i = 0 ∧ s2i(sho) = 0 | A User Theorem |
| short-neq-02 | ⊦ us2i(sho) + 65536 * i = 0 ↔ i = 0 ∧ s2i(sho) = 0 | A User Theorem |
| short-ngr | ⊦ ¬ 32767 < s2i(sho) | A User Theorem |
| short-nle | ⊦ ¬ s2i(sho) ≤ ~32769 | A User Theorem |
| short-nle-01 | ⊦ ¬ s2i(sho) ≤ ~65536 | A User Theorem |
| short-nle-02 | ⊦ j < ~32768 → ¬ s2i(sho) ≤ j | A User Theorem |
| short-nle-03 | ⊦ ¬ s2i(sho) + 65536 ≤ s2i(sho0) | A User Theorem |
| short-nls | ⊦ 0 < i → ¬ 65536 * i < s2i(sho) | A User Theorem |
| short-nls-01 | ⊦ ¬ s2i(sho) + 65536 < s2i(sho0) | A User Theorem |
| short-not-max | ⊦ 32766 < s2i(sho) ∧ 0 < i → ¬ s2i(sho) + i < 32768 | A User Theorem |
| short-overflow | ⊦ 32767 < s2i(sho) + s2i(sho0) → ¬ 0 ≤ s2i(i2s(s2i(sho) + s2i(sho0))) | A User Theorem |
| short-range | ⊦ ~32768 ≤ s2i(sho) ∧ s2i(sho) ≤ 32767 | A User Theorem |
| short-shift-pos | ⊦ 0 < s2i(sho) → s2i(i2s(s2i(sho) i>> 8)) = s2i(sho) i>> 8 | A User Theorem |
| short-size | ⊦ ¬ 32768 < 2 ^ n→i(# int2bits(s2i(sho)) - 1) | A User Theorem |
| short-size-01 | ⊦ ¬ 32768 < 2 ^ (n→i(# int2bits(s2i(sho))) - 1) | A User Theorem |
| short-size-02 | ⊦ ¬ 16 < # int2bits(s2i(sho)) | A User Theorem |
| short-sub-pos | ⊦ s2i(sho) ≤ s2i(sho0) ∧ 0 ≤ s2i(sho) → s2i(i2s(s2i(sho0) - s2i(sho))) = s2i(sho0) - s2i(sho) | A User Theorem |
| short-succ | ⊦ s2i(sho) < 32767 → s2i(i2s(s2i(sho) + 1)) = s2i(sho) + 1 | A User Theorem |
| short-succ-01 | ⊦ s2i(sho) < 0 → s2i(i2s(s2i(sho) + 1)) = s2i(sho) + 1 | A User Theorem |
| short-succ-pos | ⊦ 0 ≤ s2i(sho) ∧ s2i(sho) < s2i(shoi) → s2i(i2s(s2i(sho) + 1)) = s2i(sho) + 1 | A User Theorem |
| short-zero | ⊦ sho = i2s(0) ↔ s2i(sho) = 0 | A User Theorem |
| sis-01 | ⊦ s2i(i2s(1)) = 1 | A User Theorem |
| sis-03 | ⊦ i + j ≤ 32767 ∧ 0 ≤ i ∧ 0 ≤ j → s2i(i2s(i)) = i | A User Theorem |
| sis-05 | ⊦ 0 ≤ i ∧ i ≤ 10 → s2i(i2s(i * 141)) = i * 141 | A User Theorem |
| sis-06 | ⊦ s2i(i2s(0)) = 0 | A User Theorem |
| sis-bitlength | ⊦ # int2bits(i) ≤ 16 → s2i(i2s(i)) = i | A User Theorem |
| sis-ls-same | ⊦ i < s2i(i2s(i)) ↔ i < ~32768 | A User Theorem |
| sis-ls-same-01 | ⊦ s2i(i2s(i)) < i ↔ 32768 ≤ i | A User Theorem |
| sis-neg-high | ⊦ i < 0 ∧ ~32768 ≤ i % 65536 → s2i(i2s(i)) = i % 65536 | A User Theorem |
| sis-neg-low | ⊦ i < 0 ∧ i % 65536 < ~32768 → s2i(i2s(i)) = i % 65536 + 65536 | A User Theorem |
| sis-neg-lower | ⊦ i < ~32768 ∧ ~65536 < i → s2i(i2s(i)) = i + 65536 | A User Theorem |
| sis-on-bits | ⊦ s2i(i2s(i)) = bits2int(lastn(16, fillsgn(16, int2bits(i)))) | A User Theorem |
| sis-pos-high | ⊦ 0 ≤ i ∧ 32767 < i % 65536 → s2i(i2s(i)) = i % 65536 - 65536 | A User Theorem |
| sis-pos-low | ⊦ 0 ≤ i ∧ i % 65536 ≤ 32767 → s2i(i2s(i)) = i % 65536 | A User Theorem |
| sis-pos-upper | ⊦ 32768 ≤ i ∧ i < 65536 → s2i(i2s(i)) = i - 65536 | A User Theorem |
| sis-sub-2pot | ⊦ 0 ≤ i ∧ i < 65536 → s2i(i2s(i - 65536)) = s2i(i2s(i)) | A User Theorem |
| ubyte-abs | ⊦ abs(ub2i(by)) = ub2i(by) | A User Theorem |
| ubyte-band | ⊦ ub2i(i2b(band(i, 255))) = band(i, 255) | A User Theorem |
| ubyte-div-lsz | ⊦ ub2i(by) ≠ 0 → (i / ub2i(by) < 0 ↔ i + ub2i(by) ≤ 0) | A User Theorem |
| ubyte-inj | ⊦ ub2i(by) = ub2i(by0) ↔ by = by0 | A User Theorem |
| ubyte-max | ⊦ ¬ 255 < ub2i(by) | A User Theorem |
| ubyte-max-01 | ⊦ ¬ 256 ≤ ub2i(by) | A User Theorem |
| ubyte-max-02 | ⊦ ¬ 256 < ub2i(by) | A User Theorem |
| ubyte-mod | ⊦ ub2i(by) ≠ 0 → ¬ 256 ≤ i % ub2i(by) | A User Theorem |
| ubyte-mult | ⊦ ¬ 65536 ≤ ub2i(by) * ub2i(by0) | A User Theorem |
| ubyte-neg | ⊦ b2i(by) < 0 → ub2i(by) = 256 + b2i(by) | A User Theorem |
| ubyte-pos | ⊦ 0 ≤ b2i(by) → ub2i(by) = b2i(by) | A User Theorem |
| ubyte-pos-01 | ⊦ ¬ ub2i(by) < 0 | A User Theorem |
| ubyte-pos-02 | ⊦ ¬ ub2i(by) * ub2i(by0) < 0 | A User Theorem |
| ubyte-pos-03 | ⊦ 0 ≤ i ∧ i < 256 → ub2i(i2b(i)) = i | A User Theorem |
| ubyte-zero | ⊦ ub2i(by) ≤ 0 ↔ ub2i(by) = 0 | A User Theorem |
| ubyte-zero-01 | ⊦ ub2i(by) = 0 → b2i(by) = 0 | A User Theorem |
| ushort-abs | ⊦ abs(us2i(sho)) = us2i(sho) | A User Theorem |
| ushort-band | ⊦ us2i(i2s(band(i, 255))) = band(i, 255) | A User Theorem |
| ushort-band-01 | ⊦ band(s2i(sho), 255) = band(us2i(sho), 255) | A User Theorem |
| ushort-band-02 | ⊦ band(s2i(sho), 255) = us2i(sho) % 256 | A User Theorem |
| ushort-band-03 | ⊦ band(s2i(sho), 65535) = us2i(sho) | A User Theorem |
| ushort-band-shift | ⊦ band(s2i(sho) i>> 8, 255) = band(us2i(sho) i>> 8, 255) | A User Theorem |
| ushort-band-shift-01 | ⊦ band(s2i(sho) i>> 8, 255) = us2i(sho) / 256 | A User Theorem |
| ushort-inj | ⊦ us2i(sho) = us2i(sho0) ↔ sho = sho0 | A User Theorem |
| ushort-max | ⊦ ¬ 65536 ≤ us2i(sho) | A User Theorem |
| ushort-max-01 | ⊦ 65535 ≤ us2i(sho) ↔ us2i(sho) = 65535 | A User Theorem |
| ushort-max-02 | ⊦ 256 ≤ i ∧ 0 ≤ j → us2i(sho) ≠ i * 256 + j | A User Theorem |
| ushort-max-03 | ⊦ ¬ 255 < us2i(sho) / 256 | A User Theorem |
| ushort-max-04 | ⊦ ¬ 65535 < us2i(sho) | A User Theorem |
| ushort-max-05 | ⊦ ¬ 256 ≤ us2i(sho) / 256 | A User Theorem |
| ushort-max-06 | ⊦ 65535 ≤ i → ¬ i < us2i(sho) | A User Theorem |
| ushort-max-07 | ⊦ ¬ 65536 < us2i(sho) | A User Theorem |
| ushort-neg | ⊦ s2i(sho) < 0 → us2i(sho) = 2 ^ 16 + s2i(sho) | A User Theorem |
| ushort-nlsz | ⊦ ¬ us2i(sho) < 0 | A User Theorem |
| ushort-plus | ⊦ us2i(sho) + us2i(sho0) < 2 ^ 16 → us2i(i2s(s2i(sho) + s2i(sho0))) = us2i(sho) + us2i(sho0) | A User Theorem |
| ushort-plus-01 | ⊦ 0 ≤ i ∧ i < 32767 ∧ us2i(sho) + i < 2 ^ 16 → us2i(i2s(s2i(sho) + i)) = us2i(sho) + i | A User Theorem |
| ushort-pos | ⊦ 0 ≤ s2i(sho) → us2i(sho) = s2i(sho) | A User Theorem |
| ushort-pos-01 | ⊦ 0 ≤ i ∧ i < 65536 → us2i(i2s(i)) = i | A User Theorem |
| ushort-pos-02 | ⊦ ~65536 ≤ i ∧ i < 0 → us2i(i2s(i)) = i + 65536 | A User Theorem |
| ushort-short | ⊦ i2s(us2i(sho)) = sho | A User Theorem |
| ushort-zero | ⊦ ¬ us2i(sho0) * us2i(sho1) < 0 | A User Theorem |
| ushort-zero-01 | ⊦ us2i(sho) = 0 ↔ s2i(sho) = 0 | A User Theorem |
| ushort-zero-02 | ⊦ us2i(sho) ≤ 0 ↔ us2i(sho) = 0 | A User Theorem |