Proof step 41 from proof byte-law-righthift-not (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 42:

  # int2bits(128) = 1 + n, # int2bits(~128) = 1 + n0, i2b(bits2int(sublist(0, n, int2bits(128)))) = i2b(bits2int(sublist(0, n0, int2bits(~128)))) ⊦ n = 0, n0 = 0

Rule argument

Additional information

Used simplifier rules: ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1;% ⊦ 0 ≤ i → (# int2bits(i) = 1 ↔ i = 0);% ⊦ int2bits(j) ≠ [];% ⊦ # bits = 0 ↔ bits = [];% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1);% ⊦ bits2uint(true ') = 1;% ⊦ bits2int(false ' + bits) = bits2uint(bits);% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ bitsand(false ', bits + boolvar ') = false ';%⊦ bitsand(boolvar ' + boolvar0 ', bits0 + boolvar1 ' + boolvar2 ') = bitsand(boolvar ', bits0 + boolvar1 ') + (boolvar0 ∧ boolvar2);% ⊦ bits + boolvar = bits + boolvar ';% ⊦ boolvar + boolvar0 = boolvar ' + boolvar0 ';% ⊦ uint2bits(1) = false + true;%1 < i ⊦ uint2bits((* i)) = uint2bits(i / 2) + (i % 2 = 1);