let s be State of SCMPDS; :: thesis: for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i, c being Integer
for m, n, m1 being Element of NAT st card I > 0 & s . a = c & 1 = s . (DataLoc (c,i)) & m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & m + n = s . (intpos (m1 + 1)) & ( for t being State of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Element of NAT st t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t & I is_halting_on t & (IExec (I,t)) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,t)) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,t)) . (intpos (m + j)) <= (IExec (I,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,t)) . (intpos (m + j)) >= (IExec (I,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 (a,i,I) is_halting_on s & while>0 (a,i,I) is_closed_on s )
let I be halt-free shiftable Program of SCMPDS; :: thesis: for a being Int_position
for i, c being Integer
for m, n, m1 being Element of NAT st card I > 0 & s . a = c & 1 = s . (DataLoc (c,i)) & m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & m + n = s . (intpos (m1 + 1)) & ( for t being State of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Element of NAT st t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t & I is_halting_on t & (IExec (I,t)) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,t)) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,t)) . (intpos (m + j)) <= (IExec (I,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,t)) . (intpos (m + j)) >= (IExec (I,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 (a,i,I) is_halting_on s & while>0 (a,i,I) is_closed_on s )
let a be Int_position ; :: thesis: for i, c being Integer
for m, n, m1 being Element of NAT st card I > 0 & s . a = c & 1 = s . (DataLoc (c,i)) & m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & m + n = s . (intpos (m1 + 1)) & ( for t being State of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Element of NAT st t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t & I is_halting_on t & (IExec (I,t)) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,t)) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,t)) . (intpos (m + j)) <= (IExec (I,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,t)) . (intpos (m + j)) >= (IExec (I,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 (a,i,I) is_halting_on s & while>0 (a,i,I) is_closed_on s )
let i, c be Integer; :: thesis: for m, n, m1 being Element of NAT st card I > 0 & s . a = c & 1 = s . (DataLoc (c,i)) & m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & m + n = s . (intpos (m1 + 1)) & ( for t being State of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Element of NAT st t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t & I is_halting_on t & (IExec (I,t)) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,t)) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,t)) . (intpos (m + j)) <= (IExec (I,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,t)) . (intpos (m + j)) >= (IExec (I,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 (a,i,I) is_halting_on s & while>0 (a,i,I) is_closed_on s )
let m, n, m1 be Element of NAT ; :: thesis: ( card I > 0 & s . a = c & 1 = s . (DataLoc (c,i)) & m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & m + n = s . (intpos (m1 + 1)) & ( for t being State of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Element of NAT st t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t & I is_halting_on t & (IExec (I,t)) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,t)) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,t)) . (intpos (m + j)) <= (IExec (I,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,t)) . (intpos (m + j)) >= (IExec (I,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) implies ( while>0 (a,i,I) is_halting_on s & while>0 (a,i,I) is_closed_on s ) )
set b = DataLoc (c,i);
assume A1: card I > 0 ; :: thesis: ( not s . a = c or not 1 = s . (DataLoc (c,i)) or not m1 = (m + n) + 1 or not m + 1 = s . (intpos m1) or not m + n = s . (intpos (m1 + 1)) or ex t being State of SCMPDS ex f1, f2 being FinSequence of INT ex k1, k2, y1, yn being Element of NAT st
( t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & not ( I is_closed_on t & I is_halting_on t & (IExec (I,t)) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,t)) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,t)) . (intpos (m + j)) <= (IExec (I,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,t)) . (intpos (m + j)) >= (IExec (I,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) or ( while>0 (a,i,I) is_halting_on s & while>0 (a,i,I) is_closed_on s ) )
assume A2: s . a = c ; :: thesis: ( not 1 = s . (DataLoc (c,i)) or not m1 = (m + n) + 1 or not m + 1 = s . (intpos m1) or not m + n = s . (intpos (m1 + 1)) or ex t being State of SCMPDS ex f1, f2 being FinSequence of INT ex k1, k2, y1, yn being Element of NAT st
( t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & not ( I is_closed_on t & I is_halting_on t & (IExec (I,t)) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,t)) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,t)) . (intpos (m + j)) <= (IExec (I,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,t)) . (intpos (m + j)) >= (IExec (I,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) or ( while>0 (a,i,I) is_halting_on s & while>0 (a,i,I) is_closed_on s ) )
assume A3: 1 = s . (DataLoc (c,i)) ; :: thesis: ( not m1 = (m + n) + 1 or not m + 1 = s . (intpos m1) or not m + n = s . (intpos (m1 + 1)) or ex t being State of SCMPDS ex f1, f2 being FinSequence of INT ex k1, k2, y1, yn being Element of NAT st
( t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & not ( I is_closed_on t & I is_halting_on t & (IExec (I,t)) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,t)) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,t)) . (intpos (m + j)) <= (IExec (I,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,t)) . (intpos (m + j)) >= (IExec (I,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) or ( while>0 (a,i,I) is_halting_on s & while>0 (a,i,I) is_closed_on s ) )
assume that
A4: m1 = (m + n) + 1 and
A5: m + 1 = s . (intpos m1) and
A6: m + n = s . (intpos (m1 + 1)) ; :: thesis: ( ex t being State of SCMPDS ex f1, f2 being FinSequence of INT ex k1, k2, y1, yn being Element of NAT st
( t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & not ( I is_closed_on t & I is_halting_on t & (IExec (I,t)) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,t)) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,t)) . (intpos (m + j)) <= (IExec (I,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,t)) . (intpos (m + j)) >= (IExec (I,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) or ( while>0 (a,i,I) is_halting_on s & while>0 (a,i,I) is_closed_on s ) )
assume A7: for t being State of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Element of NAT st t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t & I is_halting_on t & (IExec (I,t)) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,t)) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,t)) . (intpos (m + j)) <= (IExec (I,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,t)) . (intpos (m + j)) >= (IExec (I,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ; :: thesis: ( while>0 (a,i,I) is_halting_on s & while>0 (a,i,I) is_closed_on s )

A8: now

let v be State of SCMPDS; :: thesis: ( DataPart v = DataPart s implies while>0 (a,i,I) is_halting_on v )
assume A9: DataPart v = DataPart s ; :: thesis: while>0 (a,i,I) is_halting_on v
then A10: 1 = v . (DataLoc (c,i)) by A3, SCMPDS_4:23;
A11: m + n = v . (intpos (m1 + 1)) by A6, A9, SCMPDS_4:23;
A12: m + 1 = v . (intpos m1) by A5, A9, SCMPDS_4:23;
v . a = c by A2, A9, SCMPDS_4:23;
hence while>0 (a,i,I) is_halting_on v by A1, A4, A7, A10, A12, A11, Lm5; :: thesis: verum

end;

hence while>0 (a,i,I) is_halting_on s ; :: thesis: while>0 (a,i,I) is_closed_on s
thus while>0 (a,i,I) is_closed_on s by A8, Th3; :: thesis: verum