Proofgold Proposition

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)

type
prop

theory
HotG

name
euclidean_algorithm

proof
PUVXT..

Megalodon
euclidean_algorithm

proofgold address
TMZk4..^{euclidean_algorithm}

creator
29757 PrQUS../31a44..

owner
29757 PrQUS../31a44..

term root
d87f0..