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 ) & e@i.first(e)  (r when e) = false
18. e@i.(r after e) = (r when e)  kind(e) = k
  e@i.kind(e) = k  Knd  (valtype(e) r T) & (vartype(i;x) r A)
  & e@i.first(e)  (r when e) = false  
  & e'@i.(r after e')
  & e'@i.
  & e'@i.(e:E. 
  & e'@i.((e <loc e')  e = e' & kind(e) = k  Knd & P((x when e),val(e)))

By:	EffectRule1 i r x k T  A (r,x,v. P(x,v)  r)

1

17. vartype(i;r) r  18. e@i.first(e)  (r when e) = false   19. e@i.(r after e) = (r when e)    kind(e) = k  Knd 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  Id  kind(e) = k  Knd  (valtype(e) r T) 24. e:E.  24. loc(e) = i  Id 24.  24. kind(e) = k  Knd  (r after e) = (P((x when e),val(e))  (r when e))   e@i.kind(e) = k  Knd  (valtype(e) r T) & (vartype(i;x) r A)   & e@i.first(e)  (r when e) = false     & e'@i.(r after e')   & e'@i.   & e'@i.(e:E.    & e'@i.((e <loc e')  e = e' & kind(e) = k  Knd & P((x when e),val(e)))

61 steps

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