| j0 * i * i0 = (j0 * i0) * i, j0 * i0 = j2 * i2, all_prime_divisors(i0) = all_prime_divisors(i * i0) -1l i, 0 ≤ j2 * i2, 0 < i, prime(i), prime(j0), j0 < j0 * i * i0, j2 < j2 * i2, prime(j2), 2 ≤ j2 * i2, 2 ≤ j0 * i * i0, 0 < j2 * i2, j0 < j2, j0 ≤ j2, j0 < j2 * i2, ∀ j1. j0 < j1 ∧ j1 < j0 * i * i0 ∧ prime(j1) → ¬ j1 | j0 * i * i0, ∀ j. j2 < j ∧ j < j2 * i2 ∧ prime(j) → ¬ j | j2 * i2, j2 < j0 * i * i0 → ¬ j2 | j0 * i * i0, ∀ j0, i1. i→n(j0) < i→n(i * j2 * i2) → i1 | j0 ∧ prime(i1) ∧ 0 < j0 → all_prime_divisors(j0 / i1) = all_prime_divisors(j0) -1l i1 ⊦ all_prime_divisors(i2) + j2 ' = all_prime_divisors(i0) + j0 ', j0 = 0, prime(j0 * i * i0), prime(j2 * i2) |
Used simplifier rules: forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs%forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs%zero-ge: ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); from specification int-mult%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%zero-gr: ⊦ 0 < i → (0 < i * j ↔ 0 < j); from specification int-mult%div-mult: ⊦ i | i * j; from specification int-gcd%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs%forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs%ls-same: ⊦ 0 < i → (i * j < i ↔ j < 1); from specification int-mult%lsone: ⊦ i < 1 ↔ i ≤ 0; from specification int-abs%lels-03: ⊦ i < j → (¬ ¬ j ≤ i ↔ false); from specification int-abs