let P be Instruction-Sequence of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS
for f, g being FinSequence of INT
for p0, n being Nat st s . GBP = 0 & s . (intpos 2) = n - 1 & s . (intpos 3) = p0 + 1 & s . (intpos 1) = 0 & p0 >= 6 & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),P,s),p0 & len f = n & len g = n holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
set a = GBP ;
let s be 0 -started State of SCMPDS; :: thesis: for f, g being FinSequence of INT
for p0, n being Nat st s . GBP = 0 & s . (intpos 2) = n - 1 & s . (intpos 3) = p0 + 1 & s . (intpos 1) = 0 & p0 >= 6 & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),P,s),p0 & len f = n & len g = n holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
let f, g be FinSequence of INT ; :: thesis: for p0, n being Nat st s . GBP = 0 & s . (intpos 2) = n - 1 & s . (intpos 3) = p0 + 1 & s . (intpos 1) = 0 & p0 >= 6 & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),P,s),p0 & len f = n & len g = n holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
let p0, n be Nat; :: thesis: ( s . GBP = 0 & s . (intpos 2) = n - 1 & s . (intpos 3) = p0 + 1 & s . (intpos 1) = 0 & p0 >= 6 & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),P,s),p0 & len f = n & len g = n implies ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) )
assume that
A1: s . GBP = 0 and
A2: s . (intpos 2) = n - 1 and
A3: s . (intpos 3) = p0 + 1 and
A4: s . (intpos 1) = 0 and
A5: p0 >= 6 and
A6: ( f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),P,s),p0 ) and
A7: len f = n and
A8: len g = n ; :: thesis: ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )

per cases ( n = 0 or n <> 0 ) ;

suppose A9: n = 0 ; :: thesis: ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )

then g = {} by A8;
hence f,g are_fiberwise_equipotent by A7, A9; :: thesis: g is_non_decreasing_on 1,n
thus g is_non_decreasing_on 1,n by A9, FINSEQ_6:165; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )

then n >= 1 + 0 by INT_1:7;
then n - 1 >= 0 by XREAL_1:19;
then reconsider n1 = n - 1 as Element of NAT by INT_1:3;
defpred S₁[ Nat] means for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for m being Nat st t . GBP = 0 & (t . (intpos 2)) + (t . (intpos 1)) = n - 1 & t . (intpos 2) = $1 & m = n - (t . (intpos 2)) & p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 & f1 is_FinSequence_on t,p0 & f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 & f1 is_non_decreasing_on 1,m & len f1 = n & len f2 = n holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n );
A10: ( (s . (intpos 2)) + (s . (intpos 1)) = (n - 1) + 0 & 1 = n - (s . (intpos 2)) ) by A2, A4;

A11: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A12: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for t being 0 -started State of SCMPDS
for f1, f2 being FinSequence of INT
for m being Nat
for Q being Instruction-Sequence of SCMPDS st t . GBP = 0 & (t . (intpos 2)) + (t . (intpos 1)) = n - 1 & t . (intpos 2) = k + 1 & m = n - (t . (intpos 2)) & p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 & f1 is_FinSequence_on t,p0 & f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 & f1 is_non_decreasing_on 1,m & len f1 = n & len f2 = n holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n )

let t be 0 -started State of SCMPDS; :: thesis: for f1, f2 being FinSequence of INT
for m being Nat
for Q being Instruction-Sequence of SCMPDS st t . GBP = 0 & (t . (intpos 2)) + (t . (intpos 1)) = n - 1 & t . (intpos 2) = k + 1 & m = n - (t . (intpos 2)) & p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 & f1 is_FinSequence_on t,p0 & f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 & f1 is_non_decreasing_on 1,m & len f1 = n & len f2 = n holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n )
let f1, f2 be FinSequence of INT ; :: thesis: for m being Nat
for Q being Instruction-Sequence of SCMPDS st t . GBP = 0 & (t . (intpos 2)) + (t . (intpos 1)) = n - 1 & t . (intpos 2) = k + 1 & m = n - (t . (intpos 2)) & p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 & f1 is_FinSequence_on t,p0 & f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 & f1 is_non_decreasing_on 1,m & len f1 = n & len f2 = n holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n )
let m be Nat; :: thesis: for Q being Instruction-Sequence of SCMPDS st t . GBP = 0 & (t . (intpos 2)) + (t . (intpos 1)) = n - 1 & t . (intpos 2) = k + 1 & m = n - (t . (intpos 2)) & p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 & f1 is_FinSequence_on t,p0 & f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 & f1 is_non_decreasing_on 1,m & len f1 = n & len f2 = n holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n )
let Q be Instruction-Sequence of SCMPDS; :: thesis: ( t . GBP = 0 & (t . (intpos 2)) + (t . (intpos 1)) = n - 1 & t . (intpos 2) = k + 1 & m = n - (t . (intpos 2)) & p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 & f1 is_FinSequence_on t,p0 & f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 & f1 is_non_decreasing_on 1,m & len f1 = n & len f2 = n implies ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n ) )
assume that
A13: t . GBP = 0 and
A14: (t . (intpos 2)) + (t . (intpos 1)) = n - 1 and
A15: t . (intpos 2) = k + 1 and
A16: m = n - (t . (intpos 2)) and
A17: p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 and
A18: f1 is_FinSequence_on t,p0 and
A19: f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 and
A20: ( f1 is_non_decreasing_on 1,m & len f1 = n ) and
A21: len f2 = n ; :: thesis: ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n )
set t1 = IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t);
set Bt = IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t);
set Q1 = Q;
A22: (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . GBP = (Initialize (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t))) . GBP by SCMPDS_5:15;
A23: (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 4) = (Initialize (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t))) . (intpos 4) by SCMPDS_5:15;
A24: (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 6) = (Initialize (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t))) . (intpos 6) by SCMPDS_5:15;
A25: (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 4) = (t . (intpos 3)) + 1 by A13, Lm10;
p0 + ((t . (intpos 1)) + 1) = t . (intpos 3) by A17;
then t . (intpos 3) >= 6 + ((t . (intpos 1)) + 1) by A5, XREAL_1:6;
then A26: t . (intpos 3) >= (6 + 1) + (t . (intpos 1)) ;
then A27: (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . GBP = 0 by A13, Lm11;
A28: (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos 2) = (t . (intpos 2)) - 1 by A13, A26, Lm11;
then A29: n - ((IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos 2)) = m + 1 by A16;
A30: (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos 1) = (t . (intpos 1)) + 1 by A13, A26, Lm11;
then A31: ((IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos 2)) + ((IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos 1)) = n - 1 by A14, A28;
(IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos 3) = (t . (intpos 3)) + 1 by A13, A26, Lm11;
then A32: (((IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos 3)) - ((IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos 1))) - 1 = p0 by A17, A30;
A33: (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 6) = (t . (intpos 1)) + 1 by A13, Lm10;
then A34: p0 = (((IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 4)) - ((IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 6))) - 1 by A17, A25;

now :: thesis: for i being Nat st 1 <= i & i <= len f2 holds
f2 . i = (IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,(Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t))))) . (intpos (p0 + i))

let i be Nat; :: thesis: ( 1 <= i & i <= len f2 implies f2 . i = (IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,(Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t))))) . (intpos (p0 + i)) )
assume ( 1 <= i & i <= len f2 ) ; :: thesis: f2 . i = (IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,(Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t))))) . (intpos (p0 + i))
hence f2 . i = (IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t)) . (intpos (p0 + i)) by A19
.= (IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,(Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t))))) . (intpos (p0 + i)) by A13, A15, A26, Lm13 ;
:: thesis: verum

end;

then A35: f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,(Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)))),p0 ;

A36: now :: thesis: for i being Nat st 1 <= i & i <= len f1 holds
f1 . i = (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos (p0 + i))

A37: p0 + 1 >= 6 + 1 by A5, XREAL_1:6;
let i be Nat; :: thesis: ( 1 <= i & i <= len f1 implies f1 . i = (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos (p0 + i)) )
assume that
A38: 1 <= i and
A39: i <= len f1 ; :: thesis: f1 . i = (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos (p0 + i))
p0 + 1 <= p0 + i by A38, XREAL_1:6;
then A40: p0 + i >= 7 by A37, XXREAL_0:2;
thus f1 . i = t . (intpos (p0 + i)) by A18, A38, A39
.= (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos (p0 + i)) by A13, A40, Lm10 ; :: thesis: verum

end;

(IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 4) = p0 + (((IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 6)) + 1) by A17, A25, A33;
then (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 4) >= 6 + (((IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 6)) + 1) by A5, XREAL_1:6;
then A41: (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 4) >= (6 + 1) + ((IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos 6)) ;
m + (k + 1) = n by A15, A16;
then A42: n > 0 + m by XREAL_1:6;
consider h being FinSequence of INT such that
A43: len h = n and
A44: for i being Nat st 1 <= i & i <= len h holds
h . i = (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t))))) . (intpos (p0 + i)) by Th1;
A45: h is_FinSequence_on IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)))),p0 by A44;

A46: now :: thesis: for i being Nat st 1 <= i & i <= len h holds
h . i = (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos (p0 + i))

A47: p0 + 1 >= 6 + 1 by A5, XREAL_1:6;
let i be Nat; :: thesis: ( 1 <= i & i <= len h implies h . i = (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos (p0 + i)) )
assume that
A48: 1 <= i and
A49: i <= len h ; :: thesis: h . i = (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos (p0 + i))
p0 + 1 <= p0 + i by A48, XREAL_1:6;
then p0 + i >= 7 by A47, XXREAL_0:2;
then A50: p0 + i > 2 by XXREAL_0:2;
thus h . i = (IExec ((while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0))))))),Q,(Initialize (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t))))) . (intpos (p0 + i)) by A44, A48, A49
.= (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos (p0 + i)) by A13, A26, A50, Lm11 ; :: thesis: verum

end;

A51: f1 is_FinSequence_on Initialize (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)),p0

proof

let i be Nat; :: according to SCPISORT:def 1 :: thesis: ( 1 <= i & i <= len f1 implies f1 . i = (Initialize (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t))) . (intpos (p0 + i)) )
assume ( 1 <= i & i <= len f1 ) ; :: thesis: f1 . i = (Initialize (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t))) . (intpos (p0 + i))
then f1 . i = (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . (intpos (p0 + i)) by A36;
hence f1 . i = (Initialize (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t))) . (intpos (p0 + i)) by SCMPDS_5:15; :: thesis: verum

end;

A52: (IExec (((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))),Q,t)) . GBP = 0 by A13, Lm10;
then A53: f1,h are_fiberwise_equipotent by A14, A16, A17, A20, A25, A43, A34, A41, A45, A42, Th16, A23, A24, A22, A51;
A54: h is_non_decreasing_on 1,m + 1 by A14, A16, A17, A20, A25, A43, A34, A41, A45, A42, Th16, A23, A24, A22, A51, A52;
A55: (Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t))) . GBP = (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . GBP by SCMPDS_5:15;
A56: (Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t))) . (intpos 1) = (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos 1) by SCMPDS_5:15;
A57: (Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t))) . (intpos 2) = (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos 2) by SCMPDS_5:15;
A58: (Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t))) . (intpos 3) = (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos 3) by SCMPDS_5:15;
A59: h is_FinSequence_on Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)),p0

proof

let i be Nat; :: according to SCPISORT:def 1 :: thesis: ( 1 <= i & i <= len h implies h . i = (Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t))) . (intpos (p0 + i)) )
assume A60: ( 1 <= i & i <= len h ) ; :: thesis: h . i = (Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t))) . (intpos (p0 + i))
thus h . i = (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t)) . (intpos (p0 + i)) by A60, A46
.= (Initialize (IExec (((((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))) ';' (AddTo (GBP,2,(- 1)))),Q,t))) . (intpos (p0 + i)) by SCMPDS_5:15 ; :: thesis: verum

end;

then h,f2 are_fiberwise_equipotent by A12, A15, A16, A21, A43, A27, A31, A29, A32, A35, A54, A55, A56, A57, A58;
hence f1,f2 are_fiberwise_equipotent by A53, CLASSES1:76; :: thesis: f2 is_non_decreasing_on 1,n
thus f2 is_non_decreasing_on 1,n by A12, A15, A16, A21, A43, A54, A27, A31, A29, A32, A35, A55, A56, A57, A58, A59; :: thesis: verum

end;

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

end;

A61: S₁[ 0 ]

proof

