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;
A5: dom (Initialize GCD-Algorithm) = {(IC SCMPDS)} \/ (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
A6: z in dom (Initialize GCD-Algorithm) and
A7: z in dom p by XBOOLE_0:3;
( z = intpos 9 or z = intpos 10 ) by A4, A7, TARSKI:def 2;
hence contradiction by A6, SCMPDS_4:31; :: thesis: verum

end;

then A8: Initialize GCD-Algorithm c= (Initialize GCD-Algorithm) +* p by FUNCT_4:33;
A9: intpos 9 in dom p by A4, TARSKI:def 2;
A10: intpos 10 in dom p by A4, TARSKI:def 2;
A11: for t being State of SCMPDS st (Initialize GCD-Algorithm) +* p c= t holds
( t . (intpos 9) = x & t . (intpos 10) = y )

proof

let t be State of SCMPDS; :: thesis: ( (Initialize GCD-Algorithm) +* p c= t implies ( t . (intpos 9) = x & t . (intpos 10) = y ) )
assume A12: (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 A13: p c= t by A12, XBOOLE_1:1;
hence t . (intpos 9) = p . (intpos 9) by A9, GRFUNC_1:8
.= x by A3, AMI_3:52, FUNCT_4:66 ;
:: thesis: t . (intpos 10) = y
thus t . (intpos 10) = p . (intpos 10) by A10, A13, GRFUNC_1:8
.= y by A3, FUNCT_4:66 ; :: thesis: verum

end;

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

proof

let s1, s2 be State of SCMPDS; :: according to EXTPRO_1:def 9 :: thesis: ( not (Initialize GCD-Algorithm) +* p c= s1 or not (Initialize GCD-Algorithm) +* p c= s2 or for b₁ being Element of NAT holds (Comput ((ProgramPart s1),s1,b₁)) | (proj1 ((Initialize GCD-Algorithm) +* p)) = (Comput ((ProgramPart s2),s2,b₁)) | (proj1 ((Initialize GCD-Algorithm) +* p)) )
assume that
A14: (Initialize GCD-Algorithm) +* p c= s1 and
A15: (Initialize GCD-Algorithm) +* p c= s2 ; :: thesis: for b₁ being Element of NAT holds (Comput ((ProgramPart s1),s1,b₁)) | (proj1 ((Initialize GCD-Algorithm) +* p)) = (Comput ((ProgramPart s2),s2,b₁)) | (proj1 ((Initialize GCD-Algorithm) +* p))
A16: Initialize GCD-Algorithm c= s1 by A8, A14, XBOOLE_1:1;
then A17: GCD-Algorithm c= s1 by COMPOS_1:132;
A18: Initialize GCD-Algorithm c= s2 by A8, A15, XBOOLE_1:1;
then A19: GCD-Algorithm c= s2 by COMPOS_1:132;
A20: s1 . (intpos 9) = x by A11, A14;
A21: s1 . (intpos 10) = y by A11, A14;
A22: s2 . (intpos 9) = x by A11, A15;
A23: s2 . (intpos 10) = y by A11, A15;
set s4 = Comput ((ProgramPart s1),s1,4);
set t4 = Comput ((ProgramPart s2),s2,4);
A24: GCD-Algorithm c= Comput ((ProgramPart s1),s1,4) by A16, AMI_1:81, COMPOS_1:132;
A25: IC (Comput ((ProgramPart s1),s1,4)) = 5 by A16, Th15;
A26: (Comput ((ProgramPart s1),s1,4)) . GBP = 0 by A16, Th15;
A27: (Comput ((ProgramPart s1),s1,4)) . SBP = 7 by A16, Th15;
A28: (Comput ((ProgramPart s1),s1,4)) . (intpos (7 + RetIC)) = 2 by A16, Th15;
A29: (Comput ((ProgramPart s1),s1,4)) . (intpos 9) = s1 . (intpos 9) by A16, Th15;
A30: (Comput ((ProgramPart s1),s1,4)) . (intpos 10) = s1 . (intpos 10) by A16, Th15;
A31: (Comput ((ProgramPart s1),s1,4)) . (DataLoc (((Comput ((ProgramPart s1),s1,4)) . SBP),3)) = (Comput ((ProgramPart s1),s1,4)) . (intpos (7 + 3)) by A27, Th5
.= y by A11, A14, A30 ;
A32: DataLoc (((Comput ((ProgramPart s1),s1,4)) . SBP),2) = intpos (7 + 2) by A27, Th5;
A33: GCD-Algorithm c= Comput ((ProgramPart s2),s2,4) by A18, AMI_1:81, COMPOS_1:132;
A34: IC (Comput ((ProgramPart s2),s2,4)) = 5 by A18, Th15;
A35: (Comput ((ProgramPart s2),s2,4)) . GBP = 0 by A18, Th15;
A36: (Comput ((ProgramPart s2),s2,4)) . SBP = 7 by A18, Th15;
A37: (Comput ((ProgramPart s2),s2,4)) . (intpos (7 + RetIC)) = 2 by A18, Th15;
A38: (Comput ((ProgramPart s2),s2,4)) . (intpos 9) = s2 . (intpos 9) by A18, Th15;
A39: (Comput ((ProgramPart s2),s2,4)) . (intpos 10) = s2 . (intpos 10) by A18, Th15;
(Comput ((ProgramPart s2),s2,4)) . (DataLoc (((Comput ((ProgramPart s2),s2,4)) . SBP),3)) = (Comput ((ProgramPart s2),s2,4)) . (intpos (7 + 3)) by A36, Th5
.= (Comput ((ProgramPart s1),s1,4)) . (DataLoc (((Comput ((ProgramPart s1),s1,4)) . SBP),3)) by A11, A15, A31, A39 ;
then consider n being Element of NAT such that
A40: CurInstr ((ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n))),(Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n))) = return SBP and
A41: (Comput ((ProgramPart s1),s1,4)) . SBP = (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n)) . SBP and
A42: CurInstr ((ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n))),(Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n))) = return SBP and
A43: (Comput ((ProgramPart s2),s2,4)) . SBP = (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n)) . SBP and
A44: for j being Element of NAT st 1 < j & j <= ((Comput ((ProgramPart s1),s1,4)) . SBP) + 1 holds
( (Comput ((ProgramPart s1),s1,4)) . (intpos j) = (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n)) . (intpos j) & (Comput ((ProgramPart s2),s2,4)) . (intpos j) = (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n)) . (intpos j) ) and
A45: for k being Element of NAT
for c being Int_position st k <= n & (Comput ((ProgramPart s1),s1,4)) . c = (Comput ((ProgramPart s2),s2,4)) . c holds
( IC (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),k)) = IC (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),k)) & (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),k)) . c = (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),k)) . c ) by A1, A2, A11, A15, A20, A24, A25, A26, A27, A29, A31, A32, A33, A34, A35, A36, A38, Lm8;
A46: (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n)) . (DataLoc (((Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n)) . SBP),RetIC)) = (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n)) . (intpos (7 + 1)) by A27, A41, Th5, SCMPDS_1:def 23
.= 2 by A27, A28, A44, SCMPDS_1:def 23 ;
A47: (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n)) . (DataLoc (((Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n)) . SBP),RetIC)) = (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n)) . (intpos (7 + 1)) by A36, A43, Th5, SCMPDS_1:def 23
.= 2 by A27, A37, A44, SCMPDS_1:def 23 ;
Y: (ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),(n + 1)))) /. (IC (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),(n + 1)))) = (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),(n + 1))) . (IC (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),(n + 1)))) by COMPOS_1:38;
T: ProgramPart (Comput ((ProgramPart s1),s1,4)) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n)) by AMI_1:123;
A48: Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),(n + 1)) = Following ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n))) by EXTPRO_1:4
.= Exec ((return SBP),(Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n))) by A40, T ;
then A49: IC (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),(n + 1))) = (abs ((Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n)) . (DataLoc (((Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n)) . SBP),RetIC)))) + 2 by SCMPDS_2:70
.= 2 + 2 by A46, ABSVALUE:46 ;
then A50: CurInstr ((ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),(n + 1)))),(Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),(n + 1)))) = (Comput ((ProgramPart s1),s1,4)) . 4 by Y, AMI_1:54
.= s1 . 4 by AMI_1:54
.= halt SCMPDS by A17, Lm1 ;
TX1: ProgramPart (Comput ((ProgramPart s1),s1,4)) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),(n + 1))) by AMI_1:123;
Y: (ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1)))) /. (IC (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1)))) = (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1))) . (IC (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1)))) by COMPOS_1:38;
T: ProgramPart (Comput ((ProgramPart s2),s2,4)) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n)) by AMI_1:123;
A51: Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1)) = Following ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n))) by EXTPRO_1:4
.= Exec ((return SBP),(Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n))) by A42, T ;
then A52: IC (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1))) = (abs ((Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n)) . (DataLoc (((Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n)) . SBP),RetIC)))) + 2 by SCMPDS_2:70
.= 2 + 2 by A47, ABSVALUE:46 ;
then A53: CurInstr ((ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1)))),(Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1)))) = (Comput ((ProgramPart s2),s2,4)) . 4 by Y, AMI_1:54
.= s2 . 4 by AMI_1:54
.= halt SCMPDS by A19, Lm1 ;
TX: ProgramPart (Comput ((ProgramPart s2),s2,4)) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1))) by AMI_1:123;
Tx: ProgramPart (Comput ((ProgramPart s2),s2,4)) = ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1))) by AMI_1:123;
A54: (Comput ((ProgramPart s1),s1,4)) . (intpos 9) = (Comput ((ProgramPart s2),s2,4)) . (intpos 9) by A16, A18, A20, A22, Lm9;
A55: (Comput ((ProgramPart s1),s1,4)) . (intpos 10) = (Comput ((ProgramPart s2),s2,4)) . (intpos 10) by A16, A18, A21, A23, Lm9;
A56: (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),(n + 1))) . (intpos 9) = (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n)) . (intpos 9) by A48, AMI_3:52, SCMPDS_2:70
.= (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n)) . (intpos 9) by A45, A54
.= (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1))) . (intpos 9) by A51, AMI_3:52, SCMPDS_2:70 ;
A57: (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),(n + 1))) . (intpos 10) = (Comput ((ProgramPart (Comput ((ProgramPart s1),s1,4))),(Comput ((ProgramPart s1),s1,4)),n)) . (intpos 10) by A48, AMI_3:52, SCMPDS_2:70
.= (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),n)) . (intpos 10) by A45, A55
.= (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1))) . (intpos 10) by A51, AMI_3:52, SCMPDS_2:70 ;

A58: now

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

A60: now

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

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

end;

end;

end;

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

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

then A63: j <= 4 by XXREAL_0:2;
hence IC (Comput ((ProgramPart s1),s1,j)) = IC (Comput ((ProgramPart s2),s2,j)) by A16, A18, A20, A22, Lm9; :: thesis: ( (Comput ((ProgramPart s1),s1,j)) . (intpos 9) = (Comput ((ProgramPart s2),s2,j)) . (intpos 9) & (Comput ((ProgramPart s1),s1,j)) . (intpos 10) = (Comput ((ProgramPart s2),s2,j)) . (intpos 10) )
thus (Comput ((ProgramPart s1),s1,j)) . (intpos 9) = (Comput ((ProgramPart s2),s2,j)) . (intpos 9) by A16, A18, A20, A22, A63, Lm9; :: thesis: (Comput ((ProgramPart s1),s1,j)) . (intpos 10) = (Comput ((ProgramPart s2),s2,j)) . (intpos 10)
thus (Comput ((ProgramPart s1),s1,j)) . (intpos 10) = (Comput ((ProgramPart s2),s2,j)) . (intpos 10) by A16, A18, A21, A23, A63, Lm9; :: thesis: verum

end;

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

then consider j1 being Nat such that
A65: j = 4 + j1 by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 13;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,4)) by AMI_1:123;
S: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,4)) by AMI_1:123;
A66: j1 <= n by A64, A65, XREAL_1:8;
thus IC (Comput ((ProgramPart s1),s1,j)) = IC (Comput ((ProgramPart s1),(Comput ((ProgramPart s1),s1,4)),j1)) by A65, EXTPRO_1:5
.= IC (Comput ((ProgramPart s2),(Comput ((ProgramPart s2),s2,4)),j1)) by A45, A54, A66, T, S
.= IC (Comput ((ProgramPart s2),s2,j)) by A65, EXTPRO_1:5 ; :: thesis: ( (Comput ((ProgramPart s1),s1,j)) . (intpos 9) = (Comput ((ProgramPart s2),s2,j)) . (intpos 9) & (Comput ((ProgramPart s1),s1,j)) . (intpos 10) = (Comput ((ProgramPart s2),s2,j)) . (intpos 10) )
thus (Comput ((ProgramPart s1),s1,j)) . (intpos 9) = (Comput ((ProgramPart s1),(Comput ((ProgramPart s1),s1,4)),j1)) . (intpos 9) by A65, EXTPRO_1:5
.= (Comput ((ProgramPart s2),(Comput ((ProgramPart s2),s2,4)),j1)) . (intpos 9) by A45, A54, A66, T, S
.= (Comput ((ProgramPart s2),s2,j)) . (intpos 9) by A65, EXTPRO_1:5 ; :: thesis: (Comput ((ProgramPart s1),s1,j)) . (intpos 10) = (Comput ((ProgramPart s2),s2,j)) . (intpos 10)
thus (Comput ((ProgramPart s1),s1,j)) . (intpos 10) = (Comput ((ProgramPart s1),(Comput ((ProgramPart s1),s1,4)),j1)) . (intpos 10) by A65, EXTPRO_1:5
.= (Comput ((ProgramPart s2),(Comput ((ProgramPart s2),s2,4)),j1)) . (intpos 10) by A45, A55, A66, T, S
.= (Comput ((ProgramPart s2),s2,j)) . (intpos 10) by A65, EXTPRO_1:5 ; :: thesis: verum

end;

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

then consider j1 being Nat such that
A67: j = (n + (1 + 4)) + j1 by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 13;
T: ProgramPart s2 = ProgramPart (Comput ((ProgramPart s2),s2,4)) by AMI_1:123;
S: ProgramPart s1 = ProgramPart (Comput ((ProgramPart s1),s1,4)) by AMI_1:123;
A68: j = ((n + 1) + j1) + 4 by A67;
hence IC (Comput ((ProgramPart s1),s1,j)) = IC (Comput ((ProgramPart s1),(Comput ((ProgramPart s1),s1,4)),((n + 1) + j1))) by EXTPRO_1:5
.= IC (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1))) by A49, A50, A52, S, TX1, EXTPRO_1:6, NAT_1:11
.= IC (Comput ((ProgramPart s2),(Comput ((ProgramPart s2),s2,4)),((n + 1) + j1))) by A53, T, TX, EXTPRO_1:6, NAT_1:11
.= IC (Comput ((ProgramPart s2),s2,j)) by A68, EXTPRO_1:5 ;
:: thesis: ( (Comput ((ProgramPart s1),s1,j)) . (intpos 9) = (Comput ((ProgramPart s2),s2,j)) . (intpos 9) & (Comput ((ProgramPart s1),s1,j)) . (intpos 10) = (Comput ((ProgramPart s2),s2,j)) . (intpos 10) )
thus (Comput ((ProgramPart s1),s1,j)) . (intpos 9) = (Comput ((ProgramPart s1),(Comput ((ProgramPart s1),s1,4)),((n + 1) + j1))) . (intpos 9) by A68, EXTPRO_1:5
.= (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1))) . (intpos 9) by A50, A56, S, TX1, EXTPRO_1:6, NAT_1:11
.= (Comput ((ProgramPart s2),(Comput ((ProgramPart s2),s2,4)),((n + 1) + j1))) . (intpos 9) by A53, T, Tx, EXTPRO_1:6, NAT_1:11
.= (Comput ((ProgramPart s2),s2,j)) . (intpos 9) by A68, EXTPRO_1:5 ; :: thesis: (Comput ((ProgramPart s1),s1,j)) . (intpos 10) = (Comput ((ProgramPart s2),s2,j)) . (intpos 10)
thus (Comput ((ProgramPart s1),s1,j)) . (intpos 10) = (Comput ((ProgramPart s1),(Comput ((ProgramPart s1),s1,4)),((n + 1) + j1))) . (intpos 10) by A68, EXTPRO_1:5
.= (Comput ((ProgramPart (Comput ((ProgramPart s2),s2,4))),(Comput ((ProgramPart s2),s2,4)),(n + 1))) . (intpos 10) by A50, A57, S, TX1, EXTPRO_1:6, NAT_1:11
.= (Comput ((ProgramPart s2),(Comput ((ProgramPart s2),s2,4)),((n + 1) + j1))) . (intpos 10) by A53, T, TX, EXTPRO_1:6, NAT_1:11
.= (Comput ((ProgramPart s2),s2,j)) . (intpos 10) by A68, EXTPRO_1:5 ; :: thesis: verum

