(7steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: general length nth tl
  r:, L:Top List. ||nth_tl(r;L)|| = if r<||L|| ||L||-r else 0 fi
By: InductionOnNat THEN RecUnfold `nth_tl` 0 THEN Reduce 0

Generated subgoals:

1   L:Top List. ||L|| = if 0<||L|| ||L||-0 else 0 fi
1 step
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
  L:Top List. 
  ||if r0 L else nth_tl(r-1;tl(L)) fi|| = if r<||L|| ||L||-r else 0 fi
5 steps

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

(7steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc