let s be 0 -started State of SCM; :: thesis: 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
let P be Instruction-Sequence of SCM; :: thesis: ( Euclid-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 A1: Euclid-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
A2: ( s . (dl. 0) = x & s . (dl. 1) = y ) and
A3: x > 0 and
A4: y > 0 ; :: thesis: (Result (P,s)) . (dl. 0) = x gcd y
A5: |.y.| = y by A4, ABSVALUE:def 1;
now :: thesis: ( ( x > y & (Result (P,s)) . (dl. 0) = x gcd y ) or ( x = y & ex s9 being set st (Result (P,s)) . (dl. 0) = x gcd y ) or ( y > x & ex s9 being set st (Result (P,s)) . (dl. 0) = x gcd y ) )
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 A1, A2, A4, Lm6; :: thesis: verum
end;
case A6: 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 A3, A4, INT_1:3;
take s9 = Comput (P,s,4); :: thesis: (Result (P,s)) . (dl. 0) = x gcd y
A7: s = Comput (P,s,(4 * 0)) by EXTPRO_1:2;
A8: s9 = Comput (P,s,(4 * (0 + 1))) ;
x mod y = x9 mod y9
.= 0 by A6, NAT_D:25 ;
then s9 . (dl. 1) = 0 by A1, A2, A3, A4, A7, A8, Lm5;
then IC s9 = 4 by A1, A2, A3, A4, A8, Lm4;
then P halts_at IC s9 by A1, Lm3;
hence (Result (P,s)) . (dl. 0) = s9 . (dl. 0) by EXTPRO_1:18
.= y by A1, A2, A3, A4, A7, A8, Lm5
.= x gcd y by A5, A6, NAT_D:32 ;
:: thesis: verum
end;
case A9: 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 A3, A4, INT_1:3;
take s9 = Comput (P,s,4); :: thesis: (Result (P,s)) . (dl. 0) = x gcd y
A10: s9 = Comput (P,s,(4 * (0 + 1))) ;
A11: s = Comput (P,s,(4 * 0)) by EXTPRO_1:2;
then A12: s9 . (dl. 0) = y by A1, A2, A3, A4, A10, Lm5;
x mod y = x9 mod y9
.= x9 by A9, NAT_D:24 ;
then A13: s9 . (dl. 1) = x by A1, A2, A3, A4, A11, A10, Lm5;
then IC s9 = 0 by A1, A2, A3, A4, A10, Lm4;
then A14: s9 is 0 -started ;
then consider k0 being Nat such that
A15: P halts_at IC (Comput (P,s9,k0)) by A3, A9, A12, A13, A1, Lm6;
A16: P halts_at IC (Comput (P,s,(k0 + 4))) by A15, EXTPRO_1:4;
(Result (P,s9)) . (dl. 0) = x gcd y by A3, A9, A12, A13, A14, A1, Lm6;
hence (Result (P,s)) . (dl. 0) = x gcd y by A16, EXTPRO_1:21; :: thesis: verum
end;
end;
end;
hence (Result (P,s)) . (dl. 0) = x gcd y ; :: thesis: verum