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 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) ) )
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 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) ) ) )
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= P 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 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) ) )

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 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) ) )

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

end;

suppose s . (DataLoc ((s . SBP),2)) < s . (DataLoc ((s . SBP),3)) ; :: thesis: 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) ) )

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 ;

hereby :: thesis: verum

reconsider n = m + 10 as Nat ;
take n = n; :: 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 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 A42; :: 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 Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )
A43: DataLoc (((Comput (P,s,(m + 9))) . SBP),2) = intpos (pn + 2) by A39, Th1;
hence (Comput (P,s,n)) . SBP = s . SBP by A38, A39, 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 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 A38, A39, SCMPDS_2:47
.= (s . (DataLoc ((s . SBP),3))) gcd ((s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3)))) by A22, A23, A40, Th1
.= (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) by A6, A7, NAT_D:30 ; :: thesis: for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j)

hereby :: thesis: verum

let j be Nat; :: thesis: ( 1 < j & j <= (s . SBP) + 1 implies s . (intpos j) = (Comput (P,s,n)) . (intpos j) )
assume that
A44: 1 < j and
A45: j <= (s . SBP) + 1 ; :: thesis: s . (intpos j) = (Comput (P,s,n)) . (intpos j)
s . SBP <= (Comput (P,s,8)) . SBP by A18, NAT_1:11;
then (s . SBP) + 1 <= ((Comput (P,s,8)) . SBP) + 1 by XREAL_1:6;
then A46: j <= ((Comput (P,s,8)) . SBP) + 1 by A45, XXREAL_0:2;
A47: (Comput (P,s,(m + 9))) . (intpos j) = (Comput (P,s,(m + 8))) . (intpos j) by A30, A44, 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 A27, A44, A46 ;
A48: pn + 1 < pn + 2 by XREAL_1:6;
(Comput (P,s,7)) . (intpos j) = s . (intpos j) by A2, A4, A7, A8, A44, A45, Lm5, A1;
hence s . (intpos j) = (Comput (P,s,8)) . (intpos j) by A10, SCMPDS_2:54
.= (Comput (P,s,n)) . (intpos j) by A38, A43, A45, A47, A48, AMI_3:10, SCMPDS_2:47 ;
:: thesis: verum

end;

end;

end;

end;