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

now

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

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

hence (Result s) . (dl. 0 ) = x gcd y by A1, A2, A3, A4, A6, Lm5; :: thesis: verum

end;

case A8: x = y ; :: thesis: ex s' being Element of K234(the Object-Kind of SCM ) st (Result s) . (dl. 0 ) = x gcd y

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

end;

case A11: y > x ; :: thesis: ex s' being Element of K234(the Object-Kind of SCM ) st (Result s) . (dl. 0 ) = x gcd y

take s' = Computation s,4; :: thesis: (Result s) . (dl. 0 ) = x gcd y
reconsider x' = x, y' = y as Element of NAT by A5, A6, INT_1:16;
A12: x mod y = x' mod y'
.= x' by A11, NAT_D:24 ;
A13: ( s = Computation s,(4 * 0 ) & s' = Computation s,(4 * (0 + 1)) ) by AMI_1:13;
then A14: ( s' . (dl. 0 ) = y & s' . (dl. 1) = x ) by A1, A2, A3, A4, A5, A6, A12, Lm4;
then IC s' = 0 by A1, A2, A3, A4, A5, A6, A13, Lm3;
then A15: s' starts_at 0 by AMI_1:def 41;
A16: Euclide-Algorithm c= s' by A2, AMI_1:86;
then consider k0 being Element of NAT such that
A17: s' halts_at IC (Computation s',k0) by A5, A11, A14, A15, Lm5;
Computation s,(k0 + 4) = Computation s',k0 by AMI_1:51;
then A18: s halts_at IC (Computation s,(k0 + 4)) by A17, AMI_1:91;
(Result s') . (dl. 0 ) = x gcd y by A5, A11, A14, A15, A16, Lm5;
hence (Result s) . (dl. 0 ) = x gcd y by A18, AMI_1:90; :: thesis: verum

end;

end;

end;

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