Proof step 11 from proof bits2bytes-2pot (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  # bits2bytes(true ' + mklist(false, 7 + 8 * m)) = m + 1 ⊦ # bits2bytes(firstn(8 + 8 * m, true ' + mklist(false, 7 + 8 * m) + false ' + false ' + false ' + false ' + false ' + false ' + false ' + false ')) = 1 + m

Rule argument

Additional information

Used simplifier rules: n < n0 ⊦ (* n) < m0 + (* n0);%n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n);% ⊦ (bytes + bytes0) + bytes1 = bytes + bytes0 + bytes1;% ⊦ # by ' = 0 +1;% ⊦ #(bytes + bytes0) = # bytes + # bytes0;% ⊦ bytes + by = bytes + by ';% ⊦ bits2uint(false ') = 0;% ⊦ bits2uint(bits + false ') = bits2uint(bits) * 2;% ⊦ bits2int(false ' + bits) = bits2uint(bits);% ⊦ (boolvar ' + bits + boolvar0 ').last ↔ boolvar0;% ⊦ lastn(1, bits) = bits.last ';%0 < n ⊦ lastn((* n), bits + boolvar ') = lastn(n -1, bits) + boolvar ';% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ n ≤ m → m + n0 - n = (m - n) + n0;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ # mklist(boolvar, n) = n;% ⊦ # boolvar ' = 0 +1;% ⊦ #(bits + bits0) = # bits + # bits0;