Def P  Q == (P  Q) & (P  Q)

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:. n+1m  mn	[not_suc_less_eq]
Thm* a,b:. ba  (c:. nnsub(a;b)<c  a<b+c)	[less_eq_sub_less]
Thm* m,i,n:. (n+1)m = (n+1)i    m = i	[mult_mono_eq]
Thm* m,i,n:. (n+1)m<(n+1)i  m<i	[less_mult_mono]
Thm* n,m:. m<n  0<nnsub(n;m)	[sub_less_0]
Thm* m,n:. nnsub(m;n) = m  m = 0    n = 0	[sub_eq_eq_0]
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,m:. n+1m+1  nm	[less_eq_mono]
Thm* x,q,n,m:. nexp(q+1;x) = mexp(q+1;x)    n = m	[mult_exp_mono]
Thm* x,m,n:. n(x+1) = m(x+1)    n = m	[mult_suc_eq]
Thm* m,n,x:. m+xn+x  mn	[less_eq_mono_add_eq]
Thm* m,n,x:. m+x = n+x    m = n	[eq_mono_add_eq]
Thm* m,n,x:. m+x<n+x  m<n	[less_mono_add_eq]
Thm* m,n,x:. nx  (m+n = x    m = nnsub(x;n))	[add_eq_sub]
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:. m+n = m    n = 0	[add_inv_0_eq]
Thm* m,n:. m+n = 0    m = 0   & n = 0	[add_eq_0]
Thm* m,n:. nnsub(m;n) = 0  mn	[sub_eq_0]
Thm* m,n:. m<n  nm	[not_less]
Thm* m,n:. m<n  m+1n	[less_eq]

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

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