Proof step 12 from proof fillsgn-rec (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ # bytes < n ∧ 0 ≤ bytes2int(bytes) → fillsgn(n, bytes) = mklist(i2b(0), n - # bytes) + bytes

• Proof step 14:

  ¬(# bytes < n + # bytes ∧ 0 ≤ bytes2int(bytes)), 0 ≤ bytes2int(bytes) ⊦ bytes = [], mklist(i2b(0), n + 1) + bytes = (¬ 0 ≤ b2i(bytes.first) ⊃ i2b(~1);i2b(0)) ' + fillsgn(n + # bytes, bytes)

• Proof step 20:

  # bytes < n + # bytes ∧ 0 ≤ bytes2int(bytes), 0 ≤ bytes2int(bytes) ⊦ bytes = [], mklist(i2b(0), n + 1) + bytes = (¬ 0 ≤ b2i(bytes.first) ⊃ i2b(~1);i2b(0)) ' + mklist(i2b(0), n + # bytes - # bytes) + bytes

Rule argument

Additional information

Used terms: bytes, n + # bytes