Proof step 8 from proof int2bits-less-2pot (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  # int2bits(j) < # uint2bits(j), 2 ^ (n→i(# int2bits(j)) - 1) ≤ j, 0 ≤ j ⊦ int2bits(j) = false '

Rule argument

Additional information

Used simplifier rules: int2bits-not-empty: ⊦ int2bits(j) ≠ [];%int2bits-first-02: ⊦ int2bits(j).first ↔ j < 0;%uint2bits-empty: 0 ≤ i ⊦ uint2bits(i) ≠ [];% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ i ≤ j → (¬ ¬ j < i ↔ false);% ⊦ m < n → n ≠ 0; (forward)% ⊦ m + n = n + m;% ⊦ (m + n0) + n1 = m + n0 + n1;% ⊦ m + 1 ≤ n ↔ m < n;%n0 < n ⊦ m + (* n) ≤ m0 + (* n0) ↔ m + (n - n0) ≤ m0;%n ≤ m ⊦ (m - n) + m0 ≤ n0 ↔ m + m0 ≤ n0 + n;% ⊦ ¬ m ≤ n ↔ n < m;% ⊦ m < 1 ↔ m = 0;% ⊦ n -1 = n - 1;% ⊦ i→n(n→i(n)) = n;% ⊦ (bits + bits0) + bits1 = bits + bits0 + bits1;% ⊦ bits + [] = bits;% ⊦ boolvar + bits = boolvar ' + bits;% ⊦ ¬ i < j ↔ j ≤ i;% ⊦ # bits = 1 ↔ bits = bits.first + [];% ⊦ # bits = 0 ↔ bits = [];% ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1);%0 ≤ i ⊦ (* i) < n→i(n) ↔ i→n(i) < n;