(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 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]
By: SplitOnConclITE

Generated subgoals:

1 8. 1+m0
  nth_tl(m-1;tl(L)) ~ [hd(nth_tl(m;L)) / L]
Auto
2 8. 0<1+m
  nth_tl(m-1;tl(L)) ~ [hd(nth_tl(m;L)) / nth_tl(1+m-1;tl(L))]
6 steps

About:
listconsifthenelseintnatural_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