let s be 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:
set b = DataLoc (c,i);
assume that
A1: card I > 0 and
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));
set iWH = Initialize (stop (while>0 (a,i,I)));
assume A5: f is_FinSequence_on s,m ; :: thesis:
defpred S₁[ Element of NAT ] means for t being State 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 ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),k))) +* (stop (while>0 (a,i,I))) = Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),k) & f2 is_FinSequence_on Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),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 ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),k)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),k)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),k)) . a = c );
assume A6: g is_FinSequence_on IExec ((while>0 (a,i,I)),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 State of SCMPDS
for f1, f2 being FinSequence of INT
for k1, k2, y1, yn being Element of NAT st t . a = c & (2 * k1) + 1 = t . (DataLoc (c,i)) & k2 = ((m + n) + (2 * k1)) + 1 & m + y1 = t . (intpos k2) & m + yn = t . (intpos (k2 + 1)) & ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) holds
( I is_closed_on t & I is_halting_on t & (IExec (I,t)) . a = t . a & ( for j being Element of NAT st 1 <= j & j < (2 * k1) + 1 holds
(IExec (I,t)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & ( y1 >= yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) - 1 & ( for j being Element of NAT st 1 <= j & j <= n holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) ) ) & ( y1 < yn implies ( (IExec (I,t)) . (DataLoc (c,i)) = (2 * k1) + 3 & ( for j being Element of NAT st ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) holds
(IExec (I,t)) . (intpos (m + j)) = t . (intpos (m + j)) ) & ex ym being Element of NAT st
( y1 <= ym & ym <= yn & m + y1 = (IExec (I,t)) . (intpos k2) & (m + ym) - 1 = (IExec (I,t)) . (intpos (k2 + 1)) & (m + ym) + 1 = (IExec (I,t)) . (intpos (k2 + 2)) & m + yn = (IExec (I,t)) . (intpos (k2 + 3)) & ( for j being Element of NAT st y1 <= j & j < ym holds
(IExec (I,t)) . (intpos (m + j)) <= (IExec (I,t)) . (intpos (m + ym)) ) & ( for j being Element of NAT st ym < j & j <= yn holds
(IExec (I,t)) . (intpos (m + j)) >= (IExec (I,t)) . (intpos (m + ym)) ) ) ) ) & ( f1 is_FinSequence_on t,m & f2 is_FinSequence_on IExec (I,t),m & len f1 = n & len f2 = n implies f1,f2 are_fiberwise_equipotent ) ) ; :: thesis:
A13: S₁[ 0 ]

proof

now

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

end;

hence f2 is_FinSequence_on Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),k),m by SCPISORT:def 1; :: thesis:
thus len f2 = n by A26; :: thesis:
f2 is_FinSequence_on IExec (I,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, SCPISORT:1, XREAL_1:52; :: 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:52; :: 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,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 ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),k)) . (intpos ((m + n) + j)) = (IExec (I,t)) . (intpos ((m + n) + j)) by A25, SCMPDS_4:23
.= t . (intpos ((m + n) + j)) by A12, A14, A15, A16, A17, A18, A19, A33, A34 ; :: thesis:

end;

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

end;

A35: now

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

now

let t be State of SCMPDS; :: thesis:
let f1 be FinSequence of INT ; :: thesis:
let k1, k2, y1, ym, yn be Element of NAT ; :: thesis:
assume that
A37: t . a = c and
A38: (2 * k1) + 1 = t . (DataLoc (c,i)) and
A39: k2 = ((m + n) + (2 * k1)) + 1 and
A40: ( ( 1 <= y1 & yn <= n ) or y1 >= yn ) and
A41: m + y1 = t . (intpos k2) and
A42: m + yn = t . (intpos (k2 + 1)) and
A43: yn - y1 <= k + 1 and
A44: f1 is_FinSequence_on t,m and
A45: len f1 = n ; :: thesis:

per cases ;

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

