let s be State of SCMPDS ; :: thesis: ( GCD-Algorithm c= s & IC s = 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc (s . SBP ),3) >= 0 & s . (DataLoc (s . SBP ),2) >= 0 implies ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = return SBP & s . SBP = (Comput (ProgramPart s),s,n) . SBP & (Comput (ProgramPart s),s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Comput (ProgramPart s),s,n) . (intpos j) ) ) )
set GA = GCD-Algorithm ;
set x = s . (DataLoc (s . SBP ),2);
set y = s . (DataLoc (s . SBP ),3);
set yy = s . (DataLoc (s . SBP ),3);
assume that
A1: GCD-Algorithm c= s and
A2: IC s = 5 and
A3: s . SBP > 0 and
A4: s . GBP = 0 and
A5: s . (DataLoc (s . SBP ),3) >= 0 and
A6: s . (DataLoc (s . SBP ),2) >= 0 ; :: thesis: ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = return SBP & s . SBP = (Comput (ProgramPart s),s,n) . SBP & (Comput (ProgramPart s),s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Comput (ProgramPart s),s,n) . (intpos j) ) )

per cases ( s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) or s . (DataLoc (s . SBP ),2) < s . (DataLoc (s . SBP ),3) ) ;

suppose s . (DataLoc (s . SBP ),2) >= s . (DataLoc (s . SBP ),3) ; :: thesis: ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = return SBP & s . SBP = (Comput (ProgramPart s),s,n) . SBP & (Comput (ProgramPart s),s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Comput (ProgramPart s),s,n) . (intpos j) ) )

hence ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = return SBP & s . SBP = (Comput (ProgramPart s),s,n) . SBP & (Comput (ProgramPart s),s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Comput (ProgramPart s),s,n) . (intpos j) ) ) by A1, A2, A3, A4, A5, Th16; :: thesis: verum

end;

suppose s . (DataLoc (s . SBP ),2) < s . (DataLoc (s . SBP ),3) ; :: thesis: ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = return SBP & s . SBP = (Comput (ProgramPart s),s,n) . SBP & (Comput (ProgramPart s),s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Comput (ProgramPart s),s,n) . (intpos j) ) )

then A7: s . (DataLoc (s . SBP ),3) > 0 by A6, XXREAL_0:2;
reconsider y = s . (DataLoc (s . SBP ),3) as Element of NAT by A5, INT_1:16;
reconsider pn = s . SBP as Element of NAT by A3, INT_1:16;
A8: pn = s . SBP ;
then A9: IC (Comput (ProgramPart s),s,7) = 5 + 7 by A1, A2, A4, A7, Lm4;
A10: Comput (ProgramPart s),s,8 = Exec (goto (- 7)),(Comput (ProgramPart s),s,7) by A1, A2, A4, A7, A8, Lm4;
A11: (Comput (ProgramPart s),s,7) . SBP = pn + 4 by A1, A2, A4, A7, Lm4;
A12: (Comput (ProgramPart s),s,7) . GBP = 0 by A1, A2, A4, A7, A8, Lm4;
A13: (Comput (ProgramPart s),s,7) . (intpos (pn + 7)) = (s . (DataLoc (s . SBP ),2)) mod y by A1, A2, A4, A7, Lm4;
A14: (Comput (ProgramPart s),s,7) . (intpos (pn + 6)) = y by A1, A2, A4, A7, Lm4;
A15: (Comput (ProgramPart s),s,7) . (intpos (pn + 4)) = pn by A1, A2, A4, A7, Lm4;
A16: (Comput (ProgramPart s),s,7) . (intpos (pn + 5)) = 11 by A1, A2, A4, A7, Lm4;
set s8 = Comput (ProgramPart s),s,8;
A17: IC (Comput (ProgramPart s),s,8) = ICplusConst (Comput (ProgramPart s),s,7),(- 7) by A10, SCMPDS_2:66
.= 5 by A9, Th6 ;
A18: GCD-Algorithm c= Comput (ProgramPart s),s,8 by A1, AMI_1:81;
A19: (Comput (ProgramPart s),s,8) . SBP = pn + 4 by A10, A11, SCMPDS_2:66;
A20: 4 <= pn + 4 by NAT_1:11;
then A21: (Comput (ProgramPart s),s,8) . SBP > 0 by A19, XXREAL_0:2;
A22: (Comput (ProgramPart s),s,8) . GBP = 0 by A10, A12, SCMPDS_2:66;
set x1 = (Comput (ProgramPart s),s,8) . (DataLoc ((Comput (ProgramPart s),s,8) . SBP ),2);
set y1 = (Comput (ProgramPart s),s,8) . (DataLoc ((Comput (ProgramPart s),s,8) . SBP ),3);
A23: (Comput (ProgramPart s),s,8) . (DataLoc ((Comput (ProgramPart s),s,8) . SBP ),2) = (Comput (ProgramPart s),s,8) . (intpos ((pn + 4) + 2)) by A19, Th5
.= y by A10, A14, SCMPDS_2:66 ;
A24: (Comput (ProgramPart s),s,8) . (DataLoc ((Comput (ProgramPart s),s,8) . SBP ),3) = (Comput (ProgramPart s),s,8) . (intpos ((pn + 4) + 3)) by A19, Th5
.= (s . (DataLoc (s . SBP ),2)) mod y by A10, A13, SCMPDS_2:66 ;
then (Comput (ProgramPart s),s,8) . (DataLoc ((Comput (ProgramPart s),s,8) . SBP ),3) < y by A7, NEWTON:79;
then consider m being Element of NAT such that
A25: CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart s),s,8)),(Comput (ProgramPart s),s,8),m)),(Comput (ProgramPart (Comput (ProgramPart s),s,8)),(Comput (ProgramPart s),s,8),m) = return SBP and
A26: (Comput (ProgramPart s),s,8) . SBP = (Comput (ProgramPart (Comput (ProgramPart s),s,8)),(Comput (ProgramPart s),s,8),m) . SBP and
A27: (Comput (ProgramPart (Comput (ProgramPart s),s,8)),(Comput (ProgramPart s),s,8),m) . (DataLoc ((Comput (ProgramPart s),s,8) . SBP ),2) = ((Comput (ProgramPart s),s,8) . (DataLoc ((Comput (ProgramPart s),s,8) . SBP ),2)) gcd ((Comput (ProgramPart s),s,8) . (DataLoc ((Comput (ProgramPart s),s,8) . SBP ),3)) and
A28: for j being Element of NAT st 1 < j & j <= ((Comput (ProgramPart s),s,8) . SBP ) + 1 holds
(Comput (ProgramPart s),s,8) . (intpos j) = (Comput (ProgramPart (Comput (ProgramPart s),s,8)),(Comput (ProgramPart s),s,8),m) . (intpos j) by A5, A17, A18, A21, A22, A23, A24, Th16, NEWTON:78;
set s9 = Comput (ProgramPart s),s,(m + 8);
T9: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,8) by AMI_1:123;
then A29: (Comput (ProgramPart s),s,8) . SBP = (Comput (ProgramPart s),s,(m + 8)) . SBP by A26, AMI_1:51;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,8) by AMI_1:123;
x: Comput (ProgramPart s),s,(m + 8) = Comput (ProgramPart s),(Comput (ProgramPart s),s,8),m by AMI_1:51;
S: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(m + 8)) by AMI_1:123;
A30: Comput (ProgramPart s),s,(m + (8 + 1)) = Comput (ProgramPart s),s,((m + 8) + 1)
.= Following (ProgramPart s),(Comput (ProgramPart s),s,(m + 8)) by AMI_1:14
.= Exec (return SBP ),(Comput (ProgramPart s),s,(m + 8)) by A25, x, T, S ;
A31: 1 < pn + 4 by A20, XXREAL_0:2;
pn + 4 < ((Comput (ProgramPart s),s,8) . SBP ) + 1 by A19, XREAL_1:31;
then A32: (Comput (ProgramPart s),s,8) . (intpos (pn + 4)) = (Comput (ProgramPart (Comput (ProgramPart s),s,8)),(Comput (ProgramPart s),s,8),m) . (intpos (pn + 4)) by A28, A31
.= (Comput (ProgramPart s),s,(m + 8)) . (intpos (pn + 4)) by T9, AMI_1:51 ;
5 <= pn + 5 by NAT_1:11;
then A33: 1 < pn + 5 by XXREAL_0:2;
A34: 11 = (Comput (ProgramPart s),s,8) . (intpos (pn + 5)) by A10, A16, SCMPDS_2:66
.= (Comput (ProgramPart (Comput (ProgramPart s),s,8)),(Comput (ProgramPart s),s,8),m) . (intpos (pn + 5)) by A19, A28, A33
.= (Comput (ProgramPart s),s,(m + 8)) . (intpos ((pn + 4) + 1)) by T9, AMI_1:51
.= (Comput (ProgramPart s),s,(m + 8)) . (DataLoc ((Comput (ProgramPart s),s,(m + 8)) . SBP ),RetIC ) by A19, A29, Th5, SCMPDS_1:def 23 ;
Y: (ProgramPart (Comput (ProgramPart s),s,(m + 9))) /. (IC (Comput (ProgramPart s),s,(m + 9))) = (Comput (ProgramPart s),s,(m + 9)) . (IC (Comput (ProgramPart s),s,(m + 9))) by COMPOS_1:38;
A35: IC (Comput (ProgramPart s),s,(m + 9)) = (abs ((Comput (ProgramPart s),s,(m + 8)) . (DataLoc ((Comput (ProgramPart s),s,(m + 8)) . SBP ),RetIC ))) + 2 by A30, SCMPDS_2:70
.= 11 + 2 by A34, Th3 ;
then A36: CurInstr (ProgramPart (Comput (ProgramPart s),s,(m + 9))),(Comput (ProgramPart s),s,(m + 9)) = s . 13 by Y, AMI_1:54
.= SBP ,2 := SBP ,6 by A1, Lm1 ;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,(m + 9)) by AMI_1:123;
A37: Comput (ProgramPart s),s,(m + (9 + 1)) = Comput (ProgramPart s),s,((m + 9) + 1)
.= Following (ProgramPart s),(Comput (ProgramPart s),s,(m + 9)) by AMI_1:14
.= Exec (SBP ,2 := SBP ,6),(Comput (ProgramPart s),s,(m + 9)) by A36, T ;
A38: (Comput (ProgramPart s),s,(m + 9)) . SBP = (Comput (ProgramPart s),s,(m + 8)) . (DataLoc (pn + 4),RetSP ) by A19, A29, A30, SCMPDS_2:70
.= (Comput (ProgramPart s),s,(m + 8)) . (intpos ((pn + 4) + 0 )) by Th5, SCMPDS_1:def 22
.= pn by A10, A15, A32, SCMPDS_2:66 ;
A39: (Comput (ProgramPart s),s,(m + 9)) . (intpos (pn + 6)) = (Comput (ProgramPart s),s,(m + 8)) . (intpos ((pn + 4) + 2)) by A30, Lm3, SCMPDS_2:70
.= (Comput (ProgramPart s),s,(m + 8)) . (DataLoc ((Comput (ProgramPart s),s,8) . SBP ),2) by A19, Th5
.= ((Comput (ProgramPart s),s,8) . (DataLoc ((Comput (ProgramPart s),s,8) . SBP ),2)) gcd ((Comput (ProgramPart s),s,8) . (DataLoc ((Comput (ProgramPart s),s,8) . SBP ),3)) by A27, T9, AMI_1:51 ;
Y: (ProgramPart (Comput (ProgramPart s),s,(m + 10))) /. (IC (Comput (ProgramPart s),s,(m + 10))) = (Comput (ProgramPart s),s,(m + 10)) . (IC (Comput (ProgramPart s),s,(m + 10))) by COMPOS_1:38;
IC (Comput (ProgramPart s),s,(m + 10)) = succ (IC (Comput (ProgramPart s),s,(m + 9))) by A37, SCMPDS_2:59
.= 13 + 1 by A35 ;
then A40: CurInstr (ProgramPart (Comput (ProgramPart s),s,(m + 10))),(Comput (ProgramPart s),s,(m + 10)) = s . 14 by Y, AMI_1:54
.= return SBP by A1, Lm1 ;

