Proofgold Object

λ x0 . ∃ x1 . and (x1 ∈ omega) (∃ x3 . and (x3 ∈ int) (x0 = mul_SNo (eps_ x1) x3))

type
ι → ο

theory
HotG

name
diadic_rational_p

definition
PUMdw..

Megalodon
diadic_rational_p

proofgold address
TMP68..^{diadic_rational_p}

creator
12548 PrGxv../cd279..

owner
12548 PrGxv../cd279..

term root
a02ca..