PrintForm Definitions hol arithmetic 3 Sections HOLlib Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hmod plus

  all
  (n:hnum. implies
  (n:hnum. (lt(0,n)
  (n:hnum. ,all
  (n:hnum. ,(j:hnum. all
  (n:hnum. ,(j:hnum. (k:hnum. equal
  (n:hnum. ,(j:hnum. (k:hnum. (mod(add(mod(j,n),mod(k,n)),n)
  (n:hnum. ,(j:hnum. (k:hnum. ,mod(add(j,k),n))))))


By: HOL "hmod_plus"


Generated subgoals:

None

About:
assertnatural_numberapply
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

PrintForm Definitions hol arithmetic 3 Sections HOLlib Doc