Proof step 2 from proof and-true (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 3:

  ⊦ 1 < # bits ∧ 1 < # bits0 → bitsand(bits, bits0) = bitsand(bits.butlast, bits0.butlast) + (bits.last ∧ bits0.last)

• Proof step 4:

  ¬(1 < # bits ∧ 1 < # bits0), bitsand(bits, bits0) = true ' ⊦ bits0 = [], bits = [], bits = bitsand(bits, bits0) ∧ bits0 = bitsand(bits, bits0)

• Proof step 22:

  1 < # bits ∧ 1 < # bits0, bitsand(bits.butlast, bits0.butlast) + (bits.last ∧ bits0.last) = true ' ⊦ bits0 = [], bits = [], bits = bitsand(bits.butlast, bits0.butlast) + (bits.last ∧ bits0.last) ∧ bits0 = bitsand(bits.butlast, bits0.butlast) + (bits.last ∧ bits0.last)

Rule argument

Additional information

Used terms: bits0, bits