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: |
|---|---|---|
| int2bits-pos | ⊦ 0 ≤ i → int2bits(i) = uint2bits(i) | An Axiom |
| int2bits-neg | ⊦ i < 0 → int2bits(i) = sgn(bitsinvert(uint2bits(abs(i))) +1) | An Axiom |
| uint2bits-zero | ⊦ uint2bits(0) = false ' | An Axiom |
| uint2bits-one | ⊦ uint2bits(1) = false + true | An Axiom |
| uint2bits-rec | ⊦ 1 < i → uint2bits(i) = uint2bits(i / 2) + (i % 2 = 1) | An Axiom |
| bits2int-pos | ⊦ bits2int(false ' + bits) = bits2uint(bits) | An Axiom |
| bits2int-neg | ⊦ bits2int(true ' + bits) = ~ bits2uint(bitsinvert(true + bits) +1) | An Axiom |
| bits2uint-base | ⊦ bits2uint([]) = 0 | An Axiom |
| bits2uint-zero | ⊦ bits2uint(bits + false ') = bits2uint(bits) * 2 | An Axiom |
| bits2uint-one | ⊦ bits2uint(bits + true ') = bits2uint(bits) * 2 + 1 | An Axiom |
| bits2int-base | ⊦ bits2int([]) = 0 | An Axiom |
| bits2bits-2pot | ⊦ ¬ true ∈ bits → int2bits(bits2int(true ' + bits)) = true ' + bits | A User Theorem |
| bits2bits-2pot-01 | ⊦ int2bits(bits2int(true ' + mklist(false, n))) = true ' + mklist(false, n) | A User Theorem |
| bits2bits-def | bits ≠ [] ⊦ int2bits(bits2int(bits)) = sgn(bits) | A User Theorem |
| bits2bits-invert | ⊦ bits ≠ [] → bits2int(bitsinvert(int2bits(bits2int(bits)))) = bits2int(bitsinvert(bits)) | A User Theorem |
| bits2bits-mone | ⊦ ¬ false ∈ bits ∧ bits ≠ [] → int2bits(bits2int(bits)) = true ' | A User Theorem |
| bits2bits-zeros | ⊦ ¬ true ∈ bits ∧ bits ≠ [] → int2bits(bits2int(bits)) = false ' | A User Theorem |
| bits2int-011x | ⊦ ¬ false ∈ bits → bits2int(false ' + bits) = 2 ^ n→i(# bits) - 1 | A User Theorem |
| bits2int-2pot | ⊦ ¬ true ∈ bits → bits2int(true ' + bits) = ~(2 ^ n→i(# bits)) | A User Theorem |
| bits2int-fill | ⊦ bits ≠ [] → bits2int(fillsgn(n, bits)) = bits2int(bits) | A User Theorem |
| bits2int-first | bits ≠ [] ⊦ 0 ≤ bits2int(bits) → ¬ bits.first | A User Theorem |
| bits2int-first-01 | bits ≠ [] ⊦ bits2int(bits) < 0 → bits.first | A User Theorem |
| bits2int-ge-zero | ⊦ bits ≠ [] → (0 ≤ bits2int(bits) ↔ ¬ bits.first) | A User Theorem |
| bits2int-inj | ⊦ bits ≠ [] ∧ bits0 ≠ [] → (bits2int(bits) = bits2int(bits0) ↔ sgn(bits) = sgn(bits0)) | A User Theorem |
| bits2int-inv | ⊦ bits ≠ [] → bits2int(bitsinvert(bits)) = ~ bits2int(bits) - 1 | A User Theorem |
| bits2int-lasteq | ⊦ bits ≠ [] ∧ bits0 ≠ [] → (bits2int(bits + boolvar ') = bits2int(bits0 + boolvar ') ↔ bits2int(bits) = bits2int(bits0)) | A User Theorem |
| bits2int-le8 | ⊦ # bits ≤ 8 ∧ bits ≠ [] → ¬ bits2int(bits) < ~128 | A User Theorem |
| bits2int-le8-01 | ⊦ # bits ≤ 8 ∧ bits ≠ [] → ¬ 127 < bits2int(bits) | A User Theorem |
| bits2int-lez | ⊦ bits ≠ [] → (bits2int(bits) < 0 ↔ bits.first) | A User Theorem |
| bits2int-mklist | ⊦ bits ≠ [] ∧ (bits.first ↔ boolvar) → bits2int(mklist(boolvar, n) + bits) = bits2int(bits) | A User Theorem |
| bits2int-mklist-01 | ⊦ bits2int(boolvar ' + mklist(boolvar, n) + bits) = bits2int(boolvar ' + bits) | A User Theorem |
| bits2int-mklist-02 | ⊦ bits2int(boolvar ' + mklist(boolvar, n)) = bits2int(boolvar ') | A User Theorem |
| bits2int-mklist-03 | ⊦ bits2int(mklist(true, # int2bits(i))) = ~1 | A User Theorem |
| bits2int-mklist-04 | ⊦ bits2int(mklist(false, # int2bits(i))) = 0 | A User Theorem |
| bits2int-mklist-05 | ⊦ n ≠ 0 → bits2int(mklist(boolvar, n) + bits) = bits2int(boolvar ' + bits) | A User Theorem |
| bits2int-mklist-06 | ⊦ n ≠ 0 → bits2int(mklist(boolvar, n)) = bits2int(boolvar ') | A User Theorem |
| bits2int-neg-01 | ⊦ bits.first ∧ bits ≠ [] → bits2int(bits) = ~ bits2uint(bitsinvert(true + bits.rest) +1) | A User Theorem |
| bits2int-neg-02 | ⊦ bits ≠ [] ∧ bits.first → bits2uint(bitsinvert(bits) +1) = ~ bits2int(bits) | A User Theorem |
| bits2int-neg-03 | ⊦ bits.first ∧ bits ≠ [] → bits2int(bits) = ~ bits2uint(bitsinvert(bits) +1) | A User Theorem |
| bits2int-neg-1bit | ⊦ i < 0 → bits2int(true ' + int2bits(i)) = i | A User Theorem |
| bits2int-neg-1bit-01 | ⊦ bits.first ∧ bits ≠ [] → bits2int(true ' + bits) = bits2int(bits) | A User Theorem |
| bits2int-nle | ⊦ # bits ≤ n ∧ bits ≠ [] → ¬ 2 ^ n→i(n) + bits2int(bits) ≤ 0 | A User Theorem |
| bits2int-nls | ⊦ bits ≠ [] → ¬ 2 ^ n→i(# bits) + bits2int(bits) < 0 | A User Theorem |
| bits2int-nls-01 | ⊦ # bits ≤ n ∧ bits ≠ [] → ¬ 2 ^ n→i(n) + bits2int(bits) < 0 | A User Theorem |
| bits2int-nls-02 | ⊦ # bits - 1 ≤ n ∧ bits ≠ [] → ¬ 2 ^ n→i(n) + bits2int(bits) < 0 | A User Theorem |
| bits2int-one | ⊦ bits2int(true ') = ~1 | A User Theorem |
| bits2int-one-01 | ⊦ (boolvar ↔ true) → bits2int(boolvar ') = ~1 | A User Theorem |
| bits2int-ones | ⊦ ¬ false ∈ bits ∧ bits ≠ [] → bits2int(bits) = ~1 | A User Theorem |
| bits2int-ones-01 | ⊦ ¬ false ∈ bits → bits2int(bits + true ' + bits0) = bits2int(true ' + bits0) | A User Theorem |
| bits2int-ones-02 | ⊦ ¬ false ∈ bits ∧ bits ≠ [] → bits2int(bits + bits0) = bits2int(true ' + bits0) | A User Theorem |
| bits2int-pos-01 | ⊦ ¬ bits.first ∧ bits ≠ [] → bits2int(bits) = bits2uint(bits.rest) | A User Theorem |
| bits2int-pos-02 | ⊦ ¬ bits.first ∧ bits ≠ [] → bits2int(bits) = bits2uint(bits) | A User Theorem |
| bits2int-range | bits ≠ [] ⊦ ~(2 ^ n→i(# bits - 1)) ≤ bits2int(bits) ∧ bits2int(bits) < 2 ^ n→i(# bits - 1) | A User Theorem |
| bits2int-rec | ⊦ boolvar ∧ ¬ bits.first ∧ bits ≠ [] → bits2int(bits + boolvar ') = bits2int(bits) * 2 + 1 | A User Theorem |
| bits2int-rec-01 | ⊦ boolvar ∧ bits.first ∧ bits ≠ [] → bits2int(bits + boolvar ') = ~(bits2uint(bitsinvert(bits.rest)) * 2 + 1) | A User Theorem |
| bits2int-rec-03 | ⊦ boolvar ∧ bits.first ∧ false ∈ bits → bits2int(bits + boolvar ') = bits2int(bits) * 2 + 1 | A User Theorem |
| bits2int-rec-04 | ⊦ boolvar ∧ bits.first ∧ bits ≠ [] → bits2int(bits + boolvar ') = bits2int(bits) * 2 + 1 | A User Theorem |
| bits2int-rec-false | ⊦ ¬ boolvar ∧ bits ≠ [] → bits2int(bits + boolvar ') = bits2int(bits) * 2 | A User Theorem |
| bits2int-rec-true | ⊦ boolvar ∧ bits ≠ [] → bits2int(bits + boolvar ') = bits2int(bits) * 2 + 1 | A User Theorem |
| bits2int-sgn | ⊦ bits2int(sgn(bits)) = bits2int(bits) | A User Theorem |
| bits2int-sgn-intro | ⊦ bits2int(bits) = bits2int(sgn(bits)) | A User Theorem |
| bits2int-sign | bits ≠ [], ¬ (¬ bits.first) ∈ bits0 ⊦ bits2int(bits0 + bits) = bits2int(bits) | A User Theorem |
| bits2int-split | ⊦ # bits0 ≠ 0 ∧ # bits ≠ 0 ∧ ¬ bits.first → bits2int(bits + bits0) = bits2uint(bits) * 2 ^ n→i(# bits0) + bits2uint(bits0) | A User Theorem |
| bits2int-split-01 | ⊦ # bits0 ≠ 0 ∧ # bits ≠ 0 ∧ bits.first → bits2int(bits + bits0) = ~(2 ^ n→i(# bits0) * bits2uint(bitsinvert(bits))) - bits2uint(bitsinvert(bits0)) + 1 | A User Theorem |
| bits2int-zero | ⊦ bits2int(false ') = 0 | A User Theorem |
| bits2int-zero-01 | ⊦ ¬ true ∈ bits ∧ bits ≠ [] → bits2int(bits) = 0 | A User Theorem |
| bits2int-zero-02 | ⊦ bits ≠ [] → (bits2int(bits) = 0 ↔ ¬ true ∈ bits) | A User Theorem |
| bits2int-zero-03 | ⊦ (boolvar ↔ false) → bits2int(boolvar ') = 0 | A User Theorem |
| bits2int-zeros | ⊦ n ≠ 0 → bits2int(mklist(false, n) + bits) = bits2int(false ' + bits) | A User Theorem |
| bits2int-zeros-01 | ⊦ ¬ true ∈ bits → bits2int(bits + false ' + bits0) = bits2int(false + bits0) | A User Theorem |
| bits2int-zeros-02 | ⊦ bits2int(false ' + false ' + bits) = bits2int(false ' + bits) | A User Theorem |
| bits2int-zeros-03 | ⊦ m ≠ 0 → bits2int(mklist(false, m)) = 0 | A User Theorem |
| bits2int16 | ⊦ # bits = 16 → ¬ bits2int(bits) < ~32768 | A User Theorem |
| bits2int16-01 | ⊦ # bits = 16 → ¬ 32767 < bits2int(bits) | A User Theorem |
| bits2int16-02 | ⊦ 16 < # bits → ¬ bits2int(lastn(16, bits)) < ~32768 | A User Theorem |
| bits2int16-03 | ⊦ 16 < # bits → ¬ 32767 < bits2int(lastn(16, bits)) | A User Theorem |
| bits2int8 | ⊦ # bits = 8 → ¬ bits2int(bits) < ~128 | A User Theorem |
| bits2int8-01 | ⊦ # bits = 8 → ¬ 127 < bits2int(bits) | A User Theorem |
| bits2int8-02 | ⊦ 8 < # bits → ¬ bits2int(lastn(8, bits)) < ~128 | A User Theorem |
| bits2int8-03 | ⊦ 8 < # bits → ¬ 127 < bits2int(lastn(8, bits)) | A User Theorem |
| bits2ubits | ⊦ bits ≠ [] ∧ bits.first → bits2int(bits) = bits2uint(bits) - 2 ^ n→i(# bits) | A User Theorem |
| bits2uint-2pot | ⊦ ¬ true ∈ bits → bits2uint(true ' + bits) = 2 ^ n→i(# bits) | A User Theorem |
| bits2uint-2pot-01 | ⊦ ¬ true ∈ bits → bits2uint(false ' + true ' + bits) = 2 ^ n→i(# bits) | A User Theorem |
| bits2uint-2pot-02 | ⊦ bits2uint(true ' + mklist(false, n)) = 2 ^ n→i(n) | A User Theorem |
| bits2uint-inv-neg | ⊦ bits ≠ [] ∧ ¬ bits.first → bits2uint(bitsinvert(bits)) = 2 ^ n→i(# bits) + ~ bits2int(bits) - 1 | A User Theorem |
| bits2uint-inv-pos | ⊦ bits ≠ [] ∧ bits.first → bits2uint(bitsinvert(bits)) = ~ bits2int(bits) - 1 | A User Theorem |
| bits2uint-ls | ⊦ # bits ≤ n → bits2uint(bits) < 2 ^ n→i(n) | A User Theorem |
| bits2uint-mklist | ⊦ bits2uint(mklist(false, n) + bits) = bits2uint(bits) | A User Theorem |
| bits2uint-mone | ⊦ bits2uint(bits) ≠ ~1 | A User Theorem |
| bits2uint-nle | ⊦ ¬ 2 ^ n→i(# bits) ≤ bits2uint(bits) | A User Theorem |
| bits2uint-nle-01 | ⊦ # bits ≤ n → ¬ 2 ^ n→i(n) ≤ bits2uint(bits) | A User Theorem |
| bits2uint-not-neg | ⊦ bits2uint(bits) ≤ 0 ↔ bits2uint(bits) = 0 | A User Theorem |
| bits2uint-not-neg-01 | ⊦ ¬ bits2uint(bits) < 0 | A User Theorem |
| bits2uint-not-zero | ⊦ true ∈ bits → bits2uint(bits) ≠ 0 | A User Theorem |
| bits2uint-not-zero-01 | ⊦ bits2uint(true ' + bits) ≠ 0 | A User Theorem |
| bits2uint-one-01 | ⊦ boolvar → bits2uint(boolvar ') = 1 | A User Theorem |
| bits2uint-one-02 | ⊦ bits2uint(false ') = 0 | A User Theorem |
| bits2uint-one-03 | ⊦ bits2uint(true ') = 1 | A User Theorem |
| bits2uint-ones | ⊦ ¬ false ∈ bits ∧ bits ≠ [] → bits2uint(bits) = 2 ^ n→i(# bits) - 1 | A User Theorem |
| bits2uint-rec | ⊦ bits ≠ [] ∧ bits.last → bits2uint(bits) = bits2uint(bits.butlast) * 2 + 1 | A User Theorem |
| bits2uint-rec-01 | ⊦ bits ≠ [] ∧ ¬ bits.last → bits2uint(bits) = bits2uint(bits.butlast) * 2 | A User Theorem |
| bits2uint-rec-02 | ⊦ boolvar → bits2uint(bits + boolvar ') = bits2uint(bits) * 2 + 1 | A User Theorem |
| bits2uint-split | ⊦ # bits0 ≠ 0 → bits2uint(bits + bits0) = bits2uint(bits) * 2 ^ n→i(# bits0) + bits2uint(bits0) | A User Theorem |
| bits2uint-succ | ⊦ bits ≠ [] → bits2uint(bits +1) = bits2uint(bits) + 1 | A User Theorem |
| bits2uint-zero-01 | ⊦ bits2uint(fillsgn(n, int2bits(i))) = 0 ↔ i = 0 | A User Theorem |
| bits2uint-zeros | ⊦ ¬ true ∈ bits → bits2uint(bits) = 0 | A User Theorem |
| bits2uint-zeros-01 | ⊦ ¬ false ∈ bits → bits2uint(bitsinvert(bits)) = 0 | A User Theorem |
| bits2uint-zeros-02 | ⊦ ¬ true ∈ bits → bits2uint(bits + bits0) = bits2uint(bits0) | A User Theorem |
| bits2uint-zeros-03 | ⊦ bits2uint(false ' + bits) = bits2uint(bits) | A User Theorem |
| bits2uint-zeros-04 | ⊦ bits2uint(mklist(false, n)) = 0 | A User Theorem |
| int2bits-011x | ⊦ ¬ false ∈ int2bits(4294967295).rest | A User Theorem |
| int2bits-256-neg-mone | ⊦ 0 < j ∧ 0 < i → int2bits(j * 256 - 1) = int2bits(j - 1) + mklist(true, i→n(8)) | A User Theorem |
| int2bits-2pot | 0 ≤ i ⊦ int2bits(2 ^ i) = false ' + true ' + mklist(false, i→n(i)) | A User Theorem |
| int2bits-2pot-01 | 0 ≤ i ⊦ int2bits(~(2 ^ i)) = true ' + mklist(false, i→n(i)) | A User Theorem |
| int2bits-2pot-02 | 0 ≤ i ⊦ int2bits(2 ^ i - 1) = false ' + mklist(true, i→n(i)) | A User Theorem |
| int2bits-2pot-03 | 0 ≤ j, ¬ false ∈ int2bits(j).rest ⊦ j = 2 ^ n→i(# int2bits(j).rest) - 1 | A User Theorem |
| int2bits-2pot-04 | 0 ≤ i, j ≠ 0 ⊦ int2bits(j * 2 ^ i) = int2bits(j) + mklist(false, i→n(i)) | A User Theorem |
| int2bits-2pot-05 | ⊦ 0 ≠ j ∧ 0 ≤ i → int2bits(~(j * 2 ^ i)) = int2bits(~ j) + mklist(false, i→n(i)) | A User Theorem |
| int2bits-2pot-neg-mone | ⊦ 0 < j ∧ 0 < i → int2bits(j * 2 ^ i - 1) = int2bits(j - 1) + mklist(true, i→n(i)) | A User Theorem |
| int2bits-add-high | ⊦ j0 < 0 ∧ 0 < i ∧ 2 ^ (i - 1) < abs(j0) ∧ abs(j0) < 2 ^ i ∧ j < 0 → int2bits(j * 2 ^ i + j0) = int2bits(j - 1) + fillsgn(i→n(i), int2bits(j0).rest) | A User Theorem |
| int2bits-add-low | ⊦ j < 0 ∧ j0 < 0 ∧ abs(j0) < 2 ^ (i - 1) ∧ 0 < i → int2bits(j * 2 ^ i + j0) = int2bits(j - 1) + fillsgn(i→n(i), int2bits(j0)) | A User Theorem |
| int2bits-bits2unit | ⊦ i < 0 → int2bits(bits2uint(int2bits(i))) = false ' + int2bits(i) | A User Theorem |
| int2bits-bits2unit-01 | ⊦ i < 0 → int2bits(bits2uint(int2bits(i))) = sgn(false ' + int2bits(i)) | A User Theorem |
| int2bits-eq | ⊦ int2bits(j) = false ' ↔ j = 0 | A User Theorem |
| int2bits-exneg | i < ~ 1 ⊦ ∃ bits. int2bits(i) = true ' + false ' + bits | A User Theorem |
| int2bits-expos | 0 < i ⊦ ∃ bits. int2bits(i) = false ' + true ' + bits | A User Theorem |
| int2bits-falsein | ⊦ 1 < i → false ∈ bitsinvert(int2bits(i)) +1 | A User Theorem |
| int2bits-falsein-01 | ⊦ i < ~1 → false ∈ int2bits(i).rest | A User Theorem |
| int2bits-falsein-02 | ⊦ false ∈ int2bits(j).rest ↔ ¬(∃ i. j = 2 ^ i - 1) | A User Theorem |
| int2bits-falsein-03 | ⊦ ¬ false ∈ bits ∧ ¬(∃ i. j = 2 ^ i - 1) → int2bits(j) ≠ boolvar ' + bits | A User Theorem |
| int2bits-fill-rest | ⊦ j < 0 ∧ ~(2 ^ (i - 1)) < j ∧ 0 < i → fillsgn(i→n(i + 1), int2bits(j)).rest = fillsgn(i→n(i), int2bits(j)) | A User Theorem |
| int2bits-fillfirst | ⊦ fillsgn(n, int2bits(j)).first ↔ int2bits(j).first | A User Theorem |
| int2bits-fillsgn | ⊦ (boolvar ↔ i < 0) → mklist(boolvar, n) + int2bits(i) = fillsgn(n + # int2bits(i), int2bits(i)) | A User Theorem |
| int2bits-first | ⊦ j < 0 → int2bits(j) ≠ false ' + bits | A User Theorem |
| int2bits-first-01 | ⊦ j < 0 → int2bits(j).first | A User Theorem |
| int2bits-first-02 | ⊦ int2bits(j).first ↔ j < 0 | A User Theorem |
| int2bits-first-03 | ⊦ 0 < j → int2bits(j) ≠ true ' + bits | A User Theorem |
| int2bits-first-04 | ⊦ 0 ≤ j → int2bits(j) ≠ true ' + bits | A User Theorem |
| int2bits-first-05 | ⊦ int2bits(i) = boolvar ' + bits ∧ 0 ≤ i → ¬ boolvar | A User Theorem |
| int2bits-first-06 | ⊦ int2bits(i) = boolvar ' + bits ∧ i < 0 → boolvar | A User Theorem |
| int2bits-inj | ⊦ int2bits(i) = int2bits(j) ↔ i = j | A User Theorem |
| int2bits-inv-first | ⊦ 0 ≤ j → bitsinvert(int2bits(j)).first | A User Theorem |
| int2bits-leading-sgn | ⊦ (bits.first ↔ bits.rest.first) ∧ 1 < # bits → int2bits(i) ≠ bits | A User Theorem |
| int2bits-lelen | ⊦ 0 < i → (# int2bits(i) ≤ m ↔ i < 2 ^ (n→i(m) - 1)) | A User Theorem |
| int2bits-lelen-01 | ⊦ 0 < i ∧ 0 ≤ j → (2 ^ j ≤ i ↔ ¬ # int2bits(i) ≤ i→n(j) + 1) | A User Theorem |
| int2bits-lelen-02 | ⊦ i < ~1 ∧ 0 ≤ j → (2 ^ j + i < 0 ↔ ¬ # int2bits(i) ≤ i→n(j) + 1) | A User Theorem |
| int2bits-lelen-03 | ⊦ i < ~1 → (# int2bits(i) ≤ m ↔ 0 ≤ i + 2 ^ (n→i(m) - 1)) | A User Theorem |
| int2bits-lelen-04 | ⊦ i < 0 ∧ 0 ≤ j ∧ ~ i ≠ 2 ^ j → (2 ^ j + i ≤ 0 ↔ ¬ # int2bits(i) ≤ i→n(j) + 1) | A User Theorem |
| int2bits-lelen-05 | ⊦ i < ~1 → (m ≤ # int2bits(i) ↔ ¬ 0 ≤ i + 2 ^ (n→i(m) - 2)) | A User Theorem |
| int2bits-lelen-06 | ⊦ 0 < i → (m ≤ # int2bits(i) ↔ ¬ i < 2 ^ (n→i(m) - 2)) | A User Theorem |
| int2bits-lelen-07 | ⊦ ¬ 2 ^ n→i(# int2bits(~ j)) + j ≤ 0 | A User Theorem |
| int2bits-len-2-32-1 | ⊦ # int2bits(4294967295) = 33 | A User Theorem |
| int2bits-len-abs | ⊦ ¬ # int2bits(j) + 1 < # int2bits(~ j) | A User Theorem |
| int2bits-len-abs-01 | ⊦ ¬ # int2bits(j) + 1 < # int2bits(abs(j)) | A User Theorem |
| int2bits-len-add | ⊦ j < 0 ∧ j0 < 0 ∧ abs(j0) < 2 ^ i ∧ 0 ≤ i → # int2bits(~(j * 2 ^ i + j0)) = # int2bits(~ j) + i→n(i) | A User Theorem |
| int2bits-len-eq | ⊦ j ≠ 2 ^ n→i(# int2bits(j)) | A User Theorem |
| int2bits-len-eq-01 | ⊦ 2 ^ n→i(# int2bits(~ j)) + j ≠ 0 | A User Theorem |
| int2bits-len-mod2pot | ⊦ 0 < j ∧ 0 < i → ¬ i→n(i) + 1 < # int2bits(j % 2 ^ i) | A User Theorem |
| int2bits-len-mon | ⊦ abs(i) < abs(j) → # int2bits(i) ≤ # int2bits(j) | A User Theorem |
| int2bits-len-neg | 0 ≤ i, ~(2 ^ (i + 1)) ≤ j, j < ~(2 ^ i) ⊦ # int2bits(j) = i→n(i + 2) | A User Theorem |
| int2bits-len-neg-01 | ⊦ i < 0 → # int2bits(i) = # int2bits(~ i - 1) | A User Theorem |
| int2bits-len-neg-02 | ⊦ ¬(∃ i. j = ~(2 ^ i)) ∧ j < 0 → # int2bits(j) = # int2bits(~ j) | A User Theorem |
| int2bits-len-one | ⊦ 0 ≤ i → (# int2bits(i) = 1 ↔ i = 0) | A User Theorem |
| int2bits-len-pos | 0 ≤ i, 2 ^ i ≤ j, j < 2 ^ (i + 1) ⊦ # int2bits(j) = i→n(i + 2) | A User Theorem |
| int2bits-len-pos-01 | ⊦ 0 ≤ j ∧ j < 2 ^ i → (i→n(i) < # int2bits(j) ↔ # int2bits(j) = i→n(i) + 1) | A User Theorem |
| int2bits-len-pos-02 | ⊦ 0 < j ∧ 0 ≤ i → # int2bits(j * 2 ^ i) = # int2bits(j) + i→n(i) | A User Theorem |
| int2bits-len-pos-03 | ⊦ j < 0 ∧ 0 ≤ i → # int2bits(~(j * 2 ^ i)) = # int2bits(~ j) + i→n(i) | A User Theorem |
| int2bits-len-pos-pred | ⊦ ¬(∃ i. 2 ^ i = j) ∧ 0 ≤ j → # int2bits(j - 1) = # int2bits(j) | A User Theorem |
| int2bits-len-pos-suc | ⊦ ¬(∃ i. 2 ^ i - 1 = j) ∧ 0 ≤ j → # int2bits(j) = # int2bits(j + 1) | A User Theorem |
| int2bits-len-range | ~(2 ^ i) ≤ j, j < 2 ^ i ⊦ # int2bits(j) ≤ i→n(i + 1) | A User Theorem |
| int2bits-leneq-neg | ⊦ j < 0 ∧ 1 < n → (# int2bits(j) = n ↔ ~(2 ^ (n→i(n) - 1)) ≤ j ∧ j < ~(2 ^ (n→i(n) - 2))) | A User Theorem |
| int2bits-leneq-pos | ⊦ 0 ≤ j ∧ 1 < n → (# int2bits(j) = n ↔ 2 ^ (n→i(n) - 2) ≤ j ∧ j < 2 ^ (n→i(n) - 1)) | A User Theorem |
| int2bits-less-2pot | 0 ≤ j ⊦ j < 2 ^ (n→i(# int2bits(j)) - 1) | A User Theorem |
| int2bits-less-2pot-01 | ⊦ abs(j) ≤ 2 ^ (n→i(# int2bits(j)) - 1) | A User Theorem |
| int2bits-less-2pot-02 | ⊦ 0 ≤ j → ¬ 2 ^ n→i(# int2bits(j)) < j | A User Theorem |
| int2bits-lslen | ⊦ 0 < i → (# int2bits(i) < m ↔ i < 2 ^ (n→i(m) - 2)) | A User Theorem |
| int2bits-lslen-01 | ⊦ 0 < i ∧ 0 ≤ j → (i < 2 ^ j ↔ # int2bits(i) ≤ i→n(j) + 1) | A User Theorem |
| int2bits-lslen-02 | ⊦ i < ~1 ∧ 0 ≤ j → (0 ≤ 2 ^ j + i ↔ # int2bits(i) ≤ i→n(j) + 1) | A User Theorem |
| int2bits-lslen-03 | ⊦ i < ~1 → (# int2bits(i) < m ↔ 0 ≤ i + 2 ^ (n→i(m) - 2)) | A User Theorem |
| int2bits-lslen-04 | ⊦ i < 0 ∧ 0 ≤ j ∧ ~ i ≠ 2 ^ j → (0 < 2 ^ j + i ↔ # int2bits(i) ≤ i→n(j) + 1) | A User Theorem |
| int2bits-lslen-05 | ⊦ i < ~1 → (m < # int2bits(i) ↔ ¬ 0 ≤ i + 2 ^ (n→i(m) - 1)) | A User Theorem |
| int2bits-lslen-06 | ⊦ 0 < i → (m < # int2bits(i) ↔ ¬ i < 2 ^ (n→i(m) - 1)) | A User Theorem |
| int2bits-lslen-07 | ⊦ ¬ # int2bits(j) + 1 < # int2bits(j + 1) | A User Theorem |
| int2bits-lslen-08 | ⊦ ¬ # int2bits(j) + 1 < # int2bits(j - 1) | A User Theorem |
| int2bits-lslen-09 | ⊦ ¬ # int2bits(~ j) + 1 < # int2bits(~(j + 1)) | A User Theorem |
| int2bits-lslen-10 | ⊦ ¬ 2 ^ n→i(# int2bits(~ j)) + j < 0 | A User Theorem |
| int2bits-lslen-11 | ⊦ 0 < i ∧ 0 ≤ j → (i < 2 ^ j ↔ ¬ i→n(j + 1) < # int2bits(i)) | A User Theorem |
| int2bits-lslen-12 | ⊦ 0 < i ∧ 0 ≤ j → (2 ^ j < i ↔ i→n(j) + 2 ≤ # int2bits(i) ∧ i ≠ 2 ^ j) | A User Theorem |
| int2bits-mod2 | ⊦ j < 0 → fillsgn(2, int2bits(j % 2)).rest = int2bits(j % 2) | A User Theorem |
| int2bits-mod2-len | ⊦ i ≤ 0 → # int2bits(i % 2) = 1 | A User Theorem |
| int2bits-mod2-neg | ⊦ i ≤ 0 → int2bits(i % 2) = int2bits(i).last ' | A User Theorem |
| int2bits-mod256 | ⊦ 0 < j ∧ 0 ≤ j0 ∧ j0 < 256 → int2bits(j * 256 + j0) = int2bits(j) + fillsgn(9, int2bits(j0)).rest | A User Theorem |
| int2bits-mod2pot | ⊦ 0 < j ∧ 0 ≤ j0 ∧ j0 < 2 ^ i ∧ 0 ≤ i → int2bits(j * 2 ^ i + j0) = int2bits(j) + fillsgn(i→n(i + 1), int2bits(j0)).rest | A User Theorem |
| int2bits-mone | ⊦ i + 1 = 0 → int2bits(i) = true ' | A User Theorem |
| int2bits-mone-01 | ⊦ int2bits(~ 1) = true ' | A User Theorem |
| int2bits-mone-02 | ⊦ int2bits(~1) = true ' | A User Theorem |
| int2bits-neg-01 | ⊦ 0 < i → sgn(bitsinvert(uint2bits(i)) +1) = int2bits(~ i) | A User Theorem |
| int2bits-neg-02 | j < 0, ¬(∃ i. ~(2 ^ i) = j) ⊦ int2bits(j) = int2bits(2 ^ n→i(# int2bits(~ j)) + j).rest | A User Theorem |
| int2bits-neg-03 | ⊦ j < 0 → int2bits(j) = sgn(int2bits(2 ^ n→i(# int2bits(~ j)) + j).rest) | A User Theorem |
| int2bits-neg-04 | ⊦ j < 0 ∧ ¬(∃ i. ~(2 ^ i) = j) → int2bits(j) = int2bits(2 ^ n→i(# int2bits(~ j)) + j).rest | A User Theorem |
| int2bits-neg-num | i < 0 ⊦ int2bits((* i)) = sgn(bitsinvert(uint2bits(abs(i))) +1) | A User Theorem |
| int2bits-not-empty | ⊦ int2bits(j) ≠ [] | A User Theorem |
| int2bits-one-bit | ⊦ int2bits(i) = boolvar ' ↔ i = 0 ∧ ¬ boolvar ∨ i = ~1 ∧ boolvar | A User Theorem |
| int2bits-ones | ⊦ ¬ false ∈ int2bits(j) ↔ j = ~ 1 | A User Theorem |
| int2bits-pos-num | 0 ≤ i ⊦ int2bits((* i)) = uint2bits(i) | A User Theorem |
| int2bits-pred | ⊦ 0 < j → int2bits(j - 1) = sgn(bitsinvert(bitsinvert(int2bits(j)) +1)) | A User Theorem |
| int2bits-pred-intro | ⊦ 0 < j → int2bits(j) = sgn(false ' + int2bits(j - 1) +1) | A User Theorem |
| int2bits-rec-2pot-neg-01 | ⊦ j ≤ ~(2 ^ i) ∧ 0 < i ∧ j % 2 ^ i = 0 → int2bits(j) = int2bits(j / 2 ^ i) + fillsgn(i→n(i + 1), int2bits(j % 2 ^ i)).rest | A User Theorem |
| int2bits-rec-2pot-neg-02 | ⊦ j ≤ ~(2 ^ i) ∧ 0 < i ∧ j % 2 ^ i ≠ 0 → int2bits(j) = int2bits(j / 2 ^ i - 1) + fillsgn(i→n(i + 1), int2bits(j % 2 ^ i)).rest | A User Theorem |
| int2bits-rec-2pot-neg-03 | ⊦ j ≤ ~(2 ^ i) ∧ 0 < i → int2bits(j) = int2bits((j - (2 ^ i - 1)) / 2 ^ i) + fillsgn(i→n(i + 1), int2bits(j % 2 ^ i)).rest | A User Theorem |
| int2bits-rec-2pot-pos | ⊦ 2 ^ i ≤ j ∧ 0 < i → int2bits(j) = int2bits(j / 2 ^ i) + fillsgn(i→n(i + 1), int2bits(j % 2 ^ i)).rest | A User Theorem |
| int2bits-rec-neg | ⊦ j < 0 ∧ j ≠ ~1 → int2bits(j) = int2bits((j - 1) / 2) + (~1 = j % 2)' | A User Theorem |
| int2bits-rec-neg-01 | ⊦ j < ~1 → int2bits(j) = int2bits((j - 1) / 2) + int2bits(j % 2) | A User Theorem |
| int2bits-rec-neg-02 | ⊦ j % 2 = 0 ∧ j < 0 → int2bits(j) = int2bits(j / 2) + false ' | A User Theorem |
| int2bits-rec-neg-03 | ⊦ j % 2 ≠ 0 ∧ j < ~1 → int2bits(j) = int2bits(j / 2 - 1) + true ' | A User Theorem |
| int2bits-rec-pos | ⊦ 1 < i → int2bits(i) = int2bits(i / 2) + (i % 2 = 1) | A User Theorem |
| int2bits-rec-pos-01 | ⊦ 1 < i → int2bits(i) = int2bits(i / 2) + (i % 2 = 1)' | A User Theorem |
| int2bits-rest | ⊦ int2bits(j).rest = [] ↔ j = 0 ∨ j = ~1 | A User Theorem |
| int2bits-restsgn | ¬(∃ i. 2 ^ i = j), 0 ≤ j ⊦ sgn(int2bits(2 ^ n→i(# int2bits(j)) - j).rest) = int2bits(2 ^ n→i(# int2bits(j)) - j).rest | A User Theorem |
| int2bits-sgn | ⊦ sgn(int2bits(i)) = int2bits(i) | A User Theorem |
| int2bits-sgn-02 | ⊦ j ≠ 0 ∧ j ≠ ~1 → sgn(int2bits(j) + bits) = int2bits(j) + bits | A User Theorem |
| int2bits-succ | ⊦ 0 ≤ j → int2bits(j + 1) = sgn(false ' + int2bits(j) +1) | A User Theorem |
| int2bits-succ-intro | ⊦ 0 ≤ j → int2bits(j) = sgn(bitsinvert(bitsinvert(int2bits(j + 1)) +1)) | A User Theorem |
| int2bits-true | ⊦ int2bits(j) = true ' ↔ j = ~1 | A User Theorem |
| int2bits-truein | ⊦ true ∈ int2bits(j) ↔ j ≠ 0 | A User Theorem |
| int2bits-truein-01 | ⊦ true ∈ int2bits(j).rest ↔ j ≠ 0 ∧ ¬(∃ i. 0 ≤ i ∧ j = ~(2 ^ i)) | A User Theorem |
| int2bits-truetrue | ⊦ int2bits(j) ≠ true ' + true ' | A User Theorem |
| int2bits-truetrue-01 | ⊦ int2bits(j) ≠ true ' + true ' + bits | A User Theorem |
| int2bits-zero | ⊦ int2bits(0) = false ' | A User Theorem |
| int2int-inj | ⊦ bits2int(int2bits(i)) = i | A User Theorem |
| int2int-lastn-2pot | ⊦ i % 2 ^ n→i(m) = 0 ∧ m ≤ # int2bits(i) ∧ m ≠ 0 → bits2int(lastn(m, int2bits(i))) = 0 | A User Theorem |
| int2int-lastn-negneg | ⊦ i < 0 ∧ lastn(m, int2bits(i)).first ∧ m ≤ # int2bits(i) ∧ m ≠ 0 ∧ ~ i ≠ 2 ^ n→i(m) → bits2int(lastn(m, int2bits(i))) = i % 2 ^ n→i(m) | A User Theorem |
| int2int-lastn-negpos | ⊦ i < 0 ∧ ¬ lastn(m, int2bits(i)).first ∧ m ≤ # int2bits(i) ∧ m ≠ 0 ∧ i % 2 ^ n→i(m) ≠ 0 → bits2int(lastn(m, int2bits(i))) = i % 2 ^ n→i(m) + 2 ^ n→i(m) | A User Theorem |
| int2int-lastn-posneg | ⊦ 0 < i ∧ lastn(m, int2bits(i)).first ∧ m ≤ # int2bits(i) ∧ m ≠ 0 → bits2int(lastn(m, int2bits(i))) = i % 2 ^ n→i(m) - 2 ^ n→i(m) | A User Theorem |
| int2int-lastn-pospos | ⊦ 0 < i ∧ ¬ lastn(m, int2bits(i)).first ∧ m ≤ # int2bits(i) ∧ m ≠ 0 → bits2int(lastn(m, int2bits(i))) = i % 2 ^ n→i(m) | A User Theorem |
| int2int-neg | ⊦ j < 0 → bits2int(int2bits(j)) = bits2int(int2bits(2 ^ n→i(# int2bits(~ j)) + j).rest) | A User Theorem |
| int2int-rest | ⊦ 0 < i → bits2int(int2bits(i).rest) = i - 2 ^ (n→i(# uint2bits(i)) - 1) | A User Theorem |
| int2int-rest-01 | ⊦ j < ~1 → bits2int(int2bits(j).rest) = j + 2 ^ (n→i(# int2bits(j)) - 1) | A User Theorem |
| int2uint-fill | ⊦ 0 ≤ j → bits2uint(fillsgn(n, int2bits(j))) = j | A User Theorem |
| int2uint-inv | ⊦ j < 0 → bits2uint(bitsinvert(int2bits(j))) + 1 = ~ j | A User Theorem |
| int2uint-inv-01 | ⊦ j < 0 → bits2uint(bitsinvert(int2bits(j))) = ~ j - 1 | A User Theorem |
| int2uint-neg | ⊦ j < 0 → bits2uint(int2bits(j)) = 2 ^ n→i(# int2bits(j)) + j | A User Theorem |
| int2uint-pos | ⊦ 0 ≤ i → bits2uint(bitsinvert(int2bits(i))) = 2 ^ n→i(# int2bits(i)) - i + 1 | A User Theorem |
| int2uint-pos-01 | ⊦ 0 ≤ j → bits2uint(int2bits(j)) = j | A User Theorem |
| int2unit-inv-rest | ⊦ 0 < i → bits2uint(bitsinvert(int2bits(i).rest)) = 2 ^ (n→i(# uint2bits(i)) - 1) - i + 1 | A User Theorem |
| ubits2bits | ⊦ bits ≠ [] ∧ bits.first → bits2uint(bits) = bits2int(bits) + 2 ^ n→i(# bits) | A User Theorem |
| ubits2ubits-def | ⊦ uint2bits(bits2uint(bits)) = sgn(false ' + bits) | A User Theorem |
| ubits2ubits-neg | ⊦ bits.first ∧ bits ≠ [] → uint2bits(bits2uint(bits)) = false ' + bits | A User Theorem |
| ubits2ubits-pos | ⊦ ¬ bits.first ∧ bits ≠ [] → uint2bits(bits2uint(bits)) = sgn(bits) | A User Theorem |
| uint2bits-2pot | 0 ≤ i ⊦ uint2bits(2 ^ i) = false ' + true ' + mklist(false, i→n(i)) | A User Theorem |
| uint2bits-2pot-01 | 0 ≤ i, 0 < j ⊦ uint2bits(j * 2 ^ i) = uint2bits(j) + mklist(false, i→n(i)) | A User Theorem |
| uint2bits-2pot-02 | 0 < i ⊦ uint2bits(2 ^ i - 1) = false ' + mklist(true, i→n(i)) | A User Theorem |
| uint2bits-2pot-03 | ⊦ ¬ true ∈ bits ∧ 0 ≤ i → (uint2bits(i) = false ' + true ' + bits ↔ i = 2 ^ n→i(# bits)) | A User Theorem |
| uint2bits-2pot-04 | ⊦ ¬ false ∈ bits ∧ 0 ≤ i → (uint2bits(i) = false ' + true ' + bits ↔ i = 2 ^ (n→i(# bits) + 1) - 1) | A User Theorem |
| uint2bits-2pot-05 | ⊦ ¬ false ∈ bits ∧ 0 ≤ i → (uint2bits(i) = boolvar ' + bits ↔ ¬ boolvar ∧ i = 2 ^ n→i(# bits) - 1) | A User Theorem |
| uint2bits-2pot-06 | 0 ≤ i, j < 0 ⊦ uint2bits(~(j * 2 ^ i)) = uint2bits(~ j) + mklist(false, i→n(i)) | A User Theorem |
| uint2bits-2pot-neg-mone | ⊦ 0 < j ∧ 0 < i → uint2bits(j * 2 ^ i - 1) = uint2bits(j - 1) + mklist(true, i→n(i)) | A User Theorem |
| uint2bits-2potrec | 0 ≤ i, 2 ^ i ≤ j ⊦ uint2bits(j) = uint2bits(j / 2 ^ i) + fillsgn(i→n(i + 1), uint2bits(j % 2 ^ i)).rest | A User Theorem |
| uint2bits-add-high | ⊦ j < 0 ∧ 0 < i ∧ 2 ^ (i - 1) < abs(j) ∧ abs(j) ≤ 2 ^ i → uint2bits(j + 2 ^ i) = sgn(int2bits(j).rest) | A User Theorem |
| uint2bits-add-high-01 | ⊦ j0 < 0 ∧ 0 < i ∧ 2 ^ (i - 1) < abs(j0) ∧ abs(j0) ≤ 2 ^ i ∧ 1 < j → uint2bits(j * 2 ^ i + j0) = uint2bits(j - 1) + fillsgn(i→n(i), int2bits(j0).rest) | A User Theorem |
| uint2bits-add-high-02 | ⊦ j0 < 0 ∧ 0 < i ∧ 2 ^ (i - 1) < abs(j0) ∧ abs(j0) ≤ 2 ^ i ∧ 0 < j → uint2bits(j * 2 ^ i + j0) = sgn(uint2bits(j - 1) + fillsgn(i→n(i), int2bits(j0).rest)) | A User Theorem |
| uint2bits-add-low | ⊦ j < 0 ∧ 0 < i ∧ abs(j) ≤ 2 ^ (i - 1) → uint2bits(j + 2 ^ i) = false ' + fillsgn(i→n(i), int2bits(j)) | A User Theorem |
| uint2bits-add-low-01 | ⊦ j0 < 0 ∧ 0 < i ∧ abs(j0) ≤ 2 ^ (i - 1) ∧ 0 < j → uint2bits(j * 2 ^ i + j0) = uint2bits(j - 1) + fillsgn(i→n(i), int2bits(j0)) | A User Theorem |
| uint2bits-div2pot | 0 ≤ i, 2 ^ i ≤ j ⊦ uint2bits(j / 2 ^ i) = butlastn(i→n(i), uint2bits(j)) | A User Theorem |
| uint2bits-div2pot-01 | 0 ≤ i, 0 < j, j % 2 ^ i = 0 ⊦ uint2bits(j) = uint2bits(j / 2 ^ i) + mklist(false, i→n(i)) | A User Theorem |
| uint2bits-empty | 0 ≤ i ⊦ uint2bits(i) ≠ [] | A User Theorem |
| uint2bits-empty-01 | ⊦ i < 0 → uint2bits(~ i) ≠ [] | A User Theorem |
| uint2bits-eq | ⊦ 0 < i → uint2bits(i) ≠ boolvar ' | A User Theorem |
| uint2bits-expos0 | 0 < i ⊦ ∃ bits. uint2bits(i) = false ' + true ' + bits | A User Theorem |
| uint2bits-expos1 | 1 < j ⊦ ∃ bits. uint2bits(j) = false ' + true ' + bits ∧ bits ≠ [] | A User Theorem |
| uint2bits-false | ⊦ 0 ≤ i → uint2bits(i) ≠ false ' + false ' + bits | A User Theorem |
| uint2bits-falsein | ⊦ 1 < i → false ∈ bitsinvert(uint2bits(i)) +1 | A User Theorem |
| uint2bits-falsein-01 | ⊦ 0 < j → (false ∈ uint2bits(j).rest ↔ ¬(∃ i. j = 2 ^ i - 1)) | A User Theorem |
| uint2bits-first | ⊦ 0 ≤ i → ¬ uint2bits(i).first | A User Theorem |
| uint2bits-first-01 | ⊦ 0 ≤ i → uint2bits(i) ≠ true ' + bits | A User Theorem |
| uint2bits-first-02 | ⊦ 0 ≤ j → ¬ uint2bits(j).first | A User Theorem |
| uint2bits-first-03 | ⊦ 0 < j → ¬ uint2bits(j).first | A User Theorem |
| uint2bits-first-04 | ⊦ j < 0 → ¬ uint2bits(~ j).first | A User Theorem |
| uint2bits-first-05 | ⊦ j < 0 → uint2bits(~ j) ≠ true ' + bits | A User Theorem |
| uint2bits-firstpos | ⊦ uint2bits(j) = boolvar ' + bits ∧ 0 ≤ j → ¬ boolvar | A User Theorem |
| uint2bits-inj | 0 ≤ i, 0 ≤ j ⊦ uint2bits(i) = uint2bits(j) ↔ i = j | A User Theorem |
| uint2bits-inv | ⊦ 0 ≤ i → bitsinvert(uint2bits(i)) ≠ false ' + bits | A User Theorem |
| uint2bits-len | 0 ≤ i, 2 ^ i ≤ j, j < 2 ^ (i + 1) ⊦ # uint2bits(j) = i→n(i + 2) | A User Theorem |
| uint2bits-len-01 | 2 * 2 ^ i ≤ j, j < 3 * 2 ^ i, 0 ≤ i ⊦ # uint2bits(j) = i→n(i + 3) | A User Theorem |
| uint2bits-len-add | ⊦ 0 < j ∧ 0 ≤ j0 ∧ j0 < 2 ^ i ∧ 0 ≤ i → # uint2bits(j * 2 ^ i + j0) = # uint2bits(j) + i→n(i) | A User Theorem |
| uint2bits-len-max | 0 ≤ i, 0 ≤ j, j < 2 ^ i ⊦ # uint2bits(j) ≤ i→n(i + 1) | A User Theorem |
| uint2bits-len-min | 0 ≤ i, 0 ≤ j, 2 ^ i ≤ j ⊦ i→n(i + 1) < # uint2bits(j) | A User Theorem |
| uint2bits-len-mon | ⊦ 0 ≤ i ∧ i ≤ j → # uint2bits(i) ≤ # uint2bits(j) | A User Theorem |
| uint2bits-len-mon-01 | ⊦ 0 ≤ i ∧ i ≤ j → (¬ # uint2bits(i) ≤ # uint2bits(j) ↔ false) | A User Theorem |
| uint2bits-len-mon-02 | ⊦ 0 ≤ i ∧ i ≤ j → ¬ # uint2bits(j) < # uint2bits(i) | A User Theorem |
| uint2bits-len-pos | ⊦ 0 < j ∧ 0 ≤ i → # uint2bits(j * 2 ^ i) = # uint2bits(j) + i→n(i) | A User Theorem |
| uint2bits-mod2pot | 0 ≤ i, 2 ^ i < j ⊦ uint2bits(j % 2 ^ i) = sgn(false ' + lastn(i→n(i), uint2bits(j).rest)) | A User Theorem |
| uint2bits-mod2pot-01 | ⊦ 0 ≤ i ∧ 0 < j ∧ 0 ≤ j0 ∧ j0 < 2 ^ i → uint2bits(j * 2 ^ i + j0) = uint2bits(j) + fillsgn(i→n(i) + 1, uint2bits(j0)).rest | A User Theorem |
| uint2bits-not-one | 0 ≤ i ⊦ uint2bits(i) ≠ true ' | A User Theorem |
| uint2bits-onein | ⊦ 0 < j → true ∈ uint2bits(j) | A User Theorem |
| uint2bits-onein-01 | ⊦ j < 0 → true ∈ uint2bits(~ j) | A User Theorem |
| uint2bits-pos-num | 1 < i ⊦ uint2bits((* i)) = uint2bits(i / 2) + (i % 2 = 1) | A User Theorem |
| uint2bits-pred | ⊦ 0 < j → uint2bits(j - 1) = sgn(bitsinvert(bitsinvert(uint2bits(j)) +1)) | A User Theorem |
| uint2bits-pred-intro | ⊦ 0 < j → uint2bits(j) = sgn(false ' + uint2bits(j - 1) +1) | A User Theorem |
| uint2bits-rec-01 | ⊦ 0 < i ∧ i ≠ 1 → uint2bits(i) = uint2bits(i / 2) + (i % 2 = 1) | A User Theorem |
| uint2bits-rest | ⊦ 0 < i → uint2bits(i).rest ≠ [] | A User Theorem |
| uint2bits-restsgn | 0 < i, 0 ≤ j, 2 ^ i < j, j < 2 * 2 ^ i ⊦ sgn(uint2bits(2 ^ (i + 2) - j).rest) = uint2bits(2 ^ (i + 2) - j).rest | A User Theorem |
| uint2bits-second | ⊦ 0 < i → uint2bits(i).rest.first | A User Theorem |
| uint2bits-sgn | ⊦ 0 < i → sgn(uint2bits(i)) = uint2bits(i) | A User Theorem |
| uint2bits-sgn-01 | ⊦ 0 ≤ j → sgn(uint2bits(j)) = uint2bits(j) | A User Theorem |
| uint2bits-sgn-02 | ⊦ 0 < j → sgn(uint2bits(j) + bits) = uint2bits(j) + bits | A User Theorem |
| uint2bits-sgn-2pot | 0 < j, ∀ i. 0 ≤ i → j ≠ 2 ^ i ⊦ sgn(bitsinvert(uint2bits(j)) +1) = bitsinvert(uint2bits(j)) +1 | A User Theorem |
| uint2bits-sgn-2pot-01 | 0 < j, true ∈ uint2bits(j).rest.rest ⊦ sgn(bitsinvert(uint2bits(j)) +1) = bitsinvert(uint2bits(j)) +1 | A User Theorem |
| uint2bits-sgn-false | ⊦ 0 ≤ j → sgn(false ' + uint2bits(j)) = uint2bits(j) | A User Theorem |
| uint2bits-sgn-false-01 | ⊦ 0 < j → sgn(uint2bits(j) + false ') = uint2bits(j) + false ' | A User Theorem |
| uint2bits-sgn-first | ⊦ 0 < j → sgn(bitsinvert(uint2bits(j)) +1) ≠ false + bits | A User Theorem |
| uint2bits-succ | ⊦ 0 ≤ j → uint2bits(j + 1) = sgn(false ' + uint2bits(j) +1) | A User Theorem |
| uint2bits-succ-intro | ⊦ 0 ≤ j → uint2bits(j) = sgn(bitsinvert(bitsinvert(uint2bits(j + 1)) +1)) | A User Theorem |
| uint2bits-truein | ⊦ 0 < j → true ∈ uint2bits(j).rest | A User Theorem |
| uint2bits-zero-01 | 0 ≤ i ⊦ uint2bits(i) = false ' ↔ i = 0 | A User Theorem |
| uint2int-01 | ⊦ 0 ≤ j → bits2int(uint2bits(j)) = j | A User Theorem |
| uint2int-invsucc | ⊦ j < 0 → bits2int(bitsinvert(uint2bits(~ j)) +1) = j | A User Theorem |
| uint2int-rest | ⊦ 0 < i → bits2int(uint2bits(i).rest) = i - 2 ^ (n→i(# uint2bits(i)) - 1) | A User Theorem |
| uint2uint-inv | 0 < i ⊦ bits2uint(bitsinvert(uint2bits(i))) = 2 ^ n→i(# uint2bits(i)) - i + 1 | A User Theorem |
| uint2uint-inv-01 | 0 < i ⊦ bits2uint(bitsinvert(uint2bits(i)) +1) = 2 ^ n→i(# uint2bits(i)) - i | A User Theorem |
| uint2uint-neg | ⊦ i < 0 → bits2uint(uint2bits(~ i)) = ~ i | A User Theorem |
| uint2uint-pos | ⊦ 0 ≤ i → bits2uint(uint2bits(i)) = i | A User Theorem |