Proof step 146 from proof int2bytes-rec-neg-05 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 147:

  ⊦ i < 0 → (~1 ≤ i ↔ i = ~1)

• Proof step 148:

  ¬ j % 2 ^ (i * 8) < 0, # fillsgn(i→n(i * 8) + 1, int2bits(j % 2 ^ (i * 8))).rest % 8 = 0, i→n(i * 8) + 1 < # int2bits(j % 2 ^ (i * 8)), j + 2 ^ (i * 8) < i, j + 2 ^ (i * 8) ≤ 0, j + 2 ^ (i * 8 - 1) < 0, 0 < i, ~1 ≤ j % 2 ^ (i * 8) ⊦ bits2bytes(fillsgn(i→n(i * 8) + 1, int2bits(j % 2 ^ (i * 8))).rest) = fix(i→n(i) + 1, int2bytes(j % 2 ^ (i * 8))).rest, j % 2 ^ (i * 8) = 0, fillsgn(i→n(i * 8) + 1, int2bits(j % 2 ^ (i * 8))).rest = []

Rule argument

Additional information

Used simplifier rules: int2bytes-byte: ~128 ≤ i, i < 128 ⊦ int2bytes((* i)) = i2b(i) ';% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i + j = j + i;% ⊦ m < n → n ≠ 0; (forward)% ⊦ j < i ∧ i ≤ 0 → j < 0; (forward)%i < 0 ⊦ int2bits((* i)) = sgn(bitsinvert(uint2bits(abs(i))) +1);% ⊦ uint2bits(1) = false + true;% ⊦ boolvar + boolvar0 = boolvar ' + boolvar0 ';% ⊦ bitsinvert(false ' + bits) = true + bitsinvert(bits);% ⊦ bitsinvert(true ') = false ';% ⊦ boolvar + bits = boolvar ' + bits;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ (bits + false ')+1 = bits + true;% ⊦ bits + boolvar = bits + boolvar ';% ⊦ sgn(true ' + true ') = true ';% ⊦ fillsgn(n + 1, boolvar ') = mklist(boolvar, n + 1);% ⊦ mklist(boolvar, m + n) = mklist(boolvar, m) + mklist(boolvar, n);%n ≠ 0 ⊦ mklist(true, (* n)) = true ' + mklist(true, n -1);% ⊦ mklist(boolvar, 0) = [];% ⊦ bits + [] = bits;% ⊦ mklist(boolvar, n) + boolvar ' = boolvar ' + mklist(boolvar, n);% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m + n = n + m;% ⊦ (boolvar ' + bits).rest = bits;% ⊦ # mklist(boolvar, n) = n;% ⊦ # boolvar ' = 0 +1;% ⊦ mklist(boolvar, m) = [] ↔ m = 0;% ⊦ i→n(i) = 0 ↔ i = 0;% ⊦ i * j = 0 ↔ i = 0 ∨ j = 0;% ⊦ i * j * j0 = (i * j) * j0;% ⊦ i * j = j * i;% ⊦ ¬ m + n < m; Used terms: j % 2 ^ (i * 8)