{ x = n , n > 0 }
{ x = n , n > 0 , 0 = 0 }
 z := 0;
{ x = n , n > z , z = 0 }
{ x = n , n > z , z = 0 , 1 = 1 }
odd := 1;
{ x = n , n > z , z = 0 , odd = 1 }
{ x = n , n > z , z = 0 , odd = 1 , 1 = 1}
sum := 1;
{ x = n , n > z , z = 0 , odd = sum , sum = 1 }
{ x = n , n > z , z = 0 , odd = sum - 0 , sum = 1 }
{ x = n , n > z , z = 0 , odd = sum - (z ^ 2) , sum = 1 }
{ x = n , n > z , z = 0 , sum - odd = (z ^ 2) , sum = (z + 1) ^ 2 , sum <= x } = INV
while sum <= x
	{ sum <= x ^ INV }
	z := z + 1;
	odd := odd + 2;
	sum := sum + odd;
{ ¬(sum <= x) , INV }
{ sum > x , INV }

{  }
{ (z ^ 2) <= n , (z + 1) ^ 2 > n }