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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 119:

  # bits = i→n(j), bitsxor(int2bits(i), (false ' + true ') + mklist(false, i→n(j))) = (false ' + true ') + bitsxor(bits, mklist(false, i→n(j))), int2bits(i) = false ' + bits, 0 ≤ j, false ∈ int2bits(i), 2 ^ j * 2 < i, 0 < i ⊦ bits = [], # int2bits(i) = 2 + i→n(j), i = 0

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward)% ⊦ i ≠ j → (i ≤ j ↔ i < j);% ⊦ 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;