(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

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)) ~ map(x.x+n;upto(m-n-1))


By: RepeatFor 2 Analyze


Generated subgoals:

None

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