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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 320:

  i→n(i * 8) % 8 = 0, # int2bits(j % 2 ^ (i * 8)) = m * 8 + n, m * 8 + n < i→n(i * 8), 2 ^ (i * 8) ≤ j, 0 ≤ j % 2 ^ (i * 8), m < i→n(i), n < 8, n < m * 8 + 7, n < 8 + m * 8, 8 < m * 8 + n, 0 ≤ bytes2int(bits2bytes(firstn(n, int2bits(j % 2 ^ (i * 8)))) + bits2bytes(restn(n, int2bits(j % 2 ^ (i * 8))))), 1 < i, 0 < i ⊦ mklist(false, 8 - n) + int2bits(j % 2 ^ (i * 8)) = [], i→n(i) - m + 1 = 0, mklist(false, 8 * (i→n(i) - m + 1)) + 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, m = 0, n = 0, bits2bytes(firstn(8, mklist(false, 8 - n) + int2bits(j % 2 ^ (i * 8)))) + bits2bytes(restn(8, mklist(false, 8 - n) + int2bits(j % 2 ^ (i * 8)))) = bits2bytes(firstn(n, int2bits(j % 2 ^ (i * 8)))) + bits2bytes(restn(n, int2bits(j % 2 ^ (i * 8)))), m * 8 = 1

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward)%i0 ≠ 0, i0 ≤ i ⊦ (* i) < j → (* i0) < j;% ⊦ 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;% ⊦ m < m + n ↔ n ≠ 0;% ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0;% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1);% ⊦ m + n < m + n0 ↔ n < n0;% ⊦ m +1 = m + 1;% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m * n = n * m;% ⊦ m0 * m * n = (m0 * m) * n;% ⊦ m < n → m % n = m;%n ≠ 0 ⊦ (m + n0 * n) % n = m % n;% ⊦ m < n → n ≠ 0;% ⊦ m < n → n ≠ 0; (forward)% ⊦ m < n ∧ n = n0 → m < n0; (forward)% ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward)% ⊦ n < n0 ∧ n0 < n1 → n +1 < n1; (forward)% ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward)% ⊦ i * j = j * i;