Proof step 4 from proof bitsand-idempotent (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  ¬(1 < # bits ∧ 1 < # bits), ∀ bits0. # bits0 < # bits → true → bits0 = [] ∨ bitsand(bits0, bits0) = bits0 ⊦ bitsand(bits, bits) = bits, bits = []

• Proof step 9:

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

Rule argument

Additional information

Used terms: bits, bits