(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
  m:, n:(m+1). upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))
By: InductionOnNat THEN Reduce 0 THEN Analyze 0

Generated subgoals:

1 1. n : 1
  nil ~ (upto(n) @ map(x.x+n;upto(0-n)))
1 step
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)
  upto(m) ~ (upto(n) @ map(x.x+n;upto(m-n)))
11 steps

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