| | Some definitions of interest. |
|
| d-realizes | Def D
Def realizes es.P(es)
Def ==  D':Dsys.
Def == D  D'   (w:World, p:FairFifo. PossibleWorld(D';w) P(ES(w))) |
|
| d-sub | Def D1 D2 == i:Id. M(i) M(i) |
|
| dsys | Def Dsys == Id  MsgA |
| | | Thm* Dsys  Type{i'} |
|
| ma-valtype | Def ma-valtype(da; k) == da(k)?Top |
|
| Kind-deq | Def KindDeq == union-deq(IdLnk Id;Id;product-deq(IdLnk;Id;IdLnkDeq;IdDeq);IdDeq) |
|
| Knd | Def Knd == (IdLnkId)+Id |
| | | Thm* Knd Type |
|
| IdLnk | Def IdLnk == IdId |
| | | Thm* IdLnk Type |
|
| es-locl | Def (e <loc e') == loc(e) = loc(e') Id & (e < e') |
|
| ma-state | Def State(ds) == x:Idds(x)?Top |
|
| Id | Def Id == Atom |
| | | Thm* Id Type |
|
| d-single-sends | Def d-single-sends(i; ds; da; k; l; f)(j)
Def == if eqof(IdDeq)(j,i) ma-single-sends(ds; da; k; l; f) else fi |
|
| m-sys-at | Def @i: A(j) == if j = i A else fi |
|
| id-deq | Def IdDeq == product-deq(Atom;;AtomDeq;NatDeq) |
|
| assert | Def  b == if b True else False fi |
| | | Thm* b: . b Prop |
|
| es-E | Def E == 1of(es) |
|
| es-valtype | Def valtype(e) == if isrcv(e) rcvtype(e) else acttype(e) fi |
|
| es-isrcv | Def isrcv(e) == isrcv(kind(e)) |
|
| es-lnk | Def lnk(e) == lnk(kind(e)) |
|
| es-tag | Def tag(e) == tag(kind(e)) |
|
| es-kind | Def kind(e) == 1of(2of(2of(2of(2of(2of(2of(2of(es))))))))(e) |
|
| es-loc | Def loc(e) == 1of(2of(2of(2of(2of(2of(2of(es)))))))(e) |
|
| es-sender | Def sender(e)
Def == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))))))(e) |
|
| es-val | Def val(e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))(e) |
|
| es-vartype | Def vartype(i;x) == 1of(2of(2of(es)))(i,x) |
|
| es-when | Def (x when e) == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es))))))))))(x,e) |
|
| fpf | Def 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 |
|
| fpf-cap | Def f(x)?z == if x dom(f) f(x) else z fi |
|
| iff | Def P  Q == (P Q) & (P Q) |
| | | Thm* A,B:Prop. (A B) Prop |
|
| isrcv | Def isrcv(k) == isl(k) |
| | | Thm* k:Knd. isrcv(k) |
|
| l_before | Def x before y l == [x; y] l |
| | | Thm* T:Type, l:T List, x,y:T. x before y l Prop |
|
| l_member | Def (x l) ==  i:. i<||l|| & x = l[i] T |
| | | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
| lnk | Def lnk(k) == 1of(outl(k)) |
| | | Thm* k:Knd. isrcv(k) lnk(k) IdLnk |
|
| lsrc | Def source(l) == 1of(l) |
| | | Thm* l:IdLnk. source(l) Id |
|
| ma-single-sends | Def ma-single-sends(ds; da; k; l; f) == mk-ma(ds; da; ; ; ; <k,l> : f; ; ) |
|
| tagged-list-messages | Def tagged-list-messages(s;v;L)
Def == concat(map( tgf.map(x.<1of(tgf),x>;2of(tgf)(s,v));L)) |
|
| map | Def map(f;as) == Case of as; nil nil ; a.as' [(f(a)) / map(f;as')]
Def (recursive) |
| | | Thm* A,B:Type, f:(AB), l:A List. map(f;l) B List |
| | | Thm* A,B:Type, f:(AB), l:A List . map(f;l) B List |
|
| rcv | Def rcv(l; tg) == inl(<l,tg>) |
| | | Thm* l:IdLnk, tg:Id. rcv(l; tg) Knd |
|
| tagof | Def tag(k) == 2of(outl(k)) |
| | | Thm* k:Knd. isrcv(k) tag(k) Id |
|
| top | Def Top == Void given Void |
| | | Thm* Top Type |