hence ex kk being Element of NAT ex f2 being FinSequence of INT st
( (Initialize (Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),kk))) +* (stop (while>0 (a,i,I))) = Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),kk) & f2 is_FinSequence_on Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),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 ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),kk)) . (intpos ((m + n) + j)) = t . (intpos ((m + n) + j)) ) & (Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),kk)) . (DataLoc (c,i)) = (t . (DataLoc (c,i))) - 2 & (Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),kk)) . a = c ) by A13, A37, A38, A39, A40, A41, A42, A44, A45; :: thesis:

end;

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

A88: now

per cases ;

suppose ym + 1 < yn ; :: thesis:

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

end;

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

end;

A89: now

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

now

per cases ;

suppose ym + 1 < yn ; :: thesis:

hence f3 . i = (Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) + 2))) . (intpos (m + i)) by A80, A90, A93; :: thesis:

end;

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

end;

hence f3 . i = f2 . i by A50, A51, A90, A92; :: thesis:

end;

A107: now

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

now

per cases ;

suppose y1 < yc ; :: thesis:

end;

suppose y1 >= yc ; :: thesis:

end;

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

end;

then f4 . ym = f3 . ym by A99, A87, XREAL_1:148;
then A111: f4 . ym = (IExec (I,t)) . (intpos (m + ym)) by A63, A88, SCMPDS_4:23;

A112: now

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

now

per cases ;

suppose ym + 1 < yn ; :: thesis:

end;

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

end;

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

end;

A116: now

let i be Element of NAT ; :: thesis:
assume that
A117: ym < i and
A118: i <= yn ; :: thesis:
consider j being Element of NAT such that
A119: ym < j and
A120: j <= yn and
A121: f3 . i = f2 . j by A40, A46, A55, A77, A78, A89, A112, A117, A118, RFINSEQ:45, XREAL_1:49;
A122: yc < i by A117, XREAL_1:148, XXREAL_0:2;
A123: 1 <= j by A65, A119, XXREAL_0:2;
A124: j <= len f2 by A40, A46, A50, A120, XREAL_1:49, XXREAL_0:2;
i <= len f4 by A40, A46, A99, A118, XREAL_1:49, XXREAL_0:2;
then f4 . i = f2 . j by A107, A122, A121
.= (Comput ((ProgramPart ((Initialize t) +* (stop (while>0 (a,i,I))))),((Initialize t) +* (stop (while>0 (a,i,I)))),((LifeSpan ((ProgramPart ((Initialize t) +* (stop I))),((Initialize t) +* (stop I)))) + 2))) . (intpos (m + j)) by A51, A123, A124
.= (IExec (I,t)) . (intpos (m + j)) by A63, SCMPDS_4:23 ;
hence f4 . ym <= f4 . i by A61, A111, A119, A120; :: thesis:

end;

A125: yn > y1 by A46, XREAL_1:49;

A126: now

let i be Element of NAT ; :: thesis:
assume that
A127: 1 <= i and
A128: i <= y0 ; :: thesis:
i - 1 < y1 - 1 by A128, XREAL_1:148, XXREAL_0:2;
then A129: i < y1 by XREAL_1:11;
y1 <= n by A40, A125, XXREAL_0:2;
then A130: i <= n by A129, XXREAL_0:2;

now

per cases ;

suppose y1 < yc ; :: thesis:

end;

suppose y1 >= yc ; :: thesis:

end;

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

end;

A131: y0 <= yc by A54, XREAL_1:11;

A132: now

let i be Element of NAT ; :: thesis:
assume that
A133: y1 <= i and
A134: i < ym ; :: thesis:
i + 1 <= ym by A134, INT_1:20;
then A135: i <= yc by XREAL_1:21;
y0 < i by A133, XREAL_1:148, XXREAL_0:2;
then consider j being Element of NAT such that
A136: y0 < j and
A137: j <= yc and
A138: f4 . i = f3 . j by A67, A99, A100, A131, A126, A107, A135, RFINSEQ:45;
A139: 1 + 0 <= j by A136, INT_1:20;
A140: j <= n by A67, A137, XXREAL_0:2;
A141: j < ym + 1 by A95, A137, XXREAL_0:2;

