set q = Euclide-Algorithm ;
set p = (Start-At (0,SCM)) +* Euclide-Algorithm;
let x be set ; :: according to EXTPRO_1:def 13 :: thesis:
A1: ( IC <> 2 & IC <> 3 ) by AMI_3:57;
A2: IC <> 4 by AMI_3:57;
( IC <> 0 & IC <> 1 ) by AMI_3:57;
then A3: not IC in dom Euclide-Algorithm by A1, A2, Th4, CARD_1:91, ENUMSET1:def 3;
A4: dom Euclide-Algorithm c= NAT by RELAT_1:def 18;
A5: dom Euclide-Algorithm misses Data-Locations SCM by A4, XBOOLE_1:63, COMPOS_1:51;
DataPart ((Start-At (0,SCM)) +* Euclide-Algorithm) = (DataPart (Start-At (0,SCM))) +* (DataPart Euclide-Algorithm) by FUNCT_4:75
.= {} +* (DataPart Euclide-Algorithm) by COMPOS_1:30
.= {} +* {} by A5, RELAT_1:95
.= {} ;
then A6: dom (DataPart ((Start-At (0,SCM)) +* Euclide-Algorithm)) = {} ;
assume x in dom Euclide-Function ; :: thesis:
then consider i1, i2 being Integer such that
A7: i1 > 0 and
A8: i2 > 0 and
A9: x = ((dl. 0),(dl. 1)) --> (i1,i2) by Th11;
reconsider d = x as FinPartState of SCM by A9;
consider t being State of SCM such that
A10: ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d c= t by PBOOLE:156;
B10: ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= ProgramPart t by A10, RELAT_1:105;
A11: dom d = {(dl. 0),(dl. 1)} by A9, FUNCT_4:65;
then A12: dl. 1 in dom d by TARSKI:def 2;
( dl. 0 <> IC & dl. 1 <> IC ) by AMI_3:57;
then ( not dl. 0 in {(IC )} & not dl. 1 in {(IC )} ) by TARSKI:def 1;
then A13: dom d misses {(IC )} by A11, ZFMISC_1:57;

A14: now

assume dom d meets NAT ; :: thesis:
then consider x being set such that
A15: x in dom d and
A16: x in NAT by XBOOLE_0:3;
( x = dl. 0 or x = dl. 1 ) by A15, A11, TARSKI:def 2;
hence contradiction by A16, AMI_3:56; :: thesis:

end;

