Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 x5 . SNo x0 ⟶ SNo x1 ⟶ SNo x2 ⟶ (∀ x6 . x6 ∈ SNoL x0 ⟶ ∀ x7 . x7 ∈ SNoL x1 ⟶ SNoLt (add_SNo (mul_SNo x6 x1) (mul_SNo x0 x7)) (add_SNo x2 (mul_SNo x6 x7))) ⟶ SNo x3 ⟶ SNoLt x2 x3 ⟶ x4 ∈ SNoL x0 ⟶ x5 ∈ SNoL x1 ⟶ SNoLe (add_SNo x3 (mul_SNo x4 x5)) (add_SNo (mul_SNo x4 x1) (mul_SNo x0 x5)) ⟶ SNo x5 ⟶ SNo (mul_SNo x4 x5) ⟶ SNoLt (add_SNo x3 (mul_SNo x4 x5)) (add_SNo x2 (mul_SNo x4 x5)) ⟶ SNoLt (mul_SNo x0 x1) x3

as obj
-

as prop
5101e..^{Conj_mul_SNo_SNoL_interpolate__5__9}

theory
HotG

stx
b740c..

address
TMRvH..^{Conj_mul_SNo_SNoL_interpolate__5__9}