let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i, c being Integer
for m, n, m1 being Nat st 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 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being 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,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 (a,i,I) is_halting_on s,P & while>0 (a,i,I) is_closed_on s,P )
let s be 0 -started State of SCMPDS; for I being halt-free shiftable Program of
for a being Int_position
for i, c being Integer
for m, n, m1 being Nat st 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 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being 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,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 (a,i,I) is_halting_on s,P & while>0 (a,i,I) is_closed_on s,P )
let I be halt-free shiftable Program of ; for a being Int_position
for i, c being Integer
for m, n, m1 being Nat st 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 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being 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,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 (a,i,I) is_halting_on s,P & while>0 (a,i,I) is_closed_on s,P )
let a be Int_position; for i, c being Integer
for m, n, m1 being Nat st 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 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being 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,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 (a,i,I) is_halting_on s,P & while>0 (a,i,I) is_closed_on s,P )
let i, c be Integer; for m, n, m1 being Nat st 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 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being 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,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) holds
( while>0 (a,i,I) is_halting_on s,P & while>0 (a,i,I) is_closed_on s,P )
let m, n, m1 be Nat; ( 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 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being 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,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) implies ( while>0 (a,i,I) is_halting_on s,P & while>0 (a,i,I) is_closed_on s,P ) )
set b = DataLoc (c,i);
assume A1:
s . a = c
; ( 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 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS ex f1, f2 being FinSequence of INT ex k1, k2, y1, yn being 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,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) or ( while>0 (a,i,I) is_halting_on s,P & while>0 (a,i,I) is_closed_on s,P ) )
assume A2:
1 = s . (DataLoc (c,i))
; ( not m1 = (m + n) + 1 or not m + 1 = s . (intpos m1) or not m + n = s . (intpos (m1 + 1)) or ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS ex f1, f2 being FinSequence of INT ex k1, k2, y1, yn being 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,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) or ( while>0 (a,i,I) is_halting_on s,P & while>0 (a,i,I) is_closed_on s,P ) )
assume that
A3:
m1 = (m + n) + 1
and
A4:
m + 1 = s . (intpos m1)
and
A5:
m + n = s . (intpos (m1 + 1))
; ( ex t being 0 -started State of SCMPDS ex Q being Instruction-Sequence of SCMPDS ex f1, f2 being FinSequence of INT ex k1, k2, y1, yn being 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,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ) or ( while>0 (a,i,I) is_halting_on s,P & while>0 (a,i,I) is_closed_on s,P ) )
assume A6:
for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being 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,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,Q,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Nat st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Nat st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Nat st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,Q,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) & ( for j being Nat st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Nat st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,Q,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) )
; ( while>0 (a,i,I) is_halting_on s,P & while>0 (a,i,I) is_closed_on s,P )
A7:
now for v being 0 -started State of SCMPDS
for V being Instruction-Sequence of SCMPDS st DataPart v = DataPart s holds
while>0 (a,i,I) is_halting_on v,Vlet v be
0 -started State of
SCMPDS;
for V being Instruction-Sequence of SCMPDS st DataPart v = DataPart s holds
while>0 (a,i,I) is_halting_on v,Vlet V be
Instruction-Sequence of
SCMPDS;
( DataPart v = DataPart s implies while>0 (a,i,I) is_halting_on v,V )assume A8:
DataPart v = DataPart s
;
while>0 (a,i,I) is_halting_on v,Vthen A9:
1
= v . (DataLoc (c,i))
by A2, SCMPDS_4:8;
A10:
m + n = v . (intpos (m1 + 1))
by A5, A8, SCMPDS_4:8;
A11:
m + 1
= v . (intpos m1)
by A4, A8, SCMPDS_4:8;
v . a = c
by A1, A8, SCMPDS_4:8;
hence
while>0 (
a,
i,
I)
is_halting_on v,
V
by A3, A6, A9, A11, A10, Lm4;
verum end;
hence
while>0 (a,i,I) is_halting_on s,P
; while>0 (a,i,I) is_closed_on s,P
thus
while>0 (a,i,I) is_closed_on s,P
by A7, Th3; verum