let G be finite real-weighted WGraph; :: thesis: for n being Nat holds
( ((PRIM:CompSeq G) . n) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . n) `2 c= G .edgesBetween (((PRIM:CompSeq G) . n) `1 ) )
set PCS = PRIM:CompSeq G;
defpred S<sub>1</sub>[ Nat] means ( ((PRIM:CompSeq G) . $1) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . $1) `2 c= G .edgesBetween (((PRIM:CompSeq G) . $1) `1 ) );

now

((PRIM:CompSeq G) . 0 ) `1 = (PRIM:Init G) `1 by Def15
.= {(choose (the_Vertices_of G))} by MCART_1:7 ;
hence ((PRIM:CompSeq G) . 0 ) `1 is non empty Subset of (the_Vertices_of G) ; :: thesis: ((PRIM:CompSeq G) . 0 ) `2 c= G .edgesBetween (((PRIM:CompSeq G) . 0 ) `1 )
((PRIM:CompSeq G) . 0 ) `2 = (PRIM:Init G) `2 by Def15
.= {} by MCART_1:7 ;
hence ((PRIM:CompSeq G) . 0 ) `2 c= G .edgesBetween (((PRIM:CompSeq G) . 0 ) `1 ) by XBOOLE_1:2; :: thesis: verum

end;

then A1: S₁[ 0 ] ;

now

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
set Gn = (PRIM:CompSeq G) . n;
set Gn1 = (PRIM:CompSeq G) . (n + 1);
set Next = PRIM:NextBestEdges ((PRIM:CompSeq G) . n);
set e = choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n));
A3: (PRIM:CompSeq G) . (n + 1) = PRIM:Step ((PRIM:CompSeq G) . n) by Def15;

now

per cases ( PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} or PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} ) ;

suppose PRIM:NextBestEdges ((PRIM:CompSeq G) . n) = {} ; :: thesis: S₁[n + 1]

then (PRIM:CompSeq G) . (n + 1) = (PRIM:CompSeq G) . n by A3, Def14;
hence S₁[n + 1] by A2; :: thesis: verum

end;

suppose A4: PRIM:NextBestEdges ((PRIM:CompSeq G) . n) <> {} ; :: thesis: S₁[n + 1]

set src = (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)));
set tar = (the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)));
A5: choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)) in PRIM:NextBestEdges ((PRIM:CompSeq G) . n) by A4;
A9: choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)) SJoins ((PRIM:CompSeq G) . n) `1 ,(the_Vertices_of G) \ (((PRIM:CompSeq G) . n) `1 ),G by A4, Def12;

now

per cases ( (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) in ((PRIM:CompSeq G) . n) `1 or not (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) in ((PRIM:CompSeq G) . n) `1 ) ;

suppose A10: (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) in ((PRIM:CompSeq G) . n) `1 ; :: thesis: ( ((PRIM:CompSeq G) . (n + 1)) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) )

then A11: (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1 ) \/ {((the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))}),((((PRIM:CompSeq G) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))})] by A3, A4, Def14;
A12: ((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1 ) \/ {((the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} by A11, MCART_1:7;
A13: ((PRIM:CompSeq G) . (n + 1)) `2 = (((PRIM:CompSeq G) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))} by A11, MCART_1:7;

now

let x be set ; :: thesis: ( x in ((PRIM:CompSeq G) . (n + 1)) `1 implies x in the_Vertices_of G )
assume A14: x in ((PRIM:CompSeq G) . (n + 1)) `1 ; :: thesis: x in the_Vertices_of G

now

per cases ( x in ((PRIM:CompSeq G) . n) `1 or x in {((the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} ) by A12, A14, XBOOLE_0:def 3;

suppose x in ((PRIM:CompSeq G) . n) `1 ; :: thesis: x in the_Vertices_of G

hence x in the_Vertices_of G by A2; :: thesis: verum

end;

suppose x in {((the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} ; :: thesis: x in the_Vertices_of G

then x = (the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) by TARSKI:def 1;
hence x in the_Vertices_of G by A5, FUNCT_2:7; :: thesis: verum

end;

end;

end;

hence x in the_Vertices_of G ; :: thesis: verum

end;

hence ((PRIM:CompSeq G) . (n + 1)) `1 is non empty Subset of (the_Vertices_of G) by A11, MCART_1:7, TARSKI:def 3; :: thesis: ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 )
A15: ((PRIM:CompSeq G) . n) `1 c= ((PRIM:CompSeq G) . (n + 1)) `1 by A12, XBOOLE_1:7;
A16: G .edgesBetween (((PRIM:CompSeq G) . n) `1 ) c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) by A12, GLIB_000:39, XBOOLE_1:7;

now

let x be set ; :: thesis: ( x in ((PRIM:CompSeq G) . (n + 1)) `2 implies x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) )
assume A17: x in ((PRIM:CompSeq G) . (n + 1)) `2 ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 )

now

per cases ( x in ((PRIM:CompSeq G) . n) `2 or x in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))} ) by A13, A17, XBOOLE_0:def 3;

