Nuprl - mb_event_system_4 Citations of pi1

mb event system 4 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def 1of(t) == t.1

is mentioned by

Def ma-sframe-compatible(A; B)
Def == kl:(KndIdLnk), tg:Id.
Def == (kl  dom(1of(2of(2of(2of(2of(2of(A)))))))
Def == (
Def == ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(A))))))(kl)))
Def == (
Def == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A)))))))))
Def == (
Def == (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B)))))))))
Def == (
Def == (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of(
Def == (deq-member(KindDeq;1of(kl);1of(B))))))))(<2of(kl),tg>)))
Def == & (kl  dom(1of(2of(2of(2of(2of(2of(B)))))))
Def == & (
Def == & ((tg  map(p.1of(p);1of(2of(2of(2of(2of(2of(B))))))(kl)))
Def == & (
Def == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(B)))))))))
Def == & (
Def == & (<2of(kl),tg>  dom(1of(2of(2of(2of(2of(2of(2of(2of(A)))))))))
Def == & (
Def == & (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of(
Def == & (deq-member(KindDeq;1of(kl);1of(A))))))))(<2of(kl),tg>))) [ma-sframe-compatible]

Def ma-frame-compatible(A; B)
Def == kx:(KndId).
Def == (kx  dom(1of(2of(2of(2of(2of(A))))))
Def == (
Def == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A))))))))
Def == (
Def == (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B))))))))
Def == (
Def == (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of(
Def == (deq-member(KindDeq;1of(kx);1of(B)))))))(2of(kx))))
Def == & (kx  dom(1of(2of(2of(2of(2of(B))))))
Def == & (
Def == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(B))))))))
Def == & (
Def == & (2of(kx)  dom(1of(2of(2of(2of(2of(2of(2of(A))))))))
Def == & (
Def == & (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of(
Def == & (deq-member(KindDeq;1of(kx);1of(A)))))))(2of(kx)))) [ma-frame-compatible]

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 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 == mk-ma(1of(M1)  1of(M2);
Def == mk-ma(1of(2of(M1))  1of(2of(M2));
Def == mk-ma(1of(2of(2of(M1)))  1of(2of(2of(M2)));
Def == mk-ma(1of(2of(2of(2of(M1))))  1of(2of(2of(2of(M2))));
Def == mk-ma(1of(2of(2of(2of(2of(M1)))))  1of(2of(2of(2of(2of(M2)))));
Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(2of(2of(2of(2of(2of(
Def == mk-ma(1of(2of(2of(2of(2of(2of(M1))))))  1of(M2))))));
Def == mk-ma(1of(2of(2of(2of(2of(2of(2of(
Def == mk-ma(1of(M1)))))))  1of(2of(2of(2of(2of(2of(2of(M2)))))));
Def == mk-ma(1of(2of(2of(2of(2of(2of(2of(2of(
Def == mk-ma(1of(M1))))))))  1of(2of(2of(2of(2of(2of(2of(2of(M2))))))))) [ma-join]

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

Def ma-is-empty(M)
Def == fpf-is-empty(1of(M))fpf-is-empty(1of(2of(M)))
Def == fpf-is-empty(1of(2of(2of(M))))fpf-is-empty(1of(2of(2of(2of(M)))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(M))))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(M)))))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(M))))))))
Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(2of(M))))))))) [ma-is-empty]

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 M.sframe(k sends <l,tg>)
Def == L != 1of(2of(2of(2of(2of(2of(2of(2of(
Def == L != 1of(M))))))))(<l,tg>) ==> deq-member(KindDeq;k;L) [ma-sframe]

Def M.frame(k affects x)
Def == L != 1of(2of(2of(2of(2of(2of(2of(M)))))))(x) ==> deq-member(KindDeq;k;L) [ma-frame]

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

Def M.send(k;l;s;v;ms;i)
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ms
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> =
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if source(l) = i
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if concat(map(tgf.
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if map(x.
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;2of(tgf)
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;(s
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;,v));L))
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> else nil fi
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (tg:Id
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if source(l) = i
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (if M.da(rcv(l; tg))
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (else Top fi) List [ma-send]

Def tagged-list-messages(s;v;L)
Def == concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)(s,v));L)) [tagged-list-messages]

