Nuprl - Proof: general length nth tl 2 2 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: general length nth tl 2 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. u : Top
5. v : Top List
6. 0<r
7. ||[u / v]||

||nth_tl(r-1;v)|| = 0

By:	InstHyp [v] 3 THEN MoveToConcl -1 THEN SplitOnConclITE

Generated subgoals:

None

About:

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