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


begin

set a = dl. 0;

set b = dl. 1;

set c = dl. 2;

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

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

begin

definition
let i be Nat;
let I be Instruction of SCM;
:: original: .-->
redefine func i .--> I -> NAT -defined FinPartState of ;
correctness
coherence
i .--> I is NAT -defined FinPartState of ;
proof end;
end;

definition
func Euclide-Algorithm -> NAT -defined FinPartState of 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 FinPartState of ;
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[ the Instructions of SCM -valued ManySortedSet of NAT ] 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 :: AMI_4:1
canceled;

theorem :: AMI_4:2
canceled;

theorem :: AMI_4:3
canceled;

theorem Th4: :: AMI_4:4
dom Euclide-Algorithm = 5
proof end;

Lm3: for P being the Instructions of SCM -valued ManySortedSet of NAT st Euclide-Algorithm c= P holds
S1[P]
proof end;

begin

theorem Th5: :: AMI_4:5
for s being State of SCM
for P being the Instructions of SCM -valued ManySortedSet of NAT 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 & (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 Th6: :: AMI_4:6
for s being State of SCM
for P being the Instructions of SCM -valued ManySortedSet of NAT 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 & (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 Th7: :: AMI_4:7
for s being State of SCM
for P being the Instructions of SCM -valued ManySortedSet of NAT 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 & (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 Th8: :: AMI_4:8
for s being State of SCM
for P being the Instructions of SCM -valued ManySortedSet of NAT 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 ) & ( (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 Th9: :: AMI_4:9
for s being State of SCM
for P being the Instructions of SCM -valued ManySortedSet of NAT 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)
proof end;

Lm4: for k being Element of NAT
for s being 0 -started State of SCM
for P being the Instructions of SCM -valued ManySortedSet of NAT st Euclide-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 Element of NAT
for s being 0 -started State of SCM
for P being the Instructions of SCM -valued ManySortedSet of NAT st Euclide-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 the Instructions of SCM -valued ManySortedSet of NAT st Euclide-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 Element of NAT st P halts_at IC (Comput (P,s,k)) )
proof end;

theorem Th10: :: AMI_4:10
for s being 0 -started State of SCM
for P being the Instructions of SCM -valued ManySortedSet of NAT st Euclide-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 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 & 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 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 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) );

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

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

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

registration
cluster Euclide-Algorithm -> NAT -defined non halt-free ;
coherence
not Euclide-Algorithm is halt-free
proof end;
end;

theorem :: AMI_4:13
ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm),(Start-At (0,SCM)) +* Euclide-Algorithm computes Euclide-Function
proof end;