Proofgold Term Root Disambiguation

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ and (and (and (and (and (SNo (add_SNo x0 x1)) (∀ x2 . x2 ∈ SNoL x0 ⟶ SNoLt (add_SNo x2 x1) (add_SNo x0 x1))) (∀ x2 . x2 ∈ SNoR x0 ⟶ SNoLt (add_SNo x0 x1) (add_SNo x2 x1))) (∀ x2 . x2 ∈ SNoL x1 ⟶ SNoLt (add_SNo x0 x2) (add_SNo x0 x1))) (∀ x2 . x2 ∈ SNoR x1 ⟶ SNoLt (add_SNo x0 x1) (add_SNo x0 x2))) (SNoCutP (binunion {add_SNo x2 x1|x2 ∈ SNoL x0} (prim5 (SNoL x1) (add_SNo x0))) (binunion {add_SNo x2 x1|x2 ∈ SNoR x0} (prim5 (SNoR x1) (add_SNo x0))))

as obj
-

as prop
5a879..^{add_SNo_prop1}

theory
HotG

stx
7edd8..

address
TMcpT..^{add_SNo_prop1}