for k being positive Nat holds
( k + 1 is prime iff ex a, b, c, d, e, f, g, h, i, j, l, m, n, o, p, q, r, s, t, u, w, v, x, y, z being Nat st
( q = ((w * z) + h) + j & z = ((((g * k) + g) + k) * (h + j)) + h & ((((2 * k) |^ 3) * ((2 * k) + 2)) * ((n + 1) |^ 2)) + 1 = f ^2 & e = ((p + q) + z) + (2 * n) & (((e |^ 3) * (e + 2)) * ((a + 1) |^ 2)) + 1 = o ^2 & [x,y] is Pell's_solution of (a ^2) -' 1 & u ^2 = ((((16 * ((a ^2) - 1)) * (r ^2)) * (y ^2)) * (y ^2)) + 1 & (x + (c * u)) ^2 = ((((a + ((u ^2) * ((u ^2) - a))) ^2) - 1) * ((n + ((4 * d) * y)) ^2)) + 1 & [m,l] is Pell's_solution of (a ^2) -' 1 & l = k + (i * (a - 1)) & (n + l) + v = y & m = (p + (l * ((a - n) - 1))) + (b * ((((2 * a) * (n + 1)) - ((n + 1) ^2)) - 1)) & x = (q + (y * ((a - p) - 1))) + (s * ((((2 * a) * (p + 1)) - ((p + 1) ^2)) - 1)) & p * m = (z + ((p * l) * (a - p))) + (t * ((((2 * a) * p) - (p ^2)) - 1)) ) )