PrintForm Definitions Lemmas SquareRootLoop Sections NuprlLIB Doc

At: rc loop sqrt sqr mono

a,b:. ab (a)sqr(b)sqr
By:
Def of ( < nat > )sqr
THEN
BackThru: Thm* i1,i2,j1,j2:. i1j1 i2j2 i1i2j1j2
Generated subgoals:

None

About:
multiplyimpliesall

PrintForm Definitions Lemmas SquareRootLoop Sections NuprlLIB Doc