| Some definitions of interest. |
|
is_prime_factorization | Def is_prime_factorization(a; b; f) == i:{a..b }. 0<f(i)  prime(i) |
| | Thm* a,b: , f:({a..b }  ). is_prime_factorization(a; b; f) Prop |
|
prime | Def prime(a) == a = 0 & (a ~ 1) & ( b,c: . a | b c  a | b a | c) |
| | Thm* a: . prime(a) Prop |
|
divides | Def b | a == c: . a = b c |
| | Thm* a,b: . (a | b) Prop |
|
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 }   |