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

then A7: s . (DataLoc ((s . SBP),3)) > 0 by A6;
reconsider y = s . (DataLoc ((s . SBP),3)) as Element of NAT by A5, INT_1:3;
reconsider pn = s . SBP as Element of NAT by A3, INT_1:3;
A8: pn = s . SBP ;
then A9: IC (Comput (P,s,7)) = 5 + 7 by A2, A4, A7, Lm4, A1;
A10: Comput (P,s,8) = Exec ((goto (- 7)),(Comput (P,s,7))) by A2, A4, A7, A8, Lm4, A1;
A11: (Comput (P,s,7)) . SBP = pn + 4 by A2, A4, A7, Lm4, A1;
A12: (Comput (P,s,7)) . GBP = 0 by A2, A4, A7, A8, Lm4, A1;
A13: (Comput (P,s,7)) . (intpos (pn + 7)) = (s . (DataLoc ((s . SBP),2))) mod y by A2, A4, A7, Lm4, A1;
A14: (Comput (P,s,7)) . (intpos (pn + 6)) = y by A2, A4, A7, Lm4, A1;
A15: (Comput (P,s,7)) . (intpos (pn + 4)) = pn by A2, A4, A7, Lm4, A1;
A16: (Comput (P,s,7)) . (intpos (pn + 5)) = 11 by A2, A4, A7, Lm4, A1;
set s8 = Comput (P,s,8);
A17: IC (Comput (P,s,8)) = ICplusConst ((Comput (P,s,7)),(- 7)) by A10, SCMPDS_2:54
.= 5 by A9, Th2 ;
A18: (Comput (P,s,8)) . SBP = pn + 4 by A10, A11, SCMPDS_2:54;
A19: 4 <= pn + 4 by NAT_1:11;
A20: (Comput (P,s,8)) . SBP > 0 by A18;
A21: (Comput (P,s,8)) . GBP = 0 by A10, A12, SCMPDS_2:54;
set x1 = (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),2));
set y1 = (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3));
A22: (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),2)) = (Comput (P,s,8)) . (intpos ((pn + 4) + 2)) by A18, Th1
.= y by A10, A14, SCMPDS_2:54 ;
A23: (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3)) = (Comput (P,s,8)) . (intpos ((pn + 4) + 3)) by A18, Th1
.= (s . (DataLoc ((s . SBP),2))) mod y by A10, A13, SCMPDS_2:54 ;
then (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3)) < y by A7, NEWTON:65;
then consider m being Nat such that
A24: CurInstr (P,(Comput (P,(Comput (P,s,8)),m))) = return SBP and
A25: (Comput (P,s,8)) . SBP = (Comput (P,(Comput (P,s,8)),m)) . SBP and
A26: (Comput (P,(Comput (P,s,8)),m)) . (DataLoc (((Comput (P,s,8)) . SBP),2)) = ((Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),2))) gcd ((Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3))) and
A27: for j being Nat st 1 < j & j <= ((Comput (P,s,8)) . SBP) + 1 holds
(Comput (P,s,8)) . (intpos j) = (Comput (P,(Comput (P,s,8)),m)) . (intpos j) by A17, A20, A21, A22, A23, Th12, A1, NEWTON:64;
set s9 = Comput (P,s,(m + 8));
A28: (Comput (P,s,8)) . SBP = (Comput (P,s,(m + 8))) . SBP by A25, EXTPRO_1:4;
A29: Comput (P,s,(m + 8)) = Comput (P,(Comput (P,s,8)),m) by EXTPRO_1:4;
A30: Comput (P,s,(m + (8 + 1))) = Comput (P,s,((m + 8) + 1))
.= Following (P,(Comput (P,s,(m + 8)))) by EXTPRO_1:3
.= Exec ((return SBP),(Comput (P,s,(m + 8)))) by A24, A29 ;
A31: 1 < pn + 4 by A19, XXREAL_0:2;
pn + 4 < ((Comput (P,s,8)) . SBP) + 1 by A18, XREAL_1:29;
then A32: (Comput (P,s,8)) . (intpos (pn + 4)) = (Comput (P,(Comput (P,s,8)),m)) . (intpos (pn + 4)) by A27, A31
.= (Comput (P,s,(m + 8))) . (intpos (pn + 4)) by EXTPRO_1:4 ;
5 <= pn + 5 by NAT_1:11;
then A33: 1 < pn + 5 by XXREAL_0:2;
A34: 11 = (Comput (P,s,8)) . (intpos (pn + 5)) by A10, A16, SCMPDS_2:54
.= (Comput (P,(Comput (P,s,8)),m)) . (intpos (pn + 5)) by A18, A27, A33
.= (Comput (P,s,(m + 8))) . (intpos ((pn + 4) + 1)) by EXTPRO_1:4
.= (Comput (P,s,(m + 8))) . (DataLoc (((Comput (P,s,(m + 8))) . SBP),RetIC)) by A18, A28, Th1, SCMPDS_I:def 14 ;
A35: P /. (IC (Comput (P,s,(m + 9)))) = P . (IC (Comput (P,s,(m + 9)))) by PBOOLE:143;
A36: IC (Comput (P,s,(m + 9))) = |.((Comput (P,s,(m + 8))) . (DataLoc (((Comput (P,s,(m + 8))) . SBP),RetIC))).| + 2 by A30, SCMPDS_2:58
.= 11 + 2 by A34, ABSVALUE:29 ;
then A37: CurInstr (P,(Comput (P,s,(m + 9)))) = P . 13 by A35
.= (SBP,2) := (SBP,6) by Lm1, A1 ;
A38: Comput (P,s,(m + (9 + 1))) = Comput (P,s,((m + 9) + 1))
.= Following (P,(Comput (P,s,(m + 9)))) by EXTPRO_1:3
.= Exec (((SBP,2) := (SBP,6)),(Comput (P,s,(m + 9)))) by A37 ;
A39: (Comput (P,s,(m + 9))) . SBP = (Comput (P,s,(m + 8))) . (DataLoc ((pn + 4),RetSP)) by A18, A28, A30, SCMPDS_2:58
.= (Comput (P,s,(m + 8))) . (intpos ((pn + 4) + 0)) by Th1, SCMPDS_I:def 13
.= pn by A10, A15, A32, SCMPDS_2:54 ;
A40: (Comput (P,s,(m + 9))) . (intpos (pn + 6)) = (Comput (P,s,(m + 8))) . (intpos ((pn + 4) + 2)) by A30, Lm3, SCMPDS_2:58
.= (Comput (P,s,(m + 8))) . (DataLoc (((Comput (P,s,8)) . SBP),2)) by A18, Th1
.= ((Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),2))) gcd ((Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3))) by A26, EXTPRO_1:4 ;
A41: P /. (IC (Comput (P,s,(m + 10)))) = P . (IC (Comput (P,s,(m + 10)))) by PBOOLE:143;
IC (Comput (P,s,(m + 10))) = (IC (Comput (P,s,(m + 9)))) + 1 by A38, SCMPDS_2:47
.= 13 + 1 by A36 ;
then A42: CurInstr (P,(Comput (P,s,(m + 10)))) = P . 14 by A41
.= return SBP by Lm1, A1 ;