IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
hmod unique all
(n:hnum. all
(n:hnum. (k:hnum. all
(n:hnum. (k:hnum. (r:hnum. implies
(n:hnum. (k:hnum. (r:hnum. (exists
(n:hnum. (k:hnum. (r:hnum. ((q:hnum. and
(n:hnum. (k:hnum. (r:hnum. ((q:hnum. (equal(k,add(mult(q,n),r))
(n:hnum. (k:hnum. (r:hnum. ((q:hnum. ,lt(r,n)))
(n:hnum. (k:hnum. (r:hnum. ,equal(mod(k,n),r)))))
By:
HOL "hmod_unique"
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
all
(
n:hnum. all
