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 SCMPDS_2:def 2;
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 A7: p is data-only by MEMSTR_0:def 6;
intpos 9 in dom p by A4, TARSKI:def 2;
then B12: intpos 9 in dom p ;
intpos 10 in dom p by A4, TARSKI:def 2;
then B13: intpos 10 in dom p ;
I2: dom (Start-At (0,SCMPDS)) = {(IC )} by FUNCOP_1:13;
A14: 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 A15: Initialize p c= t ; :: thesis: ( t . (intpos 9) = x & t . (intpos 10) = y )
p = DataPart p by A7, MEMSTR_0:7;
then dom p misses dom (Start-At (0,SCMPDS)) by I2, MEMSTR_0:4;
then p c= Initialize p by FUNCT_4:32;
then p c= Initialize p ;
then A16: p c= t by A15, XBOOLE_1:1;
hence t . (intpos 9) = p . (intpos 9) by B12, 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 A16, B13, 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 b₁, b₂ being set holds
( not Initialize p c= b₁ or not Initialize p c= b₂ or for b₃ being Element of NAT holds (Comput (P1,b₁,b₃)) | (proj1 (Initialize p)) = (Comput (P2,b₂,b₃)) | (proj1 (Initialize p)) ) )
assume A17: ( GCD-Algorithm c= P1 & GCD-Algorithm c= P2 ) ; :: thesis: for b₁, b₂ being set holds
( not Initialize p c= b₁ or not Initialize p c= b₂ or for b₃ being Element of NAT holds (Comput (P1,b₁,b₃)) | (proj1 (Initialize p)) = (Comput (P2,b₂,b₃)) | (proj1 (Initialize p)) )
let s1, s2 be State of SCMPDS; :: thesis: ( not Initialize p c= s1 or not Initialize p c= s2 or for b₁ being Element of NAT holds (Comput (P1,s1,b₁)) | (proj1 (Initialize p)) = (Comput (P2,s2,b₁)) | (proj1 (Initialize p)) )
assume that
A18: Initialize p c= s1 and
A19: Initialize p c= s2 ; :: thesis: for b₁ being Element of NAT holds (Comput (P1,s1,b₁)) | (proj1 (Initialize p)) = (Comput (P2,s2,b₁)) | (proj1 (Initialize p))
Initialize p c= s1 by A18;
then B20: Start-At (0,SCMPDS) c= s1 by MEMSTR_0:50;
then C20: s1 is 0 -started by MEMSTR_0:29;
A23: GCD-Algorithm c= P1 by A17;
Initialize p c= s2 by A19;
then B24: Start-At (0,SCMPDS) c= s2 by MEMSTR_0:50;
then C24: s2 is 0 -started by MEMSTR_0:29;
A26: GCD-Algorithm c= P2 by A17;
A27: s1 . (intpos 9) = x by A14, A18;
A28: s1 . (intpos 10) = y by A14, A18;
A29: s2 . (intpos 9) = x by A14, A19;
A30: s2 . (intpos 10) = y by A14, A19;
set s4 = Comput (P1,s1,4);
set t4 = Comput (P2,s2,4);
A32: IC (Comput (P1,s1,4)) = 5 by Th15, A23, C20;
A33: (Comput (P1,s1,4)) . GBP = 0 by Th15, A23, C20;
A34: (Comput (P1,s1,4)) . SBP = 7 by Th15, A23, C20;
A35: (Comput (P1,s1,4)) . (intpos (7 + RetIC)) = 2 by Th15, A23, C20;
A36: (Comput (P1,s1,4)) . (intpos 9) = s1 . (intpos 9) by Th15, A23, C20;
A37: (Comput (P1,s1,4)) . (intpos 10) = s1 . (intpos 10) by Th15, A23, C20;
A38: (Comput (P1,s1,4)) . (DataLoc (((Comput (P1,s1,4)) . SBP),3)) = (Comput (P1,s1,4)) . (intpos (7 + 3)) by A34, Th5
.= y by A14, A18, A37 ;
A39: DataLoc (((Comput (P1,s1,4)) . SBP),2) = intpos (7 + 2) by A34, Th5;
A41: IC (Comput (P2,s2,4)) = 5 by Th15, A26, C24;
A42: (Comput (P2,s2,4)) . GBP = 0 by Th15, A26, C24;
A43: (Comput (P2,s2,4)) . SBP = 7 by Th15, A26, C24;
A44: (Comput (P2,s2,4)) . (intpos (7 + RetIC)) = 2 by Th15, A26, C24;
A45: (Comput (P2,s2,4)) . (intpos 9) = s2 . (intpos 9) by Th15, A26, C24;
A46: (Comput (P2,s2,4)) . (intpos 10) = s2 . (intpos 10) by Th15, A26, C24;
(Comput (P2,s2,4)) . (DataLoc (((Comput (P2,s2,4)) . SBP),3)) = (Comput (P2,s2,4)) . (intpos (7 + 3)) by A43, Th5
.= (Comput (P1,s1,4)) . (DataLoc (((Comput (P1,s1,4)) . SBP),3)) by A14, A19, A38, A46 ;
then consider n being Element of NAT such that
A47: CurInstr (P1,(Comput (P1,(Comput (P1,s1,4)),n))) = return SBP and
A48: (Comput (P1,s1,4)) . SBP = (Comput (P1,(Comput (P1,s1,4)),n)) . SBP and
A49: CurInstr (P2,(Comput (P2,(Comput (P2,s2,4)),n))) = return SBP and
A50: (Comput (P2,s2,4)) . SBP = (Comput (P2,(Comput (P2,s2,4)),n)) . SBP and
A51: for j being Element of 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
A52: for k being Element of 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, A14, A19, A27, A32, A33, A34, A36, A38, A39, A41, A42, A43, A45, Lm8, A23, A26;
A53: (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 A34, A48, Th5, SCMPDS_1:def 21
.= 2 by A34, A35, A51, SCMPDS_1:def 21 ;
A54: (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 A43, A50, Th5, SCMPDS_1:def 21
.= 2 by A34, A44, A51, SCMPDS_1:def 21 ;
A55: P1 /. (IC (Comput (P1,(Comput (P1,s1,4)),(n + 1)))) = P1 . (IC (Comput (P1,(Comput (P1,s1,4)),(n + 1)))) by PBOOLE:143;
A57: 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 A47 ;
then A58: IC (Comput (P1,(Comput (P1,s1,4)),(n + 1))) = (abs ((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 A53, ABSVALUE:29 ;
then A59: CurInstr (P1,(Comput (P1,(Comput (P1,s1,4)),(n + 1)))) = P1 . 4 by A55
.= P1 . 4
.= halt SCMPDS by Lm1, A23 ;
A61: P2 /. (IC (Comput (P2,(Comput (P2,s2,4)),(n + 1)))) = P2 . (IC (Comput (P2,(Comput (P2,s2,4)),(n + 1)))) by PBOOLE:143;
A63: 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 A49 ;
then A64: IC (Comput (P2,(Comput (P2,s2,4)),(n + 1))) = (abs ((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 A54, ABSVALUE:29 ;
then A65: CurInstr (P2,(Comput (P2,(Comput (P2,s2,4)),(n + 1)))) = P2 . 4 by A61
.= P2 . 4
.= halt SCMPDS by Lm1, A26 ;
A68: (Comput (P1,s1,4)) . (intpos 9) = (Comput (P2,s2,4)) . (intpos 9) by B24, A27, A29, Lm9, A23, B20, A26;
A69: (Comput (P1,s1,4)) . (intpos 10) = (Comput (P2,s2,4)) . (intpos 10) by B24, A28, A30, Lm9, A23, B20, A26;
A70: (Comput (P1,(Comput (P1,s1,4)),(n + 1))) . (intpos 9) = (Comput (P1,(Comput (P1,s1,4)),n)) . (intpos 9) by A57, AMI_3:10, SCMPDS_2:58
.= (Comput (P2,(Comput (P2,s2,4)),n)) . (intpos 9) by A52, A68
.= (Comput (P2,(Comput (P2,s2,4)),(n + 1))) . (intpos 9) by A63, AMI_3:10, SCMPDS_2:58 ;
A71: (Comput (P1,(Comput (P1,s1,4)),(n + 1))) . (intpos 10) = (Comput (P1,(Comput (P1,s1,4)),n)) . (intpos 10) by A57, AMI_3:10, SCMPDS_2:58
.= (Comput (P2,(Comput (P2,s2,4)),n)) . (intpos 10) by A52, A69
.= (Comput (P2,(Comput (P2,s2,4)),(n + 1))) . (intpos 10) by A63, AMI_3:10, SCMPDS_2:58 ;

A72: now

let j be Element of NAT ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . (intpos 9) = (Comput (P2,s2,b₁)) . (intpos 9) & (Comput (P1,s1,b₁)) . (intpos 10) = (Comput (P2,s2,b₁)) . (intpos 10) )
A73: ( j < (n + 4) + 1 or j >= n + 5 ) ;

A74: now

assume A75: j <= n + 4 ; :: thesis: ( ( j <= 3 & j <= 3 ) or ( j >= 4 & j >= 4 & j <= n + 4 ) )
A76: ( j < 3 + 1 or j >= 4 ) ;

per cases ( j <= 3 or j >= 4 ) by A76, 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 A75; :: thesis: verum

end;

end;

end;

per cases ( j <= 3 or ( j >= 4 & j <= n + 4 ) or j >= n + 5 ) by A73, A74, NAT_1:13;

suppose j <= 3 ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . (intpos 9) = (Comput (P2,s2,b₁)) . (intpos 9) & (Comput (P1,s1,b₁)) . (intpos 10) = (Comput (P2,s2,b₁)) . (intpos 10) )

then A77: j <= 4 by XXREAL_0:2;
hence IC (Comput (P1,s1,j)) = IC (Comput (P2,s2,j)) by B24, A27, A29, Lm9, A23, B20, A26; :: 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 B24, A27, A29, A77, Lm9, A23, B20, A26; :: 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 B24, A28, A30, A77, Lm9, A23, B20, A26; :: thesis: verum

end;

suppose A78: ( j >= 4 & j <= n + 4 ) ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . (intpos 9) = (Comput (P2,s2,b₁)) . (intpos 9) & (Comput (P1,s1,b₁)) . (intpos 10) = (Comput (P2,s2,b₁)) . (intpos 10) )

then consider j1 being Nat such that
A79: j = 4 + j1 by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 12;
A82: j1 <= n by A78, A79, XREAL_1:6;
thus IC (Comput (P1,s1,j)) = IC (Comput (P1,(Comput (P1,s1,4)),j1)) by A79, EXTPRO_1:4
.= IC (Comput (P2,(Comput (P2,s2,4)),j1)) by A52, A68, A82
.= IC (Comput (P2,s2,j)) by A79, 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 A79, EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,4)),j1)) . (intpos 9) by A52, A68, A82
.= (Comput (P2,s2,j)) . (intpos 9) by A79, 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 A79, EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,4)),j1)) . (intpos 10) by A52, A69, A82
.= (Comput (P2,s2,j)) . (intpos 10) by A79, EXTPRO_1:4 ; :: thesis: verum

