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 > y & y > 0 holds
( (Result P,s) . (dl. 0 ) = x gcd y & ex k being Element of NAT st P halts_at IC (Comput P,s,k) )
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 > y & y > 0 holds
( (Result P,s) . (dl. 0 ) = x gcd y & ex k being Element of NAT st P halts_at IC (Comput P,s,k) ) )
assume A2: Euclide-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 Element of NAT st P halts_at IC (Comput P,s,k) )
deffunc H₁( Element of NAT ) -> Element of NAT = abs ((Comput P,s,(4 * $1)) . (dl. 1));
deffunc H₂( Element of NAT ) -> Element of NAT = abs ((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 Element of NAT st P halts_at IC (Comput P,s,k) ) )
assume that
A3: s . (dl. 0 ) = x and
A4: s . (dl. 1) = y and
A5: x > y and
A6: y > 0 ; :: thesis: ( (Result P,s) . (dl. 0 ) = x gcd y & ex k being Element of NAT st P halts_at IC (Comput P,s,k) )

A7: now

let k be Element of NAT ; :: thesis: ( H₁(k) > 0 implies ( H₂(k + 1) = H₁(k) & H₁(k + 1) = H₂(k) mod H₁(k) ) )
A8: ( (Comput P,s,(4 * k)) . (dl. 1) > 0 or (Comput P,s,(4 * k)) . (dl. 1) = 0 ) by A2, A3, A4, A5, A6, Lm4;
assume A9: H₁(k) > 0 ; :: thesis: ( H₂(k + 1) = H₁(k) & H₁(k + 1) = H₂(k) mod H₁(k) )
hence H₂(k + 1) = H₁(k) by A2, A3, A4, A5, A6, A8, Lm5, ABSVALUE:7; :: thesis: H₁(k + 1) = H₂(k) mod H₁(k)
A10: (Comput P,s,(4 * k)) . (dl. 0 ) >= 0 by A2, A3, A4, A5, A6, Lm4;
(Comput P,s,(4 * (k + 1))) . (dl. 1) >= 0 by A2, A3, A4, A5, A6, Lm4;
hence H₁(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 A2, A3, A4, A5, A6, A8, A9, Lm5, ABSVALUE:7
.= H₂(k) mod H₁(k) by A8, A10, INT_2:49 ;
:: thesis: verum

end;

reconsider x9 = x, y9 = y as Element of NAT by A5, A6, INT_1:16;
A11: y9 < x9 by A5;
A12: H₂( 0 ) = abs x by A3, AMI_1:13
.= x9 by ABSVALUE:def 1 ;
A13: H₁( 0 ) = abs y by A4, AMI_1:13
.= y9 by ABSVALUE:def 1 ;
A14: 0 < y9 by A6;
consider k being Element of NAT such that
A15: H₂(k) = x9 gcd y9 and
A16: H₁(k) = 0 from NEWTON:sch 1(A14, A11, A12, A13, A7);
A17: (Comput P,s,(4 * k)) . (dl. 0 ) > 0 by A2, A3, A4, A5, A6, Lm4;
(Comput P,s,(4 * k)) . (dl. 1) = 0 by A16, ABSVALUE:7;
then A18: IC (Comput P,s,(4 * k)) = 4 by A2, A3, A4, A5, A6, Lm4;
A19: P halts_at 4 by A2, Lm3;
hence (Result P,s) . (dl. 0 ) = (Comput P,s,(4 * k)) . (dl. 0 ) by A18, AMI_1:87
.= x gcd y by A15, A17, ABSVALUE:def 1 ;
:: thesis: ex k being Element of NAT st P halts_at IC (Comput P,s,k)
thus ex k being Element of NAT st P halts_at IC (Comput P,s,k) by A18, A19; :: thesis: verum