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)))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.& (
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))