then dom d misses {(IC )} \/ NAT by A13, XBOOLE_1:70;
then A17: d is data-only by COMPOS_1:def 23;
then A18: dom d misses NAT by COMPOS_1:40;
then A19: ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) = ProgramPart ((Start-At (0,SCM)) +* Euclide-Algorithm) by FUNCT_4:76;
A20: NPP d = d by A17, COMPOS_1:176;
A21: dl. 0 in dom d by A11, TARSKI:def 2;
A22: for t being State of SCM st NPP (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= t holds
( t . (dl. 0) = i1 & t . (dl. 1) = i2 )

proof

A23: d c= ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d by FUNCT_4:26;
let t be State of SCM; :: thesis:
assume Z: NPP (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= t ; :: thesis:
d c= ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d by FUNCT_4:26;
then NPP d c= NPP (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) by COMPOS_1:170;
then A24: NPP d c= t by A23, XBOOLE_1:1, Z;
hence t . (dl. 0) = d . (dl. 0) by A21, GRFUNC_1:8, A20
.= i1 by A9, AMI_3:52, FUNCT_4:66 ;
:: thesis:
thus t . (dl. 1) = d . (dl. 1) by A12, A24, GRFUNC_1:8, A20
.= i2 by A9, FUNCT_4:66 ; :: thesis:

end;

dom (Start-At (0,SCM)) = {(IC )} by FUNCOP_1:19;
then A25: dom ((Start-At (0,SCM)) +* Euclide-Algorithm) = {(IC )} \/ 5 by Th4, FUNCT_4:def 1;

A26: now

assume dom ((Start-At (0,SCM)) +* Euclide-Algorithm) meets dom d ; :: thesis:
then consider x being set such that
A27: x in dom ((Start-At (0,SCM)) +* Euclide-Algorithm) and
A28: x in dom d by XBOOLE_0:3;
( x in {(IC )} or x in 5 ) by A25, A27, XBOOLE_0:def 3;
then A29: ( x = IC or x = 0 or x = 1 or x = 2 or x = 3 or x = 4 ) by CARD_1:91, ENUMSET1:def 3, TARSKI:def 1;
( x = dl. 0 or x = dl. 1 ) by A11, A28, TARSKI:def 2;
hence contradiction by A29, AMI_3:56, AMI_3:57; :: thesis:

end;

proof

set A = {(IC ),(dl. 0),(dl. 1)};
set C = 5;
let P, Q be the Instructions of SCM -valued ManySortedSet of NAT ; :: according to EXTPRO_1:def 9 :: thesis:
assume that
A39: ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= P and
A40: ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= Q ; :: thesis:
let s1, s2 be State of SCM; :: thesis:
assume that
A41: NPP (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= s1 and
A42: NPP (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= s2 ; :: thesis:
A43: ( s2 . (dl. 0) = i1 & s2 . (dl. 1) = i2 ) by A22, A42;
let k be Element of NAT ; :: thesis:
A44: Euclide-Algorithm c= Q by A37, XBOOLE_1:1, A40;
defpred S₂[ Element of NAT ] means ( (Comput (P,s1,$1)) . (IC ) = (Comput (Q,s2,$1)) . (IC ) & (Comput (P,s1,$1)) . (dl. 0) = (Comput (Q,s2,$1)) . (dl. 0) & (Comput (P,s1,$1)) . (dl. 1) = (Comput (Q,s2,$1)) . (dl. 1) );
A45: ( Comput (P,s1,0) = s1 & Comput (Q,s2,0) = s2 ) by EXTPRO_1:3;
A46: s1 is 0 -started by A35, A41, COMPOS_1:8;
A47: dom (Comput (P,s1,k)) = the carrier of SCM by PARTFUN1:def 4
.= dom (Comput (Q,s2,k)) by PARTFUN1:def 4 ;
A48: Euclide-Algorithm c= P by A37, XBOOLE_1:1, A39;
A49: s2 is 0 -started by A35, A42, COMPOS_1:8;
A50: for i, j being Nat st S₂[4 * i] & j <> 0 & j <= 4 holds
S₂[(4 * i) + j]

proof

let i, j be Nat; :: thesis:
assume that
A51: (Comput (P,s1,(4 * i))) . (IC ) = (Comput (Q,s2,(4 * i))) . (IC ) and
A52: (Comput (P,s1,(4 * i))) . (dl. 0) = (Comput (Q,s2,(4 * i))) . (dl. 0) and
A53: (Comput (P,s1,(4 * i))) . (dl. 1) = (Comput (Q,s2,(4 * i))) . (dl. 1) ; :: thesis:
A54: i in NAT by ORDINAL1:def 13;
assume ( j <> 0 & j <= 4 ) ; :: thesis:
then A55: ( j = 1 or j = 2 or j = 3 or j = 4 ) by NAT_1:29;

per cases by A7, A8, A49, A44, A43, A54, Lm4;

suppose A56: IC (Comput (Q,s2,(4 * i))) = 0 ; :: thesis:

then A57: IC (Comput (P,s1,(4 * i))) = 0 by A51;
then A58: (Comput (P,s1,((4 * i) + 1))) . (dl. 0) = (Comput (P,s1,(4 * i))) . (dl. 0) by A48, Th5
.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 0) by A44, A52, A56, Th5 ;
A59: (Comput (P,s1,((4 * i) + 1))) . (dl. 2) = (Comput (P,s1,(4 * i))) . (dl. 1) by A48, A57, Th5
.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 2) by A44, A53, A56, Th5 ;
A60: (Comput (P,s1,((4 * i) + 1))) . (dl. 1) = (Comput (P,s1,(4 * i))) . (dl. 1) by A48, A57, Th5
.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 1) by A44, A53, A56, Th5 ;
A61: ((4 * i) + 1) + 1 = (4 * i) + (1 + 1) ;
A62: ((4 * i) + 2) + 1 = (4 * i) + (2 + 1) ;
A63: IC (Comput (Q,s2,((4 * i) + 1))) = 1 by A44, A56, Th5;
then A64: IC (Comput (Q,s2,((4 * i) + 2))) = 2 by A44, A61, Th6;
then A65: IC (Comput (Q,s2,((4 * i) + 3))) = 3 by A44, A62, Th7;
A66: IC (Comput (P,s1,((4 * i) + 1))) = 1 by A48, A57, Th5;
then A67: (Comput (P,s1,((4 * i) + 2))) . (dl. 2) = (Comput (P,s1,((4 * i) + 1))) . (dl. 2) by A48, A61, Th6
.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 2) by A44, A61, A63, A59, Th6 ;
A68: (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 A48, A61, A66, Th6
.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 1) by A44, A61, A63, A58, A60, Th6 ;
A69: IC (Comput (P,s1,((4 * i) + 2))) = 2 by A48, A61, A66, Th6;
then A70: IC (Comput (P,s1,((4 * i) + 3))) = 3 by A48, A62, Th7;
A71: (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 A48, A61, A66, Th6
.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 0) by A44, A61, A63, A58, A60, Th6 ;
A72: ((4 * i) + 3) + 1 = (4 * i) + (3 + 1) ;
A73: (Comput (P,s1,((4 * i) + 3))) . (dl. 0) = (Comput (P,s1,((4 * i) + 2))) . (dl. 2) by A48, A62, A69, Th7
.= (Comput (Q,s2,((4 * i) + 3))) . (dl. 0) by A44, A62, A64, A67, Th7 ;
A74: (Comput (P,s1,((4 * i) + 3))) . (dl. 1) = (Comput (P,s1,((4 * i) + 2))) . (dl. 1) by A48, A62, A69, Th7
.= (Comput (Q,s2,((4 * i) + 3))) . (dl. 1) by A44, A62, A64, A68, Th7 ;
( (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 A48, A44, A72, A70, A65, A74, Th8;
hence (Comput (P,s1,((4 * i) + j))) . (IC ) = (Comput (Q,s2,((4 * i) + j))) . (IC ) by A55, A66, A63, A69, A64, A70, A65; :: thesis:
(Comput (P,s1,((4 * i) + 4))) . (dl. 0) = (Comput (P,s1,((4 * i) + 3))) . (dl. 0) by A48, A72, A70, Th8
.= (Comput (Q,s2,((4 * i) + 4))) . (dl. 0) by A44, A72, A65, A73, Th8 ;
hence (Comput (P,s1,((4 * i) + j))) . (dl. 0) = (Comput (Q,s2,((4 * i) + j))) . (dl. 0) by A55, A58, A71, A73; :: thesis:
(Comput (P,s1,((4 * i) + 4))) . (dl. 1) = (Comput (P,s1,((4 * i) + 3))) . (dl. 1) by A48, A72, A70, Th8
.= (Comput (Q,s2,((4 * i) + 4))) . (dl. 1) by A44, A72, A65, A74, Th8 ;
hence (Comput (P,s1,((4 * i) + j))) . (dl. 1) = (Comput (Q,s2,((4 * i) + j))) . (dl. 1) by A55, A60, A68, A74; :: thesis:

end;

suppose A75: IC (Comput (Q,s2,(4 * i))) = 4 ; :: thesis:

then P halts_at IC (Comput (P,s1,(4 * i))) by A48, A51, Lm3;
then A76: 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 A44, A75, Lm3;
hence S₂[(4 * i) + j] by A51, A52, A53, A76, EXTPRO_1:20, NAT_1:11; :: thesis:

end;

(Comput (P,s1,0)) . (IC ) = IC s1 by EXTPRO_1:3
.= 0 by A46, COMPOS_1:def 16
.= IC s2 by A49, COMPOS_1:def 16
.= (Comput (Q,s2,0)) . (IC ) by EXTPRO_1:3 ;
then A77: S₂[ 0 ] by A22, A41, A43, A45;
A78: 4 > 0 ;
S₂[k] from NAT_D:sch 2(A77, A78, A50);
hence (Comput (P,s1,k)) | (proj1 (NPP (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d))) = (Comput (Q,s2,k)) | (proj1 (NPP (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d))) by A33, A47, GRFUNC_1:92; :: thesis:

end;

take d ; :: thesis:
thus x = d ; :: thesis:
A79: ((Start-At (0,SCM)) +* Euclide-Algorithm) +* d is halting

proof

reconsider i19 = i1, i29 = i2 as Element of NAT by A7, A8, INT_1:16;
let t be State of SCM; :: according to EXTPRO_1:def 10 :: thesis:
assume A80: NPP (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= t ; :: thesis:
then B80: NPP (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= t by XBOOLE_1:1;
let P be the Instructions of SCM -valued ManySortedSet of NAT ; :: thesis:
assume A81: ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= P ; :: thesis:
set t9 = Comput (P,t,4);
A82: ProgramPart (((Start-At (0,SCM)) +* Euclide-Algorithm) +* d) c= P by A81;
then A83: Euclide-Algorithm c= P by A37, XBOOLE_1:1;
A84: t . (dl. 1) = i2 by A22, A80, B80;
A85: ( t is 0 -started & t . (dl. 0) = i1 ) by A35, A22, A80, COMPOS_1:8, B80;

per cases by XXREAL_0:1;

suppose i1 > i2 ; :: thesis:

then ex k being Element of NAT st P halts_at IC (Comput (P,t,k)) by A8, A83, A85, A84, Lm6;
hence P halts_on t by EXTPRO_1:16; :: thesis:

end;

suppose A86: i1 = i2 ; :: thesis:

A87: i1 mod i2 = i19 mod i29
.= 0 by A86, NAT_D:25 ;
A88: Comput (P,t,4) = Comput (P,t,(4 * (0 + 1))) ;
t = Comput (P,t,(4 * 0)) by EXTPRO_1:3;
then (Comput (P,t,4)) . (dl. 1) = (t . (dl. 0)) mod (t . (dl. 1)) by A7, A8, A83, A85, A84, A88, Lm5;
then IC (Comput (P,t,4)) = 4 by A7, A8, A83, A85, A84, A87, A88, Lm4;
then P halts_at IC (Comput (P,t,4)) by A83, Lm3;
hence P halts_on t by EXTPRO_1:16; :: thesis:

end;

suppose A89: i1 < i2 ; :: thesis:

A90: Comput (P,t,4) = Comput (P,t,(4 * (0 + 1))) ;
A91: Euclide-Algorithm c= P by A82, A37, XBOOLE_1:1;
A92: t = Comput (P,t,(4 * 0)) by EXTPRO_1:3;
i1 mod i2 = i19 mod i29
.= i19 by A89, NAT_D:24 ;
then A93: (Comput (P,t,4)) . (dl. 1) = i1 by A7, A8, A83, A85, A84, A92, A90, Lm5;
then IC (Comput (P,t,4)) = 0 by A7, A8, A83, A85, A84, A90, Lm4;
then A94: Comput (P,t,4) is 0 -started by COMPOS_1:def 20;
(Comput (P,t,4)) . (dl. 0) = i2 by A7, A8, A83, A85, A84, A92, A90, Lm5;
then consider k0 being Element of NAT such that
A95: P halts_at IC (Comput (P,(Comput (P,t,4)),k0)) by A7, A89, A93, A94, A91, Lm6;
P halts_at IC (Comput (P,t,(k0 + 4))) by A95, EXTPRO_1:5;
hence P halts_on t by EXTPRO_1:16; :: thesis:

end;