set q = Euclid-Algorithm ;

set p = Start-At (0,SCM);

let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( not x in dom Euclid-Function or ex b_{1} being set st

( x = b_{1} & (Start-At (0,SCM)) +* b_{1} is Autonomy of Euclid-Algorithm & Euclid-Function . b_{1} c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* b_{1})) ) )

DataPart (Start-At (0,SCM)) = {} by MEMSTR_0:20;

then A1: dom (DataPart (Start-At (0,SCM))) = {} ;

assume x in dom Euclid-Function ; :: thesis: ex b_{1} being set st

( x = b_{1} & (Start-At (0,SCM)) +* b_{1} is Autonomy of Euclid-Algorithm & Euclid-Function . b_{1} c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* b_{1})) )

then consider i1, i2 being Integer such that

A2: i1 > 0 and

A3: i2 > 0 and

A4: x = ((dl. 0),(dl. 1)) --> (i1,i2) by Th8;

x = ((dl. 0) .--> i1) +* ((dl. 1) .--> i2) by A4;

then reconsider d = x as FinPartState of SCM ;

consider t being State of SCM such that

A5: (Start-At (0,SCM)) +* d c= t by PBOOLE:141;

consider T being Instruction-Sequence of SCM such that

A6: Euclid-Algorithm c= T by PBOOLE:145;

A7: dom d = {(dl. 0),(dl. 1)} by A4, FUNCT_4:62;

then A8: dl. 1 in dom d by TARSKI:def 2;

A9: dl. 0 in dom d by A7, TARSKI:def 2;

A10: for t being State of SCM st (Start-At (0,SCM)) +* d c= t holds

( t . (dl. 0) = i1 & t . (dl. 1) = i2 )

A19: IC in dom (Start-At (0,SCM)) by TARSKI:def 1;

(dom (Start-At (0,SCM))) /\ (dom d) = {} by A14, XBOOLE_0:def 7;

then A20: not IC in dom d by A19, XBOOLE_0:def 4;

set A = {(IC ),(dl. 0),(dl. 1)};

set C = 5;

A21: dom ((Start-At (0,SCM)) +* d) = dom ((Start-At (0,SCM)) +* d)

.= (dom (Start-At (0,SCM))) \/ (dom d) by FUNCT_4:def 1

.= ({(IC )} \/ (dom (DataPart (Start-At (0,SCM))))) \/ (dom d) by A19, MEMSTR_0:24

.= {(IC )} \/ {(dl. 0),(dl. 1)} by A4, A1, FUNCT_4:62

.= {(IC ),(dl. 0),(dl. 1)} by ENUMSET1:2 ;

A22: dom (Start-At (0,SCM)) c= dom ((Start-At (0,SCM)) +* d) by A18, RELAT_1:11;

IC ((Start-At (0,SCM)) +* d) = IC (Start-At (0,SCM)) by A20, FUNCT_4:11

.= 0 by FUNCOP_1:72 ;

then A23: (Start-At (0,SCM)) +* d is 0 -started by A22, A19;

then A24: t is 0 -started by A5, MEMSTR_0:17;

A25: (Start-At (0,SCM)) +* d is Euclid-Algorithm -autonomic

thus x = d ; :: thesis: ( (Start-At (0,SCM)) +* d is Autonomy of Euclid-Algorithm & Euclid-Function . d c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d)) )

A63: (Start-At (0,SCM)) +* d is Euclid-Algorithm -halted

then A77: Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d)) = (Result (T,t)) | (dom ((Start-At (0,SCM)) +* d)) by A6, A5, EXTPRO_1:def 13;

dl. 0 in the carrier of SCM ;

then A78: dl. 0 in dom (Result (T,t)) by PARTFUN1:def 2;

A79: d . (dl. 0) = i1 by A4, AMI_3:10, FUNCT_4:63;

A80: d . (dl. 1) = i2 by A4, FUNCT_4:63;

A81: d c= (Start-At (0,SCM)) +* d by FUNCT_4:25;

A82: dom d c= dom ((Start-At (0,SCM)) +* d) by A81, RELAT_1:11;

A83: d c= t by A81, A5;

A84: dom d = {(dl. 0),(dl. 1)} by A4, FUNCT_4:62;

then A85: dl. 1 in dom d by TARSKI:def 2;

A86: t . (dl. 1) = i2 by A83, A80, A85, GRFUNC_1:2;

A87: dl. 0 in dom d by A84, TARSKI:def 2;

t . (dl. 0) = i1 by A83, A79, A87, GRFUNC_1:2;

then A88: (Result (T,t)) . (dl. 0) = i1 gcd i2 by A2, A3, A24, A86, Th7, A6;

dom ((dl. 0) .--> (i1 gcd i2)) c= dom d by A84, ZFMISC_1:7;

then A90: dom ((dl. 0) .--> (i1 gcd i2)) c= dom ((Start-At (0,SCM)) +* d) by A82;

(dl. 0) .--> (i1 gcd i2) c= (Result (T,t)) | (dom ((Start-At (0,SCM)) +* d)) by A90, A78, A88, FUNCT_4:85, RELAT_1:151;

hence Euclid-Function . d c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d)) by A77, A2, A3, A4, Th9; :: thesis: verum

set p = Start-At (0,SCM);

