Proof step 83 from proof uint2bits-mod2pot (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 84:

  uint2bits(i1 % 2 ^ i0) = sgn(false ' + lastn(i→n(i0), uint2bits(i1).rest)), mklist(false, # lastn(i→n(i0), uint2bits(i1).rest)) = lastn(i→n(i0), uint2bits(i1).rest), 0 < i1 % 2 ^ i0, 0 ≤ i1, 0 < i0, 0 < i1, 2 ^ i0 < i1, # uint2bits(i1) ≤ i→n(i0), ∀ j0, i. i→n(j0) < i→n(i1 * 2 + 0) → 0 ≤ i ∧ 2 ^ i < j0 → uint2bits(j0 % 2 ^ i) = sgn(false ' + lastn(i→n(i), uint2bits(j0).rest)) ⊦ i0 = 0, ~1 = i0

Rule argument

Additional information

Used simplifier rules: uint2bits-empty: 0 ≤ i ⊦ uint2bits(i) ≠ [];% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ ¬ m < n ↔ n ≤ m;% ⊦ m < n + 1 ↔ ¬ n < m;%n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0;% ⊦ ¬ m ≤ n ↔ n < m;% ⊦ m < 1 ↔ m = 0;% ⊦ # bits = 0 ↔ bits = [];% ⊦ n -1 = n - 1;% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ i < j → ¬ j < i;