Proof step 4 from proof fix-rec-neg (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  ¬(#(by ' + bytes0) < n ∧ bytes2int(by ' + bytes0) < 0), 1 + # bytes0 < n, b2i(by) < 0 ⊦ fix(n, by ' + bytes0) = i2b(~1) ' + fix(n - 1, by ' + bytes0)

• Proof step 9:

  #(by ' + bytes0) < n ∧ bytes2int(by ' + bytes0) < 0, 1 + # bytes0 < n, b2i(by) < 0 ⊦ mklist(i2b(~1), n - #(by ' + bytes0)) + by ' + bytes0 = i2b(~1) ' + fix(n - 1, by ' + bytes0)

Rule argument

Additional information

Used terms: by ' + bytes0, n