(13steps 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: upto decomp 2 2 2 1 1
1. m : 
2. 0<m
3. n:(m-1+1). upto(m-1) ~ (upto(n) @ map(x.x+n;upto(m-1-n)))
4. n : (m+1)
5. n = m
6. m = 0
7. upto(m-1) ~ (upto(n) @ map(x.x+n;upto(m-1-n)))
  (map(x.x+n;upto(m-1-n)) @ [(m-1)]) ~ map(x.x+n;upto(m-n))
By: RW (AddrC [2] (RecUnfoldC `upto`)) 0 THEN SplitOnConclITE

Generated subgoals:

1 8. m-n = 0
  (map(x.x+n;upto(m-1-n)) @ [(m-1)]) ~ map(x.x+n;nil)
Auto
2 8. m-n = 0
  (map(x.x+n;upto(m-1-n)) @ [(m-1)]) ~ map(x.x+n;upto(m-n-1) @ [(m-n-1)])
3 steps

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

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