end;

end;

end;

set A = {(IC SCMPDS),(intpos 9),(intpos 10)};
A69: dom ((Initialize GCD-Algorithm) +* p) = ({(IC SCMPDS)} \/ (dom GCD-Algorithm)) \/ {(intpos 9),(intpos 10)} by A4, A5, FUNCT_4:def 1
.= ({(IC SCMPDS)} \/ {(intpos 9),(intpos 10)}) \/ (dom GCD-Algorithm) by XBOOLE_1:4
.= {(IC SCMPDS),(intpos 9),(intpos 10)} \/ (dom GCD-Algorithm) by ENUMSET1:42 ;
let k be Element of NAT ; :: thesis: (Comput ((ProgramPart s1),s1,k)) | (proj1 ((Initialize GCD-Algorithm) +* p)) = (Comput ((ProgramPart s2),s2,k)) | (proj1 ((Initialize GCD-Algorithm) +* p))
A70: GCD-Algorithm c= Comput ((ProgramPart s2),s2,k) by A19, AMI_1:86;
GCD-Algorithm c= Comput ((ProgramPart s1),s1,k) by A17, AMI_1:86;
then A71: (Comput ((ProgramPart s1),s1,k)) | (dom GCD-Algorithm) = GCD-Algorithm by GRFUNC_1:64
.= (Comput ((ProgramPart s2),s2,k)) | (dom GCD-Algorithm) by A70, GRFUNC_1:64 ;
A72: (Comput ((ProgramPart s1),s1,k)) . (IC SCMPDS) = IC (Comput ((ProgramPart s1),s1,k))
.= IC (Comput ((ProgramPart s2),s2,k)) by A58
.= (Comput ((ProgramPart s2),s2,k)) . (IC SCMPDS) ;
A73: (Comput ((ProgramPart s1),s1,k)) . (intpos 9) = (Comput ((ProgramPart s2),s2,k)) . (intpos 9) by A58;
A74: (Comput ((ProgramPart s1),s1,k)) . (intpos 10) = (Comput ((ProgramPart s2),s2,k)) . (intpos 10) by A58;
dom (Comput ((ProgramPart s1),s1,k)) = the carrier of SCMPDS by PARTFUN1:def 4
.= dom (Comput ((ProgramPart s2),s2,k)) by PARTFUN1:def 4 ;
then (Comput ((ProgramPart s1),s1,k)) | {(IC SCMPDS),(intpos 9),(intpos 10)} = (Comput ((ProgramPart s2),s2,k)) | {(IC SCMPDS),(intpos 9),(intpos 10)} by A72, A73, A74, GRFUNC_1:92;
hence (Comput ((ProgramPart s1),s1,k)) | (proj1 ((Initialize GCD-Algorithm) +* p)) = (Comput ((ProgramPart s2),s2,k)) | (proj1 ((Initialize GCD-Algorithm) +* p)) by A69, A71, RELAT_1:185; :: thesis: verum

end;