| 2 * i = j * j + j0, 0 < j, (2 * i) ^ j < ((j + 1) * (j + 1)) ^ j, 0 < i, 2 * i < (j + 1) * (j + 1), 4 ^ (j / 6) < (j + 1) * (j + 1), sqrt(2 * 1024) ≤ j, 0 ≤ (j + 1) * (j + 1), 0 ≤ 4 ^ (j / 6), (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), (j ^ 2 / 2) / 3 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, j0 ≤ 2 * j, 1024 ≤ i, 4 ^ (i / 3) ≤ (2 * i) ^ j, 0 ≤ i, j ^ 2 ≤ 2 * i, j / 6 * j ≤ (j ^ 2 / 2) / 3, 0 ≤ j / 6, 0 ≤ j, 2 * 1024 ≤ 2 * i ⊦ 36 ≤ j |
2 * i = j * j + j0, sqrt(2048) < 36, 0 < (j + 1) * (j + 1), 4 ^ (i / 3) < ((j + 1) * (j + 1)) ^ j, j ^ 2 < (j + 1) * (j + 1), j < 36, 0 < j, (2 * i) ^ j < ((j + 1) * (j + 1)) ^ j, 0 < i, 2 * i < (j + 1) * (j + 1), 4 ^ (j / 6) < (j + 1) * (j + 1), (4 ^ (j / 6)) ^ j < ((j + 1) * (j + 1)) ^ j, (4 ^ (j / 6)) ^ j ≤ (2 * i) ^ j, j / 6 * j ≤ i / 3, sqrt(2048) ≤ j, 0 ≤ 4 ^ (j / 6), (4 ^ (j / 6)) ^ j ≤ 4 ^ (i / 3), j ^ 2 / 6 ≤ i / 3, j ^ 2 / 2 ≤ i, 0 ≤ j0, j0 ≤ 2 * j, 4 ^ (i / 3) ≤ (2 * i) ^ j, 0 ≤ i, j ^ 2 ≤ 2 * i, j / 6 * j ≤ j ^ 2 / 6, 0 ≤ j, 1024 ≤ i ⊦
Used simplifier rules: ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s)% ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s)%forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1% ⊦ i ≤ j ↔ ¬ j < i; (ss)% ⊦ 0 ≤ i * i; (s)%i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s)%j ≠ 0, j0 ≠ 0 ⊦ (i / (* j)) / (* j0) = i / (j * j0); (s)% ⊦ 0 < j ∧ 0 ≤ i → 0 ≤ i / j; (s)%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2% ⊦ 0 < i ∧ 0 ≤ j → ((* j) ≤ (* i) * i0 ↔ (i + j - 1) / i ≤ i0); (s)%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult