2. a : Id
3. T : Type
4. ds : x:Id fp-> Type
5. P : State(ds)
TProp
6. w : World
7. p1 :
i:Id, t:
, l:IdLnk. 
source(l) = i 
onlnk(l;m(i;t)) = nil
8. p3 :
8.
i:Id, t:. isnull(a(i;t)) (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil
9. p4 :
9. (
i:Id, t:, l:IdLnk.
9. (isrcv(l;a(i;t))
9. (
9. (destination(l) = i & ||queue(l;t)||
1 & hd(queue(l;t)) = msg(a(i;t)))
9. & (
l:IdLnk, t:.
9. & (
t':. t
t' & isrcv(l;a(destination(l);t')) 
queue(l;t') = nil)
10.
i:Id, t:, l:IdLnk. source(l) = i onlnk(l;m(i;t)) = nil
11.
i:Id, t:. isnull(a(i;t)) (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil
12. (
i:Id, t:, l:IdLnk.
12. (isrcv(l;a(i;t))
12. (
12. (destination(l) = i & ||queue(l;t)||
1 & hd(queue(l;t)) = msg(a(i;t)))
12. & (
l:IdLnk, t:.
12. & (
t':. tt' & isrcv(l;a(destination(l);t')) queue(l;t') = nil)
13.
l:IdLnk, tg:Id.
13. (w.M(l,tg))
r if eqof(IdDeq)(source(l),i)
13. (w.M(l,tg))
r if <ds,<[locl(a)],
x.T>,,<[a],x.P>,,,,,
>
13. (w.M(l,tg))
r else fi.da(rcv(l; tg))
14. (eqof(IdDeq)(i,i)) ~ true
15.
a@0:Id, t:.
15.
t':.
15. t
t'
15. &
isnull(a(i;t')) & kind(a(i;t')) = locl(a@0)
15. &
locl(a@0) 
dom(<[locl(a)],x.T>)
15. &
P@0 != <[a],x.P>(a@0) ==> v:<[locl(a)],x.T>(locl(a@0))?Top.
15. &
P@0((x.s(i;t').x),v)
16.
t:.
16.
isnull(a(i;t))
16.
16. (islocal(kind(a(i;t)))
16. (
16. ((eqof(IdDeq)(a,act(kind(a(i;t))))
false)
16. (
16. (P((
x.s(i;t).x),val(a(i;t))))
16. & (
x:Id.
16. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)),x>;1of())
16. & (
16. & (s(i;t+1).x = 2of()(<kind(a(i;t)),x>,
x.s(i;t).x,val(a(i;t))))
16. & (
l:IdLnk.
16. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;1of(
16. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i;t)),l>;))
16. & (
16. & (withlnk(l;m(i;t))
16. & (=
16. & (if source(l) = i
16. & (if concat(map(
tgf.map(x.<1of(tgf)
16. & (if concat(map(
tgf.map(x.,x>;2of(tgf)
16. & (if concat(map(
tgf.map(x.,x>;((x.s(i;t).x)
16. & (if concat(map(
tgf.map(x.,x>;,val(a(i;t))));2of()(<kind(a(i;t)),l>)))
16. & (else nil fi)
16. & (
x:Id.
16. & (
(deq-member(IdDeq;x;1of()) deq-member(KindDeq;kind(a(i;t));2of()(x)))
16. & (
16. & (s(i;t).x = s(i;t+1).x)
16. & (
l:IdLnk, tg:Id.
16. & (
(deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l,tg>;1of())
16. & (
(
16. & (
(deq-member(KindDeq;kind(a(i;t));2of()(<l,tg>)))
16. & (
16. & (w-tagged(tg; onlnk(l;m(i;t))) = nil)
17.
x:Id. deq-member(IdDeq;x;1of()) s(i;0).x = 2of()(x)
18.
a@0:Action(i).
18.
isnull(a@0) (valtype(i;a@0) r <[locl(a)],x.T>(kind(a@0))?Top)
19.
x:Id.
19. vartype(i;x)
r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
20. IdDeq
EqDecider(Id)
21.
x:Id. vartype(i;x) r ds(x)?Top
22. j : Id
23. t :
24. j = i
25.
isnull(a(j;t))
26.
isnull(a(i;t))
27. (
x.s(i;t).x) State(ds)
28. t' :
29. t+1
t'
30.
v:T. P((x.s(i;t').x),v)
31. t2 :
32. t2<t'
33.
isnull(a(i;t2))
34.
t3:. t2<t3 & t3<t' isnull(a(i;t3))
35. t
t2
36. loc(<j,t>) = loc(<i,t2>) & (<j,t> < <i,t2>)
<j,t> = <i,t2>
37. v : T
38.
P((x.s(i;t').x),v)
39. z : Id
40. t3 :
41. 0<t3
42. t2+1
t3
43. t3
t'
44. t2+1
t3-1
45. s(i;t2+1).z = s(i;t3-1).z
46. isnull(a(i;t3-1))
47.
x:Id. s(i;t3-1+1).x = s(i;t3-1).x
48. m(i;t3-1) = nil
49. s(i;t3-1+1).z = s(i;t3-1).z
50.
x:Id. s(i;t3-1+1).x = s(i;t3-1).x
51. m(i;t3-1) = nil
52. s(i;t3-1+1).z = s(i;t3-1).z
s(i;t2+1).z = s(i;t3).z ds(z)?Top