suppose x in ((PRIM:CompSeq G) . n) `2 ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 )

then x in G .edgesBetween (((PRIM:CompSeq G) . n) `1 ) by A2;
hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) by A16; :: thesis: verum

end;

suppose x in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))} ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 )

then A18: x = choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)) by TARSKI:def 1;
then (the_Target_of G) . x in {((the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} by TARSKI:def 1;
then (the_Target_of G) . x in ((PRIM:CompSeq G) . (n + 1)) `1 by A12, XBOOLE_0:def 3;
hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) by A5, A10, A15, A18, GLIB_000:34; :: thesis: verum

end;

end;

end;

hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) ; :: thesis: verum

end;

hence ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) by TARSKI:def 3; :: thesis: verum

end;

suppose A19: not (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) in ((PRIM:CompSeq G) . n) `1 ; :: thesis: ( ((PRIM:CompSeq G) . (n + 1)) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) )

then A20: (PRIM:CompSeq G) . (n + 1) = [((((PRIM:CompSeq G) . n) `1 ) \/ {((the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))}),((((PRIM:CompSeq G) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))})] by A3, A4, Def14;
A21: ((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1 ) \/ {((the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} by A20, MCART_1:7;
A22: ((PRIM:CompSeq G) . (n + 1)) `2 = (((PRIM:CompSeq G) . n) `2 ) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))} by A20, MCART_1:7;

now

let x be set ; :: thesis: ( x in ((PRIM:CompSeq G) . (n + 1)) `1 implies x in the_Vertices_of G )
assume A23: x in ((PRIM:CompSeq G) . (n + 1)) `1 ; :: thesis: x in the_Vertices_of G

now

per cases ( x in ((PRIM:CompSeq G) . n) `1 or x in {((the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} ) by A21, A23, XBOOLE_0:def 3;

suppose x in ((PRIM:CompSeq G) . n) `1 ; :: thesis: x in the_Vertices_of G

hence x in the_Vertices_of G by A2; :: thesis: verum

end;

suppose x in {((the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} ; :: thesis: x in the_Vertices_of G

then x = (the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) by TARSKI:def 1;
hence x in the_Vertices_of G by A5, FUNCT_2:7; :: thesis: verum

end;

end;

end;

hence x in the_Vertices_of G ; :: thesis: verum

end;

hence ((PRIM:CompSeq G) . (n + 1)) `1 is non empty Subset of (the_Vertices_of G) by A20, MCART_1:7, TARSKI:def 3; :: thesis: ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 )
A24: ((PRIM:CompSeq G) . n) `1 c= ((PRIM:CompSeq G) . (n + 1)) `1 by A21, XBOOLE_1:7;
A25: G .edgesBetween (((PRIM:CompSeq G) . n) `1 ) c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) by A21, GLIB_000:39, XBOOLE_1:7;
A26: (the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) in ((PRIM:CompSeq G) . n) `1 by A9, A19, GLIB_000:def 17;

now

let x be set ; :: thesis: ( x in ((PRIM:CompSeq G) . (n + 1)) `2 implies x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) )
assume A27: x in ((PRIM:CompSeq G) . (n + 1)) `2 ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 )

now

per cases ( x in ((PRIM:CompSeq G) . n) `2 or x in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))} ) by A22, A27, XBOOLE_0:def 3;

suppose x in ((PRIM:CompSeq G) . n) `2 ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 )

then x in G .edgesBetween (((PRIM:CompSeq G) . n) `1 ) by A2;
hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) by A25; :: thesis: verum

end;

suppose x in {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))} ; :: thesis: x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 )

then A28: x = choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)) by TARSKI:def 1;
then (the_Source_of G) . x in {((the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} by TARSKI:def 1;
then (the_Source_of G) . x in ((PRIM:CompSeq G) . (n + 1)) `1 by A21, XBOOLE_0:def 3;
hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) by A5, A24, A26, A28, GLIB_000:34; :: thesis: verum

end;

end;

end;

hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) ; :: thesis: verum

end;

hence ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1 ) by TARSKI:def 3; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

end;

end;

hence S₁[n + 1] ; :: thesis: verum

end;

then A29: for n being Nat st S₁[n] holds
S₁[n + 1] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A29);
hence for n being Nat holds
( ((PRIM:CompSeq G) . n) `1 is non empty Subset of (the_Vertices_of G) & ((PRIM:CompSeq G) . n) `2 c= G .edgesBetween (((PRIM:CompSeq G) . n) `1 ) ) ; :: thesis: verum