Def xdom(f). v=f(x)   P(x;v) == x:A. x  dom(f)  P(x;f(x))

is mentioned by

Thm* eq:EqDecider(A), P:(ATypeProp), x:A, v:Type. Thm* ydom(x : v). w=x : v(y)   P(y,w)  P(x,v)

[fpf-all-single-decl]

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>)

[ma-feasible]

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