let P1, P2 be Instruction-Sequence of SCMPDS; :: thesis:
set GA = GCD-Algorithm ;
defpred S₁[ 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 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 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 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
A2: GCD-Algorithm c= P1 and
A3: GCD-Algorithm c= P2 ; :: thesis:
assume A4: IC s1 = 5 ; :: thesis:
assume that
s1 . SBP > 0 and
s1 . GBP = 0 ; :: thesis:
assume A5: 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
A6: IC s2 = IC s1 and
A7: s2 . SBP = s1 . SBP and
s2 . GBP = 0 ; :: thesis:
assume that
s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) and
A8: s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
A9: P1 /. (IC s1) = P1 . (IC s1) by PBOOLE:143;
A10: 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 A4, A9, Lm1, A2 ;
A11: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143;
A12: 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 A4, A6, A11, Lm1, A3 ;
A13: IC (Comput (P1,s1,1)) = ICplusConst (s1,9) by A5, A10, SCMPDS_2:56
.= 5 + 9 by A4, SCMPDS_6:12 ;
A14: IC (Comput (P2,s2,1)) = ICplusConst (s2,9) by A5, A7, A8, A12, SCMPDS_2:56
.= 5 + 9 by A4, A6, SCMPDS_6:12 ;
take n = 1; :: thesis:
A15: 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 A13, A15
.= return SBP by Lm1, A2 ; :: thesis:
thus (Comput (P1,s1,n)) . SBP = s1 . SBP by A10, SCMPDS_2:56; :: thesis:
A16: 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 A14, A16
.= return SBP by Lm1, A3 ; :: thesis:
thus (Comput (P2,s2,n)) . SBP = s2 . SBP by A12, SCMPDS_2:56; :: thesis:
thus for j being 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 A10, A12, SCMPDS_2:56; :: thesis:

hereby :: thesis:

let k be Nat; :: thesis:
let a be Int_position; :: thesis:
assume that
A17: k <= n and
A18: s1 . a = s2 . a ; :: thesis:

per cases by A17, NAT_1:25;

suppose A19: k = 0 ; :: thesis:

hence IC (Comput (P1,s1,k)) = IC s2 by A6, EXTPRO_1:2
.= IC (Comput (P2,s2,k)) by A19, EXTPRO_1:2 ;
:: thesis:
thus (Comput (P1,s1,k)) . a = s1 . a by A19, EXTPRO_1:2
.= (Comput (P2,s2,k)) . a by A18, A19, EXTPRO_1:2 ; :: thesis:

end;

suppose A20: k = 1 ; :: thesis:

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

end;

A21: now :: thesis:

let k be Nat; :: thesis:
assume A22: 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
A23: GCD-Algorithm c= P1 and
A24: GCD-Algorithm c= P2 ; :: thesis:
assume A25: IC s1 = 5 ; :: thesis:
assume that
A26: s1 . SBP > 0 and
A27: s1 . GBP = 0 ; :: thesis:
assume A28: s1 . (DataLoc ((s1 . SBP),3)) <= k + 1 ; :: thesis:
assume A29: s1 . (DataLoc ((s1 . SBP),3)) >= 0 ; :: thesis:
assume A30: s1 . (DataLoc ((s1 . SBP),2)) >= s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
assume that
A31: IC s2 = IC s1 and
A32: s2 . SBP = s1 . SBP and
A33: s2 . GBP = 0 ; :: thesis:
assume that
A34: s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) and
A35: s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
reconsider y = s1 . (DataLoc ((s1 . SBP),3)) as Element of NAT by A29, INT_1:3;

per cases by A28, NAT_1:8;

suppose y <= k ; :: thesis:

hence ex n being 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 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 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 A22, A25, A26, A27, A30, A31, A32, A33, A34, A35, A23, A24; :: thesis:

end;

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

then A37: y > 0 ;
reconsider n = s1 . SBP as Element of NAT by A26, INT_1:3;
A38: n = s1 . SBP ;
set s8 = Comput (P1,s1,8);
set t8 = Comput (P2,s2,8);
A39: IC (Comput (P1,s1,7)) = 5 + 7 by A25, A27, A34, A37, A38, Lm6, A23;
A40: Comput (P1,s1,8) = Exec ((goto (- 7)),(Comput (P1,s1,7))) by A25, A27, A34, A37, A38, Lm6, A23;
A41: (Comput (P1,s1,7)) . SBP = n + 4 by A25, A27, A34, A37, Lm6, A23;
A42: (Comput (P1,s1,7)) . GBP = 0 by A25, A27, A34, A37, A38, Lm6, A23;
A43: (Comput (P1,s1,7)) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A25, A27, A34, A37, Lm6, A23;
A44: (Comput (P1,s1,7)) . (intpos (n + 6)) = s1 . (intpos (n + 3)) by A25, A27, A34, A37, Lm6, A23;
A45: IC (Comput (P2,s2,7)) = 5 + 7 by A25, A31, A32, A33, A34, A35, A37, A38, Lm6, A24;
A46: Comput (P2,s2,8) = Exec ((goto (- 7)),(Comput (P2,s2,7))) by A25, A31, A32, A33, A34, A35, A37, A38, Lm6, A24;
A47: (Comput (P2,s2,7)) . SBP = n + 4 by A25, A31, A32, A33, A34, A35, A37, Lm6, A24;
A48: (Comput (P2,s2,7)) . GBP = 0 by A25, A31, A32, A33, A34, A35, A37, A38, Lm6, A24;
A49: (Comput (P2,s2,7)) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A25, A27, A31, A32, A33, A34, A35, A37, Lm6, A24;
A50: (Comput (P2,s2,7)) . (intpos (n + 6)) = s1 . (intpos (n + 3)) by A25, A27, A31, A32, A33, A34, A35, A37, Lm6, A24;
A51: (Comput (P1,s1,7)) . (intpos (n + 4)) = n by A25, A27, A34, A37, Lm6, A23;
A52: (Comput (P1,s1,7)) . (intpos (n + 5)) = 11 by A25, A27, A34, A37, Lm6, A23;
A53: (Comput (P2,s2,7)) . (intpos (n + 4)) = n by A25, A31, A32, A33, A34, A35, A37, Lm6, A24;
A54: (Comput (P2,s2,7)) . (intpos (n + 5)) = 11 by A25, A31, A32, A33, A34, A35, A37, Lm6, A24;
A55: DataLoc ((n + 4),2) = intpos ((n + 4) + 2) by Th1
.= intpos (n + (4 + 2)) ;
A56: DataLoc ((n + 4),3) = intpos ((n + 4) + 3) by Th1
.= intpos (n + (4 + 3)) ;
A57: IC (Comput (P1,s1,8)) = ICplusConst ((Comput (P1,s1,7)),(- 7)) by A40, SCMPDS_2:54
.= 5 by A39, Th2 ;
A58: (Comput (P1,s1,8)) . SBP = n + 4 by A40, A41, SCMPDS_2:54;
A59: 4 <= n + 4 by NAT_1:11;
A60: (Comput (P1,s1,8)) . SBP > 0 by A58;
A61: (Comput (P1,s1,8)) . GBP = 0 by A40, A42, 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));
A62: (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),2)) = s1 . (intpos (n + 3)) by A40, A44, A55, A58, SCMPDS_2:54
.= y by Th1 ;
A63: (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),3)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A40, A43, A56, A58, SCMPDS_2:54
.= (s1 . (intpos (n + 2))) mod y by Th1 ;
then A64: (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),3)) < y by A36, NEWTON:65;
then A65: (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),3)) <= k by A36, INT_1:7;
A66: IC (Comput (P2,s2,8)) = ICplusConst ((Comput (P2,s2,7)),(- 7)) by A46, SCMPDS_2:54
.= IC (Comput (P1,s1,8)) by A45, A57, Th2 ;
A67: (Comput (P2,s2,8)) . SBP = (Comput (P1,s1,8)) . SBP by A46, A47, A58, SCMPDS_2:54;
A68: (Comput (P2,s2,8)) . GBP = 0 by A46, A48, SCMPDS_2:54;
set x3 = (Comput (P2,s2,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),2));
A69: (Comput (P2,s2,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),2)) = s1 . (intpos (n + 3)) by A46, A50, A55, A58, SCMPDS_2:54
.= (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),2)) by A62, Th1 ;
(Comput (P2,s2,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),3)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A46, A49, A56, A58, SCMPDS_2:54
.= (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),3)) by A63, Th1 ;
then consider m being Nat such that
A70: CurInstr (P1,(Comput (P1,(Comput (P1,s1,8)),m))) = return SBP and
A71: (Comput (P1,s1,8)) . SBP = (Comput (P1,(Comput (P1,s1,8)),m)) . SBP and
A72: CurInstr (P2,(Comput (P2,(Comput (P2,s2,8)),m))) = return SBP and
A73: (Comput (P2,s2,8)) . SBP = (Comput (P2,(Comput (P2,s2,8)),m)) . SBP and
A74: for j being 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
A75: for k being 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 A22, A57, A60, A61, A62, A63, A64, A65, A66, A67, A68, A69, A23, A24, NEWTON:64;
set s9 = Comput (P1,s1,(m + 8));
set t9 = Comput (P2,s2,(m + 8));
A76: (Comput (P1,s1,8)) . SBP = (Comput (P1,s1,(m + 8))) . SBP by A71, EXTPRO_1:4;
A77: Comput (P1,s1,(m + 8)) = Comput (P1,(Comput (P1,s1,8)),m) by EXTPRO_1:4;
A78: 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 A70, A77 ;
A79: 1 < n + 4 by A59, XXREAL_0:2;
A80: n + 4 < ((Comput (P1,s1,8)) . SBP) + 1 by A58, XREAL_1:29;
then A81: (Comput (P1,s1,8)) . (intpos (n + 4)) = (Comput (P1,(Comput (P1,s1,8)),m)) . (intpos (n + 4)) by A74, A79
.= (Comput (P1,s1,(m + 8))) . (intpos (n + 4)) by EXTPRO_1:4 ;
5 <= n + 5 by NAT_1:11;
then A82: 1 < n + 5 by XXREAL_0:2;
A83: intpos (n + (4 + 1)) = intpos ((n + 4) + 1)
.= DataLoc ((n + 4),1) by Th1 ;
A84: 11 = (Comput (P1,s1,8)) . (intpos (n + 5)) by A40, A52, SCMPDS_2:54
.= (Comput (P1,(Comput (P1,s1,8)),m)) . (intpos (n + 5)) by A58, A74, A82
.= (Comput (P1,s1,(m + 8))) . (DataLoc (((Comput (P1,s1,(m + 8))) . SBP),RetIC)) by A58, A76, A83, EXTPRO_1:4, SCMPDS_I:def 14 ;
A85: (Comput (P2,s2,(m + 8))) . SBP = n + 4 by A58, A67, A73, EXTPRO_1:4;
A86: Comput (P2,s2,(m + 8)) = Comput (P2,(Comput (P2,s2,8)),m) by EXTPRO_1:4;
A87: 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 A72, A86 ;
A88: (Comput (P2,s2,8)) . (intpos (n + 4)) = (Comput (P2,(Comput (P2,s2,8)),m)) . (intpos (n + 4)) by A74, A79, A80
.= (Comput (P2,s2,(m + 8))) . (intpos (n + 4)) by EXTPRO_1:4 ;
A89: 11 = (Comput (P2,s2,8)) . (intpos (n + 5)) by A46, A54, SCMPDS_2:54
.= (Comput (P2,(Comput (P2,s2,8)),m)) . (intpos (n + 5)) by A58, A74, A82
.= (Comput (P2,s2,(m + 8))) . (DataLoc (((Comput (P2,s2,(m + 8))) . SBP),RetIC)) by A83, A85, EXTPRO_1:4, SCMPDS_I:def 14 ;
A90: P1 /. (IC (Comput (P1,s1,(m + 9)))) = P1 . (IC (Comput (P1,s1,(m + 9)))) by PBOOLE:143;
A91: IC (Comput (P1,s1,(m + 9))) = |.((Comput (P1,s1,(m + 8))) . (DataLoc (((Comput (P1,s1,(m + 8))) . SBP),RetIC))).| + 2 by A78, SCMPDS_2:58
.= 11 + 2 by A84, ABSVALUE:29 ;
then A92: CurInstr (P1,(Comput (P1,s1,(m + 9)))) = P1 . 13 by A90
.= (SBP,2) := (SBP,6) by Lm1, A23 ;
A93: 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 A92 ;
A94: (Comput (P1,s1,(m + 9))) . SBP = (Comput (P1,s1,(m + 8))) . (DataLoc ((n + 4),RetSP)) by A58, A76, A78, SCMPDS_2:58
.= (Comput (P1,s1,(m + 8))) . (intpos ((n + 4) + 0)) by Th1, SCMPDS_I:def 13
.= n by A40, A51, A81, SCMPDS_2:54 ;
A95: P2 /. (IC (Comput (P2,s2,(m + 9)))) = P2 . (IC (Comput (P2,s2,(m + 9)))) by PBOOLE:143;
A96: IC (Comput (P2,s2,(m + 9))) = |.((Comput (P2,s2,(m + 8))) . (DataLoc (((Comput (P2,s2,(m + 8))) . SBP),RetIC))).| + 2 by A87, SCMPDS_2:58
.= 11 + 2 by A89, ABSVALUE:29 ;
then A97: CurInstr (P2,(Comput (P2,s2,(m + 9)))) = P2 . 13 by A95
.= (SBP,2) := (SBP,6) by Lm1, A24 ;
A98: 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 A97 ;
A99: (Comput (P2,s2,(m + 9))) . SBP = (Comput (P2,s2,(m + 8))) . (DataLoc ((n + 4),RetSP)) by A85, A87, SCMPDS_2:58
.= (Comput (P2,s2,(m + 8))) . (intpos ((n + 4) + 0)) by Th1, SCMPDS_I:def 13
.= n by A46, A53, A88, SCMPDS_2:54 ;
A100: IC (Comput (P1,s1,(m + 10))) = (IC (Comput (P1,s1,(m + 9)))) + 1 by A93, SCMPDS_2:47
.= 13 + 1 by A91 ;
A101: IC (Comput (P2,s2,(m + 10))) = (IC (Comput (P2,s2,(m + 9)))) + 1 by A98, SCMPDS_2:47
.= 13 + 1 by A96 ;

