Selected Objects

COM	RATIONAL_DEFS	Rational defs for Sup-Inf procedureNIL
def	rat	==
def	qnum	p/q == <p,q>
def	qnumer	q.num == 1of(q)
def	qdenom	q.den == 2of(q)
def	eq_rat	a =q b == a.numb.den=b.numa.den
def	qadd	a +q b == (a.numb.den+b.numa.den)/(a.denb.den)
def	qmul	a *q b == (a.numb.num)/(a.denb.den)
COM	RATIONAL_THMS	NIL
THM	eq_rat_refl	x:. x =q x
THM	eq_rat_sym	x,y:. x =q y  y =q x
THM	eq_rat_trans	x,y,z:. x =q y  y =q z  x =q z
THM	qadd_functionality	p,q,r,s:. p =q q  r =q s  p +q r =q q +q s
THM	qmul_functionality	p,q,r,s:. p =q q  r =q s  p *q r =q q *q s
THM	qmul_assoc	p,q,r:. p *q q *q r =q p *q q *q r
THM	qadd_assoc	p,q,r:. p +q q +q r =q p +q q +q r
THM	qadd_com	p,q:. p +q q =q q +q p
THM	qmul_com	p,q:. p *q q =q q *q p
THM	qmul_dist_over_qadd	a,b,c:. a *q b +q c =q a *q b +q a *q c

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