2. da : a:Knd fp-> Type
3. init : x:Id fp-> ds(x)?Void
4. pre : a:Id fp-> State(ds)
da(locl(a))?TopProp
5. ef : kx:Knd
Id fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send :
6. kl:Knd
IdLnk fp-> (tg:Id
6. kl:Knd
IdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:Knd
IdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. frame : x:Id fp-> Knd List
8. sframe : ltg:IdLnk
Id fp-> Knd List
9. A8 : Top
10. d1 : x:Id fp-> Type
11. d2 : a:Knd fp-> Type
12. i1 : x:Id fp-> d1(x)?Void
13. p1 : a:Id fp-> State(d1)
d2(locl(a))?TopProp
14. e1 : kx:Knd
Id fp-> State(d1)d2(1of(kx))?Topd1(2of(kx))?Void
15. s1 :
15. kl:Knd
IdLnk fp-> (tg:Id
15. kl:Knd
IdLnk fp-> (State(d1)d2(1of(kl))?Top
15. kl:Knd
IdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
16. f1 : x:Id fp-> Knd List
17. s2 : ltg:IdLnk
Id fp-> Knd List
18. B8 : Top
19. <ds,da,init,pre,ef,send,frame,sframe,A8> || <d1,d2,i1,p1,e1,s1,f1,s2,B8>
20. ma-frame-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
20. ma-frame-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
21. ma-sframe-compatible(<ds,da,init,pre,ef,send,frame,sframe,A8>;
21. ma-sframe-compatible(<d1,d2,i1,p1,e1,s1,f1,s2,B8>)
22.
x:Id. x 
dom(ds) 
ds(x)
23.
k:Knd. k dom(da) Dec(da(k))
24.
a:Id. a dom(pre) (s:State(ds). Dec(
v:da(locl(a))?Top. pre(a)(s,v)))
25.
kx:(KndId).
25. kx
dom(ef) L != frame(2of(kx)) ==> deq-member(KindDeq;1of(kx);L)
26.
kl:(KndIdLnk).
26. kl
dom(send)
26.
26. (
tg:Id.
26. ((tg
map(
p.1of(p);send(kl)))
26. (
26. (L != sframe(<2of(kl),tg>) ==> deq-member(KindDeq;1of(kl);L))
27.
x:Id. x dom(d1) d1(x)
28.
k:Knd. k dom(d2) Dec(d2(k))
29.
a:Id. a dom(p1) (s:State(d1). Dec(v:d2(locl(a))?Top. p1(a)(s,v)))
30.
kx:(KndId).
30. kx
dom(e1) L != f1(2of(kx)) ==> deq-member(KindDeq;1of(kx);L)
31.
kl:(KndIdLnk).
31. kl
dom(s1)
31.
31. (
tg:Id.
31. ((tg
map(p.1of(p);s1(kl)))
31. (
31. (L != s2(<2of(kl),tg>) ==> deq-member(KindDeq;1of(kl);L))
32. kx : Knd
Id
33. kx
dom(e1)
34. 2of(kx)
dom(frame)
35. 2of(kx)
dom(frame)
deq-member(KindDeq;1of(kx);frame(2of(kx)))
2of(kx) 
