Proofgold Term Root Disambiguation

∀ x0 x1 . SNo x0 ⟶ SNo_max_of (SNoL x0) x1 ⟶ ∀ x2 . SNo x2 ⟶ SNoLt x0 x2 ⟶ SNoLt (add_SNo x1 x2) (add_SNo x0 x0) ⟶ ∃ x3 . and (x3 ∈ SNoR x2) (add_SNo x1 x3 = add_SNo x0 x0)

as obj
-

as prop
d6603..^{double_SNo_max_1}

theory
HotG

stx
5128f..

address
TMN9e..^{double_SNo_max_1}