Proofgold Term Root Disambiguation

∀ x0 . nat_p x0 ⟶ ∀ x1 x2 x3 x4 . even_nat x1 ⟶ even_nat x2 ⟶ even_nat x3 ⟶ even_nat x4 ⟶ SNoLe x1 x2 ⟶ SNoLe x3 x4 ⟶ mul_SNo 2 x0 = add_SNo (mul_SNo x1 x1) (add_SNo (mul_SNo x2 x2) (add_SNo (mul_SNo x3 x3) (mul_SNo x4 x4))) ⟶ ∀ x5 : ο . (∀ x6 . x6 ∈ omega ⟶ ∀ x7 . x7 ∈ omega ⟶ ∀ x8 . x8 ∈ omega ⟶ ∀ x9 . x9 ∈ omega ⟶ x0 = add_SNo (mul_SNo x6 x6) (add_SNo (mul_SNo x7 x7) (add_SNo (mul_SNo x8 x8) (mul_SNo x9 x9))) ⟶ x5) ⟶ x5

as obj
-

as prop
0a868..

theory
HotG

stx
6cb05..

address
TMURn..