x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type, f:(A
B(T List)).
Thm* (rcv(l; tg) = k
T = B)
Thm*
Thm* @source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)
Dsys
Thm* & (
D:Dsys.
Thm* & (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)
D
Thm* & (
Thm* & (D
Thm* & (realizes es.(vartype(source(l);x)
r A)
Thm* & (realizes es.& (
e:E.
Thm* & (realizes es.& (loc(e) = source(l)
Id
Thm* & (realizes es.& (
Thm* & (realizes es.& (kind(e) = k
Knd (valtype(e) r B))
Thm* & (realizes es.& (
e:E. kind(e) = rcv(l; tg) Knd (valtype(e) r T))
Thm* & (realizes es.& (
e:E.
Thm* & (realizes es.& (loc(e) = source(l)
Id
Thm* & (realizes es.& (
Thm* & (realizes es.& (kind(e) = k
Knd
Thm* & (realizes es.& (
Thm* & (realizes es.& ((
L:{e':E| kind(e') = rcv(l; tg) Knd } List.
Thm* & (realizes es.& (((
e':E.
Thm* & (realizes es.& ((((e'
L)
Thm* & (realizes es.& (((
Thm* & (realizes es.& (((kind(e') = rcv(l; tg)
Knd & sender(e') = e E)
Thm* & (realizes es.& ((& (
e1,e2:E. e1 before e2 L (e1 <loc e2))
Thm* & (realizes es.& ((& map(
e'.val(e');L) = f((x when e),val(e)) T List)))i:Id, k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:k: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* @i: ma-single-sends(ds; da; k; l; f)
Dsys
Thm* & (
D:Dsys.
Thm* & (@i: ma-single-sends(ds; da; k; l; f)
D
Thm* & (
Thm* & (D
Thm* & (realizes es.(
x:Id. vartype(i;x) r ds(x)?Top)
Thm* & (realizes es.& (
e:E.
Thm* & (realizes es.& (loc(e) = i
Id
Thm* & (realizes es.& (
Thm* & (realizes es.& ((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)))eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top.
Thm* f
g(x)?z ~ if x dom(f)
f(x)?z else g(x)?z fieq:EqDecider(A), x,y:A, v:Top. x dom(y : v) x = yes:ES, l:IdLnk, tg:Id, e:E.
Thm* isrcv(e)
lnk(e) = l tag(e) = tg kind(e) = rcv(l; tg)f: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||es:ES, l:IdLnk, tg:Id, e:E.
Thm* kind(e) = rcv(l; tg)
Thm*
Thm* isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l)
l:T List. (l @ nil) ~ las:Top List, f,g:Top. map(g;map(f;as)) ~ map(g o f;as)L:Top List. map(x.x;L) ~ LT:Type, L:T List, P:(TProp). (xL.P(x)) L {x:T| P(x) } Lista:T List, x:T', f:(TT'). (x map(f;a)) (y:T. (y a) & x = f(y))a,b:Knd. a = b a = b