Proof step 67 from proof bytes2bytes-zero (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 68:

  b2i(by) = 0, b2i(by0) < 0, ∀ by0, by, bytes1. # bytes1 < #(bytes0 + by1 ') → b2i(by) = 0 ∧ b2i(by0) < 0 → bits2bytes(sgn(byte2bits(by) + byte2bits(by0) + bytes2bits(bytes1))) = by ' + by0 ' + bytes1 ⊦ bits2bytes(sgn(byte2bits(by) + byte2bits(by0) + bytes2bits(bytes0))) + i2b(bits2int(lastn(8, sgn(byte2bits(by) + byte2bits(by0) + bytes2bits(bytes0)) + byte2bits(by1)))) ' = by ' + by0 ' + bytes0 + by1 ', byte2bits(by) + byte2bits(by0) + bytes2bits(bytes0) = [], ¬ true ∈ byte2bits(by) ∧ ¬ true ∈ byte2bits(by0) ∧ ¬ true ∈ bytes2bits(bytes0), ¬ false ∈ byte2bits(by) ∧ ¬ false ∈ byte2bits(by0) ∧ ¬ false ∈ bytes2bits(bytes0)

Rule argument

Additional information

Used simplifier rules: byte2bits-length: ⊦ # byte2bits(by) = 8;% ⊦ 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;