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

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 222:

  ⊦ bits ≠ [] ∧ n ≠ 0 ∧ # bits ≤ 8 * n → fix(n, bits2bytes(bits)) = bits2bytes(fillsgn(n * 8, bits))

• Proof step 223:

  int2bits(j % 2 ^ (i * 8)) ≠ [] ∧ i→n(i) + 1 ≠ 0 ∧ # int2bits(j % 2 ^ (i * 8)) ≤ 8 * (i→n(i) + 1), # int2bits(j % 2 ^ (i * 8)) < 8 * i→n(i), j + 2 ^ (i * 8 - 1) < 0, j + 2 ^ (i * 8) ≤ 0, j + 2 ^ (i * 8) < i, j % 2 ^ (i * 8) < 0, 0 < i ⊦ 1 + 8 * i→n(i) = # int2bits(j % 2 ^ (i * 8)), mklist(true, 8 * i→n(i) - # int2bits(j % 2 ^ (i * 8))) + int2bits(j % 2 ^ (i * 8)) = [], j % 2 ^ (i * 8) = 0, bits2bytes(mklist(true, 8 * i→n(i) - # int2bits(j % 2 ^ (i * 8))) + int2bits(j % 2 ^ (i * 8))) = bits2bytes(fillsgn((i→n(i) + 1) * 8, int2bits(j % 2 ^ (i * 8)))).rest, i = 0

Rule argument

Additional information

Used simplifier rules: ⊦ m * n = n * m;% ⊦ i * j = j * i;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i + j = j + i;% ⊦ int2bits(j) ≠ [];% ⊦ m + 1 ≠ 0;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m + n = n + m;% ⊦ m * (n + 1) = m * n + m;% ⊦ m0 * m * n = (m0 * m) * n;% ⊦ ¬ m ≤ n ↔ n < m;% ⊦ n < n0 ∧ n0 < n1 → n +1 < n1; (forward)% ⊦ m < n → n ≠ 0; (forward)% ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward)% ⊦ # bits = 0 ↔ bits = [];% ⊦ m +1 = m + 1;% ⊦ ¬ m + n < m; Used terms: int2bits(j % 2 ^ (i * 8)), i→n(i) + 1