Proof step 8 from proof bits2int-sign (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ bits.first ∧ bits ≠ [] → bits2int(bits) = ~ bits2uint(bitsinvert(true + bits.rest) +1)

• Proof step 10:

  ¬((bits0 + true ' + bits1).first ∧ bits0 + true ' + bits1 ≠ []) ⊦ bits0 = [], bits2uint((false ' + bitsinvert(bits1))+1) + bits2int(bits0 + true ' + bits1) = 0, false ∈ bits0

• Proof step 12:

  (bits0 + true ' + bits1).first ∧ bits0 + true ' + bits1 ≠ [] ⊦ bits0 = [], bits2uint((false ' + bitsinvert(bits1))+1) + ~ bits2uint(bitsinvert(true + (bits0 + true ' + bits1).rest) +1) = 0, false ∈ bits0

Rule argument

Additional information

Used terms: bits0 + true ' + bits1