Proof step 16 from proof short-law-righthift-not (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  ⊦ (i = 32768 ∧ j = 1 → i2s(16384) ≠ i2s((# int2bits(~32768) ≤ 1 ⊃ ~1;bits2int(sublist(0, # int2bits(~32768) - 1, int2bits(~32768)))))) ∧ ( i = 32768 ∧ j = 1 → i2s (bits2int (sublist (0, # fillsgn (32, ( ( ( ( ( ( (((((((((false ' + true ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false '), false ' + fillsgn (32, ( ( ( ( ( ( (((((((((false ' + true ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ') + false ')))) ≠ i2s(bits2int(sublist(0, # fillsgn(32, int2bits(~32768)), false ' + fillsgn(32, int2bits(~32768))))))

Rule argument

Additional information

Used simplifier rules: ⊦ bits2uint(true ') = 1;% ⊦ bits2uint(bits + false ') = bits2uint(bits) * 2;% ⊦ bits2int(false ' + bits) = bits2uint(bits);% ⊦ bits + [] = bits;% ⊦ sublist(0, 0, bits) = [];%n ≠ 0 ⊦ sublist(0, (* n), boolvar ' + bits) = boolvar ' + sublist(0, n -1, bits);% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ # boolvar ' = 0 +1;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ bits + boolvar = bits + boolvar ';% ⊦ boolvar + boolvar0 = boolvar ' + boolvar0 ';% ⊦ uint2bits(1) = false + true;%1 < i ⊦ uint2bits((* i)) = uint2bits(i / 2) + (i % 2 = 1);