:: Euclid's Algorithm
::  by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 8, 1993
:: Copyright (c) 1993-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, AMI_3, CARD_1, NAT_1, AMI_1, FUNCOP_1,
      RELAT_1, GRAPHSP, FUNCT_4, FSM_1, FUNCT_1, XBOOLE_0, TARSKI, ARYTM_3,
      INT_1, XXREAL_0, MSUALG_1, INT_2, COMPLEX1, PARTFUN1, TURING_1, STRUCT_0,
      AMI_4, EXTPRO_1, FINSET_1, COMPOS_1, XCMPLX_0;
 notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
      FUNCT_1, FINSET_1, XCMPLX_0, INT_1, NAT_1, FUNCOP_1, INT_2, FUNCT_4,
      STRUCT_0, PARTFUN1, MEMSTR_0, COMPOS_1, EXTPRO_1, AMI_3, XXREAL_0;
 constructors NAT_D, AMI_3, RELSET_1, PRE_POLY, DOMAIN_1;
 registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, STRUCT_0,
      AMI_3, XBOOLE_0, FINSET_1, MEMSTR_0, FUNCT_4, FUNCOP_1, RELAT_1,
      COMPOS_0;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: Preliminaries

reserve i,j,k for Nat;

begin :: Euclid's algorithm

definition
  func Euclid-Algorithm -> NAT-defined
   (the InstructionsF of SCM)-valued finite Function
    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 0)) +*
  (4 .--> halt SCM))));
end;



theorem :: AMI_4:1
  dom (Euclid-Algorithm qua Function) = 5;

begin :: Natural semantics of the program

theorem :: AMI_4:2
  for s being State of SCM
  for P being Instruction-Sequence of SCM
   st Euclid-Algorithm c= P
  for k st IC Comput(P,s,k) = 0 holds IC Comput(P,s,k+1) = 1 &
  Comput(P,s,k+1).dl.0 = Comput(P,s,k).dl.0 &
  Comput(P,s,k+1).dl.1 = Comput(P,s,k).dl.1 &
  Comput(P,s,k+1).dl.2 = Comput(P,s,k).dl.1;

theorem :: AMI_4:3
  for s being State of SCM
  for P being Instruction-Sequence of SCM
   st Euclid-Algorithm c= P
  for k st IC
Comput(P,s,k) = 1 holds IC Comput(P,s,k+1) = 2 &
Comput(P,s,k+1).dl.0
  = Comput(P,s,k).dl.0 div Comput(P,s,k).dl.1 &
Comput(P,s,k+1).dl.1 =
  Comput(P,s,k).dl.0 mod Comput(P,s,k).dl.1 & Comput(P,s,k+1).dl.2 =
  Comput(P,s,k).dl.2;

theorem :: AMI_4:4
  for s being State of SCM
  for P being Instruction-Sequence of SCM
   st Euclid-Algorithm c= P
  for k st IC
Comput(P,s,k) = 2 holds IC Comput(P,s,k+1) = 3 &
Comput(P,s,k+1).dl.0
  = Comput(P,s,k).dl.2 & Comput(P,s,k+1).dl.1 =
Comput(P,s,k).dl.1 &
  Comput(P,s,k+1).dl.2 = Comput(P,s,k).dl.2;

theorem :: AMI_4:5
 for s being State of SCM
  for P being Instruction-Sequence of SCM
   st Euclid-Algorithm c= P
   for k st IC
Comput(P,s,k) = 3 holds ( Comput(P,s,k).dl.1 > 0
implies IC Comput(P,s,k+1) = 0) &
( Comput(P,s,k).dl.1 <= 0 implies IC Comput(P,s,k+1) = 4) &
  Comput(P,s,k+1).dl.0 = Comput(P,s,k).dl.0 & Comput(P,s,k+1).dl.1 =
  Comput(P,s,k).dl.1;

theorem :: AMI_4:6
  for s being State of SCM
  for P being Instruction-Sequence of SCM
  st Euclid-Algorithm c= P
  for k,i st IC
  Comput(P,s,k) = 4 holds Comput(P,s,k+i) = Comput(P,s,k);

theorem :: AMI_4:7
  for s being 0-started State of SCM
  for P being Instruction-Sequence of SCM
   st Euclid-Algorithm c= P
   for x, y being Integer st s.dl.0 = x & s.dl.1 = y & x > 0 & y > 0 holds (
  Result(P,s)).dl.0 = x gcd y;

definition
  func Euclid-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:8
  for p being set holds p in dom Euclid-Function iff ex x,y being
  Integer st x > 0 & y > 0 & p = (dl.0,dl.1) --> (x,y);

theorem :: AMI_4:9
  for i,j being Integer st i > 0 & j > 0 holds Euclid-Function.((
  dl.0,dl.1) --> (i,j)) = dl.0 .--> (i gcd j);

registration
 cluster Euclid-Algorithm -> (the InstructionsF of SCM)-valued;
end;

registration
 cluster Euclid-Algorithm -> non halt-free;
end;

theorem :: AMI_4:10
  Euclid-Algorithm, Start-At(0,SCM) computes Euclid-Function;