(2steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: factorial tail split mid 1
1. n : 
2. m : 
3. k : 
4. nk+-m
5. mk
  ( i:{k+-m+-n..k}. 1+i) = ( i:{k+-m+-n..k+-m}. 1+i)( i:{k+-m..k}. 1+i)
By: BackThru: 
Thm*  a,c,b:, e:({a..b}).
Thm*  ac
Thm*  
Thm*  cb  ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i))
Using:[e(i):= 1+i] ...

Generated subgoals:

None

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

(2steps total) PrintForm Definitions Lemmas IteratedBinops Sections DiscrMathExt Doc