Proof step 102 from proof int2bytes-rec-pos-any (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 103:

  i→n(i) + 1 = # bits2bytes(restn(i→n(i * 8) % 8, int2bits(j % 2 ^ (i * 8)).rest)) + # bits2bytes((j % 2 ^ (i * 8) < 0)' + firstn(i→n(i * 8) % 8, int2bits(j % 2 ^ (i * 8)).rest)), # int2bits(j % 2 ^ (i * 8)).rest % 8 = 0, # int2bits(j % 2 ^ (i * 8)) = i→n(i * 8) + 1, 2 ^ (i * 8) ≤ j, 0 < i ⊦ bits2bytes(int2bits(j % 2 ^ (i * 8)).rest) = ( bits2bytes((¬ 0 ≤ j % 2 ^ (i * 8))' + firstn(i→n(i * 8) % 8, int2bits(j % 2 ^ (i * 8)).rest)) + bits2bytes(restn(i→n(i * 8) % 8, int2bits(j % 2 ^ (i * 8)).rest)) ).rest, (i→n(i * 8) + 1) % 8 = 0, int2bits(j % 2 ^ (i * 8)).rest = []

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < i ∧ 0 ≤ j → ((* j) < (* i) * i0 ↔ j / i < i0);%0 ≤ i ⊦ (* m) < i→n(i) ↔ n→i(m) < i;% ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j);% ⊦ i * j * j0 = (i * j) * j0;%n0 < n ⊦ (* n) < m0 + (* n0) ↔ n - n0 < m0;% ⊦ ¬ i < j ↔ j ≤ i;% ⊦ m + 1 ≠ 0;% ⊦ boolvar + bits = boolvar ' + bits;% ⊦ int2bits(j).first ↔ j < 0;% ⊦ firstn(n + 1, bits) = bits.first + firstn(n, bits.rest);% ⊦ restn(n + 1, bits) = restn(n, bits.rest);%n ≠ 0 ⊦ (m + 1) % n ≠ 0 → (m + 1) % n = m % n + 1;% ⊦ m < n → n ≠ 0; (forward)% ⊦ m < n ∧ n = n0 → m < n0; (forward)% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ (bytes + bytes0) + bytes1 = bytes + bytes0 + bytes1;% ⊦ #(bytes + bytes0) = # bytes + # bytes0;% ⊦ i * j = j * i;