let G be _finite real-weighted WGraph; :: thesis: for n being Nat holds
( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} iff ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G )
let n be Nat; :: thesis: ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} iff ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G )
set src = the Element of the_Vertices_of G;
set PCS = PRIM:CompSeq G;
set RFS = G .reachableFrom the Element of the_Vertices_of G;
set Gn = (PRIM:CompSeq G) . n;
set EG = the_Edges_of G;
set Next = PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
set GnV = ((PRIM:CompSeq G) . n) `1 ;
set GnVg = (the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1);
set e = the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
hereby :: thesis: ( ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G implies PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} )
assume A1: PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} ; :: thesis: ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G
now :: thesis: not ((PRIM:CompSeq G) . n) `1 <> G .reachableFrom the Element of the_Vertices_of G
defpred S1[ set ] means $1 SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G;
assume A2: ((PRIM:CompSeq G) . n) `1 <> G .reachableFrom the Element of the_Vertices_of G ; :: thesis: contradiction
consider BE1 being Subset of (the_Edges_of G) such that
A3: for x being set holds
( x in BE1 iff ( x in the_Edges_of G & S1[x] ) ) from SUBSET_1:sch 1();
 ((PRIM:CompSeq G) . n) `1 c= G .reachableFrom the Element of the_Vertices_of G by Th33;
then A4: ((PRIM:CompSeq G) . n) `1 c< G .reachableFrom the Element of the_Vertices_of G by A2, XBOOLE_0:def 8;
now :: thesis: not BE1 = {}
the Element of the_Vertices_of G in { the Element of the_Vertices_of G} by TARSKI:def 1;
then the Element of the_Vertices_of G in (PRIM:Init G) `1 ;
then A5: the Element of the_Vertices_of G in ((PRIM:CompSeq G) . 0) `1 by Def17;
assume A6: BE1 = {} ; :: thesis: contradiction
consider v being object such that
A7: v in G .reachableFrom the Element of the_Vertices_of G and
A8: not v in ((PRIM:CompSeq G) . n) `1 by A4, XBOOLE_0:6;
reconsider v = v as Vertex of G by A7;
consider W being Walk of G such that
A9: W is_Walk_from the Element of the_Vertices_of G,v by A7, GLIB_002:def 5;
defpred S2[ Nat] means ( $1 is odd & $1 <= len W & not W . $1 in ((PRIM:CompSeq G) . n) `1 );
W . (len W) = W .last() by GLIB_001:def 7
.= v by A9, GLIB_001:def 23 ;
then A10: ex k being Nat st S2[k] by A8;
consider k being Nat such that
A11: ( S2[k] & ( for m being Nat st S2[m] holds
k <= m ) ) from NAT_1:sch 5(A10);
A12: ((PRIM:CompSeq G) . 0) `1 c= ((PRIM:CompSeq G) . n) `1 by Th34;
now :: thesis: contradiction
per cases ( k = 1 or k <> 1 ) ;
suppose A13: k <> 1 ; :: thesis: contradiction
reconsider k9 = k as odd Element of NAT by A11, ORDINAL1:def 12;
1 <= k by A11, ABIAN:12;
then 1 < k by A13, XXREAL_0:1;
then 1 + 1 <= k by NAT_1:13;
then reconsider k2a = k9 - (2 * 1) as odd Element of NAT by INT_1:5;
set e = W . (k2a + 1);
A14: k - 2 < (len W) - 0 by A11, XREAL_1:15;
then A15: W . (k2a + 1) Joins W . k2a,W . (k2a + 2),G by GLIB_001:def 3;
then A16: W . (k2a + 1) in the_Edges_of G ;
k2a < k - 0 by XREAL_1:15;
then A17: W . k2a in ((PRIM:CompSeq G) . n) `1 by A11, A14;
W . k in the_Vertices_of G by A15, GLIB_000:13;
then W . k in (the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1) by A11, XBOOLE_0:def 5;
then S1[W . (k2a + 1)] by A17, A15, GLIB_000:17;
hence contradiction by A3, A6, A16; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
then reconsider BE1 = BE1 as non empty finite set ;
deffunc H1( Element of BE1) -> set = (the_Weight_of G) . $1;
consider e1 being Element of BE1 such that
A18: for e2 being Element of BE1 holds H1(e1) <= H1(e2) from PRE_CIRC:sch 5();
A19: now :: thesis: for e2 being set st e2 SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G holds
(the_Weight_of G) . e1 <= (the_Weight_of G) . e2
let e2 be set ; :: thesis: ( e2 SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G implies (the_Weight_of G) . e1 <= (the_Weight_of G) . e2 )
assume A20: e2 SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G ; :: thesis: (the_Weight_of G) . e1 <= (the_Weight_of G) . e2
reconsider e29 = e2 as Element of BE1 by A3, A20;
(the_Weight_of G) . e1 <= (the_Weight_of G) . e29 by A18;
hence (the_Weight_of G) . e1 <= (the_Weight_of G) . e2 ; :: thesis: verum
end;
e1 SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G by A3;
hence contradiction by A1, A19, Def13; :: thesis: verum
end;
hence ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G ; :: thesis: verum
end;
assume A21: ((PRIM:CompSeq G) . n) `1 = G .reachableFrom the Element of the_Vertices_of G ; :: thesis: PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {}
now :: thesis: not PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {}
assume PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} ; :: thesis: contradiction
then A22: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1),G by Def13;
then A23: the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in the_Edges_of G ;
now :: thesis: contradiction
per cases ( ( (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 & (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in (the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1) ) or ( (the_Source_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in (the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1) & (the_Target_of G) . the Element of PRIM:NextBestEdges ((PRIM:CompSeq G) . n) in ((PRIM:CompSeq G) . n) `1 ) ) by A22;
end;
end;
hence contradiction ; :: thesis: verum
end;
hence PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} ; :: thesis: verum