| j ≤ (j - 1) / 2 + (j - 1) / 2, 0 < j, n→i(n) ≤ (j - 1) / 2, n→i(m) ≤ (j - 1) / 2, prime(j), n < i→n(1 + (j - 1) / 2), m < i→n(1 + (j - 1) / 2), 0 ≤ j, j ≤ n→i(n) + n→i(m), 0 < n→i(n) + n→i(m), 0 ≤ n→i(n) + n→i(m), j | n→i(n) - n→i(m) ∨ j | n→i(n) + n→i(m) ⊦ ~1 = (j - 1) / 2, m = n, j = 2, countFun(0, (j - 1) / 2, λ i. (~1 - i ^2) |%| j) = [] |
prime(j), n→i(m) ≤ (j - 1) / 2, n→i(n) ≤ (j - 1) / 2, 0 < j, j ≤ 2 * (j - 1) / 2, 0 ≤ n→i(n) + n→i(m), 0 < n→i(n) + n→i(m), j ≤ n→i(n) + n→i(m), 0 ≤ j, m ≤ i→n((j - 1) / 2), n ≤ i→n((j - 1) / 2), 0 < (j - 1) / 2, j | n→i(n) - n→i(m) ∨ j | n→i(n) + n→i(m) ⊦ countFun(0, (j - 1) / 2, λ i. (~1 - i ^2) |%| j) = [], j = 2, m = n, ~1 = (j - 1) / 2
Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs%lels: ⊦ ¬ m < n ↔ n ≤ m; from specification nat%c: ⊦ m + n = n + m; from specification nat-basic2%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic2%s: ⊦ m < n + 1 ↔ ¬ n < m; from specification nat-basic2%abs-succ-03: ⊦ 0 < i → i→n(i + 1) = i→n(i) + 1; from specification intnat%zero-gr: ⊦ 0 < i → (0 < i * j ↔ 0 < j); from specification int-mult%commutativity: ⊦ i * j = j * i; from specification int-mult%associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult%zero-gels-04: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; from specification int-abs%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%zero-ge: ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); from specification int-mult%forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs%forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) 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%add-mult-two: ⊦ i + i = 2 * i; from specification int-mult