let P be Instruction-Sequence of SCMPDS; :: thesis:
let s be 0 -started State of SCMPDS; :: thesis:
let I be halt-free shiftable Program of SCMPDS; :: thesis:
let a be Int_position ; :: thesis:
let i, c be Integer; :: thesis:
let f, g be FinSequence of INT ; :: thesis:
let m, n, m1 be Element of NAT ; :: thesis:
I: 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 ; :: thesis:
set WH = while>0 (a,i,I);
set sWH = stop (while>0 (a,i,I));
assume A5: f is_FinSequence_on s,m ; :: thesis:
defpred S₁[ Element of 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 Element of 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 Element of 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 Element of NAT st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Element of NAT st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Element of 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 ; :: thesis:
assume A7: 1 = s . (DataLoc (c,i)) ; :: thesis:
assume that
A8: m1 = (m + n) + 1 and
A9: m + 1 = s . (intpos m1) and
A10: m + n = s . (intpos (m1 + 1)) ; :: thesis:
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 Element of NAT st t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t,Q & I is_halting_on t,Q & (IExec (I,Q,t)) . a = t . a & ( for j being Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Element of 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 ) ) ; :: thesis:
A13: S₁[ 0 ]

proof

let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
let f1 be FinSequence of INT ; :: thesis:
let k1, k2, y1, yn be Element of NAT ; :: thesis:
T: Initialize t = t by MEMSTR_0:44;
assume that
A14: t . a = c and
A15: (2 * k1) + 1 = t . (DataLoc (c,i)) and
A16: k2 = ((m + n) + (2 * k1)) + 1 and
A17: ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) and
A18: m + y1 = t . (intpos k2) and
A19: m + yn = t . (intpos (k2 + 1)) and
A20: yn - y1 <= 0 and
A21: f1 is_FinSequence_on t,m and
A22: len f1 = n ; :: thesis:
A23: I is_halting_on t,Q by A12, A14, A15, A16, A17, A18, A19;
take k = (LifeSpan ((Q +* (stop I)),t)) + 2; :: thesis:
set tk = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k);
A24: I is_closed_on t,Q by A12, A14, A15, A16, A17, A18, A19;
then A25: DataPart (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = DataPart (IExec (I,Q,t)) by A14, A15, A23, Th2, T;
consider f2 being FinSequence of INT such that
A26: len f2 = n and
A27: for i being Element of NAT st 1 <= i & i <= len f2 holds
f2 . i = (IExec (I,Q,t)) . (intpos (m + i)) by SCPISORT:1;
take f2 ; :: thesis:
thus Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) = Comput ((Q +* (stop (while>0 (a,i,I)))),t,k) by A14, A15, A24, A23, Th2, T; :: thesis:

now

let i be Element of NAT ; :: thesis:
assume that
A28: 1 <= i and
A29: i <= len f2 ; :: thesis:
thus f2 . i = (IExec (I,Q,t)) . (intpos (m + i)) by A27, A28, A29
.= (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos (m + i)) by A25, SCMPDS_4:8 ; :: thesis:

end;

hence f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m by SCPISORT:def 1; :: thesis:
thus len f2 = n by A26; :: thesis:
f2 is_FinSequence_on IExec (I,Q,t),m by A27, SCPISORT:def 1;
hence f1,f2 are_fiberwise_equipotent by A12, A14, A15, A16, A17, A18, A19, A21, A22, A26; :: thesis:
thus f2 is_non_decreasing_on y1,yn by A20, GRAPH_2:63, XREAL_1:50; :: thesis:
thus for j being Element of NAT st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) by A20, XREAL_1:50; :: thesis:

hereby :: thesis:

let j be Element of NAT ; :: thesis:
assume that
A30: y1 >= yn and
A31: 1 <= j and
A32: j <= n ; :: thesis:
thus f2 . j = (IExec (I,Q,t)) . (intpos (m + j)) by A26, A27, A31, A32
.= t . (intpos (m + j)) by A12, A14, A15, A16, A18, A19, A30, A31, A32 ; :: thesis:

end;

hereby :: thesis:

