Def  Iter(f;u) i:{a..b}. e(i)
Def  == if a<b f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) else u fi
Def  (recursive)

is mentioned by

Thm*  p:. prime(p)  (b,z:. p | zb  b  0 & p | z)	[prime_divs_exp]
Thm*  p:.  Thm*  prime(p) Thm*   Thm*  (a,b:, e:({a..b}). Thm*  (a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i)))	[prime_divs_mul_via_intseg]
Thm*  a,c,b:, f:({a..b}). Thm*  ac  c<b  {a..b}(f) = {a..c}(f)cf(c){c+1..b}(f)	[eval_factorization_split_pluck]
Def  {a..b}(f) ==  i:{a..b}. if(i)	[eval_factorization]

In prior sections: IteratedBinops

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html