:: by Andrzej Trybulec and Yatsuka Nakamura

::

:: Received October 8, 1993

:: Copyright (c) 1993-2018 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: dl. 2 <> dl. 0

by AMI_3:10;

definition

(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;

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)))));

(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 ;

:: 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)))));

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 S

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)))));

Lm3: for P being Instruction-Sequence of SCM st Euclid-Algorithm c= P holds

S

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) )

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) )

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) )

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) )

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)

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

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

ex b_{1} being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st

for p, q being FinPartState of SCM holds

( [p,q] in b_{1} 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 b_{1}, b_{2} being PartFunc of (FinPartSt SCM),(FinPartSt SCM) st ( for p, q being FinPartState of SCM holds

( [p,q] in b_{1} 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 b_{2} 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

b_{1} = b_{2}
end;

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 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) ) );

ex b

for p, q being FinPartState of SCM holds

( [p,q] in b

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) )

proof end;

uniqueness for b

( [p,q] in b

( 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 b

( x > 0 & y > 0 & p = ((dl. 0),(dl. 1)) --> (x,y) & q = (dl. 0) .--> (x gcd y) ) ) ) holds

b

proof end;

:: deftheorem Def2 defines Euclid-Function AMI_4:def 2 :

for b_{1} being PartFunc of (FinPartSt SCM),(FinPartSt SCM) holds

( b_{1} = Euclid-Function iff for p, q being FinPartState of SCM holds

( [p,q] in b_{1} 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 b

( b

( [p,q] in b

( 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) ) )

( 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)

Euclid-Function . (((dl. 0),(dl. 1)) --> (i,j)) = (dl. 0) .--> (i gcd j)

proof end;