Proofgold Term Root Disambiguation

∀ x0 x1 x2 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNoLe x0 x1 ⟶ SNoLt x1 (add_SNo x0 x2) ⟶ SNoLt (abs_SNo (add_SNo x1 (minus_SNo x0))) x2

as obj
-

as prop
31a8b..^{abs_SNo_intvl_bd}

theory
HotG

stx
ba872..

address
TMNJN..^{abs_SNo_intvl_bd}