| j0 < i0, i1 * 2 + j0 < 0, 0 < i0, i1 * 2 + j0 < i0 * 2, abs(j0) < 2, 0 ≤ 2 * (i0 + i1) + j0, j0 ≤ 0, 0 ≤ i0 ⊦ 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;% ⊦ i ≠ j → (i ≤ j ↔ i < j); (s)% ⊦ i < 0 ∧ 0 ≤ j → i < j; (s)% ⊦ i < 0 → abs(i) = ~ i; (s)% ⊦ ~ i < j ↔ 0 < j + i; (s)% ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s)% ⊦ i < 0 → (~2 < i ↔ i = ~1); (s)%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%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%i < 0 ⊦ (* i) + j = j - ~ i; (s)% ⊦ i - j = i0 ↔ i = i0 + j; (s)% ⊦ 2 * i ≠ 1; (s)%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult% ⊦ ~1 < i ↔ 0 ≤ i; (s)% ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; (s)% ⊦ 1 ≤ i ↔ 0 < i; (s)% ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s)% ⊦ i + 0 = i; (s) Used formulas: j0 = 0