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 f, g being FinSequence of INT
for m, n, m1 being Nat st s . a = c & len f = n & len g = n & f is_FinSequence_on s,m & g is_FinSequence_on IExec ((while>0 (a,i,I)),P,s),m & 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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
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 f, g being FinSequence of INT
for m, n, m1 being Nat st s . a = c & len f = n & len g = n & f is_FinSequence_on s,m & g is_FinSequence_on IExec ((while>0 (a,i,I)),P,s),m & 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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
let I be halt-free shiftable Program of ; for a being Int_position
for i, c being Integer
for f, g being FinSequence of INT
for m, n, m1 being Nat st s . a = c & len f = n & len g = n & f is_FinSequence_on s,m & g is_FinSequence_on IExec ((while>0 (a,i,I)),P,s),m & 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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
let a be Int_position; for i, c being Integer
for f, g being FinSequence of INT
for m, n, m1 being Nat st s . a = c & len f = n & len g = n & f is_FinSequence_on s,m & g is_FinSequence_on IExec ((while>0 (a,i,I)),P,s),m & 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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
let i, c be Integer; for f, g being FinSequence of INT
for m, n, m1 being Nat st s . a = c & len f = n & len g = n & f is_FinSequence_on s,m & g is_FinSequence_on IExec ((while>0 (a,i,I)),P,s),m & 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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
let f, g be FinSequence of INT ; for m, n, m1 being Nat st s . a = c & len f = n & len g = n & f is_FinSequence_on s,m & g is_FinSequence_on IExec ((while>0 (a,i,I)),P,s),m & 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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
let m, n, m1 be Nat; ( s . a = c & len f = n & len g = n & f is_FinSequence_on s,m & g is_FinSequence_on IExec ((while>0 (a,i,I)),P,s),m & 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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) )
A1:
Initialize s = s
by MEMSTR_0:44;
set b = DataLoc (c,i);
assume that
A2:
s . a = c
and
A3:
len f = n
and
A4:
len g = n
; ( not f is_FinSequence_on s,m or not g is_FinSequence_on IExec ((while>0 (a,i,I)),P,s),m 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 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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) )
set WH = while>0 (a,i,I);
set sWH = stop (while>0 (a,i,I));
assume A5:
f is_FinSequence_on s,m
; ( not g is_FinSequence_on IExec ((while>0 (a,i,I)),P,s),m 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 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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) )
defpred S1[ Nat] means for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1 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 & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & yn - y1 <= $1 & f1 is_FinSequence_on t,m & len f1 = n holds
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c );
assume A6:
g is_FinSequence_on IExec ((while>0 (a,i,I)),P,s),m
; ( 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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) )
assume A7:
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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) )
assume that
A8:
m1 = (m + n) + 1
and
A9:
m + 1 = s . (intpos m1)
and
A10:
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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) )
A11:
m1 = ((m + n) + (2 * 0)) + 1
by A8;
assume A12:
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 & f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
A13:
S1[ 0 ]
proof
let t be
0 -started State of
SCMPDS;
for Q being Instruction-Sequence of SCMPDS
for f1 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 & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & yn - y1 <= 0 & f1 is_FinSequence_on t,m & len f1 = n holds
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )let Q be
Instruction-Sequence of
SCMPDS;
for f1 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 & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & yn - y1 <= 0 & f1 is_FinSequence_on t,m & len f1 = n holds
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )let f1 be
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 & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & yn - y1 <= 0 & f1 is_FinSequence_on t,m & len f1 = n holds
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )let k1,
k2,
y1,
yn be
Nat;
( t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & yn - y1 <= 0 & f1 is_FinSequence_on t,m & len f1 = n implies ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c ) )
A14:
Initialize t = t
by MEMSTR_0:44;
assume that A15:
t . a = c
and A16:
(2 * k1) + 1
= t . (DataLoc (c,i))
and A17:
k2 = ((m + n) + (2 * k1)) + 1
and A18:
( ( 1
<= y1 &
yn <= n ) or
y1 >= yn )
and A19:
m + y1 = t . (intpos k2)
and A20:
m + yn = t . (intpos (k2 + 1))
and A21:
yn - y1 <= 0
and A22:
f1 is_FinSequence_on t,
m
and A23:
len f1 = n
;
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
A24:
I is_halting_on t,
Q
by A12, A15, A16, A17, A18, A19, A20;
take k =
(LifeSpan ((Q +* (stop I)),t)) + 2;
ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
set tk =
Comput (
(Q +* (stop (while>0 (a,i,I)))),
t,
k);
A25:
I is_closed_on t,
Q
by A12, A15, A16, A17, A18, A19, A20;
then A26:
DataPart (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = DataPart (IExec (I,Q,t))
by A15, A16, A24, Th2, A14;
consider f2 being
FinSequence of
INT such that A27:
len f2 = n
and A28:
for
i being
Nat st 1
<= i &
i <= len f2 holds
f2 . i = (IExec (I,Q,t)) . (intpos (m + i))
by SCPISORT:1;
take
f2
;
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
thus
Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput (
(Q +* (stop (while>0 (a,i,I)))),
t,
k)
by A15, A16, A25, A24, Th2, A14;
( f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
now for i being Nat st 1 <= i & i <= len f2 holds
f2 . i = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos (m + i))let i be
Nat;
( 1 <= i & i <= len f2 implies f2 . i = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos (m + i)) )assume that A29:
1
<= i
and A30:
i <= len f2
;
f2 . i = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos (m + i))thus f2 . i =
(IExec (I,Q,t)) . (intpos (m + i))
by A28, A29, A30
.=
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos (m + i))
by A26, SCMPDS_4:8
;
verum end;
hence
f2 is_FinSequence_on Comput (
(Q +* (stop (while>0 (a,i,I)))),
t,
k),
m
;
( len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
thus
len f2 = n
by A27;
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
f2 is_FinSequence_on IExec (
I,
Q,
t),
m
by A28;
hence
f1,
f2 are_fiberwise_equipotent
by A12, A15, A16, A17, A18, A19, A20, A22, A23, A27;
( f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
thus
f2 is_non_decreasing_on y1,
yn
by A21, FINSEQ_6:165, XREAL_1:50;
( ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
thus
for
j being
Nat st
y1 < yn & ( ( 1
<= j &
j < y1 ) or (
yn < j &
j <= n ) ) holds
f2 . j = t . (intpos (m + j))
by A21, XREAL_1:50;
( ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
hereby ( ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
let j be
Nat;
( y1 >= yn & 1 <= j & j <= n implies f2 . j = t . (intpos (m + j)) )assume that A31:
y1 >= yn
and A32:
1
<= j
and A33:
j <= n
;
f2 . j = t . (intpos (m + j))thus f2 . j =
(IExec (I,Q,t)) . (intpos (m + j))
by A27, A28, A32, A33
.=
t . (intpos (m + j))
by A12, A15, A16, A17, A19, A20, A31, A32, A33
;
verum
end;
hereby ( (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
let j be
Nat;
( 1 <= j & j < (2 * k1) + 1 implies (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) )assume that A34:
1
<= j
and A35:
j < (2 * k1) + 1
;
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j))thus (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) =
(IExec (I,Q,t)) . (intpos ((m + n) + j))
by A26, SCMPDS_4:8
.=
t . (intpos ((m + n) + j))
by A12, A15, A16, A17, A18, A19, A20, A34, A35
;
verum
end;
(
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)) ) ) )
by A12, A15, A16, A17, A19, A20;
hence
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2
by A16, A21, A26, SCMPDS_4:8, XREAL_1:50;
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c
(IExec (I,Q,t)) . a = t . a
by A12, A15, A16, A17, A18, A19, A20;
hence
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c
by A15, A26, SCMPDS_4:8;
verum
end;
A36:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A37:
S1[
k]
;
S1[k + 1]
S1[
k + 1]
proof
let t be
0 -started State of
SCMPDS;
for Q being Instruction-Sequence of SCMPDS
for f1 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 & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & yn - y1 <= k + 1 & f1 is_FinSequence_on t,m & len f1 = n holds
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )let Q be
Instruction-Sequence of
SCMPDS;
for f1 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 & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & yn - y1 <= k + 1 & f1 is_FinSequence_on t,m & len f1 = n holds
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )let f1 be
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 & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & yn - y1 <= k + 1 & f1 is_FinSequence_on t,m & len f1 = n holds
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )let k1,
k2,
y1,
yn be
Nat;
( t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & yn - y1 <= k + 1 & f1 is_FinSequence_on t,m & len f1 = n implies ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c ) )
A38:
Initialize t = t
by MEMSTR_0:44;
assume that A39:
t . a = c
and A40:
(2 * k1) + 1
= t . (DataLoc (c,i))
and A41:
k2 = ((m + n) + (2 * k1)) + 1
and A42:
( ( 1
<= y1 &
yn <= n ) or
y1 >= yn )
and A43:
m + y1 = t . (intpos k2)
and A44:
m + yn = t . (intpos (k2 + 1))
and A45:
yn - y1 <= k + 1
and A46:
f1 is_FinSequence_on t,
m
and A47:
len f1 = n
;
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )
per cases
( yn - y1 <= 0 or yn - y1 > 0 )
;
suppose
yn - y1 <= 0
;
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )hence
ex
kk being
Nat ex
f2 being
FinSequence of
INT st
(
Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,kk)) = Comput (
(Q +* (stop (while>0 (a,i,I)))),
t,
kk) &
f2 is_FinSequence_on Comput (
(Q +* (stop (while>0 (a,i,I)))),
t,
kk),
m &
len f2 = n &
f1,
f2 are_fiberwise_equipotent &
f2 is_non_decreasing_on y1,
yn & ( for
j being
Nat st
y1 < yn & ( ( 1
<= j &
j < y1 ) or (
yn < j &
j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for
j being
Nat st
y1 >= yn & 1
<= j &
j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for
j being
Nat st 1
<= j &
j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,kk)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) &
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,kk)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 &
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,kk)) . a = c )
by A13, A39, A40, A41, A42, A43, A44, A46, A47;
verum end; suppose A48:
yn - y1 > 0
;
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c )set m1 =
(LifeSpan ((Q +* (stop I)),t)) + 2;
set t1 =
Comput (
(Q +* (stop (while>0 (a,i,I)))),
t,
((LifeSpan ((Q +* (stop I)),t)) + 2));
set Q1 =
Q +* (stop (while>0 (a,i,I)));
A49:
I is_halting_on t,
Q
by A12, A39, A40, A41, A42, A43, A44;
y1 - 1
>= 0
by A42, A48, XREAL_1:47, XREAL_1:48;
then reconsider y0 =
y1 - 1 as
Element of
NAT by INT_1:3;
set jj =
(2 * k1) + 1;
A50:
(yn - y1) - 1
<= (k + 1) - 1
by A45, XREAL_1:9;
A51:
yn <= y1 + (k + 1)
by A45, XREAL_1:20;
consider f2 being
FinSequence of
INT such that A52:
len f2 = n
and A53:
for
i being
Nat st 1
<= i &
i <= len f2 holds
f2 . i = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + i))
by SCPISORT:1;
set It =
IExec (
I,
Q,
t);
A54:
(
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)) ) ) ) )
by A12, A39, A40, A41, A42, A43, A44;
then consider ym being
Nat such that A55:
y1 <= ym
and A56:
ym <= yn
and A57:
m + y1 = (IExec (I,Q,t)) . (intpos k2)
and A58:
(m + ym) - 1
= (IExec (I,Q,t)) . (intpos (k2 + 1))
and A59:
(m + ym) + 1
= (IExec (I,Q,t)) . (intpos (k2 + 2))
and A60:
m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3))
and A61:
for
j being
Nat st
y1 <= j &
j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym))
and A62:
for
j being
Nat st
ym < j &
j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym))
by A48, XREAL_1:47;
A63:
I is_closed_on t,
Q
by A12, A39, A40, A41, A42, A43, A44;
then A64:
DataPart (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) = DataPart (IExec (I,Q,t))
by A39, A40, A49, Th2, A38;
then A65:
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (DataLoc (c,i)) = (2 * k1) + 3
by A48, A54, SCMPDS_4:8, XREAL_1:47;
A66:
ym >= 1
by A42, A48, A55, XREAL_1:47, XXREAL_0:2;
then reconsider yc =
ym - 1 as
Element of
NAT by INT_1:3, XREAL_1:48;
A67:
yc <= yn
by A56, XREAL_1:146, XXREAL_0:2;
then A68:
yc <= n
by A42, A48, XREAL_1:47, XXREAL_0:2;
A69:
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (DataLoc (c,i)) = (2 * (k1 + 1)) + 1
by A48, A54, A64, SCMPDS_4:8, XREAL_1:47;
(IExec (I,Q,t)) . a = t . a
by A12, A39, A40, A41, A42, A43, A44;
then A70:
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . a = c
by A39, A64, SCMPDS_4:8;
set k3 =
((m + n) + (2 * (k1 + 1))) + 1;
set yd =
ym + 1;
A71:
ym + 1
> ym
by XREAL_1:29;
then A72:
ym + 1
>= y1
by A55, XXREAL_0:2;
then A73:
ym + 1
>= 1
by A42, A48, XREAL_1:47, XXREAL_0:2;
A74:
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos ((((m + n) + (2 * (k1 + 1))) + 1) + 1)) = m + yn
by A41, A64, A60, SCMPDS_4:8;
ym + (1 + k) >= y1 + (1 + k)
by A55, XREAL_1:6;
then
yn <= (ym + 1) + k
by A51, XXREAL_0:2;
then A75:
yn - (ym + 1) <= k
by XREAL_1:20;
A76:
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (((m + n) + (2 * (k1 + 1))) + 1)) = m + (ym + 1)
by A41, A64, A59, SCMPDS_4:8;
A77:
(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . a = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . a
by SCMPDS_5:15;
A78:
(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (DataLoc (c,i)) = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (DataLoc (c,i))
by SCMPDS_5:15;
A79:
(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos (((m + n) + (2 * (k1 + 1))) + 1)) = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (((m + n) + (2 * (k1 + 1))) + 1))
by SCMPDS_5:15;
A80:
(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos ((((m + n) + (2 * (k1 + 1))) + 1) + 1)) = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos ((((m + n) + (2 * (k1 + 1))) + 1) + 1))
by SCMPDS_5:15;
f2 is_FinSequence_on Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))),
m
proof
let i be
Nat;
SCPISORT:def 1 ( not 1 <= i or not i <= len f2 or f2 . i = (Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos (m + i)) )
assume
( 1
<= i &
i <= len f2 )
;
f2 . i = (Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos (m + i))
then
f2 . i = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + i))
by A53;
hence
f2 . i = (Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos (m + i))
by SCMPDS_5:15;
verum
end; then consider kl being
Nat,
f3 being
FinSequence of
INT such that A81:
Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) = Comput (
((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),
(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),
kl)
and A82:
f3 is_FinSequence_on Comput (
((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),
(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),
kl),
m
and A83:
len f3 = n
and A84:
f2,
f3 are_fiberwise_equipotent
and A85:
f3 is_non_decreasing_on ym + 1,
yn
and A86:
for
j being
Nat st
ym + 1
< yn & ( ( 1
<= j &
j < ym + 1 ) or (
yn < j &
j <= n ) ) holds
f3 . j = (Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos (m + j))
and A87:
for
j being
Nat st
ym + 1
>= yn & 1
<= j &
j <= n holds
f3 . j = (Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos (m + j))
and A88:
for
j being
Nat st 1
<= j &
j < (2 * (k1 + 1)) + 1 holds
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos ((m + n) + j)) = (Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos ((m + n) + j))
and A89:
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (DataLoc (c,i)) = ((Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (DataLoc (c,i))) - 2
and A90:
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . a = c
by A37, A73, A75, A52, A42, A48, A70, A77, A69, A78, A76, A79, A74, A80, XREAL_1:47;
A91:
Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) = Comput (
((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),
(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),
kl)
by A81;
A92:
f3 is_FinSequence_on Comput (
((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),
(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),
kl),
m
by A82;
A93:
len f3 = n
by A83;
A94:
f2,
f3 are_fiberwise_equipotent
by A84;
A95:
f3 is_non_decreasing_on ym + 1,
yn
by A85;
A96:
for
j being
Nat st
ym + 1
< yn & ( ( 1
<= j &
j < ym + 1 ) or (
yn < j &
j <= n ) ) holds
f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j))
proof
let j be
Nat;
( ym + 1 < yn & ( ( 1 <= j & j < ym + 1 ) or ( yn < j & j <= n ) ) implies f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j)) )
assume
(
ym + 1
< yn & ( ( 1
<= j &
j < ym + 1 ) or (
yn < j &
j <= n ) ) )
;
f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j))
then
f3 . j = (Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos (m + j))
by A86;
hence
f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j))
by SCMPDS_5:15;
verum
end; A97:
for
j being
Nat st
ym + 1
>= yn & 1
<= j &
j <= n holds
f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j))
proof
let j be
Nat;
( ym + 1 >= yn & 1 <= j & j <= n implies f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j)) )
assume
(
ym + 1
>= yn & 1
<= j &
j <= n )
;
f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j))
then
f3 . j = (Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos (m + j))
by A87;
hence
f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j))
by SCMPDS_5:15;
verum
end; A98:
for
j being
Nat st 1
<= j &
j < (2 * (k1 + 1)) + 1 holds
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos ((m + n) + j)) = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos ((m + n) + j))
proof
let j be
Nat;
( 1 <= j & j < (2 * (k1 + 1)) + 1 implies (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos ((m + n) + j)) = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos ((m + n) + j)) )
assume
( 1
<= j &
j < (2 * (k1 + 1)) + 1 )
;
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos ((m + n) + j)) = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos ((m + n) + j))
then
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos ((m + n) + j)) = (Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos ((m + n) + j))
by A88;
hence
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos ((m + n) + j)) = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos ((m + n) + j))
by SCMPDS_5:15;
verum
end; set t2 =
Comput (
((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),
(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),
kl);
set Q2 =
(Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)));
A99:
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (DataLoc (c,i)) = ((Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (DataLoc (c,i))) - 2
by A89, A78;
A100:
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . a = c
by A90;
A101:
(2 * k1) + 3
= (2 * (k1 + 1)) + 1
;
then
(2 * k1) + 1
< (2 * (k1 + 1)) + 1
by XREAL_1:6;
then A102:
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos k2) =
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos ((m + n) + ((2 * k1) + 1)))
by A41, A98, NAT_1:11
.=
m + y1
by A41, A64, A57, SCMPDS_4:8
;
A103:
ym <= n
by A42, A48, A56, XREAL_1:47, XXREAL_0:2;
A105:
now for i being Nat st 1 <= i & i <= ym holds
f3 . i = f2 . iend;
yc <= yn - 1
by A56, XREAL_1:9;
then
yc - y1 <= (yn - 1) - y1
by XREAL_1:9;
then A110:
yc - y1 <= k
by A50, XXREAL_0:2;
A111:
yc < ym + 1
by A71, XREAL_1:146, XXREAL_0:2;
set jj =
(2 * k1) + 2;
(2 * k1) + 2
>= 2
by NAT_1:11;
then A112:
(2 * k1) + 2
>= 1
by XXREAL_0:2;
(2 * k1) + 2
< (2 * (k1 + 1)) + 1
by A101, XREAL_1:6;
then A113:
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (k2 + 1)) =
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos ((m + n) + ((2 * k1) + 2)))
by A41, A98, A112
.=
m + yc
by A41, A64, A58, SCMPDS_4:8
;
A114:
( ( 1
<= y1 &
yc <= n ) or
y1 >= yc )
by A48, A68, A42, XREAL_1:47;
A115:
(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . a = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . a
by SCMPDS_5:15;
A116:
(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (DataLoc (c,i)) = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (DataLoc (c,i))
by SCMPDS_5:15;
A117:
(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (intpos k2) = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos k2)
by SCMPDS_5:15;
A118:
(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (intpos (k2 + 1)) = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (k2 + 1))
by SCMPDS_5:15;
f3 is_FinSequence_on Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)),
m
proof
let i be
Nat;
SCPISORT:def 1 ( not 1 <= i or not i <= len f3 or f3 . i = (Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (intpos (m + i)) )
assume
( 1
<= i &
i <= len f3 )
;
f3 . i = (Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (intpos (m + i))
then
f3 . i = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + i))
by A92;
hence
f3 . i = (Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (intpos (m + i))
by SCMPDS_5:15;
verum
end; then consider km being
Nat,
f4 being
FinSequence of
INT such that A119:
Initialize (Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) = Comput (
(((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),
(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),
km)
and A120:
f4 is_FinSequence_on Comput (
(((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),
(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),
km),
m
and A121:
len f4 = n
and A122:
f3,
f4 are_fiberwise_equipotent
and A123:
f4 is_non_decreasing_on y1,
yc
and A124:
for
j being
Nat st
y1 < yc & ( ( 1
<= j &
j < y1 ) or (
yc < j &
j <= n ) ) holds
f4 . j = (Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (intpos (m + j))
and A125:
for
j being
Nat st
y1 >= yc & 1
<= j &
j <= n holds
f4 . j = (Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (intpos (m + j))
and A126:
for
j being
Nat st 1
<= j &
j < (2 * k1) + 1 holds
(Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) . (intpos ((m + n) + j)) = (Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (intpos ((m + n) + j))
and A127:
(Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) . (DataLoc (c,i)) = ((Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (DataLoc (c,i))) - 2
and A128:
(Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) . a = c
by A37, A110, A93, A114, A41, A115, A100, A116, A65, A99, A117, A102, A118, A113;
A129:
Initialize (Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) = Comput (
(((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),
(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),
km)
by A119;
A130:
f4 is_FinSequence_on Comput (
(((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),
(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),
km),
m
by A120;
A131:
len f4 = n
by A121;
A132:
f3,
f4 are_fiberwise_equipotent
by A122;
A133:
f4 is_non_decreasing_on y1,
yc
by A123;
A134:
for
j being
Nat st
y1 < yc & ( ( 1
<= j &
j < y1 ) or (
yc < j &
j <= n ) ) holds
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))
proof
let j be
Nat;
( y1 < yc & ( ( 1 <= j & j < y1 ) or ( yc < j & j <= n ) ) implies f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j)) )
assume
(
y1 < yc & ( ( 1
<= j &
j < y1 ) or (
yc < j &
j <= n ) ) )
;
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))
then
f4 . j = (Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (intpos (m + j))
by A124;
hence
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))
by SCMPDS_5:15;
verum
end; A135:
for
j being
Nat st
y1 >= yc & 1
<= j &
j <= n holds
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))
proof
let j be
Nat;
( y1 >= yc & 1 <= j & j <= n implies f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j)) )
assume
(
y1 >= yc & 1
<= j &
j <= n )
;
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))
then
f4 . j = (Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (intpos (m + j))
by A125;
hence
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))
by SCMPDS_5:15;
verum
end; A136:
for
j being
Nat st 1
<= j &
j < (2 * k1) + 1 holds
(Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) . (intpos ((m + n) + j)) = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos ((m + n) + j))
proof
let j be
Nat;
( 1 <= j & j < (2 * k1) + 1 implies (Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) . (intpos ((m + n) + j)) = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos ((m + n) + j)) )
assume
( 1
<= j &
j < (2 * k1) + 1 )
;
(Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) . (intpos ((m + n) + j)) = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos ((m + n) + j))
then
(Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) . (intpos ((m + n) + j)) = (Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))) . (intpos ((m + n) + j))
by A126;
hence
(Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) . (intpos ((m + n) + j)) = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos ((m + n) + j))
by SCMPDS_5:15;
verum
end; A137:
(Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) . (DataLoc (c,i)) = ((Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (DataLoc (c,i))) - 2
by A127, A116;
A138:
(Comput ((((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),km)) . a = c
by A128;
A139:
now for i being Nat st yc < i & i <= len f4 holds
f4 . i = f3 . ilet i be
Nat;
( yc < i & i <= len f4 implies f4 . i = f3 . i )assume that A140:
yc < i
and A141:
i <= len f4
;
f4 . i = f3 . iA142:
1
+ 0 <= i
by A140, INT_1:7;
now f4 . i = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + i))per cases
( y1 < yc or y1 >= yc )
;
suppose
y1 < yc
;
f4 . i = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + i))hence
f4 . i = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + i))
by A131, A134, A140, A141;
verum end; suppose
y1 >= yc
;
f4 . i = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + i))hence
f4 . i = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + i))
by A131, A135, A141, A142;
verum end; end; end; hence
f4 . i = f3 . i
by A92, A93, A131, A141, A142;
verum end; then
f4 . ym = f3 . ym
by A131, A103, XREAL_1:146;
then A143:
f4 . ym = (IExec (I,Q,t)) . (intpos (m + ym))
by A64, A104, SCMPDS_4:8;
A144:
now for i being Nat st yn < i & i <= len f3 holds
f3 . i = f2 . iend; A148:
now for i being Nat st ym < i & i <= yn holds
f4 . ym <= f4 . ilet i be
Nat;
( ym < i & i <= yn implies f4 . ym <= f4 . i )assume that A149:
ym < i
and A150:
i <= yn
;
f4 . ym <= f4 . iconsider j being
Nat such that A151:
ym < j
and A152:
j <= yn
and A153:
f3 . i = f2 . j
by A42, A48, A56, A93, A94, A105, A144, A149, A150, RFINSEQ:32, XREAL_1:47;
A154:
yc < i
by A149, XREAL_1:146, XXREAL_0:2;
A155:
1
<= j
by A66, A151, XXREAL_0:2;
A156:
j <= len f2
by A42, A48, A52, A152, XREAL_1:47, XXREAL_0:2;
i <= len f4
by A42, A48, A131, A150, XREAL_1:47, XXREAL_0:2;
then f4 . i =
f2 . j
by A139, A154, A153
.=
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j))
by A53, A155, A156
.=
(IExec (I,Q,t)) . (intpos (m + j))
by A64, SCMPDS_4:8
;
hence
f4 . ym <= f4 . i
by A62, A143, A151, A152;
verum end; A157:
yn > y1
by A48, XREAL_1:47;
A158:
now for i being Nat st 1 <= i & i <= y0 holds
f4 . i = f3 . ilet i be
Nat;
( 1 <= i & i <= y0 implies f4 . i = f3 . i )assume that A159:
1
<= i
and A160:
i <= y0
;
f4 . i = f3 . i
i - 1
< y1 - 1
by A160, XREAL_1:146, XXREAL_0:2;
then A161:
i < y1
by XREAL_1:9;
y1 <= n
by A42, A157, XXREAL_0:2;
then A162:
i <= n
by A161, XXREAL_0:2;
now f4 . i = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + i))per cases
( y1 < yc or y1 >= yc )
;
suppose
y1 < yc
;
f4 . i = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + i))hence
f4 . i = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + i))
by A134, A159, A161;
verum end; suppose
y1 >= yc
;
f4 . i = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + i))hence
f4 . i = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + i))
by A135, A159, A162;
verum end; end; end; hence
f4 . i = f3 . i
by A92, A93, A159, A162;
verum end; A163:
y0 <= yc
by A55, XREAL_1:9;
A164:
now for i being Nat st y1 <= i & i < ym holds
f4 . i <= f4 . ymlet i be
Nat;
( y1 <= i & i < ym implies f4 . i <= f4 . ym )assume that A165:
y1 <= i
and A166:
i < ym
;
f4 . i <= f4 . ym
i + 1
<= ym
by A166, INT_1:7;
then A167:
i <= yc
by XREAL_1:19;
y0 < i
by A165, XREAL_1:146, XXREAL_0:2;
then consider j being
Nat such that A168:
y0 < j
and A169:
j <= yc
and A170:
f4 . i = f3 . j
by A68, A131, A132, A163, A158, A139, A167, RFINSEQ:32;
A171:
1
+ 0 <= j
by A168, INT_1:7;
A172:
j <= n
by A68, A169, XXREAL_0:2;
A173:
j < ym + 1
by A111, A169, XXREAL_0:2;
then A174:
f4 . i = (IExec (I,Q,t)) . (intpos (m + j))
by A64, A170, SCMPDS_4:8;
A175:
j < ym
by A169, XREAL_1:146, XXREAL_0:2;
(y1 - 1) + 1
<= j
by A168, INT_1:7;
hence
f4 . i <= f4 . ym
by A61, A143, A175, A174;
verum end; take mm =
((LifeSpan ((Q +* (stop I)),t)) + 2) + (kl + km);
ex f2 being FinSequence of INT st
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm) & f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm),m & len f2 = n & f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c )set tm =
Comput (
(Q +* (stop (while>0 (a,i,I)))),
t,
mm);
take
f4
;
( Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm) & f4 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm),m & len f4 = n & f1,f4 are_fiberwise_equipotent & f4 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c )
Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) = Comput (
(Q +* (stop (while>0 (a,i,I)))),
t,
((LifeSpan ((Q +* (stop I)),t)) + 2))
by A39, A40, A63, A49, Th2, A38;
then A176:
Comput (
(Q +* (stop (while>0 (a,i,I)))),
t,
mm) =
Comput (
(Q +* (stop (while>0 (a,i,I)))),
(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),
(kl + km))
by EXTPRO_1:4
.=
Comput (
(((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),
(Initialize (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl))),
km)
by A91, EXTPRO_1:4
;
hence
Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) = Comput (
(Q +* (stop (while>0 (a,i,I)))),
t,
mm)
by A129;
( f4 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm),m & len f4 = n & f1,f4 are_fiberwise_equipotent & f4 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c )thus
f4 is_FinSequence_on Comput (
(Q +* (stop (while>0 (a,i,I)))),
t,
mm),
m
by A130, A176;
( len f4 = n & f1,f4 are_fiberwise_equipotent & f4 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c )thus
len f4 = n
by A131;
( f1,f4 are_fiberwise_equipotent & f4 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c )now for i being Nat st 1 <= i & i <= len f2 holds
f2 . i = (IExec (I,Q,t)) . (intpos (m + i))let i be
Nat;
( 1 <= i & i <= len f2 implies f2 . i = (IExec (I,Q,t)) . (intpos (m + i)) )assume that A177:
1
<= i
and A178:
i <= len f2
;
f2 . i = (IExec (I,Q,t)) . (intpos (m + i))thus f2 . i =
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + i))
by A53, A177, A178
.=
(IExec (I,Q,t)) . (intpos (m + i))
by A64, SCMPDS_4:8
;
verum end; then
f2 is_FinSequence_on IExec (
I,
Q,
t),
m
;
then
f1,
f2 are_fiberwise_equipotent
by A12, A39, A40, A41, A42, A43, A44, A46, A47, A52;
then
f1,
f3 are_fiberwise_equipotent
by A94, CLASSES1:76;
hence
f1,
f4 are_fiberwise_equipotent
by A132, CLASSES1:76;
( f4 is_non_decreasing_on y1,yn & ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c )A179:
now for j being Nat st ym + 1 <= j & j <= yn holds
f4 . j = f3 . jlet j be
Nat;
( ym + 1 <= j & j <= yn implies f4 . j = f3 . j )assume that A180:
ym + 1
<= j
and A181:
j <= yn
;
f4 . j = f3 . jA182:
1
<= j
by A73, A180, XXREAL_0:2;
A183:
j <= n
by A42, A48, A181, XREAL_1:47, XXREAL_0:2;
A184:
yc < j
by A111, A180, XXREAL_0:2;
now f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))per cases
( y1 < yc or y1 >= yc )
;
suppose
y1 < yc
;
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))hence
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))
by A134, A183, A184;
verum end; suppose
y1 >= yc
;
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))hence
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))
by A135, A183, A182;
verum end; end; end; hence
f4 . j = f3 . j
by A92, A93, A183, A182;
verum end; now for i, j being Nat st ym + 1 <= i & i <= j & j <= yn holds
f4 . i <= f4 . jlet i,
j be
Nat;
( ym + 1 <= i & i <= j & j <= yn implies f4 . i <= f4 . j )assume that A185:
ym + 1
<= i
and A186:
i <= j
and A187:
j <= yn
;
f4 . i <= f4 . j
ym + 1
<= j
by A185, A186, XXREAL_0:2;
then A188:
f4 . j = f3 . j
by A179, A187;
i <= yn
by A186, A187, XXREAL_0:2;
then
f4 . i = f3 . i
by A179, A185;
hence
f4 . i <= f4 . j
by A95, A185, A186, A187, A188, FINSEQ_6:def 9;
verum end; then
f4 is_non_decreasing_on ym + 1,
yn
by FINSEQ_6:def 9;
hence
f4 is_non_decreasing_on y1,
yn
by A133, A164, A148, Th8;
( ( for j being Nat st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c )thus
for
j being
Nat st
y1 < yn & ( ( 1
<= j &
j < y1 ) or (
yn < j &
j <= n ) ) holds
f4 . j = t . (intpos (m + j))
( ( for j being Nat st y1 >= yn & 1 <= j & j <= n holds
f4 . j = t . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c )proof
let j be
Nat;
( y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) implies f4 . j = t . (intpos (m + j)) )
assume that A189:
y1 < yn
and A190:
( ( 1
<= j &
j < y1 ) or (
yn < j &
j <= n ) )
;
f4 . j = t . (intpos (m + j))
A191:
( 1
<= j &
j <= n )
A194:
( ( 1
<= j &
j < ym + 1 ) or (
yn < j &
j <= n ) )
A196:
( ( 1
<= j &
j < y1 ) or (
yc < j &
j <= n ) )
now f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))per cases
( y1 < yc or y1 >= yc )
;
suppose
y1 < yc
;
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))hence
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))
by A134, A196;
verum end; suppose
y1 >= yc
;
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))hence
f4 . j = (Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos (m + j))
by A135, A191;
verum end; end; end;
hence f4 . j =
f3 . j
by A92, A93, A191
.=
(IExec (I,Q,t)) . (intpos (m + j))
by A64, A195, SCMPDS_4:8
.=
t . (intpos (m + j))
by A12, A39, A40, A41, A42, A43, A44, A189, A190
;
verum
end; thus
for
j being
Nat st
y1 >= yn & 1
<= j &
j <= n holds
f4 . j = t . (intpos (m + j))
by A48, XREAL_1:47;
( ( for j being Nat st 1 <= j & j < (2 * k1) + 1 holds
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c )hereby ( (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c )
let j be
Nat;
( 1 <= j & j < (2 * k1) + 1 implies (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) )assume that A197:
1
<= j
and A198:
j < (2 * k1) + 1
;
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j))
(2 * k1) + 1
< (2 * (k1 + 1)) + 1
by A101, XREAL_1:6;
then A199:
j < (2 * (k1 + 1)) + 1
by A198, XXREAL_0:2;
thus (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (intpos ((m + n) + j)) =
(Comput (((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),kl)) . (intpos ((m + n) + j))
by A136, A176, A197, A198
.=
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos ((m + n) + j))
by A98, A197, A199
.=
(IExec (I,Q,t)) . (intpos ((m + n) + j))
by A64, SCMPDS_4:8
.=
t . (intpos ((m + n) + j))
by A12, A39, A40, A41, A42, A43, A44, A197, A198
;
verum
end; thus
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2
by A40, A65, A99, A137, A176;
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = cthus
(Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c
by A138, A176;
verum end; end;
end; hence
S1[
k + 1]
;
verum end;
A200:
for k being Nat holds S1[k]
from NAT_1:sch 2(A13, A36);
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) = Comput ((P +* (stop (while>0 (a,i,I)))),s,k) & f2 is_FinSequence_on Comput ((P +* (stop (while>0 (a,i,I)))),s,k),m & len f2 = n & f,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n & ( for j being Nat st 1 < n & ( ( 1 <= j & j < 1 ) or ( n < j & j <= n ) ) holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Nat st 1 >= n & 1 <= j & j <= n holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * 0) + 1 holds
(Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (intpos ((m + n) + j)) = s . (intpos ((m + n) + j)) ) & (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (DataLoc (c,i)) = (s . (DataLoc (c,i))) - 2 & (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . a = c )
proof
per cases
( n - 1 <= 0 or n - 1 > 0 )
;
suppose
n - 1
<= 0
;
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) = Comput ((P +* (stop (while>0 (a,i,I)))),s,k) & f2 is_FinSequence_on Comput ((P +* (stop (while>0 (a,i,I)))),s,k),m & len f2 = n & f,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n & ( for j being Nat st 1 < n & ( ( 1 <= j & j < 1 ) or ( n < j & j <= n ) ) holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Nat st 1 >= n & 1 <= j & j <= n holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * 0) + 1 holds
(Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (intpos ((m + n) + j)) = s . (intpos ((m + n) + j)) ) & (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (DataLoc (c,i)) = (s . (DataLoc (c,i))) - 2 & (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . a = c )hence
ex
k being
Nat ex
f2 being
FinSequence of
INT st
(
Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) = Comput (
(P +* (stop (while>0 (a,i,I)))),
s,
k) &
f2 is_FinSequence_on Comput (
(P +* (stop (while>0 (a,i,I)))),
s,
k),
m &
len f2 = n &
f,
f2 are_fiberwise_equipotent &
f2 is_non_decreasing_on 1,
n & ( for
j being
Nat st 1
< n & ( ( 1
<= j &
j < 1 ) or (
n < j &
j <= n ) ) holds
f2 . j = s . (intpos (m + j)) ) & ( for
j being
Nat st 1
>= n & 1
<= j &
j <= n holds
f2 . j = s . (intpos (m + j)) ) & ( for
j being
Nat st 1
<= j &
j < (2 * 0) + 1 holds
(Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (intpos ((m + n) + j)) = s . (intpos ((m + n) + j)) ) &
(Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (DataLoc (c,i)) = (s . (DataLoc (c,i))) - 2 &
(Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . a = c )
by A2, A3, A5, A7, A9, A10, A13, A11;
verum end; suppose
n - 1
> 0
;
ex k being Nat ex f2 being FinSequence of INT st
( Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) = Comput ((P +* (stop (while>0 (a,i,I)))),s,k) & f2 is_FinSequence_on Comput ((P +* (stop (while>0 (a,i,I)))),s,k),m & len f2 = n & f,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n & ( for j being Nat st 1 < n & ( ( 1 <= j & j < 1 ) or ( n < j & j <= n ) ) holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Nat st 1 >= n & 1 <= j & j <= n holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Nat st 1 <= j & j < (2 * 0) + 1 holds
(Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (intpos ((m + n) + j)) = s . (intpos ((m + n) + j)) ) & (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (DataLoc (c,i)) = (s . (DataLoc (c,i))) - 2 & (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . a = c )then reconsider nn =
n - 1 as
Element of
NAT by INT_1:3;
S1[
nn]
by A200;
hence
ex
k being
Nat ex
f2 being
FinSequence of
INT st
(
Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) = Comput (
(P +* (stop (while>0 (a,i,I)))),
s,
k) &
f2 is_FinSequence_on Comput (
(P +* (stop (while>0 (a,i,I)))),
s,
k),
m &
len f2 = n &
f,
f2 are_fiberwise_equipotent &
f2 is_non_decreasing_on 1,
n & ( for
j being
Nat st 1
< n & ( ( 1
<= j &
j < 1 ) or (
n < j &
j <= n ) ) holds
f2 . j = s . (intpos (m + j)) ) & ( for
j being
Nat st 1
>= n & 1
<= j &
j <= n holds
f2 . j = s . (intpos (m + j)) ) & ( for
j being
Nat st 1
<= j &
j < (2 * 0) + 1 holds
(Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (intpos ((m + n) + j)) = s . (intpos ((m + n) + j)) ) &
(Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (DataLoc (c,i)) = (s . (DataLoc (c,i))) - 2 &
(Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . a = c )
by A2, A3, A5, A7, A9, A10, A11;
verum end; end;
end;
then consider k being Nat, f2 being FinSequence of INT such that
A201:
Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) = Comput ((P +* (stop (while>0 (a,i,I)))),s,k)
and
A202:
f2 is_FinSequence_on Comput ((P +* (stop (while>0 (a,i,I)))),s,k),m
and
A203:
len f2 = n
and
A204:
f,f2 are_fiberwise_equipotent
and
A205:
f2 is_non_decreasing_on 1,n
and
A206:
(Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (DataLoc (c,i)) = (s . (DataLoc (c,i))) - 2
and
A207:
(Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . a = c
;
set sk = Comput ((P +* (stop (while>0 (a,i,I)))),s,k);
set s1 = Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k));
set P1 = (P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)));
set s2 = Comput (((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))),1);
set P2 = (P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)));
A208:
IC (Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))) = 0
by MEMSTR_0:def 11;
set i1 = (a,i) <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
A209:
card (while>0 (a,i,I)) = (card I) + 2
by SCMPDS_8:17;
then A210:
(card I) + 2 in dom (stop (while>0 (a,i,I)))
by COMPOS_1:64;
A211:
dom g = Seg n
by A4, FINSEQ_1:def 3;
stop (while>0 (a,i,I)) c= (P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))
by FUNCT_4:25;
then A212: ((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) . ((card I) + 2) =
(stop (while>0 (a,i,I))) . ((card I) + 2)
by A210, GRFUNC_1:2
.=
halt SCMPDS
by A209, COMPOS_1:64
;
A213:
while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1))))
by Lm1;
A214: Comput (((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))),(0 + 1)) =
Following (((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Comput (((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))),0)))
by EXTPRO_1:3
.=
Exec (((a,i) <=0_goto ((card I) + 2)),(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))))
by A213, SCMPDS_6:11
;
IC (Comput (((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))),1)) =
ICplusConst ((Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))),((card I) + 2))
by A7, A201, A206, A207, A214, SCMPDS_2:56
.=
0 + ((card I) + 2)
by A208, SCMPDS_6:12
;
then A215:
CurInstr (((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Comput (((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))),1))) = halt SCMPDS
by A212, PBOOLE:143;
A216:
Comput (((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))),1) = Comput ((P +* (stop (while>0 (a,i,I)))),s,(k + 1))
by A201, EXTPRO_1:4;
A217:
P +* (stop (while>0 (a,i,I))) halts_on s
by A215, A216, EXTPRO_1:29;
hence
while>0 (a,i,I) is_halting_on s,P
by A1, SCMPDS_6:def 3; ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
A218:
Result ((P +* (stop (while>0 (a,i,I)))),s) = Comput (((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))),1)
by A215, A216, A217, EXTPRO_1:def 9;
now for i being Nat st i in dom g holds
g . i = f2 . ilet i be
Nat;
( i in dom g implies g . i = f2 . i )reconsider a =
i as
Nat ;
set xi =
intpos (m + a);
assume A219:
i in dom g
;
g . i = f2 . ithen A220:
1
<= i
by A211, FINSEQ_1:1;
A221:
i <= n
by A211, A219, FINSEQ_1:1;
IExec (
(while>0 (a,i,I)),
P,
s)
= Comput (
((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),
(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))),1)
by A218, SCMPDS_4:def 5;
hence g . i =
(Comput (((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))),1)) . (intpos (m + a))
by A4, A6, A220, A221
.=
(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))) . (intpos (m + a))
by A214, SCMPDS_2:56
.=
f2 . i
by A201, A202, A203, A220, A221
;
verum end;
hence
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
by A4, A203, A204, A205, FINSEQ_2:9; verum