| | 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 |
|
| int_seg | Def {i..j} == {k:| i  k < j } |
| | | Thm* m,n:. {m..n} Type |
|
| prime_nats | Def Prime == {x:| prime(x) } |
|
| nat | Def == {i:| 0i } |
| | | Thm* Type |
|
| prime | Def prime(a) ==  a = 0 & (a ~ 1) & (b,c:. a | b c a | b  a | c) |
| | | Thm* a:. prime(a) Prop |
|
| prime_mset_complete | Def prime_mset_complete(f)(x) == if is_prime(x) f(x) else 0 fi |
| | | Thm* f:(Prime). prime_mset_complete(f) |
