Def P & Q == PQ

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:. nnsub(n;x)<m  n<m+x & 0<m	[sub_left_greater]
Thm* m,n,x:. nnsub(m;n)<x  m<n+x & 0<x	[sub_right_less]
Thm* m,n:. m = n  mn & nm	[eq_less_eq]
Thm* n:. (even(n)  (m:. n = 2m  )) & (odd(n)  (m:. n = 2m+1  ))	[even_odd_exists]
Thm* m,n:. odd(mn)  odd(m) & odd(n)	[odd_mult]
Thm* n:. (even(n) & odd(n))	[even_and_odd]
Thm* m,n,x:. m<n & nx  m<x	[less_less_eq_trans]
Thm* m,n,x:. mn & n<x  m<x	[less_eq_less_trans]
Thm* m,n:. 0<m & 0<n  0<mn	[less_mult2]

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

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