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 GCD-Algorithm) +* p is autonomic
let x, y be Integer; :: thesis: ( y >= 0 & x >= y & p = ((intpos 9),(intpos 10)) --> (x,y) implies (Initialize GCD-Algorithm) +* p is autonomic )
set GA = GCD-Algorithm ;
set IA = Initialize 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 GCD-Algorithm) +* p is autonomic
A4: dom p = {(intpos 9),(intpos 10)} by A3, FUNCT_4:65;
( intpos 9 in SCM-Data-Loc & intpos 10 in SCM-Data-Loc ) by SCMPDS_2:def 2;
then ( intpos 9 in Data-Locations SCMPDS & intpos 10 in Data-Locations SCMPDS ) by SCMPDS_2:100;
then A5: dom p c= Data-Locations SCMPDS by A4, ZFMISC_1:38;
A6: NAT misses Data-Locations SCMPDS by COMPOS_1:51;
not IC in Data-Locations SCMPDS by COMPOS_1:56;
then {(IC )} misses Data-Locations SCMPDS by ZFMISC_1:56;
then Data-Locations SCMPDS misses {(IC )} \/ NAT by A6, XBOOLE_1:70;
then dom p misses {(IC )} \/ NAT by A5, XBOOLE_1:63;
then A7: p is data-only by COMPOS_1:def 23;
A8: dom (Initialize GCD-Algorithm) = {(IC )} \/ (dom GCD-Algorithm) by COMPOS_1:76;

now

assume dom (Initialize GCD-Algorithm) meets dom p ; :: thesis: contradiction
then consider z being set such that
A9: z in dom (Initialize GCD-Algorithm) and
A10: z in dom p by XBOOLE_0:3;
( z = intpos 9 or z = intpos 10 ) by A4, A10, TARSKI:def 2;
hence contradiction by A9, SCMPDS_4:31; :: thesis: verum

end;

then Initialize GCD-Algorithm c= (Initialize GCD-Algorithm) +* p by FUNCT_4:33;
then B11: NPP (Initialize GCD-Algorithm) c= NPP ((Initialize GCD-Algorithm) +* p) by COMPOS_1:170;
X: intpos 9 in Data-Locations SCMPDS by SCMPDS_2:100, SCMPDS_2:def 2;
Y: intpos 10 in Data-Locations SCMPDS by SCMPDS_2:100, SCMPDS_2:def 2;
intpos 9 in dom p by A4, TARSKI:def 2;
then B12: intpos 9 in dom (NPP p) by X, COMPOS_1:219;
intpos 10 in dom p by A4, TARSKI:def 2;
then B13: intpos 10 in dom (NPP p) by Y, COMPOS_1:219;
A14: for t being State of SCMPDS st NPP ((Initialize GCD-Algorithm) +* p) c= t holds
( t . (intpos 9) = x & t . (intpos 10) = y )

proof

let t be State of SCMPDS; :: thesis: ( NPP ((Initialize GCD-Algorithm) +* p) c= t implies ( t . (intpos 9) = x & t . (intpos 10) = y ) )
assume A15: NPP ((Initialize GCD-Algorithm) +* p) c= t ; :: thesis: ( t . (intpos 9) = x & t . (intpos 10) = y )
p c= (Initialize GCD-Algorithm) +* p by FUNCT_4:26;
then NPP p c= NPP ((Initialize GCD-Algorithm) +* p) by COMPOS_1:170;
then A16: NPP p c= t by A15, XBOOLE_1:1;
hence t . (intpos 9) = (NPP p) . (intpos 9) by B12, GRFUNC_1:8
.= p . (intpos 9) by B12, GRFUNC_1:8
.= x by A3, AMI_3:52, FUNCT_4:66 ;
:: thesis: t . (intpos 10) = y
thus t . (intpos 10) = (NPP p) . (intpos 10) by A16, B13, GRFUNC_1:8
.= p . (intpos 10) by B13, GRFUNC_1:8
.= y by A3, FUNCT_4:66 ; :: thesis: verum

end;

thus (Initialize GCD-Algorithm) +* p is autonomic :: thesis: verum

proof

