mb event system 5 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Feasible(M)
Def == xdom(1of(M)). T=1of(M)(x  T
Def == kdom(1of(2of(M))). T=1of(2of(M))(k  Dec(T)
Def == adom(1of(2of(2of(2of(M))))). p=1of(2of(2of(2of(M))))(a 
Def == &s:State(1of(M)). Dec(v:1of(2of(M))(locl(a))?Top. p(s,v))
Def == kxdom(1of(2of(2of(2of(2of(M)))))). 
Def == ef=1of(2of(2of(2of(2of(M)))))(kx  M.frame(1of(kx) affects 2of(kx))
Def == kldom(1of(2of(2of(2of(2of(2of(M))))))). 
Def == & snd=1of(2of(2of(2of(2of(2of(M))))))(kl  tg:Id. 
Def == & (tg  map(p.1of(p);snd))  M.sframe(1of(kl) sends <2of(kl),tg>)

is mentioned by

Def d-feasible(D)
Def == (i:Id. Feasible(M(i)))
Def == & (l:IdLnk, tg:Id.
Def == & (M(source(l)).dout(l,tgr 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]

In prior sections: mb event system 4

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