Proof step 70 from proof band-min (previous step)

User applied rule insert elim lemma

And obtained the following new goals

• Proof step 71:

  i = i4 * 2 + j2 ∧ j2 ≤ 0 ∧ abs(j2) < 2 ∧ i4 ≤ 0 ∧ 0 < 2, # int2bits(i3) = # int2bits(i2), ~1 = ((i3 * 2 + j0) + 1) % 2, ~1 = ((i2 * 2 + j1) + 1) % 2, abs(j1) < 2, abs(j0) < 2, i3 * 2 + j0 < ~1, i2 * 2 + j1 < ~1, bits2int(bitsand(int2bits(i3), int2bits(i2))) < i4, j0 ≤ 0, i3 ≤ 0, i3 * 2 + j0 < 0, j1 ≤ 0, i2 ≤ 0, i2 * 2 + j1 < 0, 2 ^ (n→i(# int2bits(i2)) + 1) + i < 0, i < 0, j0 < i4 + 2 ^ n→i(# int2bits(i2)), i3 < i4 + 2 ^ n→i(# int2bits(i2)), j1 < i4 + 2 ^ n→i(# int2bits(i2)), i2 < i4 + 2 ^ n→i(# int2bits(i2)), 0 < i4 + 2 ^ n→i(# int2bits(i2)), ∀ i0, j, i1. i→n(i1) < i→n((i3 * 2 + j0) + 1) → # int2bits(i1) = # int2bits(j) ∧ bits2int(bitsand(int2bits(i1), int2bits(j))) < i0 ∧ i1 ≤ 0 ∧ j ≤ 0 ∧ i0 + 2 ^ n→i(# int2bits(j)) ≤ 0 → false ⊦ ~2 = i3 * 2 + j0, ~2 = i2 * 2 + j1

Rule argument

Additional information

Used simplifier rules: ⊦ i + j + i0 = (i + j) + i0;% ⊦ i + j = j + i;% ⊦ ¬ i < j ↔ j ≤ i;% ⊦ i < j → (¬ ¬ j ≤ i ↔ false);%⊦ 0 < j ∧ i < 0 → ( i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ abs(j0) < j ∧ i0 ≤ 0); (elim) Used terms: i, 2, i4, j2