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

environ

 vocabularies INT_1, NAT_1, ARYTM_3, ABSVALUE, FUNCT_1, AMI_3, AMI_1, CAT_1,
      FUNCT_4, RELAT_1, BOOLE, AMI_2, INT_2, PARTFUN1, FUNCOP_1, AMI_4, ARYTM;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, NUMBERS, RELAT_1, FUNCT_1,
      INT_1, NAT_1, NAT_D, FUNCOP_1, INT_2, STRUCT_0, PARTFUN1, AMI_1, SCMNORM,
      AMI_3, XXREAL_0;
 constructors ENUMSET1, XXREAL_0, NAT_1, NAT_D, AMI_3;
 registrations SETFAM_1, ORDINAL1, RELSET_1, FRAENKEL, NUMBERS, XXREAL_0,
      XREAL_0, NAT_1, INT_1, CARD_3, STRUCT_0, AMI_3, AMI_1, XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

reserve i,j,k for Element of NAT;

begin :: Euclide algorithm

definition let i be Nat, I be Instruction of SCM;
 redefine func i .--> I -> programmed FinPartState of SCM;
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))));
end;

canceled 3;

theorem :: AMI_4:4
  dom (Euclide-Algorithm qua Function) = 5;

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) = 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;

theorem :: AMI_4:6
  for s being State of SCM st Euclide-Algorithm c= s
  for k 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;

theorem :: AMI_4:7
  for s being State of SCM st Euclide-Algorithm c= s
  for k 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;

theorem :: AMI_4:8
  for s being State of SCM st Euclide-Algorithm c= s
  for k 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;

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

theorem :: AMI_4:10
  for s being State of SCM st s starts_at 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;