let s be 0 -started State of SCM; 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; ( 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
; 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 H1( Nat) -> Element of NAT = |.((Comput (P,s,(4 * $1))) . (dl. 1)).|;
deffunc H2( Nat) -> Element of NAT = |.((Comput (P,s,(4 * $1))) . (dl. 0)).|;
let x, y be Integer; ( 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
; ( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) )
A6:
now for k being Nat st H1(k) > 0 holds
( H2(k + 1) = H1(k) & H1(k + 1) = H2(k) mod H1(k) )let k be
Nat;
( H1(k) > 0 implies ( H2(k + 1) = H1(k) & H1(k + 1) = H2(k) mod H1(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:
H1(
k)
> 0
;
( H2(k + 1) = H1(k) & H1(k + 1) = H2(k) mod H1(k) )hence
H2(
k + 1)
= H1(
k)
by A1, A2, A3, A4, A5, A7, Lm5, ABSVALUE:2;
H1(k + 1) = H2(k) mod H1(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 H1(
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
.=
H2(
k)
mod H1(
k)
by A7, A9, INT_2:32
;
verum end;
reconsider x9 = x, y9 = y as Element of NAT by A4, A5, INT_1:3;
A10:
y9 < x9
by A4;
A11: H2( 0 ) =
|.x.|
by A2, EXTPRO_1:2
.=
x9
by ABSVALUE:def 1
;
A12: H1( 0 ) =
|.y.|
by A3, EXTPRO_1:2
.=
y9
by ABSVALUE:def 1
;
A13:
0 < y9
by A5;
consider k being Nat such that
A14:
H2(k) = x9 gcd y9
and
A15:
H1(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
;
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; verum