:: Euclid's Algorithm
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received October 8, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, AMI_3, CARD_1, NAT_1, AMI_1, FUNCOP_1,
RELAT_1, GRAPHSP, FUNCT_4, FSM_1, FUNCT_1, XBOOLE_0, TARSKI, ARYTM_3,
INT_1, XXREAL_0, MSUALG_1, INT_2, COMPLEX1, PARTFUN1, TURING_1, STRUCT_0,
AMI_4, EXTPRO_1, FINSET_1, COMPOS_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1,
FUNCT_1, FINSET_1, XCMPLX_0, INT_1, NAT_1, FUNCOP_1, INT_2, FUNCT_4,
STRUCT_0, PARTFUN1, MEMSTR_0, COMPOS_1, EXTPRO_1, AMI_3, XXREAL_0;
constructors NAT_D, AMI_3, RELSET_1, PRE_POLY, DOMAIN_1;
registrations ORDINAL1, RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, STRUCT_0,
AMI_3, XBOOLE_0, FINSET_1, MEMSTR_0, FUNCT_4, FUNCOP_1, RELAT_1,
COMPOS_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions EXTPRO_1, TARSKI, COMPOS_1;
equalities FUNCOP_1, FUNCT_4, MEMSTR_0;
expansions TARSKI, COMPOS_1, MEMSTR_0;
theorems INT_1, ABSVALUE, INT_2, TARSKI, ENUMSET1, NAT_1, FUNCOP_1, PARTFUN1,
FUNCT_4, FUNCT_1, GRFUNC_1, ZFMISC_1, AMI_3, RELAT_1, RELSET_1, XBOOLE_0,
NEWTON, XXREAL_0, ORDINAL1, NAT_D, CARD_1, PBOOLE, EXTPRO_1, MEMSTR_0,
XTUPLE_0;
schemes NAT_1, NAT_D, FUNCT_1, RELSET_1, NEWTON;
begin :: Preliminaries
reserve i,j,k for Nat;
set a = dl.0, b = dl.1, c = dl.2;
Lm1: a <> b & b <> c by AMI_3:10;
Lm2: c <> a by AMI_3:10;
begin :: Euclid's algorithm
definition
func Euclid-Algorithm -> NAT-defined
(the InstructionsF of SCM)-valued finite Function
equals
(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;
end;
defpred P[Instruction-Sequence of SCM] means
$1.0 = c := b & $1.1 = Divide(a,b) &
$1.2 = a := c & $1.3 = b >0_goto 0 &
$1 halts_at 4;
set IN0 = 0 .--> (dl.2 := b);
set IN1 = 1 .--> Divide(a,b);
set IN2 = 2 .--> (a := dl.2);
set IN3 = 3 .--> (b >0_goto 0);
set IN4 = 4 .--> halt SCM;
set EA3 = IN3 +* IN4;
set EA2 = IN2 +* EA3;
set EA1 = IN1 +* EA2;
set EA0 = IN0 +* EA1;
theorem Th1:
dom (Euclid-Algorithm qua Function) = 5
proof
dom IN3 = { 3 } & dom IN4 = { 4 };
then
A1: dom EA3 = { 3 } \/ { 4 } by FUNCT_4:def 1
.= { 3,4 } by ENUMSET1:1;
A2: dom IN1 = { 1 };
dom IN2 = { 2 };
then dom EA2 = { 2 } \/ { 3,4 } by A1,FUNCT_4:def 1
.= { 2,3,4 } by ENUMSET1:2;
then
A3: dom EA1 = { 1 } \/ { 2,3,4 } by A2,FUNCT_4:def 1
.= { 1,2,3,4 } by ENUMSET1:4;
dom IN0 = { 0 };
then dom EA0 = { 0 } \/ { 1,2,3,4 } by A3,FUNCT_4:def 1
.= 5 by CARD_1:53,ENUMSET1:7;
hence thesis;
end;
Lm3:
for P being Instruction-Sequence of SCM
st Euclid-Algorithm c= P
holds P[P]
proof
let P be Instruction-Sequence of SCM;
assume
A1: Euclid-Algorithm c= P;
EA1 c= EA0 by FUNCT_4:25;
then
A2: EA1 c= P by A1;
EA2 c= EA1 by FUNCT_4:25;
then
A3: EA2 c= P by A2;
EA3 c= EA2 by FUNCT_4:25;
then
A4: EA3 c= P by A3;
A5: dom IN4 = { 4 };
A6: not 3 in dom IN4 by TARSKI:def 1;
dom IN3 = { 3 };
then
A7: dom EA3 = { 3 } \/ { 4 } by A5,FUNCT_4:def 1
.= { 3,4 } by ENUMSET1:1;
then
A8: not 2 in dom EA3 by TARSKI:def 2;
dom IN2 = { 2 };
then
A9: dom EA2 = { 2 } \/ { 3,4 } by A7,FUNCT_4:def 1
.= { 2,3,4 } by ENUMSET1:2;
then
A10: not 1 in dom EA2 by ENUMSET1:def 1;
dom IN1 = { 1 };
then
A11: dom EA1 = { 1 } \/ { 2,3,4 } by A9,FUNCT_4:def 1
.= { 1,2,3,4 } by ENUMSET1:4;
then
A12: not 0 in dom EA1;
0 in dom EA0 by Th1,CARD_1:53,ENUMSET1:def 3;
hence P.0 = EA0.0 by A1,GRFUNC_1:2
.= IN0.0 by A12,FUNCT_4:11
.= c := b by FUNCOP_1:72;
1 in dom EA1 by A11,ENUMSET1:def 2;
hence P.1 = EA1.1 by A2,GRFUNC_1:2
.= IN1.1 by A10,FUNCT_4:11
.= Divide(a,b) by FUNCOP_1:72;
2 in dom EA2 by A9,ENUMSET1:def 1;
hence P.2 = EA2.2 by A3,GRFUNC_1:2
.= IN2.2 by A8,FUNCT_4:11
.= a := c by FUNCOP_1:72;
A13: 4 in dom IN4 by TARSKI:def 1;
3 in dom EA3 by A7,TARSKI:def 2;
hence P.3 = EA3.3 by A4,GRFUNC_1:2
.= IN3.3 by A6,FUNCT_4:11
.= b >0_goto 0 by FUNCOP_1:72;
A14: 4 in dom EA3 by A7,TARSKI:def 2;
thus P.4 = EA3.4 by A4,A14,GRFUNC_1:2
.= IN4.4 by A13,FUNCT_4:13
.= halt SCM by FUNCOP_1:72;
end;
begin :: Natural semantics of the program
theorem Th2:
for s being State of SCM
for P being Instruction-Sequence of SCM
st Euclid-Algorithm c= P
for k 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
let s be State of SCM;
let P be Instruction-Sequence of SCM such that
A1: Euclid-Algorithm c= P;
let k;
assume
A2: IC Comput(P,s,k) = 0;
A3: Comput(P,s,k+1)
= Exec(P.(IC Comput(P,s,k)),Comput(P,s,k)) by EXTPRO_1:6
.= Exec(c := b, Comput(P,s,k)) by A1,A2,Lm3;
hence IC Comput(P,s,k+1) = IC Comput(P,s,k) + 1 by AMI_3:2
.= 1 by A2;
thus Comput(P,s,k+1).a = Comput(P,s,k).a & Comput(P,s,k+1).b =
Comput(P,s,k).b by A3,AMI_3:2,10;
thus thesis by A3,AMI_3:2;
end;
theorem Th3:
for s being State of SCM
for P being Instruction-Sequence of SCM
st Euclid-Algorithm c= P
for k 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
let s be State of SCM;
let P be Instruction-Sequence of SCM such that
A1: Euclid-Algorithm c= P;
let k such that
A2: IC Comput(P,s,k) = 1;
A3: Comput(P,s,k+1)
= Exec(P.(IC Comput(P,s,k)),
Comput(P,s,k)) by EXTPRO_1:6
.= Exec(Divide(a,b), Comput(P,s,k)) by A1,A2,Lm3;
hence IC Comput(P,s,k+1) = IC Comput(P,s,k) + 1 by AMI_3:6
.= 2 by A2;
thus thesis by A3,Lm1,Lm2,AMI_3:6;
end;
theorem Th4:
for s being State of SCM
for P being Instruction-Sequence of SCM
st Euclid-Algorithm c= P
for k 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
let s be State of SCM;
let P be Instruction-Sequence of SCM such that
A1: Euclid-Algorithm c= P;
let k;
assume
A2: IC Comput(P,s,k) = 2;
A3: Comput(P,s,k+1)
= Exec(P.(IC Comput(P,s,k)),Comput(P,s,k)) by EXTPRO_1:6
.= Exec(a := c, Comput(P,s,k)) by A1,A2,Lm3;
hence IC Comput(P,s,k+1) = IC Comput(P,s,k) + 1 by AMI_3:2
.= 3 by A2;
thus Comput(P,s,k+1).a = Comput(P,s,k).c by A3,AMI_3:2;
thus thesis by A3,AMI_3:2,10;
end;
theorem Th5:
for s being State of SCM
for P being Instruction-Sequence of SCM
st Euclid-Algorithm c= P
for k 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
let s be State of SCM;
let P be Instruction-Sequence of SCM such that
A1: Euclid-Algorithm c= P;
let k;
assume
A2: IC Comput(P,s,k) = 3;
A3: Comput(P,s,k+1)
= Exec(P.(IC Comput(P,s,k)),Comput(P,s,k)) by EXTPRO_1:6
.= Exec(b >0_goto 0, Comput(P,s,k)) by A1,A2,Lm3;
hence Comput(P,s,k).b > 0 implies IC Comput(P,s,k+1) = 0 by AMI_3:9;
thus Comput(P,s,k).b <= 0 implies IC Comput(P,s,k+1) = 4
proof
assume Comput(P,s,k).b <= 0;
hence IC Comput(P,s,k+1) = IC Comput(P,s,k) + 1 by A3,AMI_3:9
.= 4 by A2;
end;
thus thesis by A3,AMI_3:9;
end;
theorem Th6:
for s being State of SCM
for P being Instruction-Sequence of SCM
st Euclid-Algorithm c= P
for k,i st IC
Comput(P,s,k) = 4 holds Comput(P,s,k+i) = Comput(P,s,k)
proof
let s be State of SCM;
let P be Instruction-Sequence of SCM such that
A1: Euclid-Algorithm c= P;
let k,i;
assume IC Comput(P,s,k) = 4;
then P halts_at IC Comput(P,s,k) by A1,Lm3;
hence thesis by EXTPRO_1:20,NAT_1:11;
end;
Lm4: for s being 0-started State of SCM
for P being Instruction-Sequence of SCM
st Euclid-Algorithm c= P & s.a
> 0 & s.b > 0 holds Comput(P,s,4*k).a > 0 & ( Comput(P,s,4*k).b > 0 & IC
Comput(P,s,4*k) = 0 or Comput(P,s,4*k).b = 0 & IC
Comput(P,s,4*k) = 4)
proof
let s be 0-started State of SCM;
let P be Instruction-Sequence of SCM such that
A1: Euclid-Algorithm c= P and
A2: s.a > 0 & s.b > 0;
A3: IC s = 0 by MEMSTR_0:def 12;
defpred P[Nat] means Comput(P,s,4*$1).a > 0 & (
Comput(P,s,
4*$1).b > 0 & IC Comput(P,s,4*$1) = 0 or Comput(P,s,4*$1).b = 0 & IC
Comput(P,s,4*$1) = 4);
A4: for k st P[k] holds P[k+1]
proof
let k;
set c4 = Comput(P,s,4*k), c5 = Comput(P,s,4*k+1),
c6 = Comput(P,s,4*k+2), c7 = Comput(P,s,4*k+3), c8 = Comput(P,s,4*k+4);
A5: c7 = Comput(P,s,4*k+2+1);
A6: c8 = Comput(P,s,4*k+3+1);
assume
A7: c4.a > 0;
assume
A8: c4.b > 0 & IC c4 = 0 or c4.b = 0 & IC c4 = 4;
A9: c6 = Comput(P,s,4*k+1+1);
now
per cases by A8;
case
A10: c4.b > 0;
then
A11: IC c5 = 1 by A1,A8,Th2;
then
A12: IC c6 = 2 by A1,A9,Th3;
then
A13: IC c7 = 3 by A1,A5,Th4;
then
A14: c8.b = c7.b by A1,A6,Th5;
A15: c7.a = c6.c & c7.b = c6.b by A1,A5,A12,Th4;
A16: c6.b = c5.a mod c5.b & c6.c = c5.c by A1,A9,A11,Th3;
A17: c5.b = c4.b & c5.c = c4.b by A1,A8,A10,Th2;
thus c8.a > 0 by A1,A6,A10,A17,A16,A13,A15,Th5;
c8.b is positive or c8.b is zero by A10,A17,A16,A15,A14;
hence c8.b > 0 & IC c8 = 0 or c8.b = 0 & IC c8 = 4
by A1,A6,A13,A14,Th5;
end;
case
c4.b = 0;
hence c8.a > 0 & c8.b = 0 & IC c8 = 4 by A1,A7,A8,Th6;
end;
end;
hence thesis;
end;
A18: P[ 0] by A3,A2,EXTPRO_1:2;
for k holds P[k] from NAT_1:sch 2(A18,A4);
hence thesis;
end;
Lm5: for s being 0-started State of SCM
for P being Instruction-Sequence of SCM
st Euclid-Algorithm c= P & s.a
> 0 & s.b > 0 holds Comput(P,s,4*k).b > 0 implies Comput(
P,s,4*(k+1)).a =
Comput(P,s,4*k).b & Comput(P,s,4*(k+1)).b = Comput(
P,s,4*k).a mod
Comput(P,s,4*k).b
proof
let s be 0-started State of SCM;
let P be Instruction-Sequence of SCM such that
A1: Euclid-Algorithm c= P and
A2: s.a > 0 & s.b > 0 and
A3: Comput(P,s,4*k).b > 0;
set c4 = Comput(P,s,4*k), c5 = Comput(P,s,4*k+1),
c6 = Comput(P,s,4*k+2), c7 = Comput(P,s,4*k+3);
A4: c4.b > 0 & IC c4 = 0 or c4.b = 0 & IC c4 = 4 by A1,A2,Lm4;
then
A5: c6 = Comput(P,s,4*k+1+1) & IC c5 = 1 by A1,A3,Th2;
then
A6: c6.c = c5.c by A1,Th3;
A7: c7 = Comput(P,s,4*k+2+1) & IC c6 = 2 by A1,A5,Th3;
then
A8: Comput(P,s,4*k+4) = Comput(P,s,4*k+3+1) & IC c7 =
3 by A1,Th4;
A9: c7.a = c6.c by A1,A7,Th4;
c5.c = c4.b by A1,A3,A4,Th2;
hence Comput(P,s,4*(k+1)).a = Comput(P,s,4*k).b by A1,A6,A8,A9,Th5;
A10: c7.b = c6.b by A1,A7,Th4;
A11: c6.b = c5.a mod c5.b by A1,A5,Th3;
c5.a = c4.a & c5.b = c4.b by A1,A3,A4,Th2;
hence thesis by A1,A11,A8,A10,Th5;
end;
Lm6: for s being 0-started State of SCM
for P being Instruction-Sequence of SCM
st Euclid-Algorithm c= P
for x,
y being Integer st s.a = x & s.b = y & x > y & y > 0 holds
(Result(P,s)).a = x gcd y & ex k st P halts_at IC Comput(P,s,k)
proof
let s be 0-started State of SCM;
let P be Instruction-Sequence of SCM such that
A1: Euclid-Algorithm c= P;
deffunc G(Nat) = |. Comput(P,s,4*$1).b.|;
deffunc F(Nat) = |. Comput(P,s,4*$1).a.|;
let x, y be Integer such that
A2: s.a = x and
A3: s.b = y and
A4: x > y and
A5: y > 0;
A6: now
let k be Nat;
A7: Comput(P,s,4*k).b > 0 or Comput(P,s,4*k).b = 0
by A1,A2,A3,A4,A5,Lm4;
assume
A8: G(k) > 0;
hence F(k+1) = G(k) by A1,A2,A3,A4,A5,A7,Lm5,ABSVALUE:2;
A9: Comput(P,s,4*k).a >= 0 by A1,A2,A3,A4,A5,Lm4;
Comput(P,s,4*(k+1)).b >= 0 by A1,A2,A3,A4,A5,Lm4;
hence G(k+1) = Comput(P,s,4*(k+1)).b by ABSVALUE:def 1
.= Comput(P,s,4*k).a mod Comput(P,s,4*k).b by A1,A2,A3,A4,A5,A7,A8,Lm5,
ABSVALUE:2
.= F(k) mod G(k) by A7,A9,INT_2:32;
end;
reconsider x9 = x, y9 = y as Element of NAT by A4,A5,INT_1:3;
A10: y9 < x9 by A4;
A11: F(0) = |.x.| by A2,EXTPRO_1:2
.= x9 by ABSVALUE:def 1;
A12: G(0) = |.y.| by A3,EXTPRO_1:2
.= y9 by ABSVALUE:def 1;
A13: 0 < y9 by A5;
consider k being Nat such that
A14: F(k) = x9 gcd y9 and
A15: G(k) = 0 from NEWTON:sch 1(A13,A10,A11,A12,A6);
A16: ( Comput(P,s,4*k)).a > 0 by A1,A2,A3,A4,A5,Lm4;
Comput(P,s,4*k).b = 0 by A15,ABSVALUE:2;
then
A17: IC Comput(P,s,4*k) = 4 by A1,A2,A3,A4,A5,Lm4;
A18: P halts_at 4 by A1,Lm3;
hence (Result(P,s)).a = ( Comput(P,s,4*k)).a by A17,EXTPRO_1:18
.= x gcd y by A14,A16,ABSVALUE:def 1;
thus thesis by A17,A18;
end;
theorem Th7:
for s being 0-started State of SCM
for P being Instruction-Sequence of SCM
st Euclid-Algorithm c= P
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
let s be 0-started State of SCM;
let P be Instruction-Sequence of SCM such that
A1: Euclid-Algorithm c= P;
let x, y be Integer such that
A2: s.a = x & s.b = y and
A3: x > 0 and
A4: y > 0;
A5: |.y.| = y by A4,ABSVALUE:def 1;
now
per cases by XXREAL_0:1;
case
x > y;
hence thesis by A1,A2,A4,Lm6;
end;
case
A6: x = y;
reconsider x9 = x, y9 = y as Element of NAT by A3,A4,INT_1:3;
take s9 = Comput(P,s,4);
A7: s = Comput(P,s,4*0) by EXTPRO_1:2;
A8: s9 = Comput(P,s,4*(0+1));
x mod y = x9 mod y9
.= 0 by A6,NAT_D:25;
then s9.b = 0 by A1,A2,A3,A4,A7,A8,Lm5;
then IC s9 = 4 by A1,A2,A3,A4,A8,Lm4;
then P halts_at IC s9 by A1,Lm3;
hence (Result(P,s)).a = s9.a by EXTPRO_1:18
.= y by A1,A2,A3,A4,A7,A8,Lm5
.= x gcd y by A5,A6,NAT_D:32;
end;
case
A9: y > x;
reconsider x9 = x, y9 = y as Element of NAT by A3,A4,INT_1:3;
take s9 = Comput(P,s,4);
A10: s9 = Comput(P,s,4*(0+1));
A11: s = Comput(P,s,4*0) by EXTPRO_1:2;
then
A12: s9.a = y by A1,A2,A3,A4,A10,Lm5;
x mod y = x9 mod y9
.= x9 by A9,NAT_D:24;
then
A13: s9.b = x by A1,A2,A3,A4,A11,A10,Lm5;
then IC s9 = 0 by A1,A2,A3,A4,A10,Lm4;
then
A14: s9 is 0-started;
then consider k0 being Nat such that
A15: P halts_at IC Comput(P,s9,k0)
by A3,A9,A12,A13,A1,Lm6;
A16: P halts_at IC Comput(P,s,k0+4) by A15,EXTPRO_1:4;
(Result(P,s9)).a = x gcd y by A3,A9,A12,A13,A14,A1,Lm6;
hence thesis by A16,EXTPRO_1:21;
end;
end;
hence thesis;
end;
definition
func Euclid-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
proof
defpred P[object,object] means
ex x,y being Integer st x > 0 & y > 0 &
$1 = (a,b ) --> (x,y) & $2 = a .--> (x gcd y);
A1: for p,q1,q2 being object st P[p,q1] & P[p,q2] holds q1=q2
proof
let p,q1,q2 be object;
given x1,y1 being Integer such that
x1 > 0 and
y1 > 0 and
A2: p = (a,b) --> (x1,y1) and
A3: q1 = a .--> (x1 gcd y1);
given x2,y2 being Integer such that
x2 > 0 and
y2 > 0 and
A4: p = (a,b) --> (x2,y2) and
A5: q2 = a .--> (x2 gcd y2);
A6: y1 = ((a,b) --> (x1,y1)).b by FUNCT_4:63
.= y2 by A2,A4,FUNCT_4:63;
x1 = ((a,b) --> (x1,y1)).a by AMI_3:10,FUNCT_4:63
.= x2 by A2,A4,AMI_3:10,FUNCT_4:63;
hence thesis by A3,A5,A6;
end;
consider f being Function such that
A7: for p,q being object holds [p,q] in f iff p in FinPartSt SCM & P[p,q]
from FUNCT_1:sch 1(A1);
A8: rng f c= FinPartSt SCM
proof
let q be object;
assume q in rng f;
then consider p being object such that
A9: [p,q] in f by XTUPLE_0:def 13;
ex x,y being Integer st x > 0 & y > 0 &p = (a,b) --> (x,y) & q = a
.--> (x gcd y) by A7,A9;
hence thesis by MEMSTR_0:75;
end;
dom f c= FinPartSt SCM
proof
let e be object;
assume e in dom f;
then [e,f.e] in f by FUNCT_1:1;
hence thesis by A7;
end;
then reconsider f as PartFunc of FinPartSt SCM, FinPartSt SCM by A8,
RELSET_1:4;
take f;
let p,q be FinPartState of SCM;
thus [p,q] in f implies ex x,y being Integer st x > 0 & y > 0 & p = (a,b)
--> (x,y) & q = a .--> (x gcd y) by A7;
given x,y being Integer such that
A10: x > 0 & y > 0 & p = (a,b) --> (x,y) & q = a .--> (x gcd y);
p in FinPartSt SCM by MEMSTR_0:75;
hence thesis by A7,A10;
end;
uniqueness
proof
defpred P[set,set] means ex x,y being Integer st x > 0 & y > 0 & $1 = (a,b
) --> (x,y) & $2 = a .--> (x gcd y);
let IT1,IT2 be PartFunc of FinPartSt SCM, FinPartSt SCM such that
A11: for p,q being FinPartState of SCM holds [p,q] in IT1 iff P[p,q] and
A12: for p,q being FinPartState of SCM holds [p,q] in IT2 iff P[p,q];
A13: for p,q being Element of FinPartSt SCM holds [p,q] in IT2 iff P[p,q]
proof
let p,q being Element of FinPartSt SCM;
thus [p,q] in IT2 implies P[p,q]
proof
assume
A14: [p,q] in IT2;
reconsider p,q as FinPartState of SCM by MEMSTR_0:76;
P[p,q] by A12,A14;
hence thesis;
end;
thus thesis by A12;
end;
A15: for p,q being Element of FinPartSt SCM holds [p,q] in IT1 iff P[p,q]
proof
let p,q being Element of FinPartSt SCM;
thus [p,q] in IT1 implies P[p,q]
proof
assume
A16: [p,q] in IT1;
reconsider p,q as FinPartState of SCM by MEMSTR_0:76;
P[p,q] by A11,A16;
hence thesis;
end;
thus thesis by A11;
end;
thus IT1 = IT2 from RELSET_1:sch 4(A15,A13);
end;
end;
theorem Th8:
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)
proof
let p be set;
A1: dom Euclid-Function c= FinPartSt SCM by RELAT_1:def 18;
A2: p in dom Euclid-Function iff [p,Euclid-Function.p] in Euclid-Function
by FUNCT_1:1;
hereby
assume
A3: p in dom Euclid-Function;
then Euclid-Function.p in FinPartSt SCM by PARTFUN1:4;
then
A4: Euclid-Function.p is FinPartState of SCM by MEMSTR_0:76;
p is FinPartState of SCM by A1,A3,MEMSTR_0:76;
then ex x,y being Integer st x > 0 & y > 0 & p = (a,b) --> (x,y) &
Euclid-Function.p = a .--> (x gcd y) by A2,A3,A4,Def2;
hence ex x,y being Integer st x > 0 & y > 0 & p = (a,b) --> (x,y);
end;
given x,y being Integer such that
A5: x > 0 & y > 0 & p = (a,b) --> (x,y);
[p,a .--> (x gcd y)] in Euclid-Function by A5,Def2;
hence thesis by FUNCT_1:1;
end;
theorem Th9:
for i,j being Integer st i > 0 & j > 0 holds Euclid-Function.((
dl.0,dl.1) --> (i,j)) = dl.0 .--> (i gcd j)
proof
let i,j be Integer;
assume i > 0 & j > 0;
then [((a,b) --> (i,j)),a .--> (i gcd j)] in Euclid-Function by Def2;
hence thesis by FUNCT_1:1;
end;
registration
cluster Euclid-Algorithm -> (the InstructionsF of SCM)-valued;
coherence;
end;
registration
cluster Euclid-Algorithm -> non halt-free;
coherence
proof
rng(4 .--> halt SCM) = {halt SCM} by FUNCOP_1:8;
then
A1: halt SCM in rng(4 .--> halt SCM) by TARSKI:def 1;
rng(4 .--> halt SCM) c= rng(((3 .--> (dl.1 >0_goto 0)) +*
(4 .--> halt SCM))) by FUNCT_4:18;
then
A2: halt SCM in rng(((3 .--> (dl.1 >0_goto 0)) +* (4 .--> halt SCM))) by A1;
rng((3 .--> (dl.1 >0_goto 0)) +* (4 .--> halt SCM)) c=
rng(((2 .--> (dl.0 := dl.2)) +* ((3 .--> (dl.1 >0_goto 0)) +*
(4 .--> halt SCM)))) by FUNCT_4:18;
then
A3: halt SCM in rng((2 .--> (dl.0 := dl.2)) +* ((3 .--> (dl.1 >0_goto 0)) +*
(4 .--> halt SCM))) by A2;
rng((2 .--> (dl.0 := dl.2)) +* ((3 .--> (dl.1 >0_goto 0)) +*
(4 .--> halt SCM))) c=
rng((1 .--> Divide(dl.0,dl.1)) +*
((2 .--> (dl.0 := dl.2)) +* ((3 .--> (dl.1 >0_goto 0)) +*
(4 .--> halt SCM)))) by FUNCT_4:18;
then
A4: halt SCM in rng((1 .--> Divide(dl.0,dl.1)) +*
((2 .--> (dl.0 := dl.2)) +* ((3 .--> (dl.1 >0_goto 0)) +*
(4 .--> halt SCM)))) by A3;
rng((1 .--> Divide(dl.0,dl.1)) +*
((2 .--> (dl.0 := dl.2)) +* ((3 .--> (dl.1 >0_goto 0)) +*
(4 .--> halt SCM)))) c= rng Euclid-Algorithm by FUNCT_4:18;
then halt SCM in rng Euclid-Algorithm by A4;
hence thesis;
end;
end;
theorem
Euclid-Algorithm, Start-At(0,SCM) computes Euclid-Function
proof
set q = Euclid-Algorithm;
set p = Start-At(0,SCM);
let x be set;
DataPart p = {} by MEMSTR_0:20;
then
A1: dom DataPart p = {};
assume x in dom Euclid-Function;
then consider i1,i2 being Integer such that
A2: i1 > 0 and
A3: i2 > 0 and
A4: x = (a,b) --> (i1,i2) by Th8;
x = (a .--> i1) +* (b .--> i2) by A4;
then reconsider d = x as FinPartState of SCM;
consider t being State of SCM such that
A5: p +* d c= t by PBOOLE:141;
consider T being Instruction-Sequence of SCM
such that
A6: q c= T by PBOOLE:145;
A7: dom d = { a, b } by A4,FUNCT_4:62;
then
A8: b in dom d by TARSKI:def 2;
A9: a in dom d by A7,TARSKI:def 2;
A10: for t being State of SCM st p +* d c= t
holds t.a = i1 & t.b = i2
proof
let t be State of SCM;
assume
A11: p +* d c= t;
d c= p +* d by FUNCT_4:25;
then
A12: d c= t by A11;
hence t.a = d.a by A9,GRFUNC_1:2
.= i1 by A4,AMI_3:10,FUNCT_4:63;
thus t.b = d.b by A8,A12,GRFUNC_1:2
.= i2 by A4,FUNCT_4:63;
end;
A14: now
assume dom p meets dom d;
then consider x being object such that
A15: x in dom p and
A16: x in dom d by XBOOLE_0:3;
A17: x = IC SCM by A15,TARSKI:def 1;
x = a or x = b by A7,A16,TARSKI:def 2;
hence contradiction by A17,AMI_3:13;
end;
then
A18: p c= p +* d by FUNCT_4:32;
A19: IC SCM in dom p by TARSKI:def 1;
dom p /\ dom d = {} by A14,XBOOLE_0:def 7;
then
A20: not IC SCM in dom d by A19,XBOOLE_0:def 4;
set A = { IC SCM, a,b }, C = 5;
A21: dom (p +* d) = dom( p +* d)
.= dom p \/ dom d by FUNCT_4:def 1
.= {IC SCM} \/ dom DataPart p \/ dom d by A19,MEMSTR_0:24
.= { IC SCM } \/ { a, b } by A4,A1,FUNCT_4:62
.= A by ENUMSET1:2;
A22: dom p c= dom(p +* d) by A18,RELAT_1:11;
IC(p +* d) = IC p by A20,FUNCT_4:11
.= 0 by FUNCOP_1:72;
then
A23: p +* d is 0-started by A22,A19;
then
A24: t is 0-started by A5,MEMSTR_0:17;
A25: p +* d is q-autonomic
proof
set A = { IC SCM, a,b }, C = 5;
let P,Q being Instruction-Sequence of SCM
such that
A26: q c= P and
A27: q c= Q;
let s1,s2 be State of SCM such that
A28: (p +* d) c= s1 and
A29: (p +* d) c= s2;
A30: s2.a = i1 & s2.b = i2 by A10,A29;
let k;
defpred P[Nat] means
IC Comput(P,s1,$1) = IC Comput(Q,s2,$1) &
Comput(P,s1,$1).a = Comput(Q,s2,$1).a &
Comput(P,s1,$1).b = Comput(Q,s2,$1).b;
A31: Comput(P,s1,0) = s1 & Comput(Q,s2,0) = s2 by EXTPRO_1:2;
A32: s1 is 0-started by A23,A28,MEMSTR_0:17;
A33: dom( Comput(P,s1,k)) = the carrier of SCM by PARTFUN1:def 2
.= dom( Comput(Q,s2,k)) by PARTFUN1:def 2;
A34: s2 is 0-started by A23,A29,MEMSTR_0:17;
A35: for i,j being Nat st P[4*i] & j<>0 & j<=4 holds P[4*i+j]
proof
let i,j be Nat;
assume that
A36: IC Comput(P,s1,4*i) = IC Comput(Q,s2,4*i) and
A37: Comput(P,s1,4*i).a = Comput(Q,s2,4*i).a and
A38: Comput(P,s1,4*i).b = Comput(Q,s2,4*i).b;
assume
A39: j <> 0 & j <= 4;
then j = 0 or ... or j = 4;
then
A40: j = 1 or ... or j = 4 by A39;
per cases by A2,A3,A34,A27,A30,Lm4;
suppose
A41: IC Comput(Q,s2,4*i) = 0;
A42: ( Comput(P,s1,4*i+1)).a = Comput(P,s1,4*i).a by A26,A36,A41,Th2
.= ( Comput(Q,s2,4*i+1)).a by A27,A37,A41,Th2;
A43: ( Comput(P,s1,4*i+1)).dl.2 = Comput(P,s1,4*i).b by A26,A36,A41,Th2
.= ( Comput(Q,s2,4*i+1)).dl.2 by A27,A38,A41,Th2;
A44: ( Comput(P,s1,4*i+1)).b = Comput(P,s1,4*i).b by A26,A36,A41,Th2
.= ( Comput(Q,s2,4*i+1)).b by A27,A38,A41,Th2;
A45: 4*i + 1 + 1 = 4*i + (1 + 1);
A46: (4*i+2)+1 = 4*i+(2+1);
A47: IC Comput(Q,s2,4*i+1) = 1 by A27,A41,Th2;
then
A48: IC Comput(Q,s2,4*i+2) = 2 by A27,A45,Th3;
then
A49: IC Comput(Q,s2,4*i+3) = 3 by A27,A46,Th4;
A50: IC Comput(P,s1,4*i+1) = 1 by A26,A36,A41,Th2;
then
A51: ( Comput(P,s1,4*i+2)).dl.2 = ( Comput(P,s1,4*i+1)).dl.2 by A26,A45,Th3
.= ( Comput(Q,s2,4*i+2)).dl.2 by A27,A45,A47,A43,Th3;
A52: ( Comput(P,s1,4*i+2)).b = ( Comput(P,s1,4*i
+1)).a mod (
Comput(P,s1,4*i+1)).b by A26,A45,A50,Th3
.= ( Comput(Q,s2,4*i+2)).b by A27,A45,A47,A42,A44,Th3;
A53: IC Comput(P,s1,4*i+2) = 2 by A26,A45,A50,Th3;
then
A54: IC Comput(P,s1,4*i+3) = 3 by A26,A46,Th4;
A55: ( Comput(P,s1,4*i+2)).a = ( Comput(P,s1,4*i+1)).a div (
Comput(P,s1,4*i+1)).b by A26,A45,A50,Th3
.= ( Comput(Q,s2,4*i+2)).a by A27,A45,A47,A42,A44,Th3;
A56: 4*i + 3 + 1 = 4*i + (3 + 1);
A57: ( Comput(P,s1,4*i+3)).a = ( Comput(P,s1,4*i+2)).dl.2 by A26,A46,A53,Th4
.= ( Comput(Q,s2,4*i+3)).a by A27,A46,A48,A51,Th4;
A58: ( Comput(P,s1,4*i+3)).b = ( Comput(P,s1,4*i+2)).b by A26,A46,A53,Th4
.= ( Comput(Q,s2,4*i+3)).b by A27,A46,A48,A52,Th4;
( Comput(P,s1,4*i+3)).b <= 0 or ( Comput(P,s1,4*i+3)).b > 0;
then
IC Comput(P,s1,4*i+4) = 4 & IC Comput(Q,s2,4*i+4) = 4 or
IC Comput(P,s1,4*i+4) = 0 & IC Comput(Q,s2,4*i+4) = 0
by A26,A27,A56,A54,A49,A58,Th5;
hence IC Comput(P,s1,4*i+j) = IC Comput(Q,s2,4*i+j)
by A40,A50,A27,A41,Th2,A26,A45,Th3,A48,A54,A46,Th4;
( Comput(P,s1,4*i+4)).a = ( Comput(P,s1,4*i+3)).a by A26,A56,A54,Th5
.= ( Comput(Q,s2,4*i+4)).a by A27,A56,A49,A57,Th5;
hence
Comput(P,s1,4*i+j).a = Comput(Q,s2,4*i+j).a by A40,A42,A55,A57;
( Comput(P,s1,4*i+4)).b = ( Comput(P,s1,4*i+3)).b by A26,A56,A54,Th5
.= ( Comput(Q,s2,4*i+4)).b by A27,A56,A49,A58,Th5;
hence thesis by A40,A44,A52,A58;
end;
suppose
A59: IC Comput(Q,s2,4*i) = 4;
then P halts_at IC Comput(P,s1,4*i)
by A26,A36,Lm3;
then
A60: Comput(P,s1,4*i+j) = Comput(P,s1,4*i) by EXTPRO_1:20,NAT_1:11;
Q halts_at IC Comput(Q,s2,4*i) by A27,A59,Lm3;
hence thesis by A36,A37,A38,A60,EXTPRO_1:20,NAT_1:11;
end;
end;
reconsider k as Element of NAT by ORDINAL1:def 12;
( Comput(P,s1,0)).IC SCM = IC s1 by EXTPRO_1:2
.= 0 by A32
.= IC s2 by A34
.= ( Comput(Q,s2,0)).IC SCM by EXTPRO_1:2;
then
A61: P[ 0] by A10,A28,A30,A31;
A62: 4 > 0;
P[k] from NAT_D:sch 2(A61,A62,A35);
hence thesis by A21,A33,GRFUNC_1:31;
end;
take d;
thus x = d;
A63: p +* d is q-halted
proof
reconsider i19 = i1, i29 = i2 as Element of NAT by A2,A3,INT_1:3;
let t be State of SCM;
assume
A64: p +* d c= t;
let P be Instruction-Sequence of SCM such that
A65: q c= P;
set t9 = Comput(P,t,4);
A66: t.b = i2 by A10,A64;
A67: t is 0-started & t.a = i1 by A23,A10,A64,MEMSTR_0:17;
per cases by XXREAL_0:1;
suppose
i1 > i2;
then ex k st P halts_at IC Comput(P,t,k)
by A3,A65,A67,A66,Lm6;
hence thesis by EXTPRO_1:16;
end;
suppose
A68: i1 = i2;
A69: i1 mod i2 = i19 mod i29
.= 0 by A68,NAT_D:25;
A70: t9 = Comput(P,t,4*(0+1));
t = Comput(P,t,4*0) by EXTPRO_1:2;
then t9.b = t.a mod t.b by A2,A3,A65,A67,A66,A70,Lm5;
then IC t9 = 4 by A2,A3,A65,A67,A66,A69,A70,Lm4;
then P halts_at IC t9 by A65,Lm3;
hence thesis by EXTPRO_1:16;
end;
suppose
A71: i1 < i2;
A72: t9 = Comput(P,t,4*(0+1));
A73: t = Comput(P,t,4*0) by EXTPRO_1:2;
i1 mod i2 = i19 mod i29
.= i19 by A71,NAT_D:24;
then
A74: t9.b = i1 by A2,A3,A65,A67,A66,A73,A72,Lm5;
then IC t9 = 0 by A2,A3,A65,A67,A66,A72,Lm4;
then
A75: t9 is 0-started;
t9.a = i2 by A2,A3,A65,A67,A66,A73,A72,Lm5;
then consider k0 being Nat such that
A76: P halts_at IC Comput(P,t9,k0) by A2,A71,A74,A75,A65,Lm6;
P halts_at IC Comput(P,t,k0+4) by A76,EXTPRO_1:4;
hence thesis by EXTPRO_1:16;
end;
end;
thus
p +* d is Autonomy of q by A25,A63,EXTPRO_1:def 12;
then
A77: Result(q,p+*d) = Result(T,t)|dom (p+*d)
by A6,A5,EXTPRO_1:def 13;
a in the carrier of SCM;
then
A78: a in dom Result(T,t) by PARTFUN1:def 2;
A79: d.a = i1 by A4,AMI_3:10,FUNCT_4:63;
A80: d.b = i2 by A4,FUNCT_4:63;
A81: d c= p +* d by FUNCT_4:25;
A82: dom d c= dom(p +* d) by A81,RELAT_1:11;
A83: d c= t by A81,A5;
A84: dom d = { a, b } by A4,FUNCT_4:62;
then
A85: b in dom d by TARSKI:def 2;
A86: t.b = i2 by A83,A80,A85,GRFUNC_1:2;
A87: a in dom d by A84,TARSKI:def 2;
t.a = i1 by A83,A79,A87,GRFUNC_1:2;
then
A88: (Result(T,t)).a = i1 gcd i2
by A2,A3,A24,A86,Th7,A6;
dom(a .--> (i1 gcd i2)) c= dom d by A84,ZFMISC_1:7;
then
A90: dom(a .--> (i1 gcd i2)) c= dom(p +* d) by A82;
a .--> (i1 gcd i2) c= (Result(T,t))|dom(p +* d)
by A90,A78,A88,FUNCT_4:85,RELAT_1:151;
hence Euclid-Function.d c= Result(q,p+* d) by A77,A2,A3,A4,Th9;
end;