Nuprl - mb_event_system_5 Citations of ma-din

mb event system 5 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def M.din(l,tg) == 1of(2of(M))(rcv(l; tg))?Top

is mentioned by

Def interface-check(D;l;tg;T) == T r M(destination(l)).din(l,tg) [interface-check]

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

mb event system 5 Sections EventSystems Doc

Def interface-check(D;l;tg;T) == T r M(destination(l)).din(l,tg)	[interface-check]
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]