Def M.ef(k,x,s,v,w)
Def == E != 1of(2of(2of(2of(2of(M)))))(<k,x>) ==> w = E(s,v)  M.ds(x) [ma-ef]

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

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 M.V(k) == ma-valtype(1of(2of(M)); k) [ma-v]

Def M.state == State(1of(M)) [ma-st]

Def M.init(x,v) == x0 != 1of(2of(2of(M)))(x) ==> v = x0  1of(M)(x)?Void [ma-init]

Def M.dout(l,tg) == 1of(2of(M))(rcv(l; tg))?Void [ma-dout]

Def M.din(l,tg) == 1of(2of(M))(rcv(l; tg))?Top [ma-din]

Def ma-outlinks(M;i) == da-outlinks(1of(2of(M));i) [ma-outlinks]

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

Def M.da(a) == 1of(2of(M))(a)?Top [ma-da]

Def M.ds(x) == 1of(M)(x)?Top [ma-ds]

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]

Def fpf-dom-list(f) == 1of(f) [fpf-dom-list]

Def f  g == <1of(f) @ filter(a.a  dom(f);1of(g)),a.f(a)?g(a)> [fpf-join]

In prior sections: core mb list 1 mb event system 1 mb event system 2 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 ma-sframe-compatible(A; B) Def == kl:(KndIdLnk), tg:Id. Def == (kl dom(1of(2of(2of(2of(2of(2of(A))))))) Def == ( Def == ((tg map(p.1of(p);1of(2of(2of(2of(2of(2of(A))))))(kl))) Def == ( Def == (<2of(kl),tg> dom(1of(2of(2of(2of(2of(2of(2of(2of(A))))))))) Def == ( Def == (<2of(kl),tg> dom(1of(2of(2of(2of(2of(2of(2of(2of(B))))))))) Def == ( Def == (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of( Def == (deq-member(KindDeq;1of(kl);1of(B))))))))(<2of(kl),tg>))) Def == & (kl dom(1of(2of(2of(2of(2of(2of(B))))))) Def == & ( Def == & ((tg map(p.1of(p);1of(2of(2of(2of(2of(2of(B))))))(kl))) Def == & ( Def == & (<2of(kl),tg> dom(1of(2of(2of(2of(2of(2of(2of(2of(B))))))))) Def == & ( Def == & (<2of(kl),tg> dom(1of(2of(2of(2of(2of(2of(2of(2of(A))))))))) Def == & ( Def == & (deq-member(KindDeq;1of(kl);1of(2of(2of(2of(2of(2of(2of(2of( Def == & (deq-member(KindDeq;1of(kl);1of(A))))))))(<2of(kl),tg>)))	[ma-sframe-compatible]
Def ma-frame-compatible(A; B) Def == kx:(KndId). Def == (kx dom(1of(2of(2of(2of(2of(A)))))) Def == ( Def == (2of(kx) dom(1of(2of(2of(2of(2of(2of(2of(A)))))))) Def == ( Def == (2of(kx) dom(1of(2of(2of(2of(2of(2of(2of(B)))))))) Def == ( Def == (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of( Def == (deq-member(KindDeq;1of(kx);1of(B)))))))(2of(kx)))) Def == & (kx dom(1of(2of(2of(2of(2of(B)))))) Def == & ( Def == & (2of(kx) dom(1of(2of(2of(2of(2of(2of(2of(B)))))))) Def == & ( Def == & (2of(kx) dom(1of(2of(2of(2of(2of(2of(2of(A)))))))) Def == & ( Def == & (deq-member(KindDeq;1of(kx);1of(2of(2of(2of(2of(2of(2of( Def == & (deq-member(KindDeq;1of(kx);1of(A)))))))(2of(kx))))	[ma-frame-compatible]
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 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 == mk-ma(1of(M1) 1of(M2); Def == mk-ma(1of(2of(M1)) 1of(2of(M2)); Def == mk-ma(1of(2of(2of(M1))) 1of(2of(2of(M2))); Def == mk-ma(1of(2of(2of(2of(M1)))) 1of(2of(2of(2of(M2)))); Def == mk-ma(1of(2of(2of(2of(2of(M1))))) 1of(2of(2of(2of(2of(M2))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(M1)))))) 1of(2of(2of(2of(2of(2of( Def == mk-ma(1of(2of(2of(2of(2of(2of(M1)))))) 1of(M2)))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(2of( Def == mk-ma(1of(M1))))))) 1of(2of(2of(2of(2of(2of(2of(M2))))))); Def == mk-ma(1of(2of(2of(2of(2of(2of(2of(2of( Def == mk-ma(1of(M1)))))))) 1of(2of(2of(2of(2of(2of(2of(2of(M2)))))))))	[ma-join]
Def M1 \|\|decl M2 == 1of(M1) \|\| 1of(M2) & 1of(2of(M1)) \|\| 1of(2of(M2))	[ma-compatible-decls]
Def ma-is-empty(M) Def == fpf-is-empty(1of(M))fpf-is-empty(1of(2of(M))) Def == fpf-is-empty(1of(2of(2of(M))))fpf-is-empty(1of(2of(2of(2of(M))))) Def == fpf-is-empty(1of(2of(2of(2of(2of(M)))))) Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(M))))))) Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(M)))))))) Def == fpf-is-empty(1of(2of(2of(2of(2of(2of(2of(2of(M)))))))))	[ma-is-empty]
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 M.sframe(k sends <l,tg>) Def == L != 1of(2of(2of(2of(2of(2of(2of(2of( Def == L != 1of(M))))))))(<l,tg>) ==> deq-member(KindDeq;k;L)	[ma-sframe]
Def M.frame(k affects x) Def == L != 1of(2of(2of(2of(2of(2of(2of(M)))))))(x) ==> deq-member(KindDeq;k;L)	[ma-frame]
Def M sends on link l Def == deq-member(IdLnkDeq;l;map(p. Def == 2of(p);1of(1of(2of(2of(2of(2of(2of(M)))))))))	[ma-sends-on]
Def M.send(k;l;s;v;ms;i) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> ms Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> = Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if source(l) = i Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if concat(map(tgf. Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if map(x. Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;2of(tgf) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;(s Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> if <1of(tgf),x>;,v));L)) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> else nil fi Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> (tg:Id Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> (if source(l) = i Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> (if M.da(rcv(l; tg)) Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==> (else Top fi) List	[ma-send]
Def tagged-list-messages(s;v;L) Def == concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)(s,v));L))	[tagged-list-messages]
Def M.ef(k,x,s,v,w) Def == E != 1of(2of(2of(2of(2of(M)))))(<k,x>) ==> w = E(s,v) M.ds(x)	[ma-ef]
Def M.pre(a,s,v) == P != 1of(2of(2of(2of(M))))(a) ==> P(s,v)	[ma-pre]
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 M.V(k) == ma-valtype(1of(2of(M)); k)	[ma-v]
Def M.state == State(1of(M))	[ma-st]
Def M.init(x,v) == x0 != 1of(2of(2of(M)))(x) ==> v = x0 1of(M)(x)?Void	[ma-init]
Def M.dout(l,tg) == 1of(2of(M))(rcv(l; tg))?Void	[ma-dout]
Def M.din(l,tg) == 1of(2of(M))(rcv(l; tg))?Top	[ma-din]
Def ma-outlinks(M;i) == da-outlinks(1of(2of(M));i)	[ma-outlinks]
Def a declared in M == locl(a) dom(1of(2of(M)))	[ma-decla]
Def M.da(a) == 1of(2of(M))(a)?Top	[ma-da]
Def M.ds(x) == 1of(M)(x)?Top	[ma-ds]
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]
Def fpf-dom-list(f) == 1of(f)	[fpf-dom-list]
Def f g == <1of(f) @ filter(a.a dom(f);1of(g)),a.f(a)?g(a)>	[fpf-join]