let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( not x in dom Euclid-Function or ex b

( x = b

DataPart (Start-At (0,SCM)) = {} by MEMSTR_0:20;

then A1: dom (DataPart (Start-At (0,SCM))) = {} ;

assume x in dom Euclid-Function ; :: thesis: ex b

( x = b

then consider i1, i2 being Integer such that

A2: i1 > 0 and

A3: i2 > 0 and

A4: x = ((dl. 0),(dl. 1)) --> (i1,i2) by Th8;

x = ((dl. 0) .--> i1) +* ((dl. 1) .--> i2) by A4;

then reconsider d = x as FinPartState of SCM ;

consider t being State of SCM such that

A5: (Start-At (0,SCM)) +* d c= t by PBOOLE:141;

consider T being Instruction-Sequence of SCM such that

A6: Euclid-Algorithm c= T by PBOOLE:145;

A7: dom d = {(dl. 0),(dl. 1)} by A4, FUNCT_4:62;

then A8: dl. 1 in dom d by TARSKI:def 2;

A9: dl. 0 in dom d by A7, TARSKI:def 2;

A10: for t being State of SCM st (Start-At (0,SCM)) +* d c= t holds

( t . (dl. 0) = i1 & t . (dl. 1) = i2 )

proof

let t be State of SCM; :: thesis: ( (Start-At (0,SCM)) +* d c= t implies ( t . (dl. 0) = i1 & t . (dl. 1) = i2 ) )

assume A11: (Start-At (0,SCM)) +* d c= t ; :: thesis: ( t . (dl. 0) = i1 & t . (dl. 1) = i2 )

d c= (Start-At (0,SCM)) +* d by FUNCT_4:25;

then A12: d c= t by A11;

hence t . (dl. 0) = d . (dl. 0) by A9, GRFUNC_1:2

.= i1 by A4, AMI_3:10, FUNCT_4:63 ;

:: thesis: t . (dl. 1) = i2

thus t . (dl. 1) = d . (dl. 1) by A8, A12, GRFUNC_1:2

.= i2 by A4, FUNCT_4:63 ; :: thesis: verum

end;assume A11: (Start-At (0,SCM)) +* d c= t ; :: thesis: ( t . (dl. 0) = i1 & t . (dl. 1) = i2 )

d c= (Start-At (0,SCM)) +* d by FUNCT_4:25;

then A12: d c= t by A11;

hence t . (dl. 0) = d . (dl. 0) by A9, GRFUNC_1:2

.= i1 by A4, AMI_3:10, FUNCT_4:63 ;

:: thesis: t . (dl. 1) = i2

thus t . (dl. 1) = d . (dl. 1) by A8, A12, GRFUNC_1:2

.= i2 by A4, FUNCT_4:63 ; :: thesis: verum

A14: now :: thesis: not dom (Start-At (0,SCM)) meets dom d

then A18:
Start-At (0,SCM) c= (Start-At (0,SCM)) +* d
by FUNCT_4:32;assume
dom (Start-At (0,SCM)) meets dom d
; :: thesis: contradiction

then consider x being object such that

A15: x in dom (Start-At (0,SCM)) and

A16: x in dom d by XBOOLE_0:3;

A17: x = IC by A15, TARSKI:def 1;

( x = dl. 0 or x = dl. 1 ) by A7, A16, TARSKI:def 2;

hence contradiction by A17, AMI_3:13; :: thesis: verum

end;then consider x being object such that

A15: x in dom (Start-At (0,SCM)) and

A16: x in dom d by XBOOLE_0:3;

A17: x = IC by A15, TARSKI:def 1;

( x = dl. 0 or x = dl. 1 ) by A7, A16, TARSKI:def 2;

hence contradiction by A17, AMI_3:13; :: thesis: verum

A19: IC in dom (Start-At (0,SCM)) by TARSKI:def 1;

(dom (Start-At (0,SCM))) /\ (dom d) = {} by A14, XBOOLE_0:def 7;

then A20: not IC in dom d by A19, XBOOLE_0:def 4;

set A = {(IC ),(dl. 0),(dl. 1)};

set C = 5;

A21: dom ((Start-At (0,SCM)) +* d) = dom ((Start-At (0,SCM)) +* d)

.= (dom (Start-At (0,SCM))) \/ (dom d) by FUNCT_4:def 1

.= ({(IC )} \/ (dom (DataPart (Start-At (0,SCM))))) \/ (dom d) by A19, MEMSTR_0:24

.= {(IC )} \/ {(dl. 0),(dl. 1)} by A4, A1, FUNCT_4:62

.= {(IC ),(dl. 0),(dl. 1)} by ENUMSET1:2 ;

A22: dom (Start-At (0,SCM)) c= dom ((Start-At (0,SCM)) +* d) by A18, RELAT_1:11;

IC ((Start-At (0,SCM)) +* d) = IC (Start-At (0,SCM)) by A20, FUNCT_4:11

.= 0 by FUNCOP_1:72 ;

then A23: (Start-At (0,SCM)) +* d is 0 -started by A22, A19;

then A24: t is 0 -started by A5, MEMSTR_0:17;

A25: (Start-At (0,SCM)) +* d is Euclid-Algorithm -autonomic

proof

take
d
; :: thesis: ( x = d & (Start-At (0,SCM)) +* d is Autonomy of Euclid-Algorithm & Euclid-Function . d c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d)) )
set A = {(IC ),(dl. 0),(dl. 1)};

set C = 5;

let P, Q be Instruction-Sequence of SCM; :: according to EXTPRO_1:def 10 :: thesis: ( not Euclid-Algorithm c= P or not Euclid-Algorithm c= Q or for b_{1}, b_{2} being set holds

( not (Start-At (0,SCM)) +* d c= b_{1} or not (Start-At (0,SCM)) +* d c= b_{2} or for b_{3} being set holds (Comput (P,b_{1},b_{3})) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,b_{2},b_{3})) | (dom ((Start-At (0,SCM)) +* d)) ) )

assume that

A26: Euclid-Algorithm c= P and

A27: Euclid-Algorithm c= Q ; :: thesis: for b_{1}, b_{2} being set holds

( not (Start-At (0,SCM)) +* d c= b_{1} or not (Start-At (0,SCM)) +* d c= b_{2} or for b_{3} being set holds (Comput (P,b_{1},b_{3})) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,b_{2},b_{3})) | (dom ((Start-At (0,SCM)) +* d)) )

