Proof step 129 from proof bxor-flip-one-bit (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 130:

  int2bits(i) = bits0 + bits, # bits = i→n(j), bitsxor(bits0 + bits, (false ' + true ') + mklist(false, i→n(j))) = (bitsxor(bits0.butlast, false ') + (¬ bits0.last)') + bitsxor(bits, mklist(false, i→n(j))), 2 ^ j * 2 < i, 0 ≤ i, 0 ≤ j ⊦ bits0 = [], bits = [], # bits0 = 1, (sgn(bitsxor(bits0 + bits, (false ' + true ') + mklist(false, i→n(j))))[# bits0 - 1] ↔ ¬ bits0.last) ∧ sgn(bitsxor(bits0 + bits, (false ' + true ') + mklist(false, i→n(j))))[# bits0 - 1, bits0.last] = bits0 + bits

Rule argument

Additional information

Used simplifier rules: ⊦ # boolvar ' = 0 +1;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ # bits = 0 ↔ bits = [];% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1);% ⊦ bits + boolvar ' + bits0 ≠ [];% ⊦ bits + boolvar = bits + boolvar ';% ⊦ (bits + boolvar ').last ↔ boolvar;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ (bits + boolvar ').butlast = bits;