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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 126:

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

Rule argument

Additional information

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