1. i : Id
2. x : Id
3. k : Knd
4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : State(ds)ma-valtype(da; k)ds(x)?Void
7. w : World
8. p : FairFifo
9. FairFifo
10. l:IdLnk, tg:Id.
10. (w.M(l,tg)) r 1of(2of(if eqof(IdDeq)(source(l),i) <ds,da,,,<k,x> : f,,,,>
10. (w.M(l,tg)) r 1of(2of(else  fi))(rcv(l; tg))?Top
11. t:. 
11. isnull(a(i;t))
11. 
11. (islocal(kind(a(i;t)))
11. (
11. (P != (act(kind(a(i;t)))) ==> P((x.s(i;t).x),val(a(i;t))))
11. & (x@0:Id. 
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> s(i;t+1).x@0
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> =
11. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==> E((x.s(i;t).x),val(a(i;t))))
11. & (l:IdLnk. 
11. & (<ds,da,,,<k,x> : f,,,,>.send(kind(a(i;t));l;x.
11. & (s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i))
11. & (x@0:Id. 
11. & (L != (x@0) ==> deq-member(KindDeq;kind(a(i;t));L)
11. & (
11. & (s(i;t).x@0 = s(i;t+1).x@0)
11. & (l:IdLnk, tg:Id.
11. & (L != (<l,tg>) ==> deq-member(KindDeq;kind(a(i;t));L)
11. & (
11. & (w-tagged(tg; onlnk(l;m(i;t))) = nil)
12. x@0:Id. x0 != (x@0) ==> s(i;0).x@0 = x0
13. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top)
14. x@0:Id. vartype(i;x@0) r ds(x@0)?Top
15. e : E
16. loc(e) = i
  valtype(e) r ma-valtype(da; kind(e))

1

14. e : E 15. loc(e) = i  Id   valtype(e) r ma-valtype(da; kind(e))

14 steps

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