Selected Objects

def	hprod	hprod('a; 'b) == 'a'b
def	hmk_pair	mk_pair == x:'a. y:'b. a:'a. b:'b. (a = x)(b = y)
def	his_pair	is_pair == p:'a'b. x:'a. y:'b. (p = (mk_pair(x,y)))
def	hrep_prod	rep_prod == p:'a'b. mk_pair(1of(p),2of(p))
def	hpair	pair == x:'a. y:'b. <x,y>
def	hfst	fst == p:'a'b. 1of(p)
def	hsnd	snd == p:'a'b. 2of(p)
def	huncurry	uncurry == f:'a'b'c. p:'a'b. f(1of(p),2of(p))
def	hcurry	curry == f:'a'b'c. x:'a. y:'b. f(<x,y>)
THM	hmk_pair_def	'a,'b:S. all (x:'a. all (x:'a. (y:'b. equal(mk_pair(x,y),a:'a. b:'b. and(equal(a,x),equal(b,y)))))
THM	his_pair_def	'a,'b:S. all (p:'a  'b  hbool. equal (p:'a  'b  hbool. (is_pair(p) (p:'a  'b  hbool. ,exists(x:'a. exists(y:'b. equal(p,mk_pair(x,y))))))
THM	hrep_prod_wd	'a,'b:S. equal (rep_prod ,select ,(rep:hprod('a; 'b) ,( 'a ,( 'b ,( hbool. and ,( hbool. (all ,( hbool. ((p':hprod('a; 'b). all ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). implies ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). (equal(rep(p'),rep(p'')) ,( hbool. ((p':hprod('a; 'b). (p'':hprod('a; 'b). ,equal(p',p'')))) ,( hbool. ,all ,( hbool. ,(p:'a  'b  hbool. equal ,( hbool. ,(p:'a  'b  hbool. (is_pair(p) ,( hbool. ,(p:'a  'b  hbool. ,exists ,( hbool. ,(p:'a  'b  hbool. ,(p':hprod('a; 'b). equal(p,rep(p'))))))))
THM	hprod_ty_def	'a,'b:S. exists(rep:hprod('a; 'b)  'a  'b  hbool. type_definition(is_pair,rep))
THM	hcomma_def	'a,'b:S. all (x:'a. all (x:'a. (y:'b. equal (x:'a. (y:'b. (pair(x,y) (x:'a. (y:'b. ,select(p:hprod('a; 'b). equal(rep_prod(p),mk_pair(x,y))))))
THM	hfst_def	'a,'b:S. all (p:hprod('a; 'b). equal (p:hprod('a; 'b). (fst(p) (p:hprod('a; 'b). ,select (p:hprod('a; 'b). ,(x:'a. exists(y:'b. equal(mk_pair(x,y),rep_prod(p))))))
THM	hsnd_def	'a,'b:S. all (p:hprod('a; 'b). equal (p:hprod('a; 'b). (snd(p) (p:hprod('a; 'b). ,select (p:hprod('a; 'b). ,(y:'b. exists(x:'a. equal(mk_pair(x,y),rep_prod(p))))))
THM	huncurry_def	'c,'a,'b:S. all (f:'a  'b  'c. all(x:'a. all(y:'b. equal(uncurry(f,pair(x,y)),f(x,y)))))
THM	hcurry_def	'c,'a,'b:S. all (f:hprod('a; 'b)  'c. all (f:hprod('a; 'b)  'c. (x:'a. all(y:'b. equal(curry(f,x,y),f(pair(x,y))))))
THM	hpair_wd	'a,'b:S. all(x:hprod('a; 'b). equal(pair(fst(x),snd(x)),x))
THM	hfst_pair	'a,'b:S. all(x:'a. all(y:'b. equal(fst(pair(x,y)),x)))
THM	hsnd_pair	'a,'b:S. all(x:'a. all(y:'b. equal(snd(pair(x,y)),y)))
THM	hpair_eq	'a,'b:S. all (b:'b. all (b:'b. (a:'a. all (b:'b. (a:'a. (y:'b. all (b:'b. (a:'a. (y:'b. (x:'a. equal (b:'b. (a:'a. (y:'b. (x:'a. (equal(pair(x,y),pair(a,b)) (b:'b. (a:'a. (y:'b. (x:'a. ,and(equal(x,a),equal(y,b)))))))
THM	pair_wd	'a,'b:S, x:('a'b). <1of(x),2of(x)> = x
THM	fst_pair	'a,'b:S, x:'a, y:'b. x = x
THM	snd_pair	'a,'b:S, x:'a, y:'b. y = y
THM	pair_eq	'a,'b:S, b:'b, a:'a, y:'b, x:'a. <x,y> = <a,b>  x = a & y = b
THM	pair_unfold	'a,'b:S, p:('a'b). p = <1of(p),2of(p)>

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