Proofgold Term Root Disambiguation

∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ ∀ x2 . x2 ∈ int ⟶ ∀ x3 . x3 ∈ int ⟶ ∀ x4 . x4 ∈ int ⟶ ∀ x5 . x5 ∈ int ⟶ x0 = add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x3 x3) (add_SNo (mul_SNo x4 x4) (mul_SNo x5 x5))) ⟶ ∀ x6 . x6 ∈ int ⟶ ∀ x7 . x7 ∈ int ⟶ ∀ x8 . x8 ∈ int ⟶ ∀ x9 . x9 ∈ int ⟶ 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 . x11 ∈ omega ⟶ ∀ x12 . x12 ∈ omega ⟶ ∀ x13 . x13 ∈ omega ⟶ ∀ x14 . x14 ∈ omega ⟶ 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
c6211..

theory
HotG

stx
007b5..

address
TMZzZ..