Nuprl - Proof: general length nth tl 2 2 1

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

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. 0<r
5. ||nil||

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

By:	InstHyp [nil] 3 THEN Reduce -1 THEN HypSubst' -1 0 THEN SplitOnConclITE

Generated subgoals:

None

About:

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