| 2 ^ i0 + j = 1, 0 ≤ j0 + 2 ^ (i - 1), 0 < 2 ^ (i - 1) + j0, j0 < 0, j < 0, 0 < i, j * 2 ^ i + j0 < 0, 0 < 2 ^ i + j0, 0 ≤ i, 0 < 2 ^ n→i(# int2bits(~ j)) + j, 0 ≤ (2 ^ n→i(# int2bits(~ j)) + j) * 2 ^ i + j0 ⊦ j * 2 ^ i + j0 = 0, sgn(int2bits(2 ^ n→i(# int2bits(~ j)) + j - 1).rest + fillsgn(i→n(i), int2bits(j0))) = int2bits(j - 1) + fillsgn(i→n(i), int2bits(j0)) |
Used simplifier rules: int2bits-2pot-02: 0 ≤ i ⊦ int2bits(2 ^ i - 1) = false ' + mklist(true, i→n(i));%int2bits-2pot-01: 0 ≤ i ⊦ int2bits(~(2 ^ i)) = true ' + mklist(false, i→n(i));%int2bits-2pot: 0 ≤ i ⊦ int2bits(2 ^ i) = false ' + true ' + mklist(false, i→n(i));% ⊦ i - j = i0 ↔ i = i0 + j;% ⊦ i + (j - i) = j;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i + j = j + i;% ⊦ ~(i - j) = j - i;% ⊦ i < 0 → 2 ^ i = 0;% ⊦ i * j = j * i;% ⊦ i * j * j0 = (i * j) * j0;% ⊦ 1 * i = i;% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ # boolvar ' = 0 +1;% ⊦ # mklist(boolvar, n) = n;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ n→i(m + n) = n→i(m) + n→i(n);% ⊦ n→i(i→n(i)) = abs(i);% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m + n = n + m;% ⊦ i + (j - i0) = i + j - i0;% ⊦ i - j - i0 = i - j + i0;% ⊦ i + j - i0 + j = i - i0;% ⊦ i - j + i = ~ j;% ⊦ i - j < i0 ↔ i < j + i0;% ⊦ i + 0 = i;% ⊦ 1 < 2 ^ i ↔ 0 < i;% ⊦ 0 < j → abs(j) = j;% ⊦ 0 < i → 2 ^ (i + 1) - 2 ^ i = 2 ^ i;% ⊦ i < j → ¬ j < i;% ⊦ (boolvar ' + bits).rest = bits;%⊦ 0 < i → sgn(true ' + mklist(false, i→n(i)) + bits) = true ' + mklist(false, i→n(i)) + bits;% ⊦ bits + bits0 = bits + bits1 ↔ bits0 = bits1; Used formulas: j = 1 - 2 ^ i0