let i, k, n be Nat; :: thesis: 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 * ; :: thesis: ( 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) <> {} ; :: thesis: ( 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;

assume k in UsedVx (g,n) ; :: thesis: 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; :: thesis: verum

( UsedVx (h,n) = (UsedVx (g,n)) \/ {k} & not k in UsedVx (g,n) )

let f, g, h be Element of REAL * ; :: thesis: ( 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) <> {} ; :: thesis: ( 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 :: thesis: for x being object st x in (UsedVx (g,n)) \/ {k} holds

x in UsedVx (h,n)

A21:
dom h = dom ((findmin n) . (((repeat ((Relax n) * (findmin n))) . i) . f))
by A6, Th33;x in UsedVx (h,n)

let x be object ; :: thesis: ( x in (UsedVx (g,n)) \/ {k} implies b_{1} in UsedVx (h,n) )

assume A9: x in (UsedVx (g,n)) \/ {k} ; :: thesis: b_{1} in UsedVx (h,n)

end;assume A9: x in (UsedVx (g,n)) \/ {k} ; :: thesis: b

per cases
( x in UsedVx (g,n) or x in {k} )
by A9, XBOOLE_0:def 3;

end;

suppose A10:
x in UsedVx (g,n)
; :: thesis: b_{1} 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; :: thesis: verum

end;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; :: thesis: verum

suppose
x in {k}
; :: thesis: b_{1} 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; :: thesis: verum

end;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; :: thesis: verum

now :: thesis: for x being object st x in UsedVx (h,n) holds

x in (UsedVx (g,n)) \/ {k}

hence
UsedVx (h,n) = (UsedVx (g,n)) \/ {k}
by A8, TARSKI:2; :: thesis: not k in UsedVx (g,n)x in (UsedVx (g,n)) \/ {k}

let x be object ; :: thesis: ( x in UsedVx (h,n) implies b_{1} in (UsedVx (g,n)) \/ {k} )

assume x in UsedVx (h,n) ; :: thesis: b_{1} 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 ;

end;assume x in UsedVx (h,n) ; :: thesis: b

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 )
;

end;

suppose
m = k
; :: thesis: b_{1} in (UsedVx (g,n)) \/ {k}

then
x in {k}
by A22, TARSKI:def 1;

hence x in (UsedVx (g,n)) \/ {k} by XBOOLE_0:def 3; :: thesis: verum

end;hence x in (UsedVx (g,n)) \/ {k} by XBOOLE_0:def 3; :: thesis: verum

suppose A27:
m <> k
; :: thesis: b_{1} 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; :: thesis: verum

end;- 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; :: thesis: verum

assume k in UsedVx (g,n) ; :: thesis: 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; :: thesis: verum