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. p : FairFifo
9. FairFifo
10.
i@0,x@0:Id.
10. vartype(i@0;x@0)
r 1of(if eqof(IdDeq)(i@0,i)
<ds,da,,,<k,x> : f,,,,
>
10. vartype(i@0;x@0)
r 1of(else fi)(x@0)?Top
11.
i@0:Id, a:Action(i@0).
11.
isnull(a)
11.
11. (valtype(i@0;a)
r 1of(2of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
11. (valtype(i@0;a)
r 1of(2of(else fi))(kind(a))?Top)
12.
l:IdLnk, tg:Id.
12. (w.M(l,tg))
r 1of(2of(if eqof(IdDeq)(source(l),i) <ds,da,,,<k,x> : f,,,,>
12. (w.M(l,tg))
r 1of(2of(else fi))(rcv(l; tg))?Top
13.
i@0,x@0:Id.
13. x0 != 1of(2of(2of(if eqof(IdDeq)(i@0,i)
<ds,da,,,<k,x> : f,,,,>
13. x0 != 1of(2of(2of(else fi)))(x@0) ==> s(i@0;0).x@0 = x0
14.
i@0:Id, t:
.
14.
isnull(a(i@0;t))
14.
14. (islocal(kind(a(i@0;t)))
14. (
14. (P != 1of(2of(2of(2of(if eqof(IdDeq)(i@0,i)
<ds,da,,,<k,x> : f,,,,>
14. (P != 1of(2of(2of(2of(else fi))))(act(kind(a(i@0;t)))) ==> P
14. (P != 1of(2of(2of(2of(else fi))))(act(kind(a(i@0;t)))) ==> ((
x.s(i@0;t).x)
14. (P != 1of(2of(2of(2of(else fi))))(act(kind(a(i@0;t)))) ==> ,val(a(i@0;t))))
14. & (
x@0:Id.
14. & (E != 1of(2of(2of(2of(2of(
14. & (E != 1of(if eqof(IdDeq)(i@0,i)
<ds,da,,,<k,x> : f,,,,>
14. & (E != 1of(else fi)))))(<kind(a(i@0;t)),x@0>) ==> s(i@0;t+1).x@0
14. & (E != 1of(else fi)))))(<kind(a(i@0;t)),x@0>) ==> =
14. & (E != 1of(else fi)))))(<kind(a(i@0;t)),x@0>) ==> E
14. & (E != 1of(else fi)))))(<kind(a(i@0;t)),x@0>) ==> ((
x.s(i@0;t).x)
14. & (E != 1of(else fi)))))(<kind(a(i@0;t)),x@0>) ==> ,val(a(i@0;t))))
14. & (
l:IdLnk.
14. & (if eqof(IdDeq)(i@0,i)
<ds,da,,,<k,x> : f,,,,>
14. & (else fi.send(kind(a(i@0;t));l;
x.
14. & (s(i@0;t).x;val(a(i@0;t));withlnk(l;m(i@0;t));i@0))
14. & (
x@0:Id.
14. & (
L != 1of(2of(2of(2of(2of(2of(2of(
14. & (
L != 1of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
14. & (
L != 1of(else fi)))))))(x@0) ==> deq-member(KindDeq;kind(a(i@0;t));L)
14. & (
14. & (s(i@0;t).x@0 = s(i@0;t+1).x@0)
14. & (
l:IdLnk, tg:Id.
14. & (
L != 1of(
14. & (
L != 2of(2of(2of(2of(2of(2of(2of(
14. & (
L != if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
14. & (
L != else fi))))))))(<l,tg>) ==> deq-member(KindDeq;kind(a(i@0;t));L)
14. & (
14. & (w-tagged(tg; onlnk(l;m(i@0;t))) = nil)
15.
x:Id. vartype(i;x) r ds(x)?Top
16.
e:E. loc(e) = i (valtype(e) r ma-valtype(da; kind(e)))
17. j : Id
18. t :
19.
isnull(a(j;t))
20. j = i
21. kind(<j,t>) = k
22. isnull(a(j;t))
(x after <j,t>) = f((z.(z when <j,t>)),val(<j,t>)) 
ds(x)?Top
