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. PossibleWorld(d-single-effect(i; ds; da; k; x; f);w)
  (x:Id. vartype(i;x) r ds(x)?Top)
  & (e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))

By:	PW_Reduce1 -1 THEN Thin -1 THEN AllHyps (h.InstHyp [i] h THENA Complete Auto THEN Thin h) THEN AllHyps (h.(RWO Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true h) THEN (Reduce h)) THEN ES_Reduce THEN Try BackThruSomeHyp

1

4. ds : x:Id fp-> Type{i} 5. da : a:Knd fp-> Type{i} 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. & (E != <k,x> : f(<kind(a(i;t)),x@0>) ==>  ds(x@0)?Top) 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  ds(x@0)?Top) 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  Msg List) 12. x@0:Id. x0 != (x@0) ==> s(i;0).x@0 = x0  ds(x@0)?Void 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  Id   valtype(e) r ma-valtype(da; kind(e))

15 steps

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