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 > y & y > 0 holds

( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) )

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 > y & y > 0 holds

( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) ) )

assume A1: Euclid-Algorithm c= P ; :: thesis: for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 holds

( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) )

deffunc H_{1}( Nat) -> Element of NAT = |.((Comput (P,s,(4 * $1))) . (dl. 1)).|;

deffunc H_{2}( Nat) -> Element of NAT = |.((Comput (P,s,(4 * $1))) . (dl. 0)).|;

let x, y be Integer; :: thesis: ( s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 implies ( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) ) )

assume that

A2: s . (dl. 0) = x and

A3: s . (dl. 1) = y and

A4: x > y and

A5: y > 0 ; :: thesis: ( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) )

A10: y9 < x9 by A4;

A11: H_{2}( 0 ) =
|.x.|
by A2, EXTPRO_1:2

.= x9 by ABSVALUE:def 1 ;

A12: H_{1}( 0 ) =
|.y.|
by A3, EXTPRO_1:2

.= y9 by ABSVALUE:def 1 ;

A13: 0 < y9 by A5;

consider k being Nat such that

A14: H_{2}(k) = x9 gcd y9
and

A15: H_{1}(k) = 0
from NEWTON:sch 1(A13, A10, A11, A12, A6);

A16: (Comput (P,s,(4 * k))) . (dl. 0) > 0 by A1, A2, A3, A4, A5, Lm4;

(Comput (P,s,(4 * k))) . (dl. 1) = 0 by A15, ABSVALUE:2;

then A17: IC (Comput (P,s,(4 * k))) = 4 by A1, A2, A3, A4, A5, Lm4;

A18: P halts_at 4 by A1, Lm3;

hence (Result (P,s)) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 0) by A17, EXTPRO_1:18

.= x gcd y by A14, A16, ABSVALUE:def 1 ;

:: thesis: ex k being Nat st P halts_at IC (Comput (P,s,k))

thus ex k being Nat st P halts_at IC (Comput (P,s,k)) by A17, A18; :: thesis: verum

for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 holds

( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) )

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 > y & y > 0 holds

( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) ) )

assume A1: Euclid-Algorithm c= P ; :: thesis: for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 holds

( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) )

deffunc H

deffunc H

let x, y be Integer; :: thesis: ( s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 implies ( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) ) )

assume that

A2: s . (dl. 0) = x and

A3: s . (dl. 1) = y and

A4: x > y and

A5: y > 0 ; :: thesis: ( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) )

A6: now :: thesis: for k being Nat st H_{1}(k) > 0 holds

( H_{2}(k + 1) = H_{1}(k) & H_{1}(k + 1) = H_{2}(k) mod H_{1}(k) )

reconsider x9 = x, y9 = y as Element of NAT by A4, A5, INT_1:3;( H

let k be Nat; :: thesis: ( H_{1}(k) > 0 implies ( H_{2}(k + 1) = H_{1}(k) & H_{1}(k + 1) = H_{2}(k) mod H_{1}(k) ) )

A7: ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 or (Comput (P,s,(4 * k))) . (dl. 1) = 0 ) by A1, A2, A3, A4, A5, Lm4;

assume A8: H_{1}(k) > 0
; :: thesis: ( H_{2}(k + 1) = H_{1}(k) & H_{1}(k + 1) = H_{2}(k) mod H_{1}(k) )

hence H_{2}(k + 1) = H_{1}(k)
by A1, A2, A3, A4, A5, A7, Lm5, ABSVALUE:2; :: thesis: H_{1}(k + 1) = H_{2}(k) mod H_{1}(k)

A9: (Comput (P,s,(4 * k))) . (dl. 0) >= 0 by A1, A2, A3, A4, A5, Lm4;

(Comput (P,s,(4 * (k + 1)))) . (dl. 1) >= 0 by A1, A2, A3, A4, A5, Lm4;

hence H_{1}(k + 1) =
(Comput (P,s,(4 * (k + 1)))) . (dl. 1)
by ABSVALUE:def 1

.= ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) by A1, A2, A3, A4, A5, A7, A8, Lm5, ABSVALUE:2

.= H_{2}(k) mod H_{1}(k)
by A7, A9, INT_2:32
;

:: thesis: verum

end;A7: ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 or (Comput (P,s,(4 * k))) . (dl. 1) = 0 ) by A1, A2, A3, A4, A5, Lm4;

assume A8: H

hence H

A9: (Comput (P,s,(4 * k))) . (dl. 0) >= 0 by A1, A2, A3, A4, A5, Lm4;

(Comput (P,s,(4 * (k + 1)))) . (dl. 1) >= 0 by A1, A2, A3, A4, A5, Lm4;

hence H

.= ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) by A1, A2, A3, A4, A5, A7, A8, Lm5, ABSVALUE:2

.= H

:: thesis: verum

A10: y9 < x9 by A4;

A11: H

.= x9 by ABSVALUE:def 1 ;

A12: H

.= y9 by ABSVALUE:def 1 ;

A13: 0 < y9 by A5;

consider k being Nat such that

A14: H

A15: H

A16: (Comput (P,s,(4 * k))) . (dl. 0) > 0 by A1, A2, A3, A4, A5, Lm4;

(Comput (P,s,(4 * k))) . (dl. 1) = 0 by A15, ABSVALUE:2;

then A17: IC (Comput (P,s,(4 * k))) = 4 by A1, A2, A3, A4, A5, Lm4;

A18: P halts_at 4 by A1, Lm3;

hence (Result (P,s)) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 0) by A17, EXTPRO_1:18

.= x gcd y by A14, A16, ABSVALUE:def 1 ;

:: thesis: ex k being Nat st P halts_at IC (Comput (P,s,k))

thus ex k being Nat st P halts_at IC (Comput (P,s,k)) by A17, A18; :: thesis: verum