hereby :: thesis:

reconsider nn = m + 10 as Nat ;
take nn = nn; :: thesis:
A102: 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 A100, A102
.= return SBP by Lm1, A23 ; :: thesis:
A103: P2 /. (IC (Comput (P2,s2,nn))) = P2 . (IC (Comput (P2,s2,nn))) by PBOOLE:143;
A104: DataLoc (((Comput (P1,s1,(m + 9))) . SBP),2) = intpos (n + 2) by A94, Th1;
hence (Comput (P1,s1,nn)) . SBP = s1 . SBP by A93, A94, Lm3, SCMPDS_2:47; :: thesis:
thus CurInstr (P2,(Comput (P2,s2,nn))) = P2 . 14 by A101, A103
.= return SBP by Lm1, A24 ; :: thesis:
A105: DataLoc (((Comput (P2,s2,(m + 9))) . SBP),2) = intpos (n + 2) by A99, Th1;
hence (Comput (P2,s2,nn)) . SBP = s2 . SBP by A32, A98, A99, Lm3, SCMPDS_2:47; :: thesis:

hereby :: thesis:

let j be Nat; :: thesis:
assume that
A106: 1 < j and
A107: j <= (s1 . SBP) + 1 ; :: thesis:
s1 . SBP <= (Comput (P1,s1,8)) . SBP by A58, NAT_1:11;
then (s1 . SBP) + 1 <= ((Comput (P1,s1,8)) . SBP) + 1 by XREAL_1:6;
then A108: j <= ((Comput (P1,s1,8)) . SBP) + 1 by A107, XXREAL_0:2;
A109: (Comput (P1,s1,(m + 9))) . (intpos j) = (Comput (P1,s1,(m + 8))) . (intpos j) by A78, A106, 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 A74, A106, A108 ;
A110: n + 1 < n + 2 by XREAL_1:6;
(Comput (P1,s1,7)) . (intpos j) = s1 . (intpos j) by A25, A27, A36, A38, A106, A107, Lm5, A23;
hence s1 . (intpos j) = (Comput (P1,s1,8)) . (intpos j) by A40, SCMPDS_2:54
.= (Comput (P1,s1,nn)) . (intpos j) by A93, A104, A107, A109, A110, AMI_3:10, SCMPDS_2:47 ;
:: thesis:
A111: (Comput (P2,s2,(m + 9))) . (intpos j) = (Comput (P2,s2,(m + 8))) . (intpos j) by A87, A106, 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 A74, A106, A108 ;
j <= n + 1 by A107;
then (Comput (P2,s2,7)) . (intpos j) = s2 . (intpos j) by A25, A31, A32, A33, A35, A36, A106, Lm5, A24;
hence s2 . (intpos j) = (Comput (P2,s2,8)) . (intpos j) by A46, SCMPDS_2:54
.= (Comput (P2,s2,nn)) . (intpos j) by A98, A105, A107, A110, A111, AMI_3:10, SCMPDS_2:47 ;
:: thesis:

end;

hereby :: thesis:

let j be Nat; :: thesis:
let a be Int_position; :: thesis:
assume that
A112: j <= nn and
A113: s1 . a = s2 . a ; :: thesis:
nn = (m + 9) + 1 ;
then A114: ( j <= m + 9 or j = nn ) by A112, NAT_1:8;
A115: m + (8 + 1) = (m + 8) + 1 ;

A116: now :: thesis:

assume A117: 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 A117; :: thesis:

end;

A118: (Comput (P1,s1,8)) . a = (Comput (P1,s1,7)) . a by A40, SCMPDS_2:54
.= (Comput (P2,s2,7)) . a by A25, A27, A31, A32, A33, A23, A24, A34, A35, A37, A38, A113, Lm7
.= (Comput (P2,s2,8)) . a by A46, SCMPDS_2:54 ;

A119: now :: thesis:

let b be Int_position; :: thesis:
assume A120: (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 A94, A99; :: thesis:

end;

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

hence (Comput (P1,s1,(m + 9))) . b = (Comput (P1,s1,(m + 8))) . b by A78, SCMPDS_2:58
.= (Comput (P1,(Comput (P1,s1,8)),m)) . b by EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,8)),m)) . b by A75, A120
.= (Comput (P2,s2,(m + 8))) . b by EXTPRO_1:4
.= (Comput (P2,s2,(m + 9))) . b by A87, A121, SCMPDS_2:58 ;
:: thesis:

