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) );
A1: ((PRIM:CompSeq G) . 0) `2 = (PRIM:Init G) `2 by Def17
.= {} by MCART_1:7 ;

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

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, Def15;
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;
A6: 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, Def13;

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 A7: (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 A8: (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, Def15;
then A9: ((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1) \/ {((the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} by MCART_1:7;
then A10: G .edgesBetween (((PRIM:CompSeq G) . n) `1) c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) by GLIB_000:36, XBOOLE_1:7;

now

let x be set ; :: thesis: ( x in ((PRIM:CompSeq G) . (n + 1)) `1 implies x in the_Vertices_of G )
assume A11: 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 A9, A11, 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:5; :: 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 A8, MCART_1:7, TARSKI:def 3; :: thesis: ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)
A12: ((PRIM:CompSeq G) . (n + 1)) `2 = (((PRIM:CompSeq G) . n) `2) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))} by A8, MCART_1:7;
A13: ((PRIM:CompSeq G) . n) `1 c= ((PRIM:CompSeq G) . (n + 1)) `1 by A9, 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 A14: 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 A12, A14, 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 A10; :: 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 A15: 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 A9, XBOOLE_0:def 3;
hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) by A5, A7, A13, A15, GLIB_000:31; :: 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 A16: 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 A17: (the_Target_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))) in ((PRIM:CompSeq G) . n) `1 by A6, GLIB_000:def 15;
A18: (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, A16, Def15;
then A19: ((PRIM:CompSeq G) . (n + 1)) `1 = (((PRIM:CompSeq G) . n) `1) \/ {((the_Source_of G) . (choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n))))} by MCART_1:7;
then A20: G .edgesBetween (((PRIM:CompSeq G) . n) `1) c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) by GLIB_000:36, XBOOLE_1:7;

now

let x be set ; :: thesis: ( x in ((PRIM:CompSeq G) . (n + 1)) `1 implies x in the_Vertices_of G )
assume A21: 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 A19, A21, 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:5; :: 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 A18, MCART_1:7, TARSKI:def 3; :: thesis: ((PRIM:CompSeq G) . (n + 1)) `2 c= G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1)
A22: ((PRIM:CompSeq G) . (n + 1)) `2 = (((PRIM:CompSeq G) . n) `2) \/ {(choose (PRIM:NextBestEdges ((PRIM:CompSeq G) . n)))} by A18, MCART_1:7;
A23: ((PRIM:CompSeq G) . n) `1 c= ((PRIM:CompSeq G) . (n + 1)) `1 by A19, 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 A24: 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, A24, 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 A20; :: 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 A25: 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 A19, XBOOLE_0:def 3;
hence x in G .edgesBetween (((PRIM:CompSeq G) . (n + 1)) `1) by A5, A23, A17, A25, GLIB_000:31; :: 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 A26: for n being Nat st S₁[n] holds
S₁[n + 1] ;
((PRIM:CompSeq G) . 0) `1 = (PRIM:Init G) `1 by Def17
.= {(choose (the_Vertices_of G))} by MCART_1:7 ;
then A27: S₁[ 0 ] by A1, XBOOLE_1:2;
for n being Nat holds S₁[n] from NAT_1:sch 2(A27, A26);
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