(12steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: nth tl decomp
  T:Type, m:, L:T List. m<||L||  (nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)])
By: ((((Analyze 0) THEN (Analyze 0)) THEN NatInd -1 THEN Analyze 0)
(THEN
((Analyze 0))
THEN
RecUnfold `nth_tl` 0
THEN
SplitOnConclITE
THEN
Unfold `select` 0
THEN
Reduce 0

Generated subgoals:

1 1. T : Type
2. L : T List
3. 0<||L||
4. 00
  L ~ [hd(L) / tl(L)]
1 step
2 1. T : Type
2. L : T List
3. 0<||L||
4. 0<0
  tl(L) ~ [hd(L) / tl(L)]
Auto
3 1. T : Type
2. m : 
3. 0<m
4. L:T List. m-1<||L||  (nth_tl(m-1;L) ~ [L[(m-1)] / nth_tl(1+m-1;L)])
5. L : T List
6. m<||L||
7. m0
  L ~ [hd(nth_tl(m;L)) / if 1+m0 L else nth_tl(1+m-1;tl(L)) fi]
Auto
4 1. T : Type
2. m : 
3. 0<m
4. L:T List. m-1<||L||  (nth_tl(m-1;L) ~ [L[(m-1)] / nth_tl(1+m-1;L)])
5. L : T List
6. m<||L||
7. 0<m
  nth_tl(m-1;tl(L)) ~ [hd(nth_tl(m;L)) / 
  nth_tl(m-1;tl(L)) ~ [if 1+m0 L else nth_tl(1+m-1;tl(L)) fi]
8 steps

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

(12steps total) PrintForm Definitions Lemmas mb list 1 Sections MarkB generic Doc