(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 2
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)))
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)])
By: RWO
Thm* f,as':Top, A:Type, as:A List. map(f;as @ as') ~ (map(f;as) @ map(f;as'))
0
THEN
Analyze

Generated subgoals:

1   map(x.x+n;upto(m-1-n)) ~ map(x.x+n;upto(m-n-1))
1 step
2   [(m-1)] ~ map(x.x+n;[(m-n-1)])
1 step

About:
listconsnilintnatural_numberaddsubtractless_than
lambdauniverseequalsqequaltopall
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