:: Euclide Algorithm
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 8, 1993
:: Copyright (c) 1993 Association of Mizar Users

set a = dl. 0 ;

set b = dl. 1;

set c = dl. 2;

Lm1: ( dl. 0 <> dl. 1 & dl. 1 <> dl. 2 & dl. 2 <> dl. 0 )
by AMI_3:52;

definition

let i be Nat;
let I be Instruction of SCM ;
:: original: .-->
redefine func i .--> I -> programmed FinPartState of SCM ;
correctness
coherence
i .--> I is programmed FinPartState of SCM ;

proof end;

end;

definition

func Euclide-Algorithm -> programmed FinPartState of SCM equals :: AMI_4:def 1
(0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide (dl. 0 ),(dl. 1))) +* ((2 .--> ((dl. 0 ) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto (il. 0 ))) +* (4 .--> (halt SCM )))));
coherence
(0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide (dl. 0 ),(dl. 1))) +* ((2 .--> ((dl. 0 ) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto (il. 0 ))) +* (4 .--> (halt SCM ))))) is programmed FinPartState of SCM ;

end;

:: deftheorem defines Euclide-Algorithm AMI_4:def 1 :

Euclide-Algorithm = (0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide (dl. 0 ),(dl. 1))) +* ((2 .--> ((dl. 0 ) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto (il. 0 ))) +* (4 .--> (halt SCM )))));

defpred S₁[ State of SCM ] means ( $1 . 0 = (dl. 2) := (dl. 1) & $1 . 1 = Divide (dl. 0 ),(dl. 1) & $1 . 2 = (dl. 0 ) := (dl. 2) & $1 . 3 = (dl. 1) >0_goto (il. 0 ) & $1 halts_at 4 );

set IN0 = 0 .--> ((dl. 2) := (dl. 1));

set IN1 = 1 .--> (Divide (dl. 0 ),(dl. 1));

set IN2 = 2 .--> ((dl. 0 ) := (dl. 2));

set IN3 = 3 .--> ((dl. 1) >0_goto (il. 0 ));

set IN4 = 4 .--> (halt SCM );

set EA3 = (3 .--> ((dl. 1) >0_goto (il. 0 ))) +* (4 .--> (halt SCM ));

set EA2 = (2 .--> ((dl. 0 ) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto (il. 0 ))) +* (4 .--> (halt SCM )));

set EA1 = (1 .--> (Divide (dl. 0 ),(dl. 1))) +* ((2 .--> ((dl. 0 ) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto (il. 0 ))) +* (4 .--> (halt SCM ))));

set EA0 = (0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide (dl. 0 ),(dl. 1))) +* ((2 .--> ((dl. 0 ) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto (il. 0 ))) +* (4 .--> (halt SCM )))));

theorem :: AMI_4:1

canceled;

theorem :: AMI_4:2

canceled;

theorem :: AMI_4:3

canceled;

theorem Th4: :: AMI_4:4

dom Euclide-Algorithm = 5

proof end;

Lm2: for s being State of SCM st Euclide-Algorithm c= s holds
S₁[s]

proof end;

theorem Th5: :: AMI_4:5

for s being State of SCM st Euclide-Algorithm c= s holds
for k being Element of NAT st IC (Computation s,k) = 0 holds
( IC (Computation s,(k + 1)) = 1 & (Computation s,(k + 1)) . (dl. 0 ) = (Computation s,k) . (dl. 0 ) & (Computation s,(k + 1)) . (dl. 1) = (Computation s,k) . (dl. 1) & (Computation s,(k + 1)) . (dl. 2) = (Computation s,k) . (dl. 1) )

proof end;

theorem Th6: :: AMI_4:6

for s being State of SCM st Euclide-Algorithm c= s holds
for k being Element of NAT st IC (Computation s,k) = 1 holds
( IC (Computation s,(k + 1)) = 2 & (Computation s,(k + 1)) . (dl. 0 ) = ((Computation s,k) . (dl. 0 )) div ((Computation s,k) . (dl. 1)) & (Computation s,(k + 1)) . (dl. 1) = ((Computation s,k) . (dl. 0 )) mod ((Computation s,k) . (dl. 1)) & (Computation s,(k + 1)) . (dl. 2) = (Computation s,k) . (dl. 2) )

proof end;

theorem Th7: :: AMI_4:7

for s being State of SCM st Euclide-Algorithm c= s holds
for k being Element of NAT st IC (Computation s,k) = 2 holds
( IC (Computation s,(k + 1)) = 3 & (Computation s,(k + 1)) . (dl. 0 ) = (Computation s,k) . (dl. 2) & (Computation s,(k + 1)) . (dl. 1) = (Computation s,k) . (dl. 1) & (Computation s,(k + 1)) . (dl. 2) = (Computation s,k) . (dl. 2) )

