1. ds : x:Id fp-> Type
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:KndId fp-> State(ds)da(1of(kx))?Topds(2of(kx))?Void
6. send : 
6. kl:KndIdLnk fp-> (tg:Id
6. kl:KndIdLnk fp-> (State(ds)da(1of(kl))?Top
6. kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
7. frame : x:Id fp-> Knd List
8. sframe : ltg:IdLnkId fp-> Knd List
9. 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:KndId fp-> State(d1)d2(1of(kx))?Topd1(2of(kx))?Void
15. s1 : 
15. kl:KndIdLnk fp-> (tg:Id
15. kl:KndIdLnk fp-> (State(d1)d2(1of(kl))?Top
15. kl:KndIdLnk fp-> ((d2(rcv(2of(kl); tg))?Void List)) List
16. f1 : x:Id fp-> Knd List
17. s2 : ltg:IdLnkId fp-> Knd List
18. Top
19. ds || d1
20. da || d2
21. init || i1
22. pre || p1
23. ef || e1
24. send || s1
25. frame || f1
26. sframe || s2
27. ds  d1  d1  ds
28. x : Knd
29. x  dom(da  d2)
30. x  dom(d2  da)
  da  d2(x) = d2  da(x)  Type

By:	RWO Thm* B:(AType), eq:EqDecider(A), f,g:a:A fp-> B(a), x:A. Thm* x  dom(f  g)  f  g(x) = if x  dom(f) f(x) else g(x) fi  B(x) 0 THEN Repeat SplitOnConclITE

1	31. x  dom(da) 32. x  dom(d2)   da(x) = d2(x)  Type	1 step
2	31. x  dom(da) 32. x  dom(d2)   d2(x) = da(x)  Type	1 step

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html