set GA = GCD-Algorithm ;
defpred S₁[ Element of NAT ] means for s1, s2 being State of SCMPDS st GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = 5 & s1 . SBP > 0 & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) <= $1 & s1 . (DataLoc (s1 . SBP ),3) >= 0 & s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) holds
ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) );
A1: S₁[ 0 ]

proof

let s1, s2 be State of SCMPDS ; :: thesis: ( GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = 5 & s1 . SBP > 0 & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) <= 0 & s1 . (DataLoc (s1 . SBP ),3) >= 0 & s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) implies ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) ) )
set x = s1 . (DataLoc (s1 . SBP ),2);
set y = s1 . (DataLoc (s1 . SBP ),3);
set y2 = s2 . (DataLoc (s1 . SBP ),3);
assume that
A2: GCD-Algorithm c= s1 and
A3: GCD-Algorithm c= s2 ; :: thesis: ( not IC s1 = 5 or not s1 . SBP > 0 or not s1 . GBP = 0 or not s1 . (DataLoc (s1 . SBP ),3) <= 0 or not s1 . (DataLoc (s1 . SBP ),3) >= 0 or not s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) ) )
assume A4: IC s1 = 5 ; :: thesis: ( not s1 . SBP > 0 or not s1 . GBP = 0 or not s1 . (DataLoc (s1 . SBP ),3) <= 0 or not s1 . (DataLoc (s1 . SBP ),3) >= 0 or not s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) ) )
assume that
s1 . SBP > 0 and
s1 . GBP = 0 ; :: thesis: ( not s1 . (DataLoc (s1 . SBP ),3) <= 0 or not s1 . (DataLoc (s1 . SBP ),3) >= 0 or not s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) ) )
assume A5: s1 . (DataLoc (s1 . SBP ),3) <= 0 ; :: thesis: ( not s1 . (DataLoc (s1 . SBP ),3) >= 0 or not s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) ) )
assume s1 . (DataLoc (s1 . SBP ),3) >= 0 ; :: thesis: ( not s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) or not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) ) )
assume s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) ; :: thesis: ( not IC s2 = IC s1 or not s2 . SBP = s1 . SBP or not s2 . GBP = 0 or not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) ) )
assume that
A6: IC s2 = IC s1 and
A7: s2 . SBP = s1 . SBP and
s2 . GBP = 0 ; :: thesis: ( not s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) or not s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) or ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) ) )
assume that
s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) and
A8: s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) ; :: thesis: ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) )
Y: (ProgramPart s1) /. (IC s1) = s1 . (IC s1) by COMPOS_1:38;
A9: Comput (ProgramPart s1),s1,(1 + 0 ) = Following (ProgramPart s1),(Comput (ProgramPart s1),s1,0 ) by AMI_1:14
.= Following (ProgramPart s1),s1 by AMI_1:13
.= Exec (SBP ,3 <=0_goto 9),s1 by A2, A4, Y, Lm1 ;
Y: (ProgramPart s2) /. (IC s2) = s2 . (IC s2) by COMPOS_1:38;
A10: Comput (ProgramPart s2),s2,(1 + 0 ) = Following (ProgramPart s2),(Comput (ProgramPart s2),s2,0 ) by AMI_1:14
.= Following (ProgramPart s2),s2 by AMI_1:13
.= Exec (SBP ,3 <=0_goto 9),s2 by A3, A4, A6, Y, Lm1 ;
A11: IC (Comput (ProgramPart s1),s1,1) = ICplusConst s1,9 by A5, A9, SCMPDS_2:68
.= 5 + 9 by A4, SCMPDS_6:23 ;
A12: IC (Comput (ProgramPart s2),s2,1) = ICplusConst s2,9 by A5, A7, A8, A10, SCMPDS_2:68
.= 5 + 9 by A4, A6, SCMPDS_6:23 ;
take n = 1; :: thesis: ( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) )
Y: (ProgramPart (Comput (ProgramPart s1),s1,n)) /. (IC (Comput (ProgramPart s1),s1,n)) = (Comput (ProgramPart s1),s1,n) . (IC (Comput (ProgramPart s1),s1,n)) by COMPOS_1:38;
thus CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = s1 . 14 by A11, Y, AMI_1:54
.= return SBP by A2, Lm1 ; :: thesis: ( s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) )
thus (Comput (ProgramPart s1),s1,n) . SBP = s1 . SBP by A9, SCMPDS_2:68; :: thesis: ( CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) )
Y: (ProgramPart (Comput (ProgramPart s2),s2,n)) /. (IC (Comput (ProgramPart s2),s2,n)) = (Comput (ProgramPart s2),s2,n) . (IC (Comput (ProgramPart s2),s2,n)) by COMPOS_1:38;
thus CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = s2 . 14 by A12, Y, AMI_1:54
.= return SBP by A3, Lm1 ; :: thesis: ( s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) )
thus (Comput (ProgramPart s2),s2,n) . SBP = s2 . SBP by A10, SCMPDS_2:68; :: thesis: ( ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) )
thus for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) by A9, A10, SCMPDS_2:68; :: thesis: for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a )

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,b₂) = IC (Comput (ProgramPart s2),s2,b₂) & (Comput (ProgramPart s1),s1,b₂) . b₃ = (Comput (ProgramPart s2),s2,b₂) . b₃ )
let a be Int_position ; :: thesis: ( k <= n & s1 . a = s2 . a implies ( IC (Comput (ProgramPart s1),s1,b₁) = IC (Comput (ProgramPart s2),s2,b₁) & (Comput (ProgramPart s1),s1,b₁) . b₂ = (Comput (ProgramPart s2),s2,b₁) . b₂ ) )
assume that
A13: k <= n and
A14: s1 . a = s2 . a ; :: thesis: ( IC (Comput (ProgramPart s1),s1,b₁) = IC (Comput (ProgramPart s2),s2,b₁) & (Comput (ProgramPart s1),s1,b₁) . b₂ = (Comput (ProgramPart s2),s2,b₁) . b₂ )

per cases ( k = 0 or k = 1 ) by A13, NAT_1:26;

suppose A15: k = 0 ; :: thesis: ( IC (Comput (ProgramPart s1),s1,b₁) = IC (Comput (ProgramPart s2),s2,b₁) & (Comput (ProgramPart s1),s1,b₁) . b₂ = (Comput (ProgramPart s2),s2,b₁) . b₂ )

