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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 148:

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

Rule argument

Additional information

Used simplifier rules: ⊦ i ≠ j → (i ≤ j ↔ i < j);% ⊦ boolvar ' ≠ [];% ⊦ ¬ bits + bits0 ≠ [] ↔ bits = [] ∧ bits0 = [];% ⊦ boolvar ' = boolvar0 ' + bits ↔ (boolvar ↔ boolvar0) ∧ bits = [];% ⊦ int2bits(0) = false ';% ⊦ 0 ≤ i → (# int2bits(i) = 1 ↔ i = 0);% ⊦ int2bits(j) ≠ [];% ⊦ # bits = 0 ↔ bits = [];% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1);% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ # mklist(boolvar, n) = n;% ⊦ # boolvar ' = 0 +1;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ m + n = n + m;