Proof step 35 from proof band-011x-pos (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  0 < j, 0 ≤ j, 0 < i, ∀ j0, i. i→n(j0) < i→n(j) → 0 ≤ j0 ∧ 0 ≤ j0 ∧ 0 ≤ i → bits2int(bitsand(false ' + mklist(true, i→n(i)), uint2bits(j0))) = j0 % 2 ^ i ⊦ j = 1, i = 0, bits2int(bitsand((false ' + mklist(true, i→n(i))).butlast, uint2bits(j / 2)) + (j % 2 = 1 ∧ (false ' + mklist(true, i→n(i))).last)') = j % 2 ^ i

Rule argument

Additional information

Used simplifier rules: ⊦ bits + [] = bits;% ⊦ boolvar + bits = boolvar ' + bits;% ⊦ # bits = 1 ↔ bits = bits.first + [];%0 ≤ i ⊦ uint2bits(i) ≠ [];% ⊦ 0 ≤ i / 2 ↔ ~1 ≤ i;% ⊦ ¬ i < j ↔ j ≤ i;% ⊦ i < j ∧ ¬ i0 < j → ¬ i0 < i;% ⊦ # bits = 0 ↔ bits = [];% ⊦ i→n(i) = 0 ↔ i = 0;%0 ≤ i ⊦ i→n(i) = (* m) ↔ i = n→i(m);% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ i < j → ¬ j < i;% ⊦ m + n = 1 ↔ m = 0 ∧ n = 1 ∨ n = 0 ∧ m = 1;% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m + 1 ≠ 0;% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1);% ⊦ # mklist(boolvar, n) = n;% ⊦ # boolvar ' = 0 +1;% ⊦ #(bits + bits0) = # bits + # bits0;% ⊦ bits + boolvar = bits + boolvar ';% ⊦ (bits + boolvar ').last ↔ boolvar;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ (bits + boolvar ').butlast = bits;