Proof step 4 from proof sgn-zeros (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:

  ¬(bits0 + false ' + bits1 ≠ [] ∧ ((bits0 + false ' + bits1).first ↔ false)), ∀ bits. sgn(bits0 + false ' + bits) = sgn(false ' + bits) ⊦ sgn((false ' + bits0) + false ' + bits1) = sgn(false ' + bits1), true ∈ bits0

• Proof step 8:

  bits0 + false ' + bits1 ≠ [] ∧ ((bits0 + false ' + bits1).first ↔ false), ∀ bits. sgn(bits0 + false ' + bits) = sgn(false ' + bits) ⊦ sgn(bits0 + false ' + bits1) = sgn(false ' + bits1), true ∈ bits0

Rule argument

Additional information

Used simplifier rules: ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1; Used terms: bits0 + false ' + bits1, false