hence IC (Comput (ProgramPart s1),s1,k) = IC s2 by A6, AMI_1:13
.= IC (Comput (ProgramPart s2),s2,k) by A15, AMI_1:13 ;
:: thesis: (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a
thus (Comput (ProgramPart s1),s1,k) . a = s1 . a by A15, AMI_1:13
.= (Comput (ProgramPart s2),s2,k) . a by A14, A15, AMI_1:13 ; :: thesis: verum

end;

suppose A16: k = 1 ; :: thesis: ( IC (Comput (ProgramPart s1),s1,b₁) = IC (Comput (ProgramPart s2),s2,b₁) & (Comput (ProgramPart s1),s1,b₁) . b₂ = (Comput (ProgramPart s2),s2,b₁) . b₂ )

hence IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) by A11, A12; :: thesis: (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a
thus (Comput (ProgramPart s1),s1,k) . a = s1 . a by A9, A16, SCMPDS_2:68
.= (Comput (ProgramPart s2),s2,k) . a by A10, A14, A16, SCMPDS_2:68 ; :: thesis: verum

end;

end;

end;

end;

A17: now

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

now

let s1, s2 be State of SCMPDS ; :: thesis: ( GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = 5 & s1 . SBP > 0 & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) <= k + 1 & s1 . (DataLoc (s1 . SBP ),3) >= 0 & s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . 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 & CurInstr (ProgramPart (Comput (ProgramPart b₂),b₂,b₃)),(Comput (ProgramPart b₂),b₂,b₃) = return SBP & b₂ . SBP = (Comput (ProgramPart b₂),b₂,b₃) . SBP & ( for j being Element of NAT st 1 < b₄ & b₄ <= (n . SBP ) + 1 holds
( n . (intpos b₄) = (Comput (ProgramPart n),n,b₃) . (intpos b₄) & j . (intpos b₄) = (Comput (ProgramPart j),j,b₃) . (intpos b₄) ) ) & ( for k being Element of NAT
for a being Int_position st b₄ <= a & n . b₅ = k . b₅ holds
( IC (Comput (ProgramPart n),n,b₄) = IC (Comput (ProgramPart k),k,b₄) & (Comput (ProgramPart n),n,b₄) . b₅ = (Comput (ProgramPart k),k,b₄) . b₅ ) ) ) )
set x = s1 . (DataLoc (s1 . SBP ),2);
set y = s1 . (DataLoc (s1 . SBP ),3);
assume that
A19: GCD-Algorithm c= s1 and
A20: GCD-Algorithm c= s2 ; :: thesis: ( IC s1 = 5 & s1 . SBP > 0 & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) <= k + 1 & s1 . (DataLoc (s1 . SBP ),3) >= 0 & s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . 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 & CurInstr (ProgramPart (Comput (ProgramPart b₂),b₂,b₃)),(Comput (ProgramPart b₂),b₂,b₃) = return SBP & b₂ . SBP = (Comput (ProgramPart b₂),b₂,b₃) . SBP & ( for j being Element of NAT st 1 < b₄ & b₄ <= (n . SBP ) + 1 holds
( n . (intpos b₄) = (Comput (ProgramPart n),n,b₃) . (intpos b₄) & j . (intpos b₄) = (Comput (ProgramPart j),j,b₃) . (intpos b₄) ) ) & ( for k being Element of NAT
for a being Int_position st b₄ <= a & n . b₅ = k . b₅ holds
( IC (Comput (ProgramPart n),n,b₄) = IC (Comput (ProgramPart k),k,b₄) & (Comput (ProgramPart n),n,b₄) . b₅ = (Comput (ProgramPart k),k,b₄) . b₅ ) ) ) )
assume A21: IC s1 = 5 ; :: thesis: ( s1 . SBP > 0 & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) <= k + 1 & s1 . (DataLoc (s1 . SBP ),3) >= 0 & s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . 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 & CurInstr (ProgramPart (Comput (ProgramPart b₂),b₂,b₃)),(Comput (ProgramPart b₂),b₂,b₃) = return SBP & b₂ . SBP = (Comput (ProgramPart b₂),b₂,b₃) . SBP & ( for j being Element of NAT st 1 < b₄ & b₄ <= (n . SBP ) + 1 holds
( n . (intpos b₄) = (Comput (ProgramPart n),n,b₃) . (intpos b₄) & j . (intpos b₄) = (Comput (ProgramPart j),j,b₃) . (intpos b₄) ) ) & ( for k being Element of NAT
for a being Int_position st b₄ <= a & n . b₅ = k . b₅ holds
( IC (Comput (ProgramPart n),n,b₄) = IC (Comput (ProgramPart k),k,b₄) & (Comput (ProgramPart n),n,b₄) . b₅ = (Comput (ProgramPart k),k,b₄) . b₅ ) ) ) )
assume that
A22: s1 . SBP > 0 and
A23: s1 . GBP = 0 ; :: thesis: ( s1 . (DataLoc (s1 . SBP ),3) <= k + 1 & s1 . (DataLoc (s1 . SBP ),3) >= 0 & s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . 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 & CurInstr (ProgramPart (Comput (ProgramPart b₂),b₂,b₃)),(Comput (ProgramPart b₂),b₂,b₃) = return SBP & b₂ . SBP = (Comput (ProgramPart b₂),b₂,b₃) . SBP & ( for j being Element of NAT st 1 < b₄ & b₄ <= (n . SBP ) + 1 holds
( n . (intpos b₄) = (Comput (ProgramPart n),n,b₃) . (intpos b₄) & j . (intpos b₄) = (Comput (ProgramPart j),j,b₃) . (intpos b₄) ) ) & ( for k being Element of NAT
for a being Int_position st b₄ <= a & n . b₅ = k . b₅ holds
( IC (Comput (ProgramPart n),n,b₄) = IC (Comput (ProgramPart k),k,b₄) & (Comput (ProgramPart n),n,b₄) . b₅ = (Comput (ProgramPart k),k,b₄) . b₅ ) ) ) )
assume A24: s1 . (DataLoc (s1 . SBP ),3) <= k + 1 ; :: thesis: ( s1 . (DataLoc (s1 . SBP ),3) >= 0 & s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . 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 & CurInstr (ProgramPart (Comput (ProgramPart b₂),b₂,b₃)),(Comput (ProgramPart b₂),b₂,b₃) = return SBP & b₂ . SBP = (Comput (ProgramPart b₂),b₂,b₃) . SBP & ( for j being Element of NAT st 1 < b₄ & b₄ <= (n . SBP ) + 1 holds
( n . (intpos b₄) = (Comput (ProgramPart n),n,b₃) . (intpos b₄) & j . (intpos b₄) = (Comput (ProgramPart j),j,b₃) . (intpos b₄) ) ) & ( for k being Element of NAT
for a being Int_position st b₄ <= a & n . b₅ = k . b₅ holds
( IC (Comput (ProgramPart n),n,b₄) = IC (Comput (ProgramPart k),k,b₄) & (Comput (ProgramPart n),n,b₄) . b₅ = (Comput (ProgramPart k),k,b₄) . b₅ ) ) ) )
assume A25: s1 . (DataLoc (s1 . SBP ),3) >= 0 ; :: thesis: ( s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . 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 & CurInstr (ProgramPart (Comput (ProgramPart b₂),b₂,b₃)),(Comput (ProgramPart b₂),b₂,b₃) = return SBP & b₂ . SBP = (Comput (ProgramPart b₂),b₂,b₃) . SBP & ( for j being Element of NAT st 1 < b₄ & b₄ <= (n . SBP ) + 1 holds
( n . (intpos b₄) = (Comput (ProgramPart n),n,b₃) . (intpos b₄) & j . (intpos b₄) = (Comput (ProgramPart j),j,b₃) . (intpos b₄) ) ) & ( for k being Element of NAT
for a being Int_position st b₄ <= a & n . b₅ = k . b₅ holds
( IC (Comput (ProgramPart n),n,b₄) = IC (Comput (ProgramPart k),k,b₄) & (Comput (ProgramPart n),n,b₄) . b₅ = (Comput (ProgramPart k),k,b₄) . b₅ ) ) ) )
assume A26: s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) ; :: thesis: ( IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . 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 & CurInstr (ProgramPart (Comput (ProgramPart b₂),b₂,b₃)),(Comput (ProgramPart b₂),b₂,b₃) = return SBP & b₂ . SBP = (Comput (ProgramPart b₂),b₂,b₃) . SBP & ( for j being Element of NAT st 1 < b₄ & b₄ <= (n . SBP ) + 1 holds
( n . (intpos b₄) = (Comput (ProgramPart n),n,b₃) . (intpos b₄) & j . (intpos b₄) = (Comput (ProgramPart j),j,b₃) . (intpos b₄) ) ) & ( for k being Element of NAT
for a being Int_position st b₄ <= a & n . b₅ = k . b₅ holds
( IC (Comput (ProgramPart n),n,b₄) = IC (Comput (ProgramPart k),k,b₄) & (Comput (ProgramPart n),n,b₄) . b₅ = (Comput (ProgramPart k),k,b₄) . b₅ ) ) ) )
assume that
A27: IC s2 = IC s1 and
A28: s2 . SBP = s1 . SBP and
A29: s2 . GBP = 0 ; :: thesis: ( s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . 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 & CurInstr (ProgramPart (Comput (ProgramPart b₂),b₂,b₃)),(Comput (ProgramPart b₂),b₂,b₃) = return SBP & b₂ . SBP = (Comput (ProgramPart b₂),b₂,b₃) . SBP & ( for j being Element of NAT st 1 < b₄ & b₄ <= (n . SBP ) + 1 holds
( n . (intpos b₄) = (Comput (ProgramPart n),n,b₃) . (intpos b₄) & j . (intpos b₄) = (Comput (ProgramPart j),j,b₃) . (intpos b₄) ) ) & ( for k being Element of NAT
for a being Int_position st b₄ <= a & n . b₅ = k . b₅ holds
( IC (Comput (ProgramPart n),n,b₄) = IC (Comput (ProgramPart k),k,b₄) & (Comput (ProgramPart n),n,b₄) . b₅ = (Comput (ProgramPart k),k,b₄) . b₅ ) ) ) )
assume that
A30: s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) and
A31: s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . 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 & CurInstr (ProgramPart (Comput (ProgramPart b₂),b₂,b₃)),(Comput (ProgramPart b₂),b₂,b₃) = return SBP & b₂ . SBP = (Comput (ProgramPart b₂),b₂,b₃) . SBP & ( for j being Element of NAT st 1 < b₄ & b₄ <= (n . SBP ) + 1 holds
( n . (intpos b₄) = (Comput (ProgramPart n),n,b₃) . (intpos b₄) & j . (intpos b₄) = (Comput (ProgramPart j),j,b₃) . (intpos b₄) ) ) & ( for k being Element of NAT
for a being Int_position st b₄ <= a & n . b₅ = k . b₅ holds
( IC (Comput (ProgramPart n),n,b₄) = IC (Comput (ProgramPart k),k,b₄) & (Comput (ProgramPart n),n,b₄) . b₅ = (Comput (ProgramPart k),k,b₄) . b₅ ) ) )
reconsider y = s1 . (DataLoc (s1 . SBP ),3) as Element of NAT by A25, INT_1:16;

