Def x:A. B(x) == x:AB(x)

is mentioned by

Thm* M1,M2:MsgA. Thm* M1  M2 Thm*  Thm* (k:Knd, l:IdLnk, tg:Id. Thm* (M2.sframe(k sends <l,tg>)  M1.sframe(k sends <l,tg>))	[ma-sframe-sub]
Thm* M1,M2:MsgA. Thm* M1  M2  (k:Knd, x:Id. M2.frame(k affects x)  M1.frame(k affects x))	[ma-frame-sub]
Thm* M1,M2:MsgA. Thm* M1  M2 Thm*  Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(tg:Id Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if source(l) = i Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(if M2.da(rcv(l; tg)) Thm* (k:Knd, l:IdLnk, s:M2.state, v:M2.da(k), i:Id, ms:(else Top fi) List. Thm* (M2.send(k;l;s;v;ms;i)  M1.send(k;l;s;v;ms;i))	[ma-send-sub]
Thm* M1,M2:MsgA. Thm* M1  M2 Thm*  Thm* (k:Knd, x:Id, s:M2.state, v:M2.da(k), w:M2.ds(x). Thm* (M2.ef(k,x,s,v,w)  M1.ef(k,x,s,v,w))	[ma-ef-sub]
Thm* M1,M2:MsgA. Thm* M1  M2 Thm*  Thm* (a:Id, s:M2.state. Thm* (a declared in M1  unsolvable M2.pre(a,s)  unsolvable M1.pre(a,s))	[ma-npre-sub]
Thm* M1,M2:MsgA. M1  M2  (a:Id. a declared in M1  a declared in M2)	[ma-decla-sub]
Thm* M1,M2:MsgA. Thm* M1  M2 Thm*  Thm* (a:Id, s:M2.state, v:M2.da(locl(a)). M2.pre(a,s,v)  M1.pre(a,s,v))	[ma-pre-sub]
Thm* V:(IdType), M1,M2:MsgA. Thm* (x:Id. V(x) r M2.ds(x)) Thm*  Thm* M1  M2  (x:Id, v:V(x). M2.init(x,v)  M1.init(x,v))	[ma-init-sub]
Thm* M1,M2:MsgA, k:Knd. M1  M2  (M2.da(k) r M1.da(k))	[ma-da-sub]
Thm* M1,M2:MsgA, x:Id. M1  M2  (M2.ds(x) r M1.ds(x))	[ma-ds-sub]
Thm* a:Id, T,A:Type, x:Id, P:(ATProp). Thm* ma-single-pre1(x;A;a;T;x,v.P(x,v))  MsgA	[ma-single-pre1_wf]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp). Thm* (with ds: ds action a:T precondition a(v) is P s v)  MsgA	[ma-single-pre_wf]
Thm* x,y:Id, k:Knd, A,B,T:Type, f:(ABTA). Thm* y = x  ma-single-effect1(x;A;y;B;k;T;f)  MsgA	[ma-single-effect1_wf]
Thm* x:Id, k:Knd, A,T:Type, f:(ATA). ma-single-effect0(x;A;k;T;f)  MsgA	[ma-single-effect0_wf]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Type, Thm* f:(State(ds)ma-valtype(da; k)ds(x)?Void). Thm* ma-single-effect(ds; da; k; x; f)  MsgA	[ma-single-effect_wf]
Thm* l:IdLnk, tg:Id, L:Knd List. only L sends on (l with tg)  MsgA	[ma-single-sframe_wf]
Thm* x:Id, L:Knd List, t:Type. only members of L affect x :t  MsgA	[ma-single-frame_wf]
Thm* x:Id, t:Type, v:t. x : t initially x = v  MsgA	[ma-single-init_wf]
Thm* A:MsgA. A ||	[ma-empty-compatible-right]
Thm* A:MsgA.  || A	[ma-empty-compatible-left]
Thm* M1,M2:MsgA. M1 || M2  M2  M1  M2	[ma-sub-join-right]
Thm* M1,M2:MsgA. M1 || M2  M2 || M1	[ma-compatible-symmetry]
Thm* M1,M2:MsgA. M1 || M2  Prop{i'}	[ma-compatible_wf]
Thm* ds,ds':ltg:Id fp-> Type. ds  ds'  State(ds')  State(ds)	[ma-state-subtype2]
Thm* ds,ds':ltg:Id fp-> Type. ds  ds'  (State(ds') r State(ds))	[ma-state-subtype]
Thm* M1,M2:MsgA. M1  M1  M2	[ma-sub-join-left]
Thm* M1,M2:MsgA. M1 ||decl M2  M1  M2  MsgA	[ma-join_wf]
Thm* A,B:MsgA. ma-is-empty(A)  A  B	[ma-is-empty-sub]
Thm* M:MsgA.   M	[ma-empty-sub]
Thm* M:MsgA. ma-is-empty(M)  M =   MsgA	[assert-ma-is-empty]
Thm* M:MsgA. ma-is-empty(M)	[ma-is-empty_wf]
Thm* M1,M2:MsgA. M1 = M2  M1  M2	[ma-sub_weakening]
Thm* M1,M2,M3:MsgA. M1  M2  M2  M3  M1  M3	[ma-sub_transitivity]
Thm* M1,M2:MsgA. M1  M2  Prop{i'}	[ma-sub_wf]
Thm* M:MsgA, k:Knd, l:IdLnk, tg:Id. M.sframe(k sends <l,tg>)  Prop	[ma-sframe_wf]
Thm* M:MsgA, k:Knd, x:Id. M.frame(k affects x)  Prop	[ma-frame_wf]
Thm* M:MsgA, l:IdLnk. M sends on link l	[ma-sends-on_wf]
Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(tg:Id Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if source(l) = i Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if M.da(rcv Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(if (l; tg)) Thm* M:MsgA, k:Knd, l:IdLnk, s:M.state, v:M.V(k), i:Id, ms:(else Top fi) List. Thm* M.send(k;l;s;v;ms;i)  Prop	[ma-send_wf]
Thm* M:MsgA, k:Knd, s:M.state, v:M.da(k), x:Id, w:M.ds(x). Thm* M.ef(k,x,s,v,w)  Prop	[ma-ef_wf]
Thm* M:MsgA, a:Id, s:M.state, v:M.da(locl(a)). M.pre(a,s,v)  Prop	[ma-pre_wf]
Thm* M:MsgA, a:Id, s:M.state. unsolvable M.pre(a,s)  Prop	[ma-npre_wf]
Thm* M:MsgA, k:Knd. M.V(k)  Type	[ma-v_wf]
Thm* M:MsgA. M.state  Type	[ma-st_wf]
Thm* M:MsgA, x:Id, v:M.ds(x). M.init(x,v)  Prop	[ma-init_wf]
Thm* M:MsgA, l:IdLnk, tg:Id. M.dout(l,tg)  Type	[ma-dout_wf]
Thm* M:MsgA, l:IdLnk, tg:Id. M.din(l,tg)  Type	[ma-din_wf]
Thm* M:MsgA, a:Knd. M.da(a)  Type	[ma-da_wf]
Thm* M:MsgA, i:Id. ma-outlinks(M;i)  (IdLnkIdType) List	[ma-outlinks_wf]
Thm* ltg:(IdLnkIdType), i:Id, da1,da2:k:Knd fp-> Type. Thm* (ltg  da-outlinks(da1  da2;i)) Thm*  Thm* (ltg  da-outlinks(da1;i))  (ltg  da-outlinks(da2;i))	[da-outlinks-join]
Thm* ltg:(IdLnkIdType), i:Id, k:Knd, T:Type. Thm* (ltg  da-outlinks(k : T;i)) Thm*  Thm* isrcv(k) & source(lnk(k)) = i Thm* & (1of(ltg) ~ lnk(k)) Thm* & (1of(2of(ltg)) ~ tag(k)) Thm* & 2of(2of(ltg)) = T	[da-outlinks-single]
Thm* da:k:Knd fp-> Type, i:Id. da-outlinks(da;i)  (IdLnkIdType) List	[da-outlinks_wf]
Thm* da:k:Knd fp-> Type, k:{k:Knd| k  dom(da) & isrcv(k) }. Thm* da-outlink-f(da;k)  IdLnkIdType	[da-outlink-f_wf]
Thm* M:MsgA, a:Id. a declared in M  Prop	[ma-decla_wf]
Thm* M:MsgA, x:Id. M.ds(x)  Type	[ma-ds_wf]
Thm* eq:EqDecider(T), f,g,h:x:T fp-> Type. Thm* f || g Thm*  Thm* h || f Thm*  Thm* h || g Thm*  Thm* g  h  f  g & f  h  f  g & h  g  h  f  g & h  f  h  f  g	[fpf-compatible-triple]
Thm* eq:EqDecider(A), P:(ATypeProp), f,g:x:A fp-> Type. Thm* ydom(f). w=f(y)   P(y,w) Thm*  Thm* ydom(g). w=g(y)   P(y,w)  ydom(f  g). w=f  g(y)   P(y,w)	[fpf-all-join-decl]
Thm* eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a). Thm* f || h  g || h  f  g || h	[fpf-compatible-join2]
Thm* eq:EqDecider(A), B:(AType), f,g:a:A fp-> B(a). f || g  g || f	[fpf-compatible-symmetry]
Thm* eq:EqDecider(A), B:(AType), f,g,h:a:A fp-> B(a). Thm* h || f  h || g  h || f  g	[fpf-compatible-join]
Thm* B:(AType), x:A, v:B(x), eqa:EqDecider(A). x : v  x : v	[fpf-single-sub-reflexive]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f || g  g  f  g	[fpf-sub-join-right]
Thm* B1,B2:(AType), eq:EqDecider(A), f:a:A fp-> B1(a), g:a:A fp-> B2(a). Thm* f  f  g	[fpf-sub-join-left]
Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top. Thm* f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi	[fpf-join-cap-sq]
Thm* B,C:(AType), eq:EqDecider(A), f:a:A fp-> B(a), g:a:A fp-> C(a), x:A. Thm* x  dom(f)  f  g(x) = f(x)  B(x)	[fpf-join-ap-left]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x  dom(f  g)  f  g(x) = if x  dom(f) f(x) else g(x) fi  B(x)	[fpf-join-ap]
Thm* A:Type, B:(AType), f,g:a:A fp-> B(a), eq:EqDecider(A). Thm* f  g  a:A fp-> B(a)	[fpf-join_wf]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. f  g  (f(x)?Void r g(x)?T)	[subtype-fpf-cap-void]
Thm* eq:EqDecider(A), ds:x:A fp-> Type, x:A. ds(x)?Void r ds(x)?Top	[fpf-cap-void-subtype]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type, x:X. g  f  (f(x)?T r g(x)?Top)	[subtype-fpf-cap-top]
Thm* eq:EqDecider(X), f,g:x:X fp-> Type. g  f  (x:X. f(x)?Top r g(x)?Top)	[subtype-fpf-cap]
Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a). f = g  f  g	[fpf-sub_weakening]
Thm* B:(AType), eq:EqDecider(A), f,g,h:a:A fp-> B(a). f  g  g  h  f  h	[fpf-sub_transitivity]
Thm* strong-subtype(A;A') Thm*  Thm* (B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), Thm* (f,g:a:A fp-> B(a). (a:A. B(a) r C(a))  f  g  f  g)	[fpf-sub_functionality]
Thm* strong-subtype(A;A') Thm*  Thm* (B:(AType), C:(A'Type), eq:EqDecider(A), eq':EqDecider(A'), Thm* (f,g:a:A fp-> B(a). (a:A. B(a) r C(a))  f  g  f  g)	[fpf-sub-functionality]
Thm* A:Type, f:a:A fp-> Type, eq:EqDecider(A), x:A, z:Type. f(x)?z  Type	[fpf-cap-wf-univ]
Thm* w:World, p:FairFifo. ES(w)  ES	[w-es_wf]
Thm* B:(AType), f:a:A fp-> B(a). f  a:A fp-> Top	[fpf-trivial-subtype-top]
Thm* A:Type, B:(AType), f:a:A fp-> B(a), eq:EqDecider(A), x:A, z:B(x). Thm* f(x)?z  B(x)	[fpf-cap_wf]
Thm* A:Type, B:(AType), f:a:A fp-> B(a), eq:EqDecider(A), x:A, Thm* P:(a:{a:A| a  dom(f) }B(a)Prop). z != f(x) ==> P(x,z)  Prop	[fpf-val_wf]
Thm* eq:EqDecider(A), B:(AType), x,y:A, v:B(x), u:B(y). Thm* (x = y  v = u  B(x))  x : v || y : u	[fpf-compatible-singles]
Def PossibleWorld(D;w) Def == FairFifo Def == & (i,x:Id. vartype(i;x) r M(i).ds(x)) Def == & & (i:Id, a:Action(i). Def == & & (isnull(a)  (valtype(i;a) r M(i).da(kind(a)))) Def == & & (l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg))) Def == & & (i,x:Id. M(i).init(x,s(i;0).x)) Def == & & (i:Id, t:. Def == & & (isnull(a(i;t)) Def == & & ( Def == & & ((islocal(kind(a(i;t))) Def == & & (( Def == & & ((M(i).pre(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t)))) Def == & & (& (x:Id.  Def == & & (& (M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x)) Def == & & (& (l:IdLnk.  Def == & & (& (M(i).send(kind(a(i;t));l;x. Def == & & (& (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i)) Def == & & (& (x:Id.  Def == & & (& (M(i).frame(kind(a(i;t)) affects x) Def == & & (& ( Def == & & (& (s(i;t).x = s(i;t+1).x  M(i).ds(x)) Def == & & (& (l:IdLnk, tg:Id. Def == & & (& (M(i).sframe(kind(a(i;t)) sends <l,tg>) Def == & & (& ( Def == & & (& (w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List)) Def == & & (i,a:Id, t:. Def == & & (t':.  Def == & & (tt' Def == & & (& isnull(a(i;t')) & kind(a(i;t')) = locl(a) Def == & & (&  a declared in M(i) Def == & & (&  unsolvable M(i).pre(a,x.s(i;t').x))	[possible-world]
Def d-feasible(D) Def == (i:Id. Feasible(M(i))) Def == & (l:IdLnk, tg:Id. Def == & (M(source(l)).dout(l,tg) r M(destination(l)).din(l,tg)) Def == & (i:Id.  Def == & (finite-type({l:IdLnk Def == & (finite-type({| destination(l) = i & M(source(l)) sends on link l }))	[d-feasible]
Def D1  D2 == i:Id. M(i)  M(i)	[d-sub]

In prior sections: core fun 1 well fnd int 1 bool 1 int 2 list 1 sqequal 1 union mb basic rel 1 mb nat mb list 1 num thy 1 mb list 2 mb event system 1 mb event system 2 mb event system 3 mb event system 4

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