| | Some definitions of interest. |
|
| complete_intseg_mset | Def complete_intseg_mset(a; b; f)(x) == if a   x < b f(x) else 0 fi |
| | | Thm*  a,b: , f:({a..b }   ). complete_intseg_mset(a; b; f)  |
|
| eval_factorization | Def   {a..b}(f) == i:{a..b}. if(i) |
| | | Thm* a,b:, f:({a..b}). {a..b}(f) |
|
| 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 |
|
| int_upper | Def {i...} == {j:| ij } |
| | | Thm* n:. {n...} Type |
|
| lelt | Def i j < k == ij & j<k |
|
| prime_nats | Def Prime == {x:| prime(x) } |
|
| nat | Def == {i:| 0i } |
| | | Thm* Type |
|
| not | Def  A == A False |
| | | Thm* A:Prop. (A) Prop |
