let n be Nat; for f being Element of REAL * st 1 <= n & 1 in dom f & f . (n + 1) <> - 1 & ( for i being Nat st 1 <= i & i <= n holds
f . i = 1 ) & ( for i being Nat st 2 <= i & i <= n holds
f . (n + i) = - 1 ) holds
( 1 = Argmin ((OuterVx (f,n)),f,n) & UsedVx (f,n) = {} & {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) )
let f be Element of REAL * ; ( 1 <= n & 1 in dom f & f . (n + 1) <> - 1 & ( for i being Nat st 1 <= i & i <= n holds
f . i = 1 ) & ( for i being Nat st 2 <= i & i <= n holds
f . (n + i) = - 1 ) implies ( 1 = Argmin ((OuterVx (f,n)),f,n) & UsedVx (f,n) = {} & {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) ) )
set R = Relax n;
set M = findmin n;
set f0 = ((repeat ((Relax n) * (findmin n))) . 0) . f;
set RT = repeat ((Relax n) * (findmin n));
assume that
A1:
1 <= n
and
A2:
( 1 in dom f & f . (n + 1) <> - 1 )
and
A3:
for i being Nat st 1 <= i & i <= n holds
f . i = 1
and
A4:
for i being Nat st 2 <= i & i <= n holds
f . (n + i) = - 1
; ( 1 = Argmin ((OuterVx (f,n)),f,n) & UsedVx (f,n) = {} & {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) )
set k = Argmin ((OuterVx (f,n)),f,n);
f . 1 = 1
by A1, A3;
then A5:
1 in { j where j is Nat : ( j in dom f & 1 <= j & j <= n & f . j <> - 1 & f . (n + j) <> - 1 ) }
by A1, A2;
thus A6:
Argmin ((OuterVx (f,n)),f,n) = 1
( UsedVx (f,n) = {} & {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) )proof
assume A7:
Argmin (
(OuterVx (f,n)),
f,
n)
<> 1
;
contradiction
1
<= Argmin (
(OuterVx (f,n)),
f,
n)
by A5, Th29;
then
1
< Argmin (
(OuterVx (f,n)),
f,
n)
by A7, XXREAL_0:1;
then A8:
1
+ 1
<= Argmin (
(OuterVx (f,n)),
f,
n)
by INT_1:7;
(
Argmin (
(OuterVx (f,n)),
f,
n)
<= n &
f . (n + (Argmin ((OuterVx (f,n)),f,n))) <> - 1 )
by A5, Th29;
hence
contradiction
by A4, A8;
verum
end;
thus A9:
UsedVx (f,n) = {}
{1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n)
OuterVx (f,n) <> {}
by A5;
then A11:
OuterVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n) <> {}
by Th21;
A12: Argmin ((OuterVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n)),(((repeat ((Relax n) * (findmin n))) . 0) . f),n) =
Argmin ((OuterVx (f,n)),(((repeat ((Relax n) * (findmin n))) . 0) . f),n)
by Th21
.=
1
by A6, Th21
;
thus UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) =
UsedVx ((((repeat ((Relax n) * (findmin n))) . (0 + 1)) . f),n)
.=
(UsedVx ((((repeat ((Relax n) * (findmin n))) . 0) . f),n)) \/ {1}
by A11, A12, Th39
.=
(UsedVx (f,n)) \/ {1}
by Th21
.=
{1}
by A9
; verum