1. i : Id
2. a : Id
3. x : Id
4. A : Type
5. T : Type
6. P : ATProp
7. @i: (with ds: x : A
7. @action a:T
7. @precondition a(v) is
7. @s,v. P(s(x),v) s v)
7.  Dsys
8. D:Dsys. 
8. @i: (with ds: x : A
8. @action a:T
8. @precondition a(v) is
8. @s,v. P(s(x),v) s v)  D
8. 
8. D 
8. realizes es.(x@0:Id. vartype(i;x@0) r x : A(x@0)?Top)
8. realizes es.& (e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T))
8. realizes es.& (e:E. 
8. realizes es.& (loc(e) = i
8. realizes es.& (
8. realizes es.& ((kind(e) = locl(a)  P((x when e),val(e)))
8. realizes es.& (& (e':E. 
8. realizes es.& (& ((e <loc e')  e = e'
8. realizes es.& (& (& kind(e') = locl(a)  (v:T. P((x after e'),v))))
9. @i: (with ds: x : A
9. @action a:T
9. @precondition a(v) is
9. @s,v. P(s(x),v) s v)
9.  Dsys
10. D : Dsys
11. @i: (with ds: x : A
11. @action a:T
11. @precondition a(v) is
11. @s,v. P(s(x),v) s v)  D
12. D':Dsys. 
12. D  D'
12. 
12. (w:World, p:FairFifo.
12. (PossibleWorld(D';w)
12. (
12. ((x@0:Id. vartype(i;x@0) r x : A(x@0)?Top)
12. (& (e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T))
12. (& (e:E. 
12. (& (loc(e) = i
12. (& (
12. (& ((kind(e) = locl(a)  P((x when e),val(e)))
12. (& (& (e':E. 
12. (& (& ((e <loc e')  e = e'
12. (& (& (& kind(e') = locl(a)  (v:T. P((x after e'),v)))))
13. D' : Dsys
14. D  D'
15. w:World, p:FairFifo.
15. PossibleWorld(D';w)
15. 
15. (x@0:Id. vartype(i;x@0) r x : A(x@0)?Top)
15. & (e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T))
15. & (e:E. 
15. & (loc(e) = i
15. & (
15. & ((kind(e) = locl(a)  P((x when e),val(e)))
15. & (& (e':E. 
15. & (& ((e <loc e')  e = e'
15. & (& (& kind(e') = locl(a)  (v:T. P((x after e'),v))))
16. w : World
17. p:FairFifo. 
17. PossibleWorld(D';w)
17. 
17. (x@0:Id. vartype(i;x@0) r x : A(x@0)?Top)
17. & (e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T))
17. & (e:E. 
17. & (loc(e) = i
17. & (
17. & ((kind(e) = locl(a)  P((x when e),val(e)))
17. & (& (e':E. 
17. & (& ((e <loc e')  e = e'
17. & (& (& kind(e') = locl(a)  (v:T. P((x after e'),v))))
18. p : FairFifo
19. PossibleWorld(D';w)
20. x@0:Id. vartype(i;x@0) r x : A(x@0)?Top
21. e:E. loc(e) = i  kind(e) = locl(a)  (valtype(e) r T)
22. e:E. 
22. loc(e) = i
22. 
22. (kind(e) = locl(a)  P((x when e),val(e)))
22. & (e':E. 
22. & ((e <loc e')  e = e' & kind(e') = locl(a)  (v:T. P((x after e'),v)))
  vartype(i;x) r A

1

23. vartype(i;x) r x : A(x)?Top   vartype(i;x) r A

1 step

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