for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS st GCD-Algorithm c= P holds
for x, y being Integer st s . (intpos 9) = x & s . (intpos 10) = y & x >= 0 & y >= 0 holds
(Result (P,s)) . (intpos 9) = x gcd y