| Some definitions of interest. |
|
eval_factorization | Def  {a..b }(f) == i:{a..b }. i f(i) |
|
| Thm* a,b: , f:({a..b }  ).  {a..b }(f)  |
|
int_seg | Def {i..j } == {k: | i k < j } |
|
| Thm* m,n: . {m..n } Type |
|
nat | Def == {i: | 0 i } |
|
| Thm* Type |
|
reduce_factorization | Def reduce_factorization(f; j)(i) == if i= j f(i)-1 else f(i) fi |
|
| Thm* a,b: , f:({a..b }  ), j:{a..b }.
Thm* 0<f(j)  reduce_factorization(f; j) {a..b }   |
|
trivial_factorization | Def trivial_factorization(z)(i) == if i= z 1 else 0 fi |
|
| Thm* a,b: , z:{a..b }. trivial_factorization(z) {a..b }   |