Definitions mb event system 6 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Some definitions of interest.
possible-worldDef PossibleWorld(D;w)
Def == FairFifo
Def == & (i,x:Id. vartype(i;xr M(i).ds(x))
Def == & & (i:Id, a:Action(i).
Def == & & (isnull(a (valtype(i;ar M(i).da(kind(a))))
Def == & & (l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(ltg)))
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))
ma-declaDef a declared in M == locl(a dom(1of(2of(M)))
ma-npreDef unsolvable M.pre(a,s)
Def == P != 1of(2of(2of(2of(M))))(a) ==> v:M.da(locl(a)). P(s,v)
ma-sendDef 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(ltg))
Def == L != 1of(2of(2of(2of(2of(2of(M))))))(<k,l>) ==>  (else Top fi) List
ma-valtypeDef ma-valtype(dak) == da(k)?Top
Kind-deqDef KindDeq == union-deq(IdLnkId;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq)
w-actionDef Action(i) == action(w-action-dec(w.TA;w.M;i))
worldDef World
Def == T:IdIdType
Def == TA:IdIdType
Def == M:IdLnkIdType
Def == (i:Id(x:IdT(i,x)))(i:Idaction(w-action-dec(TA;M;i)))
Def == (i:Id({m:Msg(M)| source(mlnk(m)) = i } List))Top
Thm* World  Type{i'}
KndDef Knd == (IdLnkId)+Id
Thm* Knd  Type
fair-fifoDef FairFifo
Def == (i:Id, t:l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List)
Def == & (i:Id, t:.
Def == & (isnull(a(i;t))
Def == & (
Def == & ((x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x))
Def == & (& m(i;t) = nil  Msg List)
Def == & (i:Id, t:l:IdLnk.
Def == & (isrcv(l;a(i;t))
Def == & (
Def == & (destination(l) = i
Def == & (& ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))  Msg)
Def == & (l:IdLnk, t:.
Def == & (t':
Def == & (tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List)
w-MsgDef Msg == Msg(w.M)
IdLnkDef IdLnk == IdId
Thm* IdLnk  Type
w-esDef ES(the_w;p)
Def == <E
Def == ,product-deq(Id;;IdDeq;NatDeq)
Def == ,(i,x. vartype(i;x))
Def == ,(i,a. V(i;locl(a)))
Def == ,the_w.M
Def == ,
Def == ,(e.loc(e))
Def == ,(e.kind(e))
Def == ,(e.val(e))
Def == ,(x,e. (x when e))
Def == ,(x,e. (x after e))
Def == ,(l,e. sends(l;e))
Def == ,(e.sender(e))
Def == ,(e.index(e))
Def == ,(e.first(e))
Def == ,(e.pred(e))
Def == ,(e,e'e <c e')
Def == ,world_DASH_event_DASH_system{1:l, i:l}(the_w,p)
Def == ,>
w-causlDef e <c e' == e e,e'e <loc e'  isrcv(kind(e')) & e = sender(e' E^+ e'
w-indexDef index(e)
Def == ||rcvs(lnk(kind(e));time(e))||-||snds(lnk(kind(e));time(sender(e)))||
w-senderDef sender(e) == <source(lnk(kind(e))),mu(t.match(lnk(kind(e));t;time(e)))>
w-sendsDef sends(l;e) == onlnk(l;m(loc(e);time(e)))
w-onlnkDef onlnk(l;mss) == filter(ms.mlnk(ms) = l;mss)
w-withlnkDef withlnk(l;mss) == mapfilter(ms.2of(ms);ms.mlnk(ms) = l;mss)
idlnk-deqDef IdLnkDeq == product-deq(Id;Id;IdDeq;product-deq(Id;;IdDeq;NatDeq))
ma-stateDef State(ds) == x:Idds(x)?Top
w-EDef E == {p:(Id)| isnull(a(1of(p);2of(p))) }
IdDef Id == Atom
Thm* Id  Type
es-valtypeDef valtype(e) == if isrcv(e) rcvtype(e) else acttype(e) fi
w-VDef V(i;k) == kindcase(k;a.1of(2of(w))(i,a);l,tg.1of(2of(2of(w)))(l,tg))
w-valtypeDef valtype(i;a) == kindcase(kind(a);a.w.TA(i,a);l,tg.w.M(l,tg))
actofDef act(k) == outr(k)
Thm* k:Knd. islocal(k act(k Id
d-single-effectDef d-single-effect(idsdakxf)(j)
Def == if eqof(IdDeq)(j,i) ma-single-effect(dsdakxf) else  fi
fpf-valDef z != f(x) ==> P(a;z) == x  dom(f P(x;f(x))
w-taggedDef w-tagged(tgmss) == filter(ms.mtag(ms) = tg;mss)
id-deqDef IdDeq == product-deq(Atom;;AtomDeq;NatDeq)
product-deqDef product-deq(A;B;a;b) == <proddeq(a;b),prod-deq(A;B;a;b)>
assertDef b == if b True else False fi
Thm* b:b  Prop
fpf-capDef f(x)?z == if x  dom(f) f(x) else z fi
deq-memberDef deq-member(eq;x;L) == reduce(a,b. eqof(eq)(a,x b;false;L)
eqofDef eqof(d) == 1of(d)
Thm* T:Type, d:EqDecider(T). eqof(d TT
es-EDef E == 1of(es)
es-afterDef (x after e)
Def == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))))(x,e)
es-kindDef kind(e) == 1of(2of(2of(2of(2of(2of(2of(2of(es))))))))(e)
es-locDef loc(e) == 1of(2of(2of(2of(2of(2of(2of(es)))))))(e)
es-valDef val(e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))(e)
es-vartypeDef vartype(i;x) == 1of(2of(2of(es)))(i,x)
es-whenDef (x when e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es))))))))))(x,e)
fpfDef a:A fp-> B(a) == d:A Lista:{a:A| (a  d) }B(a)
Thm* A:Type, B:(AType). a:A fp-> B(a Type
ma-emptyDef  == mk-ma(; ; ; ; ; ; ; )
fpf-emptyDef  == <nil,x.>
fpf-singleDef x : v == <[x],x.v>
islocalDef islocal(k) == isl(k)
Thm* k:Knd. islocal(k 
natDef  == {i:| 0i }
Thm*   Type
leDef AB == B<A
Thm* i,j:. (ij Prop
loclDef locl(a) == inr(a)
Thm* a:Id. locl(a Knd
lsrcDef source(l) == 1of(l)
Thm* l:IdLnk. source(l Id
nat-deqDef NatDeq == <a,ba=b,nat_DASH_deq_DASH_aux{1:l}>
notDef A == A  False
Thm* A:Prop. (A Prop
w-MDef w.M == 1of(2of(2of(w)))
w-ekindDef kind(e) == kind(act(e))
w-evalDef val(e) == val(act(e))
w-firstDef first(e)
Def == if time(e)=0 true
Def == i; isnull(a(loc(e);time(e)-1)) first(<loc(e),time(e)-1>)
Def == else false fi
Def (recursive)
w-predDef pred(e)
Def == if isnull(a(loc(e);time(e)-1)) pred(<loc(e),time(e)-1>)
Def == else <loc(e),time(e)-1> fi
Def (recursive)
w-aDef a(i;t) == 1of(2of(2of(2of(2of(w)))))(i,t)
w-afterDef (x after e) == s(1of(e);2of(e)+1).x
w-kindDef kind(a) == 1of(outr(a))
w-locDef loc(e) == 1of(e)
w-mDef m(i;t) == 1of(2of(2of(2of(2of(2of(w))))))(i,t)
w-whenDef (x when e) == s(1of(e);2of(e)).x
w-sDef s(i;t).x == 1of(2of(2of(2of(w))))(i,t,x)
w-vartypeDef vartype(i;x) == w.T(i,x)
pi1Def 1of(t) == t.1
Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p A
w-valDef val(a) == 2of(outr(a))
pi2Def 2of(t) == t.2
Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p B(1of(p))
rcvDef rcv(ltg) == inl(<l,tg>)
Thm* l:IdLnk, tg:Id. rcv(ltg Knd
topDef Top == Void given Void
Thm* Top  Type
w-isnullDef isnull(a) == isl(a)

About:
pairspreadspreadproductproductlistconsnilboolbfalsebtrueifthenelse
assertitvoidintnatural_numberaddsubtractless_thanatomunioninlinrset
isectlambdaapplyfunctionrecursive_def_noticeuniverseequalmembertop
subtype_relpropimpliesandorfalsetrueallexists!abstraction
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Definitions mb event system 6 Sections EventSystems Doc