per cases ( y <= k or y = k + 1 ) by A24, 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 & CurInstr (ProgramPart (Comput (ProgramPart b₂),b₂,b₃)),(Comput (ProgramPart b₂),b₂,b₃) = return SBP & b₂ . SBP = (Comput (ProgramPart b₂),b₂,b₃) . SBP & ( for j being Element of NAT st 1 < b₄ & b₄ <= (n . SBP ) + 1 holds
( n . (intpos b₄) = (Comput (ProgramPart n),n,b₃) . (intpos b₄) & j . (intpos b₄) = (Comput (ProgramPart j),j,b₃) . (intpos b₄) ) ) & ( for k being Element of NAT
for a being Int_position st b₄ <= a & n . b₅ = k . b₅ holds
( IC (Comput (ProgramPart n),n,b₄) = IC (Comput (ProgramPart k),k,b₄) & (Comput (ProgramPart n),n,b₄) . b₅ = (Comput (ProgramPart k),k,b₄) . b₅ ) ) )

hence ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) ) by A18, A19, A20, A21, A22, A23, A25, A26, A27, A28, A29, A30, A31; :: thesis: verum

end;

suppose A32: y = k + 1 ; :: thesis: ex nn being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart nn),nn,b₃)),(Comput (ProgramPart nn),nn,b₃) = return SBP & (Comput (ProgramPart nn),nn,b₃) . SBP = nn . SBP & CurInstr (ProgramPart (Comput (ProgramPart b₂),b₂,b₃)),(Comput (ProgramPart b₂),b₂,b₃) = return SBP & (Comput (ProgramPart b₂),b₂,b₃) . SBP = b₂ . SBP & ( for j being Element of NAT st 1 < b₄ & b₄ <= (nn . SBP ) + 1 holds
( nn . (intpos b₄) = (Comput (ProgramPart nn),nn,b₃) . (intpos b₄) & j . (intpos b₄) = (Comput (ProgramPart j),j,b₃) . (intpos b₄) ) ) & ( for j being Element of NAT
for a being Int_position st b₄ <= a & nn . b₅ = j . b₅ holds
( IC (Comput (ProgramPart nn),nn,b₄) = IC (Comput (ProgramPart j),j,b₄) & (Comput (ProgramPart nn),nn,b₄) . b₅ = (Comput (ProgramPart j),j,b₄) . b₅ ) ) )

