Proof step 4 from proof bitsinvert-size (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 5:

  bits ≠ [], bits.first ↔ boolvar ⊦ sgn(boolvar ' + bits) = sgn(bits)

• Proof step 6:

  ¬(bitsinvert(bits0) ≠ [] ∧ (bitsinvert(bits0).first ↔ ¬ boolvar)), # sgn(bitsinvert(bits0)) = # sgn(bits0) ⊦ # sgn((¬ boolvar)' + bitsinvert(bits0)) = # sgn(boolvar ' + bits0), bits0 = []

• Proof step 20:

  bitsinvert(bits0) ≠ [] ∧ (bitsinvert(bits0).first ↔ ¬ boolvar), # sgn(bitsinvert(bits0)) = # sgn(bits0) ⊦ # sgn(bitsinvert(bits0)) = # sgn(boolvar ' + bits0), bits0 = []

Rule argument

Additional information

Used terms: bitsinvert(bits0), ¬ boolvar