Proofgold Term Root Disambiguation

∀ x0 x1 . SNo x0 ⟶ SNo x1 ⟶ ∀ x2 x3 x4 x5 . SNo x2 ⟶ SNo x3 ⟶ SNo x4 ⟶ SNo x5 ⟶ x0 = add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x3 x3) (add_SNo (mul_SNo x4 x4) (mul_SNo x5 x5))) ⟶ ∀ x6 x7 x8 x9 . SNo x6 ⟶ SNo x7 ⟶ SNo x8 ⟶ SNo x9 ⟶ x1 = add_SNo (mul_SNo x6 x6) (add_SNo (mul_SNo x7 x7) (add_SNo (mul_SNo x8 x8) (mul_SNo x9 x9))) ⟶ ∀ x10 : ο . (∀ x11 x12 x13 x14 . SNo x11 ⟶ SNo x12 ⟶ SNo x13 ⟶ SNo x14 ⟶ mul_SNo x0 x1 = add_SNo (mul_SNo x11 x11) (add_SNo (mul_SNo x12 x12) (add_SNo (mul_SNo x13 x13) (mul_SNo x14 x14))) ⟶ x10) ⟶ x10

as obj
-

as prop
634fb..

theory
HotG

stx
007b5..

address
TMNPW..