| 0 < i + 1, 0 ≤ i, 2 ^ i ≤ i0, i0 < 2 ^ (i + 1)-1 * 2, 0 < i0 * 2 + j1, 2 ^ i < 2 ^ (i + 1)-1 * 2, 0 ≤ j1, j1 < 2, 0 ≤ i0, 0 < 2 ^ (i + 1)-1 * 2, ∀ j0. i→n(j0) < i→n(i0 * 2 + j1) → 0 < j0 → (∃ i. 0 ≤ i ∧ 2 ^ i ≤ j0 ∧ j0 < 2 ^ (i + 1)) ⊦ i0 * 2 + j1 = 1, i0 * 2 + j1 = 0, 0 ≤ i + 1 ∧ 2 ^ (i + 1)-1 * 2 ≤ i0 * 2 + j1 ∧ i0 * 2 + j1 < 2 ^ (2 + i) |
0 < i0, 0 < 2 ^ i, 0 < i0 * 2 + j1, i0 < 2 ^ i * 2, 2 ^ i ≤ i0, 0 ≤ i, 0 ≤ i0, j1 < 2, 0 ≤ j1, 1 < 2 ^ i * 2, ∀ j0. i→n(j0) < i→n(i0 * 2 + j1) → 0 < j0 → (∃ i. 0 ≤ i ∧ 2 ^ i ≤ j0 ∧ j0 < 2 ^ (i + 1)) ⊦ i0 * 2 + j1 = 0, i0 * 2 + j1 = 1, 0 ≤ i + 1 ∧ 2 ^ i * 2 ≤ i0 * 2 + j1 ∧ i0 * 2 + j1 < 2 ^ (2 + i)
Used simplifier rules: lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1%ls-same-01: ⊦ 0 < i → (i < i * j ↔ 1 < j); from specification int-mult%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%zero-gr: ⊦ 0 < i → (0 < i * j ↔ 0 < j); from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%one: ⊦ 1 * i = i; from specification int-mult%numls-09: ⊦ j < (* i1) * j ↔ 0 < (i1 - 1) * j; from specification int-mult%pred: ⊦ (i + 1)-1 = i; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%mone-06: ⊦ ~1 < i ↔ 0 ≤ i; from specification int-abs%numls-02: ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; from specification int-abs