The abstract of the Mizar article:

Euclid's Algorithm

by

Andrzej Trybulec, and

Yatsuka Nakamura

Received October 8, 1993

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;