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. 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 = x0
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(2of(2of(2of(2of(
14. & (E != 1of(if eqof(IdDeq)(i@0,i) <ds,da,,,<k,x> : f,,,,>
14. & (E != 1of(else  fi)))))(<kind(a(i@0;t)),x@0>) ==> s(i@0;t+1).x@0
14. & (E != 1of(else  fi)))))(<kind(a(i@0;t)),x@0>) ==> =
14. & (E != 1of(else  fi)))))(<kind(a(i@0;t)),x@0>) ==> E
14. & (E != 1of(else  fi)))))(<kind(a(i@0;t)),x@0>) ==> ((x.s(i@0;t).x)
14. & (E != 1of(else  fi)))))(<kind(a(i@0;t)),x@0>) ==> ,val(a(i@0;t))))
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 = s(i@0;t+1).x@0)
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)
15. x:Id. vartype(i;x) r ds(x)?Top
16. e:E. loc(e) = i  (valtype(e) r ma-valtype(da; kind(e)))
17. j : Id
18. t : 
19. j = i
20. kind(<j,t>) = k
21. isnull(a(i;t))
22. valtype(i;a(i;t)) r ma-valtype(da; k)
  (x after <j,t>) = f((z.(z when <j,t>)),val(<j,t>))  ds(x)?Top

By:	MoveToHyp -4 -1 THEN AllHyps (h.InstHyp [i;t] h THENA Complete Auto) THEN Subst ((eqof(IdDeq)(i,i)) ~ true) -1 THEN Reduce -1 THEN Try (BackThru Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true) THEN ExRepD

1

19. valtype(i;a(i;t)) r ma-valtype(da; k) 20. j = i 21. kind(<j,t>) = k  Knd 22. isnull(a(i;t)) 23. islocal(kind(a(i;t))) 23.  23. P != (act(kind(a(i;t)))) ==> P((x.s(i;t).x),val(a(i;t))) 24. x@0:Id.  24. E != <k,x> : f(<kind(a(i;t)),x@0>) ==> s(i;t+1).x@0 24. E != <k,x> : f(<kind(a(i;t)),x@0>) ==> = 24. E != <k,x> : f(<kind(a(i;t)),x@0>) ==> E((x.s(i;t).x),val(a(i;t))) 24. E != <k,x> : f(<kind(a(i;t)),x@0>) ==>  ds(x@0)?Top 25. l:IdLnk.  25. <ds,da,,,<k,x> : f,,,,>.send(kind(a(i;t));l;x. 25. s(i;t).x;val(a(i;t));withlnk(l;m(i;t));i) 26. x@0:Id.  26. L != (x@0) ==> deq-member(KindDeq;kind(a(i;t));L) 26.  26. s(i;t).x@0 = s(i;t+1).x@0  ds(x@0)?Top 27. l:IdLnk, tg:Id. 27. L != (<l,tg>) ==> deq-member(KindDeq;kind(a(i;t));L) 27.  27. w-tagged(tg; onlnk(l;m(i;t))) = nil  Msg List   (x after <j,t>) = f((z.(z when <j,t>)),val(<j,t>))  ds(x)?Top

9 steps

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