then A33: y > 0 by NAT_1:5;
reconsider n = s1 . SBP as Element of NAT by A22, INT_1:16;
A34: n = s1 . SBP ;
set s8 = Comput (ProgramPart s1),s1,8;
set t8 = Comput (ProgramPart s2),s2,8;
A35: IC (Comput (ProgramPart s1),s1,7) = 5 + 7 by A19, A21, A23, A30, A33, A34, Lm6;
A36: Comput (ProgramPart s1),s1,8 = Exec (goto (- 7)),(Comput (ProgramPart s1),s1,7) by A19, A21, A23, A30, A33, A34, Lm6;
A37: (Comput (ProgramPart s1),s1,7) . SBP = n + 4 by A19, A21, A23, A30, A33, Lm6;
A38: (Comput (ProgramPart s1),s1,7) . GBP = 0 by A19, A21, A23, A30, A33, A34, Lm6;
A39: (Comput (ProgramPart s1),s1,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A19, A21, A23, A30, A33, Lm6;
A40: (Comput (ProgramPart s1),s1,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) by A19, A21, A23, A30, A33, Lm6;
A41: IC (Comput (ProgramPart s2),s2,7) = 5 + 7 by A20, A21, A27, A28, A29, A30, A31, A33, A34, Lm6;
A42: Comput (ProgramPart s2),s2,8 = Exec (goto (- 7)),(Comput (ProgramPart s2),s2,7) by A20, A21, A27, A28, A29, A30, A31, A33, A34, Lm6;
A43: (Comput (ProgramPart s2),s2,7) . SBP = n + 4 by A20, A21, A27, A28, A29, A30, A31, A33, Lm6;
A44: (Comput (ProgramPart s2),s2,7) . GBP = 0 by A20, A21, A27, A28, A29, A30, A31, A33, A34, Lm6;
A45: (Comput (ProgramPart s2),s2,7) . (intpos (n + 7)) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A19, A20, A21, A23, A27, A28, A29, A30, A31, A33, Lm6;
A46: (Comput (ProgramPart s2),s2,7) . (intpos (n + 6)) = s1 . (intpos (n + 3)) by A19, A20, A21, A23, A27, A28, A29, A30, A31, A33, Lm6;
A47: (Comput (ProgramPart s1),s1,7) . (intpos (n + 4)) = n by A19, A21, A23, A30, A33, Lm6;
A48: (Comput (ProgramPart s1),s1,7) . (intpos (n + 5)) = 11 by A19, A21, A23, A30, A33, Lm6;
A49: (Comput (ProgramPart s2),s2,7) . (intpos (n + 4)) = n by A20, A21, A27, A28, A29, A30, A31, A33, Lm6;
A50: (Comput (ProgramPart s2),s2,7) . (intpos (n + 5)) = 11 by A20, A21, A27, A28, A29, A30, A31, A33, Lm6;
A51: DataLoc (n + 4),2 = intpos ((n + 4) + 2) by Th5
.= intpos (n + (4 + 2)) ;
A52: DataLoc (n + 4),3 = intpos ((n + 4) + 3) by Th5
.= intpos (n + (4 + 3)) ;
A53: GCD-Algorithm c= Comput (ProgramPart s1),s1,8 by A19, AMI_1:81;
A54: GCD-Algorithm c= Comput (ProgramPart s2),s2,8 by A20, AMI_1:81;
A55: IC (Comput (ProgramPart s1),s1,8) = ICplusConst (Comput (ProgramPart s1),s1,7),(- 7) by A36, SCMPDS_2:66
.= 5 by A35, Th6 ;
A56: (Comput (ProgramPart s1),s1,8) . SBP = n + 4 by A36, A37, SCMPDS_2:66;
A57: 4 <= n + 4 by NAT_1:11;
then A58: (Comput (ProgramPart s1),s1,8) . SBP > 0 by A56, XXREAL_0:2;
A59: (Comput (ProgramPart s1),s1,8) . GBP = 0 by A36, A38, SCMPDS_2:66;
set x1 = (Comput (ProgramPart s1),s1,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),2);
set y1 = (Comput (ProgramPart s1),s1,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),3);
A60: (Comput (ProgramPart s1),s1,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),2) = s1 . (intpos (n + 3)) by A36, A40, A51, A56, SCMPDS_2:66
.= y by Th5 ;
A61: (Comput (ProgramPart s1),s1,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),3) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A36, A39, A52, A56, SCMPDS_2:66
.= (s1 . (intpos (n + 2))) mod y by Th5 ;
then A62: (Comput (ProgramPart s1),s1,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),3) < y by A32, NAT_1:5, NEWTON:79;
then A63: (Comput (ProgramPart s1),s1,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),3) <= k by A32, INT_1:20;
A64: IC (Comput (ProgramPart s2),s2,8) = ICplusConst (Comput (ProgramPart s2),s2,7),(- 7) by A42, SCMPDS_2:66
.= IC (Comput (ProgramPart s1),s1,8) by A41, A55, Th6 ;
A65: (Comput (ProgramPart s2),s2,8) . SBP = (Comput (ProgramPart s1),s1,8) . SBP by A42, A43, A56, SCMPDS_2:66;
A66: (Comput (ProgramPart s2),s2,8) . GBP = 0 by A42, A44, SCMPDS_2:66;
set x3 = (Comput (ProgramPart s2),s2,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),2);
A67: (Comput (ProgramPart s2),s2,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),2) = s1 . (intpos (n + 3)) by A42, A46, A51, A56, SCMPDS_2:66
.= (Comput (ProgramPart s1),s1,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),2) by A60, Th5 ;
(Comput (ProgramPart s2),s2,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),3) = (s1 . (intpos (n + 2))) mod (s1 . (intpos (n + 3))) by A42, A45, A52, A56, SCMPDS_2:66
.= (Comput (ProgramPart s1),s1,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),3) by A61, Th5 ;
then consider m being Element of NAT such that
A68: CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart s1),s1,8)),(Comput (ProgramPart s1),s1,8),m)),(Comput (ProgramPart (Comput (ProgramPart s1),s1,8)),(Comput (ProgramPart s1),s1,8),m) = return SBP and
A69: (Comput (ProgramPart s1),s1,8) . SBP = (Comput (ProgramPart (Comput (ProgramPart s1),s1,8)),(Comput (ProgramPart s1),s1,8),m) . SBP and
A70: CurInstr (ProgramPart (Comput (ProgramPart (Comput (ProgramPart s2),s2,8)),(Comput (ProgramPart s2),s2,8),m)),(Comput (ProgramPart (Comput (ProgramPart s2),s2,8)),(Comput (ProgramPart s2),s2,8),m) = return SBP and
A71: (Comput (ProgramPart s2),s2,8) . SBP = (Comput (ProgramPart (Comput (ProgramPart s2),s2,8)),(Comput (ProgramPart s2),s2,8),m) . SBP and
A72: for j being Element of NAT st 1 < j & j <= ((Comput (ProgramPart s1),s1,8) . SBP ) + 1 holds
( (Comput (ProgramPart s1),s1,8) . (intpos j) = (Comput (ProgramPart (Comput (ProgramPart s1),s1,8)),(Comput (ProgramPart s1),s1,8),m) . (intpos j) & (Comput (ProgramPart s2),s2,8) . (intpos j) = (Comput (ProgramPart (Comput (ProgramPart s2),s2,8)),(Comput (ProgramPart s2),s2,8),m) . (intpos j) ) and
A73: for k being Element of NAT
for a being Int_position st k <= m & (Comput (ProgramPart s1),s1,8) . a = (Comput (ProgramPart s2),s2,8) . a holds
( IC (Comput (ProgramPart (Comput (ProgramPart s1),s1,8)),(Comput (ProgramPart s1),s1,8),k) = IC (Comput (ProgramPart (Comput (ProgramPart s2),s2,8)),(Comput (ProgramPart s2),s2,8),k) & (Comput (ProgramPart (Comput (ProgramPart s1),s1,8)),(Comput (ProgramPart s1),s1,8),k) . a = (Comput (ProgramPart (Comput (ProgramPart s2),s2,8)),(Comput (ProgramPart s2),s2,8),k) . a ) by A18, A33, A53, A54, A55, A58, A59, A60, A61, A62, A63, A64, A65, A66, A67, NEWTON:78;
set s9 = Comput (ProgramPart s1),s1,(m + 8);
set t9 = Comput (ProgramPart s2),s2,(m + 8);
T9: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,8) by AMI_1:123;
T8: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,8) by AMI_1:123;
A74: (Comput (ProgramPart s1),s1,8) . SBP = (Comput (ProgramPart s1),s1,(m + 8)) . SBP by A69, T9, AMI_1:51;
T: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,8) by AMI_1:123;
x: Comput (ProgramPart s1),s1,(m + 8) = Comput (ProgramPart s1),(Comput (ProgramPart s1),s1,8),m by AMI_1:51;
S: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,(m + 8)) by AMI_1:123;
A75: Comput (ProgramPart s1),s1,(m + (8 + 1)) = Comput (ProgramPart s1),s1,((m + 8) + 1)
.= Following (ProgramPart s1),(Comput (ProgramPart s1),s1,(m + 8)) by AMI_1:14
.= Exec (return SBP ),(Comput (ProgramPart s1),s1,(m + 8)) by A68, x, T, S ;
A76: 1 < n + 4 by A57, XXREAL_0:2;
A77: n + 4 < ((Comput (ProgramPart s1),s1,8) . SBP ) + 1 by A56, XREAL_1:31;
then A78: (Comput (ProgramPart s1),s1,8) . (intpos (n + 4)) = (Comput (ProgramPart (Comput (ProgramPart s1),s1,8)),(Comput (ProgramPart s1),s1,8),m) . (intpos (n + 4)) by A72, A76
.= (Comput (ProgramPart s1),s1,(m + 8)) . (intpos (n + 4)) by T9, AMI_1:51 ;
5 <= n + 5 by NAT_1:11;
then A79: 1 < n + 5 by XXREAL_0:2;
A80: intpos (n + (4 + 1)) = intpos ((n + 4) + 1)
.= DataLoc (n + 4),1 by Th5 ;
A81: 11 = (Comput (ProgramPart s1),s1,8) . (intpos (n + 5)) by A36, A48, SCMPDS_2:66
.= (Comput (ProgramPart (Comput (ProgramPart s1),s1,8)),(Comput (ProgramPart s1),s1,8),m) . (intpos (n + 5)) by A56, A72, A79
.= (Comput (ProgramPart s1),s1,(m + 8)) . (DataLoc ((Comput (ProgramPart s1),s1,(m + 8)) . SBP ),RetIC ) by A56, A74, A80, T9, AMI_1:51, SCMPDS_1:def 23 ;
A82: (Comput (ProgramPart s2),s2,(m + 8)) . SBP = n + 4 by A56, A65, A71, T8, AMI_1:51;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,8) by AMI_1:123;
x: Comput (ProgramPart s2),s2,(m + 8) = Comput (ProgramPart s2),(Comput (ProgramPart s2),s2,8),m by AMI_1:51;
S: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(m + 8)) by AMI_1:123;
A83: Comput (ProgramPart s2),s2,(m + (8 + 1)) = Comput (ProgramPart s2),s2,((m + 8) + 1)
.= Following (ProgramPart s2),(Comput (ProgramPart s2),s2,(m + 8)) by AMI_1:14
.= Exec (return SBP ),(Comput (ProgramPart s2),s2,(m + 8)) by A70, x, T, S ;
A84: (Comput (ProgramPart s2),s2,8) . (intpos (n + 4)) = (Comput (ProgramPart (Comput (ProgramPart s2),s2,8)),(Comput (ProgramPart s2),s2,8),m) . (intpos (n + 4)) by A72, A76, A77
.= (Comput (ProgramPart s2),s2,(m + 8)) . (intpos (n + 4)) by T, AMI_1:51 ;
A85: 11 = (Comput (ProgramPart s2),s2,8) . (intpos (n + 5)) by A42, A50, SCMPDS_2:66
.= (Comput (ProgramPart (Comput (ProgramPart s2),s2,8)),(Comput (ProgramPart s2),s2,8),m) . (intpos (n + 5)) by A56, A72, A79
.= (Comput (ProgramPart s2),s2,(m + 8)) . (DataLoc ((Comput (ProgramPart s2),s2,(m + 8)) . SBP ),RetIC ) by A80, A82, T, AMI_1:51, SCMPDS_1:def 23 ;
Y: (ProgramPart (Comput (ProgramPart s1),s1,(m + 9))) /. (IC (Comput (ProgramPart s1),s1,(m + 9))) = (Comput (ProgramPart s1),s1,(m + 9)) . (IC (Comput (ProgramPart s1),s1,(m + 9))) by COMPOS_1:38;
A86: IC (Comput (ProgramPart s1),s1,(m + 9)) = (abs ((Comput (ProgramPart s1),s1,(m + 8)) . (DataLoc ((Comput (ProgramPart s1),s1,(m + 8)) . SBP ),RetIC ))) + 2 by A75, SCMPDS_2:70
.= 11 + 2 by A81, Th3 ;
then A87: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(m + 9))),(Comput (ProgramPart s1),s1,(m + 9)) = s1 . 13 by Y, AMI_1:54
.= SBP ,2 := SBP ,6 by A19, Lm1 ;
T: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,(m + 9)) by AMI_1:123;
A88: Comput (ProgramPart s1),s1,(m + (9 + 1)) = Comput (ProgramPart s1),s1,((m + 9) + 1)
.= Following (ProgramPart s1),(Comput (ProgramPart s1),s1,(m + 9)) by AMI_1:14
.= Exec (SBP ,2 := SBP ,6),(Comput (ProgramPart s1),s1,(m + 9)) by A87, T ;
A89: (Comput (ProgramPart s1),s1,(m + 9)) . SBP = (Comput (ProgramPart s1),s1,(m + 8)) . (DataLoc (n + 4),RetSP ) by A56, A74, A75, SCMPDS_2:70
.= (Comput (ProgramPart s1),s1,(m + 8)) . (intpos ((n + 4) + 0 )) by Th5, SCMPDS_1:def 22
.= n by A36, A47, A78, SCMPDS_2:66 ;
Y: (ProgramPart (Comput (ProgramPart s2),s2,(m + 9))) /. (IC (Comput (ProgramPart s2),s2,(m + 9))) = (Comput (ProgramPart s2),s2,(m + 9)) . (IC (Comput (ProgramPart s2),s2,(m + 9))) by COMPOS_1:38;
A90: IC (Comput (ProgramPart s2),s2,(m + 9)) = (abs ((Comput (ProgramPart s2),s2,(m + 8)) . (DataLoc ((Comput (ProgramPart s2),s2,(m + 8)) . SBP ),RetIC ))) + 2 by A83, SCMPDS_2:70
.= 11 + 2 by A85, Th3 ;
then A91: CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(m + 9))),(Comput (ProgramPart s2),s2,(m + 9)) = s2 . 13 by Y, AMI_1:54
.= SBP ,2 := SBP ,6 by A20, Lm1 ;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(m + 9)) by AMI_1:123;
A92: Comput (ProgramPart s2),s2,(m + (9 + 1)) = Comput (ProgramPart s2),s2,((m + 9) + 1)
.= Following (ProgramPart s2),(Comput (ProgramPart s2),s2,(m + 9)) by AMI_1:14
.= Exec (SBP ,2 := SBP ,6),(Comput (ProgramPart s2),s2,(m + 9)) by A91, T ;
A93: (Comput (ProgramPart s2),s2,(m + 9)) . SBP = (Comput (ProgramPart s2),s2,(m + 8)) . (DataLoc (n + 4),RetSP ) by A82, A83, SCMPDS_2:70
.= (Comput (ProgramPart s2),s2,(m + 8)) . (intpos ((n + 4) + 0 )) by Th5, SCMPDS_1:def 22
.= n by A42, A49, A84, SCMPDS_2:66 ;
A94: IC (Comput (ProgramPart s1),s1,(m + 10)) = succ (IC (Comput (ProgramPart s1),s1,(m + 9))) by A88, SCMPDS_2:59
.= 13 + 1 by A86 ;
A95: IC (Comput (ProgramPart s2),s2,(m + 10)) = succ (IC (Comput (ProgramPart s2),s2,(m + 9))) by A92, SCMPDS_2:59
.= 13 + 1 by A90 ;

