:: deftheorem Def2 defines Euclid-Function AMI_4:def 2 :
for b₁ being PartFunc of (FinPartSt SCM),(FinPartSt SCM) holds
( b₁ = Euclid-Function iff for p, q being FinPartState of SCM holds
( [p,q] in b₁ iff ex x, y being Integer st
( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) );