Nuprl - mb_event_system_4 Citations of locl

mb event system 4 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def locl(a) == inr(a)

is mentioned by

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]

Def (with ds: ds
Def (init: init
Def action a:T
Def aprecondition a(v) is
Def aP)
Def == mk-ma(ds; locl(a) : T; init; a : P; ; ; ; ) [ma-single-pre-init]

Def (with ds: ds
Def (action a:T
Def (precondition a(v) is
Def (P s v)
Def == mk-ma(ds; locl(a) : T; ; a : P; ; ; ; ) [ma-single-pre]

Def M1 || M2
Def == M1 ||decl M2
Def == & 1of(2of(2of(M1))) || 1of(2of(2of(M2)))
Def == & 1of(2of(2of(2of(M1)))) || 1of(2of(2of(2of(M2))))
Def == & 1of(2of(2of(2of(2of(M1))))) || 1of(2of(2of(2of(2of(M2)))))
Def == & 1of(2of(2of(2of(2of(2of(M1)))))) || 1of(2of(2of(2of(2of(2of(M2))))))
Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(2of(2of(2of(2of(2of(2of(
Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) || 1of(M2)))))))
Def == & 1of(2of(2of(2of(2of(2of(2of(2of(
Def == & 1of(M1)))))))) || 1of(2of(2of(2of(2of(2of(2of(2of(M2)))))))) [ma-compatible]

Def M1  M2
Def == 1of(M1)  1of(M2) & 1of(2of(M1))  1of(2of(M2))
Def == & 1of(2of(2of(M1)))  1of(2of(2of(M2)))
Def == & & 1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2))))
Def == & & 1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2)))))
Def == & & 1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(M2))))))
Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(2of(2of(2of(2of(2of(2of(
Def == & & 1of(2of(2of(2of(2of(2of(2of(M1)))))))  1of(M2)))))))
Def == & & 1of(2of(2of(2of(2of(2of(2of(2of(
Def == & & 1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2)))))))) [ma-sub]

Def unsolvable M.pre(a,s)
Def == P != 1of(2of(2of(2of(M))))(a) ==> v:M.da(locl(a)). P(s,v) [ma-npre]

Def a declared in M == locl(a)  dom(1of(2of(M))) [ma-decla]

Def MsgA
Def == ds:x:Id fp-> Type
Def == da:a:Knd fp-> Type
Def == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop
Def == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void
Def == kl:KndIdLnk fp-> (tg:Id
Def == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl))
Def == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
Def == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop [msga]

In prior sections: mb event system 1 mb event system 3

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

mb event system 4 Sections EventSystems Doc

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]
Def (with ds: ds Def (init: init Def action a:T Def aprecondition a(v) is Def aP) Def == mk-ma(ds; locl(a) : T; init; a : P; ; ; ; )	[ma-single-pre-init]
Def (with ds: ds Def (action a:T Def (precondition a(v) is Def (P s v) Def == mk-ma(ds; locl(a) : T; ; a : P; ; ; ; )	[ma-single-pre]
Def M1 \|\| M2 Def == M1 \|\|decl M2 Def == & 1of(2of(2of(M1))) \|\| 1of(2of(2of(M2))) Def == & 1of(2of(2of(2of(M1)))) \|\| 1of(2of(2of(2of(M2)))) Def == & 1of(2of(2of(2of(2of(M1))))) \|\| 1of(2of(2of(2of(2of(M2))))) Def == & 1of(2of(2of(2of(2of(2of(M1)))))) \|\| 1of(2of(2of(2of(2of(2of(M2)))))) Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) \|\| 1of(2of(2of(2of(2of(2of(2of( Def == & 1of(2of(2of(2of(2of(2of(2of(M1))))))) \|\| 1of(M2))))))) Def == & 1of(2of(2of(2of(2of(2of(2of(2of( Def == & 1of(M1)))))))) \|\| 1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))	[ma-compatible]
Def M1 M2 Def == 1of(M1) 1of(M2) & 1of(2of(M1)) 1of(2of(M2)) Def == & 1of(2of(2of(M1))) 1of(2of(2of(M2))) Def == & & 1of(2of(2of(2of(M1)))) 1of(2of(2of(2of(M2)))) Def == & & 1of(2of(2of(2of(2of(M1))))) 1of(2of(2of(2of(2of(M2))))) Def == & & 1of(2of(2of(2of(2of(2of(M1)))))) 1of(2of(2of(2of(2of(2of(M2)))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(M1))))))) 1of(2of(2of(2of(2of(2of(2of( Def == & & 1of(2of(2of(2of(2of(2of(2of(M1))))))) 1of(M2))))))) Def == & & 1of(2of(2of(2of(2of(2of(2of(2of( Def == & & 1of(M1)))))))) 1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))	[ma-sub]
Def unsolvable M.pre(a,s) Def == P != 1of(2of(2of(2of(M))))(a) ==> v:M.da(locl(a)). P(s,v)	[ma-npre]
Def a declared in M == locl(a) dom(1of(2of(M)))	[ma-decla]
Def MsgA Def == ds:x:Id fp-> Type Def == da:a:Knd fp-> Type Def == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop Def == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void Def == kl:KndIdLnk fp-> (tg:Id Def == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl)) Def == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List Def == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop	[msga]