let s1, s2 be State of SCM; :: thesis: ( not (Start-At (0,SCM)) +* d c= s1 or not (Start-At (0,SCM)) +* d c= s2 or for b_{1} being set holds (Comput (P,s1,b_{1})) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,b_{1})) | (dom ((Start-At (0,SCM)) +* d)) )

assume that

A28: (Start-At (0,SCM)) +* d c= s1 and

A29: (Start-At (0,SCM)) +* d c= s2 ; :: thesis: for b_{1} being set holds (Comput (P,s1,b_{1})) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,b_{1})) | (dom ((Start-At (0,SCM)) +* d))

A30: ( s2 . (dl. 0) = i1 & s2 . (dl. 1) = i2 ) by A10, A29;

let k be Nat; :: thesis: (Comput (P,s1,k)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,k)) | (dom ((Start-At (0,SCM)) +* d))

defpred S_{2}[ Nat] means ( IC (Comput (P,s1,$1)) = IC (Comput (Q,s2,$1)) & (Comput (P,s1,$1)) . (dl. 0) = (Comput (Q,s2,$1)) . (dl. 0) & (Comput (P,s1,$1)) . (dl. 1) = (Comput (Q,s2,$1)) . (dl. 1) );

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 S_{2}[4 * i] & j <> 0 & j <= 4 holds

S_{2}[(4 * i) + j]

(Comput (P,s1,0)) . (IC ) = IC s1 by EXTPRO_1:2

.= 0 by A32

.= IC s2 by A34

.= (Comput (Q,s2,0)) . (IC ) by EXTPRO_1:2 ;

then A61: S_{2}[ 0 ]
by A10, A28, A30, A31;

A62: 4 > 0 ;

S_{2}[k]
from NAT_D:sch 2(A61, A62, A35);

hence (Comput (P,s1,k)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,k)) | (dom ((Start-At (0,SCM)) +* d)) by A21, A33, GRFUNC_1:31; :: thesis: verum

end;set C = 5;

let P, Q be Instruction-Sequence of SCM; :: according to EXTPRO_1:def 10 :: thesis: ( not Euclid-Algorithm c= P or not Euclid-Algorithm c= Q or for b

( not (Start-At (0,SCM)) +* d c= b

assume that

A26: Euclid-Algorithm c= P and

A27: Euclid-Algorithm c= Q ; :: thesis: for b

( not (Start-At (0,SCM)) +* d c= b

let s1, s2 be State of SCM; :: thesis: ( not (Start-At (0,SCM)) +* d c= s1 or not (Start-At (0,SCM)) +* d c= s2 or for b

assume that

A28: (Start-At (0,SCM)) +* d c= s1 and

A29: (Start-At (0,SCM)) +* d c= s2 ; :: thesis: for b

A30: ( s2 . (dl. 0) = i1 & s2 . (dl. 1) = i2 ) by A10, A29;

let k be Nat; :: thesis: (Comput (P,s1,k)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,k)) | (dom ((Start-At (0,SCM)) +* d))

defpred S

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 S

S

proof

reconsider k = k as Element of NAT by ORDINAL1:def 12;
let i, j be Nat; :: thesis: ( S_{2}[4 * i] & j <> 0 & j <= 4 implies S_{2}[(4 * i) + j] )

assume that

A36: IC (Comput (P,s1,(4 * i))) = IC (Comput (Q,s2,(4 * i))) and

A37: (Comput (P,s1,(4 * i))) . (dl. 0) = (Comput (Q,s2,(4 * i))) . (dl. 0) and

A38: (Comput (P,s1,(4 * i))) . (dl. 1) = (Comput (Q,s2,(4 * i))) . (dl. 1) ; :: thesis: ( not j <> 0 or not j <= 4 or S_{2}[(4 * i) + j] )

assume A39: ( j <> 0 & j <= 4 ) ; :: thesis: S_{2}[(4 * i) + j]

then not not j = 0 & ... & not j = 4 ;

then A40: not not j = 1 & ... & not j = 4 by A39;

end;assume that

A36: IC (Comput (P,s1,(4 * i))) = IC (Comput (Q,s2,(4 * i))) and

A37: (Comput (P,s1,(4 * i))) . (dl. 0) = (Comput (Q,s2,(4 * i))) . (dl. 0) and

A38: (Comput (P,s1,(4 * i))) . (dl. 1) = (Comput (Q,s2,(4 * i))) . (dl. 1) ; :: thesis: ( not j <> 0 or not j <= 4 or S

assume A39: ( j <> 0 & j <= 4 ) ; :: thesis: S

then not not j = 0 & ... & not j = 4 ;

then A40: not not j = 1 & ... & not j = 4 by A39;

per cases
( IC (Comput (Q,s2,(4 * i))) = 0 or IC (Comput (Q,s2,(4 * i))) = 4 )
by A2, A3, A34, A27, A30, Lm4;

end;

suppose A41:
IC (Comput (Q,s2,(4 * i))) = 0
; :: thesis: S_{2}[(4 * i) + j]

A42: (Comput (P,s1,((4 * i) + 1))) . (dl. 0) =
(Comput (P,s1,(4 * i))) . (dl. 0)
by A26, A36, A41, Th2

.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 0) by A27, A37, A41, Th2 ;

A43: (Comput (P,s1,((4 * i) + 1))) . (dl. 2) = (Comput (P,s1,(4 * i))) . (dl. 1) 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))) . (dl. 1) = (Comput (P,s1,(4 * i))) . (dl. 1) by A26, A36, A41, Th2