let P1, P2 be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: according to EXTPRO_1:def 9 :: thesis: ( not ProgramPart ((Initialize GCD-Algorithm) +* p) c= P1 or not ProgramPart ((Initialize GCD-Algorithm) +* p) c= P2 or for b₁, b₂ being set holds
( not NPP ((Initialize GCD-Algorithm) +* p) c= b₁ or not NPP ((Initialize GCD-Algorithm) +* p) c= b₂ or for b₃ being Element of NAT holds (Comput (P1,b₁,b₃)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* p))) = (Comput (P2,b₂,b₃)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* p))) ) )
assume A17: ( ProgramPart ((Initialize GCD-Algorithm) +* p) c= P1 & ProgramPart ((Initialize GCD-Algorithm) +* p) c= P2 ) ; :: thesis: for b₁, b₂ being set holds
( not NPP ((Initialize GCD-Algorithm) +* p) c= b₁ or not NPP ((Initialize GCD-Algorithm) +* p) c= b₂ or for b₃ being Element of NAT holds (Comput (P1,b₁,b₃)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* p))) = (Comput (P2,b₂,b₃)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* p))) )
let s1, s2 be State of SCMPDS; :: thesis: ( not NPP ((Initialize GCD-Algorithm) +* p) c= s1 or not NPP ((Initialize GCD-Algorithm) +* p) c= s2 or for b₁ being Element of NAT holds (Comput (P1,s1,b₁)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* p))) = (Comput (P2,s2,b₁)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* p))) )
assume that
A18: NPP ((Initialize GCD-Algorithm) +* p) c= s1 and
A19: NPP ((Initialize GCD-Algorithm) +* p) c= s2 ; :: thesis: for b₁ being Element of NAT holds (Comput (P1,s1,b₁)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* p))) = (Comput (P2,s2,b₁)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* p)))
NPP (Initialize GCD-Algorithm) c= s1 by A18, B11, XBOOLE_1:1;
then B20: Start-At (0,SCMPDS) c= s1 by COMPOS_1:210;
A22: ProgramPart ((Initialize GCD-Algorithm) +* p) = (ProgramPart (Initialize GCD-Algorithm)) +* (ProgramPart p) by FUNCT_4:75
.= (ProgramPart (Initialize GCD-Algorithm)) +* {} by A7, COMPOS_1:28
.= ProgramPart (Initialize GCD-Algorithm) by FUNCT_4:22
.= (ProgramPart GCD-Algorithm) +* (ProgramPart (Start-At (0,SCMPDS))) by FUNCT_4:75
.= (ProgramPart GCD-Algorithm) +* {} by COMPOS_1:27
.= ProgramPart GCD-Algorithm by FUNCT_4:22
.= GCD-Algorithm by RELAT_1:209 ;
then A23: GCD-Algorithm c= P1 by A17;
NPP (Initialize GCD-Algorithm) c= s2 by A19, B11, XBOOLE_1:1;
then B24: Start-At (0,SCMPDS) c= s2 by COMPOS_1:210;
A26: GCD-Algorithm c= P2 by A17, A22;
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, B20;
A33: (Comput (P1,s1,4)) . GBP = 0 by Th15, A23, B20;
A34: (Comput (P1,s1,4)) . SBP = 7 by Th15, A23, B20;
A35: (Comput (P1,s1,4)) . (intpos (7 + RetIC)) = 2 by Th15, A23, B20;
A36: (Comput (P1,s1,4)) . (intpos 9) = s1 . (intpos 9) by Th15, A23, B20;
A37: (Comput (P1,s1,4)) . (intpos 10) = s1 . (intpos 10) by Th15, A23, B20;
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 B24, Th15, A26;
A42: (Comput (P2,s2,4)) . GBP = 0 by B24, Th15, A26;
A43: (Comput (P2,s2,4)) . SBP = 7 by B24, Th15, A26;
A44: (Comput (P2,s2,4)) . (intpos (7 + RetIC)) = 2 by B24, Th15, A26;
A45: (Comput (P2,s2,4)) . (intpos 9) = s2 . (intpos 9) by B24, Th15, A26;
A46: (Comput (P2,s2,4)) . (intpos 10) = s2 . (intpos 10) by B24, Th15, A26;
(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 23
.= 2 by A34, A35, A51, SCMPDS_1:def 23 ;
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 23
.= 2 by A34, A44, A51, SCMPDS_1:def 23 ;
A55: P1 /. (IC (Comput (P1,(Comput (P1,s1,4)),(n + 1)))) = P1 . (IC (Comput (P1,(Comput (P1,s1,4)),(n + 1)))) by PBOOLE:158;
A57: Comput (P1,(Comput (P1,s1,4)),(n + 1)) = Following (P1,(Comput (P1,(Comput (P1,s1,4)),n))) by EXTPRO_1:4
.= 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:70
.= 2 + 2 by A53, ABSVALUE:46 ;
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:158;
A63: Comput (P2,(Comput (P2,s2,4)),(n + 1)) = Following (P2,(Comput (P2,(Comput (P2,s2,4)),n))) by EXTPRO_1:4
.= 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:70
.= 2 + 2 by A54, ABSVALUE:46 ;
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:52, SCMPDS_2:70
.= (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:52, SCMPDS_2:70 ;
A71: (Comput (P1,(Comput (P1,s1,4)),(n + 1))) . (intpos 10) = (Comput (P1,(Comput (P1,s1,4)),n)) . (intpos 10) by A57, AMI_3:52, SCMPDS_2:70
.= (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:52, SCMPDS_2:70 ;

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 13;
A82: j1 <= n by A78, A79, XREAL_1:8;
thus IC (Comput (P1,s1,j)) = IC (Comput (P1,(Comput (P1,s1,4)),j1)) by A79, EXTPRO_1:5
.= IC (Comput (P2,(Comput (P2,s2,4)),j1)) by A52, A68, A82
.= IC (Comput (P2,s2,j)) by A79, EXTPRO_1:5 ; :: 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:5
.= (Comput (P2,(Comput (P2,s2,4)),j1)) . (intpos 9) by A52, A68, A82
.= (Comput (P2,s2,j)) . (intpos 9) by A79, EXTPRO_1:5 ; :: 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:5
.= (Comput (P2,(Comput (P2,s2,4)),j1)) . (intpos 10) by A52, A69, A82
.= (Comput (P2,s2,j)) . (intpos 10) by A79, EXTPRO_1:5 ; :: 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 13;
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:5
.= IC (Comput (P2,(Comput (P2,s2,4)),(n + 1))) by A58, A59, A64, EXTPRO_1:6, NAT_1:11
.= IC (Comput (P2,(Comput (P2,s2,4)),((n + 1) + j1))) by A65, EXTPRO_1:6, NAT_1:11
.= IC (Comput (P2,s2,j)) by A86, EXTPRO_1:5 ;
:: 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:5
.= (Comput (P2,(Comput (P2,s2,4)),(n + 1))) . (intpos 9) by A59, A70, EXTPRO_1:6, NAT_1:11
.= (Comput (P2,(Comput (P2,s2,4)),((n + 1) + j1))) . (intpos 9) by A65, EXTPRO_1:6, NAT_1:11
.= (Comput (P2,s2,j)) . (intpos 9) by A86, EXTPRO_1:5 ; :: 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:5
.= (Comput (P2,(Comput (P2,s2,4)),(n + 1))) . (intpos 10) by A59, A71, EXTPRO_1:6, NAT_1:11
.= (Comput (P2,(Comput (P2,s2,4)),((n + 1) + j1))) . (intpos 10) by A65, EXTPRO_1:6, NAT_1:11
.= (Comput (P2,s2,j)) . (intpos 10) by A86, EXTPRO_1:5 ; :: thesis: verum

end;

end;

end;

set A = {(IC ),(intpos 9),(intpos 10)};
A88: dom ((Initialize GCD-Algorithm) +* p) = (dom (Initialize GCD-Algorithm)) \/ (dom p) by FUNCT_4:def 1;
IC in {(IC )} by TARSKI:def 1;
then IC in dom (Initialize GCD-Algorithm) by A8, XBOOLE_0:def 3;
then A89: IC in dom ((Initialize GCD-Algorithm) +* p) by A88, XBOOLE_0:def 3;
A90: dom GCD-Algorithm c= NAT by RELAT_1:def 18;
NAT misses Data-Locations SCMPDS by COMPOS_1:51;
then A91: dom GCD-Algorithm misses Data-Locations SCMPDS by A90, XBOOLE_1:63;
DataPart (Initialize GCD-Algorithm) = DataPart GCD-Algorithm by COMPOS_1:80
.= {} by A91, RELAT_1:95 ;
then dom (DataPart ((Initialize GCD-Algorithm) +* p)) = dom ({} +* (DataPart p)) by FUNCT_4:75
.= dom (DataPart p) by FUNCT_4:21
.= {(intpos 9),(intpos 10)} by A7, A4, COMPOS_1:33 ;
then A92: dom (NPP ((Initialize GCD-Algorithm) +* p)) = {(IC )} \/ {(intpos 9),(intpos 10)} by A89, COMPOS_1:70
.= {(IC ),(intpos 9),(intpos 10)} by ENUMSET1:42 ;
let k be Element of NAT ; :: thesis: (Comput (P1,s1,k)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* p))) = (Comput (P2,s2,k)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* 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 4
.= dom (Comput (P2,s2,k)) by PARTFUN1:def 4 ;
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:92;
hence (Comput (P1,s1,k)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* p))) = (Comput (P2,s2,k)) | (proj1 (NPP ((Initialize GCD-Algorithm) +* p))) by A92; :: thesis: verum

end;