end;

suppose j >= n + 5 ; :: thesis: ( IC (Comput (P1,s1,b₁)) = IC (Comput (P2,s2,b₁)) & (Comput (P1,s1,b₁)) . (intpos 9) = (Comput (P2,s2,b₁)) . (intpos 9) & (Comput (P1,s1,b₁)) . (intpos 10) = (Comput (P2,s2,b₁)) . (intpos 10) )

then consider j1 being Nat such that
A83: j = (n + (1 + 4)) + j1 by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 12;
A86: j = ((n + 1) + j1) + 4 by A83;
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 A58, A59, A64, EXTPRO_1:5, NAT_1:11
.= IC (Comput (P2,(Comput (P2,s2,4)),((n + 1) + j1))) by A65, EXTPRO_1:5, NAT_1:11
.= IC (Comput (P2,s2,j)) by A86, 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 A86, EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,4)),(n + 1))) . (intpos 9) by A59, A70, EXTPRO_1:5, NAT_1:11
.= (Comput (P2,(Comput (P2,s2,4)),((n + 1) + j1))) . (intpos 9) by A65, EXTPRO_1:5, NAT_1:11
.= (Comput (P2,s2,j)) . (intpos 9) by A86, 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 A86, EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,4)),(n + 1))) . (intpos 10) by A59, A71, EXTPRO_1:5, NAT_1:11
.= (Comput (P2,(Comput (P2,s2,4)),((n + 1) + j1))) . (intpos 10) by A65, EXTPRO_1:5, NAT_1:11
.= (Comput (P2,s2,j)) . (intpos 10) by A86, EXTPRO_1:4 ; :: thesis: verum

