Proofgold Term Root Disambiguation

∀ x0 x1 . SNoLt 0 x0 ⟶ SNoLt 0 x1 ⟶ not (mul_SNo x0 x1 ∈ real) ⟶ SNo x0 ⟶ 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 ⟶ x1 ∈ SNoS_ (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) ⟶ SNo (mul_SNo x0 x1) ⟶ SNo (minus_SNo (mul_SNo x0 x1)) ⟶ nIn (SNoLev (mul_SNo x0 x1)) omega ⟶ not (∀ x2 . SNo x2 ⟶ SNoLev x2 ∈ omega ⟶ SNoLev x2 ∈ SNoLev (mul_SNo x0 x1))

as obj
-

as prop
9e3c5..^{Conj_real_mul_SNo_pos__132__4}

theory
HotG

stx
b740c..

address
TMHGk..^{Conj_real_mul_SNo_pos__132__4}