Proofgold Term Root Disambiguation

∀ x0 x1 . (∀ x2 . x2 ∈ SNoL x0 ⟶ ∀ x3 . x3 ∈ SNoL 1 ⟶ SNoLt (add_SNo (mul_SNo x2 1) (mul_SNo x0 x3)) (add_SNo (mul_SNo x0 1) (mul_SNo x2 x3))) ⟶ 0 ∈ SNoL 1 ⟶ x1 ∈ SNoL x0 ⟶ SNo x1 ⟶ add_SNo (mul_SNo x1 1) (mul_SNo x0 0) = x1 ⟶ add_SNo (mul_SNo x0 1) (mul_SNo x1 0) = mul_SNo x0 1 ⟶ SNoLt x1 (mul_SNo x0 1)

as obj
-

as prop
59fb3..^{Conj_mul_SNo_oneR__3__0}

theory
HotG

stx
b740c..

address
TMcD2..^{Conj_mul_SNo_oneR__3__0}