Def sender(e) == <source(lnk(kind(e))),mu(t.match(lnk(kind(e));t;time(e)))>

is mentioned by

Thm* the_w:World.  Thm* FairFifo Thm*  Thm* ESAxioms{i:l} Thm* ESAxioms(E; Thm* ESAxioms((i,x. vartype(i;x)); Thm* ESAxioms(the_w.M; Thm* ESAxioms((e.loc(e)); Thm* ESAxioms((e.kind(e)); Thm* ESAxioms((e.val(e)); Thm* ESAxioms((x,e. (x when e)); Thm* ESAxioms((x,e. (x after e)); Thm* ESAxioms((l,e. sends(l;e)); Thm* ESAxioms((e.sender(e)); Thm* ESAxioms((e.index(e)); Thm* ESAxioms((e.first(e)); Thm* ESAxioms((e.pred(e)); Thm* ESAxioms((e,e'. e <c e'))	[world-event-system]
Thm* the_w:World, e:E. Thm* FairFifo  isrcv(kind(e))  index(e)  ||sends(lnk(kind(e));sender(e))||	[w-index_wf]
Def ES(the_w;p) Def == <E Def == ,product-deq(Id;;IdDeq;NatDeq) Def == ,(i,x. vartype(i;x)) Def == ,(i,a. V(i;locl(a))) Def == ,the_w.M Def == , Def == ,(e.loc(e)) Def == ,(e.kind(e)) Def == ,(e.val(e)) Def == ,(x,e. (x when e)) Def == ,(x,e. (x after e)) Def == ,(l,e. sends(l;e)) Def == ,(e.sender(e)) Def == ,(e.index(e)) Def == ,(e.first(e)) Def == ,(e.pred(e)) Def == ,(e,e'. e <c e') Def == ,world_DASH_event_DASH_system{1:l, i:l}(the_w,p) Def == ,>	[w-es]
Def e <c e' == e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^+ e'	[w-causl]
Def index(e) Def == ||rcvs(lnk(kind(e));time(e))||-||snds(lnk(kind(e));time(sender(e)))||	[w-index]

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