1. the_w : World
2. e : E
3. t : 
4. t' : 
5. FairFifo
6. isrcv(kind(e))
7. t<t'
8. f : (Msg List)
  ||concat(map(f;upto(t)))||+||f(t)||||concat(map(f;upto(t')))||

By:	Inst Thm* f:((T List)), t,t':. Thm* t<t'  concat(map(f;upto(t))) @ (f(t))  concat(map(f;upto(t'))) [Msg;f;t;t'] THEN FwdThru Thm* l1,l2:T List. l1  l2  ||l1||||l2|| [-1] THEN RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||   -1

None

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