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
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
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
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
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 )
set b = DataLoc c,i;
assume A1: ( card I > 0 & 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 )
assume A2: 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 )
assume A3: ( m1 = (m + n) + 1 & m + 1 = s . (intpos m1) & 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 )
assume A4: 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
consider f being FinSequence of INT such that
A5: ( len f = n & ( for i being Element of NAT st 1 <= i & i <= len f holds
f . i = s . (intpos (m + i)) ) ) by SCPISORT:2;
A6: f is_FinSequence_on s,m by A5, SCPISORT:def 1;
set ss = IExec (while>0 a,i,I),s;
consider g being FinSequence of INT such that
A7: ( len g = n & ( for i being Element of NAT st 1 <= i & i <= len g holds
g . i = (IExec (while>0 a,i,I),s) . (intpos (m + i)) ) ) by SCPISORT:2;
g is_FinSequence_on IExec (while>0 a,i,I),s,m by A7, SCPISORT:def 1;
hence while>0 a,i,I is_halting_on s by A1, A2, A3, A4, A5, A6, A7, Lm4; :: thesis: verum