mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
3Thm* the_w:World, e:E.
Thm* FairFifo  isrcv(kind(e))  (t:time(e). match(lnk(kind(e));t;time(e)))		[w-match-exists]
cites the following:
1Thm* r:, L:Top List. ||nth_tl(r;L)|| = if r<||L|| ||L||-r else 0 fi[general_length_nth_tl]
1Thm* m:, L:T List. m<||L||  (nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)])[nth_tl_decomp]
2Thm* ll:(T List) List, n:||concat(ll)||.
Thm* m:||ll||. 
Thm* ||concat(firstn(m;ll))||n
Thm* & n-||concat(firstn(m;ll))||<||ll[m]||
Thm* & concat(ll)[n] = ll[m][(n-||concat(firstn(m;ll))||)]		[select_concat]
0Thm* f:(AB), as:A List. ||map(f;as)|| = ||as||  [map_length]
2Thm* n,m:. firstn(n;upto(m)) ~ if nm upto(n) else upto(m) fi[firstn_upto]
1Thm* f:(TopTop), n:, l:Top List. firstn(n;map(f;l)) ~ map(f;firstn(n;l))[firstn_map]
1Thm* f:(AB), as:A List, n:||as||. map(f;as)[n] = f(as[n])[map_select]
1Thm* n:. ||upto(n)|| ~ n[length_upto]
2Thm* m:, n:m. upto(m)[n] = n[select_upto]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb event system 3 Sections EventSystems Doc