set GA = GCD-Algorithm ;
defpred S₁[ Element of NAT ] means for s being State of SCMPDS st GCD-Algorithm c= s & 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 ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & s . SBP = (Comput ((ProgramPart s),s,n)) . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) );

now

let s be State of SCMPDS; :: thesis: ( GCD-Algorithm c= s & 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 ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) ) )
set x = s . (DataLoc ((s . SBP),2));
set y = s . (DataLoc ((s . SBP),3));
assume A1: GCD-Algorithm c= s ; :: 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 ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),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 Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),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 ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),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 Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),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 Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) ) )
assume A5: s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) ; :: thesis: ex n being Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) )
Y: (ProgramPart s) /. (IC s) = s . (IC s) by COMPOS_1:38;
Z: (ProgramPart (Comput ((ProgramPart s),s,1))) /. (IC (Comput ((ProgramPart s),s,1))) = (Comput ((ProgramPart s),s,1)) . (IC (Comput ((ProgramPart s),s,1))) by COMPOS_1:38;
A6: Comput ((ProgramPart s),s,(1 + 0)) = Following ((ProgramPart s),(Comput ((ProgramPart s),s,0))) by EXTPRO_1:4
.= Following ((ProgramPart s),s) by EXTPRO_1:3
.= Exec (((SBP,3) <=0_goto 9),s) by A1, A2, Y, Lm1 ;
then A7: IC (Comput ((ProgramPart s),s,1)) = ICplusConst (s,9) by A3, SCMPDS_2:68
.= 5 + 9 by A2, SCMPDS_6:23 ;
take n = 1; :: thesis: ( CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) )
thus CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = s . 14 by A7, Z, AMI_1:54
.= return SBP by A1, Lm1 ; :: thesis: ( (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) )
thus (Comput ((ProgramPart s),s,n)) . SBP = s . SBP by A6, SCMPDS_2:68; :: thesis: ( (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) )
A8: s . (DataLoc ((s . SBP),3)) = 0 by A3, A4, XXREAL_0:1;
then A9: abs (s . (DataLoc ((s . SBP),3))) = 0 by ABSVALUE:def 1;
thus (Comput ((ProgramPart s),s,n)) . (DataLoc ((s . SBP),2)) = s . (DataLoc ((s . SBP),2)) by A6, SCMPDS_2:68
.= abs (s . (DataLoc ((s . SBP),2))) by A5, A8, ABSVALUE:def 1
.= (abs (s . (DataLoc ((s . SBP),2)))) gcd (abs (s . (DataLoc ((s . SBP),3)))) by A9, NEWTON:65
.= (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) by INT_2:51 ; :: thesis: for j being Element of NAT st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput ((ProgramPart s),s,n)) . (intpos j)
thus for j being Element of NAT st 1 < j & j <= (s . SBP) + 1 holds
s . (intpos j) = (Comput ((ProgramPart s),s,n)) . (intpos j) by A6, SCMPDS_2:68; :: thesis: verum

end;

then A10: S₁[ 0 ] ;

A11: now

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

now

