Proof step 14 from proof setShort-theorem (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  fillsgn(2, i2b(s2i(sho)) ') = by ' + by0 ' ⊦ by0 = i2b(s2i(sho)) ∧ by = i2b(b2i(i2b(s2i(sho))) >> 8)

Rule argument

Additional information

Used simplifier rules: int2bytes-byte-01: ⊦ int2bytes(b2i(by)) = by ';% ⊦ by ∈ by0 ' ↔ by = by0;% ⊦ by ∈ bytes + bytes0 ↔ ¬ ¬(by ∈ bytes ∨ by ∈ bytes0);% ⊦ by ' + bytes = bytes0 → by ∈ bytes0; (forward)% ⊦ (bytes + bytes0) + bytes1 = bytes + bytes0 + bytes1;% ⊦ bytes + by ' = bytes0 → by ∈ bytes0; (forward)% ⊦ i2b(b2i(by)) = by;