| i0 * 2 = (i + j) + 1, i0 < i, i + j < 0, i0 < j, i ≤ j, i0 ≤ 0 ⊦ |
Used simplifier rules: nummult-eq-01: j ≠ 0, j0 % j = 0 ⊦ i * (* j) = i0 * (* j0) ↔ i = i0 * j0 / j;%nummult-ls: ⊦ 0 < i ∧ 0 ≤ j → ((* i) * i0 < (* j) ↔ i0 < (i + j - 1) / i);% ⊦ i - j = i0 ↔ i = i0 + j; (s)%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2% ⊦ i + (j - i) = j; (s)% ⊦ 1 * i = i; (s)%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult% ⊦ i - j ≤ i0 ↔ i ≤ j + i0; (s)% ⊦ i + i = 2 * i; (s)% ⊦ 2 * i ≤ 2 * j + 1 ↔ i ≤ j; (s)% ⊦ i < j - i0 ↔ i + i0 < j; (s)% ⊦ i + j < (* i1) * i ↔ j < (i1 - 1) * i; (s)% ⊦ i + (j - i0) = i + j - i0; (s)% ⊦ i + j - i + 1 = j - 1; (s)% ⊦ i - j < i0 ↔ i < j + i0; (s)% ⊦ i < 1 ↔ i ≤ 0; (s)% ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s)%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs% ⊦ i + j < j ↔ i < 0; (s) Used formulas: i = i0 * 2 - j + 1