Proofgold Term Root Disambiguation

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

as obj
-

as prop
5ece1..^{Conj_add_SNo_prop1__4__2}

theory
HotG

stx
b740c..

address
TMPK1..^{Conj_add_SNo_prop1__4__2}