| 1 < i, 0 < i, 0 < j, j < i, prime(i), i | fac(j - 1), 0 < fac(j - 1), ∀ j0, i. i→n(j0) < i→n(j) → prime(i) ∧ j0 < i ∧ 0 < j0 ∧ 0 < i ∧ 1 < i → max_exp(i, fac(j0)) = 0 ⊦ |
Used simplifier rules: fac-zero: ⊦ i ≤ 0 → fac(i) = 1;%max_exp-zero-02: ⊦ prime(i) ∧ 0 < i0 → (max_exp(i, i0) = 0 ↔ ¬ i | i0);%sub-ls: ⊦ i - j < i0 ↔ i < j + i0; from specification int-abs%succ-02: ⊦ i < j + 1 ↔ i ≤ j; from specification int-abs%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%add-c: ⊦ i + j = j + i; from specification int-basic2%sub-ls-01: ⊦ i < j - i0 ↔ i + i0 < j; from specification int-abs%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%ls-01: ⊦ i < j → ¬ j < i; from specification int-basic1%lels: ⊦ ¬ i < j ↔ j ≤ i; from specification int-abs%bet: ⊦ 0 < i → (i ≤ 1 ↔ i = 1); from specification int-abs%sub-eq-01: ⊦ i = j → i - j = 0; from specification int-abs%div-one-pos: ⊦ 0 < i → (i | 1 ↔ i = 1); from specification int-gcd%lel: ⊦ i < i0 ∧ i = i1 → i1 < i0; (forward) from specification oelem[intlista]%irreflexivity: ⊦ ¬ i < i; from specification oelem[intlista]%abs-pred: ⊦ i→n(i - 1) < i→n(i) ↔ 0 < i; from specification intnat%lels-03: ⊦ i < j → (¬ ¬ j ≤ i ↔ false); from specification int-abs Used terms: j - 1, i