let j be Element of NAT ; :: thesis:
assume that
A33: 1 <= j and
A34: j < (2 * k1) + 1 ; :: thesis:
thus (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (intpos ((m + n) + j)) = (IExec (I,Q,t)) . (intpos ((m + n) + j)) by A25, SCMPDS_4:8
.= t . (intpos ((m + n) + j)) by A12, A14, A15, A16, A17, A18, A19, A33, A34 ; :: thesis:

end;

( y1 >= yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) by A12, A14, A15, A16, A18, A19;
hence (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 by A15, A20, A25, SCMPDS_4:8, XREAL_1:50; :: thesis:
(IExec (I,Q,t)) . a = t . a by A12, A14, A15, A16, A17, A18, A19;
hence (Comput ((Q +* (stop (while>0 (a,i,I)))),t,k)) . a = c by A14, A25, SCMPDS_4:8; :: thesis:

end;

A35: now

let k be Element of NAT ; :: thesis:
assume A36: S₁[k] ; :: thesis:
S₁[k + 1]

proof

per cases ;

suppose yn - y1 <= 0 ; :: thesis:

hence ex kk being Element of 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 Element of NAT st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Element of NAT st y1 >= yn & 1 <= j & j <= n holds
f2 . j = t . (intpos (m + j)) ) & ( for j being Element of 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, A37, A38, A39, A40, A41, A42, A44, A45; :: thesis:

end;

suppose A46: yn - y1 > 0 ; :: thesis:

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)));
A47: I is_halting_on t,Q by A12, A37, A38, A39, A40, A41, A42;
y1 - 1 >= 0 by A40, A46, XREAL_1:47, XREAL_1:48;
then reconsider y0 = y1 - 1 as Element of NAT by INT_1:3;
set jj = (2 * k1) + 1;
A48: (yn - y1) - 1 <= (k + 1) - 1 by A43, XREAL_1:9;
A49: yn <= y1 + (k + 1) by A43, XREAL_1:20;
consider f2 being FinSequence of INT such that
A50: len f2 = n and
A51: for i being Element of 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);
A53: ( y1 < yn implies ( (IExec (I,Q,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,Q,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of 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 Element of NAT st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) ) ) ) ) by A12, A37, A38, A39, A40, A41, A42;
then consider ym being Element of NAT such that
A54: y1 <= ym and
A55: ym <= yn and
A56: m + y1 = (IExec (I,Q,t)) . (intpos k2) and
A57: (m + ym) - 1 = (IExec (I,Q,t)) . (intpos (k2 + 1)) and
A58: (m + ym) + 1 = (IExec (I,Q,t)) . (intpos (k2 + 2)) and
A59: m + yn = (IExec (I,Q,t)) . (intpos (k2 + 3)) and
A60: for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,Q,t)) . (intpos (m + j)) <= (IExec (I,Q,t)) . (intpos (m + ym)) and
A61: for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,Q,t)) . (intpos (m + j)) >= (IExec (I,Q,t)) . (intpos (m + ym)) by A46, XREAL_1:47;
A62: I is_closed_on t,Q by A12, A37, A38, A39, A40, A41, A42;
then A63: DataPart (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) = DataPart (IExec (I,Q,t)) by A37, A38, A47, Th2, T;
then A64: (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (DataLoc (c,i)) = (2 * k1) + 3 by A46, A53, SCMPDS_4:8, XREAL_1:47;
A65: ym >= 1 by A40, A46, A54, XREAL_1:47, XXREAL_0:2;
then reconsider yc = ym - 1 as Element of NAT by INT_1:3, XREAL_1:48;
A66: yc <= yn by A55, XREAL_1:146, XXREAL_0:2;
then A67: yc <= n by A40, A46, XREAL_1:47, XXREAL_0:2;
A68: (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (DataLoc (c,i)) = (2 * (k1 + 1)) + 1 by A46, A53, A63, SCMPDS_4:8, XREAL_1:47;
(IExec (I,Q,t)) . a = t . a by A12, A37, A38, A39, A40, A41, A42;
then A69: (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . a = c by A37, A63, SCMPDS_4:8;
set k3 = ((m + n) + (2 * (k1 + 1))) + 1;
set yd = ym + 1;
A70: ym + 1 > ym by XREAL_1:29;
then A71: ym + 1 >= y1 by A54, XXREAL_0:2;
then A72: ym + 1 >= 1 by A40, A46, XREAL_1:47, XXREAL_0:2;
A73: (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 A39, A63, A59, SCMPDS_4:8;
ym + (1 + k) >= y1 + (1 + k) by A54, XREAL_1:6;
then yn <= (ym + 1) + k by A49, XXREAL_0:2;
then A74: yn - (ym + 1) <= k by XREAL_1:20;
AA: (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 A39, A63, A58, SCMPDS_4:8;
X1: (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;
X2: (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;
X3: (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;
X4: (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 Element of NAT ; :: according to SCPISORT:def 1 :: thesis:
assume ( 1 <= i & i <= len f2 ) ; :: thesis:
then f2 . i = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + i)) by A51;
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; :: thesis:

end;

then consider kl being Element of NAT , f3 being FinSequence of INT such that
W1: 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
W2: 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
W3: len f3 = n and
W4: f2,f3 are_fiberwise_equipotent and
W5: f3 is_non_decreasing_on ym + 1,yn and
W6: for j being Element of 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
W7: for j being Element of 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
W8: for j being Element of 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
W9: (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
W10: (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 A36, A72, A74, A50, A40, A46, A69, X1, A68, X2, AA, X3, A73, X4, XREAL_1:47;
A75: 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 W1;
A76: 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 W2;
A77: len f3 = n by W3;
A78: f2,f3 are_fiberwise_equipotent by W4;
A79: f3 is_non_decreasing_on ym + 1,yn by W5;
A80: for j being Element of 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 Element of NAT ; :: thesis:
assume ( ym + 1 < yn & ( ( 1 <= j & j < ym + 1 ) or ( yn < j & j <= n ) ) ) ; :: thesis:
then f3 . j = (Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos (m + j)) by W6;
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; :: thesis:

end;

A81: for j being Element of 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 Element of NAT ; :: thesis:
assume ( ym + 1 >= yn & 1 <= j & j <= n ) ; :: thesis:
then f3 . j = (Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))) . (intpos (m + j)) by W7;
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; :: thesis:

end;

A82: for j being Element of 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 Element of NAT ; :: thesis:
assume ( 1 <= j & j < (2 * (k1 + 1)) + 1 ) ; :: thesis:
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 W8;
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; :: thesis:

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)));
A83: (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 W9, X2;
A84: (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 W10;
A85: ((Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I))) = (Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I))) by FUNCT_4:93;
A86: (2 * k1) + 3 = (2 * (k1 + 1)) + 1 ;
then (2 * k1) + 1 < (2 * (k1 + 1)) + 1 by XREAL_1:6;
then A87: (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 A39, A82, NAT_1:11
.= m + y1 by A39, A63, A56, SCMPDS_4:8 ;
A88: ym <= n by A40, A46, A55, XREAL_1:47, XXREAL_0:2;

A89: now

per cases ;

suppose ym + 1 < yn ; :: thesis:

hence f3 . ym = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + ym)) by A70, A80, A65; :: thesis:

end;

suppose ym + 1 >= yn ; :: thesis:

hence f3 . ym = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + ym)) by A81, A65, A88; :: thesis:

