Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ real ⟶ SNoLt 0 x0 ⟶ (x0 = 2 ⟶ ∀ x1 : ο . x1) ⟶ (∀ x1 . x1 ∈ omega ⟶ x0 = eps_ x1 ⟶ ∀ x2 : ο . x2) ⟶ ∃ x1 . and (x1 ∈ SNoL_pos x0) (SNoLt x0 (mul_SNo 2 x1))

as obj
-

as prop
b8001..^{pos_real_left_approx_double}

theory
HotG

stx
f61d0..

address
TMNrv..^{pos_real_left_approx_double}