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


begin

set a = dl. 0;

set b = dl. 1;

set c = dl. 2;

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

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

begin

definition
func Euclide-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 Euclide-Algorithm AMI_4:def_1_:_
 Euclide-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) &amp; $1 . 1 = Divide ((dl. 0),(dl. 1)) &amp; $1 . 2 = (dl. 0) := (dl. 2) &amp; $1 . 3 = (dl. 1) >0_goto 0 &amp; $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 Euclide-Algorithm = 5
proofend;

Lm3:  for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P holds
S1[P]
proofend;

begin

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

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

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

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

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

Lm4:  for k being Element of NAT
for s being 0 -started State of SCM
for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P &amp; s . (dl. 0) > 0 &amp; s . (dl. 1) > 0 holds
( (Comput (P,s,(4 * k))) . (dl. 0) > 0 &amp; ( ( (Comput (P,s,(4 * k))) . (dl. 1) > 0 &amp; IC (Comput (P,s,(4 * k))) = 0 ) or ( (Comput (P,s,(4 * k))) . (dl. 1) = 0 &amp; IC (Comput (P,s,(4 * k))) = 4 ) ) )
proofend;

Lm5:  for k being Element of NAT
for s being 0 -started State of SCM
for P being Instruction-Sequence of SCM st Euclide-Algorithm c= P &amp; s . (dl. 0) > 0 &amp; s . (dl. 1) > 0 &amp; (Comput (P,s,(4 * k))) . (dl. 1) > 0 holds
( (Comput (P,s,(4 * (k + 1)))) . (dl. 0) = (Comput (P,s,(4 * k))) . (dl. 1) &amp; (Comput (P,s,(4 * (k + 1)))) . (dl. 1) = ((Comput (P,s,(4 * k))) . (dl. 0)) mod ((Comput (P,s,(4 * k))) . (dl. 1)) )
proofend;

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

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

definition
func Euclide-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 &amp; y > 0 &amp; p = ((dl. 0),(dl. 1)) --> (x,y) &amp; 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 &amp; y > 0 &amp; p = ((dl. 0),(dl. 1)) --> (x,y) &amp; q = (dl. 0) .--> (x gcd y) ) )
proofend;
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 &amp; y > 0 &amp; p = ((dl. 0),(dl. 1)) --> (x,y) &amp; q = (dl. 0) .--> (x gcd y) ) ) ) &amp; ( for p, q being FinPartState of SCM holds
( [p,q] in b2 iff ex x, y being Integer st
( x > 0 &amp; y > 0 &amp; p = ((dl. 0),(dl. 1)) --> (x,y) &amp; q = (dl. 0) .--> (x gcd y) ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines Euclide-Function AMI_4:def_2_:_
 for b1 being PartFunc of (FinPartSt SCM),(FinPartSt SCM) holds
( b1 = Euclide-Function iff for p, q being FinPartState of SCM holds
( [p,q] in b1 iff ex x, y being Integer st
( x > 0 &amp; y > 0 &amp; p = ((dl. 0),(dl. 1)) --> (x,y) &amp; q = (dl. 0) .--> (x gcd y) ) ) );

theorem Th8: :: AMI_4:8
for p being set holds
( p in dom Euclide-Function iff ex x, y being Integer st
( x > 0 &amp; y > 0 &amp; p = ((dl. 0),(dl. 1)) --> (x,y) ) )
proofend;

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

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

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

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