Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ add_SNo (add_SNo x0 (add_SNo x1 x2)) (add_SNo x3 x4) = add_SNo (add_SNo x4 (add_SNo x1 x2)) (add_SNo x3 x0)

as obj
-

as prop
f24a2..^{add_SNo_3a_2b}

theory
HotG

stx
ba872..

address
TMYna..^{add_SNo_3a_2b}