let s be State of SCMPDS; :: thesis: ( GCD-Algorithm c= s & 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 ((ProgramPart (Comput ((ProgramPart n),n,b₂))),(Comput ((ProgramPart n),n,b₂))) = return SBP & n . SBP = (Comput ((ProgramPart n),n,b₂)) . SBP & (Comput ((ProgramPart n),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 ((ProgramPart n),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 A13: GCD-Algorithm c= s ; :: 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 ((ProgramPart (Comput ((ProgramPart n),n,b₂))),(Comput ((ProgramPart n),n,b₂))) = return SBP & n . SBP = (Comput ((ProgramPart n),n,b₂)) . SBP & (Comput ((ProgramPart n),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 ((ProgramPart n),n,j)) . (intpos b₃) ) ) )
assume A14: 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 ((ProgramPart (Comput ((ProgramPart n),n,b₂))),(Comput ((ProgramPart n),n,b₂))) = return SBP & n . SBP = (Comput ((ProgramPart n),n,b₂)) . SBP & (Comput ((ProgramPart n),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 ((ProgramPart n),n,j)) . (intpos b₃) ) ) )
assume A15: 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 ((ProgramPart (Comput ((ProgramPart n),n,b₂))),(Comput ((ProgramPart n),n,b₂))) = return SBP & n . SBP = (Comput ((ProgramPart n),n,b₂)) . SBP & (Comput ((ProgramPart n),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 ((ProgramPart n),n,j)) . (intpos b₃) ) ) )
assume A16: 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 ((ProgramPart (Comput ((ProgramPart n),n,b₂))),(Comput ((ProgramPart n),n,b₂))) = return SBP & n . SBP = (Comput ((ProgramPart n),n,b₂)) . SBP & (Comput ((ProgramPart n),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 ((ProgramPart n),n,j)) . (intpos b₃) ) ) )
assume A17: 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 ((ProgramPart (Comput ((ProgramPart n),n,b₂))),(Comput ((ProgramPart n),n,b₂))) = return SBP & n . SBP = (Comput ((ProgramPart n),n,b₂)) . SBP & (Comput ((ProgramPart n),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 ((ProgramPart n),n,j)) . (intpos b₃) ) ) )
assume A18: 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 ((ProgramPart (Comput ((ProgramPart n),n,b₂))),(Comput ((ProgramPart n),n,b₂))) = return SBP & n . SBP = (Comput ((ProgramPart n),n,b₂)) . SBP & (Comput ((ProgramPart n),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 ((ProgramPart n),n,j)) . (intpos b₃) ) ) )
assume A19: s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) ; :: thesis: ex n being Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart n),n,b₂))),(Comput ((ProgramPart n),n,b₂))) = return SBP & n . SBP = (Comput ((ProgramPart n),n,b₂)) . SBP & (Comput ((ProgramPart n),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 ((ProgramPart n),n,j)) . (intpos b₃) ) )
then A20: s . (DataLoc ((s . SBP),2)) >= 0 by A18, XXREAL_0:2;
reconsider y = s . (DataLoc ((s . SBP),3)) as Element of NAT by A18, INT_1:16;

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

suppose y <= k ; :: thesis: ex n being Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart n),n,b₂))),(Comput ((ProgramPart n),n,b₂))) = return SBP & n . SBP = (Comput ((ProgramPart n),n,b₂)) . SBP & (Comput ((ProgramPart n),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 ((ProgramPart n),n,j)) . (intpos b₃) ) )

hence ex n being Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & s . SBP = (Comput ((ProgramPart s),s,n)) . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) ) by A12, A13, A14, A15, A16, A18, A19; :: thesis: verum

end;

suppose A21: y = k + 1 ; :: thesis: ex n being Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart n),n,b₂))),(Comput ((ProgramPart n),n,b₂))) = return SBP & (Comput ((ProgramPart n),n,b₂)) . SBP = n . SBP & (Comput ((ProgramPart n),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 ((ProgramPart n),n,j)) . (intpos b₃) ) )

