Def P & Q == PQ

is mentioned by

Thm* r:, s:{s':| CoPrime(r,s') }, a,b:. Thm* x:. ((x = a mod r) & (x = b mod s))	[chrem_exists_a]
Thm* r,s:. CoPrime(r,s)  (a,b:. x:. (x = a mod r) & (x = b mod s))	[chrem_exists]
Thm* r:, s:{s':| CoPrime(r,s') }. x:. ((x = 1 mod r) & (x = 0 mod s))	[chrem_exists_aux_a]
Thm* r,s:. CoPrime(r,s)  (x:. (x = 1 mod r) & (x = 0 mod s))	[chrem_exists_aux]
Thm* p:. prime(p)  p = 0 & (p ~ 1) & (a:. a | p  (a ~ 1)  (a ~ p))	[prime_elim]
Thm* a:. atomic(a)  (a ~ 1) & (b:. b | a  (b ~ 1)  (b ~ a))	[atomic_char]
Thm* a,b:. y:. GCD(a;b;y) & gcd(a;b) = y	[gcd_elim]
Thm* a,b,c,x,y:. Thm* GCD(a;b;x) Thm*  Thm* GCD(x;c;y) Thm*  Thm* y | a & y | b & y | c & (z:. z | a  z | b  z | c  z | y)	[gcd_of_triple]
Thm* a:, b:. a | b & b | a  a<b & a | b	[pdivisor_bound]
Thm* a,b:. a | b & b | a  a =  b	[assoc_reln]
Def prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc  a | b  a | c)	[prime]
Def atomic(a) == a = 0 & (a ~ 1) & reducible(a)	[atomic]
Def reducible(a) == b,c:. (b ~ 1) & (c ~ 1) & a = bc	[reducible]
Def GCD(a;b;y) == y | a & y | b & (z:. z | a & z | b  z | y)	[gcd_p]
Def a ~ b == a | b & b | a	[assoced]

In prior sections: core int 1 bool 1 int 2 rel 1

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