| | 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'} |
|
| Knd | Def Knd == (IdLnk Id)+Id |
| | | Thm* Knd Type |
|
| IdLnk | Def IdLnk == IdId |
| | | Thm* IdLnk Type |
|
| Id | Def Id == Atom |
| | | Thm* Id Type |
|
| d-single-sframe | Def @i: only L sends on (l with tg)(j)
Def == if eqof(IdDeq)(j,i) only L sends on (l with tg) else fi |
|
| es-tg-sends | Def sends(l,tg,e) == filter( m.mtag(m) = tg;sends(l;e)) |
|
| m-sys-at | Def @i: A(j) == if j = i A else fi |
|
| assert | Def  b == if b True else False fi |
| | | Thm* b: . b Prop |
|
| es-E | Def E == 1of(es) |
|
| 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) |
|
| l_member | Def (x l) ==  i:. i<||l|| & x = l[i] T |
| | | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
| ma-single-sframe | Def only L sends on (l with tg) == mk-ma(; ; ; ; ; ; ; <l,tg> : L) |
|
| not | Def  A == A False |
| | | Thm* A:Prop. (A) Prop |
|
| null | Def null(as) == Case of as; nil true ; a.as' false |
| | | Thm* T:Type, as:T List. null(as) |
| | | Thm* null(nil) |