end;

A90: now

let i be Element of NAT ; :: thesis:
assume that
A91: 1 <= i and
A92: i <= ym ; :: thesis:
A93: i <= n by A88, A92, XXREAL_0:2;
A94: i < ym + 1 by A70, A92, XXREAL_0:2;

now

per cases ;

suppose ym + 1 < yn ; :: thesis:

hence f3 . i = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + i)) by A80, A91, A94; :: thesis:

end;

suppose ym + 1 >= yn ; :: thesis:

hence f3 . i = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + i)) by A81, A91, A93; :: thesis:

end;

hence f3 . i = f2 . i by A50, A51, A91, A93; :: thesis:

end;

yc <= yn - 1 by A55, XREAL_1:9;
then yc - y1 <= (yn - 1) - y1 by XREAL_1:9;
then A95: yc - y1 <= k by A48, XXREAL_0:2;
A96: yc < ym + 1 by A70, XREAL_1:146, XXREAL_0:2;
set jj = (2 * k1) + 2;
(2 * k1) + 2 >= 2 by NAT_1:11;
then A97: (2 * k1) + 2 >= 1 by XXREAL_0:2;
(2 * k1) + 2 < (2 * (k1 + 1)) + 1 by A86, XREAL_1:6;
then AA: (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 A39, A82, A97
.= m + yc by A39, A63, A57, SCMPDS_4:8 ;
YY: ( ( 1 <= y1 & yc <= n ) or y1 >= yc ) by A46, A67, A40, XREAL_1:47;
X1: (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;
X2: (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;
X3: (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;
X4: (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 Element of NAT ; :: according to SCPISORT:def 1 :: thesis:
assume ( 1 <= i & i <= len f3 ) ; :: thesis:
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 A76, SCPISORT:def 1;
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; :: thesis:

end;

then consider km being Element of NAT , f4 being FinSequence of INT such that
W1: 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
W2: 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
W3: len f4 = n and
W4: f3,f4 are_fiberwise_equipotent and
W5: f4 is_non_decreasing_on y1,yc and
W6: for j being Element of 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
W7: for j being Element of 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
W8: for j being Element of 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
W9: (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
W10: (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 A36, A95, A77, YY, A39, X1, A84, X2, A64, A83, X3, A87, X4, AA;
A98: 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 W1;
A99: 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 W2;
A100: len f4 = n by W3;
A101: f3,f4 are_fiberwise_equipotent by W4;
A102: f4 is_non_decreasing_on y1,yc by W5;
A103: for j being Element of 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 Element of NAT ; :: thesis:
assume ( y1 < yc & ( ( 1 <= j & j < y1 ) or ( yc < j & j <= n ) ) ) ; :: thesis:
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 W6;
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; :: thesis:

end;

A104: for j being Element of 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 Element of NAT ; :: thesis:
assume ( y1 >= yc & 1 <= j & j <= n ) ; :: thesis:
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 W7;
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; :: thesis:

end;

A105: for j being Element of 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 Element of NAT ; :: thesis:
assume ( 1 <= j & j < (2 * k1) + 1 ) ; :: thesis:
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 W8;
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; :: thesis:

end;

A106: (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 W9, X2;
A107: (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 W10;

A108: now

let i be Element of NAT ; :: thesis:
assume that
A109: yc < i and
A110: i <= len f4 ; :: thesis:
A111: 1 + 0 <= i by A109, INT_1:7;

now

per cases ;

suppose y1 < yc ; :: thesis:

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 A100, A103, A109, A110; :: thesis:

end;

suppose y1 >= yc ; :: thesis:

end;

hence f4 . i = f3 . i by A76, A77, A100, A110, A111, SCPISORT:def 1; :: thesis:

end;

then f4 . ym = f3 . ym by A100, A88, XREAL_1:146;
then A112: f4 . ym = (IExec (I,Q,t)) . (intpos (m + ym)) by A63, A89, SCMPDS_4:8;

A113: now

let i be Element of NAT ; :: thesis:
assume that
A114: yn < i and
A115: i <= len f3 ; :: thesis:
A116: 1 + 0 <= i by A114, INT_1:7;

now

per cases ;

suppose ym + 1 < yn ; :: thesis:

hence f3 . i = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + i)) by A77, A80, A114, A115; :: thesis:

end;

suppose ym + 1 >= yn ; :: thesis:

hence f3 . i = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + i)) by A77, A81, A115, A116; :: thesis:

end;

hence f3 . i = f2 . i by A50, A51, A77, A115, A116; :: thesis:

end;

A117: now

let i be Element of NAT ; :: thesis:
assume that
A118: ym < i and
A119: i <= yn ; :: thesis:
consider j being Element of NAT such that
A120: ym < j and
A121: j <= yn and
A122: f3 . i = f2 . j by A40, A46, A55, A77, A78, A90, A113, A118, A119, RFINSEQ:32, XREAL_1:47;
A123: yc < i by A118, XREAL_1:146, XXREAL_0:2;
A124: 1 <= j by A65, A120, XXREAL_0:2;
A125: j <= len f2 by A40, A46, A50, A121, XREAL_1:47, XXREAL_0:2;
i <= len f4 by A40, A46, A100, A119, XREAL_1:47, XXREAL_0:2;
then f4 . i = f2 . j by A108, A123, A122
.= (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j)) by A51, A124, A125
.= (IExec (I,Q,t)) . (intpos (m + j)) by A63, SCMPDS_4:8 ;
hence f4 . ym <= f4 . i by A61, A112, A120, A121; :: thesis:

end;

A126: yn > y1 by A46, XREAL_1:47;

A127: now

let i be Element of NAT ; :: thesis:
assume that
A128: 1 <= i and
A129: i <= y0 ; :: thesis:
i - 1 < y1 - 1 by A129, XREAL_1:146, XXREAL_0:2;
then A130: i < y1 by XREAL_1:9;
y1 <= n by A40, A126, XXREAL_0:2;
then A131: i <= n by A130, XXREAL_0:2;

now

per cases ;

suppose y1 < yc ; :: thesis:

end;

suppose y1 >= yc ; :: thesis:

end;

hence f4 . i = f3 . i by A76, A77, A128, A131, SCPISORT:def 1; :: thesis:

end;

A132: y0 <= yc by A54, XREAL_1:9;

A133: now

let i be Element of NAT ; :: thesis:
assume that
A134: y1 <= i and
A135: i < ym ; :: thesis:
i + 1 <= ym by A135, INT_1:7;
then A136: i <= yc by XREAL_1:19;
y0 < i by A134, XREAL_1:146, XXREAL_0:2;
then consider j being Element of NAT such that
A137: y0 < j and
A138: j <= yc and
A139: f4 . i = f3 . j by A67, A100, A101, A132, A127, A108, A136, RFINSEQ:32;
A140: 1 + 0 <= j by A137, INT_1:7;
A141: j <= n by A67, A138, XXREAL_0:2;
A142: j < ym + 1 by A96, A138, XXREAL_0:2;

now

per cases ;

suppose ym + 1 < yn ; :: thesis:

hence f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j)) by A80, A140, A142; :: thesis:

end;

suppose ym + 1 >= yn ; :: thesis:

hence f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j)) by A81, A140, A141; :: thesis:

