let P be Instruction-Sequence of SCMPDS; :: thesis: for s being State of SCMPDS st GCD-Algorithm c= P & IC s = 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= 0 holds
ex n being Element of 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 Element of NAT st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )
let s be State of SCMPDS; :: thesis: ( GCD-Algorithm c= P & 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 (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 Element of NAT st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,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
A2: GCD-Algorithm c= P and
A3: IC s = 5 and
A4: s . SBP > 0 and
A5: s . GBP = 0 and
A6: s . (DataLoc ((s . SBP),3)) >= 0 and
A7: s . (DataLoc ((s . SBP),2)) >= 0 ; :: thesis: ex n being Element of 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 Element of NAT st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,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 (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 Element of NAT st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )

hence ex n being Element of 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 Element of NAT st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) ) by A3, A4, A5, A6, Th16, A2; :: thesis: verum

end;

suppose s . (DataLoc ((s . SBP),2)) < s . (DataLoc ((s . SBP),3)) ; :: thesis: ex n being Element of 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 Element of NAT st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )

then A8: s . (DataLoc ((s . SBP),3)) > 0 by A7, XXREAL_0:2;
reconsider y = s . (DataLoc ((s . SBP),3)) as Element of NAT by A6, INT_1:3;
reconsider pn = s . SBP as Element of NAT by A4, INT_1:3;
A9: pn = s . SBP ;
then A10: IC (Comput (P,s,7)) = 5 + 7 by A3, A5, A8, Lm4, A2;
A11: Comput (P,s,8) = Exec ((goto (- 7)),(Comput (P,s,7))) by A3, A5, A8, A9, Lm4, A2;
A12: (Comput (P,s,7)) . SBP = pn + 4 by A3, A5, A8, Lm4, A2;
A13: (Comput (P,s,7)) . GBP = 0 by A3, A5, A8, A9, Lm4, A2;
A14: (Comput (P,s,7)) . (intpos (pn + 7)) = (s . (DataLoc ((s . SBP),2))) mod y by A3, A5, A8, Lm4, A2;
A15: (Comput (P,s,7)) . (intpos (pn + 6)) = y by A3, A5, A8, Lm4, A2;
A16: (Comput (P,s,7)) . (intpos (pn + 4)) = pn by A3, A5, A8, Lm4, A2;
A17: (Comput (P,s,7)) . (intpos (pn + 5)) = 11 by A3, A5, A8, Lm4, A2;
set s8 = Comput (P,s,8);
A18: IC (Comput (P,s,8)) = ICplusConst ((Comput (P,s,7)),(- 7)) by A11, SCMPDS_2:54
.= 5 by A10, Th6 ;
A20: (Comput (P,s,8)) . SBP = pn + 4 by A11, A12, SCMPDS_2:54;
A21: 4 <= pn + 4 by NAT_1:11;
then A22: (Comput (P,s,8)) . SBP > 0 by A20, XXREAL_0:2;
A23: (Comput (P,s,8)) . GBP = 0 by A11, A13, 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));
A24: (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),2)) = (Comput (P,s,8)) . (intpos ((pn + 4) + 2)) by A20, Th5
.= y by A11, A15, SCMPDS_2:54 ;
A25: (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3)) = (Comput (P,s,8)) . (intpos ((pn + 4) + 3)) by A20, Th5
.= (s . (DataLoc ((s . SBP),2))) mod y by A11, A14, SCMPDS_2:54 ;
then (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3)) < y by A8, NEWTON:65;
then consider m being Element of NAT such that
A26: CurInstr (P,(Comput (P,(Comput (P,s,8)),m))) = return SBP and
A27: (Comput (P,s,8)) . SBP = (Comput (P,(Comput (P,s,8)),m)) . SBP and
A28: (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
A29: for j being Element of 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 A6, A18, A22, A23, A24, A25, Th16, A2, NEWTON:64;
set s9 = Comput (P,s,(m + 8));
A31: (Comput (P,s,8)) . SBP = (Comput (P,s,(m + 8))) . SBP by A27, EXTPRO_1:4;
A33: Comput (P,s,(m + 8)) = Comput (P,(Comput (P,s,8)),m) by EXTPRO_1:4;
A35: 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 A26, A33 ;
A36: 1 < pn + 4 by A21, XXREAL_0:2;
pn + 4 < ((Comput (P,s,8)) . SBP) + 1 by A20, XREAL_1:29;
then A37: (Comput (P,s,8)) . (intpos (pn + 4)) = (Comput (P,(Comput (P,s,8)),m)) . (intpos (pn + 4)) by A29, A36
.= (Comput (P,s,(m + 8))) . (intpos (pn + 4)) by EXTPRO_1:4 ;
5 <= pn + 5 by NAT_1:11;
then A38: 1 < pn + 5 by XXREAL_0:2;
A39: 11 = (Comput (P,s,8)) . (intpos (pn + 5)) by A11, A17, SCMPDS_2:54
.= (Comput (P,(Comput (P,s,8)),m)) . (intpos (pn + 5)) by A20, A29, A38
.= (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 A20, A31, Th5, SCMPDS_1:def 21 ;
A40: P /. (IC (Comput (P,s,(m + 9)))) = P . (IC (Comput (P,s,(m + 9)))) by PBOOLE:143;
A41: IC (Comput (P,s,(m + 9))) = (abs ((Comput (P,s,(m + 8))) . (DataLoc (((Comput (P,s,(m + 8))) . SBP),RetIC)))) + 2 by A35, SCMPDS_2:58
.= 11 + 2 by A39, ABSVALUE:29 ;
then A42: CurInstr (P,(Comput (P,s,(m + 9)))) = P . 13 by A40
.= (SBP,2) := (SBP,6) by Lm1, A2 ;
A44: 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 A42 ;
A45: (Comput (P,s,(m + 9))) . SBP = (Comput (P,s,(m + 8))) . (DataLoc ((pn + 4),RetSP)) by A20, A31, A35, SCMPDS_2:58
.= (Comput (P,s,(m + 8))) . (intpos ((pn + 4) + 0)) by Th5, SCMPDS_1:def 20
.= pn by A11, A16, A37, SCMPDS_2:54 ;
A46: (Comput (P,s,(m + 9))) . (intpos (pn + 6)) = (Comput (P,s,(m + 8))) . (intpos ((pn + 4) + 2)) by A35, Lm3, SCMPDS_2:58
.= (Comput (P,s,(m + 8))) . (DataLoc (((Comput (P,s,8)) . SBP),2)) by A20, Th5
.= ((Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),2))) gcd ((Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3))) by A28, EXTPRO_1:4 ;
A47: P /. (IC (Comput (P,s,(m + 10)))) = P . (IC (Comput (P,s,(m + 10)))) by PBOOLE:143;
IC (Comput (P,s,(m + 10))) = succ (IC (Comput (P,s,(m + 9)))) by A44, SCMPDS_2:47
.= 13 + 1 by A41 ;
then A48: CurInstr (P,(Comput (P,s,(m + 10)))) = P . 14 by A47
.= return SBP by Lm1, A2 ;

hereby :: thesis: verum

take n = m + 10; :: thesis: ( CurInstr (P,(Comput (P,s,n))) = return SBP & (Comput (P,s,n)) . SBP = s . SBP & (Comput (P,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 (P,s,n)) . (intpos j) ) )
thus CurInstr (P,(Comput (P,s,n))) = return SBP by A48; :: thesis: ( (Comput (P,s,n)) . SBP = s . SBP & (Comput (P,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 (P,s,n)) . (intpos j) ) )
A49: DataLoc (((Comput (P,s,(m + 9))) . SBP),2) = intpos (pn + 2) by A45, Th5;
hence (Comput (P,s,n)) . SBP = s . SBP by A44, A45, Lm3, SCMPDS_2:47; :: thesis: ( (Comput (P,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 (P,s,n)) . (intpos j) ) )
thus (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = (Comput (P,s,(m + 9))) . (DataLoc (pn,6)) by A44, A45, SCMPDS_2:47
.= (s . (DataLoc ((s . SBP),3))) gcd ((s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3)))) by A24, A25, A46, Th5
.= (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) by A7, A8, NAT_D:30 ; :: thesis: for j being Element of NAT st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,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 (P,s,n)) . (intpos j) )
assume that
A50: 1 < j and
A51: j <= (s . SBP) + 1 ; :: thesis: s . (intpos j) = (Comput (P,s,n)) . (intpos j)
s . SBP <= (Comput (P,s,8)) . SBP by A20, NAT_1:11;
then (s . SBP) + 1 <= ((Comput (P,s,8)) . SBP) + 1 by XREAL_1:6;
then A52: j <= ((Comput (P,s,8)) . SBP) + 1 by A51, XXREAL_0:2;
A53: (Comput (P,s,(m + 9))) . (intpos j) = (Comput (P,s,(m + 8))) . (intpos j) by A35, A50, AMI_3:10, SCMPDS_2:58
.= (Comput (P,(Comput (P,s,8)),m)) . (intpos j) by EXTPRO_1:4
.= (Comput (P,s,8)) . (intpos j) by A29, A50, A52 ;
A54: pn + 1 < pn + 2 by XREAL_1:6;
(Comput (P,s,7)) . (intpos j) = s . (intpos j) by A3, A5, A8, A9, A50, A51, Lm5, A2;
hence s . (intpos j) = (Comput (P,s,8)) . (intpos j) by A11, SCMPDS_2:54
.= (Comput (P,s,n)) . (intpos j) by A44, A49, A51, A53, A54, AMI_3:10, SCMPDS_2:47 ;
:: thesis: verum

end;

end;

end;

end;