1. i : Id
2. L : Knd List
3. x : Id
4. T : Type
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)
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. & (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. & (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 = s(i@0;t+1).x@0)
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)
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))

1	vartype(i;x) r T	1 step
2	13. 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)	12 steps

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