Selected Objects

THM	sub_0	m:. nnsub(0;m) = 0 & nnsub(m;0) = m
THM	less_trans	m,n,x:. m<n & n<x  m<x
THM	add1	m:. m+1 = m+1
THM	less_antisym	m,n:. (m<n & n<m)
THM	less_less_suc	m,n:. (m<n & n<m+1)
THM	fun_eq_lemma	'a:S, f:('a), x1,x2:'a. f(x1) & f(x2)  x1 = x2
THM	less_or	m,n:. m<n  m+1n
THM	or_less	m,n:. m+1n  m<n
THM	less_eq	m,n:. m<n  m+1n
THM	less_suc_eq_cor	m,n:. m<n & m+1 = n    m+1<n
THM	less_not_suc	m,n:. m<n & n = m+1    m+1<n
THM	less_0_cases	m:. 0 = m    0<m
THM	less_cases_imp	m,n:. m<n & m = n  n<m
THM	less_cases	m,n:. m<n  nm
THM	add_inv_0	m,n:. m+n = m    n = 0
THM	less_eq_add	m,n:. mm+n
THM	less_eq_suc_refl	m:. mm+1
THM	less_add_nonzero	m,n:. n = 0    m<m+n
THM	less_eq_antisym	m,n:. (m<n & nm)
THM	not_less	m,n:. m<n  nm
THM	sub_eq_0	m,n:. nnsub(m;n) = 0  mn
THM	add_assoc	m,n,x:. m+(n+x) = (m+n)+x
THM	mult_0	m:. m0 = 0
THM	mult_suc	m,n:. m(n+1) = m+mn
THM	mult_right_1	m:. m1 = m
THM	mult_clauses	m,n:. 0m = 0   & m0 = 0   & 1m = m   & m1 = m   & (m+1)n = mn+n   & m(n+1) = m+mn
THM	mult_sym	m,n:. mn = nm
THM	right_add_distrib	m,n,x:. (m+n)x = mx+nx
THM	left_add_distrib	m,n,x:. x(m+n) = xm+xn
THM	mult_assoc	m,n,x:. m(nx) = (mn)x
THM	sub_add	m,n:. nm  nnsub(m;n)+n = m
THM	pre_sub	m,n:. pre(nnsub(m;n)) = nnsub(pre(m);n)
THM	add_eq_0	m,n:. m+n = 0    m = 0   & n = 0
THM	add_inv_0_eq	m,n:. m+n = m    n = 0
THM	pre_suc_eq	m,n:. 0<n  (m = pre(n)  m+1 = n  )
THM	inv_pre_eq	m,n:. 0<m & 0<n  (pre(m) = pre(n)  m = n)
THM	less_suc_not	m,n:. m<n  n<m+1
THM	add_eq_sub	m,n,x:. nx  (m+n = x    m = nnsub(x;n))
THM	less_mono_add	m,n,x:. m<n  m+x<n+x
THM	less_mono_add_inv	m,n,x:. m+x<n+x  m<n
THM	less_mono_add_eq	m,n,x:. m+x<n+x  m<n
THM	eq_mono_add_eq	m,n,x:. m+x = n+x    m = n
THM	less_eq_mono_add_eq	m,n,x:. m+xn+x  mn
THM	less_eq_trans	m,n,x:. mn & nx  mx
THM	less_eq_less_eq_mono	m,n,x,q:. mx & nq  m+nx+q
THM	less_eq_refl	m:. mm
THM	less_imp_less_or_eq	m,n:. m<n  mn
THM	less_mono_mult	m,n,x:. mn  mxnx
THM	right_sub_distrib	m,n,x:. nnsub(m;n)x = nnsub(mx;nx)
THM	left_sub_distrib	m,n,x:. xnnsub(m;n) = nnsub(xm;xn)
THM	less_add_1	m,n:. n<m  (x:. m = n+x+1  )
THM	exp_add	x,q,n:. exp(n;x+q) = exp(n;x)exp(n;q)
THM	not_odd_eq_even	n,m:. n+n+1 = m+m
THM	mult_suc_eq	x,m,n:. n(x+1) = m(x+1)    n = m
THM	mult_exp_mono	x,q,n,m:. nexp(q+1;x) = mexp(q+1;x)    n = m
THM	less_equal_antisym	n,m:. nm & mn  n = m
THM	less_add_suc	m,n:. m<m+n+1
THM	zero_less_eq	n:. 0n
THM	less_eq_mono	n,m:. n+1m+1  nm
THM	less_or_eq_add	n,m:. n<m  (x:. n = x+m  )
THM	wop	P:(). (n:. P(n))  (n:. P(n) & (m:. m<n  P(m)))
THM	gen_induction	P:(). P(0) & (n:. (m:. m<n  P(m))  P(n))  (n:. P(n))
THM	da	k,n:. 0<n  (r,q:. k = qn+r   & r<n)
THM	mod_one	k:. nmod(k;0+1) = 0
THM	div_less_eq	n:. 0<n  (k:. ndiv(k;n)k)
THM	ndiv_unique	n,k,q:. (r:. k = qn+r   & r<n)  ndiv(k;n) = q
THM	mod_unique	n,k,r:. (q:. k = qn+r   & r<n)  nmod(k;n) = r
THM	div_mult	n,r:. r<n  (q:. ndiv(qn+r;n) = q)
THM	less_mod	n,k:. k<n  nmod(k;n) = k
THM	mod_eq_0	n:. 0<n  (k:. nmod(kn;n) = 0)
THM	zero_mod	n:. 0<n  nmod(0;n) = 0
THM	zero_div	n:. 0<n  ndiv(0;n) = 0
THM	mod_mult	n,r:. r<n  (q:. nmod(qn+r;n) = r)
THM	mod_times	n:. 0<n  (q,r:. nmod(qn+r;n) = nmod(r;n))
THM	mod_plus	n:. 0<n  (j,k:. nmod(nmod(j;n)+nmod(k;n);n) = nmod(j+k;n))
THM	mod_mod	n:. 0<n  (k:. nmod(nmod(k;n);n) = nmod(k;n))
THM	sub_mono_eq	n,m:. nnsub(n+1;m+1) = nnsub(n;m)
THM	sub_plus	a,b,c:. nnsub(a;b+c) = nnsub(nnsub(a;b);c)
THM	inv_pre_less	m:. 0<m  (n:. pre(m)<pre(n)  m<n)
THM	inv_pre_less_eq	n:. 0<n  (m:. pre(m)pre(n)  mn)
THM	sub_less_eq	n,m:. nnsub(n;m)n
THM	sub_eq_eq_0	m,n:. nnsub(m;n) = m  m = 0    n = 0
THM	sub_less_0	n,m:. m<n  0<nnsub(n;m)
THM	sub_less_or	m,n:. n<m  nnnsub(m;1)
THM	less_sub_add_less	n,m,i:. i<nnsub(n;m)  i+m<n
THM	times2	n:. 2n = n+n
THM	less_mult_mono	m,i,n:. (n+1)m<(n+1)i  m<i
THM	mult_mono_eq	m,i,n:. (n+1)m = (n+1)i    m = i
THM	add_sub	a,c:. nnsub(a+c;c) = a
THM	less_eq_add_sub	c,b:. cb  (a:. nnsub(a+b;c) = a+nnsub(b;c))
THM	sub_equal_0	c:. nnsub(c;c) = 0
THM	less_eq_sub_less	a,b:. ba  (c:. nnsub(a;b)<c  a<b+c)
THM	not_suc_less_eq	n,m:. n+1m  mn
THM	sub_sub	b,c:. cb  (a:. nnsub(a;nnsub(b;c)) = nnsub(a+c;b))
THM	less_imp_less_add	n,m:. n<m  (x:. n<m+x)
THM	less_eq_imp_less_suc	n,m:. nm  n<m+1
THM	sub_less_eq_add	m,x:. mx  (n:. nnsub(x;m)n  xm+n)
THM	sub_cancel	x,n,m:. nx & mx  (nnsub(x;n) = nnsub(x;m)  n = m)
THM	cancel_sub	x,n,m:. xn & xm  (nnsub(n;x) = nnsub(m;x)  n = m)

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