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 ; :: 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 Nat; :: thesis:
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 ; :: 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₁[ 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 ; :: 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 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 ) ) ; :: 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 Nat; :: thesis:
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 ; :: thesis:
A24: I is_halting_on t,Q by A12, A15, A16, A17, A18, A19, A20;
take k = (LifeSpan ((Q +* (stop I)),t)) + 2; :: thesis:
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 ; :: thesis:
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; :: thesis:

now :: thesis:

let i be Nat; :: thesis:
assume that
A29: 1 <= i and
A30: i <= len f2 ; :: thesis:
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 ; :: thesis:

end;

hence f2 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,k),m ; :: thesis:
thus len f2 = n by A27; :: thesis:
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; :: thesis:
thus f2 is_non_decreasing_on y1,yn by A21, FINSEQ_6:165, XREAL_1:50; :: thesis:
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; :: thesis:

hereby :: thesis:

let j be Nat; :: thesis:
assume that
A31: y1 >= yn and
A32: 1 <= j and
A33: j <= n ; :: thesis:
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 ; :: thesis:

end;

hereby :: thesis:

let j be Nat; :: thesis:
assume that
A34: 1 <= j and
A35: 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 A26, SCMPDS_4:8
.= t . (intpos ((m + n) + j)) by A12, A15, A16, A17, A18, A19, A20, A34, A35 ; :: thesis:

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; :: thesis:
(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; :: thesis:

end;

A36: now :: thesis:

let k be Nat; :: thesis:
assume A37: S₁[k] ; :: thesis:
S₁[k + 1]

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 Nat; :: thesis:
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 ; :: thesis:

per cases ;

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

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; :: thesis:

end;

suppose A48: 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)));
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; :: 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 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; :: thesis:

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; :: 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 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; :: thesis:

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; :: 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 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; :: thesis:

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; :: 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 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; :: 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)));
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;

A104: now :: thesis:

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 A71, A96, A66; :: 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 A97, A66, A103; :: thesis:

end;

A105: now :: thesis:

let i be Nat; :: thesis:
assume that
A106: 1 <= i and
A107: i <= ym ; :: thesis:
A108: i <= n by A103, A107, XXREAL_0:2;
A109: i < ym + 1 by A71, A107, XXREAL_0:2;

now :: thesis:

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 A96, A106, A109; :: 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 A97, A106, A108; :: thesis:

end;

hence f3 . i = f2 . i by A52, A53, A106, A108; :: thesis:

end;

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; :: 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 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; :: thesis:

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; :: 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 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; :: thesis:

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; :: 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 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; :: thesis:

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; :: 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 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; :: thesis:

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 :: thesis:

let i be Nat; :: thesis:
assume that
A140: yc < i and
A141: i <= len f4 ; :: thesis:
A142: 1 + 0 <= i by A140, INT_1:7;

now :: thesis:

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 A131, A134, A140, A141; :: thesis:

end;

suppose y1 >= yc ; :: thesis:

end;

hence f4 . i = f3 . i by A92, A93, A131, A141, A142; :: thesis:

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 :: thesis:

let i be Nat; :: thesis:
assume that
A145: yn < i and
A146: i <= len f3 ; :: thesis:
A147: 1 + 0 <= i by A145, INT_1:7;

now :: thesis:

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 A93, A96, A145, A146; :: 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 A93, A97, A146, A147; :: thesis:

end;

hence f3 . i = f2 . i by A52, A53, A93, A146, A147; :: thesis:

end;

A148: now :: thesis:

let i be Nat; :: thesis:
assume that
A149: ym < i and
A150: i <= yn ; :: thesis:
consider 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; :: thesis:

end;

A157: yn > y1 by A48, XREAL_1:47;

A158: now :: thesis:

let i be Nat; :: thesis:
assume that
A159: 1 <= i and
A160: i <= y0 ; :: thesis:
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 :: thesis:

per cases ;

suppose y1 < yc ; :: thesis:

end;

suppose y1 >= yc ; :: thesis:

end;

hence f4 . i = f3 . i by A92, A93, A159, A162; :: thesis:

end;

A163: y0 <= yc by A55, XREAL_1:9;

A164: now :: thesis:

let i be Nat; :: thesis:
assume that
A165: y1 <= i and
A166: i < ym ; :: thesis:
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;

now :: thesis:

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 A96, A171, A173; :: 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 A97, A171, A172; :: thesis:

end;

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; :: 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:
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; :: thesis:
thus f4 is_FinSequence_on Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm),m by A130, A176; :: thesis:
thus len f4 = n by A131; :: thesis:

now :: thesis:

let i be Nat; :: thesis:
assume that
A177: 1 <= i and
A178: 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 A53, A177, A178
.= (IExec (I,Q,t)) . (intpos (m + i)) by A64, SCMPDS_4:8 ; :: thesis:

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; :: thesis:

A179: now :: thesis:

let j be Nat; :: thesis:
assume that
A180: ym + 1 <= j and
A181: j <= yn ; :: thesis:
A182: 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 :: thesis:

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 A134, A183, A184; :: thesis:

end;

suppose y1 >= yc ; :: thesis:

end;

hence f4 . j = f3 . j by A92, A93, A183, A182; :: thesis:

end;

now :: thesis:

let i, j be Nat; :: thesis:
assume that
A185: ym + 1 <= i and
A186: i <= j and
A187: j <= yn ; :: thesis:
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; :: thesis:

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; :: thesis:
thus for j being 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 Nat; :: thesis:
assume that
A189: y1 < yn and
A190: ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) ; :: thesis:
A191: ( 1 <= j & j <= n )

proof

per cases by A190;

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

then j < yn by A189, XXREAL_0:2;
hence ( 1 <= j & j <= n ) by A42, A48, A192, XREAL_1:47, XXREAL_0:2; :: thesis:

end;

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

then y1 < j by A189, XXREAL_0:2;
hence ( 1 <= j & j <= n ) by A42, A48, A193, XREAL_1:47, XXREAL_0:2; :: thesis:

end;

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

proof

per cases by A190;

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

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

end;

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

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

end;

A195: now :: thesis:

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 A96, A194; :: 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 A97, A191; :: thesis:

end;

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

proof

per cases by A190;

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 A67, XXREAL_0:2; :: thesis:

end;

now :: thesis:

per cases ;

suppose y1 < yc ; :: thesis:

end;

suppose y1 >= yc ; :: thesis:

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 ;
:: thesis:

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; :: thesis:

hereby :: thesis:

let j be Nat; :: thesis:
assume that
A197: 1 <= j and
A198: j < (2 * k1) + 1 ; :: thesis:
(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 ; :: thesis:

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; :: thesis:
thus (Comput ((Q +* (stop (while>0 (a,i,I)))),t,mm)) . a = c by A138, A176; :: thesis:

end;

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

end;

A200: for k being Nat holds S₁[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 ;

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

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; :: thesis:

end;

suppose n - 1 > 0 ; :: thesis:

then reconsider nn = n - 1 as Element of NAT by INT_1:3;
S₁[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; :: thesis:

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; :: thesis:
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 :: thesis:

let i be Nat; :: thesis:
reconsider a = i as Nat ;
set xi = intpos (m + a);
assume A219: i in dom g ; :: thesis:
then 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 ;
:: thesis:

end;

hence ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) by A4, A203, A204, A205, FINSEQ_2:9; :: thesis: