1. T : Type
2. A : Type
3. P : AT
4. k : Knd
5. i : Id
6. r : Id
7. x : Id
8. A
9. T
10. x = r
11. (loc.(recognizer1(loc;T;A;P;k;i;r;x)))  Dsys
12. D' : Dsys
13. loc.(recognizer1(loc;T;A;P;k;i;r;x))  D'
14. w : World
15. p : FairFifo
16. PossibleWorld(D';w)
17. vartype(i;r) r 
18. e:E. loc(e) = i  first(e)  (r when e) = false
19. e:E. loc(e) = i  (r after e) = (r when e)  kind(e) = k
20. @i: ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v)  r)  Dsys
21. vartype(i;r) r 
22. vartype(i;x) r A
23. e:E. loc(e) = i  kind(e) = k  (valtype(e) r T)
24. e:E. 
24. loc(e) = i
24. 
24. kind(e) = k  (r after e) = (P((x when e),val(e))  (r when e))
25. e' : E
26. loc(e') = i
27. first(e')
28. (r after pred(e'))
28. 
28. (e@0:E. 
28. ((e@0 <loc pred(e'))  e@0 = pred(e')
28. (& kind(e@0) = k
28. (& P((x when e@0),val(e@0)))
29. (r when e') = (r after pred(e'))
  (r after e')
  
  (e@0:E. 
  ((e@0 <loc e')  e@0 = e' & kind(e@0) = k  Knd & P((x when e@0),val(e@0)))

1	28. (r after pred(e')) 28.  28. (e@0:E.  28. ((e@0 <loc pred(e'))  e@0 = pred(e')  E 28. (& kind(e@0) = k  Knd 28. (& P((x when e@0),val(e@0))) 29. (r after pred(e'))  (e@0:E.  29. (e@0 <loc pred(e'))  e@0 = pred(e')  E 29. & kind(e@0) = k  Knd 29. & P((x when e@0),val(e@0))) 30. (r when e') = (r after pred(e'))   31. (r after e')   e@0:E.    (e@0 <loc e')  e@0 = e' & kind(e@0) = k  Knd & P((x when e@0),val(e@0))	12 steps
2	28. (r after pred(e')) 28.  28. (e@0:E.  28. ((e@0 <loc pred(e'))  e@0 = pred(e')  E 28. (& kind(e@0) = k  Knd 28. (& P((x when e@0),val(e@0))) 29. (r after pred(e'))  (e@0:E.  29. (e@0 <loc pred(e'))  e@0 = pred(e')  E 29. & kind(e@0) = k  Knd 29. & P((x when e@0),val(e@0))) 30. (r when e') = (r after pred(e'))   31. e@0:E.  31. (e@0 <loc e')  e@0 = e' & kind(e@0) = k  Knd & P((x when e@0),val(e@0))   (r after e')	17 steps

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