Proof step 8 from proof getShort-isi (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ⊦ s2i (i2s (bor (bits2int ( int2bits(b2i(byi)) + mklist (false, i→n(bits2int(bitsand((((false ' + true ') + false ') + false ') + false ', ((((false ' + true ') + true ') + true ') + true ') + true '))))), band(b2i(byj), 255)))) = bor (bits2int ( int2bits(b2i(byi)) + mklist (false, i→n(bits2int(bitsand((((false ' + true ') + false ') + false ') + false ', ((((false ' + true ') + true ') + true ') + true ') + true '))))), band(b2i(byj), 255)), ¬ bor (bits2int ( int2bits(b2i(byi)) + mklist (false, i→n (bits2int(bitsand((((false ' + true ') + false ') + false ') + false ', ((((false ' + true ') + true ') + true ') + true ') + true '))))), band(b2i(byj), 255)) < ~32768 ∧ ¬ 32767 < bor (bits2int ( int2bits(b2i(byi)) + mklist (false, i→n (bits2int(bitsand((((false ' + true ') + false ') + false ') + false ', ((((false ' + true ') + true ') + true ') + true ') + true '))))), band(b2i(byj), 255))

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ i < j ↔ j ≤ i;% ⊦ band(i, j) = band(j, i);% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ bits + boolvar = bits + boolvar ';% ⊦ boolvar + boolvar0 = boolvar ' + boolvar0 ';% ⊦ uint2bits(1) = false + true;%1 < i ⊦ uint2bits((* i)) = uint2bits(i / 2) + (i % 2 = 1);%0 ≤ i ⊦ int2bits((* i)) = uint2bits(i);