:: Euclid's Algorithm
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 8, 1993
:: Copyright (c) 1993-2016 Association of Mizar Users

environ

vocabularies HIDDEN, 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 HIDDEN, 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;
definitions EXTPRO_1, TARSKI, COMPOS_1;
theorems INT_1, ABSVALUE, INT_2, TARSKI, ENUMSET1, NAT_1, FUNCOP_1, PARTFUN1, FUNCT_4, FUNCT_1, GRFUNC_1, ZFMISC_1, AMI_3, RELAT_1, RELSET_1, XBOOLE_0, NEWTON, XXREAL_0, ORDINAL1, NAT_D, CARD_1, PBOOLE, EXTPRO_1, MEMSTR_0, XTUPLE_0;
schemes NAT_1, NAT_D, FUNCT_1, RELSET_1, NEWTON;
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;
constructors HIDDEN, NAT_D, AMI_3, RELSET_1, PRE_POLY, DOMAIN_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities FUNCOP_1, FUNCT_4, MEMSTR_0;
expansions TARSKI, COMPOS_1, MEMSTR_0;


set a = dl. 0;

set b = dl. 1;

set c = dl. 2;

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

Lm2: dl. 2 <> dl. 0
by AMI_3:10;

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)))));
coherence
(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))))) is NAT -defined the InstructionsF of SCM -valued finite Function ;
end;

:: deftheorem defines Euclid-Algorithm AMI_4:def 1 :
Euclid-Algorithm = (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)))));

defpred S1[ Instruction-Sequence 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 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 0);

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

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

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

set EA1 = (1 .--> (Divide ((dl. 0),(dl. 1)))) +* ((2 .--> ((dl. 0) := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 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 0)) +* (4 .--> (halt SCM)))));

theorem Th1: :: AMI_4:1
dom Euclid-Algorithm = 5
proof end;

Lm3: for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds
S1[P]
proof end;

theorem Th2: :: AMI_4:2
for s being State of SCM
for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds
for k being Nat 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) )
proof end;

theorem Th3: :: AMI_4:3
for s being State of SCM
for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds
for k being Nat 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) )
proof end;

theorem Th4: :: AMI_4:4
for s being State of SCM
for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds
for k being Nat 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) )
proof end;

theorem Th5: :: AMI_4:5
for s being State of SCM
for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds
for k being Nat 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) )
proof end;

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

Lm4: for k being Nat
for s being 0 -started State of SCM
for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P & s . (dl. 0) > 0 & s . (dl. 1) > 0 holds
( (Comput (P,s,(4 * k))) . (dl. 0) > 0 & ( ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 & IC (Comput (P,s,(4 * k))) = 0 ) or ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 & IC (Comput (P,s,(4 * k))) = 4 ) ) )
proof end;

Lm5: for k being Nat
for s being 0 -started State of SCM
for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P & s . (dl. 0) > 0 & s . (dl. 1) > 0 & (Comput (P,s,(4 * k))) . (dl. 1) > 0 holds
( (Comput (P,s,(4 * (k + 1)))) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 1) & (Comput (P,s,(4 * (k + 1)))) . (dl. 1) = ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) )
proof end;

Lm6: for s being 0 -started State of SCM
for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds
for x, y being Integer st s . (dl. 0) = x & s . (dl. 1) = y & x > y & y > 0 holds
( (Result (P,s)) . (dl. 0) = x gcd y & ex k being Nat st P halts_at IC (Comput (P,s,k)) )
proof end;

theorem Th7: :: AMI_4:7
for s being 0 -started State of SCM
for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds
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
proof end;

definition
func Euclid-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 b1 being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st
for p, q being FinPartState of SCM holds
( [p,q] in b1 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 b1, b2 being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st ( for p, q being FinPartState of SCM holds
( [p,q] in b1 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 b2 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
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Euclid-Function AMI_4:def 2 :
for b1 being PartFunc of (FinPartSt SCM),(FinPartSt SCM) holds
( b1 = Euclid-Function iff for p, q being FinPartState of SCM holds
( [p,q] in b1 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 Th8: :: 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) ) )
proof end;

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

registration
cluster Euclid-Algorithm -> NAT -defined the InstructionsF of SCM -valued finite ;
coherence
Euclid-Algorithm is the InstructionsF of SCM -valued ;
end;

registration
cluster Euclid-Algorithm -> NAT -defined the InstructionsF of SCM -valued finite non halt-free ;
coherence
not Euclid-Algorithm is halt-free
proof end;
end;

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