Proof step 4 from proof sgn-in-01 (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 ≠ [] ∧ (bits0.first ↔ boolvar)), ∀ boolvar. boolvar ∈ sgn(bits0) ↔ boolvar ∈ bits0 ⊦ boolvar0 ∈ sgn(boolvar ' + bits0) ↔ (boolvar0 ↔ boolvar) ∨ boolvar0 ∈ bits0, bits0 = []

• Proof step 10:

  bits0 ≠ [] ∧ (bits0.first ↔ boolvar), ∀ boolvar. boolvar ∈ sgn(bits0) ↔ boolvar ∈ bits0 ⊦ boolvar0 ∈ sgn(bits0) ↔ (boolvar0 ↔ boolvar) ∨ boolvar0 ∈ bits0, bits0 = []

Rule argument

Additional information

Used terms: bits0, boolvar