x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type.
Thm* (rcv(l; tg) = k
T = B)
Thm*
Thm* (
f:(A
BT), c:(AB
).
Thm* (@source(l): ma-single-sends1(A;
Thm* (@source(l): ma-single-sends1(B;
Thm* (@source(l): ma-single-sends1(T;
Thm* (@source(l): ma-single-sends1(x;
Thm* (@source(l): ma-single-sends1(k;
Thm* (@source(l): ma-single-sends1(l;
Thm* (@source(l): ma-single-sends1(tg;
Thm* (@source(l): ma-single-sends1((
a,b. if c(a,b)
[(f(a,b))] else nil fi))
Thm* (
Dsys
Thm* (& (
D:Dsys.
Thm* (& (@source(l): ma-single-sends1(A;
Thm* (& (@source(l): ma-single-sends1(B;
Thm* (& (@source(l): ma-single-sends1(T;
Thm* (& (@source(l): ma-single-sends1(x;
Thm* (& (@source(l): ma-single-sends1(k;
Thm* (& (@source(l): ma-single-sends1(l;
Thm* (& (@source(l): ma-single-sends1(tg;
Thm* (& (@source(l): ma-single-sends1((
a,b. if c(a,b) [(f(a,b))] else nil fi)
Thm* (& (@source(l): ma-single-sends1()
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.& ((c((x when e),val(e))
Thm* (& (realizes es.& ((
Thm* (& (realizes es.& (((
e':E.
Thm* (& (realizes es.& (((kind(e') = rcv(l; tg)
Knd
Thm* (& (realizes es.& (((& sender(e') = e
E
Thm* (& (realizes es.& (((& & (
e'':E.
Thm* (& (realizes es.& (((& & (kind(e'') = rcv(l; tg)
Knd
Thm* (& (realizes es.& (((& & (
Thm* (& (realizes es.& (((& & (sender(e'') = e
E e'' = e' E)
Thm* (& (realizes es.& (((& & val(e') = f((x when e),val(e))
T))
Thm* (& (realizes es.& (& (
c((x when e),val(e))
Thm* (& (realizes es.& (& (
Thm* (& (realizes es.& (& (
(e':E.
Thm* (& (realizes es.& (& (
(kind(e') = rcv(l; tg) Knd
Thm* (& (realizes es.& (& (
(& sender(e') = e E)))))x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type, f:(AB(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)))a,x:T. (x [a]) x = aes: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)
f:Top, T:Type, L:T List. ||map(f;L)|| ~ ||L||