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')))
6. t=0
7. isnull(a(i;t-1))
  first(<i,t-1>)  (t':. t'<t  isnull(a(i;t')))

By:	AssertBY (first(<i,t-1>)  ) (BackThru Thm* the_w:World, i:Id, t:. first(<i,t>)  )

1

8. first(<i,t-1>)     first(<i,t-1>)  (t':. t'<t  isnull(a(i;t')))

5 steps

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