Def P  Q == PQ

is mentioned by

Thm* x,n,m:. xn & xm  (nnsub(n;x) = nnsub(m;x)  n = m)	[cancel_sub]
Thm* x,n,m:. nx & mx  (nnsub(x;n) = nnsub(x;m)  n = m)	[sub_cancel]
Thm* m,x:. mx  (n:. nnsub(x;m)n  xm+n)	[sub_less_eq_add]
Thm* n,m:. nm  n<m+1	[less_eq_imp_less_suc]
Thm* n,m:. n<m  (x:. n<m+x)	[less_imp_less_add]
Thm* b,c:. cb  (a:. nnsub(a;nnsub(b;c)) = nnsub(a+c;b))	[sub_sub]
Thm* a,b:. ba  (c:. nnsub(a;b)<c  a<b+c)	[less_eq_sub_less]
Thm* c,b:. cb  (a:. nnsub(a+b;c) = a+nnsub(b;c))	[less_eq_add_sub]
Thm* n,m,i:. i<nnsub(n;m)  i+m<n	[less_sub_add_less]
Thm* m,n:. n<m  nnnsub(m;1)	[sub_less_or]
Thm* n:. 0<n  (m:. pre(m)pre(n)  mn)	[inv_pre_less_eq]
Thm* m:. 0<m  (n:. pre(m)<pre(n)  m<n)	[inv_pre_less]
Thm* n:. 0<n  (k:. nmod(nmod(k;n);n) = nmod(k;n))	[mod_mod]
Thm* n:. 0<n  (j,k:. nmod(nmod(j;n)+nmod(k;n);n) = nmod(j+k;n))	[mod_plus]
Thm* n:. 0<n  (q,r:. nmod(qn+r;n) = nmod(r;n))	[mod_times]
Thm* n,r:. r<n  (q:. nmod(qn+r;n) = r)	[mod_mult]
Thm* n:. 0<n  ndiv(0;n) = 0	[zero_div]
Thm* n:. 0<n  nmod(0;n) = 0	[zero_mod]
Thm* n:. 0<n  (k:. nmod(kn;n) = 0)	[mod_eq_0]
Thm* n,k:. k<n  nmod(k;n) = k	[less_mod]
Thm* n,r:. r<n  (q:. ndiv(qn+r;n) = q)	[div_mult]
Thm* n,k,r:. (q:. k = qn+r   & r<n)  nmod(k;n) = r	[mod_unique]
Thm* n,k,q:. (r:. k = qn+r   & r<n)  ndiv(k;n) = q	[ndiv_unique]
Thm* n:. 0<n  (k:. ndiv(k;n)k)	[div_less_eq]
Thm* k,n:. 0<n  (r,q:. k = qn+r   & r<n)	[da]
Thm* P:(). P(0) & (n:. (m:. m<n  P(m))  P(n))  (n:. P(n))	[gen_induction]
Thm* P:(). (n:. P(n))  (n:. P(n) & (m:. m<n  P(m)))	[wop]
Thm* n,m:. nm & mn  n = m	[less_equal_antisym]
Thm* m,n:. n<m  (x:. m = n+x+1  )	[less_add_1]
Thm* m,n,x:. mn  mxnx	[less_mono_mult]
Thm* m,n:. m<n  mn	[less_imp_less_or_eq]
Thm* m,n,x,q:. mx & nq  m+nx+q	[less_eq_less_eq_mono]
Thm* m,n,x:. mn & nx  mx	[less_eq_trans]
Thm* m,n,x:. m+x<n+x  m<n	[less_mono_add_inv]
Thm* m,n,x:. m<n  m+x<n+x	[less_mono_add]
Thm* m,n,x:. nx  (m+n = x    m = nnsub(x;n))	[add_eq_sub]
Thm* m,n:. m<n  n<m+1	[less_suc_not]
Thm* m,n:. 0<m & 0<n  (pre(m) = pre(n)  m = n)	[inv_pre_eq]
Thm* m,n:. 0<n  (m = pre(n)  m+1 = n  )	[pre_suc_eq]
Thm* m,n:. nm  nnsub(m;n)+n = m	[sub_add]
Thm* m,n:. n = 0    m<m+n	[less_add_nonzero]
Thm* m,n:. m+n = m    n = 0	[add_inv_0]
Thm* m,n:. m<n & m = n  n<m	[less_cases_imp]
Thm* m,n:. m<n & n = m+1    m+1<n	[less_not_suc]
Thm* m,n:. m<n & m+1 = n    m+1<n	[less_suc_eq_cor]
Thm* m,n:. m+1n  m<n	[or_less]
Thm* m,n:. m<n  m+1n	[less_or]
Thm* 'a:S, f:('a), x1,x2:'a. f(x1) & f(x2)  x1 = x2	[fun_eq_lemma]
Thm* m,n,x:. m<n & n<x  m<x	[less_trans]

In prior sections: core fun 1 well fnd int 1 bool 1 hol hol bool hol num hol prim rec hol arithmetic 1 int 2 hol arithmetic 3

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html