Proofgold Proposition

∀ x0 . nat_p x0 ⟶ 0 ∈ x0 ⟶ ∀ x1 : ο . (∀ x2 . and (x2 ∈ omega) (∀ x3 : ο . (∀ x4 : ι → ι . and (and (168aa.. prime_nat x2 x4) (05ecb.. x4 x2 = x0)) (∀ x5 . x5 ∈ omega ⟶ ∀ x6 : ι → ι . 168aa.. prime_nat x5 x6 ⟶ 05ecb.. x6 x5 = x0 ⟶ and (x5 = x2) (∀ x7 . x7 ∈ x2 ⟶ x6 x7 = x4 x7)) ⟶ x3) ⟶ x3) ⟶ x1) ⟶ x1

type
prop

theory
HotG

name
-

proof
PUQQ9..

Megalodon
prime_factorization_ex_uniq

proofgold address
TMaSw..^{prime_factorization_ex_uniq}

creator
30111 PrQUS../1cb16..

owner
30111 PrQUS../1cb16..

term root
ae2a4..