Proofgold Term Root Disambiguation

∀ x0 x1 x2 . SNo x0 ⟶ (∀ x3 . x3 ∈ SNoS_ (SNoLev x0) ⟶ and (and (and (SNo (minus_SNo x3)) (∀ x4 . x4 ∈ SNoL x3 ⟶ SNoLt (minus_SNo x3) (minus_SNo x4))) (∀ x4 . x4 ∈ SNoR x3 ⟶ SNoLt (minus_SNo x4) (minus_SNo x3))) (SNoCutP (prim5 (SNoR x3) minus_SNo) (prim5 (SNoL x3) minus_SNo))) ⟶ SNo x1 ⟶ SNoLev x1 ∈ SNoLev x0 ⟶ SNoLt x0 x1 ⟶ SNo x2 ⟶ SNoLt x2 x0 ⟶ SNo (minus_SNo x2) ⟶ (∀ x3 . x3 ∈ SNoR x2 ⟶ SNoLt (minus_SNo x3) (minus_SNo x2)) ⟶ (∀ x3 . x3 ∈ SNoL x1 ⟶ SNoLt (minus_SNo x1) (minus_SNo x3)) ⟶ SNoLt x2 x1 ⟶ SNoLt (minus_SNo x1) (minus_SNo x2)

as obj
-

as prop
d0d3d..^{Conj_minus_SNo_prop1__5__9}

theory
HotG

stx
b740c..

address
TMPmu..^{Conj_minus_SNo_prop1__5__9}