| 0 ≤ 2 * (i0 + i1) + j0, j0 < i0, j0 ≤ 0, i1 * 2 + j0 < 0, abs(j0) < 2, 0 < i0, 0 ≤ i0, i1 * 2 + j0 < i0 * 2 ⊦ j0 + (2 * (i0 + i1) + j0) % 2 = 0, i1 * 2 + j0 = 0 |
Used simplifier rules: mod-two-02: ⊦ (i * 2) % 2 = 0;%mod-two-03: ⊦ 0 < i → (i * 2 - 1) % 2 = 1;%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%zero-gels-01: ⊦ i < 0 ∧ 0 ≤ j → i < j; from specification int-abs%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs%minus-add: i < 0 ⊦ (* i) + j = j - ~ i; from specification int-abs%sub-eq: ⊦ i - j = i0 ↔ i = i0 + j; from specification int-abs%neq-two: ⊦ 2 * i ≠ 1; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%mone-06: ⊦ ~1 < i ↔ 0 ≤ i; from specification int-abs%sub-le-01: ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; from specification int-abs%leone: ⊦ 1 ≤ i ↔ 0 < i; from specification int-abs%zero-gr: ⊦ 0 < i → (0 < i * j ↔ 0 < j); from specification int-mult%add-zero: ⊦ i + 0 = i; from specification int-basic2 Used formulas: j0 = 0