hereby :: thesis: verum

take nn = m + 10; :: thesis: ( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,nn)),(Comput (ProgramPart s1),s1,nn) = return SBP & (Comput (ProgramPart s1),s1,nn) . SBP = s1 . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,nn)),(Comput (ProgramPart s2),s2,nn) = return SBP & (Comput (ProgramPart s2),s2,nn) . SBP = s2 . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,nn) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,nn) . (intpos j) ) ) & ( for j being Element of NAT
for a being Int_position st j <= nn & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,j) = IC (Comput (ProgramPart s2),s2,j) & (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a ) ) )
Y: (ProgramPart (Comput (ProgramPart s1),s1,nn)) /. (IC (Comput (ProgramPart s1),s1,nn)) = (Comput (ProgramPart s1),s1,nn) . (IC (Comput (ProgramPart s1),s1,nn)) by COMPOS_1:38;
thus CurInstr (ProgramPart (Comput (ProgramPart s1),s1,nn)),(Comput (ProgramPart s1),s1,nn) = s1 . 14 by A94, Y, AMI_1:54
.= return SBP by A19, Lm1 ; :: thesis: ( (Comput (ProgramPart s1),s1,nn) . SBP = s1 . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,nn)),(Comput (ProgramPart s2),s2,nn) = return SBP & (Comput (ProgramPart s2),s2,nn) . SBP = s2 . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,nn) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,nn) . (intpos j) ) ) & ( for j being Element of NAT
for a being Int_position st j <= nn & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,j) = IC (Comput (ProgramPart s2),s2,j) & (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a ) ) )
Y: (ProgramPart (Comput (ProgramPart s2),s2,nn)) /. (IC (Comput (ProgramPart s2),s2,nn)) = (Comput (ProgramPart s2),s2,nn) . (IC (Comput (ProgramPart s2),s2,nn)) by COMPOS_1:38;
A96: DataLoc ((Comput (ProgramPart s1),s1,(m + 9)) . SBP ),2 = intpos (n + 2) by A89, Th5;
hence (Comput (ProgramPart s1),s1,nn) . SBP = s1 . SBP by A88, A89, Lm3, SCMPDS_2:59; :: thesis: ( CurInstr (ProgramPart (Comput (ProgramPart s2),s2,nn)),(Comput (ProgramPart s2),s2,nn) = return SBP & (Comput (ProgramPart s2),s2,nn) . SBP = s2 . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,nn) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,nn) . (intpos j) ) ) & ( for j being Element of NAT
for a being Int_position st j <= nn & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,j) = IC (Comput (ProgramPart s2),s2,j) & (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a ) ) )
thus CurInstr (ProgramPart (Comput (ProgramPart s2),s2,nn)),(Comput (ProgramPart s2),s2,nn) = s2 . 14 by A95, Y, AMI_1:54
.= return SBP by A20, Lm1 ; :: thesis: ( (Comput (ProgramPart s2),s2,nn) . SBP = s2 . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,nn) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,nn) . (intpos j) ) ) & ( for j being Element of NAT
for a being Int_position st j <= nn & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,j) = IC (Comput (ProgramPart s2),s2,j) & (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a ) ) )
A97: DataLoc ((Comput (ProgramPart s2),s2,(m + 9)) . SBP ),2 = intpos (n + 2) by A93, Th5;
hence (Comput (ProgramPart s2),s2,nn) . SBP = s2 . SBP by A28, A92, A93, Lm3, SCMPDS_2:59; :: thesis: ( ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,nn) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,nn) . (intpos j) ) ) & ( for j being Element of NAT
for a being Int_position st j <= nn & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,j) = IC (Comput (ProgramPart s2),s2,j) & (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a ) ) )

