a:
, b:
, f:({a..b
}
), p:.
is_prime_factorization(a; b; f)
prime(p)
p | 
{a..b}(f) {a..b}(f) = p
{a..b}(reduce_factorization(f; p)) a:, b:, f:({a..b}), p:.
is_prime_factorization(a; b; f)
prime(p)
p | {a..b}(f) {a..b}(f) = p{a..b}(reduce_factorization(f; p))| By: |
Thm* a:, b:, f:({a..b}), p:.
Thm* is_prime_factorization(a; b; f) Thm*
Thm* prime(p) p | {a..b}(f) p  {a..b} & 0<f(p)
THEN Analyze-1 |
| 1 |
2. b :
3. f : {a..b }
4. p :
5. is_prime_factorization(a; b; f) 6. prime(p) 7. p | {a..b}(f)
8. p {a..b}
9. 0<f(p) {a..b}(f) = p{a..b}(reduce_factorization(f; p)) | 1 step |
About:
 |  |  |  |  |  |  |  |  |  |