end;

end;

end;

set A = {(IC ),(intpos 9),(intpos 10)};
A89: 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 A7, A4, MEMSTR_0:7 ;
then A92: dom (Initialize p) = {(IC )} \/ {(intpos 9),(intpos 10)} by A89, MEMSTR_0:24
.= {(IC ),(intpos 9),(intpos 10)} by ENUMSET1:2 ;
let k be Element of NAT ; :: thesis: (Comput (P1,s1,k)) | (proj1 (Initialize p)) = (Comput (P2,s2,k)) | (proj1 (Initialize p))
A95: (Comput (P1,s1,k)) . (IC ) = IC (Comput (P1,s1,k))
.= IC (Comput (P2,s2,k)) by A72
.= (Comput (P2,s2,k)) . (IC ) ;
A96: (Comput (P1,s1,k)) . (intpos 9) = (Comput (P2,s2,k)) . (intpos 9) by A72;
A97: (Comput (P1,s1,k)) . (intpos 10) = (Comput (P2,s2,k)) . (intpos 10) by A72;
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 A95, A96, A97, GRFUNC_1:31;
hence (Comput (P1,s1,k)) | (proj1 (Initialize p)) = (Comput (P2,s2,k)) | (proj1 (Initialize p)) by A92; :: thesis: verum