Def x:A. B(x) == x:AB(x)

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* 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* c:. nnsub(c;c) = 0	[sub_equal_0]
Thm* c,b:. cb  (a:. nnsub(a+b;c) = a+nnsub(b;c))	[less_eq_add_sub]
Thm* a,c:. nnsub(a+c;c) = a	[add_sub]
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:. 2n = n+n	[times2]
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,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,m:. nnsub(n;m)n	[sub_less_eq]
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* a,b,c:. nnsub(a;b+c) = nnsub(nnsub(a;b);c)	[sub_plus]
Thm* n,m:. nnsub(n+1;m+1) = nnsub(n;m)	[sub_mono_eq]
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:. nmod(k;0+1) = 0	[mod_one]
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:. n<m  (x:. n = x+m  )	[less_or_eq_add]
Thm* n,m:. n+1m+1  nm	[less_eq_mono]
Thm* n:. 0n	[zero_less_eq]
Thm* m,n:. m<m+n+1	[less_add_suc]
Thm* n,m:. nm & mn  n = m	[less_equal_antisym]
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* n,m:. n+n+1 = m+m	[not_odd_eq_even]
Thm* x,q,n:. exp(n;x+q) = exp(n;x)exp(n;q)	[exp_add]
Thm* m,n:. n<m  (x:. m = n+x+1  )	[less_add_1]
Thm* m,n,x:. xnnsub(m;n) = nnsub(xm;xn)	[left_sub_distrib]
Thm* m,n,x:. nnsub(m;n)x = nnsub(mx;nx)	[right_sub_distrib]
Thm* m,n,x:. mn  mxnx	[less_mono_mult]
Thm* m,n:. m<n  mn	[less_imp_less_or_eq]
Thm* m:. mm	[less_eq_refl]
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+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:. 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:. 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:. pre(nnsub(m;n)) = nnsub(pre(m);n)	[pre_sub]
Thm* m,n:. nm  nnsub(m;n)+n = m	[sub_add]
Thm* m,n,x:. m(nx) = (mn)x	[mult_assoc]
Thm* m,n,x:. x(m+n) = xm+xn	[left_add_distrib]
Thm* m,n,x:. (m+n)x = mx+nx	[right_add_distrib]
Thm* m,n:. mn = nm	[mult_sym]
Thm* m,n:. Thm* 0m = 0   Thm* & m0 = 0   Thm* & 1m = m   Thm* & m1 = m   Thm* & (m+1)n = mn+n   Thm* & m(n+1) = m+mn	[mult_clauses]
Thm* m:. m1 = m	[mult_right_1]
Thm* m,n:. m(n+1) = m+mn	[mult_suc]
Thm* m:. m0 = 0	[mult_0]
Thm* m,n,x:. m+(n+x) = (m+n)+x	[add_assoc]
Thm* m,n:. nnsub(m;n) = 0  mn	[sub_eq_0]
Thm* m,n:. m<n  nm	[not_less]
Thm* m,n:. (m<n & nm)	[less_eq_antisym]
Thm* m,n:. n = 0    m<m+n	[less_add_nonzero]
Thm* m:. mm+1	[less_eq_suc_refl]
Thm* m,n:. mm+n	[less_eq_add]
Thm* m,n:. m+n = m    n = 0	[add_inv_0]
Thm* m,n:. m<n  nm	[less_cases]
Thm* m,n:. m<n & m = n  n<m	[less_cases_imp]
Thm* m:. 0 = m    0<m	[less_0_cases]
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<n  m+1n	[less_eq]
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:. (m<n & n<m+1)	[less_less_suc]
Thm* m,n:. (m<n & n<m)	[less_antisym]
Thm* m:. m+1 = m+1	[add1]
Thm* m,n,x:. m<n & n<x  m<x	[less_trans]
Thm* m:. nnsub(0;m) = 0 & nnsub(m;0) = m	[sub_0]

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

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