hereby :: thesis: for j being Element of NAT
for a being Int_position st j <= nn & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,j) = IC (Comput (ProgramPart s2),s2,j) & (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a )

let j be Element of NAT ; :: thesis: ( 1 < j & j <= (s1 . SBP ) + 1 implies ( s1 . (intpos j) = (Comput (ProgramPart s1),s1,nn) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,nn) . (intpos j) ) )
assume that
A98: 1 < j and
A99: j <= (s1 . SBP ) + 1 ; :: thesis: ( s1 . (intpos j) = (Comput (ProgramPart s1),s1,nn) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,nn) . (intpos j) )
s1 . SBP <= (Comput (ProgramPart s1),s1,8) . SBP by A56, NAT_1:11;
then (s1 . SBP ) + 1 <= ((Comput (ProgramPart s1),s1,8) . SBP ) + 1 by XREAL_1:8;
then A100: j <= ((Comput (ProgramPart s1),s1,8) . SBP ) + 1 by A99, XXREAL_0:2;
A101: (Comput (ProgramPart s1),s1,(m + 9)) . (intpos j) = (Comput (ProgramPart s1),s1,(m + 8)) . (intpos j) by A75, A98, AMI_3:52, SCMPDS_2:70
.= (Comput (ProgramPart (Comput (ProgramPart s1),s1,8)),(Comput (ProgramPart s1),s1,8),m) . (intpos j) by T9, AMI_1:51
.= (Comput (ProgramPart s1),s1,8) . (intpos j) by A72, A98, A100 ;
A102: n + 1 < n + 2 by XREAL_1:8;
T: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,8) by AMI_1:123;
(Comput (ProgramPart s1),s1,7) . (intpos j) = s1 . (intpos j) by A19, A21, A23, A32, A34, A98, A99, Lm5, NAT_1:5;
hence s1 . (intpos j) = (Comput (ProgramPart s1),s1,8) . (intpos j) by A36, SCMPDS_2:66
.= (Comput (ProgramPart s1),s1,nn) . (intpos j) by A88, A96, A99, A101, A102, AMI_3:52, SCMPDS_2:59 ;
:: thesis: s2 . (intpos j) = (Comput (ProgramPart s2),s2,nn) . (intpos j)
A103: (Comput (ProgramPart s2),s2,(m + 9)) . (intpos j) = (Comput (ProgramPart s2),s2,(m + 8)) . (intpos j) by A83, A98, AMI_3:52, SCMPDS_2:70
.= (Comput (ProgramPart s2),(Comput (ProgramPart s2),s2,8),m) . (intpos j) by AMI_1:51
.= (Comput (ProgramPart s2),s2,8) . (intpos j) by A72, A98, A100, T ;
j <= n + 1 by A99;
then (Comput (ProgramPart s2),s2,7) . (intpos j) = s2 . (intpos j) by A20, A21, A27, A28, A29, A31, A32, A98, Lm5, NAT_1:5;
hence s2 . (intpos j) = (Comput (ProgramPart s2),s2,8) . (intpos j) by A42, SCMPDS_2:66
.= (Comput (ProgramPart s2),s2,nn) . (intpos j) by A92, A97, A99, A102, A103, AMI_3:52, SCMPDS_2:59 ;
:: thesis: verum

