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

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 319:

  ⊦ ¬ true ∈ bits ∧ (# bits0 < # bits ∧ ¬ bits0.first) ∧ bits ≠ [] ∧ bits0 ≠ [] → bitsand(bits, bits0) = mklist(false, # bits0)

• Proof step 320:

  ¬(¬ true ∈ bits ∧ # bits0 < # bits ∧ ¬ bits0.first ∧ bits ≠ [] ∧ bits0 ≠ []), n = # fillsgn(n, bits), # bits < n ⊦ bits = [], bits0 = [], mklist(false, n) = lastn(n, fillsgn(n, bitsand(bits, bits0))), true ∈ bits

• Proof step 347:

  ¬ true ∈ bits ∧ # bits0 < # bits ∧ ¬ bits0.first ∧ bits ≠ [] ∧ bits0 ≠ [], n = # fillsgn(n, bits), # bits < n ⊦ bits = [], bits0 = [], mklist(false, n) = lastn(n, fillsgn(n, mklist(false, # bits0))), true ∈ bits

Rule argument

Additional information

Used terms: bits0, bits