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

is mentioned by

Thm* m,n,x:. nnsub(m;n) = x  m = n+x    mn & x0	[sub_right_eq]
Thm* m,n,x:. m = nnsub(n;x)  m+x = n    m0 & nx	[sub_left_eq]
Thm* m,n,x:. x<nnsub(m;n)  n+x<m	[sub_right_greater]
Thm* m,n,x:. nnsub(n;x)<m  n<m+x & 0<m	[sub_left_greater]
Thm* m,n,x:. xnnsub(m;n)  n+xm  x0	[sub_right_greater_eq]
Thm* m,n,x:. nnsub(n;x)m  nm+x	[sub_left_greater_eq]
Thm* m,n,x:. nnsub(m;n)<x  m<n+x & 0<x	[sub_right_less]
Thm* m,n,x:. m<nnsub(n;x)  m+x<n	[sub_left_less]
Thm* m,n,x:. nnsub(m;n)x  mn+x	[sub_right_less_eq]
Thm* m,n,x:. mnnsub(n;x)  m+xn  m0	[sub_left_less_eq]
Thm* m,n,x:. mn  (x+1)m(x+1)n	[mult_less_eq_suc]
Thm* m,n:. nm  m+1n	[not_greater_eq]
Thm* m,n:. n<m  mn	[not_greater]
Thm* m,n:. m = n  m+1n  n+1m	[not_num_eq]
Thm* m,n:. mn  n+1m	[not_leq]
Thm* m,n,x:. m+nm+x  nx	[add_mono_less_eq]
Thm* m,n:. m = n  mn & nm	[eq_less_eq]
Thm* n:. odd(n)  (m:. n = 2m+1  )	[odd_exists]
Thm* n:. even(n)  (m:. n = 2m  )	[even_exists]
Thm* m,n:. odd(mn)  odd(m) & odd(n)	[odd_mult]
Thm* m,n:. odd(m+n)  (odd(m)  odd(n))	[odd_add]
Thm* m,n:. even(mn)  even(m)  even(n)	[even_mult]
Thm* m,n:. even(m+n)  (even(m)  even(n))	[even_add]
Thm* n:. odd(n)  even(n)	[odd_even]
Thm* n:. even(n)  odd(n)	[even_odd]
Thm* m,n:. mn = 0    m = 0    n = 0	[mult_eq_0]
Thm* n:. n0  n = 0	[less_eq_0]
Thm* m,n:. mn  n<m	[not_less_equal]
Thm* m,n:. mn  (x:. n = m+x  )	[less_eq_exists]

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 hol arithmetic 4

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