let i, k, n be Nat; :: thesis: for f, g, h being Element of REAL * st g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & i in UsedVx (g,n) & len f = ((n * n) + (3 * n)) + 1 holds
h . (n + i) = g . (n + i)
let f, g, h be Element of REAL * ; :: thesis: ( g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & i in UsedVx (g,n) & len f = ((n * n) + (3 * n)) + 1 implies h . (n + i) = g . (n + i) )
set R = Relax n;
set M = findmin n;
set RF = repeat ((Relax n) * (findmin n));
set mi = ((n * n) + (3 * n)) + 1;
set Ak = Argmin ((OuterVx (g,n)),g,n);
assume that
A1: g = ((repeat ((Relax n) * (findmin n))) . k) . f and
A2: h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f and
A3: OuterVx (g,n) <> {} and
A4: i in UsedVx (g,n) and
A5: len f = ((n * n) + (3 * n)) + 1 ; :: thesis: h . (n + i) = g . (n + i)
A6: h = (Relax n) . ((findmin n) . g) by A1, A2, Th22
.= Relax (((findmin n) . g),n) by Def15 ;
set ni = n + i;
A7: ex j being Nat st
( i = j & j in dom g & 1 <= j & j <= n & g . j = - 1 ) by A4;
then A8: n + i <= n + n by XREAL_1:7;
A9: 1 <= n + i by A7, NAT_1:12;
A10: 2 * n < ((n * n) + (3 * n)) + 1 by Lm7;
then n + i < ((n * n) + (3 * n)) + 1 by A8, XXREAL_0:2;
then n + i in dom f by A5, A9, FINSEQ_3:25;
then n + i in dom g by A1, Th41;
then A11: ( (n + i) -' n = i & n + i in dom ((findmin n) . g) ) by Th33, NAT_D:34;
A12: Argmin ((OuterVx (g,n)),g,n) <= n by A3, Th29;
A13: n < ((n * n) + (3 * n)) + 1 by Lm7;
A14: (findmin n) . g = (g,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (g,n)),g,n)),(- jj)) by Def11;
g . (Argmin ((OuterVx (g,n)),g,n)) <> - 1 by A3, Th29;
then A15: not (findmin n) . g hasBetterPathAt n,i by A14, A7, A13, Th18;
n + 1 <= n + i by A7, XREAL_1:7;
then A16: n < n + i by NAT_1:13;
n + i <= 2 * n by A8;
hence h . (n + i) = ((findmin n) . g) . (n + i) by A6, A16, A11, A15, Def14
.= g . (n + i) by A14, A12, A8, A16, A10, Th18 ;
:: thesis: verum