mb event system 4 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* l:IdLnk, tg:Id, L:Knd List. Feasible(only L sends on (l with tg))[ma-single-sframe-feasible]
Thm* x:Id, L:Knd List, t:Type. t  Feasible(only members of L affect x :t)[ma-single-frame-feasible]
Thm* x:Id, t:Type, v:t. Feasible(x : t initially x = v)[ma-single-init-feasible]
Thm* ltg:(IdLnkIdType), i:Id. (ltg  da-outlinks(;i))  False[da-outlinks-empty]
Thm* A:Type, eq:EqDecider(A), f:a:A fp-> Top.
Thm* fpf-dom-list(f)  {a:A| a  dom(f) } List		[fpf-dom-list_wf]
Thm* eq:EqDecider(A), B:Top, f:a:A fp-> Top.  || f[fpf-empty-compatible-left]
Thm* eq:EqDecider(A), B:Top, f:a:A fp-> Top. f || [fpf-empty-compatible-right]
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]
Thm* eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v) ~ (eqof(eq)(y,x))[fpf-single-dom-sq]
Thm* eq:EqDecider(A), x,y:A, v:Top. x  dom(y : v)  x = y[fpf-single-dom]
Thm* eq:EqDecider(A), x:A, v,P:Top. z != x : v(x) ==> P(a,z) ~ (True  P(x,v))[fpf-val-single1]
Thm* eq:EqDecider(A), x,y:A, v,z:Top.
Thm* x : v(y)?z ~ if eqof(eq)(x,y) v else z fi		[fpf-cap-single]
Thm* eq,x,v:Top. x : v(x) ~ v[fpf-ap-single]
Thm* eq:EqDecider(A), x:A, v,z:Top. x : v(x)?z ~ v[fpf-cap-single1]
Thm* A:Type, B:(AType), x:A, v:B(x). x : v  x:A fp-> B(x)[fpf-single_wf]
Thm* eq:EqDecider(A), f:a:A fp-> Top, g:Top, x:A.
Thm* f  g(x) ~ if x  dom(f) f(x) else g(x) fi		[fpf-join-ap-sq]
Thm* eq:EqDecider(A), f,g:x:A fp-> Top.
Thm* fpf-is-empty(f  g) ~ (fpf-is-empty(f)fpf-is-empty(g))		[fpf-join-is-empty]
Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A.
Thm* x  dom(f  g)  x  dom(f)  x  dom(g)		[fpf-join-dom2]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A.
Thm* x  dom(f  g)  x  dom(f)  x  dom(g)		[fpf-join-dom]
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 unsolvable M.pre(a,s)
Def == P != 1of(2of(2of(2of(M))))(a) ==> v:M.da(locl(a)). P(s,v)		[ma-npre]
Def xdom(f). v=f(x)   P(x;v) == x:A. x  dom(f)  P(x;f(x))[fpf-all]
Def f || g == x:A. x  dom(f) & x  dom(g)  f(x) = g(x)  B(x)[fpf-compatible]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 sqequal 1 mb basic rel 1 mb nat mb list 1 union num thy 1 mb list 2 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