Selected Objects

def	hsum	hsum('a; 'b) == 'a+'b
def	hrep_sum	rep_sum == u:'a+'b. InjCase(u == u:'a+'b. InjCase; p. b:. x:'a. y:'b. (x = p)b == u:'a+'b. InjCase; q. b:. x:'a. y:'b. (y = q)b)
def	habs_sum	abs_sum == f:'a'b. @u:'a+'b. (rep_sum(u) = f  'a'b)
def	his_sum_rep	is_sum_rep == f:'a'b. u:'a+'b. (f = (rep_sum(u)))
def	hinl	inl == x:'a. inl(x)
def	hinr	inr == x:'b. inr(x)
def	hisl	isl == u:'a+'b. isl(u)
def	hisr	isr == u:'a+'b. isr(u)
def	houtl	outl == u:'a+'b. InjCase(u; x. x, arb('a))
THM	houtl_nuprl	'a,'b:S, u:'a+'b. isl(u)  outl(u) = outl(u)
def	houtr	outr == u:'a+'b. InjCase(u; x. arb('b), x)
THM	houtr_nuprl	'a,'b:S, u:'a+'b. isr(u)  outr(u) = outr(u)
THM	his_sum_rep_wd	'a,'b:S. all (f:hbool ( 'a ( 'b ( hbool. equal ( hbool. (is_sum_rep(f) ( hbool. ,exists ( hbool. ,(v1:'a. exists ( hbool. ,(v1:'a. (v2:'b. or ( hbool. ,(v1:'a. (v2:'b. (equal ( hbool. ,(v1:'a. (v2:'b. ((f ( hbool. ,(v1:'a. (v2:'b. (,b:hbool. x:'a. y:'b. and(equal(x,v1),b)) ( hbool. ,(v1:'a. (v2:'b. ,equal ( hbool. ,(v1:'a. (v2:'b. ,(f ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. and ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. (equal(y,v2) ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. ,not(b))))))))
THM	hsum_iso_def	'a,'b:S. and (all(a:hsum('a; 'b). equal(abs_sum(rep_sum(a)),a)) ,all ,(r:hbool  'a  'b  hbool. equal ,(r:hbool  'a  'b  hbool. (is_sum_rep(r) ,(r:hbool  'a  'b  hbool. ,equal(rep_sum(abs_sum(r)),r))))
THM	sum_iso	'a,'b:S. (x:'a+'b. abs_sum(rep_sum(x)) = x  'a+'b) & (x:('a'b). is_sum_rep(x) = ((rep_sum(abs_sum(x))) = x))
THM	hrep_sum_inj	'a,'b:S, u,v:'a+'b. rep_sum(u) = rep_sum(v)  'a'b  u = v
THM	hsum_ty_def	'a,'b:S. exists (rep:hsum('a; 'b)  hbool  'a  'b  hbool. type_definition (rep:hsum('a; 'b)  hbool  'a  'b  hbool. (is_sum_rep (rep:hsum('a; 'b)  hbool  'a  'b  hbool. ,rep))
THM	hinl_def	'b,'a:S. all(e:'a. equal(inl(e),abs_sum(b:hbool. x:'a. y:'b. and(equal(x,e),b))))
THM	hinr_def	'a,'b:S. all (e:'b. equal(inr(e),abs_sum(b:hbool. x:'a. y:'b. and(equal(y,e),not(b)))))
THM	hisl_wd	'b,'a:S. and(all(x:'a. isl(inl(x))),all(y:'b. not(isl(inr(y)))))
THM	hisr_wd	'a,'b:S. and(all(x:'b. isr(inr(x))),all(y:'a. not(isr(inl(y)))))
THM	houtl_wd	'a,'b:S. all(x:'a. equal(outl(inl(x)),x))
THM	houtr_wd	'b,'a:S. all(x:'b. equal(outr(inr(x)),x))
THM	hsum_axiom	'c,'b,'a:S. all (f:'a  'c. all (f:'a  'c. (g:'b  'c. exists_unique (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. and (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. (equal(o(h,inl),f) (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,equal(o(h,inr),g)))))
THM	hsum_axiom_2	'c,'b,'a:S. all (f:'a  'c. all (f:'a  'c. (g:'b  'c. exists_unique (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. and (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. (all (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ((x:'a. equal (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ((x:'a. (h(inl(x)) (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ((x:'a. ,f(x))) (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,all (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,(x:'b. equal (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,(x:'b. (h(inr(x)) (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,(x:'b. ,g(x)))))))
THM	hisl_or_isr	'a,'b:S. all(x:hsum('a; 'b). or(isl(x),isr(x)))
THM	hinl_houtl	'a,'b:S. all(x:hsum('a; 'b). implies(isl(x),equal(inl(outl(x)),x)))
THM	hinr_houtr	'a,'b:S. all(x:hsum('a; 'b). implies(isr(x),equal(inr(outr(x)),x)))
THM	sum_axiom	'c,'b,'a:S, f:('a'c), g:('b'c). (h:(('a+'b)'c).  (h o (x:'a. inl(x)) = f  'a'c & h o (x:'b. inr(x)) = g  'b'c) & (h,y:(('a+'b)'c). & (h o (x:'a. inl(x)) = f  'a'c & h o (x:'b. inr(x)) = g  'b'c & (& y o (x:'a. inl(x)) = f  'a'c & (& y o (x:'b. inr(x)) = g  'b'c & ( & (h = y)
THM	sum_axiom_2	'c,'b,'a:S, f:('a'c), g:('b'c). (h:(('a+'b)'c). (x:'a. h(inl(x)) = f(x)) & (x:'b. h(inr(x)) = g(x))) & (h,y:(('a+'b)'c). & ((x:'a. h(inl(x)) = f(x)) & (x:'b. h(inr(x)) = g(x)) & (& (x:'a. y(inl(x)) = f(x)) & (& (x:'b. y(inr(x)) = g(x)) & ( & (h = y)
THM	isl_or_isr	'a,'b:S, x:'a+'b. isl(x)  isr(x)
THM	inl_houtl	'a,'b:S, x:'a+'b. isl(x)  inl(outl(x)) = x
THM	inr_houtr	'a,'b:S, x:'a+'b. isr(x)  inr(outr(x)) = x

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