Proof step 965 from proof bitsand-cast (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 966:

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

• Proof step 967:

  ¬(# bits0 ≤ # bits1 ∧ bits0 ≠ [] ∧ ¬ bits0.first) ⊦ bits1 = [], bits2 + bits1 = [], bits0 = [], bits1 = lastn(# bits1, fillsgn(# bits1, bitsand(bits2 + bits1, bits0))), true ∈ bits1

• Proof step 1008:

  # bits0 ≤ # bits1 ∧ bits0 ≠ [] ∧ ¬ bits0.first ⊦ bits1 = [], bits2 + bits1 = [], bits0 = [], bits1 = lastn(# bits1, fillsgn(# bits1, bitsand(bits1, bits0))), true ∈ bits1

Rule argument

Additional information

Used terms: bits0, bits1, bits2