Def S == {T:Type| x:T. True }

is mentioned by

Thm* 'a,'b:S, x:'a+'b. isr(x)  inr(outr(x)) = x	[inr_houtr]
Thm* 'a,'b:S, x:'a+'b. isl(x)  inl(outl(x)) = x	[inl_houtl]
Thm* 'a,'b:S, x:'a+'b. isl(x)  isr(x)	[isl_or_isr]
Thm* 'c,'b,'a:S, f:('a'c), g:('b'c). Thm* (h:(('a+'b)'c). (x:'a. h(inl(x)) = f(x)) & (x:'b. h(inr(x)) = g(x))) Thm* & (h,y:(('a+'b)'c). Thm* & ((x:'a. h(inl(x)) = f(x)) & (x:'b. h(inr(x)) = g(x)) Thm* & (& (x:'a. y(inl(x)) = f(x)) Thm* & (& (x:'b. y(inr(x)) = g(x)) Thm* & ( Thm* & (h = y)	[sum_axiom_2]
Thm* 'c,'b,'a:S, f:('a'c), g:('b'c). Thm* (h:(('a+'b)'c).  Thm* (h o (x:'a. inl(x)) = f  'a'c & h o (x:'b. inr(x)) = g  'b'c) Thm* & (h,y:(('a+'b)'c). Thm* & (h o (x:'a. inl(x)) = f  'a'c & h o (x:'b. inr(x)) = g  'b'c Thm* & (& y o (x:'a. inl(x)) = f  'a'c Thm* & (& y o (x:'b. inr(x)) = g  'b'c Thm* & ( Thm* & (h = y)	[sum_axiom]
Thm* 'a,'b:S. all(x:hsum('a; 'b). implies(isr(x),equal(inr(outr(x)),x)))	[hinr_houtr]
Thm* 'a,'b:S. all(x:hsum('a; 'b). implies(isl(x),equal(inl(outl(x)),x)))	[hinl_houtl]
Thm* 'a,'b:S. all(x:hsum('a; 'b). or(isl(x),isr(x)))	[hisl_or_isr]
Thm* 'c,'b,'a:S. Thm* all Thm* (f:'a  'c. all Thm* (f:'a  'c. (g:'b  'c. exists_unique Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. and Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. (all Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ((x:'a. equal Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ((x:'a. (h(inl(x)) Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ((x:'a. ,f(x))) Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,all Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,(x:'b. equal Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,(x:'b. (h(inr(x)) Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,(x:'b. ,g(x)))))))	[hsum_axiom_2]
Thm* 'c,'b,'a:S. Thm* all Thm* (f:'a  'c. all Thm* (f:'a  'c. (g:'b  'c. exists_unique Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. and Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. (equal(o(h,inl),f) Thm* (f:'a  'c. (g:'b  'c. (h:hsum('a; 'b)  'c. ,equal(o(h,inr),g)))))	[hsum_axiom]
Thm* 'b,'a:S. all(x:'b. equal(outr(inr(x)),x))	[houtr_wd]
Thm* 'a,'b:S. all(x:'a. equal(outl(inl(x)),x))	[houtl_wd]
Thm* 'a,'b:S. and(all(x:'b. isr(inr(x))),all(y:'a. not(isr(inl(y)))))	[hisr_wd]
Thm* 'b,'a:S. and(all(x:'a. isl(inl(x))),all(y:'b. not(isl(inr(y)))))	[hisl_wd]
Thm* 'a,'b:S. Thm* all Thm* (e:'b. equal Thm* (e:'b. (inr(e) Thm* (e:'b. ,abs_sum(b:hbool. x:'a. y:'b. and(equal(y,e),not(b)))))	[hinr_def]
Thm* 'b,'a:S. Thm* all Thm* (e:'a. equal(inl(e),abs_sum(b:hbool. x:'a. y:'b. and(equal(x,e),b))))	[hinl_def]
Thm* 'a,'b:S. Thm* exists Thm* (rep:hsum('a; 'b)  hbool  'a  'b  hbool. type_definition Thm* (rep:hsum('a; 'b)  hbool  'a  'b  hbool. (is_sum_rep Thm* (rep:hsum('a; 'b)  hbool  'a  'b  hbool. ,rep))	[hsum_ty_def]
Thm* 'a,'b:S, u,v:'a+'b. rep_sum(u) = rep_sum(v)  'a'b  u = v	[hrep_sum_inj]
Thm* 'a,'b:S. Thm* (x:'a+'b. abs_sum(rep_sum(x)) = x  'a+'b) Thm* & (x:('a'b). is_sum_rep(x) = ((rep_sum(abs_sum(x))) = x))	[sum_iso]
Thm* 'a,'b:S. Thm* and Thm* (all(a:hsum('a; 'b). equal(abs_sum(rep_sum(a)),a)) Thm* ,all Thm* ,(r:hbool  'a  'b  hbool. equal Thm* ,(r:hbool  'a  'b  hbool. (is_sum_rep(r) Thm* ,(r:hbool  'a  'b  hbool. ,equal(rep_sum(abs_sum(r)),r))))	[hsum_iso_def]
Thm* 'a,'b:S. Thm* all Thm* (f:hbool Thm* ( 'a Thm* ( 'b Thm* ( hbool. equal Thm* ( hbool. (is_sum_rep(f) Thm* ( hbool. ,exists Thm* ( hbool. ,(v1:'a. exists Thm* ( hbool. ,(v1:'a. (v2:'b. or Thm* ( hbool. ,(v1:'a. (v2:'b. (equal Thm* ( hbool. ,(v1:'a. (v2:'b. ((f Thm* ( hbool. ,(v1:'a. (v2:'b. (,b:hbool. x:'a. y:'b. and(equal(x,v1),b)) Thm* ( hbool. ,(v1:'a. (v2:'b. ,equal Thm* ( hbool. ,(v1:'a. (v2:'b. ,(f Thm* ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. and Thm* ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. (equal(y,v2) Thm* ( hbool. ,(v1:'a. (v2:'b. ,,b:hbool. x:'a. y:'b. ,not(b))))))))	[his_sum_rep_wd]
Thm* 'a,'b:S. hsum('a; 'b)  S	[hsum_wf]
Thm* 'a,'b:S, u:'a+'b. isr(u)  outr(u) = outr(u)	[houtr_nuprl]
Thm* 'a,'b:S, u:'a+'b. isl(u)  outl(u) = outl(u)	[houtl_nuprl]

In prior sections: hol hol min hol bool hol combin

Try larger context: HOLlib IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html