proof end;

theorem Th8: :: AMI_4:8

for s being State of SCM st Euclide-Algorithm c= s holds
for k being Element of NAT st IC (Computation s,k) = 3 holds
( ( (Computation s,k) . (dl. 1) > 0 implies IC (Computation s,(k + 1)) = 0 ) & ( (Computation s,k) . (dl. 1) <= 0 implies IC (Computation s,(k + 1)) = 4 ) & (Computation s,(k + 1)) . (dl. 0 ) = (Computation s,k) . (dl. 0 ) & (Computation s,(k + 1)) . (dl. 1) = (Computation s,k) . (dl. 1) )

proof end;

theorem Th9: :: AMI_4:9

for s being State of SCM st Euclide-Algorithm c= s holds
for k, i being Element of NAT st IC (Computation s,k) = 4 holds
Computation s,(k + i) = Computation s,k

proof end;

Lm3: for k being Element of NAT
for s being State of SCM st s starts_at 0 & Euclide-Algorithm c= s & s . (dl. 0 ) > 0 & s . (dl. 1) > 0 holds
( (Computation s,(4 * k)) . (dl. 0 ) > 0 & ( ( (Computation s,(4 * k)) . (dl. 1) > 0 & IC (Computation s,(4 * k)) = 0 ) or ( (Computation s,(4 * k)) . (dl. 1) = 0 & IC (Computation s,(4 * k)) = 4 ) ) )

proof end;

Lm4: for k being Element of NAT
for s being State of SCM st s starts_at 0 & Euclide-Algorithm c= s & s . (dl. 0 ) > 0 & s . (dl. 1) > 0 & (Computation s,(4 * k)) . (dl. 1) > 0 holds
( (Computation s,(4 * (k + 1))) . (dl. 0 ) = (Computation s,(4 * k)) . (dl. 1) & (Computation s,(4 * (k + 1))) . (dl. 1) = ((Computation s,(4 * k)) . (dl. 0 )) mod ((Computation s,(4 * k)) . (dl. 1)) )

proof end;

Lm5: for s being State of SCM st s starts_at 0 & Euclide-Algorithm c= s holds
for x, y being Integer st s . (dl. 0 ) = x & s . (dl. 1) = y & x > y & y > 0 holds
( (Result s) . (dl. 0 ) = x gcd y & ex k being Element of NAT st s halts_at IC (Computation s,k) )

proof end;

theorem Th10: :: AMI_4:10

for s being State of SCM st s starts_at 0 & Euclide-Algorithm c= s holds
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

proof end;

definition

func Euclide-Function -> PartFunc of FinPartSt SCM , FinPartSt SCM means :Def2: :: AMI_4:def 2
for p, q being FinPartState of SCM holds
( [p,q] in it iff ex x, y being Integer st
( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y & q = (dl. 0 ) .--> (x gcd y) ) );
existence
ex b₁ being PartFunc of FinPartSt SCM , FinPartSt SCM st
for p, q being FinPartState of SCM holds
( [p,q] in b₁ iff ex x, y being Integer st
( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y & q = (dl. 0 ) .--> (x gcd y) ) )

proof end;

uniqueness
for b₁, b₂ being PartFunc of FinPartSt SCM , FinPartSt SCM st ( for p, q being FinPartState of SCM holds
( [p,q] in b₁ iff ex x, y being Integer st
( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y & q = (dl. 0 ) .--> (x gcd y) ) ) ) & ( for p, q being FinPartState of SCM holds
( [p,q] in b₂ iff ex x, y being Integer st
( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y & q = (dl. 0 ) .--> (x gcd y) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines Euclide-Function AMI_4:def 2 :

for b₁ being PartFunc of FinPartSt SCM , FinPartSt SCM holds
( b₁ = Euclide-Function iff for p, q being FinPartState of SCM holds
( [p,q] in b₁ iff ex x, y being Integer st
( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y & q = (dl. 0 ) .--> (x gcd y) ) ) );

theorem Th11: :: AMI_4:11

for p being set holds
( p in dom Euclide-Function iff ex x, y being Integer st
( x > 0 & y > 0 & p = (dl. 0 ),(dl. 1) --> x,y ) )

proof end;

theorem Th12: :: AMI_4:12

for i, j being Integer st i > 0 & j > 0 holds
Euclide-Function . ((dl. 0 ),(dl. 1) --> i,j) = (dl. 0 ) .--> (i gcd j)

proof end;

theorem :: AMI_4:13

(Start-At (il. 0 )) +* Euclide-Algorithm computes Euclide-Function

proof end;