a:{2...}, b:
, g,h:({a..b
}
).
is_prime_factorization(a; b; g)
is_prime_factorization(a; b; h) 
{a..b}(g) = {a..b}(h) g = hAt: prime factorization unique
a:{2...}, b:, g,h:({a..b}).
is_prime_factorization(a; b; g)
is_prime_factorization(a; b; h) {a..b}(g) = {a..b}(h) g = h| By: |
{a..b}(g), holding a and b constant. }
2 Times Analyze ...w
THEN (Enough that ( k:, g,h:({a..b}).
(is_prime_factorization(a; b; g) & is_prime_factorization(a; b; h) (
( {a..b}(g) = k  {a..b}(g) = {a..b}(h) g = h {a..b}
( By SideProof)
THEN CompNatInd Concl ... |
| 1 |
2. b :
3. k :
4. k1:.
4. k1<k 4.
4. ( g,h:({a..b}).
4. (is_prime_factorization(a; b; g) & is_prime_factorization(a; b; h) 4. (
4. ( {a..b}(g) = k1 {a..b}(g) = {a..b}(h) g = h)
5. g : {a..b }
6. h : {a..b }
7. is_prime_factorization(a; b; g) 8. is_prime_factorization(a; b; h) 9. {a..b}(g) = k
10. {a..b}(g) = {a..b}(h)
g = h | 11 steps |
About:
 |  |  |  |  |  |  |
 |  |  |