let p be FinPartState of SCMPDS; :: thesis: for x, y being Integer st y >= 0 & x >= y & p = ((intpos 9),(intpos 10)) --> (x,y) holds
Initialize p is GCD-Algorithm -autonomic
let x, y be Integer; :: thesis: ( y >= 0 & x >= y & p = ((intpos 9),(intpos 10)) --> (x,y) implies Initialize p is GCD-Algorithm -autonomic )
set GA = GCD-Algorithm ;
set a = intpos 9;
set b = intpos 10;
assume that
A1: y >= 0 and
A2: x >= y and
A3: p = ((intpos 9),(intpos 10)) --> (x,y) ; :: thesis: Initialize p is GCD-Algorithm -autonomic
A4: dom p = {(intpos 9),(intpos 10)} by A3, FUNCT_4:62;
( intpos 9 in SCM-Data-Loc & intpos 10 in SCM-Data-Loc ) by AMI_2:def 16;
then ( intpos 9 in Data-Locations & intpos 10 in Data-Locations ) by SCMPDS_2:84;
then A5: dom p c= Data-Locations by A4, ZFMISC_1:32;
not IC in Data-Locations by STRUCT_0:3;
then {(IC )} misses Data-Locations by ZFMISC_1:50;
then Data-Locations misses {(IC )} ;
then dom p misses {(IC )} by A5, XBOOLE_1:63;
then A6: p is data-only ;
intpos 9 in dom p by A4, TARSKI:def 2;
then A7: intpos 9 in dom p ;
intpos 10 in dom p by A4, TARSKI:def 2;
then A8: intpos 10 in dom p ;
A9: dom (Start-At (0,SCMPDS)) = {(IC )} by FUNCOP_1:13;
A10: for t being State of SCMPDS st Initialize p c= t holds
( t . (intpos 9) = x & t . (intpos 10) = y )
proof
let t be State of SCMPDS; :: thesis: ( Initialize p c= t implies ( t . (intpos 9) = x & t . (intpos 10) = y ) )
assume A11: Initialize p c= t ; :: thesis: ( t . (intpos 9) = x & t . (intpos 10) = y )
p = DataPart p by A6, MEMSTR_0:7;
then dom p misses dom (Start-At (0,SCMPDS)) by A9, MEMSTR_0:4;
then p c= Initialize p by FUNCT_4:32;
then p c= Initialize p ;
then A12: p c= t by A11, XBOOLE_1:1;
hence t . (intpos 9) = p . (intpos 9) by A7, GRFUNC_1:2
.= p . (intpos 9)
.= x by A3, AMI_3:10, FUNCT_4:63 ;
:: thesis: t . (intpos 10) = y
thus t . (intpos 10) = p . (intpos 10) by A12, A8, GRFUNC_1:2
.= p . (intpos 10)
.= y by A3, FUNCT_4:63 ; :: thesis: verum
end;
let P1, P2 be Instruction-Sequence of SCMPDS; :: according to EXTPRO_1:def 10 :: thesis: ( not GCD-Algorithm c= P1 or not GCD-Algorithm c= P2 or for b1, b2 being set holds
( not Initialize p c= b1 or not Initialize p c= b2 or for b3 being set holds (Comput (P1,b1,b3)) | (dom (Initialize p)) = (Comput (P2,b2,b3)) | (dom (Initialize p)) ) )
assume A13: ( GCD-Algorithm c= P1 & GCD-Algorithm c= P2 ) ; :: thesis: for b1, b2 being set holds
( not Initialize p c= b1 or not Initialize p c= b2 or for b3 being set holds (Comput (P1,b1,b3)) | (dom (Initialize p)) = (Comput (P2,b2,b3)) | (dom (Initialize p)) )
let s1, s2 be State of SCMPDS; :: thesis: ( not Initialize p c= s1 or not Initialize p c= s2 or for b1 being set holds (Comput (P1,s1,b1)) | (dom (Initialize p)) = (Comput (P2,s2,b1)) | (dom (Initialize p)) )
assume that
A14: Initialize p c= s1 and
A15: Initialize p c= s2 ; :: thesis: for b1 being set holds (Comput (P1,s1,b1)) | (dom (Initialize p)) = (Comput (P2,s2,b1)) | (dom (Initialize p))
Initialize p c= s1 by A14;
then A16: Start-At (0,SCMPDS) c= s1 by MEMSTR_0:50;
then A17: s1 is 0 -started by MEMSTR_0:29;
A18: GCD-Algorithm c= P1 by A13;
Initialize p c= s2 by A15;
then A19: Start-At (0,SCMPDS) c= s2 by MEMSTR_0:50;
then A20: s2 is 0 -started by MEMSTR_0:29;
A21: GCD-Algorithm c= P2 by A13;
A22: s1 . (intpos 9) = x by A10, A14;
A23: s1 . (intpos 10) = y by A10, A14;
A24: s2 . (intpos 9) = x by A10, A15;
A25: s2 . (intpos 10) = y by A10, A15;
set s4 = Comput (P1,s1,4);
set t4 = Comput (P2,s2,4);
A26: IC (Comput (P1,s1,4)) = 5 by Th11, A18, A17;
A27: (Comput (P1,s1,4)) . GBP = 0 by Th11, A18, A17;
A28: (Comput (P1,s1,4)) . SBP = 7 by Th11, A18, A17;
A29: (Comput (P1,s1,4)) . (intpos (7 + RetIC)) = 2 by Th11, A18, A17;
A30: (Comput (P1,s1,4)) . (intpos 9) = s1 . (intpos 9) by Th11, A18, A17;
A31: (Comput (P1,s1,4)) . (intpos 10) = s1 . (intpos 10) by Th11, A18, A17;
A32: (Comput (P1,s1,4)) . (DataLoc (((Comput (P1,s1,4)) . SBP),3)) = (Comput (P1,s1,4)) . (intpos (7 + 3)) by A28, Th1
.= y by A10, A14, A31 ;
A33: DataLoc (((Comput (P1,s1,4)) . SBP),2) = intpos (7 + 2) by A28, Th1;
A34: IC (Comput (P2,s2,4)) = 5 by Th11, A21, A20;
A35: (Comput (P2,s2,4)) . GBP = 0 by Th11, A21, A20;
A36: (Comput (P2,s2,4)) . SBP = 7 by Th11, A21, A20;
A37: (Comput (P2,s2,4)) . (intpos (7 + RetIC)) = 2 by Th11, A21, A20;
A38: (Comput (P2,s2,4)) . (intpos 9) = s2 . (intpos 9) by Th11, A21, A20;
A39: (Comput (P2,s2,4)) . (intpos 10) = s2 . (intpos 10) by Th11, A21, A20;
(Comput (P2,s2,4)) . (DataLoc (((Comput (P2,s2,4)) . SBP),3)) = (Comput (P2,s2,4)) . (intpos (7 + 3)) by A36, Th1
.= (Comput (P1,s1,4)) . (DataLoc (((Comput (P1,s1,4)) . SBP),3)) by A10, A15, A32, A39 ;
then consider n being Nat such that
A40: CurInstr (P1,(Comput (P1,(Comput (P1,s1,4)),n))) = return SBP and
A41: (Comput (P1,s1,4)) . SBP = (Comput (P1,(Comput (P1,s1,4)),n)) . SBP and
A42: CurInstr (P2,(Comput (P2,(Comput (P2,s2,4)),n))) = return SBP and
A43: (Comput (P2,s2,4)) . SBP = (Comput (P2,(Comput (P2,s2,4)),n)) . SBP and
A44: for j being Nat st 1 < j & j <= ((Comput (P1,s1,4)) . SBP) + 1 holds
( (Comput (P1,s1,4)) . (intpos j) = (Comput (P1,(Comput (P1,s1,4)),n)) . (intpos j) & (Comput (P2,s2,4)) . (intpos j) = (Comput (P2,(Comput (P2,s2,4)),n)) . (intpos j) ) and
A45: for k being Nat
for c being Int_position st k <= n & (Comput (P1,s1,4)) . c = (Comput (P2,s2,4)) . c holds
( IC (Comput (P1,(Comput (P1,s1,4)),k)) = IC (Comput (P2,(Comput (P2,s2,4)),k)) & (Comput (P1,(Comput (P1,s1,4)),k)) . c = (Comput (P2,(Comput (P2,s2,4)),k)) . c ) by A1, A2, A10, A15, A22, A26, A27, A28, A30, A32, A33, A34, A35, A36, A38, Lm8, A18, A21;
A46: (Comput (P1,(Comput (P1,s1,4)),n)) . (DataLoc (((Comput (P1,(Comput (P1,s1,4)),n)) . SBP),RetIC)) = (Comput (P1,(Comput (P1,s1,4)),n)) . (intpos (7 + 1)) by A28, A41, Th1, SCMPDS_I:def 14
.= 2 by A28, A29, A44, SCMPDS_I:def 14 ;
A47: (Comput (P2,(Comput (P2,s2,4)),n)) . (DataLoc (((Comput (P2,(Comput (P2,s2,4)),n)) . SBP),RetIC)) = (Comput (P2,(Comput (P2,s2,4)),n)) . (intpos (7 + 1)) by A36, A43, Th1, SCMPDS_I:def 14
.= 2 by A28, A37, A44, SCMPDS_I:def 14 ;
A48: P1 /. (IC (Comput (P1,(Comput (P1,s1,4)),(n + 1)))) = P1 . (IC (Comput (P1,(Comput (P1,s1,4)),(n + 1)))) by PBOOLE:143;
A49: Comput (P1,(Comput (P1,s1,4)),(n + 1)) = Following (P1,(Comput (P1,(Comput (P1,s1,4)),n))) by EXTPRO_1:3
.= Exec ((return SBP),(Comput (P1,(Comput (P1,s1,4)),n))) by A40 ;
then A50: IC (Comput (P1,(Comput (P1,s1,4)),(n + 1))) = |.((Comput (P1,(Comput (P1,s1,4)),n)) . (DataLoc (((Comput (P1,(Comput (P1,s1,4)),n)) . SBP),RetIC))).| + 2 by SCMPDS_2:58
.= 2 + 2 by A46, ABSVALUE:29 ;
then A51: CurInstr (P1,(Comput (P1,(Comput (P1,s1,4)),(n + 1)))) = P1 . 4 by A48
.= P1 . 4
.= halt SCMPDS by Lm1, A18 ;
A52: P2 /. (IC (Comput (P2,(Comput (P2,s2,4)),(n + 1)))) = P2 . (IC (Comput (P2,(Comput (P2,s2,4)),(n + 1)))) by PBOOLE:143;
A53: Comput (P2,(Comput (P2,s2,4)),(n + 1)) = Following (P2,(Comput (P2,(Comput (P2,s2,4)),n))) by EXTPRO_1:3
.= Exec ((return SBP),(Comput (P2,(Comput (P2,s2,4)),n))) by A42 ;
then A54: IC (Comput (P2,(Comput (P2,s2,4)),(n + 1))) = |.((Comput (P2,(Comput (P2,s2,4)),n)) . (DataLoc (((Comput (P2,(Comput (P2,s2,4)),n)) . SBP),RetIC))).| + 2 by SCMPDS_2:58
.= 2 + 2 by A47, ABSVALUE:29 ;
then A55: CurInstr (P2,(Comput (P2,(Comput (P2,s2,4)),(n + 1)))) = P2 . 4 by A52
.= P2 . 4
.= halt SCMPDS by Lm1, A21 ;
A56: (Comput (P1,s1,4)) . (intpos 9) = (Comput (P2,s2,4)) . (intpos 9) by A19, A22, A24, Lm9, A18, A16, A21;
A57: (Comput (P1,s1,4)) . (intpos 10) = (Comput (P2,s2,4)) . (intpos 10) by A19, A23, A25, Lm9, A18, A16, A21;
A58: (Comput (P1,(Comput (P1,s1,4)),(n + 1))) . (intpos 9) = (Comput (P1,(Comput (P1,s1,4)),n)) . (intpos 9) by A49, AMI_3:10, SCMPDS_2:58
.= (Comput (P2,(Comput (P2,s2,4)),n)) . (intpos 9) by A45, A56
.= (Comput (P2,(Comput (P2,s2,4)),(n + 1))) . (intpos 9) by A53, AMI_3:10, SCMPDS_2:58 ;
A59: (Comput (P1,(Comput (P1,s1,4)),(n + 1))) . (intpos 10) = (Comput (P1,(Comput (P1,s1,4)),n)) . (intpos 10) by A49, AMI_3:10, SCMPDS_2:58
.= (Comput (P2,(Comput (P2,s2,4)),n)) . (intpos 10) by A45, A57
.= (Comput (P2,(Comput (P2,s2,4)),(n + 1))) . (intpos 10) by A53, AMI_3:10, SCMPDS_2:58 ;
A60: now :: thesis: for j being Nat holds
( IC (Comput (P1,s1,j)) = IC (Comput (P2,s2,j)) & (Comput (P1,s1,j)) . (intpos 9) = (Comput (P2,s2,j)) . (intpos 9) & (Comput (P1,s1,j)) . (intpos 10) = (Comput (P2,s2,j)) . (intpos 10) )
let j be Nat; :: thesis: ( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . (intpos 9) = (Comput (P2,s2,b1)) . (intpos 9) & (Comput (P1,s1,b1)) . (intpos 10) = (Comput (P2,s2,b1)) . (intpos 10) )
A61: ( j < (n + 4) + 1 or j >= n + 5 ) ;
A62: now :: thesis: ( not j <= n + 4 or ( j <= 3 & j <= 3 ) or ( j >= 4 & j >= 4 & j <= n + 4 ) )
assume A63: j <= n + 4 ; :: thesis: ( ( j <= 3 & j <= 3 ) or ( j >= 4 & j >= 4 & j <= n + 4 ) )
A64: ( j < 3 + 1 or j >= 4 ) ;
per cases ( j <= 3 or j >= 4 ) by A64, NAT_1:13;
case j <= 3 ; :: thesis: j <= 3
hence j <= 3 ; :: thesis: verum
end;
case j >= 4 ; :: thesis: ( j >= 4 & j <= n + 4 )
hence ( j >= 4 & j <= n + 4 ) by A63; :: thesis: verum
end;
end;
end;
per cases ( j <= 3 or ( j >= 4 & j <= n + 4 ) or j >= n + 5 ) by A61, A62, NAT_1:13;
suppose j <= 3 ; :: thesis: ( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . (intpos 9) = (Comput (P2,s2,b1)) . (intpos 9) & (Comput (P1,s1,b1)) . (intpos 10) = (Comput (P2,s2,b1)) . (intpos 10) )
then A65: j <= 4 by XXREAL_0:2;
hence IC (Comput (P1,s1,j)) = IC (Comput (P2,s2,j)) by A19, A22, A24, Lm9, A18, A16, A21; :: thesis: ( (Comput (P1,s1,j)) . (intpos 9) = (Comput (P2,s2,j)) . (intpos 9) & (Comput (P1,s1,j)) . (intpos 10) = (Comput (P2,s2,j)) . (intpos 10) )
thus (Comput (P1,s1,j)) . (intpos 9) = (Comput (P2,s2,j)) . (intpos 9) by A19, A22, A24, A65, Lm9, A18, A16, A21; :: thesis: (Comput (P1,s1,j)) . (intpos 10) = (Comput (P2,s2,j)) . (intpos 10)
thus (Comput (P1,s1,j)) . (intpos 10) = (Comput (P2,s2,j)) . (intpos 10) by A19, A23, A25, A65, Lm9, A18, A16, A21; :: thesis: verum
end;
suppose A66: ( j >= 4 & j <= n + 4 ) ; :: thesis: ( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . (intpos 9) = (Comput (P2,s2,b1)) . (intpos 9) & (Comput (P1,s1,b1)) . (intpos 10) = (Comput (P2,s2,b1)) . (intpos 10) )
then consider j1 being Nat such that
A67: j = 4 + j1 by NAT_1:10;
reconsider j1 = j1 as Nat ;
A68: j1 <= n by A66, A67, XREAL_1:6;
thus IC (Comput (P1,s1,j)) = IC (Comput (P1,(Comput (P1,s1,4)),j1)) by A67, EXTPRO_1:4
.= IC (Comput (P2,(Comput (P2,s2,4)),j1)) by A45, A56, A68
.= IC (Comput (P2,s2,j)) by A67, EXTPRO_1:4 ; :: thesis: ( (Comput (P1,s1,j)) . (intpos 9) = (Comput (P2,s2,j)) . (intpos 9) & (Comput (P1,s1,j)) . (intpos 10) = (Comput (P2,s2,j)) . (intpos 10) )
thus (Comput (P1,s1,j)) . (intpos 9) = (Comput (P1,(Comput (P1,s1,4)),j1)) . (intpos 9) by A67, EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,4)),j1)) . (intpos 9) by A45, A56, A68
.= (Comput (P2,s2,j)) . (intpos 9) by A67, EXTPRO_1:4 ; :: thesis: (Comput (P1,s1,j)) . (intpos 10) = (Comput (P2,s2,j)) . (intpos 10)
thus (Comput (P1,s1,j)) . (intpos 10) = (Comput (P1,(Comput (P1,s1,4)),j1)) . (intpos 10) by A67, EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,4)),j1)) . (intpos 10) by A45, A57, A68
.= (Comput (P2,s2,j)) . (intpos 10) by A67, EXTPRO_1:4 ; :: thesis: verum
end;
suppose j >= n + 5 ; :: thesis: ( IC (Comput (P1,s1,b1)) = IC (Comput (P2,s2,b1)) & (Comput (P1,s1,b1)) . (intpos 9) = (Comput (P2,s2,b1)) . (intpos 9) & (Comput (P1,s1,b1)) . (intpos 10) = (Comput (P2,s2,b1)) . (intpos 10) )
then consider j1 being Nat such that
A69: j = (n + (1 + 4)) + j1 by NAT_1:10;
reconsider j1 = j1 as Nat ;
A70: j = ((n + 1) + j1) + 4 by A69;
hence IC (Comput (P1,s1,j)) = IC (Comput (P1,(Comput (P1,s1,4)),((n + 1) + j1))) by EXTPRO_1:4
.= IC (Comput (P2,(Comput (P2,s2,4)),(n + 1))) by A50, A51, A54, EXTPRO_1:5, NAT_1:11
.= IC (Comput (P2,(Comput (P2,s2,4)),((n + 1) + j1))) by A55, EXTPRO_1:5, NAT_1:11
.= IC (Comput (P2,s2,j)) by A70, EXTPRO_1:4 ;
:: thesis: ( (Comput (P1,s1,j)) . (intpos 9) = (Comput (P2,s2,j)) . (intpos 9) & (Comput (P1,s1,j)) . (intpos 10) = (Comput (P2,s2,j)) . (intpos 10) )
thus (Comput (P1,s1,j)) . (intpos 9) = (Comput (P1,(Comput (P1,s1,4)),((n + 1) + j1))) . (intpos 9) by A70, EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,4)),(n + 1))) . (intpos 9) by A51, A58, EXTPRO_1:5, NAT_1:11
.= (Comput (P2,(Comput (P2,s2,4)),((n + 1) + j1))) . (intpos 9) by A55, EXTPRO_1:5, NAT_1:11
.= (Comput (P2,s2,j)) . (intpos 9) by A70, EXTPRO_1:4 ; :: thesis: (Comput (P1,s1,j)) . (intpos 10) = (Comput (P2,s2,j)) . (intpos 10)
thus (Comput (P1,s1,j)) . (intpos 10) = (Comput (P1,(Comput (P1,s1,4)),((n + 1) + j1))) . (intpos 10) by A70, EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,4)),(n + 1))) . (intpos 10) by A51, A59, EXTPRO_1:5, NAT_1:11
.= (Comput (P2,(Comput (P2,s2,4)),((n + 1) + j1))) . (intpos 10) by A55, EXTPRO_1:5, NAT_1:11
.= (Comput (P2,s2,j)) . (intpos 10) by A70, EXTPRO_1:4 ; :: thesis: verum
end;
end;
end;
set A = {(IC ),(intpos 9),(intpos 10)};
A71: IC in dom (Initialize p) by MEMSTR_0:48;
dom (DataPart (Initialize p)) = dom (DataPart p) by MEMSTR_0:45
.= dom (DataPart p)
.= {(intpos 9),(intpos 10)} by A6, A4, MEMSTR_0:7 ;
then A72: dom (Initialize p) = {(IC )} \/ {(intpos 9),(intpos 10)} by A71, MEMSTR_0:24
.= {(IC ),(intpos 9),(intpos 10)} by ENUMSET1:2 ;
let k be Nat; :: thesis: (Comput (P1,s1,k)) | (dom (Initialize p)) = (Comput (P2,s2,k)) | (dom (Initialize p))
A73: (Comput (P1,s1,k)) . (IC ) = IC (Comput (P1,s1,k))
.= IC (Comput (P2,s2,k)) by A60
.= (Comput (P2,s2,k)) . (IC ) ;
A74: (Comput (P1,s1,k)) . (intpos 9) = (Comput (P2,s2,k)) . (intpos 9) by A60;
A75: (Comput (P1,s1,k)) . (intpos 10) = (Comput (P2,s2,k)) . (intpos 10) by A60;
dom (Comput (P1,s1,k)) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (Comput (P2,s2,k)) by PARTFUN1:def 2 ;
then (Comput (P1,s1,k)) | {(IC ),(intpos 9),(intpos 10)} = (Comput (P2,s2,k)) | {(IC ),(intpos 9),(intpos 10)} by A73, A74, A75, GRFUNC_1:31;
hence (Comput (P1,s1,k)) | (dom (Initialize p)) = (Comput (P2,s2,k)) | (dom (Initialize p)) by A72; :: thesis: verum