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 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 ;
defpred S₁[ 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 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) ) );

now :: 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),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) holds
ex n being 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 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),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being 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 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 A1: 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 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 Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) ) )
assume A2: 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 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 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 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 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 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 Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) ) )
assume A3: 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 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 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),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being 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 Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) ) )
assume A5: s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) ; :: thesis: ex n being 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 Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )
A6: P /. (IC s) = P . (IC s) by PBOOLE:143;
A7: P /. (IC (Comput (P,s,1))) = P . (IC (Comput (P,s,1))) by PBOOLE:143;
A8: 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 A2, A6, Lm1, A1 ;
then A9: IC (Comput (P,s,1)) = ICplusConst (s,9) by A3, SCMPDS_2:56
.= 5 + 9 by A2, SCMPDS_6:12 ;
reconsider n = 1 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))) = P . 14 by A9, A7
.= return SBP by Lm1, A1 ; :: 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) ) )
thus (Comput (P,s,n)) . SBP = s . SBP by A8, 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 Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) ) )
A10: s . (DataLoc ((s . SBP),3)) = 0 by A3, A4;
then A11: |.(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 A8, SCMPDS_2:56
.= |.(s . (DataLoc ((s . SBP),2))).| by A5, A10, ABSVALUE:def 1
.= |.(s . (DataLoc ((s . SBP),2))).| gcd |.(s . (DataLoc ((s . SBP),3))).| by A11, NEWTON:52
.= (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) by INT_2:34 ; :: thesis: for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j)
thus for j being Nat st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput (P,s,n)) . (intpos j) by A8, SCMPDS_2:56; :: thesis: verum

end;

then A12: S₁[ 0 ] ;

A13: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A14: S₁[k] ; :: thesis: S₁[k + 1]

now :: 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)) <= k + 1 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) 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)) <= k + 1 & s . (DataLoc ((s . SBP),3)) >= 0 & s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being 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 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 A15: 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 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 Nat st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A16: 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 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 Nat st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A17: 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 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 Nat st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A18: 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 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 Nat st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A19: 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 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 Nat st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A20: s . (DataLoc ((s . SBP),3)) >= 0 ; :: thesis: ( s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) implies ex n being 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 Nat st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) ) )
assume A21: s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) ; :: thesis: ex n being 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 Nat st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) )
then A22: s . (DataLoc ((s . SBP),2)) >= 0 by A20;
reconsider y = s . (DataLoc ((s . SBP),3)) as Element of NAT by A20, INT_1:3;

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

suppose y <= k ; :: thesis: ex n being 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 Nat st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) )

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 A14, A16, A17, A18, A21, A15; :: thesis: verum

end;

suppose A23: y = k + 1 ; :: thesis: ex n being 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 Nat st 1 < b₃ & b₃ <= (n . SBP) + 1 holds
n . (intpos b₃) = (Comput (P,n,j)) . (intpos b₃) ) )

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

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 A61; :: 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) ) )
A62: DataLoc (((Comput (P,s,(m + 9))) . SBP),2) = intpos (pn + 2) by A58, Th1;
hence (Comput (P,s,n)) . SBP = s . SBP by A57, A58, 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 A57, A58, SCMPDS_2:47
.= (s . (DataLoc ((s . SBP),3))) gcd ((s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3)))) by A40, A41, A59, Th1
.= (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) by A22, A23, 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
A63: 1 < j and
A64: j <= (s . SBP) + 1 ; :: thesis: s . (intpos j) = (Comput (P,s,n)) . (intpos j)
s . SBP <= (Comput (P,s,8)) . SBP by A36, NAT_1:11;
then (s . SBP) + 1 <= ((Comput (P,s,8)) . SBP) + 1 by XREAL_1:6;
then A65: j <= ((Comput (P,s,8)) . SBP) + 1 by A64, XXREAL_0:2;
A66: (Comput (P,s,(m + 9))) . (intpos j) = (Comput (P,s,(m + 8))) . (intpos j) by A49, A63, 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 A46, A63, A65 ;
A67: pn + 1 < pn + 2 by XREAL_1:6;
(Comput (P,s,7)) . (intpos j) = s . (intpos j) by A16, A18, A23, A25, A63, A64, Lm5, A15;
hence s . (intpos j) = (Comput (P,s,8)) . (intpos j) by A27, SCMPDS_2:54
.= (Comput (P,s,n)) . (intpos j) by A57, A62, A64, A66, A67, AMI_3:10, SCMPDS_2:47 ;
:: thesis: verum

end;

end;

end;

end;

end;

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

end;

A68: for n being Nat holds S₁[n] from NAT_1:sch 2(A12, A13);
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 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) ) ) )
assume that
A69: GCD-Algorithm c= P and
A70: IC s = 5 and
A71: s . SBP > 0 and
A72: s . GBP = 0 and
A73: s . (DataLoc ((s . SBP),3)) >= 0 and
A74: 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) ) )
reconsider m = s . (DataLoc ((s . SBP),3)) as Element of NAT by A73, INT_1:3;
S₁[m] by A68;
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 A70, A71, A72, A74, A69; :: thesis: verum