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)) >= s . (DataLoc ((s . SBP),3)) 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) ) )
set GA = GCD-Algorithm ;
defpred S₁[ Element of NAT ] means 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)) <= $1 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) 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) ) );

now

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),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( 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) ) ) )
set x = s . (DataLoc ((s . SBP),2));
set y = s . (DataLoc ((s . SBP),3));
assume A2: GCD-Algorithm c= P ; :: thesis: ( IC s = 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) <= 0 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( 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) ) ) )
assume A3: IC s = 5 ; :: thesis: ( s . SBP > 0 & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) <= 0 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( 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) ) ) )
assume s . SBP > 0 ; :: thesis: ( s . GBP = 0 & s . (DataLoc ((s . SBP),3)) <= 0 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( 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) ) ) )
assume s . GBP = 0 ; :: thesis: ( s . (DataLoc ((s . SBP),3)) <= 0 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( 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) ) ) )
assume A4: s . (DataLoc ((s . SBP),3)) <= 0 ; :: thesis: ( s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( 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) ) ) )
assume A5: s . (DataLoc ((s . SBP),3)) >= 0 ; :: thesis: ( s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( 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) ) ) )
assume A6: 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 & (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) ) )
A7: P /. (IC s) = P . (IC s) by PBOOLE:143;
A8: P /. (IC (Comput (P,s,1))) = P . (IC (Comput (P,s,1))) by PBOOLE:143;
A9: Comput (P,s,(1 + 0)) = Following (P,(Comput (P,s,0))) by EXTPRO_1:3
.= Following (P,s) by EXTPRO_1:2
.= Exec (((SBP,3) <=0_goto 9),s) by A3, A7, Lm1, A2 ;
then A10: IC (Comput (P,s,1)) = ICplusConst (s,9) by A4, SCMPDS_2:56
.= 5 + 9 by A3, SCMPDS_6:12 ;
take n = 1; :: 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))) = P . 14 by A10, A8
.= return SBP by Lm1, A2 ; :: 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) ) )
thus (Comput (P,s,n)) . SBP = s . SBP by A9, SCMPDS_2:56; :: 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) ) )
A11: s . (DataLoc ((s . SBP),3)) = 0 by A4, A5, XXREAL_0:1;
then A12: abs (s . (DataLoc ((s . SBP),3))) = 0 by ABSVALUE:def 1;
thus (Comput (P,s,n)) . (DataLoc ((s . SBP),2)) = s . (DataLoc ((s . SBP),2)) by A9, SCMPDS_2:56
.= abs (s . (DataLoc ((s . SBP),2))) by A6, A11, ABSVALUE:def 1
.= (abs (s . (DataLoc ((s . SBP),2)))) gcd (abs (s . (DataLoc ((s . SBP),3)))) by A12, NEWTON:52
.= (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) by INT_2:34 ; :: thesis: for j being Element of NAT st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j)
thus for j being Element of NAT st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) by A9, SCMPDS_2:56; :: thesis: verum

end;

then A13: S₁[ 0 ] ;

A14: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A15: S₁[k] ; :: thesis: S₁[k + 1]

