Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 . SNo x0 ⟶ SNo x1 ⟶ (∀ x5 . x5 ∈ SNoS_ omega ⟶ (∀ x6 . x6 ∈ omega ⟶ SNoLt (abs_SNo (add_SNo x5 (minus_SNo x0))) (eps_ x6)) ⟶ x5 = x0) ⟶ (∀ x5 . x5 ∈ omega ⟶ SNo (ap (lam omega (λ x6 . add_SNo (ap x2 (ordsucc x6)) (ap x3 (ordsucc x6)))) x5)) ⟶ (∀ x5 . x5 ∈ omega ⟶ SNoLt (add_SNo x0 x1) (add_SNo (ap (lam omega (λ x6 . add_SNo (ap x2 (ordsucc x6)) (ap x3 (ordsucc x6)))) x5) (eps_ x5))) ⟶ SNo x4 ⟶ SNoLt x4 x0 ⟶ x4 ∈ SNoS_ omega ⟶ not (∀ x5 : ο . (∀ x6 . and (x6 ∈ omega) (SNoLe (add_SNo x4 x1) (ap (lam omega (λ x7 . add_SNo (ap x2 (ordsucc x7)) (ap x3 (ordsucc x7)))) x6)) ⟶ x5) ⟶ x5) ⟶ SNoLt 0 (add_SNo x0 (minus_SNo x4)) ⟶ x4 = x0 ⟶ ∀ x5 : ο . x5

as obj
-

as prop
fe17b..^{Conj_real_add_SNo__18__2}

theory
HotG

stx
b740c..

address
TMFU4..^{Conj_real_add_SNo__18__2}