2. x : Id
3. k : Knd
4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : State(ds)
ma-valtype(da; k)ds(x)?Void
7. w : World
8. FairFifo
9. FairFifo
10.
l:IdLnk, tg:Id.
10. (w.M(l,tg))
r 1of(2of(if eqof(IdDeq)(source(l),i)
<ds,da,,,<k,x> : f,,,,
>
10. (w.M(l,tg))
r 1of(2of(else fi))(rcv(l; tg))?Top
11.
t:
.
11.
isnull(a(i;t))
11.
11. (islocal(kind(a(i;t)))
11. (
11. (P != (act(kind(a(i;t)))) ==> P((
x.s(i;t).x),val(a(i;t))))
11. & (
x@0:Id.
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> s(i;t+1).x@0
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> =
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> E((
x.s(i;t).x),val(a(i;t))))
11. & (
l:IdLnk.
11. & (<ds,da,,,<k,x> : f,,,,
>.send(kind(a(i;t));l;x.
11. & (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
11. & (
x@0:Id.
11. & (
L != (x@0) ==> deq-member(KindDeq;kind(a(i;t));L)
11. & (
11. & (s(i;t).x@0 = s(i;t+1).x@0)
11. & (
l:IdLnk, tg:Id.
11. & (
L != (<l,tg>) ==> deq-member(KindDeq;kind(a(i;t));L)
11. & (
11. & (w-tagged(tg; onlnk(l;m(i;t))) = nil)
12.
x@0:Id. x0 != (x@0) ==> s(i;0).x@0 = x0
13.
a:Action(i). isnull(a) (valtype(i;a) r da(kind(a))?Top)
14. e : E
15. loc(e) = i
16. valtype(i;act(e))
r ma-valtype(da; kind(act(e)))
17.
isnull(act(e))
valtype(loc(e);act(e)) = valtype(i;act(e)) 
Type
