Selected Objects

def	divides	b | a == c:. a = bc
THM	zero_divs_only_zero	a:. 0 | a  a = 0
THM	one_divs_any	a:. 1 | a
THM	any_divs_zero	b:. b | 0
THM	divides_invar_1	a,b:. a | b  -a | b
THM	divides_invar_2	a,b:. a | b  a | -b
THM	divisors_bound	a:, b:. a | b  ab
THM	only_pm_one_divs_one	b:. b | 1  b =  1
THM	divides_of_absvals	a,b:. |a| | |b|  a | b
THM	divides_reflexivity	a:. a | a
THM	divides_transitivity	a,b,c:. a | b  b | c  a | c
THM	divides_preorder	Preorder(;x,y.x | y)
THM	divides_anti_sym_n	a,b:. a | b  b | a  a = b
THM	divides_anti_sym	a,b:. a | b  b | a  a =  b
THM	assoc_reln	a,b:. a | b & b | a  a =  b
THM	divisor_of_sum	a,b1,b2:. a | b1  a | b2  a | b1+b2
THM	divisor_of_minus	a,b:. a | b  a | -b
THM	divisor_of_mul	a,b,c:. a | b  a | bc
THM	divides_mul	a,b:. a | b  (n:. na | nb)
THM	divisor_bound	a:, b:. a | b  ab
THM	divides_iff_rem_zero	a:, b:. b | a  (a rem b) = 0
THM	divides_iff_div_exact	a:, n:. n | a  (a  n)n = a
THM	decidable__divides	a,b:. Dec(a | b)
COM	divides_instance_com	The proof here illustrates how the evaluation of the extract of one theorem (decidable__divides) can help to prove another theorem. ...
THM	divides_instance	3 | 6
COM	gcd_p_com	Should redo this not using uncurried antecedents.Makes forward chaining a lot easier.
def	assoced	a ~ b == a | b & b | a
THM	assoced_equiv_rel	EquivRel x,y:. x ~ y
THM	divides_functionality_wrt_assoced	a,a',b,b':. (a ~ a')  (b ~ b')  (a | b  a' | b')
THM	assoced_weakening	a,b:. a = b  (a ~ b)
THM	assoced_transitivity	a,b,c:. (a ~ b)  (b ~ c)  (a ~ c)
THM	multiply_functionality_wrt_assoced	a,a',b,b':. (a ~ a')  (b ~ b')  ((ab) ~ (a'b'))
THM	assoced_functionality_wrt_assoced	a,b,a',b':. (a ~ a')  (b ~ b')  ((a ~ b)  (a' ~ b'))
THM	assoced_elim	a,b:. (a ~ b)  a = b  a = -b
THM	mul_cancel_in_assoced	a,b:, n:. ((na) ~ (nb))  (a ~ b)
THM	neg_assoced	a:. (-a) ~ a
THM	absval_assoced	a:. |a| ~ a
THM	unit_chars	a:. a | 1  (a ~ 1)
THM	assoced_nelim	a,b:. (a ~ b)  a = b
THM	pdivisor_bound	a:, b:. a | b & b | a  a<b & a | b
THM	divides_nchar	a,b:. a | b  (c:. b = ac  )
def	gcd_p	GCD(a;b;y) == y | a & y | b & (z:. z | a & z | b  z | y)
THM	gcd_p_functionality_wrt_assoced	a,a',b,b',y,y':. (a ~ a')  (b ~ b')  (y ~ y')  (GCD(a;b;y)  GCD(a';b';y'))
THM	gcd_p_eq_args	a:. GCD(a;a;a)
THM	gcd_p_zero	a:. GCD(a;0;a)
THM	gcd_p_one	a:. GCD(a;1;1)
THM	gcd_p_zero_rel	a,b:. GCD(a;0;b)  a = b  a = -b
THM	gcd_p_sym	a,b,y:. GCD(a;b;y)  GCD(b;a;y)
THM	gcd_p_sym_a	a,b,y:. GCD(a;b;y)  GCD(b;a;y)
THM	gcd_p_neg_arg	a,b,y:. GCD(a;b;y)  GCD(a;-b;y)
THM	gcd_p_neg_arg_a	a,b,y:. GCD(a;b;y)  GCD(-a;b;y)
THM	gcd_p_neg_arg_2	a,b,y:. GCD(a;b;y)  GCD(a;-b;y)
THM	gcd_p_shift	a,b,y,k:. GCD(a;b;y)  GCD(a;b+ka;y)
THM	gcd_unique	a,b,y1,y2:. GCD(a;b;y1)  GCD(a;b;y2)  (y1 ~ y2)
THM	gcd_of_triple	a,b,c,x,y:. GCD(a;b;x) GCD(x;c;y)  y | a & y | b & y | c & (z:. z | a  z | b  z | c  z | y)
def	gcd	gcd(a;b) == if b=0 a else gcd(b;a rem b) fi  (recursive)
THM	gcd_sat_gcd_p	a,b:. GCD(a;b;gcd(a;b))
THM	gcd_sat_pred	a,b:. GCD(a;b;gcd(a;b))
THM	gcd_elim	a,b:. y:. GCD(a;b;y) & gcd(a;b) = y
THM	gcd_sym	a,b:. gcd(a;b) ~ gcd(b;a)
THM	gcd_is_divisor_1	a,b:. gcd(a;b) | a
THM	gcd_is_divisor_2	a,b:. gcd(a;b) | b
THM	gcd_is_gcd	a,b,c:. c | a  c | b  c | gcd(a;b)
COM	quot_rem_exists_com	The q and r computed by the extracts of these theorems are not the same as those returned by the divides(a;b) and remainder(a;b) built-in arithmetic functions: ...
THM	quot_rem_exists_n	a:, b:. q:, r:b. a = qb+r
THM	quot_rem_exists	a:, b:. q:, r:b. a = qb+r
THM	gcd_exists_n	b:, a:. y:. GCD(a;b;y)
THM	gcd_ex_n	b:, a:. y:. GCD(a;b;y)
THM	gcd_exists	a,b:. y:. GCD(a;b;y)
THM	bezout_ident_n	b:, a:. u,v:. GCD(a;b;ua+vb)
THM	bezout_ident	a,b:. u,v:. GCD(a;b;ua+vb)
THM	gcd_p_mul	a,b,y,n:. GCD(a;b;y)  GCD(na;nb;ny)
THM	gcd_mul	a,b,n:. (ngcd(a;b)) ~ gcd(na;nb)
THM	gcd_assoc	a,b,c:. gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c))
def	coprime	CoPrime(a,b) == GCD(a;b;1)
THM	sq_stable__coprime	i,j:. SqStable(CoPrime(i,j))
COM	prime_com	We follow a more abstract characterization of primeness here, defining separately notions of primeness and irreducibility. ...
def	reducible	reducible(a) == b,c:. (b ~ 1) & (c ~ 1) & a = bc
def	atomic	atomic(a) == a = 0 & (a ~ 1) & reducible(a)
COM	atomic_char_com	This theorem was quite tedious to prove. ...
THM	atomic_char	a:. atomic(a)  (a ~ 1) & (b:. b | a  (b ~ 1)  (b ~ a))
def	prime	prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc  a | b  a | c)
THM	self_divisor_mul	a:, b:. ab | a  (b ~ 1)
THM	prime_imp_atomic	a:. prime(a)  atomic(a)
THM	prime_elim	p:. prime(p)  p = 0 & (p ~ 1) & (a:. a | p  (a ~ 1)  (a ~ p))
THM	coprime_intro	a,b:. (c:. c | a  c | b  c | 1)  CoPrime(a,b)
THM	coprime_elim	a,b:. CoPrime(a,b)  (c:. c | a  c | b  (c ~ 1))
THM	coprime_elim_a	a,b:. CoPrime(a,b)  (gcd(a;b) ~ 1)
THM	coprime_iff_ndivides	a,p:. prime(p)  (CoPrime(p,a)  p | a)
THM	coprime_bezout_id0	a,b:. CoPrime(a,b)  (x,y:. (ax+by) ~ 1)
THM	coprime_bezout_id1	a,b:. CoPrime(a,b)  (x,y:. ax+by = 1)
THM	coprime_bezout_id2	a,b:. (x,y:. ax+by = 1)  CoPrime(a,b)
THM	coprime_bezout_id	a,b:. CoPrime(a,b)  (x,y:. ax+by = 1)
THM	coprime_prod	a,b1,b2:. CoPrime(a,b1)  CoPrime(a,b2)  CoPrime(a,b1b2)
THM	coprime_divisors_prod	a1,a2,b:. CoPrime(a1,a2)  a1 | b  a2 | b  a1a2 | b
THM	atomic_imp_prime	a:. atomic(a)  prime(a)
THM	prime_divs_prod	p:. prime(p)  (a1,a2:. p | a1a2  p | a1  p | a2)
def	eqmod	a = b mod m == m | a-b
THM	eqmod_weakening	m,a,b:. a = b  (a = b mod m)
THM	eqmod_transitivity	m,a,b,c:. (a = b mod m)  (b = c mod m)  (a = c mod m)
THM	eqmod_inversion	m,a,b:. (a = b mod m)  (b = a mod m)
THM	eqmod_functionality_wrt_eqmod	m,m',a,a',b,b':. m = m' (a = a' mod m)  (b = b' mod m)  ((a = b mod m)  (a' = b' mod m'))
THM	eqmod_fun	m,a,a',b,b':. (a = a' mod m)  (b = b' mod m)  ((a = b mod m)  (a' = b' mod m))
THM	add_functionality_wrt_eqmod	m,a,a',b,b':. (a = a' mod m)  (b = b' mod m)  ((a+b) = (a'+b') mod m)
THM	multiply_functionality_wrt_eqmod	m,a,a',b,b':. (a = a' mod m)  (b = b' mod m)  ((ab) = (a'b') mod m)
COM	chrem_com	Here is the existential half of the chinese remainder theorem for pairs of integers. ...
THM	chrem_exists_aux	r,s:. CoPrime(r,s)  (x:. (x = 1 mod r) & (x = 0 mod s))
THM	chrem_exists_aux_a	r:, s:{s':| CoPrime(r,s') }. x:. ((x = 1 mod r) & (x = 0 mod s))
THM	chrem_exists	r,s:. CoPrime(r,s)  (a,b:. x:. (x = a mod r) & (x = b mod s))
THM	chrem_exists_a	r:, s:{s':| CoPrime(r,s') }, a,b:. x:. ((x = a mod r) & (x = b mod s))
def	fib	fib(n) == if n=0  n=1 1 else fib(n-1)+fib(n-2) fi  (recursive)
THM	fib_coprime	n:. CoPrime(fib(n),fib(n+1))

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html