let s be State of SCMPDS ; :: thesis: for I being shiftable No-StopCode 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 shiftable No-StopCode 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