Proofgold Term Root Disambiguation

∀ x0 x1 x2 . x1 ∈ int ⟶ gcd_reln x0 (add_SNo x1 (minus_SNo x0)) x2 ⟶ gcd_reln x0 x1 x2

as obj
-

as prop
29c3b..^{euclidean_algorithm_prop_1}

theory
HotG

stx
e9e67..

address
TMRRL..^{euclidean_algorithm_prop_1}