1. i : Id
2. L : Knd List
3. x : Id
4. T : Type
  @i: only L affects x : T realizes2 es.(vartype(i;x) r T)
  & (e:E. 
  & (loc(e) = i  Id
  & (
  & (((x after e) = (x when e)  T  (kind(e)  L))
  & (& ((kind(e)  L)  (x after e) = (x when e)  T))

By:	let T  Auto THEN D_ES_Subtype THEN ExRepD in RepeatFor 3 (Analyze 0 THENA Complete Auto) THEN ES_Reduce THEN PW_Reduce -1 THENA T

1

5. w : World 6. FairFifo 7. FairFifo 8. i@0,x@0:Id. 8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(i@0,i) 8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T> 8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if , 8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if , 8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if , 8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if , 8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if , 8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,<[x],x.L> 8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if , 8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(if ,> 8. vartype(i@0;x@0) r if deq-member(IdDeq;x@0;1of(1of(else  fi))) 8. vartype(i@0;x@0) r if 2of(1of(if eqof(IdDeq)(i@0,i) 8. vartype(i@0;x@0) r if 2of(1of(if <<[x],x.T>,,,,,,<[x],x.L>,,> 8. vartype(i@0;x@0) r if 2of(1of(else  fi)) 8. vartype(i@0;x@0) r if (x@0) 8. vartype(i@0;x@0) r else Top fi 9. i@0:Id, a:Action(i@0). 9. isnull(a) 9.  9. (valtype(i@0;a) r if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,> 9. (valtype(i@0;a) r else  fi.da(kind(a))) 10. l:IdLnk, tg:Id. 10. (w.M(l,tg)) r if eqof(IdDeq)(source(l),i) <<[x],x.T>,,,,,,<[x],x.L>,,> 10. (w.M(l,tg)) r else  fi.da(rcv(l; tg)) 11. i@0,x@0:Id. 11. deq-member(IdDeq;x@0;1of(1of(2of(2of(if eqof(IdDeq)(i@0,i) 11. deq-member(IdDeq;x@0;1of(1of(2of(2of(if <<[x],x.T>,,,,,,<[x],x.L>,,> 11. deq-member(IdDeq;x@0;1of(1of(2of(2of(else  fi))))) 11.  11. s(i@0;0).x@0 11. = 11. 2of(1of(2of(2of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,> 11. 2of(1of(2of(2of(else  fi)))) 11. (x@0) 11.  if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(i@0,i) 11.  if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>,,,,,,<[x],x.L>,,> 11.  if deq-member(IdDeq;x@0;1of(1of(else  fi))) 11.  if 2of(1of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,> 11.  if 2of(1of(else  fi)) 11.  if (x@0) 11.  else Void fi 12. i@0:Id, t:. 12. isnull(a(i@0;t)) 12.  12. (islocal(kind(a(i@0;t))) 12. ( 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if eqof(IdDeq) 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if (i@0 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,i) 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if <<[x],x.T> 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if , 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if , 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if , 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if , 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if , 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,<[x],x.L> 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if , 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(if ,> 12. (deq-member(IdDeq;act(kind(a(i@0;t)));1of(1of(2of(2of(2of(else  fi)))))) 12. ( 12. (2of(1of(2of(2of(2of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,> 12. (2of(1of(2of(2of(2of(else  fi))))) 12. ((act(kind(a(i@0;t))) 12. (,x.s(i@0;t).x 12. (,val(a(i@0;t)))) 12. & (x@0:Id.  12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);<kind(a(i@0;t)) 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;1of(1of( 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;2of(2of(2of(2of( 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if eqof(IdDeq)(i@0,i) 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if <<[x],x.T> 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if , 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if , 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if , 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if , 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if , 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,<[x],x.L> 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if , 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;if ,> 12. & (deq-member(product-deq(Knd;Id;KindDeq;IdDeq);,x@0>;else  fi))))))) 12. & ( 12. & (s(i@0;t+1).x@0 12. & (= 12. & (2of(1of(2of(2of(2of(2of(if eqof(IdDeq)(i@0,i) 12. & (2of(1of(2of(2of(2of(2of(if <<[x],x.T>,,,,,,<[x],x.L>,,> 12. & (2of(1of(2of(2of(2of(2of(else  fi)))))) 12. & ((<kind(a(i@0;t)),x@0> 12. & (,x.s(i@0;t).x 12. & (,val(a(i@0;t))) 12. & ( if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(i@0,i) 12. & ( if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>,,,,,,<[x],x.L>,,> 12. & ( if deq-member(IdDeq;x@0;1of(1of(else  fi))) 12. & ( if 2of(1of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,> 12. & ( if 2of(1of(else  fi)) 12. & ( if (x@0) 12. & ( else Top fi) 12. & (l:IdLnk.  12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;1of( 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;1of( 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of( 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of( 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of( 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of( 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;2of( 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if eqof(IdDeq) 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if (i@0 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,i) 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if <<[x] 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if <,x. 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if <,T> 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if , 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if , 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if , 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if , 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if , 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,<[x] 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,,x. 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,,L> 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if , 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;if ,> 12. & (deq-member(product-deq(Knd;IdLnk;KindDeq;IdLnkDeq);<kind(a(i@0;t)),l>;else  fi)))))))) 12. & ( 12. & (withlnk(l;m(i@0;t)) 12. & (= 12. & (if source(l) = i@0 12. & (if concat(map(tgf.map(x. 12. & (if <1of(tgf),x>;2of(tgf) 12. & (if <1of(tgf),x>;((x.s(i@0;t).x) 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(2of(2of(2of(2of(2of( 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if eqof(IdDeq)(i@0,i) 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if <<[x],x.T> 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if , 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if , 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if , 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if , 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if , 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,<[x],x.L> 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if , 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(if ,> 12. & (if <1of(tgf),x>;,val(a(i@0;t))));2of(1of(else  fi))))))) 12. & (if <1of(tgf),x>;,val(a(i@0;t))));(<kind(a(i@0;t)),l>))) 12. & (else nil fi 12. & ( (tg:Id 12. & ( (if source(l) = i@0 12. & ( (if if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,> 12. & ( (if else  fi.da(rcv(l; tg)) 12. & ( (else Top fi) List) 12. & (x@0:Id.  12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if eqof(IdDeq) 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if (i@0 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,i) 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if <<[x],x.T> 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if , 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if , 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if , 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if , 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if , 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,<[x],x.L> 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if , 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(if ,> 12. & ((deq-member(IdDeq;x@0;1of(1of(2of(2of(2of(2of(2of(2of(else  fi))))))))) 12. & (( 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of( 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i) 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <<[x],x.T> 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[x],x.L> 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,> 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(else  fi)))))))) 12. & ((deq-member(KindDeq;kind(a(i@0;t));(x@0))) 12. & ( 12. & (s(i@0;t).x@0 12. & (= 12. & (s(i@0;t+1).x@0 12. & ( if deq-member(IdDeq;x@0;1of(1of(if eqof(IdDeq)(i@0,i) 12. & ( if deq-member(IdDeq;x@0;1of(1of(if <<[x],x.T>,,,,,,<[x],x.L>,,> 12. & ( if deq-member(IdDeq;x@0;1of(1of(else  fi))) 12. & ( if 2of(1of(if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,> 12. & ( if 2of(1of(else  fi)) 12. & ( if (x@0) 12. & ( else Top fi) 12. & (l:IdLnk, tg:Id. 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);<l 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;1of(1of( 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of(2of( 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;2of(2of(2of( 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if eqof(IdDeq) 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if (i@0 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,i) 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if <<[x],x.T> 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if , 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if , 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if , 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if , 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if , 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,<[x],x.L> 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if , 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;if ,> 12. & ((deq-member(product-deq(IdLnk;Id;IdLnkDeq;IdDeq);,tg>;else  fi)))))))))) 12. & (( 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(2of(2of(2of(2of(2of(2of(2of( 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if eqof(IdDeq)(i@0,i) 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if <<[x],x.T> 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,<[x],x.L> 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if , 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(if ,> 12. & ((deq-member(KindDeq;kind(a(i@0;t));2of(1of(else  fi))))))))) 12. & ((deq-member(KindDeq;kind(a(i@0;t));(<l,tg>))) 12. & ( 12. & (w-tagged(tg; onlnk(l;m(i@0;t))) = nil  Msg List) 13. i@0,a:Id, t:. 13. t':.  13. tt' 13. & isnull(a(i@0;t')) & kind(a(i@0;t')) = locl(a) 13. &  a declared in if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,> 13. &  a declared in else  fi 13. &  unsolvable if eqof(IdDeq)(i@0,i) <<[x],x.T>,,,,,,<[x],x.L>,,> 13. &  unsolvable else  fi.pre(a,x.s(i@0;t').x)   (vartype(i;x) r T)   & (e:E.    & (loc(e) = i  Id   & (   & (((x after e) = (x when e)  T  (kind(e)  L))   & (& ((kind(e)  L)  (x after e) = (x when e)  T))

14 steps

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