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
:: 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
canceled;
theorem
canceled;
theorem
canceled;
theorem Th4:
Lm3:
for P being the Instructions of SCM -valued ManySortedSet of NAT st Euclide-Algorithm c= P holds
S1[P]
begin
theorem Th5:
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) )
theorem Th6:
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) )
theorem Th7:
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) )
theorem Th8:
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) )
theorem Th9:
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 ) ) )
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)) )
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) )
theorem Th10:
definition
func Euclide-Function -> PartFunc of
(FinPartSt SCM ),
(FinPartSt SCM ) means :
Def2:
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) ) )
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
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:
theorem Th12:
theorem