theorem :: SCPINVAR:19

for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for x, y being Integer st s . (intpos 1) = x & s . (intpos 2) = y & x > 0 & y > 0 holds
( (IExec (GCD-Algorithm,P,s)) . (intpos 1) = x gcd y & (IExec (GCD-Algorithm,P,s)) . (intpos 2) = x gcd y & GCD-Algorithm is_closed_on s,P & GCD-Algorithm is_halting_on s,P ) by Lm14;