Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 . SNo x0 ⟶ SNo (minus_SNo x0) ⟶ x2 ∈ SNoS_ omega ⟶ (∀ x4 . x4 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x2 (minus_SNo x0))) (eps_ x4)) ⟶ SNo x2 ⟶ SNo (add_SNo x2 (minus_SNo x0)) ⟶ (∀ x4 . x4 ∈ SNoS_ omega ⟶ (∀ x5 . x5 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x4 (minus_SNo (ap x1 (ordsucc x3))))) (eps_ x5)) ⟶ x4 = ap x1 (ordsucc x3)) ⟶ SNo (ap x1 (ordsucc x3)) ⟶ SNoLt (ap x1 (ordsucc x3)) x2 ⟶ SNoLt 0 (add_SNo x2 (minus_SNo (ap x1 (ordsucc x3)))) ⟶ SNoLt x0 (ap x1 (ordsucc x3)) ⟶ abs_SNo (add_SNo x2 (minus_SNo x0)) = add_SNo x2 (minus_SNo x0) ⟶ x2 = ap x1 (ordsucc x3) ⟶ SNoLt x2 (ap x1 x3)

as obj
-

as prop
694cf..^{Conj_SNo_approx_real__10__10}

theory
HotG

stx
b740c..

address
TMMwA..^{Conj_SNo_approx_real__10__10}