i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm*
f:(tg:Id
State(ds)
ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List.
Thm* source(l) = i
Thm*
Thm* d-single-sends(i; ds; da; k; l; f)
Thm* realizes es.(
x:Id. vartype(i;x) 
r ds(x)?Top)
Thm* realizes es.& (
e:E.
Thm* realizes es.& (loc(e) = i
Id (valtype(e) r ma-valtype(da; kind(e))))
Thm* realizes es.& (
e:E.
Thm* realizes es.& (isrcv(e)
Thm* realizes es.& (
Thm* realizes es.& (lnk(e) = l
IdLnk
Thm* realizes es.& (
Thm* realizes es.& ((valtype(e)
r ma-valtype(da; kind(e))))
Thm* realizes es.& ({m:Msg| source(mlnk(m)) = i }
r Msg
Thm* realizes es.& (((
l,tg. da(rcv(l; tg))?Top)))
Thm* realizes es.& (
e:E.
Thm* realizes es.& (loc(e) = i
Id
Thm* realizes es.& (
Thm* realizes es.& (kind(e) = k
Knd
Thm* realizes es.& (
Thm* realizes es.& (sends(l;e)
Thm* realizes es.& (=
Thm* realizes es.& (tagged-messages(l;
z.(z when e);val(e);f)
Thm* realizes es.& (
Msg((l,tg. da(rcv(l; tg))?Top)) List)D:Dsys, P:({es:ES| es is an event system of D }Prop{i'}).
Thm* D realizes2 es.P(es)
D realizes es.P(es)the_w:World, e:E. act(e) {a:Action(loc(e))| 
isnull(a) } (EqDecider(B) r EqDecider(A))d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true
i:Id, w:World, p:FairFifo, t:
.
Thm*
isnull(a(i;t)) (valtype(<i,t>) ~ valtype(i;a(i;t)))as:Top List, f,g:Top. map(g;map(f;as)) ~ map(g o f;as)T:Type, P:(T
), l:T List. filter(P;l) {x:T| P(x) } Lista:T List, f:(TT). (x:T. (x a) f(x) = x) map(f;a) = af:(AB), l:A List. map(f;l) = nil 
l = nil