:: Euclid's Algorithm
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Copyright (c) 1993-2017 Association of Mizar Users

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

defpred S1[ Instruction-Sequence of SCM] means ( \$1 . 0 = (dl. 2) := (dl. 1) & \$1 . 1 = Divide ((),(dl. 1)) & \$1 . 2 = () := (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. 1)));

set IN2 = 2 .--> (() := (dl. 2));

set IN3 = 3 .--> ((dl. 1) >0_goto 0);

set IN4 = 4 .--> ();

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

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

set EA1 = (1 .--> (Divide ((),(dl. 1)))) +* ((2 .--> (() := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> ())));

set EA0 = (0 .--> ((dl. 2) := (dl. 1))) +* ((1 .--> (Divide ((),(dl. 1)))) +* ((2 .--> (() := (dl. 2))) +* ((3 .--> ((dl. 1) >0_goto 0)) +* (4 .--> ()))));

theorem Th1: :: AMI_4:1
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))) . () = (Comput (P,s,k)) . () & (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))) . () = ((Comput (P,s,k)) . ()) div ((Comput (P,s,k)) . (dl. 1)) & (Comput (P,s,(k + 1))) . (dl. 1) = ((Comput (P,s,k)) . ()) 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))) . () = (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))) . () = (Comput (P,s,k)) . () & (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 . () > 0 & s . (dl. 1) > 0 holds
( (Comput (P,s,(4 * k))) . () > 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 . () > 0 & s . (dl. 1) > 0 & (Comput (P,s,(4 * k))) . (dl. 1) > 0 holds
( (Comput (P,s,(4 * (k + 1)))) . () = (Comput (P,s,(4 * k))) . (dl. 1) & (Comput (P,s,(4 * (k + 1)))) . (dl. 1) = ((Comput (P,s,(4 * k))) . ()) 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 . () = x & s . (dl. 1) = y & x > y & y > 0 holds
( (Result (P,s)) . () = 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 . () = x & s . (dl. 1) = y & x > 0 & y > 0 holds
(Result (P,s)) . () = x gcd y
proof end;

definition
func Euclid-Function -> PartFunc of (),() 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. 1)) --> (x,y) & q = () .--> (x gcd y) ) );
existence
ex b1 being PartFunc of (),() 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. 1)) --> (x,y) & q = () .--> (x gcd y) ) )
proof end;
uniqueness
for b1, b2 being PartFunc of (),() 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. 1)) --> (x,y) & q = () .--> (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. 1)) --> (x,y) & q = () .--> (x gcd y) ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines Euclid-Function AMI_4:def 2 :
for b1 being PartFunc of (),() 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. 1)) --> (x,y) & q = () .--> (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. 1)) --> (x,y) ) )
proof end;

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

registration
coherence ;
end;

registration
coherence
proof end;
end;

theorem :: AMI_4:10
proof end;