set q = Euclide-Algorithm ;
set p = Start-At (0,SCM);
let x be set ; :: according to EXTPRO_1:def 14 :: thesis: ( not x in proj1 Euclide-Function or ex b1 being set st
( x = b1 & (Start-At (0,SCM)) +* b1 is Autonomy of Euclide-Algorithm & Euclide-Function . b1 c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* b1)) ) )
DataPart (Start-At (0,SCM)) = {} by MEMSTR_0:20;
then A6: dom (DataPart (Start-At (0,SCM))) = {} ;
assume x in dom Euclide-Function ; :: thesis: ex b1 being set st
( x = b1 & (Start-At (0,SCM)) +* b1 is Autonomy of Euclide-Algorithm & Euclide-Function . b1 c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* b1)) )
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;
x = ((dl. 0) .--> i1) +* ((dl. 1) .--> i2) by A9;
then reconsider d = x as FinPartState of SCM ;
consider t being State of SCM such that
A10: (Start-At (0,SCM)) +* d c= t by PBOOLE:141;
consider T being Instruction-Sequence of SCM such that
C10: Euclide-Algorithm c= T by PBOOLE:145;
A11: dom d = {(dl. 0),(dl. 1)} by A9, FUNCT_4:62;
then A12: dl. 1 in dom d by TARSKI:def 2;
A21: dl. 0 in dom d by A11, TARSKI:def 2;
A22: 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 Z: (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 A24: d c= t by Z, XBOOLE_1:1;
hence t . (dl. 0) = d . (dl. 0) by A21, GRFUNC_1:2
.= i1 by A9, AMI_3:10, FUNCT_4:63 ;
:: thesis: t . (dl. 1) = i2
thus t . (dl. 1) = d . (dl. 1) by A12, A24, GRFUNC_1:2
.= i2 by A9, FUNCT_4:63 ; :: thesis: verum
end;
A25: dom (Start-At (0,SCM)) = {(IC )} by FUNCOP_1:13;
A26: now
assume dom (Start-At (0,SCM)) meets dom d ; :: thesis: contradiction
then consider x being set such that
A27: x in dom (Start-At (0,SCM)) and
A28: x in dom d by XBOOLE_0:3;
A29: ( x = IC or x = 0 or x = 1 or x = 2 or x = 3 or x = 4 ) by A25, A27, TARSKI:def 1;
( x = dl. 0 or x = dl. 1 ) by A11, A28, TARSKI:def 2;
hence contradiction by A29, AMI_3:12, AMI_3:13; :: thesis: verum
end;
then A30: Start-At (0,SCM) c= (Start-At (0,SCM)) +* d by FUNCT_4:32;
A31: IC in dom (Start-At (0,SCM)) by A25, TARSKI:def 1;
(dom (Start-At (0,SCM))) /\ (dom d) = {} by A26, XBOOLE_0:def 7;
then A32: not IC in dom d by A31, XBOOLE_0:def 4;
set A = {(IC ),(dl. 0),(dl. 1)};
set C = 5;
A33: 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 A31, MEMSTR_0:24
.= {(IC )} \/ {(dl. 0),(dl. 1)} by A9, A6, FUNCT_4:62
.= {(IC ),(dl. 0),(dl. 1)} by ENUMSET1:2 ;
A34: dom (Start-At (0,SCM)) c= dom ((Start-At (0,SCM)) +* d) by A30, RELAT_1:11;
IC ((Start-At (0,SCM)) +* d) = IC (Start-At (0,SCM)) by A32, FUNCT_4:11
.= 0 by FUNCOP_1:72 ;
then A35: (Start-At (0,SCM)) +* d is 0 -started by A34, A31, MEMSTR_0:def 8;
then A36: t is 0 -started by A10, MEMSTR_0:17;
A38: (Start-At (0,SCM)) +* d is Euclide-Algorithm -autonomic
proof
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 Euclide-Algorithm c= P or not Euclide-Algorithm c= Q or for b1, b2 being set holds
( not (Start-At (0,SCM)) +* d c= b1 or not (Start-At (0,SCM)) +* d c= b2 or for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 ((Start-At (0,SCM)) +* d)) = (Comput (Q,b2,b3)) | (proj1 ((Start-At (0,SCM)) +* d)) ) )
assume that
A39: Euclide-Algorithm c= P and
A40: Euclide-Algorithm c= Q ; :: thesis: for b1, b2 being set holds
( not (Start-At (0,SCM)) +* d c= b1 or not (Start-At (0,SCM)) +* d c= b2 or for b3 being Element of NAT holds (Comput (P,b1,b3)) | (proj1 ((Start-At (0,SCM)) +* d)) = (Comput (Q,b2,b3)) | (proj1 ((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 b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,b1)) | (proj1 ((Start-At (0,SCM)) +* d)) )
assume that
A41: (Start-At (0,SCM)) +* d c= s1 and
A42: (Start-At (0,SCM)) +* d c= s2 ; :: thesis: for b1 being Element of NAT holds (Comput (P,s1,b1)) | (proj1 ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,b1)) | (proj1 ((Start-At (0,SCM)) +* d))
A43: ( s2 . (dl. 0) = i1 & s2 . (dl. 1) = i2 ) by A22, A42;
let k be Element of NAT ; :: thesis: (Comput (P,s1,k)) | (proj1 ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,k)) | (proj1 ((Start-At (0,SCM)) +* d))
defpred S2[ Element of 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) );
A45: ( Comput (P,s1,0) = s1 & Comput (Q,s2,0) = s2 ) by EXTPRO_1:2;
A46: s1 is 0 -started by A35, A41, MEMSTR_0:17;
A47: dom (Comput (P,s1,k)) = the carrier of SCM by PARTFUN1:def 2
.= dom (Comput (Q,s2,k)) by PARTFUN1:def 2 ;
A49: s2 is 0 -started by A35, A42, MEMSTR_0:17;
A50: for i, j being Nat st S2[4 * i] & j <> 0 & j <= 4 holds
S2[(4 * i) + j]
proof
let i, j be Nat; :: thesis: ( S2[4 * i] & j <> 0 & j <= 4 implies S2[(4 * i) + j] )
assume that
A51: IC (Comput (P,s1,(4 * i))) = IC (Comput (Q,s2,(4 * i))) 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: ( not j <> 0 or not j <= 4 or S2[(4 * i) + j] )
A54: i in NAT by ORDINAL1:def 12;
assume ( j <> 0 & j <= 4 ) ; :: thesis: S2[(4 * i) + j]
then A55: ( j = 1 or j = 2 or j = 3 or j = 4 ) by NAT_1:28;
per cases ( IC (Comput (Q,s2,(4 * i))) = 0 or IC (Comput (Q,s2,(4 * i))) = 4 ) by A7, A8, A49, A40, A43, A54, Lm4;
suppose A56: IC (Comput (Q,s2,(4 * i))) = 0 ; :: thesis: S2[(4 * i) + j]
A58: (Comput (P,s1,((4 * i) + 1))) . (dl. 0) = (Comput (P,s1,(4 * i))) . (dl. 0) by A39, A51, A56, Th5
.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 0) by A40, A52, A56, Th5 ;
A59: (Comput (P,s1,((4 * i) + 1))) . (dl. 2) = (Comput (P,s1,(4 * i))) . (dl. 1) by A39, A51, A56, Th5
.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 2) by A40, A53, A56, Th5 ;
A60: (Comput (P,s1,((4 * i) + 1))) . (dl. 1) = (Comput (P,s1,(4 * i))) . (dl. 1) by A39, A51, A56, Th5
.= (Comput (Q,s2,((4 * i) + 1))) . (dl. 1) by A40, 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 A40, A56, Th5;
then A64: IC (Comput (Q,s2,((4 * i) + 2))) = 2 by A40, A61, Th6;
then A65: IC (Comput (Q,s2,((4 * i) + 3))) = 3 by A40, A62, Th7;
A66: IC (Comput (P,s1,((4 * i) + 1))) = 1 by A39, A51, A56, Th5;
then A67: (Comput (P,s1,((4 * i) + 2))) . (dl. 2) = (Comput (P,s1,((4 * i) + 1))) . (dl. 2) by A39, A61, Th6
.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 2) by A40, 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 A39, A61, A66, Th6
.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 1) by A40, A61, A63, A58, A60, Th6 ;
A69: IC (Comput (P,s1,((4 * i) + 2))) = 2 by A39, A61, A66, Th6;
then A70: IC (Comput (P,s1,((4 * i) + 3))) = 3 by A39, 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 A39, A61, A66, Th6
.= (Comput (Q,s2,((4 * i) + 2))) . (dl. 0) by A40, 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 A39, A62, A69, Th7
.= (Comput (Q,s2,((4 * i) + 3))) . (dl. 0) by A40, A62, A64, A67, Th7 ;
A74: (Comput (P,s1,((4 * i) + 3))) . (dl. 1) = (Comput (P,s1,((4 * i) + 2))) . (dl. 1) by A39, A62, A69, Th7
.= (Comput (Q,s2,((4 * i) + 3))) . (dl. 1) by A40, 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 A39, A40, A72, A70, A65, A74, Th8;
hence IC (Comput (P,s1,((4 * i) + j))) = IC (Comput (Q,s2,((4 * i) + j))) by A55, A66, A40, A56, Th5, A39, A61, Th6, A64, A70, A62, Th7; :: 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 A39, A72, A70, Th8
.= (Comput (Q,s2,((4 * i) + 4))) . (dl. 0) by A40, 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) + 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 A39, A72, A70, Th8
.= (Comput (Q,s2,((4 * i) + 4))) . (dl. 1) by A40, 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: verum
end;
suppose A75: IC (Comput (Q,s2,(4 * i))) = 4 ; :: thesis: S2[(4 * i) + j]
then P halts_at IC (Comput (P,s1,(4 * i))) by A39, 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 A40, A75, Lm3;
hence S2[(4 * i) + j] by A51, A52, A53, A76, EXTPRO_1:20, NAT_1:11; :: thesis: verum
end;
end;
end;
(Comput (P,s1,0)) . (IC ) = IC s1 by EXTPRO_1:2
.= 0 by A46, MEMSTR_0:def 8
.= IC s2 by A49, MEMSTR_0:def 8
.= (Comput (Q,s2,0)) . (IC ) by EXTPRO_1:2 ;
then A77: S2[ 0 ] by A22, A41, A43, A45;
A78: 4 > 0 ;
S2[k] from NAT_D:sch 2(A77, A78, A50);
hence (Comput (P,s1,k)) | (proj1 ((Start-At (0,SCM)) +* d)) = (Comput (Q,s2,k)) | (proj1 ((Start-At (0,SCM)) +* d)) by A33, A47, GRFUNC_1:31; :: thesis: verum
end;
take d ; :: thesis: ( x = d & (Start-At (0,SCM)) +* d is Autonomy of Euclide-Algorithm & Euclide-Function . d c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* d)) )
thus x = d ; :: thesis: ( (Start-At (0,SCM)) +* d is Autonomy of Euclide-Algorithm & Euclide-Function . d c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* d)) )
A79: (Start-At (0,SCM)) +* d is Euclide-Algorithm -halted
proof
reconsider i19 = i1, i29 = i2 as Element of NAT by A7, A8, 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 b1 being set holds
( not Euclide-Algorithm c= b1 or b1 halts_on t ) )
assume B80: (Start-At (0,SCM)) +* d c= t ; :: thesis: for b1 being set holds
( not Euclide-Algorithm c= b1 or b1 halts_on t )
let P be Instruction-Sequence of SCM; :: thesis: ( not Euclide-Algorithm c= P or P halts_on t )
assume A81: Euclide-Algorithm c= P ; :: thesis: P halts_on t
set t9 = Comput (P,t,4);
A84: t . (dl. 1) = i2 by A22, B80;
A85: ( t is 0 -started & t . (dl. 0) = i1 ) by A35, A22, B80, MEMSTR_0:17;
per cases ( i1 > i2 or i1 = i2 or i1 < i2 ) by XXREAL_0:1;
suppose A86: i1 = i2 ; :: thesis: P halts_on t
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:2;
then (Comput (P,t,4)) . (dl. 1) = (t . (dl. 0)) mod (t . (dl. 1)) by A7, A8, A81, A85, A84, A88, Lm5;
then IC (Comput (P,t,4)) = 4 by A7, A8, A81, A85, A84, A87, A88, Lm4;
then P halts_at IC (Comput (P,t,4)) by A81, Lm3;
hence P halts_on t by EXTPRO_1:16; :: thesis: verum
end;
suppose A89: i1 < i2 ; :: thesis: P halts_on t
A90: Comput (P,t,4) = Comput (P,t,(4 * (0 + 1))) ;
A92: t = Comput (P,t,(4 * 0)) by EXTPRO_1:2;
i1 mod i2 = i19 mod i29
.= i19 by A89, NAT_D:24 ;
then A93: (Comput (P,t,4)) . (dl. 1) = i1 by A7, A8, A81, A85, A84, A92, A90, Lm5;
then IC (Comput (P,t,4)) = 0 by A7, A8, A81, A85, A84, A90, Lm4;
then A94: Comput (P,t,4) is 0 -started by MEMSTR_0:def 9;
(Comput (P,t,4)) . (dl. 0) = i2 by A7, A8, A81, 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, A81, Lm6;
P halts_at IC (Comput (P,t,(k0 + 4))) by A95, EXTPRO_1:4;
hence P halts_on t by EXTPRO_1:16; :: thesis: verum
end;
end;
end;
thus (Start-At (0,SCM)) +* d is Autonomy of Euclide-Algorithm by A38, A79, EXTPRO_1:def 12; :: thesis: Euclide-Function . d c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* d))
then A98: Result (Euclide-Algorithm,((Start-At (0,SCM)) +* d)) = (Result (T,t)) | (dom ((Start-At (0,SCM)) +* d)) by C10, A10, EXTPRO_1:def 13;
dl. 0 in the carrier of SCM ;
then A99: dl. 0 in dom (Result (T,t)) by PARTFUN1:def 2;
A101: d . (dl. 0) = i1 by A9, AMI_3:10, FUNCT_4:63;
A102: d . (dl. 1) = i2 by A9, FUNCT_4:63;
A103: d c= (Start-At (0,SCM)) +* d by FUNCT_4:25;
A104: dom d c= dom ((Start-At (0,SCM)) +* d) by A103, RELAT_1:11;
A105: d c= t by A103, A10, XBOOLE_1:1;
A106: dom d = {(dl. 0),(dl. 1)} by A9, FUNCT_4:62;
then BB: dl. 1 in dom d by TARSKI:def 2;
A107: t . (dl. 1) = i2 by A105, A102, BB, GRFUNC_1:2;
AA: dl. 0 in dom d by A106, TARSKI:def 2;
t . (dl. 0) = i1 by A105, A101, AA, GRFUNC_1:2;
then A109: (Result (T,t)) . (dl. 0) = i1 gcd i2 by A7, A8, A36, A107, Th10, C10;
A111: dom ((dl. 0) .--> (i1 gcd i2)) = {(dl. 0)} by FUNCOP_1:13;
dom ((dl. 0) .--> (i1 gcd i2)) c= dom d by A106, A111, ZFMISC_1:7;
then A112: dom ((dl. 0) .--> (i1 gcd i2)) c= dom ((Start-At (0,SCM)) +* d) by A104, XBOOLE_1:1;
(dl. 0) .--> (i1 gcd i2) c= (Result (T,t)) | (dom ((Start-At (0,SCM)) +* d)) by A112, A99, A109, FUNCT_4:85, RELAT_1:151;
hence Euclide-Function . d c= Result (Euclide-Algorithm,((Start-At (0,SCM)) +* d)) by A98, A7, A8, A9, Th12; :: thesis: verum