| int2bits(j - 1) = int2bits(2 ^ n→i(# int2bits(1 - j)) + j - 1).rest, 1 = 2 ^ i0 + j, 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: uint2bits-one: ⊦ uint2bits(1) = false + true;%uint2bits-pos-num: 1 < i ⊦ uint2bits((* i)) = uint2bits(i / 2) + (i % 2 = 1);%int2bits-pos-num: 0 ≤ i ⊦ int2bits((* i)) = uint2bits(i);%int2bits-zero: ⊦ int2bits(0) = false ';%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 = j * i;% ⊦ i - j = i0 ↔ i = i0 + j;% ⊦ i - j - i0 = i - j + i0;% ⊦ i - j + i = ~ j;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i + j = j + i;% ⊦ i - (j - j0) = i + j0 - j;% ⊦ (* i) + i0 - (* j) = (i - j) + i0;% ⊦ i + 0 = i;% ⊦ i + (j - i0) = i + j - i0;% ⊦ i + j - i0 + j = i - i0;% ⊦ i + (j - i) = j;% ⊦ ~(i - j) = j - i;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ boolvar ' ≠ [];% ⊦ boolvar ' = boolvar0 ' + bits ↔ (boolvar ↔ boolvar0) ∧ bits = [];% ⊦ (boolvar ' + bits).rest = bits;% ⊦ bits + boolvar = bits + boolvar ';% ⊦ boolvar + boolvar0 = boolvar ' + boolvar0 ';% ⊦ i < 0 → 2 ^ i = 0;% ⊦ # boolvar ' = 0 +1;% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ # mklist(boolvar, n) = n;% ⊦ 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;% ⊦ 1 < 2 ^ i ↔ 0 < i;% ⊦ 0 < j → abs(j) = j;% ⊦ 0 < i → 2 ^ (i + 1) - 2 ^ i = 2 ^ i;% ⊦ i < j → ¬ j < i;%⊦ 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