mb event system 4 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def deq-member(eq;x;L) == reduce(a,b. eqof(eq)(a,x b;false;L)

is mentioned by

Def ma-sframe-compatible(AB)
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(AB)
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 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]

In prior sections: 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