| Some definitions of interest. |
|
int_seg | Def {i..j } == {k: | i k < j } |
| | Thm* m,n: . {m..n } Type |
|
int_upper | Def {i...} == {j: | i j } |
| | Thm* n: . {n...} Type |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
split_factor2 | Def split_factor2(g; x; y)(u)
Def == if u= x g(x)+g(x y) ; u= y g(y)+g(x y) ; u= x y 0 else g(u) fi |
| | Thm* k:{2...}, g:({2..k }  ), x,y:{2..k }.
Thm* x y<k  split_factor2(g; x; y) {2..k }   |