Proofgold Term Root Disambiguation

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

as obj
-

as prop
a96cd..^{prime_factorization_ex_uniq}

theory
HotG

stx
afc5a..

address
TMSfw..^{prime_factorization_ex_uniq}