let s be 0 -started State of SCM ; :: thesis: for P being the Instructions of SCM -valued ManySortedSet of NAT st Euclide-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
let P be the Instructions of SCM -valued ManySortedSet of NAT ; :: thesis: ( Euclide-Algorithm c= P implies 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 )
assume A2: Euclide-Algorithm c= P ; :: thesis: 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
let x, y be Integer; :: thesis: ( s . (dl. 0 ) = x & s . (dl. 1) = y & x > 0 & y > 0 implies (Result P,s) . (dl. 0 ) = x gcd y )
assume that
A3: ( s . (dl. 0 ) = x & s . (dl. 1) = y ) and
A4: x > 0 and
A5: y > 0 ; :: thesis: (Result P,s) . (dl. 0 ) = x gcd y
A6: abs y = y by A5, ABSVALUE:def 1;

now

per cases ( x > y or x = y or y > x ) by XXREAL_0:1;

case x > y ; :: thesis: (Result P,s) . (dl. 0 ) = x gcd y

hence (Result P,s) . (dl. 0 ) = x gcd y by A2, A3, A5, Lm6; :: thesis: verum

end;

case A7: x = y ; :: thesis: ex s9 being set st (Result P,s) . (dl. 0 ) = x gcd y

reconsider x9 = x, y9 = y as Element of NAT by A4, A5, INT_1:16;
take s9 = Comput P,s,4; :: thesis: (Result P,s) . (dl. 0 ) = x gcd y
A8: s = Comput P,s,(4 * 0 ) by AMI_1:13;
A9: s9 = Comput P,s,(4 * (0 + 1)) ;
x mod y = x9 mod y9
.= 0 by A7, NAT_D:25 ;
then s9 . (dl. 1) = 0 by A2, A3, A4, A5, A8, A9, Lm5;
then IC s9 = 4 by A2, A3, A4, A5, A9, Lm4;
then P halts_at IC s9 by A2, Lm3;
hence (Result P,s) . (dl. 0 ) = s9 . (dl. 0 ) by AMI_1:87
.= y by A2, A3, A4, A5, A8, A9, Lm5
.= x gcd y by A6, A7, NAT_D:32 ;
:: thesis: verum

end;

case A10: y > x ; :: thesis: ex s9 being set st (Result P,s) . (dl. 0 ) = x gcd y

reconsider x9 = x, y9 = y as Element of NAT by A4, A5, INT_1:16;
take s9 = Comput P,s,4; :: thesis: (Result P,s) . (dl. 0 ) = x gcd y
A11: s9 = Comput P,s,(4 * (0 + 1)) ;
A12: s = Comput P,s,(4 * 0 ) by AMI_1:13;
then A13: s9 . (dl. 0 ) = y by A2, A3, A4, A5, A11, Lm5;
A14: Euclide-Algorithm c= P by A2;
x mod y = x9 mod y9
.= x9 by A10, NAT_D:24 ;
then A15: s9 . (dl. 1) = x by A2, A3, A4, A5, A12, A11, Lm5;
then IC s9 = 0 by A2, A3, A4, A5, A11, Lm4;
then A16: s9 is 0 -started by COMPOS_1:def 20;
then consider k0 being Element of NAT such that
A17: P halts_at IC (Comput P,s9,k0) by A4, A10, A13, A15, A14, Lm6;
Comput P,s,(k0 + 4) = Comput P,s9,k0 by AMI_1:51;
then A18: P halts_at IC (Comput P,s,(k0 + 4)) by A17;
(Result P,s9) . (dl. 0 ) = x gcd y by A4, A10, A13, A15, A16, A14, Lm6;
hence (Result P,s) . (dl. 0 ) = x gcd y by A18, AMI_1:90; :: thesis: verum

end;

end;

end;

hence (Result P,s) . (dl. 0 ) = x gcd y ; :: thesis: verum