Proof step 61 from proof bytes2bytes-mone (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 62:

  b2i(bytes0.first) = ~1, 0 ≤ b2i((bytes0.rest + by ').first), false ∈ bytes2bits(bytes0), true ∈ bytes2bits(bytes0), ∀ bytes1. # bytes1 < #(bytes0 + by ') → b2i(bytes1.first) = ~1 ∧ 0 ≤ b2i(bytes1.rest.first) → bits2bytes(sgn(bytes2bits(bytes1))) = bytes1 ∨ # bytes1 = 1 ∨ bytes1 = [] ⊦ bytes0 = [], bits2bytes(sgn(bytes2bits(bytes0))) + i2b(bits2int(lastn(8, sgn(bytes2bits(bytes0)) + byte2bits(by)))) ' = bytes0 + by '

Rule argument

Additional information

Used simplifier rules: byte2bits-length: ⊦ # byte2bits(by) = 8;%bytes2bits-empty-01: ⊦ bytes2bits(bytes) = [] ↔ bytes = [];% ⊦ sgn(bits) = [] ↔ bits = [];% ⊦ # bits = 0 ↔ bits = [];% ⊦ m < m + n ↔ n ≠ 0;% ⊦ bytes + by = bytes + by ';% ⊦ firstn(# bits, bits + bits0) = bits;% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ 0 + m = m;% ⊦ n ≤ m → m + n0 - n = (m - n) + n0;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ #(bits + bits0) = # bits + # bits0;