Proof step 19 from proof cast-law-and-one (previous step)

User applied rule insert rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ bits ≠ [] ∧ bits0 ≠ [] → bitsand(bits, bits0) ≠ []

Rule argument

Additional information

Used simplifier rules: ⊦ sgn(bits) = [] ↔ bits = [];% ⊦ lastn(n, bits) = [] ↔ n = 0;% ⊦ i→n(i) = 0 ↔ i = 0;% ⊦ int2bits(j) ≠ [];% ⊦ fillsgn(0, bits) = bits;% ⊦ lastn(0, bits) = [];% ⊦ sgn([]) = []; Used terms: int2bits(j0), sgn(lastn(i→n(i), fillsgn(i→n(i), int2bits(j))))