Proofgold Term Root Disambiguation

∀ 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

as obj
-

as prop
a96cd..^{prime_factorization_ex_uniq}

theory
HotG

stx
afc5a..

address
TMSfw..^{prime_factorization_ex_uniq}