:: Euclid's Algorithm :: by Andrzej Trybulec and Yatsuka Nakamura :: :: Received October 8, 1993 :: Copyright (c) 1993-2018 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 } by FUNCOP_1:13; then A1: dom EA3 = { 3 } \/ { 4 } by FUNCT_4:def 1 .= { 3,4 } by ENUMSET1:1; A2: dom IN1 = { 1 } by FUNCOP_1:13; dom IN2 = { 2 } by FUNCOP_1:13; 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 } by FUNCOP_1:13; 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 } by FUNCOP_1:13; then A6: not 3 in dom IN4 by TARSKI:def 1; dom IN3 = { 3 } by FUNCOP_1:13; 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 } by FUNCOP_1:13; 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 } by FUNCOP_1:13; 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 A5,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,NEWTON:64; 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; A13: dom p = { IC SCM } by FUNCOP_1:13; 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 A13,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 A13,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; A89: dom(a .--> (i1 gcd i2)) = { a } by FUNCOP_1:13; dom(a .--> (i1 gcd i2)) c= dom d by A84,A89,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;