Proof step 46 from proof bitsand-cast-05 (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 47:

  ⊦ # bits1 ≤ # bits0 ∧ bits1 ≠ [] ∧ ¬ bits1.first → bitsand(bits + bits0, bits1) = bitsand(bits0, bits1)

• Proof step 48:

  ¬(# bits ≤ # bits1 ∧ bits ≠ [] ∧ ¬ bits.first), # bits = # bits1 ⊦ bits1 = [], sgn(bitsand(false ' + bits1, bits)) = sgn(false ' + bitsand(bits, bits1)), bits = []

• Proof step 53:

  # bits ≤ # bits1 ∧ bits ≠ [] ∧ ¬ bits.first, # bits = # bits1 ⊦ bits1 = [], sgn(bitsand(bits1, bits)) = sgn(false ' + bitsand(bits, bits1)), bits = []

Rule argument

Additional information

Used terms: bits, bits1, false '