Proofgold Term Root Disambiguation

and (and (and (and (and (and (∀ x0 . x0 ∈ setminus omega (Sing 0) ⟶ gcd_reln x0 x0 x0) (∀ x0 . x0 ∈ setminus omega (Sing 0) ⟶ gcd_reln 0 x0 x0)) (∀ x0 . x0 ∈ setminus omega (Sing 0) ⟶ gcd_reln x0 0 x0)) (∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ SNoLt x0 x1 ⟶ ∀ x2 . gcd_reln x0 (add_SNo x1 (minus_SNo x0)) x2 ⟶ gcd_reln x0 x1 x2)) (∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ omega ⟶ SNoLt x1 x0 ⟶ ∀ x2 . gcd_reln x1 x0 x2 ⟶ gcd_reln x0 x1 x2)) (∀ x0 . x0 ∈ omega ⟶ ∀ x1 . x1 ∈ int ⟶ SNoLt x1 0 ⟶ ∀ x2 . gcd_reln x0 (minus_SNo x1) x2 ⟶ gcd_reln x0 x1 x2)) (∀ x0 . x0 ∈ int ⟶ ∀ x1 . x1 ∈ int ⟶ SNoLt x0 0 ⟶ ∀ x2 . gcd_reln (minus_SNo x0) x1 x2 ⟶ gcd_reln x0 x1 x2)

as obj
-

as prop
24974..^{euclidean_algorithm}

theory
HotG

stx
e9e67..

address
TMN2U..^{euclidean_algorithm}