theorem Th7: :: AMI_4:7

for s being 0 -started State of SCM
for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds
for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > 0 & y > 0 holds
(Result (P,s)) . (dl. 0) = x gcd y