1. the_w : World
2. i : Id
3. t : 
4. 0<t
5. first(<i,t-1>)  (t':. t'<t-1  isnull(a(i;t')))
  if t=0 true ; isnull(a(i;t-1)) first(<i,t-1>) else false fi
  
  (t':. t'<t  isnull(a(i;t')))

1	6. t=0 7. isnull(a(i;t-1))   first(<i,t-1>)  (t':. t'<t  isnull(a(i;t')))	6 steps
2	6. t=0 7. isnull(a(i;t-1))   false  (t':. t'<t  isnull(a(i;t')))	1 step

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