let i, k, n be Nat; for f, g, 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 f, g, 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,(- jj))
by A1, A3, Def11;
A6:
dom h = dom (((repeat ((Relax n) * (findmin n))) . i) . f)
by A2, Th37;
A7:
dom g = dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))
by A1, Th33;
A8:
now for x being object st x in (UsedVx (g,n)) \/ {k} holds
x in UsedVx (h,n)let x be
object ;
( 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
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, Th22
.=
((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . m
by A7, A13, A15, Th36
.=
- 1
by A1, A13, A15, A16, A11, Th32
;
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, Th29;
A19:
1
<= k
by A3, A4, Th29;
A20:
k <= n
by A3, A4, Th29;
h . k =
((Relax n) . ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))) . k
by A2, Th22
.=
((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . k
by A7, A18, A20, Th36
.=
- jj
by A1, A5, A18, Th19
;
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, Th33;
now for x being object st x in UsedVx (h,n) holds
x in (UsedVx (g,n)) \/ {k}let x be
object ;
( 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
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, Th22
.=
((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f)) . m
by A21, A23, A25, Th36
.=
(((repeat ((Relax n) * (findmin n))) . i) . f) . m
by A5, A25, A27, A28, Th18
;
then
m in { j where j is 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:2; not k in UsedVx (g,n)
assume
k in UsedVx (g,n)
; contradiction
then
ex j being Nat st
( j = k & j in dom g & 1 <= j & j <= n & g . j = - 1 )
;
hence
contradiction
by A3, A4, Th29; verum