Proof step 15 from proof int2bits-leneq-neg (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  2 < # int2bits(j), # int2bits(j) ≤ i→n(n→i(# int2bits(j)) - 2) + 1, j < 0, j < ~1 ⊦ # int2bits(j) = 1, # int2bits(j) = 3, # int2bits(j) = 2

Rule argument

Additional information

Used simplifier rules: int2bits-not-empty: ⊦ int2bits(j) ≠ [];%num-i2n-eq: 0 ≤ i ⊦ i→n(i) = (* m) ↔ i = n→i(m); from specification intnat%num-n2i-eq: 0 ≤ i ⊦ n→i(n) = (* i) ↔ n = i→n(i); from specification intnat%sub-eq: ⊦ i - j = i0 ↔ i = i0 + j; from specification int-abs%abs-zero: ⊦ i→n(i) = 0 ↔ i = 0; from specification intnat%one: ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); from specification nat-basic1%l-num-04: n0 < n ⊦ (* n) < m0 + (* n0) ↔ n - n0 < m0; from specification nat%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat%lels-03: ⊦ m < n → m ≤ n; from specification nat%c: ⊦ m + n = n + m; from specification nat-basic2%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%num-n2i-ls-02: 0 ≤ i ⊦ (* i) < n→i(n) ↔ i→n(i) < n; from specification intnat%sub-ls-01: ⊦ i < j - i0 ↔ i + i0 < j; from specification int-abs%leone: ⊦ 1 ≤ i ↔ 0 < i; from specification int-abs%num-i2n-le-02: 0 ≤ i ⊦ (* m) ≤ i→n(i) ↔ n→i(m) ≤ i; from specification intnat%lels-01: ⊦ ¬ m ≤ n ↔ n < m; from specification nat%twols-01: ⊦ m ≠ 1 → (m < 2 ↔ m = 0); from specification nat-basic1%le-num-04: n0 < n ⊦ (* n) ≤ m0 + (* n0) ↔ n - n0 ≤ m0; from specification nat%l: ⊦ # bits = 0 ↔ bits = []; from specification list-data[bitlista]%let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat%not-zero: 0 < n ⊦ (* n) ≤ m → m ≠ 0; (forward) from specification nat%num-n2i-ls-06: 0 ≤ i ⊦ (* i) ≤ n→i(n) ↔ i→n(i) ≤ n; from specification intnat%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%sub-le-01: ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; from specification int-abs