Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* n:. CoPrime(fib(n),fib(n+1))	[fib_coprime]
Thm* n:. fib(n)	[fib_wf]
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* 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:. CoPrime(a,b)  (x,y:. ax+by = 1)	[coprime_bezout_id]
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)  (gcd(a;b) ~ 1)	[coprime_elim_a]
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* i,j:. SqStable(CoPrime(i,j))	[sq_stable__coprime]
Thm* a,b,c:. gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c))	[gcd_assoc]
Thm* a,b,n:. (ngcd(a;b)) ~ gcd(na;nb)	[gcd_mul]
Thm* a,b,y,n:. GCD(a;b;y)  GCD(na;nb;ny)	[gcd_p_mul]
Thm* a,b:. u,v:. GCD(a;b;ua+vb)	[bezout_ident]
Thm* b:, a:. u,v:. GCD(a;b;ua+vb)	[bezout_ident_n]
Thm* a,b:. y:. GCD(a;b;y)	[gcd_exists]
Thm* b:, a:. y:. GCD(a;b;y)	[gcd_ex_n]
Thm* b:, a:. y:. GCD(a;b;y)	[gcd_exists_n]
Thm* a:, b:. q:, r:b. a = qb+r	[quot_rem_exists]
Thm* a:, b:. q:, r:b. a = qb+r	[quot_rem_exists_n]
Thm* a,b,c:. c | a  c | b  c | gcd(a;b)	[gcd_is_gcd]
Thm* a,b:. gcd(a;b) | b	[gcd_is_divisor_2]
Thm* a,b:. gcd(a;b) | a	[gcd_is_divisor_1]
Thm* a,b:. gcd(a;b) ~ gcd(b;a)	[gcd_sym]
Thm* a,b:. y:. GCD(a;b;y) & gcd(a;b) = y	[gcd_elim]
Thm* a,b:. GCD(a;b;gcd(a;b))	[gcd_sat_pred]
Thm* a,b:. GCD(a;b;gcd(a;b))	[gcd_sat_gcd_p]
Thm* a,b:. gcd(a;b)	[gcd_wf]
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_2]
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:. GCD(a;1;1)	[gcd_p_one]
Thm* a:. GCD(a;0;a)	[gcd_p_zero]
Thm* a:. GCD(a;a;a)	[gcd_p_eq_args]
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:. a | b  (c:. b = ac  )	[divides_nchar]
Thm* a:, b:. a | b & b | a  a<b & a | b	[pdivisor_bound]
Thm* a,b:. (a ~ b)  a = b	[assoced_nelim]
Thm* a:. a | 1  (a ~ 1)	[unit_chars]
Thm* a:. |a| ~ a	[absval_assoced]
Thm* a:. (-a) ~ a	[neg_assoced]
Thm* a,b:, n:. ((na) ~ (nb))  (a ~ b)	[mul_cancel_in_assoced]
Thm* a,b:. (a ~ b)  a = b  a = -b	[assoced_elim]
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:. Dec(a | b)	[decidable__divides]
Thm* a:, n:. n | a  (a  n)n = a	[divides_iff_div_exact]
Thm* a:, b:. b | a  (a rem b) = 0	[divides_iff_rem_zero]
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	[assoc_reln]
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* a:. a | a	[divides_reflexivity]
Thm* a,b:. |a| | |b|  a | b	[divides_of_absvals]
Thm* b:. b | 1  b =  1	[only_pm_one_divs_one]
Thm* a:, b:. a | b  ab	[divisors_bound]
Thm* a,b:. a | b  a | -b	[divides_invar_2]
Thm* a,b:. a | b  -a | b	[divides_invar_1]
Thm* b:. b | 0	[any_divs_zero]
Thm* a:. 1 | a	[one_divs_any]
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