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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  2 < i, 0 < i ⊦ i = 0, (sgn(bitsxor(int2bits(i).butlast, false ') + (¬ int2bits(i).last)')[# int2bits(i) - 1] ↔ ¬ int2bits(i).last) ∧ sgn(bitsxor(int2bits(i).butlast, false ') + (¬ int2bits(i).last)')[# int2bits(i) - 1, int2bits(i).last] = int2bits(i)

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ bits + bits0 ≠ [] ↔ bits = [] ∧ bits0 = [];% ⊦ boolvar ' ≠ [];%bits ≠ [] ⊦ int2bits(bits2int(bits)) = sgn(bits);% ⊦ bits + boolvar ' ≠ [];% ⊦ bits + boolvar = bits + boolvar ';% ⊦ (bits + boolvar ').last ↔ boolvar;% ⊦ (bits + boolvar ').butlast = bits;% ⊦ i ≠ j → (i ≤ j ↔ i < j);% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ # boolvar ' = 0 +1;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ 0 ≤ i → (# int2bits(i) = 1 ↔ i = 0);% ⊦ int2bits(j) ≠ [];% ⊦ # bits = 0 ↔ bits = [];% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1);