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