SquareRootLoop
Doc
A proof that a certain loop program computes natural square root without depending on explicit well formedness established beforehand. I got this formulation from Constable. 08/06/02 (sfa)
Tue Aug 6 18:24:00 EDT 2002
SquareRootLoop
Doc