Proof step 30 from proof bits2int-lasteq (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 31:

  ⊦ boolvar ∧ bits.first ∧ bits ≠ [] → bits2int(bits + boolvar ') = ~(bits2uint(bitsinvert(bits.rest)) * 2 + 1)

• Proof step 32:

  ¬(true ∧ bits0.first ∧ bits0 ≠ []) ⊦ bits0 = [], ~1 = 2 * bits2uint(bitsinvert(bits1)) + bits2int(bits0 + true ') ↔ ~1 = bits2int(bits0) + bits2uint(bitsinvert(bits1))

• Proof step 34:

  true ∧ bits0.first ∧ bits0 ≠ [] ⊦ bits0 = [], ~1 = 2 * bits2uint(bitsinvert(bits1)) + ~(bits2uint(bitsinvert(bits0.rest)) * 2 + 1) ↔ ~1 = bits2int(bits0) + bits2uint(bitsinvert(bits1))

Rule argument

Additional information

Used terms: true, bits0