Definitions IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
int_segDef  {i..j} == {k:i  k < j }
Thm*  m,n:. {m..n Type
is_assoc_sepDef  is_assoc_sep(Af) == is_assoc(Ax,y.(f(x,y)))
Thm*  f:(AAA). is_assoc_sep(Af Prop
is_identDef  is_ident(Afu) == x:Af(u,x) = x & f(x,u) = x
Thm*  f:(AAA), u:A. is_ident(Afu Prop
iter_via_intsegDef  Iter(f;ui:{a..b}. e(i)
Def  == if a<b f((Iter(f;ui:{a..b-1}. e(i)),e(b-1)) else u fi
Def  (recursive)
Thm*  f:(AAA), u:Aa,b:e:({a..b}A). (Iter(f;ui:{a..b}. e(i))  A
leDef  AB == B<A
Thm*  i,j:. (ij Prop

About:
ifthenelseintnatural_numbersubtractless_thansetapplyfunction
recursive_def_noticeuniverseequalmemberpropandall!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions IteratedBinops Sections DiscrMathExt Doc