end;

hereby :: thesis: verum

let j be Element of NAT ; :: thesis: for a being Int_position st j <= nn & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,b₂) = IC (Comput (ProgramPart s2),s2,b₂) & (Comput (ProgramPart s1),s1,b₂) . b₃ = (Comput (ProgramPart s2),s2,b₂) . b₃ )
let a be Int_position ; :: thesis: ( j <= nn & s1 . a = s2 . a implies ( IC (Comput (ProgramPart s1),s1,b₁) = IC (Comput (ProgramPart s2),s2,b₁) & (Comput (ProgramPart s1),s1,b₁) . b₂ = (Comput (ProgramPart s2),s2,b₁) . b₂ ) )
assume that
A104: j <= nn and
A105: s1 . a = s2 . a ; :: thesis: ( IC (Comput (ProgramPart s1),s1,b₁) = IC (Comput (ProgramPart s2),s2,b₁) & (Comput (ProgramPart s1),s1,b₁) . b₂ = (Comput (ProgramPart s2),s2,b₁) . b₂ )
nn = (m + 9) + 1 ;
then A106: ( j <= m + 9 or j = nn ) by A104, NAT_1:8;
A107: m + (8 + 1) = (m + 8) + 1 ;

A108: now

assume A109: j <= m + 8 ; :: thesis: ( j <= 7 or ( j >= 8 & j <= m + 8 ) )

per cases ( j < 7 + 1 or j >= 8 ) ;

suppose j < 7 + 1 ; :: thesis: ( j <= 7 or ( j >= 8 & j <= m + 8 ) )

hence ( j <= 7 or ( j >= 8 & j <= m + 8 ) ) by NAT_1:13; :: thesis: verum

end;

suppose j >= 8 ; :: thesis: ( j <= 7 or ( j >= 8 & j <= m + 8 ) )

hence ( j <= 7 or ( j >= 8 & j <= m + 8 ) ) by A109; :: thesis: verum

end;

end;

end;

A110: (Comput (ProgramPart s1),s1,8) . a = (Comput (ProgramPart s1),s1,7) . a by A36, SCMPDS_2:66
.= (Comput (ProgramPart s2),s2,7) . a by A19, A20, A21, A23, A27, A28, A29, A30, A31, A33, A34, A105, Lm7
.= (Comput (ProgramPart s2),s2,8) . a by A42, SCMPDS_2:66 ;

A111: now

let b be Int_position ; :: thesis: ( (Comput (ProgramPart s1),s1,8) . b = (Comput (ProgramPart s2),s2,8) . b implies (Comput (ProgramPart s1),s1,(m + 9)) . b₁ = (Comput (ProgramPart s2),s2,(m + 9)) . b₁ )
assume A112: (Comput (ProgramPart s1),s1,8) . b = (Comput (ProgramPart s2),s2,8) . b ; :: thesis: (Comput (ProgramPart s1),s1,(m + 9)) . b₁ = (Comput (ProgramPart s2),s2,(m + 9)) . b₁

per cases ( b = SBP or b <> SBP ) ;

suppose b = SBP ; :: thesis: (Comput (ProgramPart s1),s1,(m + 9)) . b₁ = (Comput (ProgramPart s2),s2,(m + 9)) . b₁

hence (Comput (ProgramPart s1),s1,(m + 9)) . b = (Comput (ProgramPart s2),s2,(m + 9)) . b by A89, A93; :: thesis: verum

end;

suppose A113: b <> SBP ; :: thesis: (Comput (ProgramPart s1),s1,(m + 9)) . b₁ = (Comput (ProgramPart s2),s2,(m + 9)) . b₁

hence (Comput (ProgramPart s1),s1,(m + 9)) . b = (Comput (ProgramPart s1),s1,(m + 8)) . b by A75, SCMPDS_2:70
.= (Comput (ProgramPart (Comput (ProgramPart s1),s1,8)),(Comput (ProgramPart s1),s1,8),m) . b by T9, AMI_1:51
.= (Comput (ProgramPart (Comput (ProgramPart s2),s2,8)),(Comput (ProgramPart s2),s2,8),m) . b by A73, A112
.= (Comput (ProgramPart s2),s2,(m + 8)) . b by T8, AMI_1:51
.= (Comput (ProgramPart s2),s2,(m + 9)) . b by A83, A113, SCMPDS_2:70 ;
:: thesis: verum

end;

end;

end;

A114: (Comput (ProgramPart s1),s1,8) . (DataLoc ((Comput (ProgramPart s1),s1,(m + 9)) . SBP ),6) = (Comput (ProgramPart s1),s1,8) . (DataLoc ((Comput (ProgramPart s1),s1,8) . SBP ),2) by A51, A56, A89, Th5
.= (Comput (ProgramPart s2),s2,8) . (DataLoc ((Comput (ProgramPart s1),s1,(m + 9)) . SBP ),6) by A51, A56, A67, A89, Th5 ;

A115: now

per cases ( a <> DataLoc ((Comput (ProgramPart s2),s2,(m + 9)) . SBP ),2 or a = DataLoc ((Comput (ProgramPart s2),s2,(m + 9)) . SBP ),2 ) ;

suppose A116: a <> DataLoc ((Comput (ProgramPart s2),s2,(m + 9)) . SBP ),2 ; :: thesis: (Comput (ProgramPart s1),s1,nn) . a = (Comput (ProgramPart s2),s2,nn) . a

hence (Comput (ProgramPart s1),s1,nn) . a = (Comput (ProgramPart s1),s1,(m + 9)) . a by A88, A89, A93, SCMPDS_2:59
.= (Comput (ProgramPart s2),s2,(m + 9)) . a by A110, A111
.= (Comput (ProgramPart s2),s2,nn) . a by A92, A116, SCMPDS_2:59 ;
:: thesis: verum

