Proofgold Object

{x0 ∈ SNoS_ (ordsucc omega)|and (and (x0 = omega ⟶ ∀ x1 : ο . x1) (x0 = minus_SNo omega ⟶ ∀ x1 : ο . x1)) (∀ x1 . x1 ∈ SNoS_ omega ⟶ (∀ x2 . x2 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) (eps_ x2)) ⟶ x1 = x0)}

type
ι

theory
HotG

name
real

definition
PUgvb..

Megalodon
real

proofgold address
TMJ3A..^real

creator
12283 PrGxv../6fef0..

owner
12283 PrGxv../6fef0..

term root
e26ff..