1. x : Id
2. tg : Id
3. k : Knd
4. l : IdLnk
5. T : Type
6. A : Type
7. B : Type
8. rcv(l; tg) = k  T = B
9. f : ABT
10. AB
11. D : Dsys
12. D' : Dsys
13. D  D'
14. w : World
15. p : FairFifo
16. PossibleWorld(D';w)
17. vartype(source(l);x) r A
18. e:E. loc(e) = source(l)  kind(e) = k  (valtype(e) r B)
19. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
20. vartype(source(l);x) r A
21. e:E. loc(e) = source(l)  kind(e) = k  (valtype(e) r B)
22. e:E. kind(e) = rcv(l; tg)  (valtype(e) r T)
23. e : E
24. loc(e) = source(l)
25. kind(e) = k
26. u : {e':E| kind(e') = rcv(l; tg) }
27. e':E. (e'  [u])  kind(e') = rcv(l; tg) & sender(e') = e
28. [val(u)] = [(f((x when e),val(e)))]
29. e' : E
30. kind(e') = rcv(l; tg)
31. e'' : E
32. kind(e'') = rcv(l; tg)
  isrcv(e'')

By:	(FwdThru (Thm* es:ES, l:IdLnk, tg:Id, e:E. (Thm* kind(e) = rcv(l; tg) (Thm*  (Thm* isrcv(e) & lnk(e) = l & tag(e) = tg & loc(sender(e)) = source(l) ([-1]) THEN ExRepD

None

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