| ¬(2 ≠ 0 ∧ (i - 1) % 2 = 0), 2 * 0 ≤ 2 * 2 ^ (abs(j) - 2) + 2 * (i - 1) / 2, 2 * 2 ^ (abs(j) - 2) + i < 0, 1 < abs(j), 0 ≤ 2 ^ (abs(j) - 2) + (i - 1) / 2, i < 0, 2 ^ (abs(j) - 2) + i < (i - 1) / 2, ∀ i, j0. i→n(j0) < i→n(j) → i + 2 ^ (abs(j0) - 1) < 0 → j0 = 0 ∨ i >> abs(j0) = (i + 1 - 2 ^ abs(j0)) / 2 ^ abs(j0) ⊦ (i - 1) / 2 >> (abs(j) - 1) = (i + 1 - 2 ^ abs(j)) / 2 ^ abs(j), j = 0 |
Used simplifier rules: ⊦ i < j → ¬ j < i;% ⊦ ¬ i ≤ j ↔ j < i;% ⊦ i + j = j + i;% ⊦ i - j = i0 ↔ i = i0 + j;% ⊦ i + j + i0 = (i + j) + i0;% ⊦ i - j < i0 ↔ i < j + i0;% ⊦ i < 1 ↔ i ≤ 0;% ⊦ i < 0 ∧ 0 ≤ j → i ≤ j;% ⊦ i * j + i * j0 = i * (j + j0);% ⊦ i * j * j0 = (i * j) * j0;% ⊦ i * j = j * i;% ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j);% ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j;% ⊦ i ≠ j → (i ≤ j ↔ i < j);% ⊦ i < 0 → abs(i) = ~ i;% ⊦ ~ i < j ↔ 0 < j + i;% ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0;% ⊦ i < 0 → (~2 < i ↔ i = ~1);% ⊦ i < j ∧ j ≤ j0 → i < j0; (forward)% ⊦ j < i ∧ i ≤ 0 → j < 0; (forward)% ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward)% ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward)% ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward)% ⊦ ~1 < i ↔ 0 ≤ i;% ⊦ i + 0 = i;% ⊦ (* i2) * i < i + j0 ↔ (i2 - 1) * i < j0;% ⊦ 1 * i = i;% ⊦ (* i1) * j < j ↔ 0 < (1 - i1) * j;% ⊦ i * ~1 = ~ i;% ⊦ 0 < ~ i ↔ i < 0;% ⊦ i ≤ j → (¬ ¬ j < i ↔ false);%⊦ 0 < j ∧ i < 0 → ( i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ abs(j0) < j ∧ i0 ≤ 0); (elim) Used terms: i - 1, 2, i0, j1