now

per cases ;

suppose ym + 1 < yn ; :: thesis:

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

end;

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

end;

then A142: f4 . i = (IExec (I,t)) . (intpos (m + j)) by A63, A138, SCMPDS_4:23;
A143: j < ym by A137, XREAL_1:148, XXREAL_0:2;
(y1 - 1) + 1 <= j by A136, INT_1:20;
hence f4 . i <= f4 . ym by A60, A111, A143, A142; :: thesis:

end;

now

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

end;

then f2 is_FinSequence_on IExec (I,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:84;
hence f1,f4 are_fiberwise_equipotent by A100, CLASSES1:84; :: thesis:

A147: now

let j be Element of NAT ; :: thesis:
assume that
A148: ym + 1 <= j and
A149: j <= yn ; :: thesis:
A150: 1 <= j by A72, A148, XXREAL_0:2;
A151: j <= n by A40, A46, A149, XREAL_1:49, XXREAL_0:2;
A152: yc < j by A95, A148, XXREAL_0:2;

now

per cases ;

suppose y1 < yc ; :: thesis:

end;

suppose y1 >= yc ; :: thesis:

end;

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

end;

now

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

end;

then f4 is_non_decreasing_on ym + 1,yn by GRAPH_2:def 13;
hence f4 is_non_decreasing_on y1,yn by A101, A132, A116, 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
A157: y1 < yn and
A158: ( ( 1 <= j & j < y1 ) or ( yn < j & j <= n ) ) ; :: thesis:
A159: ( 1 <= j & j <= n )

proof

per cases by A158;

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

then j < yn by A157, XXREAL_0:2;
hence ( 1 <= j & j <= n ) by A40, A46, A160, XREAL_1:49, XXREAL_0:2; :: thesis:

end;

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

then y1 < j by A157, XXREAL_0:2;
hence ( 1 <= j & j <= n ) by A40, A46, A161, XREAL_1:49, XXREAL_0:2; :: thesis:

end;

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

proof

per cases by A158;

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;

A163: now

per cases ;

suppose ym + 1 < yn ; :: thesis:

end;

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

end;

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

proof

per cases by A158;

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, A159, SCPISORT:def 1
.= (IExec (I,t)) . (intpos (m + j)) by A63, A163, SCMPDS_4:23
.= t . (intpos (m + j)) by A12, A37, A38, A39, A40, A41, A42, A157, A158 ;
:: 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:49; :: thesis:

hereby :: thesis:

end;

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

end;

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

end;

A168: 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 ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k))) +* (stop (while>0 (a,i,I))) = Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k) & f2 is_FinSequence_on Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),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 ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k)) . (intpos ((m + n) + j)) = s . (intpos ((m + n) + j)) ) & (Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k)) . (DataLoc (c,i)) = (s . (DataLoc (c,i))) - 2 & (Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),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 ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k))) +* (stop (while>0 (a,i,I))) = Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k) & f2 is_FinSequence_on Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),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 ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k)) . (intpos ((m + n) + j)) = s . (intpos ((m + n) + j)) ) & (Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k)) . (DataLoc (c,i)) = (s . (DataLoc (c,i))) - 2 & (Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),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:16;
S₁[nn] by A168;
hence ex k being Element of NAT ex f2 being FinSequence of INT st
( (Initialize (Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k))) +* (stop (while>0 (a,i,I))) = Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k) & f2 is_FinSequence_on Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),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 ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k)) . (intpos ((m + n) + j)) = s . (intpos ((m + n) + j)) ) & (Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k)) . (DataLoc (c,i)) = (s . (DataLoc (c,i))) - 2 & (Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),k)) . a = c ) by A2, A3, A5, A7, A9, A10, A11; :: thesis:

end;

now

end;

hence ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) by A4, A171, A172, A173, FINSEQ_2:10; :: thesis: