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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 43:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i + j = j + i;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0;% ⊦ i→n(i) = 0 ↔ i = 0;% ⊦ m < n → n ≠ 0; (forward)% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ int2bits(j) ≠ [];% ⊦ mklist(boolvar, m) = [] ↔ m = 0;% ⊦ ¬ bits + bits0 ≠ [] ↔ bits = [] ∧ bits0 = [];% ⊦ n -1 = n - 1;% ⊦ m ≠ n → (m ≤ n ↔ m < n);% ⊦ m ≤ n → (n - m = 0 ↔ n = m);% ⊦ i * j = j * i;