end;

then A143: f4 . i = (IExec (I,Q,t)) . (intpos (m + j)) by A63, A139, SCMPDS_4:8;
A144: j < ym by A138, XREAL_1:146, XXREAL_0:2;
(y1 - 1) + 1 <= j by A137, INT_1:7;
hence f4 . i <= f4 . ym by A60, A112, A144, A143; :: thesis:

end;

take mm = ((LifeSpan ((Q +* (stop I)),t)) + 2) + (kl + km); :: thesis:
set tm = Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm);
take f4 ; :: thesis:
A145: (Q +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I))) = Q +* (stop (while>0 (a,i,I))) by FUNCT_4:93;
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 A37, A38, A62, A47, Th2, T;
then A146: 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)))),(Initialize (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2)))),(kl + km)) by A145
.= 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 A75, A85, 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 A98; :: thesis:
thus f4 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm),m by A99, A146; :: thesis:
thus len f4 = n by A100; :: thesis:

now

let i be Element of NAT ; :: thesis:
assume that
A147: 1 <= i and
A148: i <= len f2 ; :: thesis:
thus f2 . i = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + i)) by A51, A147, A148
.= (IExec (I,Q,t)) . (intpos (m + i)) by A63, SCMPDS_4:8 ; :: thesis:

end;

then f2 is_FinSequence_on IExec (I,Q,t),m by SCPISORT:def 1;
then f1,f2 are_fiberwise_equipotent by A12, A37, A38, A39, A40, A41, A42, A44, A45, A50;
then f1,f3 are_fiberwise_equipotent by A78, CLASSES1:76;
hence f1,f4 are_fiberwise_equipotent by A101, CLASSES1:76; :: thesis:

A149: now

let j be Element of NAT ; :: thesis:
assume that
A150: ym + 1 <= j and
A151: j <= yn ; :: thesis:
A152: 1 <= j by A72, A150, XXREAL_0:2;
A153: j <= n by A40, A46, A151, XREAL_1:47, XXREAL_0:2;
A154: yc < j by A96, A150, XXREAL_0:2;

now

per cases ;

suppose y1 < yc ; :: thesis:

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 A103, A153, A154; :: thesis:

end;

suppose y1 >= yc ; :: thesis:

end;

hence f4 . j = f3 . j by A76, A77, A153, A152, SCPISORT:def 1; :: thesis:

end;

now

let i, j be Element of NAT ; :: thesis:
assume that
A155: ym + 1 <= i and
A156: i <= j and
A157: j <= yn ; :: thesis:
ym + 1 <= j by A155, A156, XXREAL_0:2;
then A158: f4 . j = f3 . j by A149, A157;
i <= yn by A156, A157, XXREAL_0:2;
then f4 . i = f3 . i by A149, A155;
hence f4 . i <= f4 . j by A79, A155, A156, A157, A158, GRAPH_2:def 12; :: thesis:

end;

then f4 is_non_decreasing_on ym + 1,yn by GRAPH_2:def 12;
hence f4 is_non_decreasing_on y1,yn by A102, A133, A117, Th8; :: thesis:
thus for j being Element of NAT st y1 < yn & ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
f4 . j = t . (intpos (m + j)) :: thesis:

