Def AB == B<A

is mentioned by

Thm* 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]
Thm* L:Top List, n:. ||L||n  (firstn(n;L) ~ L)	[firstn_all]
Thm* t',m:, T:Type, f:(T), P:(T). Thm* m+1||filter(P;map(f;upto(t')))|| Thm*  Thm* (t:. P(f(t)) & ||filter(P;map(f;upto(t)))|| = m  )	[filter_map_upto2]
Thm* i,j:. ij  upto(i)  upto(j)	[upto_iseg]
Thm* f:(A), L:A List. 0<||L||  (aL.(xL.f(x)f(a)))	[maximal-in-list]

In prior sections: int 1 bool 1 int 2 list 1 mb nat mb list 1 num thy 1 core

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