A,B,T:Type, x:Id, a:Knd, tg:Id, l:IdLnk, f:(AB(T List)).
  (a = rcv(l; tg)  T = B)  ma-single-sends1(A; B; T; x; a; l; tg; f)  MsgA

By:

Auto THEN AssertBY (x : A  x:Id fp-> Type) Auto THEN AssertBY (a : B  x:Knd fp-> Type) Auto THEN Unfold `ma-single-sends1` 0 THEN Try (Fold `ma-state` 0) THEN All (Unfold `ma-valtype`) THEN All (RWO (Thm* eq:EqDecider(A), f,g:a:A fp-> Top, x:A, z:Top. (Thm* f  g(x)?z ~ if x  dom(f) f(x)?z else g(x)?z fi) THEN All Reduce

1	1. A : Type 2. B : Type 3. T : Type 4. x : Id 5. a : Knd 6. tg : Id 7. l : IdLnk 8. AB(T List) 9. a = rcv(l; tg)  T = B 10. x : A  x:Id fp-> Type 11. a : B  x:Knd fp-> Type 12. State(x : A) 13. v : if a  dom(a : B) B else rcv(l; tg) : T(a)?Top fi   v  B	2 steps
2	1. A : Type 2. B : Type 3. T : Type 4. x : Id 5. a : Knd 6. tg : Id 7. l : IdLnk 8. f : AB(T List) 9. a = rcv(l; tg)  T = B 10. x : A  x:Id fp-> Type 11. a : B  x:Knd fp-> Type 12. s : State(x : A) 13. v : if a  dom(a : B) B else rcv(l; tg) : T(a)?Top fi 14. f(s(x),v) = f(s(x),v) 15. T List 16. T List 17. u : T   u  if rcv(l; tg)  dom(a : B) a : B(rcv(l; tg))?Void else T fi	2 steps

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