let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis:
set GA = GCD-Algorithm ;
defpred S₁[ Element of NAT ] means for s1, s2 being State of SCMPDS st GCD-Algorithm c= P1 & GCD-Algorithm c= P2 & IC s1 = 5 & s1 . SBP > 0 & s1 . GBP = 0 & s1 . (DataLoc ((s1 . SBP),3)) <= $1 & s1 . (DataLoc ((s1 . SBP),3)) >= 0 & s1 . (DataLoc ((s1 . SBP),2)) >= s1 . (DataLoc ((s1 . SBP),3)) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) & s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) holds
ex n being Element of NAT st
( CurInstr (P1,(Comput (P1,s1,n))) = return SBP & s1 . SBP = (Comput (P1,s1,n)) . SBP & CurInstr (P2,(Comput (P2,s2,n))) = return SBP & s2 . SBP = (Comput (P2,s2,n)) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP) + 1 holds
( s1 . (intpos j) = (Comput (P1,s1,n)) . (intpos j) & s2 . (intpos j) = (Comput (P2,s2,n)) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) ) );
A1: S₁[ 0 ]

proof

let s1, s2 be State of SCMPDS; :: thesis:
set x = s1 . (DataLoc ((s1 . SBP),2));
set y = s1 . (DataLoc ((s1 . SBP),3));
set y2 = s2 . (DataLoc ((s1 . SBP),3));
assume that
A4: GCD-Algorithm c= P1 and
A5: GCD-Algorithm c= P2 ; :: thesis:
assume A6: IC s1 = 5 ; :: thesis:
assume that
s1 . SBP > 0 and
s1 . GBP = 0 ; :: thesis:
assume A7: s1 . (DataLoc ((s1 . SBP),3)) <= 0 ; :: thesis:
assume s1 . (DataLoc ((s1 . SBP),3)) >= 0 ; :: thesis:
assume s1 . (DataLoc ((s1 . SBP),2)) >= s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
assume that
A8: IC s2 = IC s1 and
A9: s2 . SBP = s1 . SBP and
s2 . GBP = 0 ; :: thesis:
assume that
s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) and
A10: s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
A11: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
A12: Comput (P1,s1,(1 + 0)) = Following (P1,(Comput (P1,s1,0))) by EXTPRO_1:3
.= Following (P1,s1) by EXTPRO_1:2
.= Exec (((SBP,3) <=0_goto 9),s1) by A6, A11, Lm1, A4 ;
A13: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A14: Comput (P2,s2,(1 + 0)) = Following (P2,(Comput (P2,s2,0))) by EXTPRO_1:3
.= Following (P2,s2) by EXTPRO_1:2
.= Exec (((SBP,3) <=0_goto 9),s2) by A6, A8, A13, Lm1, A5 ;
A15: IC (Comput (P1,s1,1)) = ICplusConst (s1,9) by A7, A12, SCMPDS_2:56
.= 5 + 9 by A6, SCMPDS_6:12 ;
A16: IC (Comput (P2,s2,1)) = ICplusConst (s2,9) by A7, A9, A10, A14, SCMPDS_2:56
.= 5 + 9 by A6, A8, SCMPDS_6:12 ;
take n = 1; :: thesis:
A17: P1 /. (IC (Comput (P1,s1,n))) = P1 . (IC (Comput (P1,s1,n))) by PBOOLE:143;
thus CurInstr (P1,(Comput (P1,s1,n))) = P1 . 14 by A15, A17
.= return SBP by Lm1, A4 ; :: thesis:
thus (Comput (P1,s1,n)) . SBP = s1 . SBP by A12, SCMPDS_2:56; :: thesis:
A18: P2 /. (IC (Comput (P2,s2,n))) = P2 . (IC (Comput (P2,s2,n))) by PBOOLE:143;
thus CurInstr (P2,(Comput (P2,s2,n))) = P2 . 14 by A16, A18
.= return SBP by Lm1, A5 ; :: thesis:
thus (Comput (P2,s2,n)) . SBP = s2 . SBP by A14, SCMPDS_2:56; :: thesis:
thus for j being Element of NAT st 1 < j & j <= (s1 . SBP) + 1 holds
( s1 . (intpos j) = (Comput (P1,s1,n)) . (intpos j) & s2 . (intpos j) = (Comput (P2,s2,n)) . (intpos j) ) by A12, A14, SCMPDS_2:56; :: thesis:

hereby :: thesis:

let k be Element of NAT ; :: thesis:
let a be Int_position ; :: thesis:
assume that
A19: k <= n and
A20: s1 . a = s2 . a ; :: thesis:

per cases by A19, NAT_1:25;

suppose A21: k = 0 ; :: thesis:

hence IC (Comput (P1,s1,k)) = IC s2 by A8, EXTPRO_1:2
.= IC (Comput (P2,s2,k)) by A21, EXTPRO_1:2 ;
:: thesis:
thus (Comput (P1,s1,k)) . a = s1 . a by A21, EXTPRO_1:2
.= (Comput (P2,s2,k)) . a by A20, A21, EXTPRO_1:2 ; :: thesis:

end;

suppose A22: k = 1 ; :: thesis:

hence IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) by A15, A16; :: thesis:
thus (Comput (P1,s1,k)) . a = s1 . a by A12, A22, SCMPDS_2:56
.= (Comput (P2,s2,k)) . a by A14, A20, A22, SCMPDS_2:56 ; :: thesis:

end;

A23: now

let k be Element of NAT ; :: thesis:
assume A24: S₁[k] ; :: thesis:
thus S₁[k + 1] :: thesis:

proof

let s1, s2 be State of SCMPDS; :: thesis:
set x = s1 . (DataLoc ((s1 . SBP),2));
set y = s1 . (DataLoc ((s1 . SBP),3));
assume that
A27: GCD-Algorithm c= P1 and
A28: GCD-Algorithm c= P2 ; :: thesis:
assume A29: IC s1 = 5 ; :: thesis:
assume that
A30: s1 . SBP > 0 and
A31: s1 . GBP = 0 ; :: thesis:
assume A32: s1 . (DataLoc ((s1 . SBP),3)) <= k + 1 ; :: thesis:
assume A33: s1 . (DataLoc ((s1 . SBP),3)) >= 0 ; :: thesis:
assume A34: s1 . (DataLoc ((s1 . SBP),2)) >= s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
assume that
A35: IC s2 = IC s1 and
A36: s2 . SBP = s1 . SBP and
A37: s2 . GBP = 0 ; :: thesis:
assume that
A38: s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) and
A39: s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
reconsider y = s1 . (DataLoc ((s1 . SBP),3)) as Element of NAT by A33, INT_1:3;

per cases by A32, NAT_1:8;

suppose y <= k ; :: thesis:

hence ex n being Element of NAT st
( CurInstr (P1,(Comput (P1,s1,n))) = return SBP & s1 . SBP = (Comput (P1,s1,n)) . SBP & CurInstr (P2,(Comput (P2,s2,n))) = return SBP & s2 . SBP = (Comput (P2,s2,n)) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP) + 1 holds
( s1 . (intpos j) = (Comput (P1,s1,n)) . (intpos j) & s2 . (intpos j) = (Comput (P2,s2,n)) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) ) ) by A24, A29, A30, A31, A33, A34, A35, A36, A37, A38, A39, A27, A28; :: thesis:

end;

suppose A40: y = k + 1 ; :: thesis:

then A41: y > 0 by NAT_1:5;
reconsider n = s1 . SBP as Element of NAT by A30, INT_1:3;
A42: n = s1 . SBP ;
set s8 = Comput (P1,s1,8);
set t8 = Comput (P2,s2,8);
A43: IC (Comput (P1,s1,7)) = 5 + 7 by A29, A31, A38, A41, A42, Lm6, A27;
A44: Comput (P1,s1,8) = Exec ((goto (- 7)),(Comput (P1,s1,7))) by A29, A31, A38, A41, A42, Lm6, A27;
A45: (Comput (P1,s1,7)) . SBP = n + 4 by A29, A31, A38, A41, Lm6, A27;
A46: (Comput (P1,s1,7)) . GBP = 0 by A29, A31, A38, A41, A42, Lm6, A27;
A47: (Comput (P1,s1,7)) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A29, A31, A38, A41, Lm6, A27;
A48: (Comput (P1,s1,7)) . (intpos (n + 6)) = s1 . (intpos (n + 3)) by A29, A31, A38, A41, Lm6, A27;
A49: IC (Comput (P2,s2,7)) = 5 + 7 by A29, A35, A36, A37, A38, A39, A41, A42, Lm6, A28;
A50: Comput (P2,s2,8) = Exec ((goto (- 7)),(Comput (P2,s2,7))) by A29, A35, A36, A37, A38, A39, A41, A42, Lm6, A28;
A51: (Comput (P2,s2,7)) . SBP = n + 4 by A29, A35, A36, A37, A38, A39, A41, Lm6, A28;
A52: (Comput (P2,s2,7)) . GBP = 0 by A29, A35, A36, A37, A38, A39, A41, A42, Lm6, A28;
A53: (Comput (P2,s2,7)) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A29, A31, A35, A36, A37, A38, A39, A41, Lm6, A28;
A54: (Comput (P2,s2,7)) . (intpos (n + 6)) = s1 . (intpos (n + 3)) by A29, A31, A35, A36, A37, A38, A39, A41, Lm6, A28;
A55: (Comput (P1,s1,7)) . (intpos (n + 4)) = n by A29, A31, A38, A41, Lm6, A27;
A56: (Comput (P1,s1,7)) . (intpos (n + 5)) = 11 by A29, A31, A38, A41, Lm6, A27;
A57: (Comput (P2,s2,7)) . (intpos (n + 4)) = n by A29, A35, A36, A37, A38, A39, A41, Lm6, A28;
A58: (Comput (P2,s2,7)) . (intpos (n + 5)) = 11 by A29, A35, A36, A37, A38, A39, A41, Lm6, A28;
A59: DataLoc ((n + 4),2) = intpos ((n + 4) + 2) by Th5
.= intpos (n + (4 + 2)) ;
A60: DataLoc ((n + 4),3) = intpos ((n + 4) + 3) by Th5
.= intpos (n + (4 + 3)) ;
A63: IC (Comput (P1,s1,8)) = ICplusConst ((Comput (P1,s1,7)),(- 7)) by A44, SCMPDS_2:54
.= 5 by A43, Th6 ;
A64: (Comput (P1,s1,8)) . SBP = n + 4 by A44, A45, SCMPDS_2:54;
A65: 4 <= n + 4 by NAT_1:11;
then A66: (Comput (P1,s1,8)) . SBP > 0 by A64, XXREAL_0:2;
A67: (Comput (P1,s1,8)) . GBP = 0 by A44, A46, SCMPDS_2:54;
set x1 = (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),2));
set y1 = (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),3));
A68: (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),2)) = s1 . (intpos (n + 3)) by A44, A48, A59, A64, SCMPDS_2:54
.= y by Th5 ;
A69: (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),3)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A44, A47, A60, A64, SCMPDS_2:54
.= (s1 . (intpos (n + 2))) mod y by Th5 ;
then A70: (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),3)) < y by A40, NAT_1:5, NEWTON:65;
then A71: (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),3)) <= k by A40, INT_1:7;
A72: IC (Comput (P2,s2,8)) = ICplusConst ((Comput (P2,s2,7)),(- 7)) by A50, SCMPDS_2:54
.= IC (Comput (P1,s1,8)) by A49, A63, Th6 ;
A73: (Comput (P2,s2,8)) . SBP = (Comput (P1,s1,8)) . SBP by A50, A51, A64, SCMPDS_2:54;
A74: (Comput (P2,s2,8)) . GBP = 0 by A50, A52, SCMPDS_2:54;
set x3 = (Comput (P2,s2,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),2));
A75: (Comput (P2,s2,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),2)) = s1 . (intpos (n + 3)) by A50, A54, A59, A64, SCMPDS_2:54
.= (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),2)) by A68, Th5 ;
(Comput (P2,s2,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),3)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A50, A53, A60, A64, SCMPDS_2:54
.= (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),3)) by A69, Th5 ;
then consider m being Element of NAT such that
A76: CurInstr (P1,(Comput (P1,(Comput (P1,s1,8)),m))) = return SBP and
A77: (Comput (P1,s1,8)) . SBP = (Comput (P1,(Comput (P1,s1,8)),m)) . SBP and
A78: CurInstr (P2,(Comput (P2,(Comput (P2,s2,8)),m))) = return SBP and
A79: (Comput (P2,s2,8)) . SBP = (Comput (P2,(Comput (P2,s2,8)),m)) . SBP and
A80: for j being Element of NAT st 1 < j & j <= ((Comput (P1,s1,8)) . SBP) + 1 holds
( (Comput (P1,s1,8)) . (intpos j) = (Comput (P1,(Comput (P1,s1,8)),m)) . (intpos j) & (Comput (P2,s2,8)) . (intpos j) = (Comput (P2,(Comput (P2,s2,8)),m)) . (intpos j) ) and
A81: for k being Element of NAT
for a being Int_position st k <= m & (Comput (P1,s1,8)) . a = (Comput (P2,s2,8)) . a holds
( IC (Comput (P1,(Comput (P1,s1,8)),k)) = IC (Comput (P2,(Comput (P2,s2,8)),k)) & (Comput (P1,(Comput (P1,s1,8)),k)) . a = (Comput (P2,(Comput (P2,s2,8)),k)) . a ) by A24, A41, A63, A66, A67, A68, A69, A70, A71, A72, A73, A74, A75, A27, A28, NEWTON:64;
set s9 = Comput (P1,s1,(m + 8));
set t9 = Comput (P2,s2,(m + 8));
A84: (Comput (P1,s1,8)) . SBP = (Comput (P1,s1,(m + 8))) . SBP by A77, EXTPRO_1:4;
A86: Comput (P1,s1,(m + 8)) = Comput (P1,(Comput (P1,s1,8)),m) by EXTPRO_1:4;
A88: Comput (P1,s1,(m + (8 + 1))) = Comput (P1,s1,((m + 8) + 1))
.= Following (P1,(Comput (P1,s1,(m + 8)))) by EXTPRO_1:3
.= Exec ((return SBP),(Comput (P1,s1,(m + 8)))) by A76, A86 ;
A89: 1 < n + 4 by A65, XXREAL_0:2;
A90: n + 4 < ((Comput (P1,s1,8)) . SBP) + 1 by A64, XREAL_1:29;
then A91: (Comput (P1,s1,8)) . (intpos (n + 4)) = (Comput (P1,(Comput (P1,s1,8)),m)) . (intpos (n + 4)) by A80, A89
.= (Comput (P1,s1,(m + 8))) . (intpos (n + 4)) by EXTPRO_1:4 ;
5 <= n + 5 by NAT_1:11;
then A92: 1 < n + 5 by XXREAL_0:2;
A93: intpos (n + (4 + 1)) = intpos ((n + 4) + 1)
.= DataLoc ((n + 4),1) by Th5 ;
A94: 11 = (Comput (P1,s1,8)) . (intpos (n + 5)) by A44, A56, SCMPDS_2:54
.= (Comput (P1,(Comput (P1,s1,8)),m)) . (intpos (n + 5)) by A64, A80, A92
.= (Comput (P1,s1,(m + 8))) . (DataLoc (((Comput (P1,s1,(m + 8))) . SBP),RetIC)) by A64, A84, A93, EXTPRO_1:4, SCMPDS_1:def 21 ;
A95: (Comput (P2,s2,(m + 8))) . SBP = n + 4 by A64, A73, A79, EXTPRO_1:4;
A97: Comput (P2,s2,(m + 8)) = Comput (P2,(Comput (P2,s2,8)),m) by EXTPRO_1:4;
A99: Comput (P2,s2,(m + (8 + 1))) = Comput (P2,s2,((m + 8) + 1))
.= Following (P2,(Comput (P2,s2,(m + 8)))) by EXTPRO_1:3
.= Exec ((return SBP),(Comput (P2,s2,(m + 8)))) by A78, A97 ;
A100: (Comput (P2,s2,8)) . (intpos (n + 4)) = (Comput (P2,(Comput (P2,s2,8)),m)) . (intpos (n + 4)) by A80, A89, A90
.= (Comput (P2,s2,(m + 8))) . (intpos (n + 4)) by EXTPRO_1:4 ;
A101: 11 = (Comput (P2,s2,8)) . (intpos (n + 5)) by A50, A58, SCMPDS_2:54
.= (Comput (P2,(Comput (P2,s2,8)),m)) . (intpos (n + 5)) by A64, A80, A92
.= (Comput (P2,s2,(m + 8))) . (DataLoc (((Comput (P2,s2,(m + 8))) . SBP),RetIC)) by A93, A95, EXTPRO_1:4, SCMPDS_1:def 21 ;
A102: P1 /. (IC (Comput (P1,s1,(m + 9)))) = P1 . (IC (Comput (P1,s1,(m + 9)))) by PBOOLE:143;
A103: IC (Comput (P1,s1,(m + 9))) = (abs ((Comput (P1,s1,(m + 8))) . (DataLoc (((Comput (P1,s1,(m + 8))) . SBP),RetIC)))) + 2 by A88, SCMPDS_2:58
.= 11 + 2 by A94, ABSVALUE:29 ;
then A104: CurInstr (P1,(Comput (P1,s1,(m + 9)))) = P1 . 13 by A102
.= (SBP,2) := (SBP,6) by Lm1, A27 ;
A106: Comput (P1,s1,(m + (9 + 1))) = Comput (P1,s1,((m + 9) + 1))
.= Following (P1,(Comput (P1,s1,(m + 9)))) by EXTPRO_1:3
.= Exec (((SBP,2) := (SBP,6)),(Comput (P1,s1,(m + 9)))) by A104 ;
A107: (Comput (P1,s1,(m + 9))) . SBP = (Comput (P1,s1,(m + 8))) . (DataLoc ((n + 4),RetSP)) by A64, A84, A88, SCMPDS_2:58
.= (Comput (P1,s1,(m + 8))) . (intpos ((n + 4) + 0)) by Th5, SCMPDS_1:def 20
.= n by A44, A55, A91, SCMPDS_2:54 ;
A108: P2 /. (IC (Comput (P2,s2,(m + 9)))) = P2 . (IC (Comput (P2,s2,(m + 9)))) by PBOOLE:143;
A109: IC (Comput (P2,s2,(m + 9))) = (abs ((Comput (P2,s2,(m + 8))) . (DataLoc (((Comput (P2,s2,(m + 8))) . SBP),RetIC)))) + 2 by A99, SCMPDS_2:58
.= 11 + 2 by A101, ABSVALUE:29 ;
then A110: CurInstr (P2,(Comput (P2,s2,(m + 9)))) = P2 . 13 by A108
.= (SBP,2) := (SBP,6) by Lm1, A28 ;
A112: Comput (P2,s2,(m + (9 + 1))) = Comput (P2,s2,((m + 9) + 1))
.= Following (P2,(Comput (P2,s2,(m + 9)))) by EXTPRO_1:3
.= Exec (((SBP,2) := (SBP,6)),(Comput (P2,s2,(m + 9)))) by A110 ;
A113: (Comput (P2,s2,(m + 9))) . SBP = (Comput (P2,s2,(m + 8))) . (DataLoc ((n + 4),RetSP)) by A95, A99, SCMPDS_2:58
.= (Comput (P2,s2,(m + 8))) . (intpos ((n + 4) + 0)) by Th5, SCMPDS_1:def 20
.= n by A50, A57, A100, SCMPDS_2:54 ;
A114: IC (Comput (P1,s1,(m + 10))) = succ (IC (Comput (P1,s1,(m + 9)))) by A106, SCMPDS_2:47
.= 13 + 1 by A103 ;
A115: IC (Comput (P2,s2,(m + 10))) = succ (IC (Comput (P2,s2,(m + 9)))) by A112, SCMPDS_2:47
.= 13 + 1 by A109 ;

hereby :: thesis:

take nn = m + 10; :: thesis:
A116: P1 /. (IC (Comput (P1,s1,nn))) = P1 . (IC (Comput (P1,s1,nn))) by PBOOLE:143;
thus CurInstr (P1,(Comput (P1,s1,nn))) = P1 . 14 by A114, A116
.= return SBP by Lm1, A27 ; :: thesis:
A117: P2 /. (IC (Comput (P2,s2,nn))) = P2 . (IC (Comput (P2,s2,nn))) by PBOOLE:143;
A118: DataLoc (((Comput (P1,s1,(m + 9))) . SBP),2) = intpos (n + 2) by A107, Th5;
hence (Comput (P1,s1,nn)) . SBP = s1 . SBP by A106, A107, Lm3, SCMPDS_2:47; :: thesis:
thus CurInstr (P2,(Comput (P2,s2,nn))) = P2 . 14 by A115, A117
.= return SBP by Lm1, A28 ; :: thesis:
A119: DataLoc (((Comput (P2,s2,(m + 9))) . SBP),2) = intpos (n + 2) by A113, Th5;
hence (Comput (P2,s2,nn)) . SBP = s2 . SBP by A36, A112, A113, Lm3, SCMPDS_2:47; :: thesis:

hereby :: thesis:

let j be Element of NAT ; :: thesis:
assume that
A120: 1 < j and
A121: j <= (s1 . SBP) + 1 ; :: thesis:
s1 . SBP <= (Comput (P1,s1,8)) . SBP by A64, NAT_1:11;
then (s1 . SBP) + 1 <= ((Comput (P1,s1,8)) . SBP) + 1 by XREAL_1:6;
then A122: j <= ((Comput (P1,s1,8)) . SBP) + 1 by A121, XXREAL_0:2;
A123: (Comput (P1,s1,(m + 9))) . (intpos j) = (Comput (P1,s1,(m + 8))) . (intpos j) by A88, A120, AMI_3:10, SCMPDS_2:58
.= (Comput (P1,(Comput (P1,s1,8)),m)) . (intpos j) by EXTPRO_1:4
.= (Comput (P1,s1,8)) . (intpos j) by A80, A120, A122 ;
A124: n + 1 < n + 2 by XREAL_1:6;
(Comput (P1,s1,7)) . (intpos j) = s1 . (intpos j) by A29, A31, A40, A42, A120, A121, Lm5, A27, NAT_1:5;
hence s1 . (intpos j) = (Comput (P1,s1,8)) . (intpos j) by A44, SCMPDS_2:54
.= (Comput (P1,s1,nn)) . (intpos j) by A106, A118, A121, A123, A124, AMI_3:10, SCMPDS_2:47 ;
:: thesis:
A126: (Comput (P2,s2,(m + 9))) . (intpos j) = (Comput (P2,s2,(m + 8))) . (intpos j) by A99, A120, AMI_3:10, SCMPDS_2:58
.= (Comput (P2,(Comput (P2,s2,8)),m)) . (intpos j) by EXTPRO_1:4
.= (Comput (P2,s2,8)) . (intpos j) by A80, A120, A122 ;
j <= n + 1 by A121;
then (Comput (P2,s2,7)) . (intpos j) = s2 . (intpos j) by A29, A35, A36, A37, A39, A40, A120, Lm5, A28, NAT_1:5;
hence s2 . (intpos j) = (Comput (P2,s2,8)) . (intpos j) by A50, SCMPDS_2:54
.= (Comput (P2,s2,nn)) . (intpos j) by A112, A119, A121, A124, A126, AMI_3:10, SCMPDS_2:47 ;
:: thesis:

end;

hereby :: thesis:

let j be Element of NAT ; :: thesis:
let a be Int_position ; :: thesis:
assume that
A127: j <= nn and
A128: s1 . a = s2 . a ; :: thesis:
nn = (m + 9) + 1 ;
then A129: ( j <= m + 9 or j = nn ) by A127, NAT_1:8;
A130: m + (8 + 1) = (m + 8) + 1 ;

A131: now

assume A132: j <= m + 8 ; :: thesis:

per cases ;

suppose j < 7 + 1 ; :: thesis:

hence ( j <= 7 or ( j >= 8 & j <= m + 8 ) ) by NAT_1:13; :: thesis:

end;

suppose j >= 8 ; :: thesis:

hence ( j <= 7 or ( j >= 8 & j <= m + 8 ) ) by A132; :: thesis:

end;

A133: (Comput (P1,s1,8)) . a = (Comput (P1,s1,7)) . a by A44, SCMPDS_2:54
.= (Comput (P2,s2,7)) . a by A29, A31, A35, A36, A37, A27, A28, A38, A39, A41, A42, A128, Lm7
.= (Comput (P2,s2,8)) . a by A50, SCMPDS_2:54 ;

A134: now

let b be Int_position ; :: thesis:
assume A135: (Comput (P1,s1,8)) . b = (Comput (P2,s2,8)) . b ; :: thesis:

per cases ;

suppose b = SBP ; :: thesis:

hence (Comput (P1,s1,(m + 9))) . b = (Comput (P2,s2,(m + 9))) . b by A107, A113; :: thesis:

end;

suppose A136: b <> SBP ; :: thesis:

hence (Comput (P1,s1,(m + 9))) . b = (Comput (P1,s1,(m + 8))) . b by A88, SCMPDS_2:58
.= (Comput (P1,(Comput (P1,s1,8)),m)) . b by EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,8)),m)) . b by A81, A135
.= (Comput (P2,s2,(m + 8))) . b by EXTPRO_1:4
.= (Comput (P2,s2,(m + 9))) . b by A99, A136, SCMPDS_2:58 ;
:: thesis:

end;

A137: (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,(m + 9))) . SBP),6)) = (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),2)) by A59, A64, A107, Th5
.= (Comput (P2,s2,8)) . (DataLoc (((Comput (P1,s1,(m + 9))) . SBP),6)) by A59, A64, A75, A107, Th5 ;

A138: now

per cases ;

suppose A139: a <> DataLoc (((Comput (P2,s2,(m + 9))) . SBP),2) ; :: thesis:

hence (Comput (P1,s1,nn)) . a = (Comput (P1,s1,(m + 9))) . a by A106, A107, A113, SCMPDS_2:47
.= (Comput (P2,s2,(m + 9))) . a by A133, A134
.= (Comput (P2,s2,nn)) . a by A112, A139, SCMPDS_2:47 ;
:: thesis:

end;

suppose A140: a = DataLoc (((Comput (P2,s2,(m + 9))) . SBP),2) ; :: thesis:

hence (Comput (P1,s1,nn)) . a = (Comput (P1,s1,(m + 9))) . (DataLoc (((Comput (P1,s1,(m + 9))) . SBP),6)) by A106, A107, A113, SCMPDS_2:47
.= (Comput (P2,s2,(m + 9))) . (DataLoc (((Comput (P2,s2,(m + 9))) . SBP),6)) by A107, A113, A134, A137
.= (Comput (P2,s2,nn)) . a by A112, A140, SCMPDS_2:47 ;
:: thesis:

end;

per cases by A129, A130, A131, NAT_1:8;

suppose j <= 7 ; :: thesis:

hence ( IC (Comput (P1,s1,j)) = IC (Comput (P2,s2,j)) & (Comput (P1,s1,j)) . a = (Comput (P2,s2,j)) . a ) by A29, A31, A35, A36, A37, A38, A39, A41, A42, A128, Lm7, A27, A28; :: thesis:

end;

suppose A141: ( j >= 8 & j <= m + 8 ) ; :: thesis:

then consider j1 being Nat such that
A142: j = 8 + j1 by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 12;
A145: j1 <= m by A141, A142, XREAL_1:6;
thus IC (Comput (P1,s1,j)) = IC (Comput (P1,(Comput (P1,s1,8)),j1)) by A142, EXTPRO_1:4
.= IC (Comput (P2,(Comput (P2,s2,8)),j1)) by A81, A133, A145
.= IC (Comput (P2,s2,j)) by A142, EXTPRO_1:4 ; :: thesis:
thus (Comput (P1,s1,j)) . a = (Comput (P1,(Comput (P1,s1,8)),j1)) . a by A142, EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,8)),j1)) . a by A81, A133, A145
.= (Comput (P2,s2,j)) . a by A142, EXTPRO_1:4 ; :: thesis:

end;

suppose A146: j = m + 9 ; :: thesis:

hence IC (Comput (P1,s1,j)) = IC (Comput (P2,s2,j)) by A103, A109; :: thesis:
thus (Comput (P1,s1,j)) . a = (Comput (P2,s2,j)) . a by A133, A134, A146; :: thesis:

end;

suppose A147: j = nn ; :: thesis:

hence IC (Comput (P1,s1,j)) = IC (Comput (P2,s2,j)) by A114, A115; :: thesis:
thus (Comput (P1,s1,j)) . a = (Comput (P2,s2,j)) . a by A138, A147; :: thesis:

end;

A148: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A23);
let s1, s2 be State of SCMPDS; :: thesis:
assume that
A151: GCD-Algorithm c= P1 and
A152: GCD-Algorithm c= P2 and
A153: IC s1 = 5 and
A154: s1 . SBP > 0 and
A155: s1 . GBP = 0 and
A156: s1 . (DataLoc ((s1 . SBP),3)) >= 0 and
A157: s1 . (DataLoc ((s1 . SBP),2)) >= s1 . (DataLoc ((s1 . SBP),3)) and
A158: IC s2 = IC s1 and
A159: s2 . SBP = s1 . SBP and
A160: s2 . GBP = 0 and
A161: s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) and
A162: s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
reconsider m = s1 . (DataLoc ((s1 . SBP),3)) as Element of NAT by A156, INT_1:3;
S₁[m] by A148;
hence ex n being Element of NAT st
( CurInstr (P1,(Comput (P1,s1,n))) = return SBP & s1 . SBP = (Comput (P1,s1,n)) . SBP & CurInstr (P2,(Comput (P2,s2,n))) = return SBP & s2 . SBP = (Comput (P2,s2,n)) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP) + 1 holds
( s1 . (intpos j) = (Comput (P1,s1,n)) . (intpos j) & s2 . (intpos j) = (Comput (P2,s2,n)) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (P1,s1,k)) = IC (Comput (P2,s2,k)) & (Comput (P1,s1,k)) . a = (Comput (P2,s2,k)) . a ) ) ) by A153, A154, A155, A156, A157, A158, A159, A160, A161, A162, A151, A152; :: thesis: