| | Some definitions of interest. |
|
| alle-at | Def  e@i.P(e) == e:E. loc(e) = i  Id   P(e) |
|
| 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'} |
|
| Id | Def Id == Atom  |
| | | Thm* Id Type |
|
| es-after | Def (x after e)
Def == 1of(2of(2of(2of(2of(2of(2of(2of(2of(2of(2of(es)))))))))))(x,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) |
|
| m-sys-at | Def @i: A(j) == if j = i A else fi |
|
| ma-single-frame | Def only members of L affect x :t == mk-ma(x : t; ; ; ; ; ; x : L; ) |
