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

By:

Repeat (Unfolds ([`w-valtype` (;`es-valtype` (;`kindcase` (;`es-isrcv` (;`es-kind` (;`w-ekind` (;`es-rcvtype` (;`es-acttype` (;`w-M` (;`w-V` (;`es-lnk` (;`es-tag` (;`es-loc` (;`es-act`] (0 (THEN (Reduce 0) THEN SplitOnConclITE THEN SplitOnConclITE THEN Try (RWO Thm* k:Knd. islocal(k) ~ isrcv(k) -1 THEN RW assert_pushdownC -1 (THEN (Complete Auto) THEN Try (Fold `w-TA` 0 THEN Trivial)

None

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