proof

let j be Element of NAT ; :: thesis:
assume that
A159: y1 < yn and
A160: ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) ; :: thesis:
A161: ( 1 <= j & j <= n )

proof

per cases by A160;

suppose A162: ( 1 <= j & j < y1 ) ; :: thesis:

then j < yn by A159, XXREAL_0:2;
hence ( 1 <= j & j <= n ) by A40, A46, A162, XREAL_1:47, XXREAL_0:2; :: thesis:

end;

suppose A163: ( yn < j & j <= n ) ; :: thesis:

then y1 < j by A159, XXREAL_0:2;
hence ( 1 <= j & j <= n ) by A40, A46, A163, XREAL_1:47, XXREAL_0:2; :: thesis:

end;

A164: ( ( 1 <= j & j < ym + 1 ) or ( yn < j & j <= n ) )

proof

per cases by A160;

suppose ( 1 <= j & j < y1 ) ; :: thesis:

hence ( ( 1 <= j & j < ym + 1 ) or ( yn < j & j <= n ) ) by A71, XXREAL_0:2; :: thesis:

end;

suppose ( yn < j & j <= n ) ; :: thesis:

hence ( ( 1 <= j & j < ym + 1 ) or ( yn < j & j <= n ) ) ; :: thesis:

end;

A165: now

per cases ;

suppose ym + 1 < yn ; :: thesis:

hence f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j)) by A80, A164; :: thesis:

end;

suppose ym + 1 >= yn ; :: thesis:

hence f3 . j = (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos (m + j)) by A81, A161; :: thesis:

end;

A166: ( ( 1 <= j & j < y1 ) or ( yc < j & j <= n ) )

proof

per cases by A160;

suppose ( 1 <= j & j < y1 ) ; :: thesis:

hence ( ( 1 <= j & j < y1 ) or ( yc < j & j <= n ) ) ; :: thesis:

end;

suppose ( yn < j & j <= n ) ; :: thesis:

hence ( ( 1 <= j & j < y1 ) or ( yc < j & j <= n ) ) by A66, XXREAL_0:2; :: thesis:

end;

now

per cases ;

suppose y1 < yc ; :: thesis:

end;

suppose y1 >= yc ; :: thesis:

end;

hence f4 . j = f3 . j by A76, A77, A161, SCPISORT:def 1
.= (IExec (I,Q,t)) . (intpos (m + j)) by A63, A165, SCMPDS_4:8
.= t . (intpos (m + j)) by A12, A37, A38, A39, A40, A41, A42, A159, A160 ;
:: thesis:

end;

thus for j being Element of NAT st y1 >= yn & 1 <= j & j <= n holds
f4 . j = t . (intpos (m + j)) by A46, XREAL_1:47; :: thesis:

hereby :: thesis:

let j be Element of NAT ; :: thesis:
assume that
A167: 1 <= j and
A168: j < (2 * k1) + 1 ; :: thesis:
(2 * k1) + 1 < (2 * (k1 + 1)) + 1 by A86, XREAL_1:6;
then A169: j < (2 * (k1 + 1)) + 1 by A168, 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 A105, A146, A167, A168
.= (Comput ((Q +* (stop (while>0 (a,i,I)))),t,((LifeSpan ((Q +* (stop I)),t)) + 2))) . (intpos ((m + n) + j)) by A82, A167, A169
.= (IExec (I,Q,t)) . (intpos ((m + n) + j)) by A63, SCMPDS_4:8
.= t . (intpos ((m + n) + j)) by A12, A37, A38, A39, A40, A41, A42, A167, A168 ; :: thesis:

