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)
10. (x:Id. vartype(i;x) r ds(x)?Top)
10. & (e:E. loc(e) = i  (valtype(e) r ma-valtype(da; kind(e))))
  e:E. 
  loc(e) = i  Id
  
  kind(e) = k  Knd  (x after e) = f((z.(z when e)),val(e))  ds(x)?Top

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. i@0,x@0:Id. 10. vartype(i@0;x@0) r 1of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> 10. vartype(i@0;x@0) r 1of(else  fi)(x@0)?Top 11. i@0:Id, a:Action(i@0). 11. isnull(a) 11.  11. (valtype(i@0;a) r 1of(2of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> 11. (valtype(i@0;a) r 1of(2of(else  fi))(kind(a))?Top) 12. l:IdLnk, tg:Id. 12. (w.M(l,tg)) r 1of(2of(if eqof(IdDeq)(source(l),i) <ds,da,,,<k,x> : f,,,,> 12. (w.M(l,tg)) r 1of(2of(else  fi))(rcv(l; tg))?Top 13. i@0,x@0:Id. 13. x0 != 1of(2of(2of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> 13. x0 != 1of(2of(2of(else  fi)))(x@0) ==> s(i@0;0).x@0 13. x0 != 1of(2of(2of(else  fi)))(x@0) ==> = 13. x0 != 1of(2of(2of(else  fi)))(x@0) ==> x0 13. x0 != 1of(2of(2of(else  fi)))(x@0) ==>  1of(if eqof(IdDeq)(i@0,i) 13. x0 != 1of(2of(2of(else  fi)))(x@0) ==>  1of(if <ds,da,,,<k,x> : f,,,,> 13. x0 != 1of(2of(2of(else  fi)))(x@0) ==>  1of(else  fi)(x@0)?Void 14. i@0:Id, t:. 14. isnull(a(i@0;t)) 14.  14. (islocal(kind(a(i@0;t))) 14. ( 14. (P != 1of(2of(2of(2of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> 14. (P != 1of(2of(2of(2of(else  fi))))(act(kind(a(i@0;t)))) ==> P 14. (P != 1of(2of(2of(2of(else  fi))))(act(kind(a(i@0;t)))) ==> ((x.s(i@0;t).x) 14. (P != 1of(2of(2of(2of(else  fi))))(act(kind(a(i@0;t)))) ==> ,val(a(i@0;t)))) 14. & (x@0:Id.  14. & (E != 1of( 14. & (E != 2of(2of(2of(2of( 14. & (E != if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==> s(i@0;t+1).x@0 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==> = 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==> E 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==> ((x.s(i@0;t).x) 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==> ,val(a(i@0;t))) 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==>  1of(if eqof(IdDeq)(i@0,i) 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==>  1of(if <ds 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==>  1of(if ,da 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==>  1of(if , 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==>  1of(if , 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==>  1of(if ,<k,x> : f 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==>  1of(if , 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==>  1of(if , 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==>  1of(if , 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==>  1of(if ,> 14. & (E != else  fi)))))(<kind(a(i@0;t)),x@0>) ==>  1of(else  fi)(x@0)?Top) 14. & (l:IdLnk.  14. & (if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> 14. & (else  fi.send(kind(a(i@0;t));l;x. 14. & (s(i@0;t).x;val(a(i@0;t));withlnk(l;m(i@0;t));i@0)) 14. & (x@0:Id.  14. & (L != 1of(2of(2of(2of(2of(2of(2of( 14. & (L != 1of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> 14. & (L != 1of(else  fi)))))))(x@0) ==> deq-member(KindDeq;kind(a(i@0;t));L) 14. & ( 14. & (s(i@0;t).x@0 14. & (= 14. & (s(i@0;t+1).x@0 14. & ( 1of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> else  fi)(x@0)?Top) 14. & (l:IdLnk, tg:Id. 14. & (L != 1of( 14. & (L != 2of(2of(2of(2of(2of(2of(2of( 14. & (L != if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> 14. & (L != else  fi))))))))(<l,tg>) ==> deq-member(KindDeq;kind(a(i@0;t));L) 14. & ( 14. & (w-tagged(tg; onlnk(l;m(i@0;t))) = nil  Msg List) 15. i@0,a:Id, t:. 15. t':.  15. tt' 15. & isnull(a(i@0;t')) & kind(a(i@0;t')) = locl(a) 15. &  a declared in if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> else  fi 15. &  unsolvable if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,> 15. &  unsolvable else  fi.pre(a,x.s(i@0;t').x) 16. x:Id. vartype(i;x) r ds(x)?Top 17. e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))) 18. e : E 19. loc(e) = i  Id 20. kind(e) = k  Knd   (x after e) = f((z.(z when e)),val(e))  ds(x)?Top

22 steps

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