then A22: y > 0 by NAT_1:5;
reconsider pn = s . SBP as Element of NAT by A15, INT_1:16;
A23: pn = s . SBP ;
then A24: IC (Comput ((ProgramPart s),s,7)) = 5 + 7 by A13, A14, A16, A22, Lm4;
A25: Comput ((ProgramPart s),s,8) = Exec ((goto (- 7)),(Comput ((ProgramPart s),s,7))) by A13, A14, A16, A22, A23, Lm4;
A26: (Comput ((ProgramPart s),s,7)) . SBP = pn + 4 by A13, A14, A16, A22, Lm4;
A27: (Comput ((ProgramPart s),s,7)) . GBP = 0 by A13, A14, A16, A22, A23, Lm4;
A28: (Comput ((ProgramPart s),s,7)) . (intpos (pn + 7)) = (s . (DataLoc ((s . SBP),2))) mod y by A13, A14, A16, A22, Lm4;
A29: (Comput ((ProgramPart s),s,7)) . (intpos (pn + 6)) = y by A13, A14, A16, A22, Lm4;
A30: (Comput ((ProgramPart s),s,7)) . (intpos (pn + 4)) = pn by A13, A14, A16, A22, Lm4;
A31: (Comput ((ProgramPart s),s,7)) . (intpos (pn + 5)) = 11 by A13, A14, A16, A22, Lm4;
set s8 = Comput ((ProgramPart s),s,8);
A32: IC (Comput ((ProgramPart s),s,8)) = ICplusConst ((Comput ((ProgramPart s),s,7)),(- 7)) by A25, SCMPDS_2:66
.= 5 by A24, Th6 ;
A33: GCD-Algorithm c= Comput ((ProgramPart s),s,8) by A13, AMI_1:81;
A34: (Comput ((ProgramPart s),s,8)) . SBP = pn + 4 by A25, A26, SCMPDS_2:66;
A35: 4 <= pn + 4 by NAT_1:11;
then A36: (Comput ((ProgramPart s),s,8)) . SBP > 0 by A34, XXREAL_0:2;
A37: (Comput ((ProgramPart s),s,8)) . GBP = 0 by A25, A27, SCMPDS_2:66;
set x1 = (Comput ((ProgramPart s),s,8)) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),2));
set y1 = (Comput ((ProgramPart s),s,8)) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),3));
A38: (Comput ((ProgramPart s),s,8)) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),2)) = (Comput ((ProgramPart s),s,8)) . (intpos ((pn + 4) + 2)) by A34, Th5
.= y by A25, A29, SCMPDS_2:66 ;
A39: (Comput ((ProgramPart s),s,8)) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),3)) = (Comput ((ProgramPart s),s,8)) . (intpos ((pn + 4) + 3)) by A34, Th5
.= (s . (DataLoc ((s . SBP),2))) mod y by A25, A28, SCMPDS_2:66 ;
then A40: (Comput ((ProgramPart s),s,8)) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),3)) < y by A21, NAT_1:5, NEWTON:79;
then (Comput ((ProgramPart s),s,8)) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),3)) <= k by A21, INT_1:20;
then consider m being Element of NAT such that
A41: CurInstr ((ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s),s,8))),(Comput ((ProgramPart s),s,8)),m))),(Comput ((ProgramPart (Comput ((ProgramPart s),s,8))),(Comput ((ProgramPart s),s,8)),m))) = return SBP and
A42: (Comput ((ProgramPart s),s,8)) . SBP = (Comput ((ProgramPart (Comput ((ProgramPart s),s,8))),(Comput ((ProgramPart s),s,8)),m)) . SBP and
A43: (Comput ((ProgramPart (Comput ((ProgramPart s),s,8))),(Comput ((ProgramPart s),s,8)),m)) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),2)) = ((Comput ((ProgramPart s),s,8)) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),2))) gcd ((Comput ((ProgramPart s),s,8)) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),3))) and
A44: for j being Element of NAT st 1 < j & j <= ((Comput ((ProgramPart s),s,8)) . SBP) + 1 holds
(Comput ((ProgramPart s),s,8)) . (intpos j) = (Comput ((ProgramPart (Comput ((ProgramPart s),s,8))),(Comput ((ProgramPart s),s,8)),m)) . (intpos j) by A12, A22, A32, A33, A36, A37, A38, A39, A40, NEWTON:78;
set s9 = Comput ((ProgramPart s),s,(m + 8));
T9: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,8)) by AMI_1:123;
then A45: (Comput ((ProgramPart s),s,8)) . SBP = (Comput ((ProgramPart s),s,(m + 8))) . SBP by A42, EXTPRO_1:5;
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,8)) by AMI_1:123;
x: Comput ((ProgramPart s),s,(m + 8)) = Comput ((ProgramPart s),(Comput ((ProgramPart s),s,8)),m) by EXTPRO_1:5;
S: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,(m + 8))) by AMI_1:123;
A46: Comput ((ProgramPart s),s,(m + (8 + 1))) = Comput ((ProgramPart s),s,((m + 8) + 1))
.= Following ((ProgramPart s),(Comput ((ProgramPart s),s,(m + 8)))) by EXTPRO_1:4
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart s),s,(m + 8)))),(Comput ((ProgramPart s),s,(m + 8))))),(Comput ((ProgramPart s),s,(m + 8)))) by S
.= Exec ((CurInstr ((ProgramPart (Comput ((ProgramPart (Comput ((ProgramPart s),s,8))),(Comput ((ProgramPart s),s,8)),m))),(Comput ((ProgramPart (Comput ((ProgramPart s),s,8))),(Comput ((ProgramPart s),s,8)),m)))),(Comput ((ProgramPart s),s,(m + 8)))) by x, T
.= Exec ((return SBP),(Comput ((ProgramPart s),s,(m + 8)))) by A41 ;
A47: 1 < pn + 4 by A35, XXREAL_0:2;
pn + 4 < ((Comput ((ProgramPart s),s,8)) . SBP) + 1 by A34, XREAL_1:31;
then A48: (Comput ((ProgramPart s),s,8)) . (intpos (pn + 4)) = (Comput ((ProgramPart (Comput ((ProgramPart s),s,8))),(Comput ((ProgramPart s),s,8)),m)) . (intpos (pn + 4)) by A44, A47
.= (Comput ((ProgramPart s),s,(m + 8))) . (intpos (pn + 4)) by T9, EXTPRO_1:5 ;
5 <= pn + 5 by NAT_1:11;
then A49: 1 < pn + 5 by XXREAL_0:2;
A50: 11 = (Comput ((ProgramPart s),s,8)) . (intpos (pn + 5)) by A25, A31, SCMPDS_2:66
.= (Comput ((ProgramPart (Comput ((ProgramPart s),s,8))),(Comput ((ProgramPart s),s,8)),m)) . (intpos (pn + 5)) by A34, A44, A49
.= (Comput ((ProgramPart s),s,(m + 8))) . (intpos ((pn + 4) + 1)) by T9, EXTPRO_1:5
.= (Comput ((ProgramPart s),s,(m + 8))) . (DataLoc (((Comput ((ProgramPart s),s,(m + 8))) . SBP),RetIC)) by A34, A45, Th5, SCMPDS_1:def 23 ;
Y: (ProgramPart (Comput ((ProgramPart s),s,(m + 9)))) /. (IC (Comput ((ProgramPart s),s,(m + 9)))) = (Comput ((ProgramPart s),s,(m + 9))) . (IC (Comput ((ProgramPart s),s,(m + 9)))) by COMPOS_1:38;
A51: IC (Comput ((ProgramPart s),s,(m + 9))) = (abs ((Comput ((ProgramPart s),s,(m + 8))) . (DataLoc (((Comput ((ProgramPart s),s,(m + 8))) . SBP),RetIC)))) + 2 by A46, SCMPDS_2:70
.= 11 + 2 by A50, ABSVALUE:46 ;
then A52: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,(m + 9)))),(Comput ((ProgramPart s),s,(m + 9)))) = s . 13 by Y, AMI_1:54
.= (SBP,2) := (SBP,6) by A13, Lm1 ;
T: ProgramPart s = ProgramPart (Comput ((ProgramPart s),s,(m + 9))) by AMI_1:123;
A53: Comput ((ProgramPart s),s,(m + (9 + 1))) = Comput ((ProgramPart s),s,((m + 9) + 1))
.= Following ((ProgramPart s),(Comput ((ProgramPart s),s,(m + 9)))) by EXTPRO_1:4
.= Exec (((SBP,2) := (SBP,6)),(Comput ((ProgramPart s),s,(m + 9)))) by A52, T ;
A54: (Comput ((ProgramPart s),s,(m + 9))) . SBP = (Comput ((ProgramPart s),s,(m + 8))) . (DataLoc ((pn + 4),RetSP)) by A34, A45, A46, SCMPDS_2:70
.= (Comput ((ProgramPart s),s,(m + 8))) . (intpos ((pn + 4) + 0)) by Th5, SCMPDS_1:def 22
.= pn by A25, A30, A48, SCMPDS_2:66 ;
A55: (Comput ((ProgramPart s),s,(m + 9))) . (intpos (pn + 6)) = (Comput ((ProgramPart s),s,(m + 8))) . (intpos ((pn + 4) + 2)) by A46, Lm3, SCMPDS_2:70
.= (Comput ((ProgramPart s),s,(m + 8))) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),2)) by A34, Th5
.= ((Comput ((ProgramPart s),s,8)) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),2))) gcd ((Comput ((ProgramPart s),s,8)) . (DataLoc (((Comput ((ProgramPart s),s,8)) . SBP),3))) by A43, T9, EXTPRO_1:5 ;
Y: (ProgramPart (Comput ((ProgramPart s),s,(m + 10)))) /. (IC (Comput ((ProgramPart s),s,(m + 10)))) = (Comput ((ProgramPart s),s,(m + 10))) . (IC (Comput ((ProgramPart s),s,(m + 10)))) by COMPOS_1:38;
IC (Comput ((ProgramPart s),s,(m + 10))) = succ (IC (Comput ((ProgramPart s),s,(m + 9)))) by A53, SCMPDS_2:59
.= 13 + 1 by A51 ;
then A56: CurInstr ((ProgramPart (Comput ((ProgramPart s),s,(m + 10)))),(Comput ((ProgramPart s),s,(m + 10)))) = s . 14 by Y, AMI_1:54
.= return SBP by A13, Lm1 ;

