Proofgold Term Root Disambiguation

∀ x0 x1 . SNoLt 0 x0 ⟶ SNoLt 0 x1 ⟶ not (mul_SNo x0 x1 ∈ real) ⟶ SNo x0 ⟶ SNoLev x0 ∈ ordsucc omega ⟶ x0 ∈ SNoS_ (ordsucc omega) ⟶ SNoLt x0 omega ⟶ (∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x3)) ⟶ x2 = x0) ⟶ SNo x1 ⟶ SNoLev x1 ∈ ordsucc omega ⟶ SNoLt x1 omega ⟶ (∀ x2 . x2 ∈ SNoS_ omega ⟶ (∀ x3 . x3 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x1))) (eps_ x3)) ⟶ x2 = x1) ⟶ (∀ x2 . x2 ∈ omega ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ SNoS_ omega ⟶ SNoLt 0 x4 ⟶ SNoLt x4 x0 ⟶ SNoLt x0 (add_SNo x4 (eps_ x2)) ⟶ x3) ⟶ x3) ⟶ (∀ x2 . x2 ∈ omega ⟶ ∀ x3 : ο . (∀ x4 . x4 ∈ SNoS_ omega ⟶ SNoLt 0 x4 ⟶ SNoLt x4 x1 ⟶ SNoLt x1 (add_SNo x4 (eps_ x2)) ⟶ x3) ⟶ x3) ⟶ not (SNo (mul_SNo x0 x1))

as obj
-

as prop
e4ae8..^{Conj_real_mul_SNo_pos__135__10}

theory
HotG

stx
b740c..

address
TMNKy..^{Conj_real_mul_SNo_pos__135__10}