| Who Cites prime factorization of? |
|
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_mset_complete | Def prime_mset_complete(f)(x) == if is_prime(x) f(x) else 0 fi |
| | Thm* f:(Prime   ). prime_mset_complete(f)     |
|
eval_factorization | Def  {a..b }(f) == i:{a..b }. i f(i) |
| | Thm* a,b: , f:({a..b }  ).  {a..b }(f)  |
|
prime_nats | Def Prime == {x: | prime(x) } |
|
prime_decider | Def is_prime(x) == prime_decider_exists{1:l}(x) |
| | Thm* x: . is_prime(x)  |
|
iter_via_intseg | Def Iter(f;u) i:{a..b }. e(i)
Def == if a< b f((Iter(f;u) i:{a..b-1 }. e(i)),e(b-1)) else u fi
Def (recursive) |
| | Thm* f:(A A A), u:A, a,b: , e:({a..b } A). (Iter(f;u) i:{a..b }. e(i)) A |
|
prime | Def prime(a) == a = 0 & (a ~ 1) & ( b,c: . a | b c  a | b a | c) |
| | Thm* a: . prime(a) Prop |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
lt_int | Def i< j == if i<j true ; false fi |
| | Thm* i,j: . (i< j)  |
|
assoced | Def a ~ b == a | b & b | a |
| | Thm* a,b: . (a ~ b) Prop |
|
divides | Def b | a == c: . a = b c |
| | Thm* a,b: . (a | b) Prop |
|
le | Def A B == B<A |
| | Thm* i,j: . (i j) Prop |
|
not | Def A == A  False |
| | Thm* A:Prop. ( A) Prop |