.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 1) 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))) . (dl. 1) = ((Comput (P,s1,((4 * i) + 1))) . (dl. 0)) mod ((Comput (P,s1,((4 * i) + 1))) . (dl. 1)) by A26, A45, A50, Th3

.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 1) 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))) . (dl. 0) = ((Comput (P,s1,((4 * i) + 1))) . (dl. 0)) div ((Comput (P,s1,((4 * i) + 1))) . (dl. 1)) by A26, A45, A50, Th3

.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 0) by A27, A45, A47, A42, A44, Th3 ;

A56: ((4 * i) + 3) + 1 = (4 * i) + (3 + 1) ;

A57: (Comput (P,s1,((4 * i) + 3))) . (dl. 0) = (Comput (P,s1,((4 * i) + 2))) . (dl. 2) by A26, A46, A53, Th4

.= (Comput (Q,s2,((4 * i) + 3))) . (dl. 0) by A27, A46, A48, A51, Th4 ;

A58: (Comput (P,s1,((4 * i) + 3))) . (dl. 1) = (Comput (P,s1,((4 * i) + 2))) . (dl. 1) by A26, A46, A53, Th4

.= (Comput (Q,s2,((4 * i) + 3))) . (dl. 1) by A27, A46, A48, A52, Th4 ;

( (Comput (P,s1,((4 * i) + 3))) . (dl. 1) <= 0 or (Comput (P,s1,((4 * i) + 3))) . (dl. 1) > 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; :: thesis: ( (Comput (P,s1,((4 * i) + j))) . (dl. 0) = (Comput (Q,s2,((4 * i) + j))) . (dl. 0) & (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1) )

(Comput (P,s1,((4 * i) + 4))) . (dl. 0) = (Comput (P,s1,((4 * i) + 3))) . (dl. 0) by A26, A56, A54, Th5

.= (Comput (Q,s2,((4 * i) + 4))) . (dl. 0) by A27, A56, A49, A57, Th5 ;

hence (Comput (P,s1,((4 * i) + j))) . (dl. 0) = (Comput (Q,s2,((4 * i) + j))) . (dl. 0) by A40, A42, A55, A57; :: thesis: (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1)

(Comput (P,s1,((4 * i) + 4))) . (dl. 1) = (Comput (P,s1,((4 * i) + 3))) . (dl. 1) by A26, A56, A54, Th5

.= (Comput (Q,s2,((4 * i) + 4))) . (dl. 1) by A27, A56, A49, A58, Th5 ;

hence (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1) by A40, A44, A52, A58; :: thesis: verum

end;.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 0) by A27, A37, A41, Th2 ;