hereby :: thesis: verum

take n = m + 10; :: thesis: ( CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = return SBP & (Comput (ProgramPart s),s,n) . SBP = s . SBP & (Comput (ProgramPart s),s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Comput (ProgramPart s),s,n) . (intpos j) ) )
thus CurInstr (ProgramPart (Comput (ProgramPart s),s,n)),(Comput (ProgramPart s),s,n) = return SBP by A40; :: thesis: ( (Comput (ProgramPart s),s,n) . SBP = s . SBP & (Comput (ProgramPart s),s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Comput (ProgramPart s),s,n) . (intpos j) ) )
A41: DataLoc ((Comput (ProgramPart s),s,(m + 9)) . SBP ),2 = intpos (pn + 2) by A38, Th5;
hence (Comput (ProgramPart s),s,n) . SBP = s . SBP by A37, A38, Lm3, SCMPDS_2:59; :: thesis: ( (Comput (ProgramPart s),s,n) . (DataLoc (s . SBP ),2) = (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) & ( for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Comput (ProgramPart s),s,n) . (intpos j) ) )
thus (Comput (ProgramPart s),s,n) . (DataLoc (s . SBP ),2) = (Comput (ProgramPart s),s,(m + 9)) . (DataLoc pn,6) by A37, A38, SCMPDS_2:59
.= (s . (DataLoc (s . SBP ),3)) gcd ((s . (DataLoc (s . SBP ),2)) mod (s . (DataLoc (s . SBP ),3))) by A23, A24, A39, Th5
.= (s . (DataLoc (s . SBP ),2)) gcd (s . (DataLoc (s . SBP ),3)) by A6, A7, NAT_D:30 ; :: thesis: for j being Element of NAT st 1 < j & j <= (s . SBP ) + 1 holds
s . (intpos j) = (Comput (ProgramPart s),s,n) . (intpos j)

