2. B : Dsys
3. A
B
4. w : World
5.
i,x:Id. vartype(i;x) r M(i).ds(x)
6.
i:Id, a:Action(i). 
isnull(a) 
(valtype(i;a) r M(i).da(kind(a)))
7.
l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg))
8.
i,x:Id. M(i).init(x,s(i;0).x)
9.
i:Id, t:
.
9.
isnull(a(i;t))
9.
9. (islocal(kind(a(i;t)))
9. (
9. (M(i).pre(act(kind(a(i;t))),
x.s(i;t).x,val(a(i;t))))
9. & (
x:Id. M(i).ef(kind(a(i;t)),x,x.s(i;t).x,val(a(i;t)),s(i;t+1).x))
9. & (
l:IdLnk.
9. & (M(i).send(kind(a(i;t));l;
x.s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
9. & (
x:Id. M(i).frame(kind(a(i;t)) affects x) s(i;t).x = s(i;t+1).x)
9. & (
l:IdLnk, tg:Id.
9. & (
M(i).sframe(kind(a(i;t)) sends <l,tg>)
9. & (
9. & (w-tagged(tg; onlnk(l;m(i;t))) = nil)
10.
i,a:Id, t:.
10.
t':.
10. t
t'
10. &
isnull(a(i;t')) & kind(a(i;t')) = locl(a)
10. &
a declared in M(i)
10. &
unsolvable M(i).pre(a,x.s(i;t').x)
11.
i,x:Id. vartype(i;x) r M(i).ds(x)
12.
i:Id, a:Action(i). isnull(a) (valtype(i;a) r M(i).da(kind(a)))
13.
l:IdLnk, tg:Id. (w.M(l,tg)) r M(source(l)).da(rcv(l; tg))
14.
i,x:Id. M(i).init(x,s(i;0).x)
15. i : Id
16. t :
17.
isnull(a(i;t))
18. (
x.s(i;t).x) 
M(i).state
19. (
x.s(i;t+1).x) M(i).state
20. M(i)
M(i)
21.
x:Id. M(i).ds(x) r M(i).ds(x)
22. islocal(kind(a(i;t)))
23. M(i).pre(act(kind(a(i;t))),
x.s(i;t).x,val(a(i;t)))
valtype(i;a(i;t)) r M(i).da(kind(a(i;t)))
