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: |
|---|---|---|
| band-def | ⊦ band(i, j) = bits2int(bitsand(int2bits(i), int2bits(j))) | An Axiom |
| bxor-def | ⊦ bxor(i, j) = bits2int(bitsxor(int2bits(i), int2bits(j))) | An Axiom |
| bor-def | ⊦ bor(i, j) = bits2int(bitsor(int2bits(i), int2bits(j))) | An Axiom |
| bcompl-def | ⊦ bcompl(i) = bits2int(bitsinvert(int2bits(i))) | An Axiom |
| bitsand-onel | ⊦ bitsand(true ', bits + boolvar ') = bits + boolvar | An Axiom |
| bitsand-oner | ⊦ bitsand(bits + boolvar ', true ') = bits + boolvar | An Axiom |
| bitsand-zerol | ⊦ bitsand(false ', bits + boolvar ') = false ' | An Axiom |
| bitsand-zeror | ⊦ bitsand(bits + boolvar ', false ') = false ' | An Axiom |
| bitsand-rec | ⊦ bitsand(bits + boolvar ' + boolvar0 ', bits0 + boolvar1 ' + boolvar2 ') = bitsand(bits + boolvar, bits0 + boolvar1) + (boolvar0 ∧ boolvar2) | An Axiom |
| bitsxor-onel | ⊦ bitsxor(true ', bits + boolvar ') = bitsinvert(bits + boolvar) | An Axiom |
| bitsxor-oner | ⊦ bitsxor(bits + boolvar ', true ') = bitsinvert(bits + boolvar) | An Axiom |
| bitsxor-zerol | ⊦ bitsxor(false ', bits + boolvar ') = bits + boolvar | An Axiom |
| bitsxor-zeror | ⊦ bitsxor(bits + boolvar ', false ') = bits + boolvar | An Axiom |
| bitsxor-rec | ⊦ bitsxor(bits + boolvar ' + boolvar0 ', bits0 + boolvar1 ' + boolvar2 ') = bitsxor(bits + boolvar, bits0 + boolvar1) + (¬(boolvar0 ↔ boolvar2)) | An Axiom |
| bitsor-onel | ⊦ bitsor(true ', bits + boolvar ') = true ' | An Axiom |
| bitsor-oner | ⊦ bitsor(bits + boolvar ', true ') = true ' | An Axiom |
| bitsor-zerol | ⊦ bitsor(false ', bits + boolvar ') = bits + boolvar | An Axiom |
| bitsor-zeror | ⊦ bitsor(bits + boolvar ', false ') = bits + boolvar | An Axiom |
| bitsor-rec | ⊦ bitsor(bits + boolvar ' + boolvar0 ', bits0 + boolvar1 ' + boolvar2 ') = bitsor(bits + boolvar, bits0 + boolvar1) + (boolvar0 ∨ boolvar2) | An Axiom |
| intshiftleft | ⊦ i i<< j = bits2int(int2bits(i) + mklist(false, i→n(band(j, 31)))) | An Axiom |
| intshiftrsign | ⊦ i i>> j = bits2int(sublist(0, # int2bits(i), mklist(int2bits(i).first, i→n(band(j, 31))) + int2bits(i))) | An Axiom |
| cast-def | ⊦ cast(i, j) = bits2int(lastn(i→n(i), fillsgn(i→n(i), int2bits(j)))) | An Axiom |
| intshiftrzero-def | ⊦ i i>>> j = bits2int(sublist(0, # fillsgn(32, int2bits(i)), mklist(false, i→n(band(j, 31))) + fillsgn(32, int2bits(i)))) | An Axiom |
| longshiftrzero-def | ⊦ i l>>> j = bits2int(sublist(0, # fillsgn(64, int2bits(i)), mklist(false, i→n(band(j, 63))) + fillsgn(64, int2bits(i)))) | An Axiom |
| longshiftrsign | ⊦ i l>> j = bits2int(sublist(0, # int2bits(i), mklist(int2bits(i).first, i→n(band(j, 63))) + int2bits(i))) | An Axiom |
| longshiftleft | ⊦ i l<< j = bits2int(int2bits(i) + mklist(false, i→n(band(j, 63)))) | An Axiom |
| shiftrzero-def-01 | ⊦ >>>(n, i, j) = bits2int(sublist(0, # fillsgn(n, int2bits(i)), mklist(false, i→n(j)) + fillsgn(n, int2bits(i)))) | An Axiom |
| shiftrsign-01 | ⊦ i >> j = bits2int(sublist(0, # int2bits(i), mklist(int2bits(i).first, i→n(j)) + int2bits(i))) | An Axiom |
| shiftleft-01 | ⊦ i << j = bits2int(int2bits(i) + mklist(false, i→n(j))) | An Axiom |
| add-ones-grlen | ⊦ ¬ false ∈ bits ∧ # bits0 ≤ # bits ∧ bits0.first ∧ bits0 ≠ [] → bitsand(bits, bits0) = fillsgn(# bits, bits0) | A User Theorem |
| add-ones-grlen-01 | ⊦ ¬ false ∈ bits ∧ # bits0 ≤ # bits ∧ bits0.first ∧ bits0 ≠ [] → bitsand(bits0, bits) = fillsgn(# bits, bits0) | A User Theorem |
| add-ones-grlen-02 | ⊦ ¬ false ∈ bits ∧ # bits0 ≤ # bits ∧ ¬ bits0.first ∧ bits0 ≠ [] → bitsand(bits, bits0) = bits0 | A User Theorem |
| add-ones-lelen | ⊦ ¬ false ∈ bits ∧ # bits ≤ # bits0 ∧ bits ≠ [] → bitsand(bits, bits0) = bits0 | A User Theorem |
| add-ones-lelen-01 | ⊦ ¬ false ∈ bits ∧ # bits ≤ # bits0 ∧ bits ≠ [] → bitsand(bits0, bits) = bits0 | A User Theorem |
| and-011x-neg | ¬ false ∈ bits0, bits ≠ [], bits.first, bitsand(false ' + bits0, bits) = false ' + bits1 ⊦ bits2uint(bits1) = 2 ^ n→i(# bits0) - bits2uint(bitsinvert(bits)) % 2 ^ n→i(# bits0) + 1 | A User Theorem |
| and-ass | ⊦ bits ≠ [] ∧ bits0 ≠ [] ∧ bits1 ≠ [] → bitsand(bits, bitsand(bits0, bits1)) = bitsand(bitsand(bits, bits0), bits1) | A User Theorem |
| and-bits2int-sgn | ⊦ bits ≠ [] ∧ bits0 ≠ [] → bits2int(bitsand(sgn(bits), bits0)) = bits2int(bitsand(bits, bits0)) | A User Theorem |
| and-com | ⊦ bits ≠ [] ∧ bits0 ≠ [] → bitsand(bits, bits0) = bitsand(bits0, bits) | A User Theorem |
| and-false | ⊦ bits.first ∧ bits0.first ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsand(bits, bits0) ≠ false ' + bits1 | A User Theorem |
| and-first | ⊦ bits ≠ [] ∧ bits0 ≠ [] → (bitsand(bits, bits0).first ↔ bits.first ∧ bits0.first) | A User Theorem |
| and-insgn | ⊦ bits ≠ [] ∧ bits0 ≠ [] → (boolvar ∈ bitsand(sgn(bits), bits0) ↔ boolvar ∈ bitsand(bits, bits0)) | A User Theorem |
| and-notempty | ⊦ bits ≠ [] ∧ bits0 ≠ [] → bitsand(bits, bits0) ≠ [] | A User Theorem |
| and-notempty-01 | ⊦ bits ≠ [] → bitsand(bits, boolvar ' + bits0) ≠ [] | A User Theorem |
| and-notempty-02 | ⊦ bits0 ≠ [] → bitsand(boolvar ' + bits, bits0) ≠ [] | A User Theorem |
| and-notempty-03 | ⊦ bits ≠ [] → bitsand(bits, bits0 + boolvar ') ≠ [] | A User Theorem |
| and-notempty-04 | ⊦ bits0 ≠ [] → bitsand(bits + boolvar ', bits0) ≠ [] | A User Theorem |
| and-notempty-05 | ⊦ bitsand(boolvar0 ' + bits, boolvar ' + bits0) ≠ [] | A User Theorem |
| and-notempty-06 | ⊦ bitsand(boolvar ' + bits, boolvar0 ' + bits0) ≠ [] | A User Theorem |
| and-notempty-07 | ⊦ bits ≠ [] → bitsand(bits, bits1 + boolvar ' + bits0) ≠ [] | A User Theorem |
| and-notempty-08 | ⊦ bits0 ≠ [] → bitsand(bits1 + boolvar ' + bits, bits0) ≠ [] | A User Theorem |
| and-notempty-09 | ⊦ bitsand(int2bits(i), int2bits(i0)) ≠ [] | A User Theorem |
| and-notone | ⊦ bits ≠ [] → ¬ bitsand(bits, false ' + bits0).first | A User Theorem |
| and-notone-01 | ⊦ bits ≠ [] → bitsand(bits, false ' + bits0) ≠ true ' + bits1 | A User Theorem |
| and-notone-02 | ⊦ bits ≠ [] → bitsand(bits, false ' + bits0) + bits2 ≠ true ' + bits1 | A User Theorem |
| and-notone-03 | ⊦ bits ≠ [] ∧ bits0 ≠ [] ∧ ¬ bits0.first → bitsand(bits, bits0) ≠ true ' + bits1 | A User Theorem |
| and-one | ⊦ bitsand(boolvar ', boolvar0 ') = (boolvar ∧ boolvar0)' | A User Theorem |
| and-one-01 | bits ≠ [], bits0 ≠ [] ⊦ bitsand(bits, bits0) = true ' + bits1 → bits.first ∧ bits0.first | A User Theorem |
| and-onel-01 | ⊦ bits ≠ [] → bitsand(true ', bits) = bits | A User Theorem |
| and-onel-02 | ⊦ bitsand(true ', boolvar ' + bits) = boolvar ' + bits | A User Theorem |
| and-oner | ⊦ bitsand(boolvar ' + bits, true ') = boolvar ' + bits | A User Theorem |
| and-oner-01 | ⊦ bits ≠ [] → bitsand(bits, true ') = bits | A User Theorem |
| and-ones | ⊦ bits ≠ [] ∧ ¬ false ∈ bits ∧ ¬ false ∈ bits0 → bitsand(bits, false ' + bits0) = false ' + bits0 | A User Theorem |
| and-onesin | ⊦ ¬ false ∈ bits ∧ bits ≠ [] ∧ bits0 ≠ [] → (boolvar ∈ bitsand(bits, bits0) ↔ boolvar ∈ bits0) | A User Theorem |
| and-pos | ⊦ bits ≠ [] ∧ bits0 ≠ [] ∧ ¬ bits.first ∧ ¬ bits0.first → ¬ bitsand(bits, bits0).first | A User Theorem |
| and-rec | ⊦ 1 < # bits ∧ 1 < # bits0 → bitsand(bits, bits0) = bitsand(bits.butlast, bits0.butlast) + (bits.last ∧ bits0.last) | A User Theorem |
| and-rec-01 | ⊦ bits ≠ [] ∧ bits0 = true ' → bitsand(bits, bits0) = bits | A User Theorem |
| and-rec-02 | ⊦ bits ≠ [] ∧ bits0 = false ' → bitsand(bits, bits0) = false ' | A User Theorem |
| and-rec-03 | ⊦ bits0 ≠ [] ∧ bits = true ' → bitsand(bits, bits0) = bits0 | A User Theorem |
| and-rec-04 | ⊦ bits0 ≠ [] ∧ bits = false ' → bitsand(bits, bits0) = false ' | A User Theorem |
| and-rec-05 | ⊦ bitsand(bits + boolvar ' + true ', bits0 + boolvar1 ' + true ') = bitsand(bits + boolvar, bits0 + boolvar1) + true ' | A User Theorem |
| and-rec-06 | ⊦ bits ≠ [] ∧ bits0 ≠ [] → bitsand(bits0 + boolvar0 ', boolvar1 ' + bits) = bitsand(bits0, boolvar1 ' + bits.butlast) + (boolvar0 ∧ bits.last) | A User Theorem |
| and-rec-07 | ⊦ bitsand(boolvar ' + boolvar0 ', bits0 + boolvar1 ' + boolvar2 ') = bitsand(boolvar ', bits0 + boolvar1 ') + (boolvar0 ∧ boolvar2) | A User Theorem |
| and-rec-08 | ⊦ bitsand(bits + boolvar ' + boolvar0 ', boolvar1 ' + boolvar2 ') = bitsand(bits + boolvar ', boolvar1 ') + (boolvar0 ∧ boolvar2) | A User Theorem |
| and-rec-09 | ⊦ bits ≠ [] → bitsand(boolvar ' + boolvar0 ', boolvar1 ' + bits) = bitsand(boolvar ', boolvar1 ' + bits.butlast) + (boolvar0 ∧ bits.last) | A User Theorem |
| and-rec-10 | ⊦ bitsand(bits + boolvar ' + false ', bits0 + boolvar1 ' + true ') = bitsand(bits + boolvar, bits0 + boolvar1) + false ' | A User Theorem |
| and-rec-11 | ⊦ bitsand(bits + boolvar ' + true ', bits0 + boolvar1 ' + false ') = bitsand(bits + boolvar, bits0 + boolvar1) + false ' | A User Theorem |
| and-rec-12 | ⊦ bitsand(bits + boolvar ' + false ', bits0 + boolvar1 ' + false ') = bitsand(bits + boolvar, bits0 + boolvar1) + false ' | A User Theorem |
| and-sgn | ⊦ bits ≠ [] ∧ bits0 ≠ [] → sgn(bitsand(sgn(bits), bits0)) = sgn(bitsand(bits, bits0)) | A User Theorem |
| and-size-one | ⊦ bits.first ∧ # bits ≤ # bits1 ∧ bits ≠ [] → bitsand(bits, bits0 + bits1) = bits0 + bitsand(bits, bits1) | A User Theorem |
| and-size-one-01 | ⊦ bits.first ∧ # bits = # bits1 + 1 ∧ bits1 ≠ [] ∧ bits0 ≠ [] → bitsand(bits, bits0 + bits1) = bits0 + bitsand(bits.rest, bits1) | A User Theorem |
| and-true | ⊦ bits ≠ [] ∧ bits0 ≠ [] → (bitsand(bits, bits0) = true ' ↔ bits = true ' ∧ bits0 = true ') | A User Theorem |
| and-two | ⊦ bitsand(boolvar ' + boolvar0 ', boolvar1 ' + boolvar2 ') = (boolvar ∧ boolvar1)' + (boolvar0 ∧ boolvar2)' | A User Theorem |
| and-two-02 | ⊦ bitsand(boolvar ' + true ', bits0 + boolvar1 ' + true ') = bitsand(boolvar ', bits0 + boolvar1) + true ' | A User Theorem |
| and-two-03 | ⊦ bitsand(boolvar ' + false ', bits0 + boolvar1 ' + true ') = bitsand(boolvar ', bits0 + boolvar1) + false ' | A User Theorem |
| and-two-04 | ⊦ bitsand(boolvar ' + true ', bits0 + boolvar1 ' + false ') = bitsand(boolvar ', bits0 + boolvar1) + false ' | A User Theorem |
| and-two-05 | ⊦ bitsand(boolvar ' + false ', bits0 + boolvar1 ' + false ') = bitsand(boolvar ', bits0 + boolvar1) + false ' | A User Theorem |
| and-two-06 | ⊦ bitsand(bits + boolvar ' + true ', boolvar1 ' + true ') = bitsand(bits + boolvar, boolvar1 ') + true ' | A User Theorem |
| and-two-07 | ⊦ bitsand(bits + boolvar ' + false ', boolvar1 ' + true ') = bitsand(bits + boolvar, boolvar1 ') + false ' | A User Theorem |
| and-two-08 | ⊦ bitsand(bits + boolvar ' + true ', boolvar1 ' + false ') = bitsand(bits + boolvar, boolvar1 ') + false ' | A User Theorem |
| and-two-09 | ⊦ bitsand(bits + boolvar ' + false ', boolvar1 ' + false ') = bitsand(bits + boolvar, boolvar1 ') + false ' | A User Theorem |
| and-zero-01 | ⊦ bitsand(false ', boolvar ' + bits) = false ' | A User Theorem |
| and-zero-02 | ⊦ bits ≠ [] → bitsand(false ', bits) = false ' | A User Theorem |
| and-zero-03 | ⊦ bits ≠ [] → bitsand(bits, false ') = false ' | A User Theorem |
| and-zerosin | ⊦ ¬ true ∈ bits ∧ bits ≠ [] ∧ bits0 ≠ [] → ¬ true ∈ bitsand(bits, bits0) | A User Theorem |
| band-011x | ⊦ band(4294967295, ~2147483648) = 2147483648 | A User Theorem |
| band-011x-eq | ⊦ ¬ false ∈ int2bits(i).rest ∧ 0 ≤ i → band(i - j, i) + band(j, i) = i | A User Theorem |
| band-011x-eq-01 | ⊦ ¬ false ∈ int2bits(i).rest ∧ 0 ≤ i → band(i - j, i) = i - band(j, i) | A User Theorem |
| band-011x-is-lastn | ⊦ i→n(i) ≤ # int2bits(j) ∧ 0 < i → band(j, 2 ^ i - 1) = bits2uint(lastn(i→n(i), int2bits(j))) | A User Theorem |
| band-011x-is-unsigned | ⊦ abs(j) ≤ 2 ^ (i - 1) ∧ 0 < i → band(j, 2 ^ i - 1) = bits2uint(fillsgn(i→n(i), int2bits(j))) | A User Theorem |
| band-011x-is-unsigned-01 | ⊦ ¬ false ∈ int2bits(i0).rest ∧ abs(j) ≤ 2 ^ n→i(# int2bits(i0) - 2) ∧ 0 < i0 → band(j, i0) = bits2uint(fillsgn(# int2bits(i0) - 1, int2bits(j))) | A User Theorem |
| band-011x-is-unsigned-03 | ⊦ i→n(i) = # int2bits(j) ∧ 0 < i → band(j, 2 ^ i - 1) = bits2uint(int2bits(j)) | A User Theorem |
| band-011x-is-unsigned-fix | ⊦ 0 < i → band(j, 2 ^ i - 1) = bits2uint(fix(i→n(i), int2bits(j))) | A User Theorem |
| band-011x-is-unsigned-fix-01 | ⊦ ¬ false ∈ int2bits(i).rest ∧ 0 ≤ i → band(j, i) = bits2uint(fix((# int2bits(i))-1, int2bits(j))) | A User Theorem |
| band-011x-is-unsigned-fix-02 | ⊦ band(j, 4294967295) = bits2uint(fix(32, int2bits(j))) | A User Theorem |
| band-011x-is-unsigned-fix-03 | ⊦ bits2uint(fix(32, int2bits(j))) = band(j, 4294967295) | A User Theorem |
| band-011x-neg | ⊦ j < 0 ∧ 0 ≤ i → band(j, 2 ^ i - 1) = (j + 1) % 2 ^ i + 2 ^ i - 1 | A User Theorem |
| band-011x-neg-01 | ⊦ j < 0 ∧ ¬ false ∈ int2bits(i).rest ∧ 0 ≤ i → band(j, i) = (j + 1) % 2 ^ n→i(# int2bits(i) - 1) + 2 ^ n→i(# int2bits(i) - 1) - 1 | A User Theorem |
| band-011x-neg-02 | ⊦ j < 0 ∧ ¬ false ∈ int2bits(i).rest ∧ 0 ≤ i → band(j, i) = (j + 1) % (i + 1) + i | A User Theorem |
| band-011x-neg-03 | ⊦ ¬ false ∈ int2bits(i).rest ∧ 0 ≤ i → band(~ j, i) = band(i + 1 - j, i) | A User Theorem |
| band-011x-neg-04 | ⊦ ¬ false ∈ int2bits(i).rest ∧ 0 ≤ i → band(j, i) = band((i + 1) + j, i) | A User Theorem |
| band-011x-pos | ⊦ 0 ≤ j ∧ 0 ≤ i → band(j, 2 ^ i - 1) = j % 2 ^ i | A User Theorem |
| band-011x-pos-01 | ⊦ 0 ≤ j ∧ ¬ false ∈ int2bits(i).rest ∧ 0 ≤ i → band(j, i) = j % 2 ^ n→i(# int2bits(i) - 1) | A User Theorem |
| band-011x-pos-02 | ⊦ 0 ≤ j ∧ ¬ false ∈ int2bits(i).rest ∧ 0 ≤ i → band(j, i) = j % (i + 1) | A User Theorem |
| band-011x-zero | ⊦ band(4294967295, i) ≤ 0 ↔ band(4294967295, i) = 0 | A User Theorem |
| band-255-neg | ⊦ i < 0 → band(i, 255) = (i + 1) % 256 + 255 | A User Theorem |
| band-255-pos | ⊦ 0 ≤ i → band(i, 255) = i % 256 | A User Theorem |
| band-31-pos | ⊦ 0 ≤ i ∧ i < 32 → band(i, 31) = i | A User Theorem |
| band-31-pos-01 | ⊦ 0 ≤ i ∧ i ≤ 31 → band(i, 31) = i | A User Theorem |
| band-31-pos-02 | ⊦ 0 < i ∧ i < 32 → band(i, 31) = i | A User Theorem |
| band-32-not-neg | ⊦ ¬ band(4294967295, i) + band(4294967295, j) < 0 | A User Theorem |
| band-63-lezero | ⊦ band(j, 63) ≤ 0 ↔ band(j, 63) = 0 | A User Theorem |
| band-63-pos | ⊦ 0 ≤ i ∧ i < 64 → band(i, 63) = i | A User Theorem |
| band-63-pos-01 | ⊦ 0 ≤ i ∧ i ≤ 63 → band(i, 63) = i | A User Theorem |
| band-63-pos-02 | ⊦ 0 < i ∧ i < 64 → band(i, 63) = i | A User Theorem |
| band-65535-neg | ⊦ i < 0 → band(i, 65535) = (i + 1) % 65536 + 65535 | A User Theorem |
| band-65535-pos | ⊦ 0 ≤ i → band(i, 65535) = i % 65536 | A User Theorem |
| band-associativity | ⊦ band(i, band(i0, j)) = band(band(i, i0), j) | A User Theorem |
| band-bitlength | # int2bits(i) < n, # int2bits(j) < n ⊦ # int2bits(band(i, j)) < n | A User Theorem |
| band-commutativity | ⊦ band(i, j) = band(j, i) | A User Theorem |
| band-idempotent | ⊦ band(band(i, j), j) = band(i, j) | A User Theorem |
| band-idempotent-01 | ⊦ band(i, i) = i | A User Theorem |
| band-le-zero | ⊦ band(j, 31) ≤ 0 ↔ band(j, 31) = 0 | A User Theorem |
| band-ls-zero-01 | ⊦ ¬ band(j, 31) < 0 | A User Theorem |
| band-max | ⊦ 0 ≤ i → ¬ i < band(i, j) | A User Theorem |
| band-max-01 | ⊦ 0 ≤ j → ¬ j < band(i, j) | A User Theorem |
| band-max-02 | ⊦ 0 ≤ i ∧ i ≤ i0 → ¬ i0 < band(i, j) | A User Theorem |
| band-max-03 | ⊦ 0 ≤ i ∧ i ≤ i0 → ¬ i0 < band(j, i) | A User Theorem |
| band-max-04 | ⊦ ¬ 256 ≤ band(i, 255) | A User Theorem |
| band-max-05 | ⊦ 0 ≤ i ∧ i < i0 → ¬ i0 ≤ band(i, j) | A User Theorem |
| band-max-06 | ⊦ 0 ≤ i ∧ i < i0 → ¬ i0 ≤ band(j, i) | A User Theorem |
| band-min | ⊦ i0 ≤ ~(2 ^ n→i(# int2bits(i))) ∧ # int2bits(i) = # int2bits(j) ∧ i ≤ 0 ∧ j ≤ 0 → ¬ band(i, j) < i0 | A User Theorem |
| band-min-01 | ⊦ i0 ≤ ~(2 ^ n→i(# int2bits(i))) ∧ i0 ≤ ~(2 ^ n→i(# int2bits(j))) → ¬ band(i, j) < i0 | A User Theorem |
| band-min-02 | ⊦ i0 ≤ ~(2 ^ (n→i(# int2bits(i)) - 1)) ∧ i0 ≤ ~(2 ^ (n→i(# int2bits(j)) - 1)) → ¬ band(i, j) < i0 | A User Theorem |
| band-minus-one | ⊦ band(~1, i) = i | A User Theorem |
| band-mod256-neg | ⊦ 0 ≤ i ∧ 127 < i % 256 → band(255, i % 256 - 256) = i % 256 | A User Theorem |
| band-mod256-pos | ⊦ 0 ≤ i → band(255, i % 256) = i % 256 | A User Theorem |
| band-neg | ⊦ i < 0 ∧ j < 0 → ¬ 0 ≤ band(i, j) | A User Theorem |
| band-notneg | ⊦ 0 ≤ i → ¬ band(i, j) < 0 | A User Theorem |
| band-notneg-01 | ⊦ 0 ≤ j → ¬ band(i, j) < 0 | A User Theorem |
| band-num | ⊦ band((* i), (* j)) = bits2int(bitsand(int2bits(i), int2bits(j))) | A User Theorem |
| band-one-is-mod2 | ⊦ 0 ≤ i → (band(i, 1) = 1 ↔ i % 2 = 1) | A User Theorem |
| band-zero | ⊦ band(0, i) = 0 | A User Theorem |
| bcompl-absorption | ⊦ bcompl(bcompl(i)) = i | A User Theorem |
| bcompl-num | ⊦ bcompl((* i)) = bits2int(bitsinvert(int2bits(i))) | A User Theorem |
| bcompl-size | ⊦ # int2bits(bcompl(i)) ≤ # int2bits(i) | A User Theorem |
| bcompl-size-01 | ⊦ ¬ # int2bits(i) < # int2bits(bcompl(i)) | A User Theorem |
| bits2int-is-cast | ⊦ n < # int2bits(i) → bits2int(lastn(n, int2bits(i))) = cast(n→i(n), i) | A User Theorem |
| bits2int-is-cast-01 | ⊦ bits2int(lastn(n, fillsgn(n, int2bits(i)))) = cast(n→i(n), i) | A User Theorem |
| bitsand-app | ⊦ # bits = # bits1 ∧ bits0 ≠ [] ∧ bits2 ≠ [] ∧ bits ≠ [] → bitsand(bits0 + bits, bits2 + bits1) = bitsand(bits0, bits2) + bitsand(bits, bits1) | A User Theorem |
| bitsand-app-false | ⊦ # bits1 ≤ # bits0 ∧ bits1 ≠ [] ∧ ¬ bits1.first → bitsand(bits + bits0, bits1) = bitsand(bits0, bits1) | A User Theorem |
| bitsand-app-ones | ⊦ ¬ false ∈ bits → bitsand(bits + true ' + bits0, false ' + bits1) = bitsand(true ' + bits0, false ' + bits1) | A User Theorem |
| bitsand-app-true | ⊦ # bits1 ≤ # bits0 ∧ bits1 ≠ [] ∧ bits1.first → bitsand(bits + bits0, bits1) = bits + bitsand(bits0, bits1) | A User Theorem |
| bitsand-app-zeros | ⊦ ¬ true ∈ bits → sgn(bitsand(bits + false ' + bits0, false ' + bits1)) = sgn(bitsand(false ' + bits0, false ' + bits1)) | A User Theorem |
| bitsand-app-zeros-01 | ⊦ ¬ true ∈ bits ∧ bits1 ≠ [] → sgn(bitsand(bits + false ' + bits0, bits1)) = sgn(bitsand(false ' + bits0, bits1)) | A User Theorem |
| bitsand-cast | ⊦ bits ≠ [] ∧ bits0 ≠ [] → lastn(n, fillsgn(n, bitsand(sgn(lastn(n, fillsgn(n, bits))), bits0))) = lastn(n, fillsgn(n, bitsand(bits, bits0))) | A User Theorem |
| bitsand-cast-01 | ⊦ bits ≠ [] ∧ bits0 ≠ [] → lastn(n, fillsgn(n, bitsand(lastn(n, fillsgn(n, bits)), bits0))) = lastn(n, fillsgn(n, bitsand(bits, bits0))) | A User Theorem |
| bitsand-cast-04 | ⊦ # bits0 ≤ n ∧ ¬ bits0.first ∧ bits ≠ [] ∧ bits0 ≠ [] → sgn(bitsand(lastn(n, fillsgn(n, bits)), bits0)) = sgn(bitsand(bits, bits0)) | A User Theorem |
| bitsand-cast-05 | ⊦ (# bits0)-1 ≤ n ∧ ¬ bits0.first ∧ n ≠ 0 ∧ bits ≠ [] ∧ bits0 ≠ [] → sgn(bitsand(lastn(n, fillsgn(n, bits)), bits0)) = sgn(bitsand(bits, bits0)) | A User Theorem |
| bitsand-false | ⊦ bitsand(false ', int2bits(i)) = false ' | A User Theorem |
| bitsand-false-01 | ⊦ bitsand(int2bits(i), false ') = false ' | A User Theorem |
| bitsand-fillsgn | ⊦ bits ≠ [] ∧ bits0 ≠ [] → fillsgn(n, bitsand(fillsgn(n, bits), bits0)) = fillsgn(n, bitsand(bits, bits0)) | A User Theorem |
| bitsand-first-samesize | ⊦ # bits = # bits0 ∧ 1 < # bits → bitsand(bits, bits0) = (bits.first ∧ bits0.first)' + bitsand(bits.rest, bits0.rest) | A User Theorem |
| bitsand-idempotent | ⊦ bits ≠ [] → bitsand(bits, bits) = bits | A User Theorem |
| bitsand-len-false | ⊦ ¬ bits0.first ∧ # bits0 ≤ # bits ∧ bits0 ≠ [] → # bitsand(bits, bits0) = # bits0 | A User Theorem |
| bitsand-len-true | ⊦ bits0.first ∧ # bits0 ≤ # bits ∧ bits0 ≠ [] → # bitsand(bits, bits0) = # bits | A User Theorem |
| bitsand-onein | ⊦ ¬ true ∈ bits ∧ bits1 ≠ [] → (true ∈ bitsand(bits + false ' + bits0, bits1) ↔ true ∈ bitsand(false ' + bits0, bits1)) | A User Theorem |
| bitsand-true | ⊦ bitsand(true ', int2bits(i)) = int2bits(i) | A User Theorem |
| bitsand-zero-in | ⊦ bits ≠ [] ∧ bits0 ≠ [] → (false ∈ bitsand(bits, bits0) ↔ false ∈ bits ∨ false ∈ bits0) | A User Theorem |
| bitsand-zeros | ⊦ ¬ true ∈ bits ∧ (# bits ≤ # bits0 ∨ bits0.first) ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsand(bits, bits0) = bits | A User Theorem |
| bitsand-zeros-01 | ⊦ ¬ true ∈ bits ∧ (# bits0 < # bits ∧ ¬ bits0.first) ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsand(bits, bits0) = mklist(false, # bits0) | A User Theorem |
| bitsand-zeros-02 | ⊦ ¬ true ∈ bits ∧ bits ≠ [] ∧ bits0 ≠ [] → sgn(bitsand(bits, bits0)) = false ' | A User Theorem |
| bitsor-app | ⊦ # bits0 = # bits2 ∧ bits ≠ [] ∧ bits0 ≠ [] ∧ bits1 ≠ [] ∧ bits2 ≠ [] → bitsor(bits + bits0, bits1 + bits2) = bitsor(bits, bits1) + bitsor(bits0, bits2) | A User Theorem |
| bitsor-bi-ones | ⊦ ¬ false ∈ bits ∧ bits ≠ [] ∧ bits0 ≠ [] → bits2int(bitsor(bits, bits0) + bits1) = bits2int(true ' + bits1) | A User Theorem |
| bitsor-bi-sgn | ⊦ bits ≠ [] ∧ bits0 ≠ [] → bits2int(bitsor(sgn(bits), bits0)) = bits2int(bitsor(bits, bits0)) | A User Theorem |
| bitsor-bi-zeroes | ⊦ ¬ true ∈ bits ∧ bits ≠ [] ∧ bits0 ≠ [] → bits2int(bitsor(bits, bits0) + bits1) = bits2int(bits0 + bits1) | A User Theorem |
| bitsor-com | ⊦ bits ≠ [] ∧ bits0 ≠ [] → bitsor(bits, bits0) = bitsor(bits0, bits) | A User Theorem |
| bitsor-empty | ⊦ bits ≠ [] ∧ bits0 ≠ [] → bitsor(bits, bits0) ≠ [] | A User Theorem |
| bitsor-first | ⊦ bits0 ≠ [] → bitsor(true ' + bits, bits0) ≠ false ' + bits1 | A User Theorem |
| bitsor-first-01 | ⊦ bits ≠ [] ∧ bits0 ≠ [] → (bitsor(bits, bits0).first ↔ bits.first ∨ bits0.first) | A User Theorem |
| bitsor-first-02 | ⊦ ¬ bits.first ∧ ¬ bits0.first ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsor(bits, bits0) ≠ true ' + bits1 | A User Theorem |
| bitsor-mklist-in | ⊦ n ≠ 0 ∧ bits0 ≠ [] → (boolvar ∈ bitsor(mklist(boolvar0, n) + bits, bits0) ↔ boolvar ∈ bitsor(boolvar0 ' + bits, bits0)) | A User Theorem |
| bitsor-ones-false | ⊦ ¬ false ∈ bits ∧ ¬ bits0.first ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsor(bits, bits0) = bits | A User Theorem |
| bitsor-ones-samelen | ⊦ ¬ false ∈ bits ∧ # bits = # bits0 ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsor(bits, bits0) = bits | A User Theorem |
| bitsor-ones-true | ⊦ ¬ false ∈ bits ∧ bits0.first ∧ # bits ≤ # bits0 ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsor(bits, bits0) = bits | A User Theorem |
| bitsor-sgn-in | ⊦ bits ≠ [] ∧ bits0 ≠ [] → (boolvar ∈ bitsor(sgn(bits), bits0) ↔ boolvar ∈ bitsor(bits, bits0)) | A User Theorem |
| bitsor-zeroes-false | ⊦ ¬ true ∈ bits ∧ ¬ bits0.first ∧ # bits ≤ # bits0 ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsor(bits, bits0) = bits0 | A User Theorem |
| bitsor-zeroes-samelen | ⊦ ¬ true ∈ bits ∧ # bits = # bits0 ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsor(bits, bits0) = bits0 | A User Theorem |
| bitsor-zeroes-true | ⊦ ¬ true ∈ bits ∧ bits0.first ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsor(bits, bits0) = bits0 | A User Theorem |
| bitsxor-append-same-size | ⊦ # bits0 = # bits2 ∧ bits ≠ [] ∧ bits0 ≠ [] ∧ bits1 ≠ [] → bitsxor(bits + bits0, bits1 + bits2) = bitsxor(bits, bits1) + bitsxor(bits0, bits2) | A User Theorem |
| bitsxor-bit | ⊦ bitsxor(boolvar ', boolvar0 ') = (¬(boolvar ↔ boolvar0))' | A User Theorem |
| bitsxor-empty | ⊦ bits ≠ [] ∧ bits0 ≠ [] → bitsxor(bits, bits0) ≠ [] | A User Theorem |
| bitsxor-first | ⊦ # bits = # bits0 ∧ 1 < # bits → bitsxor(bits, bits0) = (¬(bits.first ↔ bits0.first))' + bitsxor(bits.rest, bits0.rest) | A User Theorem |
| bitsxor-is-orand | ⊦ bits ≠ [] ∧ bits0 ≠ [] → bits2int(bitsxor(bits, bits0)) = bits2int(bitsor(bitsand(bitsinvert(bits), bits0), bitsand(bitsinvert(bits0), bits))) | A User Theorem |
| bitsxor-rec-01 | ⊦ 1 < # bits ∧ 1 < # bits0 → bitsxor(bits, bits0) = bitsxor(bits.butlast, bits0.butlast) + (¬(bits.last ↔ bits0.last)) | A User Theorem |
| bitsxor-rec-01-01 | ⊦ bits ≠ [] ∧ bits0 = true ' → bitsxor(bits, bits0) = bitsinvert(bits) | A User Theorem |
| bitsxor-rec-02 | ⊦ bits ≠ [] ∧ bits0 = false ' → bitsxor(bits, bits0) = bits | A User Theorem |
| bitsxor-rec-03 | ⊦ bits0 ≠ [] ∧ bits = true ' → bitsxor(bits, bits0) = bitsinvert(bits0) | A User Theorem |
| bitsxor-rec-04 | ⊦ bits0 ≠ [] ∧ bits = false ' → bitsxor(bits, bits0) = bits0 | A User Theorem |
| bitsxor-zeros | ⊦ ¬ true ∈ bits0 ∧ # bits0 ≤ # bits ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsxor(bits, bits0) = bits | A User Theorem |
| bitsxor-zeros-01 | ⊦ n ≤ # bits ∧ bits ≠ [] ∧ n ≠ 0 → bitsxor(bits, mklist(false, n)) = bits | A User Theorem |
| bor-256-plus | ⊦ j0 < 256 ∧ 0 ≤ j0 ∧ 0 ≤ j → bor(j * 256, j0) = j * 256 + j0 | A User Theorem |
| bor-256-plus-01 | ⊦ j0 < 256 ∧ 0 ≤ j0 → bor(j * 256, j0) = j * 256 + j0 | A User Theorem |
| bor-2pot-plus | ⊦ j0 < 2 ^ i ∧ 0 ≤ i ∧ 0 ≤ j0 ∧ 0 ≤ j → bor(j * 2 ^ i, j0) = j * 2 ^ i + j0 | A User Theorem |
| bor-2pot-plus-01 | ⊦ j0 < 2 ^ i ∧ 0 ≤ i ∧ 0 ≤ j0 ∧ j < 0 → bor(j * 2 ^ i, j0) = j * 2 ^ i + j0 | A User Theorem |
| bor-2pot-plus-02 | ⊦ j0 < 2 ^ i ∧ 0 ≤ i ∧ 0 ≤ j0 → bor(j * 2 ^ i, j0) = j * 2 ^ i + j0 | A User Theorem |
| bor-65536-plus | ⊦ j0 < 65536 ∧ 0 ≤ j0 → bor(j * 65536, j0) = j * 65536 + j0 | A User Theorem |
| bor-assoc | ⊦ bor(bor(i, i0), j0) = bor(i, bor(i0, j0)) | A User Theorem |
| bor-bitlength | # int2bits(i) < n, # int2bits(j) < n ⊦ # int2bits(bor(i, j)) < n | A User Theorem |
| bor-com | ⊦ bor(i, j) = bor(j, i) | A User Theorem |
| bor-neq | ⊦ bor(i, j) ≠ bor(i0, j) → i ≠ i0 | A User Theorem |
| bor-notAndNot | ⊦ bor(i, j) = bcompl(band(bcompl(i), bcompl(j))) | A User Theorem |
| bor-num | ⊦ bor((* i), (* j)) = bits2int(bitsor(int2bits(i), int2bits(j))) | A User Theorem |
| bor-shift-plus | ⊦ j0 < 2 ^ i ∧ 0 ≤ j0 ∧ 0 ≤ i ∧ i < 32 → bor(j i<< i, j0) = j * 2 ^ i + j0 | A User Theorem |
| bor-zero | ⊦ bor(i, 0) = i | A User Theorem |
| bxor-bitlength | # int2bits(i) < n, # int2bits(j) < n ⊦ # int2bits(bxor(i, j)) < n | A User Theorem |
| bxor-com | ⊦ bxor(i, j) = bxor(j, i) | A User Theorem |
| bxor-def-logic | ⊦ bxor(i, j) = bor(band(i, bcompl(j)), band(bcompl(i), j)) | A User Theorem |
| bxor-flip-one-bit | 2 ^ (j + 1) < i ∧ 0 ≤ i ∧ 0 ≤ j, boolvar ↔ int2bits(i)[# int2bits(i) - i→n(j) +1] ⊦ (int2bits(bxor(i, 2 ^ j))[# int2bits(i) - i→n(j) +1] ↔ ¬ boolvar) ∧ int2bits(bxor(i, 2 ^ j))[# int2bits(i) - i→n(j) +1, boolvar] = int2bits(i) | A User Theorem |
| bxor-minus-one | ⊦ bxor(i, ~1) = bcompl(i) | A User Theorem |
| bxor-num | ⊦ bxor((* i), (* j)) = bits2int(bitsxor(int2bits(i), int2bits(j))) | A User Theorem |
| bxor-zero | ⊦ bxor(i, 0) = i | A User Theorem |
| cast-add-2pot | ⊦ 0 < i → cast(i, j + 2 ^ i) = cast(i, j) | A User Theorem |
| cast-add-2pot-01 | ⊦ 0 < i → cast(i, ~(j + 2 ^ i)) = cast(i, ~ j) | A User Theorem |
| cast-add-2pot-h | ⊦ ~(2 ^ i) < j ∧ j < 0 ∧ 0 < i → cast(i, j + 2 ^ i) = cast(i, j) | A User Theorem |
| cast-band | n→i((# int2bits(j0))-1) ≤ i, 0 ≤ j0 ⊦ band(cast(i, j), j0) = band(j, j0) | A User Theorem |
| cast-cast | ⊦ 0 < i → cast(i, cast(i, j)) = cast(i, j) | A User Theorem |
| cast-help-comm | 0 < i, 0 < i0, i < i0 ⊦ cast(i, cast(i0, j)) = cast(i0, cast(i, j)) | A User Theorem |
| cast-if | ⊦ 0 < i → cast(i, j) = (0 ≤ j ∧ j % 2 ^ i ≤ 2 ^ (i - 1) - 1 ⊃ j % 2 ^ i ;(0 ≤ j ∧ 2 ^ (i - 1) - 1 < j % 2 ^ i ⊃ j % 2 ^ i - 2 ^ i ;(j < 0 ∧ j % 2 ^ i < ~(2 ^ (i - 1)) ⊃ j % 2 ^ i + 2 ^ i;(j < 0 ∧ ~(2 ^ (i - 1)) ≤ j % 2 ^ i ⊃ j % 2 ^ i;j)) ) ) | A User Theorem |
| cast-law-absorption | 0 < i, i ≤ i0 ⊦ cast(i, cast(i0, j)) = cast(i, j) | A User Theorem |
| cast-law-add | 0 < i ⊦ cast(i, j + j0) = cast(i, cast(i, j) + cast(i, j0)) | A User Theorem |
| cast-law-add-one | 0 < i ⊦ cast(i, j + j0) = cast(i, cast(i, j) + j0) | A User Theorem |
| cast-law-add-pos | ⊦ 0 ≤ j ∧ 0 ≤ j0 ∧ 0 < i → cast(i, j + j0) = cast(i, cast(i, j) + j0) | A User Theorem |
| cast-law-add-pos-01 | ⊦ 0 ≤ j ∧ 0 < i → cast(i, j + j0) = cast(i, cast(i, j) + j0) | A User Theorem |
| cast-law-and-one | 0 < i ⊦ cast(i, band(j, j0)) = cast(i, band(cast(i, j), j0)) | A User Theorem |
| cast-law-comm | 0 < i, 0 < i0 ⊦ cast(i, cast(i0, j)) = cast(i0, cast(i, j)) | A User Theorem |
| cast-law-compl | 0 < i ⊦ cast(i, bcompl(j)) = cast(i, bcompl(cast(i, j))) | A User Theorem |
| cast-law-leftshift | 0 < i ⊦ cast(i, j i<< j0) = cast(i, cast(i, j) i<< j0) | A User Theorem |
| cast-law-mult | 0 < i ⊦ cast(i, j * j0) = cast(i, cast(i, j) * cast(i, j0)) | A User Theorem |
| cast-law-mult-one | 0 < i ⊦ cast(i, j * j0) = cast(i, cast(i, j) * j0) | A User Theorem |
| cast-law-mult-pos | ⊦ 0 ≤ j ∧ 0 < i → cast(i, j * j0) = cast(i, cast(i, j) * j0) | A User Theorem |
| cast-law-neg | 0 < i ⊦ cast(i, ~ j) = cast(i, ~ cast(i, j)) | A User Theorem |
| cast-law-neg-pos | ⊦ 0 ≤ j ∧ 0 < i → cast(i, ~ j) = cast(i, ~ cast(i, j)) | A User Theorem |
| cast-law-or-one | 0 < i ⊦ cast(i, bor(j, j0)) = cast(i, bor(cast(i, j), j0)) | A User Theorem |
| cast-law-shift-snd-l | 5 ≤ i ⊦ j0 i<< j = j0 i<< cast(i, j) | A User Theorem |
| cast-law-shift-snd-r | 5 ≤ i ⊦ j0 i>> j = j0 i>> cast(i, j) | A User Theorem |
| cast-law-shift-snd-zr | 5 ≤ i ⊦ j0 i>>> j = j0 i>>> cast(i, j) | A User Theorem |
| cast-law-sub | 0 < i ⊦ cast(i, j - j0) = cast(i, cast(i, j) - cast(i, j0)) | A User Theorem |
| cast-law-sub-one | 0 < i ⊦ cast(i, j - j0) = cast(i, cast(i, j) - j0) | A User Theorem |
| cast-law-sub-one-01 | 0 < i ⊦ cast(i, j - j0) = cast(i, j - cast(i, j0)) | A User Theorem |
| cast-law-xor-one | 0 < i ⊦ cast(i, bxor(j, j0)) = cast(i, bxor(cast(i, j), j0)) | A User Theorem |
| cast-length | ⊦ 0 < i → # int2bits(cast(i, j)) ≤ i→n(i) | A User Theorem |
| cast-max | ⊦ 0 < i → cast(i, j) < 2 ^ (i - 1) | A User Theorem |
| cast-min | ⊦ 0 < i → ~(2 ^ (i - 1)) ≤ cast(i, j) | A User Theorem |
| cast-mod-in | 0 < i, ~(2 ^ (i - 1)) ≤ j, j < 2 ^ (i - 1) ⊦ cast(i, j) = j | A User Theorem |
| cast-mod-ls | 0 < i, abs(j) < 2 ^ (i - 1) ⊦ cast(i, j) = j | A User Theorem |
| cast-mod-ls-most | 0 < i, j = ~(2 ^ (i - 1)) ⊦ cast(i, j) = j | A User Theorem |
| cast-mod-ls-neg | 0 < i, j < 0, abs(j) < 2 ^ (i - 1) ⊦ cast(i, j) = j | A User Theorem |
| cast-mod-ls-pos | 0 < i, 0 ≤ j, j < 2 ^ (i - 1) ⊦ cast(i, j) = j | A User Theorem |
| cast-mod-neg-high | j < 0, ~(2 ^ (i - 1)) ≤ j % 2 ^ i, 0 < i ⊦ cast(i, j) = j % 2 ^ i | A User Theorem |
| cast-mod-neg-low | j < 0, j % 2 ^ i < ~(2 ^ (i - 1)), 0 < i ⊦ cast(i, j) = j % 2 ^ i + 2 ^ i | A User Theorem |
| cast-mod-pos-high | 0 ≤ j, 2 ^ (i - 1) - 1 < j % 2 ^ i, 0 < i ⊦ cast(i, j) = j % 2 ^ i - 2 ^ i | A User Theorem |
| cast-mod-pos-low | 0 ≤ j, j % 2 ^ i ≤ 2 ^ (i - 1) - 1, 0 < i ⊦ cast(i, j) = j % 2 ^ i | A User Theorem |
| cast-mult-2pot | ⊦ 0 < i → cast(i, j * 2 ^ i) = 0 | A User Theorem |
| cast-mult-add | ⊦ 0 < i → cast(i, j * 2 ^ i + j0) = cast(i, j0) | A User Theorem |
| cast-mult-add-h | ⊦ j < 0 ∧ 0 ≤ j0 ∧ j0 < 2 ^ i ∧ 0 < i → cast(i, j * 2 ^ i + j0) = cast(i, j0) | A User Theorem |
| cast-mult-add-h-01 | ⊦ 0 ≤ j ∧ j0 < 0 ∧ abs(j0) < 2 ^ i ∧ 0 < i → cast(i, j * 2 ^ i + j0) = cast(i, j0) | A User Theorem |
| cast-mult-neg | ⊦ j < 0 ∧ j0 < 0 ∧ 0 < i → cast(i, j * 2 ^ i + j0) = cast(i, j0) | A User Theorem |
| cast-mult-neg-01 | ⊦ 0 < i → cast(i, ~(j * 2 ^ i)) = 0 | A User Theorem |
| cast-mult-neg-02 | ⊦ 0 < i → cast(i, ~(j * 2 ^ i + j0)) = cast(i, ~ j0) | A User Theorem |
| cast-mult-pos | ⊦ 0 ≤ j ∧ 0 ≤ j0 ∧ 0 < i → cast(i, j * 2 ^ i + j0) = cast(i, j0) | A User Theorem |
| cast-neg-add | ⊦ 0 < i → cast(i, cast(i, ~ j) + j0) = cast(i, ~ j + j0) | A User Theorem |
| cast-neg-add-01 | ⊦ 0 < i → cast(i, cast(i, ~ j) + j0) = cast(i, ~ cast(i, j) + j0) | A User Theorem |
| cast-nls | ⊦ j0 ≤ ~(2 ^ (i - 1)) ∧ 0 < i → ¬ cast(i, j) < j0 | A User Theorem |
| cast-nls-01 | ⊦ 2 ^ (i - 1) - 1 ≤ j0 ∧ 0 < i → ¬ j0 < cast(i, j) | A User Theorem |
| cast-one | ⊦ cast(1, j) ≠ 0 → cast(1, j) = ~1 | A User Theorem |
| cast-size-fits | ⊦ n→i(# int2bits(j)) ≤ i → cast(i, j) = j | A User Theorem |
| cast-size-fits-01 | 0 < i ⊦ ~(2 ^ (i - 1)) ≤ j ∧ j < 2 ^ (i - 1) → cast(i, j) = j | A User Theorem |
| cast-sub-2pot | ⊦ 0 < i → cast(i, 2 ^ i - j0) = cast(i, ~ j0) | A User Theorem |
| cast-zero | ⊦ 0 < i → cast(i, 0) = 0 | A User Theorem |
| compl-def | ⊦ bcompl(i) = ~ i - 1 | A User Theorem |
| compl-zero | ⊦ bcompl(0) = ~ 1 | A User Theorem |
| divide-by-10 | ⊦ 0 ≤ i ∧ i ≤ 2 ^ 16 → i * 52429 i>>> (16 + 3) = i / 10 | A User Theorem |
| intshiftleft-band31 | ⊦ i i<< j = i i<< band(j, 31) | A User Theorem |
| intshiftleft-is-mult | ⊦ 0 ≤ j ∧ j < 32 → i i<< j = i * 2 ^ j | A User Theorem |
| intshiftleft-is-mult-01 | ⊦ i i<< j = i * 2 ^ band(j, 31) | A User Theorem |
| intshiftleft-is-shiftleft | ⊦ i i<< j = i << band(j, 31) | A User Theorem |
| intshiftleft-num | ⊦ (* i) i<< (* j) = bits2int(int2bits(i) + mklist(false, i→n(band(j, 31)))) | A User Theorem |
| intshiftright-def-unbounded | ⊦ j i>> i = j >> band(i, 31) | A User Theorem |
| intshiftright-ls | ⊦ i i>> 8 < 0 ↔ i < 0 | A User Theorem |
| intshiftright-ls-01 | ⊦ 0 ≤ j ∧ j < 32 → (i i>> j < 0 ↔ i < 0) | A User Theorem |
| intshiftright-ls-02 | ⊦ i < 0 → ¬ 0 < i i>> j | A User Theorem |
| intshiftright-mone | ⊦ ~1 i>> 16 = ~1 | A User Theorem |
| intshiftright-unbounded-same | ⊦ 0 ≤ i ∧ i < 32 → j i>> i = j >> i | A User Theorem |
| intshiftrsign-2pot-neg | ⊦ i < 0 ∧ i % 2 ^ j = 0 ∧ 0 < j ∧ j < 32 → i i>> j = i / 2 ^ j | A User Theorem |
| intshiftrsign-2pot-neg-01 | ⊦ i < 0 ∧ 0 < j ∧ j < 32 → i i>> j = (i - (2 ^ j - 1)) / 2 ^ j | A User Theorem |
| intshiftrsign-2pot-neg-02 | ⊦ i < 0 ∧ i % 2 ^ j ≠ 0 ∧ 0 < j ∧ j < 32 → i i>> j = i / 2 ^ j - 1 | A User Theorem |
| intshiftrsign-2pot-pos | ⊦ 0 ≤ i ∧ 0 < j ∧ j < 32 → i i>> j = i / 2 ^ j | A User Theorem |
| intshiftrsign-abs-le | ⊦ abs(i i>> j) ≤ abs(i) | A User Theorem |
| intshiftrsign-band31 | ⊦ i i>> j = i i>> band(j, 31) | A User Theorem |
| intshiftrsign-if | ⊦ i i>> j = (# int2bits(i) ≤ i→n(band(j, 31)) ⊃ (i < 0 ⊃ ~1;0);bits2int(sublist(0, # int2bits(i) - i→n(band(j, 31)), int2bits(i)))) | A User Theorem |
| intshiftrsign-neg-01 | ⊦ i < 0 ∧ i % 256 = 0 → i i>> 8 = i / 256 | A User Theorem |
| intshiftrsign-neg-02 | ⊦ i < 0 ∧ i % 256 ≠ 0 → i i>> 8 = i / 256 - 1 | A User Theorem |
| intshiftrsign-num | ⊦ (* i) i>> (* j) = (# int2bits(i) ≤ i→n(band(j, 31)) ⊃ (i < 0 ⊃ ~1;0);bits2int(sublist(0, # int2bits(i) - i→n(band(j, 31)), int2bits(i)))) | A User Theorem |
| intshiftrsign-pos-8 | ⊦ 0 ≤ i → i i>> 8 = i / 256 | A User Theorem |
| intshiftrsign-pos-num | 0 ≤ i, i < 2147483648, 0 < j, j < 16 ⊦ (* i) i>> (* j) = i / 2 ^ j | A User Theorem |
| intshiftrsign-rec-neg | ⊦ i < 0 ∧ 0 < j ∧ j < 32 → i i>> j = (i - 1) / 2 i>> (j - 1) | A User Theorem |
| intshiftrsign-rec-pos | ⊦ 0 ≤ i ∧ 0 < j ∧ j < 32 → i i>> j = i / 2 i>> (j - 1) | A User Theorem |
| intshiftrsign-zero | ⊦ i i>> 0 = i | A User Theorem |
| intshiftrsign-zero-01 | ⊦ 0 i>> j = 0 | A User Theorem |
| intshiftrsign32 | ⊦ # int2bits(i) ≤ 32 → i i>> j = bits2int(sublist(0, 32, mklist(int2bits(i).first, i→n(band(j, 31))) + fillsgn(32, int2bits(i)))) | A User Theorem |
| intshiftrzero-prop-01 | i < 0, ~(2 ^ 31) ≤ i, band(j, 31) ≠ 0 ⊦ i i>>> j = (i i>> j) + (2 i<< bcompl(j)) | A User Theorem |
| intshiftzero-def-unbounded | ⊦ j i>>> i = >>>(32, j, band(i, 31)) | A User Theorem |
| intshiftzero-mone | ⊦ ~1 i>>> 16 = 65535 | A User Theorem |
| longshiftright-2pot-pos | ⊦ 0 ≤ i ∧ 0 < j ∧ j < 64 → i l>> j = i / 2 ^ j | A User Theorem |
| longshiftright-def-unbounded | ⊦ j l>> i = j >> band(i, 63) | A User Theorem |
| longshiftzero-band-63 | ⊦ i l>>> j = i l>>> band(j, 63) | A User Theorem |
| longshiftzero-carry | ⊦ 0 ≤ i ∧ i ≤ 1 → ¬ (i + band(4294967295, j) + band(4294967295, j0)) l>>> 32 < 0 | A User Theorem |
| longshiftzero-carry-01 | ⊦ 0 ≤ i ∧ i ≤ 1 → ¬ 1 < (i + band(4294967295, j) + band(4294967295, j0)) l>>> 32 | A User Theorem |
| longshiftzero-def-pos | ⊦ 0 ≤ i → i l>>> j = i >> band(j, 63) | A User Theorem |
| longshiftzero-def-unbounded | ⊦ j l>>> i = >>>(64, j, band(i, 63)) | A User Theorem |
| longshiftzero-not-neg | ⊦ 0 ≤ i → ¬ i l>>> j < 0 | A User Theorem |
| longshiftzero-not-neg-01 | ⊦ 0 ≤ i ∨ band(j, 63) ≠ 0 → ¬ i l>>> j < 0 | A User Theorem |
| longshiftzero-pos | ⊦ 0 ≤ i → i l>>> j = i l>> j | A User Theorem |
| longshiftzero-zero | ⊦ 0 l>>> j = 0 | A User Theorem |
| longshiftzero-zero-01 | ⊦ band(j, 63) = 0 → i l>>> j = i | A User Theorem |
| longshiftzero-zero-02 | ⊦ i l>>> 0 = i | A User Theorem |
| longshiftzero-zero-03 | ⊦ 0 ≤ i → (i l>>> j = 0 ↔ i / 2 ^ band(j, 63) = 0) | A User Theorem |
| or-invandinv | ⊦ bits ≠ [] ∧ bits0 ≠ [] → bitsor(bits, bits0) = bitsinvert(bitsand(bitsinvert(bits), bitsinvert(bits0))) | A User Theorem |
| or-last | ⊦ bits ≠ [] ∧ bits0 ≠ [] → bitsor(bits + boolvar ', bits0 + boolvar0 ') = bitsor(bits, bits0) + (boolvar ∨ boolvar0)' | A User Theorem |
| or-rec | ⊦ 1 < # bits ∧ 1 < # bits0 → bitsor(bits, bits0) = bitsor(bits.butlast, bits0.butlast) + (bits.last ∨ bits0.last) | A User Theorem |
| or-rec-01 | ⊦ bits ≠ [] ∧ bits0 = true ' → bitsor(bits, bits0) = true ' | A User Theorem |
| or-rec-02 | ⊦ bits ≠ [] ∧ bits0 = false ' → bitsor(bits, bits0) = bits | A User Theorem |
| or-rec-03 | ⊦ bits0 ≠ [] ∧ bits = true ' → bitsor(bits, bits0) = true ' | A User Theorem |
| or-rec-04 | ⊦ bits0 ≠ [] ∧ bits = false ' → bitsor(bits, bits0) = bits0 | A User Theorem |
| or-rec-05 | ⊦ bitsor(bits + boolvar ' + true ', bits0 + boolvar1 ' + true ') = bitsor(bits + boolvar, bits0 + boolvar1) + true ' | A User Theorem |
| or-rec-06 | ⊦ bitsor(bits + boolvar ' + false ', bits0 + boolvar1 ' + true ') = bitsor(bits + boolvar, bits0 + boolvar1) + true ' | A User Theorem |
| or-rec-07 | ⊦ bitsor(bits + boolvar ' + true ', bits0 + boolvar1 ' + false ') = bitsor(bits + boolvar, bits0 + boolvar1) + true ' | A User Theorem |
| or-rec-08 | ⊦ bitsor(bits + boolvar ' + false ', bits0 + boolvar1 ' + false ') = bitsor(bits + boolvar, bits0 + boolvar1) + false ' | A User Theorem |
| or-two | ⊦ bitsor(boolvar ' + boolvar0 ', boolvar1 ' + boolvar2 ') = bitsor(boolvar ', boolvar1 ') + (boolvar0 ∨ boolvar2) | A User Theorem |
| or-two-01 | ⊦ bitsor(boolvar ' + true ', bits0 + boolvar1 ' + true ') = bitsor(boolvar ', bits0 + boolvar1) + true ' | A User Theorem |
| or-two-02 | ⊦ bitsor(boolvar ' + false ', bits0 + boolvar1 ' + true ') = bitsor(boolvar ', bits0 + boolvar1) + true ' | A User Theorem |
| or-two-03 | ⊦ bitsor(boolvar ' + true ', bits0 + boolvar1 ' + false ') = bitsor(boolvar ', bits0 + boolvar1) + true ' | A User Theorem |
| or-two-04 | ⊦ bitsor(boolvar ' + false ', bits0 + boolvar1 ' + false ') = bitsor(boolvar ', bits0 + boolvar1) + false ' | A User Theorem |
| or-two-05 | ⊦ bitsor(bits + boolvar ' + true ', boolvar1 ' + true ') = bitsor(bits + boolvar, boolvar1 ') + true ' | A User Theorem |
| or-two-06 | ⊦ bitsor(bits + boolvar ' + false ', boolvar1 ' + true ') = bitsor(bits + boolvar, boolvar1 ') + true ' | A User Theorem |
| or-two-07 | ⊦ bitsor(bits + boolvar ' + true ', boolvar1 ' + false ') = bitsor(bits + boolvar, boolvar1 ') + true ' | A User Theorem |
| or-two-08 | ⊦ bitsor(bits + boolvar ' + false ', boolvar1 ' + false ') = bitsor(bits + boolvar, boolvar1 ') + false ' | A User Theorem |
| rightshift-zero | ⊦ i >> 0 = i | A User Theorem |
| shiftright-abs | ⊦ i >> j = i >> abs(j) | A User Theorem |
| shiftright-is-le | ⊦ i >> j ≤ abs(i) | A User Theorem |
| shiftright-minus-one | ⊦ ~1 >> j = ~1 | A User Theorem |
| shiftright-neg-div | ⊦ i < ~(2 ^ (abs(j) - 1)) ∧ j ≠ 0 → i >> j = (i - (2 ^ abs(j) - 1)) / 2 ^ abs(j) | A User Theorem |
| shiftright-neg-div-01 | ⊦ i % 2 ^ abs(j) = 0 ∧ i < ~(2 ^ (abs(j) - 1)) ∧ j ≠ 0 → i >> j = i / 2 ^ abs(j) | A User Theorem |
| shiftright-neg-div-02 | ⊦ i % 2 ^ abs(j) ≠ 0 ∧ i < ~(2 ^ (abs(j) - 1)) ∧ j ≠ 0 → i >> j = i / 2 ^ abs(j) - 1 | A User Theorem |
| shiftright-neg-mone | ⊦ ~(2 ^ (abs(j) - 1)) ≤ i ∧ i < 0 → i >> j = ~1 | A User Theorem |
| shiftright-not-le | ⊦ 0 ≤ i → (i ≤ i >> j ↔ i = 0 ∨ j = 0) | A User Theorem |
| shiftright-not-ls | ⊦ ¬ abs(i) < i >> j | A User Theorem |
| shiftright-not-ls-01 | ⊦ 0 ≤ i → ¬ i < i >> j | A User Theorem |
| shiftright-not-neg | ⊦ 0 ≤ i → ¬ i >> j < 0 | A User Theorem |
| shiftright-not-pos | ⊦ i < 0 → ¬ 0 < i >> j | A User Theorem |
| shiftright-not-pos-01 | ⊦ i < 0 → ¬ 0 ≤ i >> j | A User Theorem |
| shiftright-pos-div | ⊦ 0 ≤ i ∧ 0 ≤ j → i >> j = i / 2 ^ j | A User Theorem |
| shiftright-pos-div-01 | ⊦ 0 ≤ i → i >> j = i / 2 ^ abs(j) | A User Theorem |
| shiftright-rec-8 | ⊦ 0 ≤ i ∧ 8 ≤ j → i >> j = i / 256 >> (j - 8) | A User Theorem |
| shiftright-rec-8-neg | ⊦ i < 0 ∧ 8 ≤ j → i >> j = (i - 255) / 256 >> (j - 8) | A User Theorem |
| shiftright-rec-neg | ⊦ i < 0 ∧ j ≠ 0 → i >> j = (i - 1) / 2 >> (abs(j) - 1) | A User Theorem |
| shiftright-rec-pos | ⊦ 0 ≤ i ∧ 0 < j → i >> j = i / 2 >> (j - 1) | A User Theorem |
| shiftright-rec-pos-01 | ⊦ 0 ≤ i ∧ j ≠ 0 → i >> j = i / 2 >> (abs(j) - 1) | A User Theorem |
| shiftright-shift | ⊦ 0 ≤ j ∧ 0 ≤ j0 ∧ j + j0 < 32 → (i >> j) >> j0 = i >> (j + j0) | A User Theorem |
| shiftright-zero | ⊦ 0 >> j = 0 | A User Theorem |
| shiftzero-by-one | ⊦ i < ~1 ∧ n ≠ 0 → >>>(n, i, 1) = bits2uint(fillsgn(n -1, int2bits((i - 1) / 2))) | A User Theorem |
| shiftzero-by-one-01 | ⊦ i < ~1 ∧ n ≠ 0 → >>>(n, i, 1) = 2 ^ n→i((# fillsgn(n, int2bits(i)))-1) + (i - 1) / 2 | A User Theorem |
| shiftzero-max-neg | ⊦ i < 0 ∧ # int2bits(i) ≤ n ∧ 0 < j ∧ n ≠ 0 → >>>(n, i, j) < 2 ^ (n→i(n) - 1) | A User Theorem |
| shiftzero-max-neg-01 | ⊦ i < 0 ∧ # int2bits(i) ≤ n ∧ j ≤ n→i(n) ∧ 0 < j ∧ n ≠ 0 → >>>(n, i, j) < 2 ^ (n→i(n) - j) | A User Theorem |
| shiftzero-minus-one | ⊦ j ≠ 0 ∧ n ≠ 0 → >>>(n, ~1, j) = (2 ^ n→i(n) - 1) >> j | A User Theorem |
| shiftzero-not-neg | ⊦ 0 ≤ i ∨ j ≠ 0 → ¬ >>>(n, i, j) < 0 | A User Theorem |
| shiftzero-pos | ⊦ 0 ≤ i → >>>(n, i, j) = i >> j | A User Theorem |
| shiftzero-rec-neg-longer | ⊦ i < ~1 ∧ n < # int2bits(i) ∧ 1 < j → >>>(n, i, j) = >>>(n, (i - 1) / 2, j - 1) | A User Theorem |
| shiftzero-rec-neg-shorter | ⊦ i < ~1 ∧ # int2bits(i) ≤ n ∧ 1 < j → >>>(n, i, j) = >>>(n -1, (i - 1) / 2, j - 1) | A User Theorem |
| shiftzero-zero | ⊦ >>>(n, i, 0) = i | A User Theorem |
| shiftzero-zero-size | ⊦ j ≠ 0 → >>>(0, i, j) = bits2uint(int2bits(i)) >> j | A User Theorem |
| shiftzero-zero-size-01 | ⊦ i < 0 ∧ j ≠ 0 → >>>(0, i, j) = (2 ^ n→i(# int2bits(i)) + i) >> j | A User Theorem |