hereby :: thesis: verum

let j be Element of NAT ; :: thesis: ( 1 < j & j <= (s . SBP ) + 1 implies s . (intpos j) = (Comput (ProgramPart s),s,n) . (intpos j) )
assume that
A42: 1 < j and
A43: j <= (s . SBP ) + 1 ; :: thesis: s . (intpos j) = (Comput (ProgramPart s),s,n) . (intpos j)
s . SBP <= (Comput (ProgramPart s),s,8) . SBP by A19, NAT_1:11;
then (s . SBP ) + 1 <= ((Comput (ProgramPart s),s,8) . SBP ) + 1 by XREAL_1:8;
then A44: j <= ((Comput (ProgramPart s),s,8) . SBP ) + 1 by A43, XXREAL_0:2;
A45: (Comput (ProgramPart s),s,(m + 9)) . (intpos j) = (Comput (ProgramPart s),s,(m + 8)) . (intpos j) by A30, A42, AMI_3:52, SCMPDS_2:70
.= (Comput (ProgramPart (Comput (ProgramPart s),s,8)),(Comput (ProgramPart s),s,8),m) . (intpos j) by T9, AMI_1:51
.= (Comput (ProgramPart s),s,8) . (intpos j) by A28, A42, A44 ;
A46: pn + 1 < pn + 2 by XREAL_1:8;
(Comput (ProgramPart s),s,7) . (intpos j) = s . (intpos j) by A1, A2, A4, A7, A8, A42, A43, Lm5;
hence s . (intpos j) = (Comput (ProgramPart s),s,8) . (intpos j) by A10, SCMPDS_2:66
.= (Comput (ProgramPart s),s,n) . (intpos j) by A37, A41, A43, A45, A46, AMI_3:52, SCMPDS_2:59 ;
:: thesis: verum

end;

end;

end;

end;