| Some definitions of interest. |
|
int_seg | Def {i..j } == {k: | i k < j } |
| | Thm* m,n: . {m..n } Type |
|
prime_factorization_of | Def f is a factorization of k
Def == ( x:Prime . k<x  f(x) = 0) & k =  {2..k+1 }(prime_mset_complete(f)) |
| | Thm* f:(Prime   ), k: . f is a factorization of k Prop |
|
prime_nats | Def Prime == {x: | prime(x) } |
|
nat | Def == {i: | 0 i } |
| | 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)     |