== {i:
| 0
i } == {i:| 0i }is mentioned by
 m,n,x:. nnsub(m;n) = x   m = n+x   mn & x0 | [sub_right_eq] |
| m,n,x:. m = nnsub(n;x) m+x = n m0 & nx | [sub_left_eq] |
| m,n,x:. x<nnsub(m;n) n+x<m | [sub_right_greater] |
| m,n,x:. nnsub(n;x)<m n<m+x & 0<m | [sub_left_greater] |
| m,n,x:. xnnsub(m;n) n+xm x0 | [sub_right_greater_eq] |
| m,n,x:. nnsub(n;x)m nm+x | [sub_left_greater_eq] |
| m,n,x:. nnsub(m;n)<x m<n+x & 0<x | [sub_right_less] |
| m,n,x:. m<nnsub(n;x) m+x<n | [sub_left_less] |
| m,n,x:. nnsub(m;n)x mn+x | [sub_right_less_eq] |
| m,n,x:. mnnsub(n;x) m+xn m0 | [sub_left_less_eq] |
m,n:. nnsub(m;n)+1 = if m n then 0+1 else nnsub(m+1;n) fi | [sub_left_suc] |
| m,n,x:. nnsub(nnsub(m;n);x) = nnsub(m;n+x) | [sub_right_sub] |
| m,n,x:. nnsub(m;nnsub(n;x)) = if nx then m else nnsub(m+x;n) fi | [sub_left_sub] |
| m,n,x:. nnsub(m;n)+x = if mn then x else nnsub(m+x;n) fi | [sub_right_add] |
| m,n,x:. m+nnsub(n;x) = if nx then m else nnsub(m+n;x) fi | [sub_left_add] |
m,n,x:. mn (x+1) m(x+1)n | [mult_less_eq_suc] |
m,n:.  m+n+1m | [not_suc_add_less_eq] |
| m,n:. m+n+1 = n+1+m | [suc_add_sym] |
| n:. n+1 = 1+n | [suc_one_add] |
| m,n:. nm m+1n | [not_greater_eq] |
| m,n:. n<m mn | [not_greater] |
| m,n:. m = n m+1n n+1m | [not_num_eq] |
| m,n:. mn n+1m | [not_leq] |
| n:. n+10 | [not_suc_less_eq_0] |
| m,n,x:. m+nm+x nx | [add_mono_less_eq] |
| m,n:. m = n mn & nm | [eq_less_eq] |
n:. odd(n) ( m:. n = 2m+1 ) | [odd_exists] |
| n:. even(n) (m:. n = 2m ) | [even_exists] |
n:. (even(n)  (m:. n = 2m )) & (odd(n) (m:. n = 2m+1 )) | [even_odd_exists] |
| n:. odd(2n+1) | [odd_double] |
| n:. even(2n) | [even_double] |
| m,n:. odd(mn) odd(m) & odd(n) | [odd_mult] |
| m,n:. odd(m+n) (odd(m) odd(n)) | [odd_add] |
| m,n:. even(mn) even(m) even(n) | [even_mult] |
| m,n:. even(m+n) (even(m) even(n)) | [even_add] |
| n:. (even(n) & odd(n)) | [even_and_odd] |
| n:. even(n) odd(n) | [even_or_odd] |
| n:. odd(n) even(n) | [odd_even] |
| n:. even(n) odd(n) | [even_odd] |
| n:. 0<fact(n) | [fact_less] |
| m,n,x:. m<n & nx m<x | [less_less_eq_trans] |
| m,n,x:. mn & n<x m<x | [less_eq_less_trans] |
| m,n:. 0<m & 0<n 0<mn | [less_mult2] |
| m,n:. mn = 0 m = 0 n = 0 | [mult_eq_0] |
| n:. n0 n = 0 | [less_eq_0] |
| m,n:. mn n<m | [not_less_equal] |
| m,n:. mn (x:. n = m+x ) | [less_eq_exists] |
| m,n:. mn (x:. n = m+x ) | [less_equal_add] |
| m,n:. mn nm | [less_eq_cases] |
| n,m:. True | [greater_eq] |
| m,n:. m = n m<n n<m | [less_less_cases] |
| n,m:. exp(m+1+1;n)<exp(m+1+1;n+1) | [less_exp_suc_mono] |
| n:. m:. n = (0+1+1)m n = (0+1+1)m+1 | [odd_or_even] |
| m,n:. 0<exp(n+1;m) | [zero_less_exp] |
| m,n:. exp(n+1;m) = 0 | [not_exp_0] |
In prior sections: int 1 bool 1 hol num hol prim rec hol arithmetic 1 int 2 hol arithmetic 4 hol min
Try larger context:
HOLlib
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html