theorem :: SCMP_GCD:15

for p being FinPartState of SCMPDS
for x, y being Integer st y >= 0 & x >= y & p = ((intpos 9),(intpos 10)) --> (x,y) holds
Initialize p is GCD-Algorithm -autonomic