Nuprl - Proof: general length nth tl 2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: general length nth tl 2 2

1. r :

2. 0<r
3.

L:Top List. ||nth_tl(r-1;L)|| = if r-1<

||L||

||L||-(r-1) else 0 fi
4. L : Top List
5. 0<r
6. ||L||

||nth_tl(r-1;tl(L))|| = 0

By:	Analyze 4 THEN Reduce 0

Generated subgoals:

1 4. 0<r
5. ||nil||r
||nth_tl(r-1;nil)|| = 0
1 step

2 4. u : Top
5. v : Top List
6. 0<r
7. ||[u / v]||r
||nth_tl(r-1;v)|| = 0
1 step

About:

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

1	4. 0<r 5. \|\|nil\|\|r \|\|nth_tl(r-1;nil)\|\| = 0	1 step
2	4. u : Top 5. v : Top List 6. 0<r 7. \|\|[u / v]\|\|r \|\|nth_tl(r-1;v)\|\| = 0	1 step