1. i : Id
2. L : Knd List
3. x : Id
4. T : Type
5. w : World
6. FairFifo
7. FairFifo
8. vartype(i;x) r T
9. e1 : Id
10. e2 : 
11. isnull(a(e1;e2))  [not for witness]
12. e1 = i
13. isnull(a(i;e2))
14. islocal(kind(a(i;e2)))
14. 
14. deq-member(IdDeq;act(kind(a(i;e2)));1of())
14. 
14. 2of()(act(kind(a(i;e2))),x.s(i;e2).x,val(a(i;e2)))
15. (True  (kind(a(i;e2))  L))  s(i;e2).x = s(i;e2+1).x
  (s(e1;e2+1).x = s(e1;e2).x  T  (kind(a(e1;e2))  L))
  & ((kind(a(e1;e2))  L)  s(e1;e2+1).x = s(e1;e2).x  T)

By:	Assert Dec((kind(a(e1;e2))  L))

1	Dec((kind(a(e1;e2))  L))	1 step
2	16. Dec((kind(a(e1;e2))  L))   (s(e1;e2+1).x = s(e1;e2).x  T  (kind(a(e1;e2))  L))   & ((kind(a(e1;e2))  L)  s(e1;e2+1).x = s(e1;e2).x  T)	8 steps

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