Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

### Euclid's Algorithm

by
Andrzej Trybulec, and
Yatsuka Nakamura

MML identifier: AMI_4
[ Mizar article, MML identifier index ]

```environ

vocabulary INT_1, NAT_1, ARYTM_3, ARYTM_1, ABSVALUE, FUNCT_1, CQC_LANG, AMI_3,
AMI_1, CAT_1, FUNCT_4, RELAT_1, BOOLE, AMI_2, INT_2, PARTFUN1, FUNCOP_1,
AMI_4;
notation TARSKI, XBOOLE_0, ENUMSET1, NUMBERS, XCMPLX_0, XREAL_0, FUNCT_1,
FUNCT_2, INT_1, NAT_1, CQC_LANG, GROUP_1, INT_2, STRUCT_0, RELAT_1,
PARTFUN1, AMI_1, AMI_3;
constructors ENUMSET1, REAL_1, NAT_1, INT_2, AMI_2, AMI_3, MEMBERED, XBOOLE_0;
clusters AMI_1, AMI_3, RELSET_1, XREAL_0, INT_1, FRAENKEL, MEMBERED, ZFMISC_1,
XBOOLE_0, NUMBERS, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin :: Preliminaries

theorem :: AMI_4:1
for i,j being Integer st i >= 0 & j >= 0
holds i div j >= 0;

theorem :: AMI_4:2
for i,j being Integer st i >= 0 & j > 0
holds abs(i) mod abs(j) = i mod j
& abs(i) div abs(j) = i div j;

reserve i,j,k for Nat;

scheme Euklides' { F(Nat)->Nat,G(Nat)->Nat,a()->Nat,b()->Nat } :
ex k st F(k) = a() hcf b() & G(k) = 0
provided
0 < b() and
b() < a() and
F(0) = a() and
G(0) = b() and
for k st G(k) > 0 holds F(k+1) = G(k) & G(k+1) = F(k) mod G(k);

begin :: Euclide algorithm

definition
func Euclide-Algorithm -> programmed FinPartState of SCM equals
:: AMI_4:def 1

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

canceled;

theorem :: AMI_4:4
dom Euclide-Algorithm = { il.0,il.1,il.2,il.3,il.4 };

begin :: Natural semantics of the program

theorem :: AMI_4:5
for s being State of SCM st Euclide-Algorithm c= s
for k st IC (Computation s).k = il.0
holds IC (Computation s).(k+1) = il.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;

theorem :: AMI_4:6
for s being State of SCM st Euclide-Algorithm c= s
for k st IC (Computation s).k = il.1
holds IC (Computation s).(k+1) = il.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;

theorem :: AMI_4:7
for s being State of SCM st Euclide-Algorithm c= s
for k st IC (Computation s).k = il.2
holds IC (Computation s).(k+1) = il.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;

theorem :: AMI_4:8
for s being State of SCM st Euclide-Algorithm c= s
for k st IC (Computation s).k = il.3
holds
((Computation s).k.dl.1 > 0 implies IC (Computation s).(k+1) = il.0) &
((Computation s).k.dl.1 <= 0 implies IC (Computation s).(k+1) = il.4) &
(Computation s).(k+1).dl.0 = (Computation s).k.dl.0 &
(Computation s).(k+1).dl.1 = (Computation s).k.dl.1;

theorem :: AMI_4:9
for s being State of SCM st Euclide-Algorithm c= s
for k,i st IC (Computation s).k = il.4
holds (Computation s).(k+i) = (Computation s).k;

theorem :: AMI_4:10
for s being State of SCM st s starts_at il.0 & Euclide-Algorithm c= s
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;

definition
func Euclide-Function -> PartFunc of FinPartSt SCM, FinPartSt SCM means
:: 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);
end;

theorem :: 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);

theorem :: 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);

theorem :: AMI_4:13
(Start-At il.0) +* Euclide-Algorithm computes Euclide-Function;
```