Proof step 35 from proof byte-law-and-one (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  bitsand(lastn(8, fillsgn(8, int2bits(i))), int2bits(j)) = [] ⊦ lastn(8, fillsgn(8, sgn(bitsand(int2bits(i), int2bits(j))))) = ((((((false ' + false ') + false ') + false ') + false ') + false ') + false ') + false '

Rule argument

Additional information

Used simplifier rules: ⊦ lastn(1, boolvar ') = boolvar ';%0 < n ⊦ lastn((* n), bits + boolvar ') = lastn(n -1, bits) + boolvar ';% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ bits + [] = bits;% ⊦ mklist(boolvar, 0) = [];%n ≠ 0 ⊦ mklist(false, (* n)) = false ' + mklist(false, n -1);% ⊦ fillsgn(n, []) = mklist(false, n);% ⊦ sgn([]) = [];