let t be 0 -started State of SCMPDS; :: thesis: for Q being Instruction-Sequence of SCMPDS
for f1, f2 being FinSequence of INT
for m being Nat st t . GBP = 0 & (t . (intpos 2)) + (t . (intpos 1)) = n - 1 & t . (intpos 2) = 0 & m = n - (t . (intpos 2)) & p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 & f1 is_FinSequence_on t,p0 & f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 & f1 is_non_decreasing_on 1,m & len f1 = n & len f2 = n holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n )
let Q be Instruction-Sequence of SCMPDS; :: thesis: for f1, f2 being FinSequence of INT
for m being Nat st t . GBP = 0 & (t . (intpos 2)) + (t . (intpos 1)) = n - 1 & t . (intpos 2) = 0 & m = n - (t . (intpos 2)) & p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 & f1 is_FinSequence_on t,p0 & f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 & f1 is_non_decreasing_on 1,m & len f1 = n & len f2 = n holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n )
let f1, f2 be FinSequence of INT ; :: thesis: for m being Nat st t . GBP = 0 & (t . (intpos 2)) + (t . (intpos 1)) = n - 1 & t . (intpos 2) = 0 & m = n - (t . (intpos 2)) & p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 & f1 is_FinSequence_on t,p0 & f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 & f1 is_non_decreasing_on 1,m & len f1 = n & len f2 = n holds
( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n )
let m be Nat; :: thesis: ( t . GBP = 0 & (t . (intpos 2)) + (t . (intpos 1)) = n - 1 & t . (intpos 2) = 0 & m = n - (t . (intpos 2)) & p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 & f1 is_FinSequence_on t,p0 & f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 & f1 is_non_decreasing_on 1,m & len f1 = n & len f2 = n implies ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n ) )
A62: Initialize t = t by MEMSTR_0:44;
assume that
A63: t . GBP = 0 and
(t . (intpos 2)) + (t . (intpos 1)) = n - 1 and
A64: t . (intpos 2) = 0 and
A65: m = n - (t . (intpos 2)) and
p0 = ((t . (intpos 3)) - (t . (intpos 1))) - 1 and
A66: f1 is_FinSequence_on t,p0 and
A67: f2 is_FinSequence_on IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,t),p0 and
A68: f1 is_non_decreasing_on 1,m and
A69: ( len f1 = n & len f2 = n ) ; :: thesis: ( f1,f2 are_fiberwise_equipotent & f2 is_non_decreasing_on 1,n )
A70: t . (DataLoc ((t . GBP),2)) = 0 by A63, A64, SCMP_GCD:1;

A71: now :: thesis: for i being Nat st 1 <= i & i <= len f2 holds
f2 . i = f1 . i

let i be Nat; :: thesis: ( 1 <= i & i <= len f2 implies f2 . i = f1 . i )
assume A72: ( 1 <= i & i <= len f2 ) ; :: thesis: f2 . i = f1 . i
thus f2 . i = (IExec ((for-down (GBP,2,1,(((((AddTo (GBP,3,1)) ';' ((GBP,4) := (GBP,3))) ';' (AddTo (GBP,1,1))) ';' ((GBP,6) := (GBP,1))) ';' (while>0 (GBP,6,((((GBP,5) := ((intpos 4),(- 1))) ';' (SubFrom (GBP,5,(intpos 4),0))) ';' (if>0 (GBP,5,((((((GBP,5) := ((intpos 4),(- 1))) ';' (((intpos 4),(- 1)) := ((intpos 4),0))) ';' (((intpos 4),0) := (GBP,5))) ';' (AddTo (GBP,4,(- 1)))) ';' (AddTo (GBP,6,(- 1)))),(Load ((GBP,6) := 0)))))))))),Q,(Initialize t))) . (intpos (p0 + i)) by A67, A72, A62
.= t . (intpos (p0 + i)) by A70, SCMPDS_7:47
.= f1 . i by A66, A69, A72 ; :: thesis: verum

end;

hence f1,f2 are_fiberwise_equipotent by A69, FINSEQ_1:14; :: thesis: f2 is_non_decreasing_on 1,n
thus f2 is_non_decreasing_on 1,n by A64, A65, A68, A69, A71, FINSEQ_1:14; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A61, A11);
then A73: S₁[n1] ;
( p0 = ((s . (intpos 3)) - (s . (intpos 1))) - 1 & f is_non_decreasing_on 1,1 ) by A3, A4, FINSEQ_6:165;
hence ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) by A1, A6, A7, A8, A10, A73; :: thesis: verum

end;

end;