| ¬ 2 ^ (n→i(n) - 1) + j < 0 ∧ ¬ 0 ≤ j + 2 ^ (n→i(n) - 2), j < 0 ⊦ # int2bits(j) = n, n = 1, n = 0 |
0 ≤ 2 ^ (n→i(n) - 1) + j, j + 2 ^ (n→i(n) - 2) < 0, j < 0 ⊦ n = 0, n = 1, # int2bits(j) = n
Used simplifier rules: zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%ler: ⊦ m ≤ m; from specification nat%le: ⊦ n→i(m) ≤ n→i(n) ↔ m ≤ n; from specification intnat%succ-02: ⊦ i < j + 1 ↔ i ≤ j; from specification int-abs%numsub: ⊦ (* i) + i0 - (* j) = (i - j) + i0; from specification int-abs%sub-add-01: ⊦ i + (j - i0) = i + j - i0; from specification int-abs%sub-ls: ⊦ i - j < i0 ↔ i < j + i0; from specification int-abs%ls-pos-2pot-01: 0 ≤ j ⊦ 2 ^ j < 2 ^ j0 ↔ j < j0; from specification int-pot%sub-le-01: ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; from specification int-abs%num-n2i-ls-06: 0 ≤ i ⊦ (* i) ≤ n→i(n) ↔ i→n(i) ≤ n; from specification intnat%lels-01: ⊦ ¬ m ≤ n ↔ n < m; from specification nat%twols-01: ⊦ m ≠ 1 → (m < 2 ↔ m = 0); from specification nat-basic1%ls-01: ⊦ i + j < i + i0 ↔ j < i0; from specification int-basic2%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs