theorem :: HILB10_1:39

for x, y, z being Nat holds
( y = x |^ z iff ( ( y = 1 & z = 0 ) or ( x = 0 & y = 0 & z > 0 ) or ( x = 1 & y = 1 & z > 0 ) or ( x > 1 & z > 0 & ex y1, y2, y3, K being Nat st
( y1 = Py (x,(z + 1)) & K > (2 * z) * y1 & y2 = Py (K,(z + 1)) & y3 = Py ((K * x),(z + 1)) & ( ( 0 <= y - (y3 / y2) & y - (y3 / y2) < 1 / 2 ) or ( 0 <= (y3 / y2) - y & (y3 / y2) - y < 1 / 2 ) ) ) ) ) )