A43: (Comput (P,s1,((4 * i) + 1))) . (dl. 2) = (Comput (P,s1,(4 * i))) . (dl. 1) 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))) . (dl. 1) = (Comput (P,s1,(4 * i))) . (dl. 1) by A26, A36, A41, Th2

.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 1) 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))) . (dl. 1) = ((Comput (P,s1,((4 * i) + 1))) . (dl. 0)) mod ((Comput (P,s1,((4 * i) + 1))) . (dl. 1)) by A26, A45, A50, Th3

.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 1) 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))) . (dl. 0) = ((Comput (P,s1,((4 * i) + 1))) . (dl. 0)) div ((Comput (P,s1,((4 * i) + 1))) . (dl. 1)) by A26, A45, A50, Th3

.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 0) by A27, A45, A47, A42, A44, Th3 ;

A56: ((4 * i) + 3) + 1 = (4 * i) + (3 + 1) ;

A57: (Comput (P,s1,((4 * i) + 3))) . (dl. 0) = (Comput (P,s1,((4 * i) + 2))) . (dl. 2) by A26, A46, A53, Th4

.= (Comput (Q,s2,((4 * i) + 3))) . (dl. 0) by A27, A46, A48, A51, Th4 ;

A58: (Comput (P,s1,((4 * i) + 3))) . (dl. 1) = (Comput (P,s1,((4 * i) + 2))) . (dl. 1) by A26, A46, A53, Th4

.= (Comput (Q,s2,((4 * i) + 3))) . (dl. 1) by A27, A46, A48, A52, Th4 ;

( (Comput (P,s1,((4 * i) + 3))) . (dl. 1) <= 0 or (Comput (P,s1,((4 * i) + 3))) . (dl. 1) > 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; :: thesis: ( (Comput (P,s1,((4 * i) + j))) . (dl. 0) = (Comput (Q,s2,((4 * i) + j))) . (dl. 0) & (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1) )

(Comput (P,s1,((4 * i) + 4))) . (dl. 0) = (Comput (P,s1,((4 * i) + 3))) . (dl. 0) by A26, A56, A54, Th5

.= (Comput (Q,s2,((4 * i) + 4))) . (dl. 0) by A27, A56, A49, A57, Th5 ;

hence (Comput (P,s1,((4 * i) + j))) . (dl. 0) = (Comput (Q,s2,((4 * i) + j))) . (dl. 0) by A40, A42, A55, A57; :: thesis: (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1)

(Comput (P,s1,((4 * i) + 4))) . (dl. 1) = (Comput (P,s1,((4 * i) + 3))) . (dl. 1) by A26, A56, A54, Th5

.= (Comput (Q,s2,((4 * i) + 4))) . (dl. 1) by A27, A56, A49, A58, Th5 ;

hence (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1) by A40, A44, A52, A58; :: thesis: verum

suppose A59:
IC (Comput (Q,s2,(4 * i))) = 4
; :: thesis: S_{2}[(4 * i) + j]

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 S_{2}[(4 * i) + j]
by A36, A37, A38, A60, EXTPRO_1:20, NAT_1:11; :: thesis: verum

end;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 S

(Comput (P,s1,0)) . (IC ) = IC s1 by EXTPRO_1:2

.= 0 by A32

.= IC s2 by A34

.= (Comput (Q,s2,0)) . (IC ) by EXTPRO_1:2 ;

then A61: S

A62: 4 > 0 ;

S

hence (Comput (P,s1,k)) | (dom ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,k)) | (dom ((Start-At (0,SCM)) +* d)) by A21, A33, GRFUNC_1:31; :: thesis: verum

