1. i : Id
2. k : Knd
3. l : IdLnk
4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : (tg:IdState(ds)ma-valtype(da; k)(da(rcv(l; tg))?Void List)) List
7. source(l) = i
8. w : World
9. p : FairFifo
10. FairFifo
11. l@0:IdLnk, tg:Id.
11. (w.M(l@0,tg)) r if eqof(IdDeq)(source(l@0),i)
11. (w.M(l@0,tg)) r if <ds,da,,,,<[<k,l>],x.f>,,,>
11. (w.M(l@0,tg)) r else  fi.da(rcv(l@0; tg))
12. (eqof(IdDeq)(i,i)) ~ true
13. (x:Id. vartype(i;x) r ds(x)?Top)
13. & (e:E. loc(e) = i  (valtype(e) r ma-valtype(da; kind(e))))
13. & (e:E. isrcv(e)  lnk(e) = l  (valtype(e) r ma-valtype(da; kind(e))))
13. & ({m:Msg| source(mlnk(m)) = i } r Msg((l,tg. da(rcv(l; tg))?Top)))
14. a:Id, t:.
14. t':. 
14. tt'
14. & isnull(a(i;t')) & kind(a(i;t')) = locl(a)
14. &  locl(a)  dom(da)
14. &  P != (a) ==> v:da(locl(a))?Top. P((x.s(i;t').x),v)
15. t:. 
15. isnull(a(i;t))
15. 
15. (islocal(kind(a(i;t)))
15. (
15. (deq-member(IdDeq;act(kind(a(i;t)));1of())
15. (
15. (2of()(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t))))
15. & (x:Id. 
15. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)),x>;1of())
15. & (
15. & (s(i;t+1).x = 2of()(<kind(a(i;t)),x>,x.s(i;t).x,val(a(i;t))))
15. & (l@0:IdLnk. 
15. & ((eqof(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq))(<k,l>,<kind(a(i;t)),l@0>)
15. & (( false)
15. & (
15. & (withlnk(l@0;m(i;t))
15. & (=
15. & (if source(l@0) = i
15. & (if concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf)
15. & (if concat(map(tgf.map(x.<1of(tgf),x>;((x.s(i;t).x)
15. & (if concat(map(tgf.map(x.<1of(tgf),x>;,val(a(i;t))));f))
15. & (else nil fi)
15. & (x:Id. 
15. & ((deq-member(IdDeq;x;1of())  deq-member(KindDeq;kind(a(i;t));2of()(x)))
15. & (
15. & (s(i;t).x = s(i;t+1).x)
15. & (l@0:IdLnk, tg:Id.
15. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l@0,tg>;1of())
15. & ((
15. & ((deq-member(KindDeq;kind(a(i;t));2of()(<l@0,tg>)))
15. & (
15. & (w-tagged(tg; onlnk(l@0;m(i;t))) = nil)
16. x:Id. deq-member(IdDeq;x;1of())  s(i;0).x = 2of()(x)
17. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top)
18. x:Id. 
18. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi
  e:E. 
  loc(e) = i  Id
  
  kind(e) = k  Knd
  
  sends(l;e)
  =
  tagged-messages(l;z.(z when e);val(e);f)
   Msg((l,tg. da(rcv(l; tg))?Top)) List

1

14. t:.  14. isnull(a(i;t)) 14.  14. (islocal(kind(a(i;t))) 14. ( 14. (deq-member(IdDeq;act(kind(a(i;t)));1of()) 14. ( 14. (2of()(act(kind(a(i;t))),x.s(i;t).x,val(a(i;t)))) 14. & (x:Id.  14. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i;t)),x>;1of()) 14. & ( 14. & (s(i;t+1).x 14. & (= 14. & (2of()(<kind(a(i;t)),x>,x.s(i;t).x,val(a(i;t))) 14. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi) 14. & (l@0:IdLnk.  14. & ((eqof(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq))(<k,l>,<kind(a(i;t)),l@0>) 14. & (( false) 14. & ( 14. & (withlnk(l@0;m(i;t)) 14. & (= 14. & (if source(l@0) = i 14. & (if concat(map(tgf.map(x.<1of(tgf),x>;2of(tgf) 14. & (if concat(map(tgf.map(x.<1of(tgf),x>;((x.s(i;t).x) 14. & (if concat(map(tgf.map(x.<1of(tgf),x>;,val(a(i;t))));f)) 14. & (else nil fi 14. & ( (tg:Idif source(l@0) = i da(rcv(l@0; tg))?Top else Top fi) List) 14. & (x:Id.  14. & ((deq-member(IdDeq;x;1of())  deq-member(KindDeq;kind(a(i;t));2of()(x))) 14. & ( 14. & (s(i;t).x 14. & (= 14. & (s(i;t+1).x 14. & ( if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi) 14. & (l@0:IdLnk, tg:Id. 14. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l@0,tg>;1of()) 14. & (( 14. & ((deq-member(KindDeq;kind(a(i;t));2of()(<l@0,tg>))) 14. & ( 14. & (w-tagged(tg; onlnk(l@0;m(i;t))) = nil  Msg List) 15. a:Action(i). isnull(a)  (valtype(i;a) r da(kind(a))?Top) 16. x:Id.  16. vartype(i;x) r if deq-member(IdDeq;x;1of(ds)) 2of(ds)(x) else Top fi   e:E.    loc(e) = i  Id      kind(e) = k  Knd      sends(l;e)   =   tagged-messages(l;z.(z when e);val(e);f)    Msg((l,tg. da(rcv(l; tg))?Top)) List

108 steps

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