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
(Initialized GCD-Algorithm ) +* p is autonomic
let x, y be Integer; :: thesis: ( y >= 0 & x >= y & p = (intpos 9),(intpos 10) --> x,y implies (Initialized GCD-Algorithm ) +* p is autonomic )
set GA = GCD-Algorithm ;
set IA = Initialized 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: (Initialized GCD-Algorithm ) +* p is autonomic
A4: dom p = {(intpos 9),(intpos 10)} by A3, FUNCT_4:65;
A5: dom (Initialized GCD-Algorithm ) = {(IC SCMPDS )} \/ (dom GCD-Algorithm ) by SCMPDS_4:27;
now
assume dom (Initialized GCD-Algorithm ) meets dom p ; :: thesis: contradiction
then consider z being set such that
A6: z in dom (Initialized 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: Initialized GCD-Algorithm c= (Initialized 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 (Initialized GCD-Algorithm ) +* p c= t holds
( t . (intpos 9) = x & t . (intpos 10) = y )
proof
let t be State of SCMPDS ; :: thesis: ( (Initialized GCD-Algorithm ) +* p c= t implies ( t . (intpos 9) = x & t . (intpos 10) = y ) )
assume A12: (Initialized GCD-Algorithm ) +* p c= t ; :: thesis: ( t . (intpos 9) = x & t . (intpos 10) = y )
p c= (Initialized 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 (Initialized GCD-Algorithm ) +* p is autonomic :: thesis: verum
proof
let s1, s2 be State of SCMPDS ; :: according to AMI_1:def 25 :: thesis: ( not (Initialized GCD-Algorithm ) +* p c= s1 or not (Initialized GCD-Algorithm ) +* p c= s2 or for b1 being Element of NAT holds (Comput (ProgramPart s1),s1,b1) | (proj1 ((Initialized GCD-Algorithm ) +* p)) = (Comput (ProgramPart s2),s2,b1) | (proj1 ((Initialized GCD-Algorithm ) +* p)) )
assume that
A14: (Initialized GCD-Algorithm ) +* p c= s1 and
A15: (Initialized GCD-Algorithm ) +* p c= s2 ; :: thesis: for b1 being Element of NAT holds (Comput (ProgramPart s1),s1,b1) | (proj1 ((Initialized GCD-Algorithm ) +* p)) = (Comput (ProgramPart s2),s2,b1) | (proj1 ((Initialized GCD-Algorithm ) +* p))
A16: Initialized GCD-Algorithm c= s1 by A8, A14, XBOOLE_1:1;
then A17: GCD-Algorithm c= s1 by SCMPDS_4:57;
A18: Initialized GCD-Algorithm c= s2 by A8, A15, XBOOLE_1:1;
then A19: GCD-Algorithm c= s2 by SCMPDS_4:57;
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, SCMPDS_4:57;
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, SCMPDS_4:57;
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 AMI_1:150;
T: ProgramPart (Comput (ProgramPart s1),s1,4) = ProgramPart (Comput (ProgramPart (Comput (ProgramPart s1),s1,4)),(Comput (ProgramPart s1),s1,4),n) by AMI_1:144;
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 AMI_1:14
.= 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, Th3 ;
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 AMI_1:54, Y
.= 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:144;
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 AMI_1:150;
T: ProgramPart (Comput (ProgramPart s2),s2,4) = ProgramPart (Comput (ProgramPart (Comput (ProgramPart s2),s2,4)),(Comput (ProgramPart s2),s2,4),n) by AMI_1:144;
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 AMI_1:14
.= 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, Th3 ;
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 AMI_1:54, Y
.= 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:144;
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:144;
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,b1) = IC (Comput (ProgramPart s2),s2,b1) & (Comput (ProgramPart s1),s1,b1) . (intpos 9) = (Comput (ProgramPart s2),s2,b1) . (intpos 9) & (Comput (ProgramPart s1),s1,b1) . (intpos 10) = (Comput (ProgramPart s2),s2,b1) . (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,b1) = IC (Comput (ProgramPart s2),s2,b1) & (Comput (ProgramPart s1),s1,b1) . (intpos 9) = (Comput (ProgramPart s2),s2,b1) . (intpos 9) & (Comput (ProgramPart s1),s1,b1) . (intpos 10) = (Comput (ProgramPart s2),s2,b1) . (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,b1) = IC (Comput (ProgramPart s2),s2,b1) & (Comput (ProgramPart s1),s1,b1) . (intpos 9) = (Comput (ProgramPart s2),s2,b1) . (intpos 9) & (Comput (ProgramPart s1),s1,b1) . (intpos 10) = (Comput (ProgramPart s2),s2,b1) . (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:144;
S: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,4) by AMI_1:144;
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, AMI_1:51
.= IC (Comput (ProgramPart s2),(Comput (ProgramPart s2),s2,4),j1) by A45, A54, A66, T, S
.= IC (Comput (ProgramPart s2),s2,j) by A65, AMI_1:51 ; :: 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, AMI_1:51
.= (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, AMI_1:51 ; :: 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, AMI_1:51
.= (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, AMI_1:51 ; :: thesis: verum
end;
suppose j >= n + 5 ; :: thesis: ( IC (Comput (ProgramPart s1),s1,b1) = IC (Comput (ProgramPart s2),s2,b1) & (Comput (ProgramPart s1),s1,b1) . (intpos 9) = (Comput (ProgramPart s2),s2,b1) . (intpos 9) & (Comput (ProgramPart s1),s1,b1) . (intpos 10) = (Comput (ProgramPart s2),s2,b1) . (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:144;
S: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,4) by AMI_1:144;
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 AMI_1:51
.= IC (Comput (ProgramPart (Comput (ProgramPart s2),s2,4)),(Comput (ProgramPart s2),s2,4),(n + 1)) by A49, A50, A52, AMI_1:52, NAT_1:11, T, S, TX1
.= IC (Comput (ProgramPart s2),(Comput (ProgramPart s2),s2,4),((n + 1) + j1)) by A53, AMI_1:52, NAT_1:11, T, TX
.= IC (Comput (ProgramPart s2),s2,j) by A68, AMI_1:51 ;
:: 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, AMI_1:51
.= (Comput (ProgramPart (Comput (ProgramPart s2),s2,4)),(Comput (ProgramPart s2),s2,4),(n + 1)) . (intpos 9) by A50, A56, AMI_1:52, NAT_1:11, T, S, TX, TX1
.= (Comput (ProgramPart s2),(Comput (ProgramPart s2),s2,4),((n + 1) + j1)) . (intpos 9) by A53, AMI_1:52, NAT_1:11, T, S, Tx
.= (Comput (ProgramPart s2),s2,j) . (intpos 9) by A68, AMI_1:51 ; :: 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, AMI_1:51
.= (Comput (ProgramPart (Comput (ProgramPart s2),s2,4)),(Comput (ProgramPart s2),s2,4),(n + 1)) . (intpos 10) by A50, A57, AMI_1:52, NAT_1:11, T, S, TX1
.= (Comput (ProgramPart s2),(Comput (ProgramPart s2),s2,4),((n + 1) + j1)) . (intpos 10) by A53, AMI_1:52, NAT_1:11, T, S, TX
.= (Comput (ProgramPart s2),s2,j) . (intpos 10) by A68, AMI_1:51 ; :: thesis: verum
end;
end;
end;
set A = {(IC SCMPDS ),(intpos 9),(intpos 10)};
A69: dom ((Initialized 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 ((Initialized GCD-Algorithm ) +* p)) = (Comput (ProgramPart s2),s2,k) | (proj1 ((Initialized 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 ((Initialized GCD-Algorithm ) +* p)) = (Comput (ProgramPart s2),s2,k) | (proj1 ((Initialized GCD-Algorithm ) +* p)) by A69, A71, RELAT_1:185; :: thesis: verum
end;