end;

suppose A117: a = DataLoc ((Comput (ProgramPart s2),s2,(m + 9)) . SBP ),2 ; :: thesis: (Comput (ProgramPart s1),s1,nn) . a = (Comput (ProgramPart s2),s2,nn) . a

hence (Comput (ProgramPart s1),s1,nn) . a = (Comput (ProgramPart s1),s1,(m + 9)) . (DataLoc ((Comput (ProgramPart s1),s1,(m + 9)) . SBP ),6) by A88, A89, A93, SCMPDS_2:59
.= (Comput (ProgramPart s2),s2,(m + 9)) . (DataLoc ((Comput (ProgramPart s2),s2,(m + 9)) . SBP ),6) by A89, A93, A111, A114
.= (Comput (ProgramPart s2),s2,nn) . a by A92, A117, SCMPDS_2:59 ;
:: thesis: verum

end;

end;

end;

per cases ( j <= 7 or ( j >= 8 & j <= m + 8 ) or j = m + 9 or j = nn ) by A106, A107, A108, NAT_1:8;

suppose j <= 7 ; :: thesis: ( IC (Comput (ProgramPart s1),s1,b₁) = IC (Comput (ProgramPart s2),s2,b₁) & (Comput (ProgramPart s1),s1,b₁) . b₂ = (Comput (ProgramPart s2),s2,b₁) . b₂ )

hence ( IC (Comput (ProgramPart s1),s1,j) = IC (Comput (ProgramPart s2),s2,j) & (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a ) by A19, A20, A21, A23, A27, A28, A29, A30, A31, A33, A34, A105, Lm7; :: thesis: verum

end;

suppose A118: ( j >= 8 & j <= m + 8 ) ; :: thesis: ( IC (Comput (ProgramPart s1),s1,b₁) = IC (Comput (ProgramPart s2),s2,b₁) & (Comput (ProgramPart s1),s1,b₁) . b₂ = (Comput (ProgramPart s2),s2,b₁) . b₂ )

then consider j1 being Nat such that
A119: j = 8 + j1 by NAT_1:10;
reconsider j1 = j1 as Element of NAT by ORDINAL1:def 13;
T: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,8) by AMI_1:123;
S: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,8) by AMI_1:123;
A120: j1 <= m by A118, A119, XREAL_1:8;
thus IC (Comput (ProgramPart s1),s1,j) = IC (Comput (ProgramPart s1),(Comput (ProgramPart s1),s1,8),j1) by A119, AMI_1:51
.= IC (Comput (ProgramPart s2),(Comput (ProgramPart s2),s2,8),j1) by A73, A110, A120, T, S
.= IC (Comput (ProgramPart s2),s2,j) by A119, AMI_1:51 ; :: thesis: (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a
thus (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s1),(Comput (ProgramPart s1),s1,8),j1) . a by A119, AMI_1:51
.= (Comput (ProgramPart (Comput (ProgramPart s2),s2,8)),(Comput (ProgramPart s2),s2,8),j1) . a by A73, A110, A120, T
.= (Comput (ProgramPart s2),s2,j) . a by A119, S, AMI_1:51 ; :: thesis: verum

end;

suppose A121: j = m + 9 ; :: thesis: ( IC (Comput (ProgramPart s1),s1,b₁) = IC (Comput (ProgramPart s2),s2,b₁) & (Comput (ProgramPart s1),s1,b₁) . b₂ = (Comput (ProgramPart s2),s2,b₁) . b₂ )

hence IC (Comput (ProgramPart s1),s1,j) = IC (Comput (ProgramPart s2),s2,j) by A86, A90; :: thesis: (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a
thus (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a by A110, A111, A121; :: thesis: verum

end;

suppose A122: j = nn ; :: thesis: ( IC (Comput (ProgramPart s1),s1,b₁) = IC (Comput (ProgramPart s2),s2,b₁) & (Comput (ProgramPart s1),s1,b₁) . b₂ = (Comput (ProgramPart s2),s2,b₁) . b₂ )

hence IC (Comput (ProgramPart s1),s1,j) = IC (Comput (ProgramPart s2),s2,j) by A94, A95; :: thesis: (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a
thus (Comput (ProgramPart s1),s1,j) . a = (Comput (ProgramPart s2),s2,j) . a by A115, A122; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

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

end;

A123: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A17);
let s1, s2 be State of SCMPDS ; :: thesis: ( GCD-Algorithm c= s1 & GCD-Algorithm c= s2 & IC s1 = 5 & s1 . SBP > 0 & s1 . GBP = 0 & s1 . (DataLoc (s1 . SBP ),3) >= 0 & s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) & IC s2 = IC s1 & s2 . SBP = s1 . SBP & s2 . GBP = 0 & s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) & s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) implies ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) ) )
assume that
A124: GCD-Algorithm c= s1 and
A125: GCD-Algorithm c= s2 and
A126: IC s1 = 5 and
A127: s1 . SBP > 0 and
A128: s1 . GBP = 0 and
A129: s1 . (DataLoc (s1 . SBP ),3) >= 0 and
A130: s1 . (DataLoc (s1 . SBP ),2) >= s1 . (DataLoc (s1 . SBP ),3) and
A131: IC s2 = IC s1 and
A132: s2 . SBP = s1 . SBP and
A133: s2 . GBP = 0 and
A134: s2 . (DataLoc (s1 . SBP ),2) = s1 . (DataLoc (s1 . SBP ),2) and
A135: s2 . (DataLoc (s1 . SBP ),3) = s1 . (DataLoc (s1 . SBP ),3) ; :: thesis: ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) )
reconsider m = s1 . (DataLoc (s1 . SBP ),3) as Element of NAT by A129, INT_1:16;
S₁[m] by A123;
hence ex n being Element of NAT st
( CurInstr (ProgramPart (Comput (ProgramPart s1),s1,n)),(Comput (ProgramPart s1),s1,n) = return SBP & s1 . SBP = (Comput (ProgramPart s1),s1,n) . SBP & CurInstr (ProgramPart (Comput (ProgramPart s2),s2,n)),(Comput (ProgramPart s2),s2,n) = return SBP & s2 . SBP = (Comput (ProgramPart s2),s2,n) . SBP & ( for j being Element of NAT st 1 < j & j <= (s1 . SBP ) + 1 holds
( s1 . (intpos j) = (Comput (ProgramPart s1),s1,n) . (intpos j) & s2 . (intpos j) = (Comput (ProgramPart s2),s2,n) . (intpos j) ) ) & ( for k being Element of NAT
for a being Int_position st k <= n & s1 . a = s2 . a holds
( IC (Comput (ProgramPart s1),s1,k) = IC (Comput (ProgramPart s2),s2,k) & (Comput (ProgramPart s1),s1,k) . a = (Comput (ProgramPart s2),s2,k) . a ) ) ) by A124, A125, A126, A127, A128, A129, A130, A131, A132, A133, A134, A135; :: thesis: verum