Proofgold Term Root Disambiguation

∀ x0 x1 . x0 ∈ omega ⟶ SNo (eps_ (ordsucc x0)) ⟶ SNo x1 ⟶ SNoLev x1 ∈ ordsucc (ordsucc x0) ⟶ SNoLt x1 (eps_ (ordsucc x0)) ⟶ SNoLe x1 0 ⟶ and (SNoLt (add_SNo x1 (eps_ (ordsucc x0))) (eps_ x0)) (SNoLt (add_SNo (eps_ (ordsucc x0)) x1) (eps_ x0))

as obj
-

as prop
47fc9..^{Conj_eps_ordsucc_half_add__7__0}

theory
HotG

stx
b740c..

address
TMJ4S..^{Conj_eps_ordsucc_half_add__7__0}