| ¬(n→i(n) ≤ (j - 1) / 2 - 0 ∧ 0 ≤ 0 ∧ 0 ≤ (j - 1) / 2), n→i(m) ^2 |%| j = countFun(0, (j - 1) / 2, λ i. i ^2 |%| j)[n], 0 ≤ j, m < i→n(1 + (j - 1) / 2), n < i→n(1 + (j - 1) / 2), prime(j), n→i(m) ≤ (j - 1) / 2 ⊦ countFun(0, (j - 1) / 2, λ i. i ^2 |%| j) = [], j = 2, m = n, ~1 = (j - 1) / 2 |
n→i(m) ^2 |%| j = countFun(0, (j - 1) / 2, λ i. i ^2 |%| j)[n], m < i→n(1 + (j - 1) / 2), m < n, 0 ≤ j, n < i→n(1 + (j - 1) / 2), prime(j), n→i(m) ≤ (j - 1) / 2, (j - 1) / 2 < n→i(n), m + 1 < i→n(1 + (j - 1) / 2) ⊦ countFun(0, (j - 1) / 2, λ i. i ^2 |%| j) = [], j = 2, ~1 = (j - 1) / 2
Used simplifier rules: succ: ⊦ m +1 = m + 1; from specification nat-basic2%f: ⊦ m < n → n ≠ 0; from specification nat-basic1%trans-1: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic1%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic1%lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic1%nat2int-04: ⊦ n→i(m) < n→i(n) ↔ m < n; from specification intnat%forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs%lels-01: ⊦ ¬ i ≤ j ↔ j < i; from specification int-abs%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%add-c: ⊦ i + j = j + i; from specification int-basic2%add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2%sub-le-01: ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; from specification int-abs%div-two-zero-01: ⊦ 0 ≤ i / 2 ↔ ~1 ≤ i; from specification int-div%sub-zero-01: ⊦ i - 0 = i; from specification int-abs