Selected Objects

THM	not_exp_0	m,n:. exp(n+1;m) = 0
THM	zero_less_exp	m,n:. 0<exp(n+1;m)
THM	odd_or_even	n:. m:. n = (0+1+1)m    n = (0+1+1)m+1
THM	less_exp_suc_mono	n,m:. exp(m+1+1;n)<exp(m+1+1;n+1)
THM	less_less_cases	m,n:. m = n  m<n  n<m
THM	greater_eq	n,m:. True
THM	less_eq_cases	m,n:. mn  nm
THM	less_equal_add	m,n:. mn  (x:. n = m+x  )
THM	less_eq_exists	m,n:. mn  (x:. n = m+x  )
THM	not_less_equal	m,n:. mn  n<m
THM	less_eq_0	n:. n0  n = 0
THM	mult_eq_0	m,n:. mn = 0    m = 0    n = 0
THM	less_mult2	m,n:. 0<m & 0<n  0<mn
THM	less_eq_less_trans	m,n,x:. mn & n<x  m<x
THM	less_less_eq_trans	m,n,x:. m<n & nx  m<x
THM	fact_less	n:. 0<fact(n)
THM	even_odd	n:. even(n)  odd(n)
THM	odd_even	n:. odd(n)  even(n)
THM	even_or_odd	n:. even(n)  odd(n)
THM	even_and_odd	n:. (even(n) & odd(n))
THM	even_add	m,n:. even(m+n)  (even(m)  even(n))
THM	even_mult	m,n:. even(mn)  even(m)  even(n)
THM	odd_add	m,n:. odd(m+n)  (odd(m)  odd(n))
THM	odd_mult	m,n:. odd(mn)  odd(m) & odd(n)
THM	even_double	n:. even(2n)
THM	odd_double	n:. odd(2n+1)
THM	even_odd_exists	n:. (even(n)  (m:. n = 2m  )) & (odd(n)  (m:. n = 2m+1  ))
THM	even_exists	n:. even(n)  (m:. n = 2m  )
THM	odd_exists	n:. odd(n)  (m:. n = 2m+1  )
THM	eq_less_eq	m,n:. m = n  mn & nm
THM	add_mono_less_eq	m,n,x:. m+nm+x  nx
THM	not_suc_less_eq_0	n:. n+10
THM	not_leq	m,n:. mn  n+1m
THM	not_num_eq	m,n:. m = n  m+1n  n+1m
THM	not_greater	m,n:. n<m  mn
THM	not_greater_eq	m,n:. nm  m+1n
THM	suc_one_add	n:. n+1 = 1+n
THM	suc_add_sym	m,n:. m+n+1 = n+1+m
THM	not_suc_add_less_eq	m,n:. m+n+1m
THM	mult_less_eq_suc	m,n,x:. mn  (x+1)m(x+1)n
THM	sub_left_add	m,n,x:. m+nnsub(n;x) = if nx then m else nnsub(m+n;x) fi
THM	sub_right_add	m,n,x:. nnsub(m;n)+x = if mn then x else nnsub(m+x;n) fi
THM	sub_left_sub	m,n,x:. nnsub(m;nnsub(n;x)) = if nx then m else nnsub(m+x;n) fi
THM	sub_right_sub	m,n,x:. nnsub(nnsub(m;n);x) = nnsub(m;n+x)
THM	sub_left_suc	m,n:. nnsub(m;n)+1 = if mn then 0+1 else nnsub(m+1;n) fi
THM	sub_left_less_eq	m,n,x:. mnnsub(n;x)  m+xn  m0
THM	sub_right_less_eq	m,n,x:. nnsub(m;n)x  mn+x
THM	sub_left_less	m,n,x:. m<nnsub(n;x)  m+x<n
THM	sub_right_less	m,n,x:. nnsub(m;n)<x  m<n+x & 0<x
THM	sub_left_greater_eq	m,n,x:. nnsub(n;x)m  nm+x
THM	sub_right_greater_eq	m,n,x:. xnnsub(m;n)  n+xm  x0
THM	sub_left_greater	m,n,x:. nnsub(n;x)<m  n<m+x & 0<m
THM	sub_right_greater	m,n,x:. x<nnsub(m;n)  n+x<m
THM	sub_left_eq	m,n,x:. m = nnsub(n;x)  m+x = n    m0 & nx
THM	sub_right_eq	m,n,x:. nnsub(m;n) = x  m = n+x    mn & x0

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