thus x = d ; :: thesis: ( (Start-At (0,SCM)) +* d is Autonomy of Euclid-Algorithm & Euclid-Function . d c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d)) )

A63: (Start-At (0,SCM)) +* d is Euclid-Algorithm -halted

proof

thus
(Start-At (0,SCM)) +* d is Autonomy of Euclid-Algorithm
by A25, A63, EXTPRO_1:def 12; :: thesis: Euclid-Function . d c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d))
reconsider i19 = i1, i29 = i2 as Element of NAT by A2, A3, INT_1:3;

let t be State of SCM; :: according to EXTPRO_1:def 11 :: thesis: ( not (Start-At (0,SCM)) +* d c= t or for b_{1} being set holds

( not Euclid-Algorithm c= b_{1} or b_{1} halts_on t ) )

assume A64: (Start-At (0,SCM)) +* d c= t ; :: thesis: for b_{1} being set holds

( not Euclid-Algorithm c= b_{1} or b_{1} halts_on t )

let P be Instruction-Sequence of SCM; :: thesis: ( not Euclid-Algorithm c= P or P halts_on t )

assume A65: Euclid-Algorithm c= P ; :: thesis: P halts_on t

set t9 = Comput (P,t,4);

A66: t . (dl. 1) = i2 by A10, A64;

A67: ( t is 0 -started & t . (dl. 0) = i1 ) by A23, A10, A64, MEMSTR_0:17;

