Def M sends on link l
Def == deq-member(IdLnkDeq;l;map(p.
Def == 2of(p);1of(1of(2of(2of(2of(2of(2of(M)))))))))

is mentioned by

Def d-feasible(D) Def == (i:Id. Feasible(M(i))) Def == & (l:IdLnk, tg:Id. Def == & (M(source(l)).dout(l,tg) r M(destination(l)).din(l,tg)) Def == & (i:Id.  Def == & (finite-type({l:IdLnk Def == & (finite-type({| destination(l) = i & M(source(l)) sends on link l }))

[d-feasible]

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