end;

thus (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 by A38, A64, A83, A106, A146; :: thesis:
thus (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c by A107, A146; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A170: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A13, A35);
ex k being Element of 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 Element of NAT st 1 < n & ( ( 1 <= j & j < 1 ) or ( n < j & j <= n ) ) holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Element of NAT st 1 >= n & 1 <= j & j <= n holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Element of 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 ;

suppose n - 1 <= 0 ; :: thesis:

hence ex k being Element of 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 Element of NAT st 1 < n & ( ( 1 <= j & j < 1 ) or ( n < j & j <= n ) ) holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Element of NAT st 1 >= n & 1 <= j & j <= n holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Element of 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; :: thesis:

end;

suppose n - 1 > 0 ; :: thesis:

then reconsider nn = n - 1 as Element of NAT by INT_1:3;
S₁[nn] by A170;
hence ex k being Element of 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 Element of NAT st 1 < n & ( ( 1 <= j & j < 1 ) or ( n < j & j <= n ) ) holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Element of NAT st 1 >= n & 1 <= j & j <= n holds
f2 . j = s . (intpos (m + j)) ) & ( for j being Element of 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; :: thesis:

end;

then consider k being Element of NAT , f2 being FinSequence of INT such that
A171: Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) = Comput ((P +* (stop (while>0 (a,i,I)))),s,k) and
A172: f2 is_FinSequence_on Comput ((P +* (stop (while>0 (a,i,I)))),s,k),m and
A173: len f2 = n and
A174: f,f2 are_fiberwise_equipotent and
A175: f2 is_non_decreasing_on 1,n and
A176: (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)) . (DataLoc (c,i)) = (s . (DataLoc (c,i))) - 2 and
A177: (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)));
A179: IC (Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))) = 0 by MEMSTR_0:def 8;
set i1 = (a,i) <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
A180: card (while>0 (a,i,I)) = (card I) + 2 by SCMPDS_8:17;
then A181: (card I) + 2 in dom (stop (while>0 (a,i,I))) by COMPOS_1:64;
A182: 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 A183: ((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 A181, GRFUNC_1:2
.= halt SCMPDS by A180, COMPOS_1:64 ;
A184: while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by Lm2;
A185: 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
.= Following (((P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I)))),(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)))) by EXTPRO_1:2
.= Exec (((a,i) <=0_goto ((card I) + 2)),(Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k)))) by A184, 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)) = (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)) . (IC )
.= ICplusConst ((Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))),((card I) + 2)) by A7, A171, A176, A177, A185, SCMPDS_2:56
.= 0 + ((card I) + 2) by A179, SCMPDS_6:12 ;
then A187: 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 A183, PBOOLE:143;
(P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I))) = P +* (stop (while>0 (a,i,I))) by FUNCT_4:93;
then A188: 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 A171, EXTPRO_1:4;
A189: P +* (stop (while>0 (a,i,I))) = (P +* (stop (while>0 (a,i,I)))) +* (stop (while>0 (a,i,I))) by FUNCT_4:93;
then A190: P +* (stop (while>0 (a,i,I))) halts_on s by A187, A188, EXTPRO_1:29;
hence while>0 (a,i,I) is_halting_on s,P by I, SCMPDS_6:def 3; :: thesis:
A191: 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 A187, A188, A190, A189, EXTPRO_1:def 9;

now

let i be Nat; :: thesis:
reconsider a = i as Element of NAT by ORDINAL1:def 12;
set xi = intpos (m + a);
assume A194: i in dom g ; :: thesis:
then A195: 1 <= i by A182, FINSEQ_1:1;
A196: i <= n by A182, A194, 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 A191, 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, A195, A196, SCPISORT:def 1
.= (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))
.= (Initialize (Comput ((P +* (stop (while>0 (a,i,I)))),s,k))) . (intpos (m + a)) by A185, SCMPDS_2:56
.= f2 . i by A171, A172, A173, A195, A196, SCPISORT:def 1 ;
:: thesis:

end;

hence ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) by A4, A173, A174, A175, FINSEQ_2:9; :: thesis: