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

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

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

• Proof step 28:

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

Rule argument

Additional information

Used terms: bytes, m + 1