end;let t be State of SCM; :: according to EXTPRO_1:def 11 :: thesis: ( not (Start-At (0,SCM)) +* d c= t or for b

( not Euclid-Algorithm c= b

assume A64: (Start-At (0,SCM)) +* d c= t ; :: thesis: for b

( not Euclid-Algorithm c= b

let P be Instruction-Sequence of SCM; :: thesis: ( not Euclid-Algorithm c= P or P halts_on t )

assume A65: Euclid-Algorithm c= P ; :: thesis: P halts_on t

set t9 = Comput (P,t,4);

A66: t . (dl. 1) = i2 by A10, A64;

A67: ( t is 0 -started & t . (dl. 0) = i1 ) by A23, A10, A64, MEMSTR_0:17;

per cases
( i1 > i2 or i1 = i2 or i1 < i2 )
by XXREAL_0:1;

end;

suppose
i1 > i2
; :: thesis: P halts_on t

then
ex k being Nat st P halts_at IC (Comput (P,t,k))
by A3, A65, A67, A66, Lm6;

hence P halts_on t by EXTPRO_1:16; :: thesis: verum

end;hence P halts_on t by EXTPRO_1:16; :: thesis: verum

suppose A68:
i1 = i2
; :: thesis: P halts_on t

A69: i1 mod i2 =
i19 mod i29

.= 0 by A68, NAT_D:25 ;

A70: Comput (P,t,4) = Comput (P,t,(4 * (0 + 1))) ;

t = Comput (P,t,(4 * 0)) by EXTPRO_1:2;

then (Comput (P,t,4)) . (dl. 1) = (t . (dl. 0)) mod (t . (dl. 1)) by A2, A3, A65, A67, A66, A70, Lm5;

then IC (Comput (P,t,4)) = 4 by A2, A3, A65, A67, A66, A69, A70, Lm4;

then P halts_at IC (Comput (P,t,4)) by A65, Lm3;

hence P halts_on t by EXTPRO_1:16; :: thesis: verum

end;.= 0 by A68, NAT_D:25 ;

A70: Comput (P,t,4) = Comput (P,t,(4 * (0 + 1))) ;

t = Comput (P,t,(4 * 0)) by EXTPRO_1:2;

then (Comput (P,t,4)) . (dl. 1) = (t . (dl. 0)) mod (t . (dl. 1)) by A2, A3, A65, A67, A66, A70, Lm5;

then IC (Comput (P,t,4)) = 4 by A2, A3, A65, A67, A66, A69, A70, Lm4;

then P halts_at IC (Comput (P,t,4)) by A65, Lm3;

hence P halts_on t by EXTPRO_1:16; :: thesis: verum

suppose A71:
i1 < i2
; :: thesis: P halts_on t

A72:
Comput (P,t,4) = 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: (Comput (P,t,4)) . (dl. 1) = i1 by A2, A3, A65, A67, A66, A73, A72, Lm5;

then IC (Comput (P,t,4)) = 0 by A2, A3, A65, A67, A66, A72, Lm4;

then A75: Comput (P,t,4) is 0 -started ;

(Comput (P,t,4)) . (dl. 0) = i2 by A2, A3, A65, A67, A66, A73, A72, Lm5;

then consider k0 being Nat such that

A76: P halts_at IC (Comput (P,(Comput (P,t,4)),k0)) by A2, A71, A74, A75, A65, Lm6;

P halts_at IC (Comput (P,t,(k0 + 4))) by A76, EXTPRO_1:4;

hence P halts_on t by EXTPRO_1:16; :: thesis: verum

end;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: (Comput (P,t,4)) . (dl. 1) = i1 by A2, A3, A65, A67, A66, A73, A72, Lm5;

then IC (Comput (P,t,4)) = 0 by A2, A3, A65, A67, A66, A72, Lm4;

then A75: Comput (P,t,4) is 0 -started ;

(Comput (P,t,4)) . (dl. 0) = i2 by A2, A3, A65, A67, A66, A73, A72, Lm5;

then consider k0 being Nat such that

A76: P halts_at IC (Comput (P,(Comput (P,t,4)),k0)) by A2, A71, A74, A75, A65, Lm6;

P halts_at IC (Comput (P,t,(k0 + 4))) by A76, EXTPRO_1:4;

hence P halts_on t by EXTPRO_1:16; :: thesis: verum

then A77: Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d)) = (Result (T,t)) | (dom ((Start-At (0,SCM)) +* d)) by A6, A5, EXTPRO_1:def 13;

dl. 0 in the carrier of SCM ;

then A78: dl. 0 in dom (Result (T,t)) by PARTFUN1:def 2;

A79: d . (dl. 0) = i1 by A4, AMI_3:10, FUNCT_4:63;

A80: d . (dl. 1) = i2 by A4, FUNCT_4:63;

A81: d c= (Start-At (0,SCM)) +* d by FUNCT_4:25;

A82: dom d c= dom ((Start-At (0,SCM)) +* d) by A81, RELAT_1:11;

A83: d c= t by A81, A5;

A84: dom d = {(dl. 0),(dl. 1)} by A4, FUNCT_4:62;

then A85: dl. 1 in dom d by TARSKI:def 2;

A86: t . (dl. 1) = i2 by A83, A80, A85, GRFUNC_1:2;

A87: dl. 0 in dom d by A84, TARSKI:def 2;

t . (dl. 0) = i1 by A83, A79, A87, GRFUNC_1:2;

then A88: (Result (T,t)) . (dl. 0) = i1 gcd i2 by A2, A3, A24, A86, Th7, A6;

dom ((dl. 0) .--> (i1 gcd i2)) c= dom d by A84, ZFMISC_1:7;

then A90: dom ((dl. 0) .--> (i1 gcd i2)) c= dom ((Start-At (0,SCM)) +* d) by A82;

(dl. 0) .--> (i1 gcd i2) c= (Result (T,t)) | (dom ((Start-At (0,SCM)) +* d)) by A90, A78, A88, FUNCT_4:85, RELAT_1:151;

hence Euclid-Function . d c= Result (Euclid-Algorithm,((Start-At (0,SCM)) +* d)) by A77, A2, A3, A4, Th9; :: thesis: verum