hereby :: thesis: verum

take n = m + 10; :: thesis: ( CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) )
thus CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP by A56; :: thesis: ( (Comput ((ProgramPart s),s,n)) . SBP = s . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) )
A57: DataLoc (((Comput ((ProgramPart s),s,(m + 9))) . SBP),2) = intpos (pn + 2) by A54, Th5;
hence (Comput ((ProgramPart s),s,n)) . SBP = s . SBP by A53, A54, Lm3, SCMPDS_2:59; :: thesis: ( (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) )
thus (Comput ((ProgramPart s),s,n)) . (DataLoc ((s . SBP),2)) = (Comput ((ProgramPart s),s,(m + 9))) . (DataLoc (pn,6)) by A53, A54, SCMPDS_2:59
.= (s . (DataLoc ((s . SBP),3))) gcd ((s . (DataLoc ((s . SBP),2))) mod (s . (DataLoc ((s . SBP),3)))) by A38, A39, A55, Th5
.= (s . (DataLoc ((s . SBP),2))) gcd (s . (DataLoc ((s . SBP),3))) by A20, A21, 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 ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) )
assume that
A58: 1 < j and
A59: j <= (s . SBP) + 1 ; :: thesis: s . (intpos j) = (Comput ((ProgramPart s),s,n)) . (intpos j)
s . SBP <= (Comput ((ProgramPart s),s,8)) . SBP by A34, NAT_1:11;
then (s . SBP) + 1 <= ((Comput ((ProgramPart s),s,8)) . SBP) + 1 by XREAL_1:8;
then A60: j <= ((Comput ((ProgramPart s),s,8)) . SBP) + 1 by A59, XXREAL_0:2;
A61: (Comput ((ProgramPart s),s,(m + 9))) . (intpos j) = (Comput ((ProgramPart s),s,(m + 8))) . (intpos j) by A46, A58, AMI_3:52, SCMPDS_2:70
.= (Comput ((ProgramPart (Comput ((ProgramPart s),s,8))),(Comput ((ProgramPart s),s,8)),m)) . (intpos j) by T9, EXTPRO_1:5
.= (Comput ((ProgramPart s),s,8)) . (intpos j) by A44, A58, A60 ;
A62: pn + 1 < pn + 2 by XREAL_1:8;
(Comput ((ProgramPart s),s,7)) . (intpos j) = s . (intpos j) by A13, A14, A16, A21, A23, A58, A59, Lm5, NAT_1:5;
hence s . (intpos j) = (Comput ((ProgramPart s),s,8)) . (intpos j) by A25, SCMPDS_2:66
.= (Comput ((ProgramPart s),s,n)) . (intpos j) by A53, A57, A59, A61, A62, AMI_3:52, SCMPDS_2:59 ;
:: thesis: verum

end;

end;

end;

end;

end;

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

end;

A63: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A10, A11);
let s be State of SCMPDS; :: thesis: ( GCD-Algorithm c= s & 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 ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & s . SBP = (Comput ((ProgramPart s),s,n)) . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) ) )
assume that
A64: GCD-Algorithm c= s and
A65: IC s = 5 and
A66: s . SBP > 0 and
A67: s . GBP = 0 and
A68: s . (DataLoc ((s . SBP),3)) >= 0 and
A69: s . (DataLoc ((s . SBP),2)) >= s . (DataLoc ((s . SBP),3)) ; :: thesis: ex n being Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & s . SBP = (Comput ((ProgramPart s),s,n)) . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) )
reconsider m = s . (DataLoc ((s . SBP),3)) as Element of NAT by A68, INT_1:16;
S₁[m] by A63;
hence ex n being Element of NAT st
( CurInstr ((ProgramPart (Comput ((ProgramPart s),s,n))),(Comput ((ProgramPart s),s,n))) = return SBP & s . SBP = (Comput ((ProgramPart s),s,n)) . SBP & (Comput ((ProgramPart s),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 ((ProgramPart s),s,n)) . (intpos j) ) ) by A64, A65, A66, A67, A68, A69; :: thesis: verum