end;

A122: (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,(m + 9))) . SBP),6)) = (Comput (P1,s1,8)) . (DataLoc (((Comput (P1,s1,8)) . SBP),2)) by A55, A58, A94, Th1
.= (Comput (P2,s2,8)) . (DataLoc (((Comput (P1,s1,(m + 9))) . SBP),6)) by A55, A58, A69, A94, Th1 ;

A123: now :: thesis:

per cases ;

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

hence (Comput (P1,s1,nn)) . a = (Comput (P1,s1,(m + 9))) . a by A93, A94, A99, SCMPDS_2:47
.= (Comput (P2,s2,(m + 9))) . a by A118, A119
.= (Comput (P2,s2,nn)) . a by A98, A124, SCMPDS_2:47 ;
:: thesis:

end;

suppose A125: 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 A93, A94, A99, SCMPDS_2:47
.= (Comput (P2,s2,(m + 9))) . (DataLoc (((Comput (P2,s2,(m + 9))) . SBP),6)) by A94, A99, A119, A122
.= (Comput (P2,s2,nn)) . a by A98, A125, SCMPDS_2:47 ;
:: thesis:

end;

per cases by A114, A115, A116, 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 A25, A27, A31, A32, A33, A34, A35, A37, A38, A113, Lm7, A23, A24; :: thesis:

end;

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

then consider j1 being Nat such that
A127: j = 8 + j1 by NAT_1:10;
reconsider j1 = j1 as Nat ;
A128: j1 <= m by A126, A127, XREAL_1:6;
thus IC (Comput (P1,s1,j)) = IC (Comput (P1,(Comput (P1,s1,8)),j1)) by A127, EXTPRO_1:4
.= IC (Comput (P2,(Comput (P2,s2,8)),j1)) by A75, A118, A128
.= IC (Comput (P2,s2,j)) by A127, EXTPRO_1:4 ; :: thesis:
thus (Comput (P1,s1,j)) . a = (Comput (P1,(Comput (P1,s1,8)),j1)) . a by A127, EXTPRO_1:4
.= (Comput (P2,(Comput (P2,s2,8)),j1)) . a by A75, A118, A128
.= (Comput (P2,s2,j)) . a by A127, EXTPRO_1:4 ; :: thesis:

end;

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

hence IC (Comput (P1,s1,j)) = IC (Comput (P2,s2,j)) by A91, A96; :: thesis:
thus (Comput (P1,s1,j)) . a = (Comput (P2,s2,j)) . a by A118, A119, A129; :: thesis:

end;

suppose A130: j = nn ; :: thesis:

hence IC (Comput (P1,s1,j)) = IC (Comput (P2,s2,j)) by A100, A101; :: thesis:
thus (Comput (P1,s1,j)) . a = (Comput (P2,s2,j)) . a by A123, A130; :: thesis:

end;

A131: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A21);
let s1, s2 be State of SCMPDS; :: thesis:
assume that
A132: GCD-Algorithm c= P1 and
A133: GCD-Algorithm c= P2 and
A134: IC s1 = 5 and
A135: s1 . SBP > 0 and
A136: s1 . GBP = 0 and
A137: s1 . (DataLoc ((s1 . SBP),3)) >= 0 and
A138: s1 . (DataLoc ((s1 . SBP),2)) >= s1 . (DataLoc ((s1 . SBP),3)) and
A139: IC s2 = IC s1 and
A140: s2 . SBP = s1 . SBP and
A141: s2 . GBP = 0 and
A142: s2 . (DataLoc ((s1 . SBP),2)) = s1 . (DataLoc ((s1 . SBP),2)) and
A143: s2 . (DataLoc ((s1 . SBP),3)) = s1 . (DataLoc ((s1 . SBP),3)) ; :: thesis:
reconsider m = s1 . (DataLoc ((s1 . SBP),3)) as Element of NAT by A137, INT_1:3;
S₁[m] by A131;
hence ex n being 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 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 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 A134, A135, A136, A138, A139, A140, A141, A142, A143, A132, A133; :: thesis: