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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 138:

  int2bits(i) = (bits1 + boolvar ') + bits, # bits = i→n(j), bitsxor(int2bits(i), (false ' + true ') + mklist(false, i→n(j))) = (bits1 + (¬ boolvar)') + bitsxor(bits, mklist(false, i→n(j))), 2 ^ j * 2 < i, 0 ≤ i, 0 ≤ j ⊦ bits = [], bits1 = [], bits1.first ↔ ¬ (bits1.rest + (¬ boolvar)').first, (sgn((bits1 + (¬ boolvar)') + bitsxor(bits, mklist(false, i→n(j))))[# bits1] ↔ ¬ boolvar) ∧ sgn((bits1 + (¬ boolvar)') + bitsxor(bits, mklist(false, i→n(j))))[# bits1, boolvar] = int2bits(i)

Rule argument

Additional information

Used simplifier rules: ⊦ # bits = 0 ↔ bits = [];% ⊦ m + n = 0 ↔ m = 0 ∧ n = 0;% ⊦ 1 = m + 1 ↔ m = 0;% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m + 1 ≠ 0;% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1);% ⊦ # boolvar ' = 0 +1;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ (bits + boolvar ' + bits0).first ↔ (bits + boolvar ').first;% ⊦ bits ≠ [] → (bits + bits0).rest = bits.rest + bits0;% ⊦ bits ≠ [] → ((bits + bits0).first ↔ bits.first);% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;