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

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ 1 < # int2bytes(i) ∧ # int2bytes(i) ≤ n → fillsgn(n, int2bytes(i)) = fillsgn(n -1, int2bytes(i >> 8)) + i2b(i)

• Proof step 7:

  ¬(1 < # int2bytes(s2i(sho)) ∧ # int2bytes(s2i(sho)) ≤ 2), fillsgn(2, int2bytes(s2i(sho))) = by ' + by0 ' ⊦ by0 = i2b(s2i(sho)) ∧ by = i2b(s2i(sho) >> 8)

• Proof step 20:

  1 < # int2bytes(s2i(sho)) ∧ # int2bytes(s2i(sho)) ≤ 2, fillsgn(2 -1, int2bytes(s2i(sho) >> 8)) + i2b(s2i(sho)) = by ' + by0 ' ⊦ by0 = i2b(s2i(sho)) ∧ by = i2b(s2i(sho) >> 8)

Rule argument

Additional information

Used terms: s2i(sho), 2