let P be Instruction-Sequence of SCMPDS; for s being 0 -started State of SCMPDS
for f, g being FinSequence of INT
for p0, n being Nat st p0 >= 6 & len f = n & len g = n & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),P,s),p0 holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
set a = GBP ;
let s be 0 -started State of SCMPDS; for f, g being FinSequence of INT
for p0, n being Nat st p0 >= 6 & len f = n & len g = n & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),P,s),p0 holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
let f, g be FinSequence of INT ; for p0, n being Nat st p0 >= 6 & len f = n & len g = n & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),P,s),p0 holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
let p0, n be Nat; ( p0 >= 6 & len f = n & len g = n & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),P,s),p0 implies ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n ) )
assume that
A1:
p0 >= 6
and
A2:
( len f = n & len g = n )
and
A3:
f is_FinSequence_on s,p0
and
A4:
g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),P,s),p0
; ( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
A5:
p0 + 1 >= 6 + 1
by A1, XREAL_1:6;
set i1 = GBP := 0;
set i2 = (GBP,1) := 0;
set i3 = (GBP,2) := (n - 1);
set i4 = (GBP,3) := (p0 + 1);
set I4 = (((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1));
set t1 = IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s);
set t2 = IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s);
set t3 = IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s);
set t4 = Exec ((GBP := 0),s);
A6:
(Exec ((GBP := 0),s)) . GBP = 0
by SCMPDS_2:45;
then A7:
DataLoc (((Exec ((GBP := 0),s)) . GBP),1) = intpos (0 + 1)
by SCMP_GCD:1;
A8: (IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . GBP =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),s)))) . GBP
by SCMPDS_5:42
.=
0
by A6, A7, AMI_3:10, SCMPDS_2:46
;
then A9:
DataLoc (((IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . GBP),2) = intpos (0 + 2)
by SCMP_GCD:1;
A10: (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . GBP =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)))) . GBP
by SCMPDS_5:41
.=
0
by A8, A9, AMI_3:10, SCMPDS_2:46
;
then A11:
DataLoc (((IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . GBP),3) = intpos (0 + 3)
by SCMP_GCD:1;
A12:
now for i being Nat st i > 3 holds
(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . (intpos i) = s . (intpos i)let i be
Nat;
( i > 3 implies (IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . (intpos i) = s . (intpos i) )assume A13:
i > 3
;
(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . (intpos i) = s . (intpos i)then A14:
i > 1
by XXREAL_0:2;
thus (IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . (intpos i) =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),s)))) . (intpos i)
by SCMPDS_5:42
.=
(Exec ((GBP := 0),s)) . (intpos i)
by A7, A14, AMI_3:10, SCMPDS_2:46
.=
s . (intpos i)
by A13, AMI_3:10, SCMPDS_2:45
;
verum end;
A15:
now for i being Nat st i > 3 holds
(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . (intpos i) = s . (intpos i)let i be
Nat;
( i > 3 implies (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . (intpos i) = s . (intpos i) )assume A16:
i > 3
;
(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . (intpos i) = s . (intpos i)then A17:
i > 2
by XXREAL_0:2;
thus (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . (intpos i) =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)))) . (intpos i)
by SCMPDS_5:41
.=
(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . (intpos i)
by A9, A17, AMI_3:10, SCMPDS_2:46
.=
s . (intpos i)
by A12, A16
;
verum end;
now for i being Nat st 1 <= i & i <= len f holds
(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . (intpos (p0 + i)) = f . ilet i be
Nat;
( 1 <= i & i <= len f implies (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . (intpos (p0 + i)) = f . i )assume that A18:
1
<= i
and A19:
i <= len f
;
(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . (intpos (p0 + i)) = f . iset pi =
p0 + i;
p0 + i >= p0 + 1
by A18, XREAL_1:6;
then
p0 + i >= 7
by A5, XXREAL_0:2;
then A20:
p0 + i > 3
by XXREAL_0:2;
thus (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . (intpos (p0 + i)) =
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos (p0 + i))
by SCMPDS_5:15
.=
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)))) . (intpos (p0 + i))
by SCMPDS_5:41
.=
(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . (intpos (p0 + i))
by A11, A20, AMI_3:10, SCMPDS_2:46
.=
s . (intpos (p0 + i))
by A15, A20
.=
f . i
by A3, A18, A19
;
verum end;
then A21:
f is_FinSequence_on Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)),p0
;
A22: (IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)) . (intpos 1) =
(Exec (((GBP,1) := 0),(Exec ((GBP := 0),s)))) . (intpos 1)
by SCMPDS_5:42
.=
0
by A7, SCMPDS_2:46
;
A23: (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . (intpos 1) =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)))) . (intpos 1)
by SCMPDS_5:41
.=
0
by A22, A9, AMI_3:10, SCMPDS_2:46
;
A24:
( (((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1)) is_closed_on s,P & (((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1)) is_halting_on s,P )
by SCMPDS_6:20, SCMPDS_6:21;
A25: (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . GBP =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)))) . GBP
by SCMPDS_5:41
.=
0
by A10, A11, AMI_3:10, SCMPDS_2:46
;
A26: (IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)) . (intpos 2) =
(Exec (((GBP,2) := (n - 1)),(IExec (((GBP := 0) ';' ((GBP,1) := 0)),P,s)))) . (intpos 2)
by SCMPDS_5:41
.=
n - 1
by A9, SCMPDS_2:46
;
A27: (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 3) =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)))) . (intpos 3)
by SCMPDS_5:41
.=
p0 + 1
by A11, SCMPDS_2:46
;
A28:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 3) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . (intpos 3)
by SCMPDS_5:15;
A29:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 1) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . (intpos 1)
by SCMPDS_5:15;
A30:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . GBP = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . GBP
by SCMPDS_5:15;
A31:
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 2) = (Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))) . (intpos 2)
by SCMPDS_5:15;
A32: (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 1) =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)))) . (intpos 1)
by SCMPDS_5:41
.=
0
by A23, A11, AMI_3:10, SCMPDS_2:46
;
then
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 3) >= ((IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 1)) + 7
by A27, A5;
then
( 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))))))))) is_closed_on Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)),P & 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))))))))) is_halting_on Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)),P )
by A25, Lm12, A28, A29, A30;
then A33:
( 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))))))))) is_closed_on IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s),P & 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))))))))) is_halting_on IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s),P )
by SCMPDS_6:125, SCMPDS_6:126;
now for i being Nat st 1 <= i & i <= len g holds
g . 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)))))))))),P,(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))))) . (intpos (p0 + i))let i be
Nat;
( 1 <= i & i <= len g implies g . 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)))))))))),P,(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))))) . (intpos (p0 + i)) )assume
( 1
<= i &
i <= len g )
;
g . 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)))))))))),P,(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))))) . (intpos (p0 + i))hence g . i =
(IExec ((((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))) ';' (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)) . (intpos (p0 + i))
by A4
.=
(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,(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s))))) . (intpos (p0 + i))
by A24, A33, SCMPDS_7:30
;
verum end;
then A34:
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,(Initialize (IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)))),p0
;
(IExec (((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))) ';' ((GBP,3) := (p0 + 1))),P,s)) . (intpos 2) =
(Exec (((GBP,3) := (p0 + 1)),(IExec ((((GBP := 0) ';' ((GBP,1) := 0)) ';' ((GBP,2) := (n - 1))),P,s)))) . (intpos 2)
by SCMPDS_5:41
.=
n - 1
by A26, A11, AMI_3:10, SCMPDS_2:46
;
hence
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )
by A1, A2, A25, A32, A27, A21, A34, Lm15, A28, A29, A30, A31; verum