Def P  Q == PQ

is mentioned by

Thm* r,s:. CoPrime(r,s)  (a,b:. x:. (x = a mod r) & (x = b mod s))	[chrem_exists]
Thm* r,s:. CoPrime(r,s)  (x:. (x = 1 mod r) & (x = 0 mod s))	[chrem_exists_aux]
Thm* m,a,a',b,b':. (a = a' mod m)  (b = b' mod m)  ((ab) = (a'b') mod m)	[multiply_functionality_wrt_eqmod]
Thm* m,a,a',b,b':. (a = a' mod m)  (b = b' mod m)  ((a+b) = (a'+b') mod m)	[add_functionality_wrt_eqmod]
Thm* m,a,a',b,b':. Thm* (a = a' mod m)  (b = b' mod m)  ((a = b mod m)  (a' = b' mod m))	[eqmod_fun]
Thm* m,m',a,a',b,b':. Thm* m = m' Thm*  Thm* (a = a' mod m)  (b = b' mod m)  ((a = b mod m)  (a' = b' mod m'))	[eqmod_functionality_wrt_eqmod]
Thm* m,a,b:. (a = b mod m)  (b = a mod m)	[eqmod_inversion]
Thm* m,a,b,c:. (a = b mod m)  (b = c mod m)  (a = c mod m)	[eqmod_transitivity]
Thm* m,a,b:. a = b  (a = b mod m)	[eqmod_weakening]
Thm* p:. prime(p)  (a1,a2:. p | a1a2  p | a1  p | a2)	[prime_divs_prod]
Thm* a:. atomic(a)  prime(a)	[atomic_imp_prime]
Thm* a1,a2,b:. CoPrime(a1,a2)  a1 | b  a2 | b  a1a2 | b	[coprime_divisors_prod]
Thm* a,b1,b2:. CoPrime(a,b1)  CoPrime(a,b2)  CoPrime(a,b1b2)	[coprime_prod]
Thm* a,b:. (x,y:. ax+by = 1)  CoPrime(a,b)	[coprime_bezout_id2]
Thm* a,b:. CoPrime(a,b)  (x,y:. ax+by = 1)	[coprime_bezout_id1]
Thm* a,b:. CoPrime(a,b)  (x,y:. (ax+by) ~ 1)	[coprime_bezout_id0]
Thm* a,p:. prime(p)  (CoPrime(p,a)  p | a)	[coprime_iff_ndivides]
Thm* a,b:. CoPrime(a,b)  (c:. c | a  c | b  (c ~ 1))	[coprime_elim]
Thm* a,b:. (c:. c | a  c | b  c | 1)  CoPrime(a,b)	[coprime_intro]
Thm* p:. prime(p)  p = 0 & (p ~ 1) & (a:. a | p  (a ~ 1)  (a ~ p))	[prime_elim]
Thm* a:. prime(a)  atomic(a)	[prime_imp_atomic]
Thm* a:, b:. ab | a  (b ~ 1)	[self_divisor_mul]
Thm* a:. atomic(a)  (a ~ 1) & (b:. b | a  (b ~ 1)  (b ~ a))	[atomic_char]
Thm* a,b,y,n:. GCD(a;b;y)  GCD(na;nb;ny)	[gcd_p_mul]
Thm* a,b,c:. c | a  c | b  c | gcd(a;b)	[gcd_is_gcd]
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,y1,y2:. GCD(a;b;y1)  GCD(a;b;y2)  (y1 ~ y2)	[gcd_unique]
Thm* a,b,y,k:. GCD(a;b;y)  GCD(a;b+ka;y)	[gcd_p_shift]
Thm* a,b,y:. GCD(a;b;y)  GCD(-a;b;y)	[gcd_p_neg_arg_a]
Thm* a,b,y:. GCD(a;b;y)  GCD(a;-b;y)	[gcd_p_neg_arg]
Thm* a,b,y:. GCD(a;b;y)  GCD(b;a;y)	[gcd_p_sym_a]
Thm* a,b,y:. GCD(a;b;y)  GCD(b;a;y)	[gcd_p_sym]
Thm* a,b:. GCD(a;0;b)  a = b  a = -b	[gcd_p_zero_rel]
Thm* a,a',b,b',y,y':. Thm* (a ~ a')  (b ~ b')  (y ~ y')  (GCD(a;b;y)  GCD(a';b';y'))	[gcd_p_functionality_wrt_assoced]
Thm* a,b:, n:. ((na) ~ (nb))  (a ~ b)	[mul_cancel_in_assoced]
Thm* a,b,a',b':. (a ~ a')  (b ~ b')  ((a ~ b)  (a' ~ b'))	[assoced_functionality_wrt_assoced]
Thm* a,a',b,b':. (a ~ a')  (b ~ b')  ((ab) ~ (a'b'))	[multiply_functionality_wrt_assoced]
Thm* a,b,c:. (a ~ b)  (b ~ c)  (a ~ c)	[assoced_transitivity]
Thm* a,b:. a = b  (a ~ b)	[assoced_weakening]
Thm* a,a',b,b':. (a ~ a')  (b ~ b')  (a | b  a' | b')	[divides_functionality_wrt_assoced]
Thm* a:, b:. a | b  ab	[divisor_bound]
Thm* a,b:. a | b  (n:. na | nb)	[divides_mul]
Thm* a,b,c:. a | b  a | bc	[divisor_of_mul]
Thm* a,b:. a | b  a | -b	[divisor_of_minus]
Thm* a,b1,b2:. a | b1  a | b2  a | b1+b2	[divisor_of_sum]
Thm* a,b:. a | b  b | a  a =  b	[divides_anti_sym]
Thm* a,b:. a | b  b | a  a = b	[divides_anti_sym_n]
Thm* a,b,c:. a | b  b | c  a | c	[divides_transitivity]
Thm* b:. b | 1  b =  1	[only_pm_one_divs_one]
Thm* a:, b:. a | b  ab	[divisors_bound]
Thm* a:. 0 | a  a = 0	[zero_divs_only_zero]
Def prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc  a | b  a | c)	[prime]
Def GCD(a;b;y) == y | a & y | b & (z:. z | a & z | b  z | y)	[gcd_p]

In prior sections: core well fnd int 1 bool 1 int 2 union rel 1

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