now

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)) <= k + 1 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( CurInstr (P,(Comput (P,n,b₂))) = return SBP & n . SBP = (Comput (P,n,b₂)) . SBP & (Comput (P,n,b₂)) . (DataLoc ((n . SBP),2)) = (n . (DataLoc ((n . SBP),2))) gcd (n . (DataLoc ((n . SBP),3))) & ( for j being Element of NAT st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
set x = s . (DataLoc ((s . SBP),2));
set y = s . (DataLoc ((s . SBP),3));
set yy = s . (DataLoc ((s . SBP),3));
assume A17: GCD-Algorithm c= P ; :: thesis: ( IC s = 5 & s . SBP > 0 & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) <= k + 1 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( CurInstr (P,(Comput (P,n,b₂))) = return SBP & n . SBP = (Comput (P,n,b₂)) . SBP & (Comput (P,n,b₂)) . (DataLoc ((n . SBP),2)) = (n . (DataLoc ((n . SBP),2))) gcd (n . (DataLoc ((n . SBP),3))) & ( for j being Element of NAT st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A18: IC s = 5 ; :: thesis: ( s . SBP > 0 & s . GBP = 0 & s . (DataLoc ((s . SBP),3)) <= k + 1 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( CurInstr (P,(Comput (P,n,b₂))) = return SBP & n . SBP = (Comput (P,n,b₂)) . SBP & (Comput (P,n,b₂)) . (DataLoc ((n . SBP),2)) = (n . (DataLoc ((n . SBP),2))) gcd (n . (DataLoc ((n . SBP),3))) & ( for j being Element of NAT st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A19: s . SBP > 0 ; :: thesis: ( s . GBP = 0 & s . (DataLoc ((s . SBP),3)) <= k + 1 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( CurInstr (P,(Comput (P,n,b₂))) = return SBP & n . SBP = (Comput (P,n,b₂)) . SBP & (Comput (P,n,b₂)) . (DataLoc ((n . SBP),2)) = (n . (DataLoc ((n . SBP),2))) gcd (n . (DataLoc ((n . SBP),3))) & ( for j being Element of NAT st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A20: s . GBP = 0 ; :: thesis: ( s . (DataLoc ((s . SBP),3)) <= k + 1 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( CurInstr (P,(Comput (P,n,b₂))) = return SBP & n . SBP = (Comput (P,n,b₂)) . SBP & (Comput (P,n,b₂)) . (DataLoc ((n . SBP),2)) = (n . (DataLoc ((n . SBP),2))) gcd (n . (DataLoc ((n . SBP),3))) & ( for j being Element of NAT st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A21: s . (DataLoc ((s . SBP),3)) <= k + 1 ; :: thesis: ( s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( CurInstr (P,(Comput (P,n,b₂))) = return SBP & n . SBP = (Comput (P,n,b₂)) . SBP & (Comput (P,n,b₂)) . (DataLoc ((n . SBP),2)) = (n . (DataLoc ((n . SBP),2))) gcd (n . (DataLoc ((n . SBP),3))) & ( for j being Element of NAT st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A22: s . (DataLoc ((s . SBP),3)) >= 0 ; :: thesis: ( s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being Element of NAT st
( CurInstr (P,(Comput (P,n,b₂))) = return SBP & n . SBP = (Comput (P,n,b₂)) . SBP & (Comput (P,n,b₂)) . (DataLoc ((n . SBP),2)) = (n . (DataLoc ((n . SBP),2))) gcd (n . (DataLoc ((n . SBP),3))) & ( for j being Element of NAT st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A23: s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) ; :: thesis: ex n being Element of NAT st
( CurInstr (P,(Comput (P,n,b₂))) = return SBP & n . SBP = (Comput (P,n,b₂)) . SBP & (Comput (P,n,b₂)) . (DataLoc ((n . SBP),2)) = (n . (DataLoc ((n . SBP),2))) gcd (n . (DataLoc ((n . SBP),3))) & ( for j being Element of NAT st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) )
then A24: s . (DataLoc ((s . SBP),2)) >= 0 by A22, XXREAL_0:2;
reconsider y = s . (DataLoc ((s . SBP),3)) as Element of NAT by A22, INT_1:3;

per cases ( y <= k or y = k + 1 ) by A21, NAT_1:8;

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

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 A15, A18, A19, A20, A22, A23, A17; :: thesis: verum

end;

suppose A25: y = k + 1 ; :: thesis: ex n being Element of NAT st
( CurInstr (P,(Comput (P,n,b₂))) = return SBP & (Comput (P,n,b₂)) . SBP = n . SBP & (Comput (P,n,b₂)) . (DataLoc ((n . SBP),2)) = (n . (DataLoc ((n . SBP),2))) gcd (n . (DataLoc ((n . SBP),3))) & ( for j being Element of NAT st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) )

then A26: y > 0 by NAT_1:5;
reconsider pn = s . SBP as Element of NAT by A19, INT_1:3;
A27: pn = s . SBP ;
then A28: IC (Comput (P,s,7)) = 5 + 7 by A18, A20, A26, Lm4, A17;
A29: Comput (P,s,8) = Exec ((goto (- 7)),(Comput (P,s,7))) by A18, A20, A26, A27, Lm4, A17;
A30: (Comput (P,s,7)) . SBP = pn + 4 by A18, A20, A26, Lm4, A17;
A31: (Comput (P,s,7)) . GBP = 0 by A18, A20, A26, A27, Lm4, A17;
A32: (Comput (P,s,7)) . (intpos (pn + 7)) = (s . (DataLoc ((s . SBP),2))) mod y by A18, A20, A26, Lm4, A17;
A33: (Comput (P,s,7)) . (intpos (pn + 6)) = y by A18, A20, A26, Lm4, A17;
A34: (Comput (P,s,7)) . (intpos (pn + 4)) = pn by A18, A20, A26, Lm4, A17;
A35: (Comput (P,s,7)) . (intpos (pn + 5)) = 11 by A18, A20, A26, Lm4, A17;
set s8 = Comput (P,s,8);
set P8 = P;
A36: IC (Comput (P,s,8)) = ICplusConst ((Comput (P,s,7)),(- 7)) by A29, SCMPDS_2:54
.= 5 by A28, Th6 ;
A37: GCD-Algorithm c= P by A17;
A38: (Comput (P,s,8)) . SBP = pn + 4 by A29, A30, SCMPDS_2:54;
A39: 4 <= pn + 4 by NAT_1:11;
then A40: (Comput (P,s,8)) . SBP > 0 by A38, XXREAL_0:2;
A41: (Comput (P,s,8)) . GBP = 0 by A29, A31, 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));
A42: (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),2)) = (Comput (P,s,8)) . (intpos ((pn + 4) + 2)) by A38, Th5
.= y by A29, A33, SCMPDS_2:54 ;
A43: (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3)) = (Comput (P,s,8)) . (intpos ((pn + 4) + 3)) by A38, Th5
.= (s . (DataLoc ((s . SBP),2))) mod y by A29, A32, SCMPDS_2:54 ;
then A44: (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3)) < y by A25, NAT_1:5, NEWTON:65;
then (Comput (P,s,8)) . (DataLoc (((Comput (P,s,8)) . SBP),3)) <= k by A25, INT_1:7;
then consider m being Element of NAT such that
A45: CurInstr (P,(Comput (P,(Comput (P,s,8)),m))) = return SBP and
A46: (Comput (P,s,8)) . SBP = (Comput (P,(Comput (P,s,8)),m)) . SBP and
A47: (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
A48: 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 A15, A26, A36, A37, A40, A41, A42, A43, A44, NEWTON:64;
set s9 = Comput (P,s,(m + 8));
A50: (Comput (P,s,8)) . SBP = (Comput (P,s,(m + 8))) . SBP by A46, EXTPRO_1:4;
A52: Comput (P,s,(m + 8)) = Comput (P,(Comput (P,s,8)),m) by EXTPRO_1:4;
A54: Comput (P,s,(m + (8 + 1))) = Comput (P,s,((m + 8) + 1))
.= Following (P,(Comput (P,s,(m + 8)))) by EXTPRO_1:3
.= Exec ((CurInstr (P,(Comput (P,s,(m + 8))))),(Comput (P,s,(m + 8))))
.= Exec ((CurInstr (P,(Comput (P,(Comput (P,s,8)),m)))),(Comput (P,s,(m + 8)))) by A52
.= Exec ((return SBP),(Comput (P,s,(m + 8)))) by A45 ;
A55: 1 < pn + 4 by A39, XXREAL_0:2;
pn + 4 < ((Comput (P,s,8)) . SBP) + 1 by A38, XREAL_1:29;
then A56: (Comput (P,s,8)) . (intpos (pn + 4)) = (Comput (P,(Comput (P,s,8)),m)) . (intpos (pn + 4)) by A48, A55
.= (Comput (P,s,(m + 8))) . (intpos (pn + 4)) by EXTPRO_1:4 ;
5 <= pn + 5 by NAT_1:11;
then A57: 1 < pn + 5 by XXREAL_0:2;
A58: 11 = (Comput (P,s,8)) . (intpos (pn + 5)) by A29, A35, SCMPDS_2:54
.= (Comput (P,(Comput (P,s,8)),m)) . (intpos (pn + 5)) by A38, A48, A57
.= (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 A38, A50, Th5, SCMPDS_1:def 21 ;
A59: P /. (IC (Comput (P,s,(m + 9)))) = P . (IC (Comput (P,s,(m + 9)))) by PBOOLE:143;
A60: IC (Comput (P,s,(m + 9))) = (abs ((Comput (P,s,(m + 8))) . (DataLoc (((Comput (P,s,(m + 8))) . SBP),RetIC)))) + 2 by A54, SCMPDS_2:58
.= 11 + 2 by A58, ABSVALUE:29 ;
then A61: CurInstr (P,(Comput (P,s,(m + 9)))) = P . 13 by A59
.= (SBP,2) := (SBP,6) by Lm1, A17 ;
A63: 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 A61 ;
A64: (Comput (P,s,(m + 9))) . SBP = (Comput (P,s,(m + 8))) . (DataLoc ((pn + 4),RetSP)) by A38, A50, A54, SCMPDS_2:58
.= (Comput (P,s,(m + 8))) . (intpos ((pn + 4) + 0)) by Th5, SCMPDS_1:def 20
.= pn by A29, A34, A56, SCMPDS_2:54 ;
A65: (Comput (P,s,(m + 9))) . (intpos (pn + 6)) = (Comput (P,s,(m + 8))) . (intpos ((pn + 4) + 2)) by A54, Lm3, SCMPDS_2:58
.= (Comput (P,s,(m + 8))) . (DataLoc (((Comput (P,s,8)) . SBP),2)) by A38, 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 A47, EXTPRO_1:4 ;
A66: 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 A63, SCMPDS_2:47
.= 13 + 1 by A60 ;
then A67: CurInstr (P,(Comput (P,s,(m + 10)))) = P . 14 by A66
.= return SBP by Lm1, A17 ;

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 A67; :: 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) ) )
A68: DataLoc (((Comput (P,s,(m + 9))) . SBP),2) = intpos (pn + 2) by A64, Th5;
hence (Comput (P,s,n)) . SBP = s . SBP by A63, A64, 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 A63, A64, SCMPDS_2:47
.= (s . (DataLoc ((s . SBP),3))) gcd ((s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3)))) by A42, A43, A65, Th5
.= (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) by A24, A25, NAT_1:5, 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
A69: 1 < j and
A70: j <= (s . SBP) + 1 ; :: thesis: s . (intpos j) = (Comput (P,s,n)) . (intpos j)
s . SBP <= (Comput (P,s,8)) . SBP by A38, NAT_1:11;
then (s . SBP) + 1 <= ((Comput (P,s,8)) . SBP) + 1 by XREAL_1:6;
then A71: j <= ((Comput (P,s,8)) . SBP) + 1 by A70, XXREAL_0:2;
A72: (Comput (P,s,(m + 9))) . (intpos j) = (Comput (P,s,(m + 8))) . (intpos j) by A54, A69, 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 A48, A69, A71 ;
A73: pn + 1 < pn + 2 by XREAL_1:6;
(Comput (P,s,7)) . (intpos j) = s . (intpos j) by A18, A20, A25, A27, A69, A70, Lm5, A17, NAT_1:5;
hence s . (intpos j) = (Comput (P,s,8)) . (intpos j) by A29, SCMPDS_2:54
.= (Comput (P,s,n)) . (intpos j) by A63, A68, A70, A72, A73, AMI_3:10, SCMPDS_2:47 ;
:: thesis: verum

end;

end;

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A74: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A13, A14);
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)) >= s . (DataLoc ((s . SBP),3)) 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) ) ) )
assume that
A76: GCD-Algorithm c= P and
A77: IC s = 5 and
A78: s . SBP > 0 and
A79: s . GBP = 0 and
A80: s . (DataLoc ((s . SBP),3)) >= 0 and
A81: 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) ) )
reconsider m = s . (DataLoc ((s . SBP),3)) as Element of NAT by A80, INT_1:3;
S₁[m] by A74;
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 A77, A78, A79, A80, A81, A76; :: thesis: verum