| 2 * (i1 * 2 + j1) = (i0 * 4 + j2) + 1, 2 * j1 = i2 + 1, i0 * 4 + j2 < 0, i0 ≤ 0, j2 ≤ 0, i1 * 2 + j1 < 0, i1 ≤ 0, j1 ≤ 0, i0 * 4 + j2 < ~3, abs(j1) < 2, abs(j2) < 4, 4 ≤ abs(i2), abs(j2) < abs(i2) ⊦ j1 = ~1, i1 = i0, i2 = 0 |
Used simplifier rules: lels-02: ⊦ i ≠ j → (i ≤ j ↔ i < j); from specification int-abs%abs-08: ⊦ i < 0 → abs(i) = ~ i; from specification int-abs%neg-13: ⊦ ~ i < j ↔ 0 < j + i; from specification int-abs%numls-02: ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; from specification int-abs%minus-one: ⊦ i < 0 → (~2 < i ↔ i = ~1); from specification int-basic1%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%add-zero-rev: ⊦ 0 + i = i; from specification int-basic2%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%numadd-01: ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; from specification int-abs%zero-ls: ⊦ 0 < i → (i * j < 0 ↔ j < 0); from specification int-mult%zero-gels-03: ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%lsone: ⊦ i < 1 ↔ i ≤ 0; from specification int-abs%abs-zero: ⊦ abs(i) ≤ 0 ↔ i = 0; from specification int-abs Used formulas: j1 = 0