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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 225:

  8 * (i→n(i) - 1 - m) = 0, i→n(i * 8) % 8 = 0, # int2bits(j % 2 ^ (i * 8)) = m * 8 + n, 0 ≤ bytes2int(bits2bytes(int2bits(j % 2 ^ (i * 8)))), m * 8 + n < i→n(i * 8), 0 < i, 2 ^ (i * 8) ≤ j, 0 ≤ j % 2 ^ (i * 8), m < i→n(i), n < 8 ⊦ n = 0, mklist(false, 8 - n) + int2bits(j % 2 ^ (i * 8)) = [], i→n(i * 8) + 1 = m * 8 + n, m * 8 + n = i→n(i * 8), i = 0, bits2bytes(mklist(false, 8 - n) + int2bits(j % 2 ^ (i * 8))) = mklist(i2b(0), i→n(i) - m + 1) + bits2bytes(int2bits(j % 2 ^ (i * 8)))

Rule argument

Additional information

Used simplifier rules: ⊦ [] + bits = bits;% ⊦ mklist(boolvar, 0) = [];% ⊦ m * n = n * m;% ⊦ m0 * m * n = (m0 * m) * n;%n ≠ 0 ⊦ (m + n0 * n) % n = m % n;% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ n < m → (m - n) + n = m;% ⊦ n < m → m - n ≠ 0;% ⊦ ¬ bits + bits0 ≠ [] ↔ bits = [] ∧ bits0 = [];% ⊦ mklist(boolvar, m) = [] ↔ m = 0;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ # mklist(boolvar, n) = n;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ n -1 = n - 1;% ⊦ i * j = j * i;