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.& (
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.& ((
L:{e':E| isrcv(e') & lnk(e') = l IdLnk } List.
Thm* realizes es.& (((
e':E.
Thm* realizes es.& ((((e'
L)
Thm* realizes es.& (((
Thm* realizes es.& (((isrcv(e') & lnk(e') = l
IdLnk & sender(e') = e E)
Thm* realizes es.& ((& (
e1,e2:E. e1 before e2 L (e1 <loc e2))
Thm* realizes es.& ((& map(
e'.<tag(e'),val(e')>;L)
Thm* realizes es.& ((& =
Thm* realizes es.& ((& tagged-list-messages(
z.(z when e);val(e);f)
Thm* realizes es.& ((&
(tg:Idma-valtype(da; rcv(l; tg))) List))i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Type,
Thm*
f:(tg:IdState(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)a:T List, x:T', f:(TT'). (x map(f;a)) (y:T. (y a) & x = f(y))n,i:
. i<n (i upto(n))the_es:ES, e:E. 
(e <loc e)f:(TT'), L:T List, x',y':T'.
Thm* x' before y'
map(f;L) (x,y:T. x before y L & f(x) = x' & f(y) = y')n:, x,y:n. x before y upto(n) x<yP:(TProp), A,B:T List.
Thm* A = B
(i:||A||. P(A[i])) A = B {x:T| P(x) } Listas:Top List, f,g:Top. map(g;map(f;as)) ~ map(g o f;as)a,b:T List. ||a|| = ||b|| 
(i:. i<||a|| a[i] = b[i]) a = bf:Top, T:Type, L:T List, i:||L||. map(f;L)[i] ~ (f(L[i]))f:Top, T:Type, L:T List. ||map(f;L)|| ~ ||L||n:. ||upto(n)|| ~ nm:, n:m. upto(m)[n] = n