let n, i, k be Element of NAT ; for g, f, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . i) . f & h = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f & k = Argmin ((OuterVx (g,n)),g,n) & OuterVx (g,n) <> {} holds
( UsedVx (h,n) = (UsedVx (g,n)) \/ {k} & not k in UsedVx (g,n) )
let g, f, h be Element of REAL * ; ( g = ((repeat ((Relax n) * (findmin n))) . i) . f & h = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f & k = Argmin ((OuterVx (g,n)),g,n) & OuterVx (g,n) <> {} implies ( UsedVx (h,n) = (UsedVx (g,n)) \/ {k} & not k in UsedVx (g,n) ) )
set R = Relax n;
set M = findmin n;
set ff = ((repeat ((Relax n) * (findmin n))) . i) . f;
set Fi1 = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f;
set mi = ((n * n) + (3 * n)) + 1;
assume that
A1:
g = ((repeat ((Relax n) * (findmin n))) . i) . f
and
A2:
h = ((repeat ((Relax n) * (findmin n))) . (i + 1)) . f
and
A3:
k = Argmin ((OuterVx (g,n)),g,n)
and
A4:
OuterVx (g,n) <> {}
; ( UsedVx (h,n) = (UsedVx (g,n)) \/ {k} & not k in UsedVx (g,n) )
A5:
(findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f) = ((((repeat ((Relax n) * (findmin n))) . i) . f),(((n * n) + (3 * n)) + 1)) := (k,(- 1))
by A1, A3, Def11;
A6:
dom h = dom (((repeat ((Relax n) * (findmin n))) . i) . f)
by A2, Th38;
A7:
dom g = dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))
by A1, Th34;
A8:
now let x be
set ;
( x in (UsedVx (g,n)) \/ {k} implies b1 in UsedVx (h,n) )assume A9:
x in (UsedVx (g,n)) \/ {k}
;
b1 in UsedVx (h,n)per cases
( x in UsedVx (g,n) or x in {k} )
by A9, XBOOLE_0:def 3;
suppose A10:
x in UsedVx (
g,
n)
;
b1 in UsedVx (h,n)A11:
n < ((n * n) + (3 * n)) + 1
by Lm7;
consider m being
Element of
NAT such that A12:
x = m
and A13:
m in dom g
and A14:
1
<= m
and A15:
m <= n
and A16:
g . m = - 1
by A10;
h . m =
((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . m
by A2, Th23
.=
((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . m
by A7, A13, A15, Th37
.=
- 1
by A1, A13, A15, A16, A11, Th33
;
hence
x in UsedVx (
h,
n)
by A1, A6, A12, A13, A14, A15;
verum end; suppose
x in {k}
;
b1 in UsedVx (h,n)then A17:
x = k
by TARSKI:def 1;
A18:
k in dom g
by A3, A4, Th30;
A19:
1
<= k
by A3, A4, Th30;
A20:
k <= n
by A3, A4, Th30;
h . k =
((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . k
by A2, Th23
.=
((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . k
by A7, A18, A20, Th37
.=
- 1
by A1, A5, A18, Th20
;
hence
x in UsedVx (
h,
n)
by A1, A6, A17, A18, A19, A20;
verum end; end;
A21:
dom h = dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))
by A6, Th34;
now let x be
set ;
( x in UsedVx (h,n) implies b1 in (UsedVx (g,n)) \/ {k} )assume
x in UsedVx (
h,
n)
;
b1 in (UsedVx (g,n)) \/ {k}then consider m being
Element of
NAT such that A22:
x = m
and A23:
m in dom h
and A24:
1
<= m
and A25:
m <= n
and A26:
h . m = - 1
;
per cases
( m = k or m <> k )
;
suppose A27:
m <> k
;
b1 in (UsedVx (g,n)) \/ {k}A28:
n < ((n * n) + (3 * n)) + 1
by Lm7;
- 1 =
((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . m
by A2, A26, Th23
.=
((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . m
by A21, A23, A25, Th37
.=
(((repeat ((Relax n) * (findmin n))) . i) . f) . m
by A5, A25, A27, A28, Th19
;
then
m in { j where j is Element of NAT : ( j in dom (((repeat ((Relax n) * (findmin n))) . i) . f) & 1 <= j & j <= n & (((repeat ((Relax n) * (findmin n))) . i) . f) . j = - 1 ) }
by A6, A23, A24, A25;
hence
x in (UsedVx (g,n)) \/ {k}
by A1, A22, XBOOLE_0:def 3;
verum end; end;
hence
UsedVx (h,n) = (UsedVx (g,n)) \/ {k}
by A8, TARSKI:1; not k in UsedVx (g,n)
assume
k in UsedVx (g,n)
; contradiction
then
ex j being Element of NAT st
( j = k & j in dom g & 1 <= j & j <= n & g . j = - 1 )
;
hence
contradiction
by A3, A4, Th30; verum