glib_004.miz



    begin

    

     Lm1: for F be Function, x,y be set holds ( dom (F +* (x .--> y))) = (( dom F) \/ {x})

    proof

      let F be Function, x,y be set;

      

      thus ( dom (F +* (x .--> y))) = (( dom F) \/ ( dom (x .--> y))) by FUNCT_4:def 1

      .= (( dom F) \/ {x});

    end;

    

     Lm2: for F be Function, x,y,z be set st z in ( dom (F +* (x .--> y))) & not z in ( dom F) holds x = z

    proof

      let F be Function, x,y,z be set such that

       A1: z in ( dom (F +* (x .--> y))) and

       A2: not z in ( dom F);

      ( dom (x .--> y)) = {x};

      then z in (( dom F) \/ {x}) by A1, FUNCT_4:def 1;

      then z in {x} by A2, XBOOLE_0:def 3;

      hence thesis by TARSKI:def 1;

    end;

    theorem :: GLIB_004:1

    

     Th1: for f,g be Function holds ( support (f +* g)) c= (( support f) \/ ( support g))

    proof

      let f,g be Function;

      let a be object;

      assume a in ( support (f +* g));

      then

       A1: ((f +* g) . a) <> 0 by PRE_POLY:def 7;

      assume

       A2: not a in (( support f) \/ ( support g));

      then not a in ( support f) by XBOOLE_0:def 3;

      then

       A3: (f . a) = 0 by PRE_POLY:def 7;

       not a in ( support g) by A2, XBOOLE_0:def 3;

      then

       A4: (g . a) = 0 by PRE_POLY:def 7;

      a in ( dom g) or not a in ( dom g);

      hence contradiction by A1, A3, A4, FUNCT_4: 11, FUNCT_4: 13;

    end;

    theorem :: GLIB_004:2

    

     Th2: for f be Function, x,y be object holds ( support (f +* (x .--> y))) c= (( support f) \/ {x})

    proof

      let f be Function, x,y be object;

      let a be object;

      assume a in ( support (f +* (x .--> y)));

      then

       A1: ((f +* (x .--> y)) . a) <> 0 by PRE_POLY:def 7;

      per cases ;

        suppose a = x;

        then a in {x} by TARSKI:def 1;

        hence thesis by XBOOLE_0:def 3;

      end;

        suppose a <> x;

        then ((f +* (x .--> y)) . a) = (f . a) by FUNCT_4: 83;

        then a in ( support f) by A1, PRE_POLY:def 7;

        hence thesis by XBOOLE_0:def 3;

      end;

    end;

    theorem :: GLIB_004:3

    

     Th3: for A,B be set, b be Rbag of A, b1 be Rbag of B, b2 be Rbag of (A \ B) st b = (b1 +* b2) holds ( Sum b) = (( Sum b1) + ( Sum b2))

    proof

      let A,B be set, b be Rbag of A, b1 be Rbag of B, b2 be Rbag of (A \ B) such that

       A1: b = (b1 +* b2);

      ( dom b) = (( dom b1) \/ ( dom b2)) by A1, FUNCT_4:def 1;

      then ( dom b1) c= ( dom b) by XBOOLE_1: 7;

      then B c= ( dom b) by PARTFUN1:def 2;

      then

       A2: B c= A by PARTFUN1:def 2;

      set B1 = (( EmptyBag A) +* b1);

      

       A3: ( dom B1) = (( dom ( EmptyBag A)) \/ ( dom b1)) by FUNCT_4:def 1

      .= (A \/ ( dom b1)) by PARTFUN1:def 2

      .= (A \/ B) by PARTFUN1:def 2

      .= A by A2, XBOOLE_1: 12;

      ( support B1) c= (( support ( EmptyBag A)) \/ ( support b1)) by Th1;

      then

      reconsider B1 as Rbag of A by A3, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;

      set B2 = (( EmptyBag A) +* b2);

      

       A4: ( dom B2) = (( dom ( EmptyBag A)) \/ ( dom b2)) by FUNCT_4:def 1

      .= (A \/ ( dom b2)) by PARTFUN1:def 2

      .= (A \/ (A \ B)) by PARTFUN1:def 2

      .= A by XBOOLE_1: 12;

      ( support B2) c= (( support ( EmptyBag A)) \/ ( support b2)) by Th1;

      then

      reconsider B2 as Rbag of A by A4, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;

       A5:

      now

        let x be object;

        assume

         A6: x in A;

        

         A7: ( dom b1) = B by PARTFUN1:def 2;

        

         A8: ( dom b2) = (A \ B) by PARTFUN1:def 2;

        per cases ;

          suppose

           A9: x in B;

          then

           A10: (B1 . x) = (b1 . x) by A7, FUNCT_4: 13;

          

           A11: not x in ( dom b2) by A9, XBOOLE_0:def 5;

          

          then (B2 . x) = (( EmptyBag A) . x) by FUNCT_4: 11

          .= 0 by PBOOLE: 5;

          

          hence (b . x) = ((B1 . x) + (B2 . x)) by A1, A11, A10, FUNCT_4: 11

          .= ((B1 + B2) . x) by PRE_POLY:def 5;

        end;

          suppose

           A12: not x in B;

          

          then

           A13: (B1 . x) = (( EmptyBag A) . x) by A7, FUNCT_4: 11

          .= 0 by PBOOLE: 5;

          

           A14: x in ( dom b2) by A6, A8, A12, XBOOLE_0:def 5;

          then (B2 . x) = (b2 . x) by FUNCT_4: 13;

          

          hence (b . x) = ((B1 . x) + (B2 . x)) by A1, A13, A14, FUNCT_4: 13

          .= ((B1 + B2) . x) by PRE_POLY:def 5;

        end;

      end;

      consider F2 be FinSequence of REAL such that

       A15: ( Sum B2) = ( Sum F2) and

       A16: F2 = (B2 * ( canFS ( support B2))) by UPROOTS:def 3;

      ( rng ( canFS ( support B2))) = ( support B2) & ( support B2) c= ( dom B2) by FUNCT_2:def 3, PRE_POLY: 37;

      then

       A17: ( dom F2) = ( dom ( canFS ( support B2))) by A16, RELAT_1: 27;

      consider F1 be FinSequence of REAL such that

       A18: ( Sum B1) = ( Sum F1) and

       A19: F1 = (B1 * ( canFS ( support B1))) by UPROOTS:def 3;

      consider f1 be FinSequence of REAL such that

       A20: ( Sum b1) = ( Sum f1) and

       A21: f1 = (b1 * ( canFS ( support b1))) by UPROOTS:def 3;

      

       A22: ( rng ( canFS ( support b1))) = ( support b1) & ( support b1) c= ( dom b1) by FUNCT_2:def 3, PRE_POLY: 37;

      then

       A23: ( dom f1) = ( dom ( canFS ( support b1))) by A21, RELAT_1: 27;

       A24:

      now

        let x be object;

        hereby

          assume

           A25: x in ( support b1);

          then

           A26: (b1 . x) <> 0 by PRE_POLY:def 7;

          ( support b1) c= ( dom b1) by PRE_POLY: 37;

          then (B1 . x) = (b1 . x) by A25, FUNCT_4: 13;

          hence x in ( support B1) by A26, PRE_POLY:def 7;

        end;

        assume

         A27: x in ( support B1);

        then

         A28: (B1 . x) <> 0 by PRE_POLY:def 7;

        per cases ;

          suppose not x in ( dom b1);

          

          then (B1 . x) = (( EmptyBag A) . x) by FUNCT_4: 11

          .= 0 by PBOOLE: 5;

          hence x in ( support b1) by A27, PRE_POLY:def 7;

        end;

          suppose x in ( dom b1);

          then (B1 . x) = (b1 . x) by FUNCT_4: 13;

          hence x in ( support b1) by A28, PRE_POLY:def 7;

        end;

      end;

      then

       A29: ( support b1) = ( support B1) by TARSKI: 2;

       A30:

      now

        let k be Nat such that

         A31: k in ( dom f1);

        

         A32: (( canFS ( support b1)) . k) in ( rng ( canFS ( support b1))) by A23, A31, FUNCT_1: 3;

        

        thus (f1 . k) = (b1 . (( canFS ( support b1)) . k)) by A21, A23, A31, FUNCT_1: 13

        .= (B1 . (( canFS ( support b1)) . k)) by A22, A32, FUNCT_4: 13

        .= (F1 . k) by A19, A23, A29, A31, FUNCT_1: 13;

      end;

      ( rng ( canFS ( support B1))) = ( support B1) & ( support B1) c= ( dom B1) by FUNCT_2:def 3, PRE_POLY: 37;

      then ( dom F1) = ( dom ( canFS ( support B1))) by A19, RELAT_1: 27;

      then ( dom f1) = ( dom F1) by A23, A24, TARSKI: 2;

      then

       A33: ( Sum B1) = ( Sum b1) by A20, A18, A30, FINSEQ_1: 13;

      consider f2 be FinSequence of REAL such that

       A34: ( Sum b2) = ( Sum f2) and

       A35: f2 = (b2 * ( canFS ( support b2))) by UPROOTS:def 3;

      

       A36: ( rng ( canFS ( support b2))) = ( support b2) & ( support b2) c= ( dom b2) by FUNCT_2:def 3, PRE_POLY: 37;

      then

       A37: ( dom f2) = ( dom ( canFS ( support b2))) by A35, RELAT_1: 27;

      now

        let x be object;

        hereby

          assume

           A38: x in ( support b2);

          then

           A39: (b2 . x) <> 0 by PRE_POLY:def 7;

          ( support b2) c= ( dom b2) by PRE_POLY: 37;

          then (B2 . x) = (b2 . x) by A38, FUNCT_4: 13;

          hence x in ( support B2) by A39, PRE_POLY:def 7;

        end;

        assume

         A40: x in ( support B2);

        then

         A41: (B2 . x) <> 0 by PRE_POLY:def 7;

        per cases ;

          suppose not x in ( dom b2);

          

          then (B2 . x) = (( EmptyBag A) . x) by FUNCT_4: 11

          .= 0 by PBOOLE: 5;

          hence x in ( support b2) by A40, PRE_POLY:def 7;

        end;

          suppose x in ( dom b2);

          then (B2 . x) = (b2 . x) by FUNCT_4: 13;

          hence x in ( support b2) by A41, PRE_POLY:def 7;

        end;

      end;

      then

       A42: ( support b2) = ( support B2) by TARSKI: 2;

      now

        let k be Nat such that

         A43: k in ( dom f2);

        

         A44: (( canFS ( support b2)) . k) in ( rng ( canFS ( support b2))) by A37, A43, FUNCT_1: 3;

        

        thus (f2 . k) = (b2 . (( canFS ( support b2)) . k)) by A35, A37, A43, FUNCT_1: 13

        .= (B2 . (( canFS ( support b2)) . k)) by A36, A44, FUNCT_4: 13

        .= (F2 . k) by A16, A37, A42, A43, FUNCT_1: 13;

      end;

      then ( Sum B2) = ( Sum b2) by A34, A35, A15, A36, A17, A42, FINSEQ_1: 13, RELAT_1: 27;

      hence thesis by A33, A5, PBOOLE: 3, UPROOTS: 15;

    end;

    theorem :: GLIB_004:4

    

     Th4: for X,x be set, b be Rbag of X st ( dom b) = {x} holds ( Sum b) = (b . x)

    proof

      let X,x be set, b be Rbag of X;

      assume

       A1: ( dom b) = {x};

      then

       A2: x in ( dom b) by TARSKI:def 1;

      ( support b) c= {x} & {x} c= X by A1, PRE_POLY: 37;

      then

      consider f be FinSequence of REAL such that

       A3: f = (b * ( canFS {x})) and

       A4: ( Sum b) = ( Sum f) by UPROOTS: 14;

      reconsider bx = (b . x) as Element of REAL by XREAL_0:def 1;

      f = (b * <*x*>) by A3, FINSEQ_1: 94;

      then f = <*bx*> by A2, FINSEQ_2: 34;

      hence thesis by A4, FINSOP_1: 11;

    end;

    theorem :: GLIB_004:5

    

     Th5: for A be set, b1,b2 be Rbag of A st (for x be set st x in A holds (b1 . x) <= (b2 . x)) holds ( Sum b1) <= ( Sum b2)

    proof

      let A be set, b1,b2 be Rbag of A such that

       A1: for x be set st x in A holds (b1 . x) <= (b2 . x);

      set S = (( support b1) \/ ( support b2));

      

       A2: ( dom b2) = A by PARTFUN1:def 2;

      then

       A3: ( support b2) c= A by PRE_POLY: 37;

      

       A4: ( dom b1) = A by PARTFUN1:def 2;

      then ( support b1) c= A by PRE_POLY: 37;

      then

      reconsider S as finite Subset of A by A3, XBOOLE_1: 8;

      consider f1 be FinSequence of REAL such that

       A5: f1 = (b1 * ( canFS S)) and

       A6: ( Sum b1) = ( Sum f1) by UPROOTS: 14, XBOOLE_1: 7;

      consider f2 be FinSequence of REAL such that

       A7: f2 = (b2 * ( canFS S)) and

       A8: ( Sum b2) = ( Sum f2) by UPROOTS: 14, XBOOLE_1: 7;

      

       A9: ( rng ( canFS S)) = S by FUNCT_2:def 3;

      then

       A10: ( dom f1) = ( dom ( canFS S)) by A4, A5, RELAT_1: 27;

       A11:

      now

        let j be Nat;

        assume j in ( Seg ( len f1));

        then

         A12: j in ( dom f1) by FINSEQ_1:def 3;

        then

         A13: (( canFS S) . j) in S by A9, A10, FUNCT_1: 3;

        (f1 . j) = (b1 . (( canFS S) . j)) & (f2 . j) = (b2 . (( canFS S) . j)) by A5, A7, A10, A12, FUNCT_1: 13;

        hence (f1 . j) <= (f2 . j) by A1, A13;

      end;

      ( dom f2) = ( dom ( canFS S)) by A2, A7, A9, RELAT_1: 27;

      then

       A14: ( len f1) = ( len f2) by A10, FINSEQ_3: 29;

      f1 is Element of (( len f1) -tuples_on REAL ) & f2 is Element of (( len f2) -tuples_on REAL ) by FINSEQ_2: 92;

      hence thesis by A6, A8, A14, A11, RVSUM_1: 82;

    end;

    theorem :: GLIB_004:6

    for A be set, b1,b2 be Rbag of A st (for x be set st x in A holds (b1 . x) = (b2 . x)) holds ( Sum b1) = ( Sum b2)

    proof

      let A be set, b1,b2 be Rbag of A;

      assume

       A1: for x be set st x in A holds (b1 . x) = (b2 . x);

      then for x be set st x in A holds (b2 . x) <= (b1 . x);

      then

       A2: ( Sum b2) <= ( Sum b1) by Th5;

      for x be set st x in A holds (b1 . x) <= (b2 . x) by A1;

      then ( Sum b1) <= ( Sum b2) by Th5;

      hence thesis by A2, XXREAL_0: 1;

    end;

    theorem :: GLIB_004:7

    for A1,A2 be set, b1 be Rbag of A1, b2 be Rbag of A2 st b1 = b2 holds ( Sum b1) = ( Sum b2)

    proof

      let A1,A2 be set, b1 be Rbag of A1, b2 be Rbag of A2;

      assume b1 = b2;

      then ex f1 be FinSequence of REAL st ( Sum b1) = ( Sum f1) & f1 = (b2 * ( canFS ( support b2))) by UPROOTS:def 3;

      hence thesis by UPROOTS:def 3;

    end;

    theorem :: GLIB_004:8

    

     Th8: for X,x be set, b be Rbag of X, y be Real st b = (( EmptyBag X) +* (x .--> y)) holds ( Sum b) = y

    proof

      let X,x be set, b be Rbag of X, y be Real such that

       A1: b = (( EmptyBag X) +* (x .--> y));

      ( dom (x .--> y)) = {x} & ( dom b) = (( dom ( EmptyBag X)) \/ ( dom (x .--> y))) by A1, FUNCT_4:def 1;

      then

       A2: {x} c= ( dom b) by XBOOLE_1: 7;

      then

      reconsider S = {x} as finite Subset of X by PARTFUN1:def 2;

      ( support b) c= S

      proof

        let a be object;

        assume a in ( support b);

        then

         A3: (b . a) <> 0 by PRE_POLY:def 7;

        assume not a in S;

        then a <> x by TARSKI:def 1;

        then (b . a) = (( EmptyBag X) . a) by A1, FUNCT_4: 83;

        hence contradiction by A3, PBOOLE: 5;

      end;

      then

      consider f be FinSequence of REAL such that

       A4: f = (b * ( canFS S)) and

       A5: ( Sum b) = ( Sum f) by UPROOTS: 14;

      reconsider bx = (b . x) as Element of REAL by XREAL_0:def 1;

       {x} c= X by A2, PARTFUN1:def 2;

      then x in X by ZFMISC_1: 31;

      then ( canFS S) = <*x*> & x in ( dom b) by FINSEQ_1: 94, PARTFUN1:def 2;

      then f = <*bx*> by A4, FINSEQ_2: 34;

      

      hence ( Sum b) = (b . x) by A5, FINSOP_1: 11

      .= y by A1, FUNCT_7: 94;

    end;

    theorem :: GLIB_004:9

    for X,x be set, b1,b2 be Rbag of X, y be Real st b2 = (b1 +* (x .--> y)) holds ( Sum b2) = ((( Sum b1) + y) - (b1 . x))

    proof

      let X,x be set, b1,b2 be Rbag of X, y be Real such that

       A1: b2 = (b1 +* (x .--> y));

      ( dom (x .--> y)) = {x} & ( dom b2) = (( dom b1) \/ ( dom (x .--> y))) by A1, FUNCT_4:def 1;

      then {x} c= ( dom b2) by XBOOLE_1: 7;

      then {x} c= X by PARTFUN1:def 2;

      then

       A2: x in X by ZFMISC_1: 31;

      set c = (( EmptyBag X) +* (x .--> y));

      

       A3: ( dom c) = (( dom ( EmptyBag X)) \/ ( dom (x .--> y))) by FUNCT_4:def 1

      .= (X \/ ( dom (x .--> y))) by PARTFUN1:def 2

      .= (X \/ {x})

      .= X by A2, ZFMISC_1: 40;

      set a = (b1 +* (x .--> 0 ));

      

       A4: ( dom a) = (( dom b1) \/ ( dom (x .--> 0 ))) by FUNCT_4:def 1

      .= (X \/ ( dom (x .--> 0 ))) by PARTFUN1:def 2

      .= (X \/ {x})

      .= X by A2, ZFMISC_1: 40;

      set b = (( EmptyBag X) +* (x .--> (b1 . x)));

      

       A5: ( dom b) = (( dom ( EmptyBag X)) \/ ( dom (x .--> (b1 . x)))) by FUNCT_4:def 1

      .= (X \/ ( dom (x .--> (b1 . x)))) by PARTFUN1:def 2

      .= (X \/ {x})

      .= X by A2, ZFMISC_1: 40;

      ( support b) c= (( support ( EmptyBag X)) \/ {x}) by Th2;

      then

      reconsider b as Rbag of X by A5, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;

      ( support a) c= (( support b1) \/ {x}) by Th2;

      then

      reconsider a as Rbag of X by A4, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;

      ( support c) c= (( support ( EmptyBag X)) \/ {x}) by Th2;

      then

      reconsider c as Rbag of X by A3, PARTFUN1:def 2, PRE_POLY:def 8, RELAT_1:def 18;

      now

        let i be object;

        assume i in X;

        

         A6: (( EmptyBag X) . i) = 0 by PBOOLE: 5;

        per cases ;

          suppose

           A7: i = x;

          

          thus ((a + b) . i) = ((a . i) + (b . i)) by PRE_POLY:def 5

          .= ( 0 qua Nat + (b . i)) by A7, FUNCT_7: 94

          .= (b1 . i) by A7, FUNCT_7: 94;

        end;

          suppose

           A8: i <> x;

          

          thus ((a + b) . i) = ((a . i) + (b . i)) by PRE_POLY:def 5

          .= ((b1 . i) + (b . i)) by A8, FUNCT_4: 83

          .= ((b1 . i) + 0 qua Nat) by A6, A8, FUNCT_4: 83

          .= (b1 . i);

        end;

      end;

      then

       A9: (( Sum b1) - ( Sum b)) = ((( Sum a) + ( Sum b)) - ( Sum b)) by PBOOLE: 3, UPROOTS: 15;

      

       A10: ( Sum c) = y & ( Sum b) = (b1 . x) by Th8;

      now

        let i be object;

        assume i in X;

        

         A11: (( EmptyBag X) . i) = 0 by PBOOLE: 5;

        per cases ;

          suppose

           A12: i = x;

          

          hence (b2 . i) = y by A1, FUNCT_7: 94

          .= ( 0 qua Nat + (c . i)) by A12, FUNCT_7: 94

          .= ((a . i) + (c . i)) by A12, FUNCT_7: 94

          .= ((a + c) . i) by PRE_POLY:def 5;

        end;

          suppose

           A13: i <> x;

          then

           A14: (c . i) = 0 by A11, FUNCT_4: 83;

          

          thus (b2 . i) = (b1 . i) by A1, A13, FUNCT_4: 83

          .= ((a . i) + (c . i)) by A13, A14, FUNCT_4: 83

          .= ((a + c) . i) by PRE_POLY:def 5;

        end;

      end;

      

      hence ( Sum b2) = ((( Sum b1) - ( Sum b)) + ( Sum c)) by A9, PBOOLE: 3, UPROOTS: 15

      .= ((( Sum b1) + y) - (b1 . x)) by A10;

    end;

    begin

    definition

      let G1 be real-weighted WGraph, G2 be WSubgraph of G1, v be set;

      :: GLIB_004:def1

      pred G2 is_mincost_DTree_rooted_at v means G2 is Tree-like & for x be Vertex of G2 holds ex W2 be DPath of G2 st W2 is_Walk_from (v,x) & for W1 be DPath of G1 st W1 is_Walk_from (v,x) holds (W2 .cost() ) <= (W1 .cost() );

    end

    definition

      let G be real-weighted WGraph, W be DPath of G, x,y be set;

      :: GLIB_004:def2

      pred W is_mincost_DPath_from x,y means W is_Walk_from (x,y) & for W2 be DPath of G st W2 is_Walk_from (x,y) holds (W .cost() ) <= (W2 .cost() );

    end

    definition

      let G be _finite real-weighted WGraph, x,y be set;

      :: GLIB_004:def3

      func G .min_DPath_cost (x,y) -> Real means

      : Def3: ex W be DPath of G st W is_mincost_DPath_from (x,y) & it = (W .cost() ) if ex W be DWalk of G st W is_Walk_from (x,y)

      otherwise it = 0 ;

      existence

      proof

        set X = { W where W be DPath of G : W is_Walk_from (x,y) };

        now

          let e be object;

          assume e in X;

          then ex W be DPath of G st e = W & W is_Walk_from (x,y);

          then e in the set of all w where w be DPath of G;

          hence e in (G .allDPaths() ) by GLIB_001:def 38;

        end;

        then

        reconsider X as finite Subset of (G .allDPaths() ) by TARSKI:def 3;

        hereby

          assume ex W be DWalk of G st W is_Walk_from (x,y);

          then

          consider W be DWalk of G such that

           A1: W is_Walk_from (x,y);

          set P = the DPath of W;

          P is_Walk_from (x,y) by A1, GLIB_001: 160;

          then P in X;

          then

          reconsider X as non empty finite Subset of (G .allDPaths() );

          deffunc F( Element of X) = ($1 .cost() );

          consider W1 be Element of X such that

           A2: for W2 be Element of X holds F(W1) <= F(W2) from PRE_CIRC:sch 5;

          W1 in X;

          then

          consider WA be DPath of G such that

           A3: WA = W1 and

           A4: WA is_Walk_from (x,y);

           A5:

          now

            let WB be DPath of G;

            assume WB is_Walk_from (x,y);

            then WB in X;

            then

            reconsider WB9 = WB as Element of X;

             F(W1) <= F(WB9) by A2;

            hence (WA .cost() ) <= (WB .cost() ) by A3;

          end;

          reconsider WA as DPath of G;

          set IT = (WA .cost() );

          take IT, WA;

          thus WA is_mincost_DPath_from (x,y) by A4, A5;

          thus IT = (WA .cost() );

        end;

        thus thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be Real;

        hereby

          assume ex W be DWalk of G st W is_Walk_from (x,y);

          given W1 be DPath of G such that

           A6: W1 is_mincost_DPath_from (x,y) and

           A7: IT1 = (W1 .cost() );

          given W2 be DPath of G such that

           A8: W2 is_mincost_DPath_from (x,y) and

           A9: IT2 = (W2 .cost() );

          W2 is_Walk_from (x,y) by A8;

          then

           A10: IT1 <= IT2 by A6, A7, A9;

          W1 is_Walk_from (x,y) by A6;

          then IT2 <= IT1 by A7, A8, A9;

          hence IT1 = IT2 by A10, XXREAL_0: 1;

        end;

        thus thesis;

      end;

      consistency ;

    end

    definition

      :: GLIB_004:def4

      func WGraphSelectors -> non empty finite Subset of NAT equals { VertexSelector , EdgeSelector , SourceSelector , TargetSelector , WeightSelector };

      coherence ;

    end

    

     Lm3: for G be WGraph holds WGraphSelectors c= ( dom G)

    proof

      let G be WGraph;

      let x be object;

      assume x in WGraphSelectors ;

      then x = VertexSelector or x = EdgeSelector or x = SourceSelector or x = TargetSelector or x = WeightSelector by ENUMSET1:def 3;

      hence x in ( dom G) by GLIB_000:def 10, GLIB_003:def 4;

    end;

    registration

      let G be WGraph;

      cluster (G | WGraphSelectors ) -> [Graph-like] [Weighted];

      coherence

      proof

        set G2 = (G | WGraphSelectors );

        

         A1: VertexSelector in WGraphSelectors by ENUMSET1:def 3;

        

         A2: TargetSelector in WGraphSelectors by ENUMSET1:def 3;

        then

         A3: ( the_Target_of G2) = ( the_Target_of G) by FUNCT_1: 49;

        

         A4: SourceSelector in WGraphSelectors by ENUMSET1:def 3;

        then

         A5: ( the_Source_of G2) = ( the_Source_of G) by FUNCT_1: 49;

        

         A6: EdgeSelector in WGraphSelectors by ENUMSET1:def 3;

        then

         A7: ( the_Edges_of G2) = ( the_Edges_of G) by FUNCT_1: 49;

        

         A8: ( dom G2) = (( dom G) /\ WGraphSelectors ) by RELAT_1: 61

        .= WGraphSelectors by Lm3, XBOOLE_1: 28;

        then for x be object st x in _GraphSelectors holds x in ( dom G2) by A1, A6, A4, A2, ENUMSET1:def 2;

        then

         A9: _GraphSelectors c= ( dom G2);

        ( the_Vertices_of G2) = ( the_Vertices_of G) by A1, FUNCT_1: 49;

        hence G2 is [Graph-like] by A7, A5, A3, A9, GLIB_000: 5;

        

         A10: WeightSelector in WGraphSelectors by ENUMSET1:def 3;

        then (G2 . WeightSelector ) = (G . WeightSelector ) by FUNCT_1: 49;

        then (G2 . WeightSelector ) is ManySortedSet of ( the_Edges_of G2) by A7, GLIB_003:def 4;

        hence thesis by A8, A10;

      end;

    end

    

     Lm4: for G be WGraph holds G == (G | WGraphSelectors ) & ( the_Weight_of G) = ( the_Weight_of (G | WGraphSelectors ))

    proof

      let G be WGraph;

      set G2 = (G | WGraphSelectors );

       EdgeSelector in WGraphSelectors by ENUMSET1:def 3;

      then

       A1: ( the_Edges_of G2) = ( the_Edges_of G) by FUNCT_1: 49;

       SourceSelector in WGraphSelectors by ENUMSET1:def 3;

      then

       A2: ( the_Source_of G2) = ( the_Source_of G) by FUNCT_1: 49;

       TargetSelector in WGraphSelectors by ENUMSET1:def 3;

      then

       A3: ( the_Target_of G2) = ( the_Target_of G) by FUNCT_1: 49;

       VertexSelector in WGraphSelectors by ENUMSET1:def 3;

      then ( the_Vertices_of G2) = ( the_Vertices_of G) by FUNCT_1: 49;

      hence G == G2 by A1, A2, A3;

       WeightSelector in WGraphSelectors by ENUMSET1:def 3;

      hence thesis by FUNCT_1: 49;

    end;

    

     Lm5: for G be WGraph holds ( dom (G | WGraphSelectors )) = WGraphSelectors

    proof

      let G be WGraph;

       WGraphSelectors c= ( dom G) by Lm3;

      hence thesis by RELAT_1: 62;

    end;

    definition

      let G be WGraph;

      :: GLIB_004:def5

      func G .allWSubgraphs() -> non empty set means

      : Def5: for x be set holds x in it iff ex G2 be WSubgraph of G st x = G2 & ( dom G2) = WGraphSelectors ;

      existence

      proof

        set G9 = (G | WGraphSelectors );

        

         A1: G == G9 by Lm4;

        

         A2: ( the_Weight_of G) = ( the_Weight_of G9) by Lm4;

        reconsider G9 as [Weighted] Subgraph of G by A1, GLIB_000: 87;

        ( the_Weight_of G9) = (( the_Weight_of G) | ( the_Edges_of G9)) by A2;

        then

        reconsider G9 as WSubgraph of G by GLIB_003:def 10;

        set Z = {( bool ( the_Vertices_of G)), ( bool ( the_Edges_of G)), ( bool ( the_Source_of G)), ( bool ( the_Target_of G)), ( bool ( the_Weight_of G))};

        set Y = ( union Z);

        set X = ( Funcs ( WGraphSelectors ,Y));

        defpred P[ set] means $1 is WSubgraph of G;

        consider IT be Subset of X such that

         A3: for x be set holds x in IT iff x in X & P[x] from SUBSET_1:sch 1;

         A4:

        now

          let G2 be WSubgraph of G;

          assume

           A5: ( dom G2) = WGraphSelectors ;

          now

            let y be object;

            assume y in ( rng G2);

            then

            consider x be object such that

             A6: x in WGraphSelectors and

             A7: (G2 . x) = y by A5, FUNCT_1:def 3;

            now

              per cases by A6, ENUMSET1:def 3;

                suppose

                 A8: x = VertexSelector ;

                

                 A9: ( bool ( the_Vertices_of G)) in Z by ENUMSET1:def 3;

                y = ( the_Vertices_of G2) by A7, A8;

                hence y in Y by A9, TARSKI:def 4;

              end;

                suppose

                 A10: x = EdgeSelector ;

                

                 A11: ( bool ( the_Edges_of G)) in Z by ENUMSET1:def 3;

                y = ( the_Edges_of G2) by A7, A10;

                hence y in Y by A11, TARSKI:def 4;

              end;

                suppose x = SourceSelector ;

                then y = ( the_Source_of G2) by A7;

                then y = (( the_Source_of G) | ( the_Edges_of G2)) by GLIB_000: 45;

                then

                 A12: (G2 . x) c= ( the_Source_of G) by RELAT_1: 59, A7;

                ( bool ( the_Source_of G)) in Z by ENUMSET1:def 3;

                hence y in Y by A12, TARSKI:def 4, A7;

              end;

                suppose x = TargetSelector ;

                then y = ( the_Target_of G2) by A7;

                then y = (( the_Target_of G) | ( the_Edges_of G2)) by GLIB_000: 45;

                then

                 A13: (G2 . x) c= ( the_Target_of G) by RELAT_1: 59, A7;

                ( bool ( the_Target_of G)) in Z by ENUMSET1:def 3;

                hence y in Y by A13, TARSKI:def 4, A7;

              end;

                suppose x = WeightSelector ;

                then y = ( the_Weight_of G2) by A7;

                then y = (( the_Weight_of G) | ( the_Edges_of G2)) by GLIB_003:def 10;

                then

                 A14: (G2 . x) c= ( the_Weight_of G) by RELAT_1: 59, A7;

                ( bool ( the_Weight_of G)) in Z by ENUMSET1:def 3;

                hence y in Y by A14, TARSKI:def 4, A7;

              end;

            end;

            hence y in Y;

          end;

          hence ( rng G2) c= Y;

        end;

        

         A15: ( dom G9) = WGraphSelectors by Lm5;

        then ( rng G9) c= Y by A4;

        then G9 in X by A15, FUNCT_2:def 2;

        then

        reconsider IT as non empty set by A3;

        take IT;

        let x be set;

        hereby

          assume

           A16: x in IT;

          then

          reconsider x9 = x as WSubgraph of G by A3;

          take x9;

          thus x9 = x;

          ex f be Function st f = x & ( dom f) = WGraphSelectors & ( rng f) c= Y by A16, FUNCT_2:def 2;

          hence ( dom x9) = WGraphSelectors ;

        end;

        given G2 be WSubgraph of G such that

         A17: G2 = x and

         A18: ( dom G2) = WGraphSelectors ;

        ( rng G2) c= Y by A4, A18;

        then x in X by A17, A18, FUNCT_2:def 2;

        hence thesis by A3, A17;

      end;

      uniqueness

      proof

        let IT1,IT2 be non empty set such that

         A19: for x be set holds x in IT1 iff ex G2 be WSubgraph of G st x = G2 & ( dom G2) = WGraphSelectors and

         A20: for x be set holds x in IT2 iff ex G2 be WSubgraph of G st x = G2 & ( dom G2) = WGraphSelectors ;

        now

          let x be object;

          x in IT1 iff ex G2 be WSubgraph of G st x = G2 & ( dom G2) = WGraphSelectors by A19;

          hence x in IT1 iff x in IT2 by A20;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    registration

      let G be _finite WGraph;

      cluster (G .allWSubgraphs() ) -> finite;

      coherence

      proof

        set Z = {( bool ( the_Vertices_of G)), ( bool ( the_Edges_of G)), ( bool ( the_Source_of G)), ( bool ( the_Target_of G)), ( bool ( the_Weight_of G))}, Y = ( union Z);

        for x be set st x in Z holds x is finite by ENUMSET1:def 3;

        then

        reconsider Y as finite set by FINSET_1: 7;

        set X = ( Funcs ( WGraphSelectors ,Y));

        now

          let x be object;

          assume x in (G .allWSubgraphs() );

          then

          consider G2 be WSubgraph of G such that

           A1: x = G2 and

           A2: ( dom G2) = WGraphSelectors by Def5;

          now

            let y be object;

            assume y in ( rng G2);

            then

            consider x be object such that

             A3: x in WGraphSelectors and

             A4: (G2 . x) = y by A2, FUNCT_1:def 3;

            now

              per cases by A3, ENUMSET1:def 3;

                suppose

                 A5: x = VertexSelector ;

                

                 A6: ( bool ( the_Vertices_of G)) in Z by ENUMSET1:def 3;

                y = ( the_Vertices_of G2) by A4, A5;

                hence y in Y by A6, TARSKI:def 4;

              end;

                suppose

                 A7: x = EdgeSelector ;

                

                 A8: ( bool ( the_Edges_of G)) in Z by ENUMSET1:def 3;

                y = ( the_Edges_of G2) by A4, A7;

                hence y in Y by A8, TARSKI:def 4;

              end;

                suppose x = SourceSelector ;

                then y = ( the_Source_of G2) by A4;

                then y = (( the_Source_of G) | ( the_Edges_of G2)) by GLIB_000: 45;

                then

                 A9: (G2 . x) c= ( the_Source_of G) by RELAT_1: 59, A4;

                ( bool ( the_Source_of G)) in Z by ENUMSET1:def 3;

                hence y in Y by A9, TARSKI:def 4, A4;

              end;

                suppose x = TargetSelector ;

                then y = ( the_Target_of G2) by A4;

                then y = (( the_Target_of G) | ( the_Edges_of G2)) by GLIB_000: 45;

                then

                 A10: (G2 . x) c= ( the_Target_of G) by RELAT_1: 59, A4;

                ( bool ( the_Target_of G)) in Z by ENUMSET1:def 3;

                hence y in Y by A10, TARSKI:def 4, A4;

              end;

                suppose x = WeightSelector ;

                then y = ( the_Weight_of G2) by A4;

                then y = (( the_Weight_of G) | ( the_Edges_of G2)) by GLIB_003:def 10;

                then

                 A11: (G2 . x) c= ( the_Weight_of G) by RELAT_1: 59, A4;

                ( bool ( the_Weight_of G)) in Z by ENUMSET1:def 3;

                hence y in Y by A11, TARSKI:def 4, A4;

              end;

            end;

            hence y in Y;

          end;

          then ( rng G2) c= Y;

          hence x in X by A1, A2, FUNCT_2:def 2;

        end;

        then (G .allWSubgraphs() ) c= X;

        hence thesis;

      end;

    end

    definition

      let G be WGraph, X be non empty Subset of (G .allWSubgraphs() );

      :: original: Element

      redefine

      mode Element of X -> WSubgraph of G ;

      coherence

      proof

        let x be Element of X;

        ex G2 be WSubgraph of G st G2 = x & ( dom G2) = WGraphSelectors by Def5;

        hence thesis;

      end;

    end

    definition

      let G be _finite real-weighted WGraph;

      :: GLIB_004:def6

      func G .cost() -> Real equals ( Sum ( the_Weight_of G));

      coherence ;

    end

    theorem :: GLIB_004:10

    

     Th10: for G1 be _finite real-weighted WGraph, e be set, G2 be weight-inheriting [Weighted] removeEdge of G1, e st e in ( the_Edges_of G1) holds (G1 .cost() ) = ((G2 .cost() ) + (( the_Weight_of G1) . e))

    proof

      let G1 be _finite real-weighted WGraph, e be set, G2 be weight-inheriting [Weighted] removeEdge of G1, e;

      set EG1 = ( the_Edges_of G1), EG2 = ( the_Edges_of G2);

      assume

       A1: e in EG1;

      

       A2: ( dom ( the_Weight_of G1)) = EG1 by PARTFUN1:def 2;

      set b2 = (e .--> (( the_Weight_of G1) . e));

      

       A3: ( dom b2) = {e};

      

       A4: EG2 = (EG1 \ {e}) by GLIB_000: 51;

      

      then (EG1 \ EG2) = (EG1 /\ {e}) by XBOOLE_1: 48

      .= {e} by A1, ZFMISC_1: 46;

      then

      reconsider b2 as ManySortedSet of (EG1 \ EG2);

      reconsider b2 as Rbag of (EG1 \ EG2);

      

       A5: ( the_Weight_of G2) = (( the_Weight_of G1) | EG2) by GLIB_003:def 10;

       A6:

      now

        let x be object;

        assume x in ( dom ( the_Weight_of G1));

        then

         A7: x in EG1;

        now

          per cases ;

            suppose

             A8: x in {e};

            then

             A9: x = e by TARSKI:def 1;

            

            hence ((( the_Weight_of G2) +* b2) . x) = (b2 . e) by A3, A8, FUNCT_4: 13

            .= (( the_Weight_of G1) . x) by A9, FUNCOP_1: 72;

          end;

            suppose not x in {e};

            then ((( the_Weight_of G2) +* b2) . x) = (( the_Weight_of G2) . x) & x in (EG1 \ {e}) by A3, A7, FUNCT_4: 11, XBOOLE_0:def 5;

            hence ((( the_Weight_of G2) +* b2) . x) = (( the_Weight_of G1) . x) by A4, A5, FUNCT_1: 49;

          end;

        end;

        hence (( the_Weight_of G1) . x) = ((( the_Weight_of G2) +* b2) . x);

      end;

      ( dom (( the_Weight_of G2) +* b2)) = (( dom ( the_Weight_of G2)) \/ {e}) by A3, FUNCT_4:def 1

      .= ((EG1 \ {e}) \/ {e}) by A4, PARTFUN1:def 2

      .= (EG1 \/ {e}) by XBOOLE_1: 39

      .= EG1 by A1, ZFMISC_1: 40;

      

      hence (G1 .cost() ) = ((G2 .cost() ) + ( Sum b2)) by A2, A6, Th3, FUNCT_1: 2

      .= ((G2 .cost() ) + (b2 . e)) by A3, Th4

      .= ((G2 .cost() ) + (( the_Weight_of G1) . e)) by FUNCOP_1: 72;

    end;

    theorem :: GLIB_004:11

    

     Th11: for G be _finite real-weighted WGraph, V1 be non empty Subset of ( the_Vertices_of G), E1 be Subset of (G .edgesBetween V1), G1 be inducedWSubgraph of G, V1, E1, e be set, G2 be inducedWSubgraph of G, V1, (E1 \/ {e}) st not e in E1 & e in (G .edgesBetween V1) holds ((G1 .cost() ) + (( the_Weight_of G) . e)) = (G2 .cost() )

    proof

      let G be _finite real-weighted WGraph, V1 be non empty Subset of ( the_Vertices_of G), E1 be Subset of (G .edgesBetween V1), G1 be inducedWSubgraph of G, V1, E1, e be set, G2 be inducedWSubgraph of G, V1, (E1 \/ {e});

      assume that

       A1: not e in E1 and

       A2: e in (G .edgesBetween V1);

       {e} c= (G .edgesBetween V1) by A2, ZFMISC_1: 31;

      then (E1 \/ {e}) c= (G .edgesBetween V1) by XBOOLE_1: 8;

      then

       A3: ( the_Edges_of G2) = (E1 \/ {e}) by GLIB_000:def 37;

      then

       A4: ( dom ( the_Weight_of G2)) = (E1 \/ {e}) by PARTFUN1:def 2;

      set W2 = (e .--> (( the_Weight_of G) . e));

      

       A6: ( the_Edges_of G1) = E1 by GLIB_000:def 37;

      

      then (( the_Edges_of G2) \ ( the_Edges_of G1)) = ( {e} \ E1) by A3, XBOOLE_1: 40

      .= {e} by A1, ZFMISC_1: 59;

      then

      reconsider W2 as ManySortedSet of (( the_Edges_of G2) \ ( the_Edges_of G1));

      reconsider W2 as Rbag of (( the_Edges_of G2) \ ( the_Edges_of G1));

      

       A7: ( the_Weight_of G1) = (( the_Weight_of G) | E1) by A6, GLIB_003:def 10;

       A8:

      now

        let x be object;

        assume x in ( dom ( the_Weight_of G2));

        then

         A9: x in (E1 \/ {e}) by A3;

        ( the_Weight_of G2) = (( the_Weight_of G) | (E1 \/ {e})) by A3, GLIB_003:def 10;

        then

         A10: (( the_Weight_of G2) . x) = (( the_Weight_of G) . x) by A9, FUNCT_1: 49;

        now

          per cases ;

            suppose not x in ( dom W2);

            then ((( the_Weight_of G1) +* W2) . x) = (( the_Weight_of G1) . x) & x in E1 by A9, FUNCT_4: 11, XBOOLE_0:def 3;

            hence ((( the_Weight_of G1) +* W2) . x) = (( the_Weight_of G2) . x) by A7, A10, FUNCT_1: 49;

          end;

            suppose

             A11: x in ( dom W2);

            then

             A12: x = e by TARSKI:def 1;

            ((( the_Weight_of G1) +* W2) . x) = (W2 . x) by A11, FUNCT_4: 13

            .= (( the_Weight_of G) . e) by A12, FUNCOP_1: 72;

            hence ((( the_Weight_of G1) +* W2) . x) = (( the_Weight_of G2) . x) by A10, A11, TARSKI:def 1;

          end;

        end;

        hence (( the_Weight_of G2) . x) = ((( the_Weight_of G1) +* W2) . x);

      end;

      ( dom W2) = {e};

      

      then

       A13: ( Sum W2) = (W2 . e) by Th4

      .= (( the_Weight_of G) . e) by FUNCOP_1: 72;

      ( dom (( the_Weight_of G1) +* W2)) = (( dom ( the_Weight_of G1)) \/ ( dom W2)) by FUNCT_4:def 1

      .= (E1 \/ {e}) by A6, PARTFUN1:def 2;

      hence thesis by A4, A8, A13, Th3, FUNCT_1: 2;

    end;

    theorem :: GLIB_004:12

    

     Th12: for G be _finite nonnegative-weighted WGraph, W be DPath of G, x,y be set, m,n be Element of NAT st W is_mincost_DPath_from (x,y) holds (W .cut (m,n)) is_mincost_DPath_from (((W .cut (m,n)) .first() ),((W .cut (m,n)) .last() ))

    proof

      let G be _finite nonnegative-weighted WGraph, W be DPath of G, x,y be set, m,n be Element of NAT ;

      set WC = (W .cut (m,n));

      

       A1: WC is_Walk_from ((WC .first() ),(WC .last() )) by GLIB_001:def 23;

      assume

       A2: W is_mincost_DPath_from (x,y);

      then

       A3: W is_Walk_from (x,y);

      then

       A4: (W . 1) = x & (W . ( len W)) = y by GLIB_001: 17;

      now

        per cases ;

          suppose

           A5: m is odd & n is odd & m <= n & n <= ( len W);

          set W1 = (W .cut (1,m)), W3 = (W .cut (n,( len W)));

          

           A6: 1 <= n by A5, ABIAN: 12;

          

          then

           A7: ((W .cut (1,n)) .append W3) = (W .cut (1,( len W))) by A5, GLIB_001: 38, JORDAN12: 2

          .= W by GLIB_001: 39;

          ((W .cut (1,n)) .last() ) = (W . n) by A5, A6, GLIB_001: 37, JORDAN12: 2

          .= (W3 .first() ) by A5, GLIB_001: 37;

          then

           A8: (W .cost() ) = (((W .cut (1,n)) .cost() ) + (W3 .cost() )) by A7, GLIB_003: 24;

          

           A9: 1 <= m by A5, ABIAN: 12;

          then

           A10: (W1 .append WC) = (W .cut (1,n)) by A5, GLIB_001: 38, JORDAN12: 2;

          

           A11: m <= ( len W) by A5, XXREAL_0: 2;

          

          then (W1 .last() ) = (W . m) by A5, A9, GLIB_001: 37, JORDAN12: 2

          .= (WC .first() ) by A5, GLIB_001: 37;

          then ((W .cut (1,n)) .cost() ) = ((W1 .cost() ) + (WC .cost() )) by A10, GLIB_003: 24;

          then

           A12: (W .cost() ) = ((WC .cost() ) + ((W1 .cost() ) + (W3 .cost() ))) by A8;

          

           A13: W3 is_Walk_from ((W . n),(W . ( len W))) by A5, GLIB_001: 37;

          

           A14: W1 is_Walk_from ((W . 1),(W . m)) by A5, A9, A11, GLIB_001: 37, JORDAN12: 2;

          now

            assume not WC is_mincost_DPath_from ((WC .first() ),(WC .last() ));

            then

            consider W2 be DPath of G such that

             A15: W2 is_Walk_from ((WC .first() ),(WC .last() )) and

             A16: (W2 .cost() ) < (WC .cost() ) by A1;

            set WA = (W1 .append W2), WB = (WA .append W3);

            set WB2 = the DPath of WB;

            

             A17: (WC .last() ) = (W . n) by A5, GLIB_001: 37;

            

             A18: (WC .first() ) = (W . m) by A5, GLIB_001: 37;

            then WA is_Walk_from ((W . 1),(W . n)) by A14, A15, A17, GLIB_001: 31;

            then WB is_Walk_from (x,y) by A4, A13, GLIB_001: 31;

            then

             A19: WB2 is_Walk_from (x,y) by GLIB_001: 160;

            (W2 .first() ) = (W . m) by A15, A18, GLIB_001:def 23;

            then

             A20: (W1 .last() ) = (W2 .first() ) by A5, A9, A11, GLIB_001: 37, JORDAN12: 2;

            then

             A21: (WA .cost() ) = ((W1 .cost() ) + (W2 .cost() )) by GLIB_003: 24;

            (W2 .last() ) = (W . n) by A15, A17, GLIB_001:def 23;

            

            then (W3 .first() ) = (W2 .last() ) by A5, GLIB_001: 37

            .= (WA .last() ) by A20, GLIB_001: 30;

            

            then (WB .cost() ) = (((W1 .cost() ) + (W2 .cost() )) + (W3 .cost() )) by A21, GLIB_003: 24

            .= ((W2 .cost() ) + ((W1 .cost() ) + (W3 .cost() )));

            then

             A22: (WB .cost() ) < (W .cost() ) by A12, A16, XREAL_1: 8;

            (WB2 .cost() ) <= (WB .cost() ) by GLIB_003: 30;

            then (WB2 .cost() ) < (W .cost() ) by A22, XXREAL_0: 2;

            hence contradiction by A2, A19;

          end;

          hence thesis;

        end;

          suppose not (m is odd & n is odd & m <= n & n <= ( len W));

          then

           A23: WC = W by GLIB_001:def 11;

          then (WC .first() ) = x by A3, GLIB_001:def 23;

          hence thesis by A2, A23, GLIB_001:def 23;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_004:13

    for G be _finite real-weighted WGraph, W1,W2 be DPath of G, x,y be set st W1 is_mincost_DPath_from (x,y) & W2 is_mincost_DPath_from (x,y) holds (W1 .cost() ) = (W2 .cost() )

    proof

      let G be _finite real-weighted WGraph, W1,W2 be DPath of G, x,y be set;

      assume that

       A1: W1 is_mincost_DPath_from (x,y) and

       A2: W2 is_mincost_DPath_from (x,y);

      W2 is_Walk_from (x,y) by A2;

      then

       A3: (W1 .cost() ) <= (W2 .cost() ) by A1;

      W1 is_Walk_from (x,y) by A1;

      then (W2 .cost() ) <= (W1 .cost() ) by A2;

      hence thesis by A3, XXREAL_0: 1;

    end;

    theorem :: GLIB_004:14

    

     Th14: for G be _finite real-weighted WGraph, W be DPath of G, x,y be set st W is_mincost_DPath_from (x,y) holds (G .min_DPath_cost (x,y)) = (W .cost() ) by Def3;

    begin

    definition

      let G be _Graph;

      mode DIJK:Labeling of G is Element of [:( PFuncs (( the_Vertices_of G), REAL )), ( bool ( the_Edges_of G)):];

    end

    definition

      let X1,X3 be set, X2 be non empty set;

      let x be Element of [:( PFuncs (X1,X3)), X2:];

      :: original: `1

      redefine

      func x `1 -> Element of ( PFuncs (X1,X3)) ;

      coherence by MCART_1: 10;

    end

    registration

      let G be _finite _Graph, L be DIJK:Labeling of G;

      cluster (L `1 ) -> finite;

      coherence

      proof

        ( dom (L `1 )) c= ( the_Vertices_of G);

        hence thesis by FINSET_1: 10;

      end;

      cluster (L `2 ) -> finite;

      coherence ;

    end

    definition

      let G be real-weighted WGraph, L be DIJK:Labeling of G;

      :: GLIB_004:def7

      func DIJK:NextBestEdges (L) -> Subset of ( the_Edges_of G) means

      : Def7: for e1 be set holds e1 in it iff e1 DSJoins (( dom (L `1 )),(( the_Vertices_of G) \ ( dom (L `1 ))),G) & for e2 be set st e2 DSJoins (( dom (L `1 )),(( the_Vertices_of G) \ ( dom (L `1 ))),G) holds (((L `1 ) . (( the_Source_of G) . e1)) + (( the_Weight_of G) . e1)) <= (((L `1 ) . (( the_Source_of G) . e2)) + (( the_Weight_of G) . e2));

      existence

      proof

        defpred P[ set] means $1 DSJoins (( dom (L `1 )),(( the_Vertices_of G) \ ( dom (L `1 ))),G) & for e2 be set st e2 DSJoins (( dom (L `1 )),(( the_Vertices_of G) \ ( dom (L `1 ))),G) holds (((L `1 ) . (( the_Source_of G) . $1)) + (( the_Weight_of G) . $1)) <= (((L `1 ) . (( the_Source_of G) . e2)) + (( the_Weight_of G) . e2));

        consider IT be Subset of ( the_Edges_of G) such that

         A1: for e be set holds e in IT iff e in ( the_Edges_of G) & P[e] from SUBSET_1:sch 1;

        take IT;

        now

          let e1 be set;

          thus e1 in IT implies P[e1] by A1;

          assume

           A2: P[e1];

          then e1 in ( the_Edges_of G) by GLIB_000:def 16;

          hence e1 in IT by A1, A2;

        end;

        hence thesis;

      end;

      uniqueness

      proof

        defpred P[ set] means $1 DSJoins (( dom (L `1 )),(( the_Vertices_of G) \ ( dom (L `1 ))),G) & for e2 be set st e2 DSJoins (( dom (L `1 )),(( the_Vertices_of G) \ ( dom (L `1 ))),G) holds (((L `1 ) . (( the_Source_of G) . $1)) + (( the_Weight_of G) . $1)) <= (((L `1 ) . (( the_Source_of G) . e2)) + (( the_Weight_of G) . e2));

        let IT1,IT2 be Subset of ( the_Edges_of G) such that

         A3: for y be set holds y in IT1 iff P[y] and

         A4: for y be set holds y in IT2 iff P[y];

        now

          let x be object;

          reconsider xx = x as set by TARSKI: 1;

          hereby

            assume x in IT1;

            then P[xx] by A3;

            hence x in IT2 by A4;

          end;

          assume x in IT2;

          then P[xx] by A4;

          hence x in IT1 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let G be real-weighted WGraph, L be DIJK:Labeling of G;

      :: GLIB_004:def8

      func DIJK:Step (L) -> DIJK:Labeling of G equals

      : Def8: L if ( DIJK:NextBestEdges L) = {}

      otherwise [((L `1 ) +* ((( the_Target_of G) . the Element of ( DIJK:NextBestEdges L)) .--> (((L `1 ) . (( the_Source_of G) . the Element of ( DIJK:NextBestEdges L))) + (( the_Weight_of G) . the Element of ( DIJK:NextBestEdges L))))), ((L `2 ) \/ { the Element of ( DIJK:NextBestEdges L)})];

      coherence

      proof

        set V = ( the_Vertices_of G), E = ( the_Edges_of G);

        set BE = ( DIJK:NextBestEdges L), e = the Element of BE;

        set nE = ((L `2 ) \/ {e});

        set s = (( the_Source_of G) . e), t = (( the_Target_of G) . e);

        set val = (((L `1 ) . s) + (( the_Weight_of G) . e));

        now

          assume

           A1: BE <> {} ;

          then e in BE;

          then

          reconsider e9 = e as Element of E;

          

           A2: e in BE by A1;

          then

          reconsider t9 = t as Element of V by FUNCT_2: 5;

          (L `2 ) in ( bool E) & {e9} c= E by A2, ZFMISC_1: 31;

          then

           A3: nE c= E by XBOOLE_1: 8;

           {t9} c= V & ( dom ((L `1 ) +* (t .--> val))) = (( dom (L `1 )) \/ {t}) by Lm1;

          then

           A4: ( dom ((L `1 ) +* (t .--> val))) c= V by XBOOLE_1: 8;

          ( rng ((L `1 ) +* (t .--> val))) c= REAL ;

          then ((L `1 ) +* (t .--> val)) in ( PFuncs (V, REAL )) by A4, PARTFUN1:def 3;

          hence [((L `1 ) +* (t .--> val)), nE] is DIJK:Labeling of G by A3, ZFMISC_1:def 2;

        end;

        hence thesis;

      end;

      consistency ;

    end

    definition

      let G be real-weighted WGraph, src be Vertex of G;

      :: GLIB_004:def9

      func DIJK:Init (src) -> DIJK:Labeling of G equals [(src .--> 0 ), {} ];

      coherence

      proof

        set f = (src .--> 0 );

        ( dom f) = {src} & ( rng f) = { 0 } by FUNCOP_1: 8;

        then

         A1: f in ( PFuncs (( the_Vertices_of G), REAL )) by PARTFUN1:def 3;

         {} c= ( the_Edges_of G);

        hence thesis by A1, ZFMISC_1:def 2;

      end;

    end

    definition

      let G be real-weighted WGraph;

      :: GLIB_004:def10

      mode DIJK:LabelingSeq of G -> ManySortedSet of NAT means

      : Def10: for n be Nat holds (it . n) is DIJK:Labeling of G;

      existence

      proof

        defpred P[ object, object] means $2 is DIJK:Labeling of G;

         A1:

        now

          let i be object;

          assume i in NAT ;

          reconsider r = [ {} , {} ] as object;

          take r;

           {} is PartFunc of ( the_Vertices_of G), REAL by RELSET_1: 12;

          then

           A2: {} in ( PFuncs (( the_Vertices_of G), REAL )) by PARTFUN1: 45;

           {} c= ( the_Edges_of G);

          hence P[i, r] by A2, ZFMISC_1:def 2;

        end;

        consider s be ManySortedSet of NAT such that

         A3: for i be object st i in NAT holds P[i, (s . i)] from PBOOLE:sch 3( A1);

        take s;

        let i be Nat;

        i in NAT by ORDINAL1:def 12;

        hence thesis by A3;

      end;

    end

    definition

      let G be real-weighted WGraph, S be DIJK:LabelingSeq of G, n be Nat;

      :: original: .

      redefine

      func S . n -> DIJK:Labeling of G ;

      coherence by Def10;

    end

    definition

      let G be real-weighted WGraph, src be Vertex of G;

      :: GLIB_004:def11

      func DIJK:CompSeq (src) -> DIJK:LabelingSeq of G means

      : Def11: (it . 0 ) = ( DIJK:Init src) & for n be Nat holds (it . (n + 1)) = ( DIJK:Step (it . n));

      existence

      proof

        defpred P[ set, set, set] means ($2 is DIJK:Labeling of G & ex Gn,Gn1 be DIJK:Labeling of G st $2 = Gn & $3 = Gn1 & Gn1 = ( DIJK:Step Gn)) or ( not $2 is DIJK:Labeling of G & $2 = $3);

        now

          let n be Nat, x be set;

          now

            per cases ;

              suppose x is DIJK:Labeling of G;

              then

              reconsider Gn = x as DIJK:Labeling of G;

               P[n, x, ( DIJK:Step Gn)];

              hence ex y be set st P[n, x, y];

            end;

              suppose not x is DIJK:Labeling of G;

              hence ex y be set st P[n, x, y];

            end;

          end;

          hence ex y be set st P[n, x, y];

        end;

        then

         A1: for n be Nat holds for x be set holds ex y be set st P[n, x, y];

        consider IT be Function such that

         A2: ( dom IT) = NAT & (IT . 0 ) = ( DIJK:Init src) & for n be Nat holds P[n, (IT . n), (IT . (n + 1))] from RECDEF_1:sch 1( A1);

        reconsider IT as ManySortedSet of NAT by A2, PARTFUN1:def 2, RELAT_1:def 18;

        defpred P2[ Nat] means (IT . $1) is DIJK:Labeling of G;

         A3:

        now

          let n be Nat;

          assume

           A4: P2[n];

          ex Gn,Gn1 be DIJK:Labeling of G st (IT . n) = Gn & (IT . (n + 1)) = Gn1 & Gn1 = ( DIJK:Step Gn) by A2, A4;

          hence P2[(n + 1)];

        end;

        

         A5: P2[ 0 ] by A2;

        for n be Nat holds P2[n] from NAT_1:sch 2( A5, A3);

        then

        reconsider IT as DIJK:LabelingSeq of G by Def10;

        reconsider IT as DIJK:LabelingSeq of G;

        take IT;

        thus (IT . 0 ) = ( DIJK:Init src) by A2;

        let n be Nat;

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        ex Gn,Gn1 be DIJK:Labeling of G st (IT . n9) = Gn & (IT . (n + 1)) = Gn1 & Gn1 = ( DIJK:Step Gn) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be DIJK:LabelingSeq of G such that

         A6: (IT1 . 0 ) = ( DIJK:Init src) and

         A7: for n be Nat holds (IT1 . (n + 1)) = ( DIJK:Step (IT1 . n)) and

         A8: (IT2 . 0 ) = ( DIJK:Init src) and

         A9: for n be Nat holds (IT2 . (n + 1)) = ( DIJK:Step (IT2 . n));

        defpred P[ Nat] means (IT1 . $1) = (IT2 . $1);

        now

          let n be Nat;

          assume P[n];

          

          then (IT1 . (n + 1)) = ( DIJK:Step (IT2 . n)) by A7

          .= (IT2 . (n + 1)) by A9;

          hence P[(n + 1)];

        end;

        then

         A10: for n be Nat st P[n] holds P[(n + 1)];

        

         A11: P[ 0 ] by A6, A8;

        for n be Nat holds P[n] from NAT_1:sch 2( A11, A10);

        then for n be object st n in NAT holds (IT1 . n) = (IT2 . n);

        hence IT1 = IT2 by PBOOLE: 3;

      end;

    end

    definition

      let G be real-weighted WGraph, src be Vertex of G;

      :: GLIB_004:def12

      func DIJK:SSSP (G,src) -> DIJK:Labeling of G equals (( DIJK:CompSeq src) .Result() );

      coherence

      proof

        set DCS = ( DIJK:CompSeq src);

        (DCS .Result() ) = (DCS . (DCS .Lifespan() ));

        hence thesis;

      end;

    end

    begin

    theorem :: GLIB_004:15

    

     Th15: for G be _finite real-weighted WGraph, L be DIJK:Labeling of G holds (( card ( dom (( DIJK:Step L) `1 ))) = ( card ( dom (L `1 ))) iff ( DIJK:NextBestEdges L) = {} ) & (( card ( dom (( DIJK:Step L) `1 ))) = (( card ( dom (L `1 ))) + 1) iff ( DIJK:NextBestEdges L) <> {} )

    proof

      let G be _finite real-weighted WGraph, L be DIJK:Labeling of G;

      set BestEdges = ( DIJK:NextBestEdges L), e = the Element of BestEdges;

      set nextEG = ((L `2 ) \/ {e}), nL = ( DIJK:Step L);

      set src = (( the_Source_of G) . e), target = (( the_Target_of G) . e);

      set val = (((L `1 ) . src) + (( the_Weight_of G) . e));

      hereby

        assume

         A1: ( card ( dom (nL `1 ))) = ( card ( dom (L `1 )));

        now

          assume

           A2: BestEdges <> {} ;

          then nL = [((L `1 ) +* (target .--> val)), nextEG] by Def8;

          then (nL `1 ) = ((L `1 ) +* (target .--> val));

          then

           A3: ( dom (nL `1 )) = (( dom (L `1 )) \/ {target}) by Lm1;

          e in BestEdges by A2;

          then

          reconsider target as Vertex of G by FUNCT_2: 5;

          e DSJoins (( dom (L `1 )),(( the_Vertices_of G) \ ( dom (L `1 ))),G) by A2, Def7;

          then target in (( the_Vertices_of G) \ ( dom (L `1 )));

          then not target in ( dom (L `1 )) by XBOOLE_0:def 5;

          then ( card ( dom (nL `1 ))) = (( card ( dom (L `1 ))) + 1) by A3, CARD_2: 41;

          hence contradiction by A1;

        end;

        hence BestEdges = {} ;

      end;

      thus BestEdges = {} implies ( card ( dom (nL `1 ))) = ( card ( dom (L `1 ))) by Def8;

      hereby

        assume

         A4: ( card ( dom (nL `1 ))) = (( card ( dom (L `1 ))) + 1);

        now

          assume BestEdges = {} ;

          then ( 0 + ( card ( dom (L `1 )))) = (( card ( dom (L `1 ))) + 1) by A4, Def8;

          hence contradiction;

        end;

        hence BestEdges <> {} ;

      end;

      assume

       A5: BestEdges <> {} ;

      then nL = [((L `1 ) +* (target .--> val)), nextEG] by Def8;

      then (nL `1 ) = ((L `1 ) +* (target .--> val));

      then

       A6: ( dom (nL `1 )) = (( dom (L `1 )) \/ {target}) by Lm1;

      e in BestEdges by A5;

      then

      reconsider target as Vertex of G by FUNCT_2: 5;

      e DSJoins (( dom (L `1 )),(( the_Vertices_of G) \ ( dom (L `1 ))),G) by A5, Def7;

      then target in (( the_Vertices_of G) \ ( dom (L `1 )));

      then not target in ( dom (L `1 )) by XBOOLE_0:def 5;

      hence thesis by A6, CARD_2: 41;

    end;

    theorem :: GLIB_004:16

    

     Th16: for G be real-weighted WGraph, L be DIJK:Labeling of G holds ( dom (L `1 )) c= ( dom (( DIJK:Step L) `1 )) & (L `2 ) c= (( DIJK:Step L) `2 )

    proof

      let G be real-weighted WGraph, L be DIJK:Labeling of G;

      set nL = ( DIJK:Step L);

      set BestEdges = ( DIJK:NextBestEdges L), e = the Element of BestEdges;

      set NextEG = ((L `2 ) \/ {e}), target = (( the_Target_of G) . e);

      set val = (((L `1 ) . (( the_Source_of G) . e)) + (( the_Weight_of G) . e));

      now

        per cases ;

          suppose BestEdges = {} ;

          hence thesis by Def8;

        end;

          suppose BestEdges <> {} ;

          then

           A1: nL = [((L `1 ) +* (target .--> val)), NextEG] by Def8;

          then (nL `1 ) = ((L `1 ) +* (target .--> val));

          then

           A2: ( dom (nL `1 )) = (( dom (L `1 )) \/ {target}) by Lm1;

          now

            let x be object;

            assume

             A3: x in ( dom (L `1 ));

            ( dom (L `1 )) c= ( dom (nL `1 )) by A2, XBOOLE_1: 7;

            hence x in ( dom (nL `1 )) by A3;

          end;

          hence ( dom (L `1 )) c= ( dom (nL `1 ));

          now

            let x be object;

            assume

             A4: x in (L `2 );

            (L `2 ) c= NextEG & NextEG = (nL `2 ) by A1, XBOOLE_1: 7;

            hence x in (nL `2 ) by A4;

          end;

          hence (L `2 ) c= (nL `2 );

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_004:17

    for G be real-weighted WGraph, src be Vertex of G holds ( dom (( DIJK:Init src) `1 )) = {src};

    theorem :: GLIB_004:18

    

     Th18: for G be real-weighted WGraph, src be Vertex of G, i,j be Nat st i <= j holds ( dom ((( DIJK:CompSeq src) . i) `1 )) c= ( dom ((( DIJK:CompSeq src) . j) `1 )) & ((( DIJK:CompSeq src) . i) `2 ) c= ((( DIJK:CompSeq src) . j) `2 )

    proof

      let G be real-weighted WGraph, src be Vertex of G, i,j be Nat;

      set DCS = ( DIJK:CompSeq src);

      set dDCS = ( dom ((DCS . i) `1 ));

      set eDCS = ((DCS . i) `2 );

      defpred P[ Nat] means dDCS c= ( dom ((DCS . (i + $1)) `1 )) & eDCS c= ((DCS . (i + $1)) `2 );

      assume i <= j;

      then

       A1: ex x be Nat st j = (i + x) by NAT_1: 10;

      now

        let k be Nat;

        (DCS . ((i + k) + 1)) = ( DIJK:Step (DCS . (i + k))) by Def11;

        then

         A2: ( dom ((DCS . (i + k)) `1 )) c= ( dom ((DCS . ((i + k) + 1)) `1 )) & ((DCS . (i + k)) `2 ) c= ((DCS . ((i + k) + 1)) `2 ) by Th16;

        assume dDCS c= ( dom ((DCS . (i + k)) `1 )) & eDCS c= ((DCS . (i + k)) `2 );

        hence dDCS c= ( dom ((DCS . (i + (k + 1))) `1 )) & eDCS c= ((DCS . (i + (k + 1))) `2 ) by A2;

      end;

      then

       A3: for k be Nat st P[k] holds P[(k + 1)];

      

       A4: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A4, A3);

      hence thesis by A1;

    end;

    theorem :: GLIB_004:19

    

     Th19: for G be _finite real-weighted WGraph, src be Vertex of G, n be Nat holds ( dom ((( DIJK:CompSeq src) . n) `1 )) c= (G .reachableDFrom src)

    proof

      let G be _finite real-weighted WGraph, src be Vertex of G;

      set DCS = ( DIJK:CompSeq src);

      defpred P[ Nat] means ( dom ((DCS . $1) `1 )) c= (G .reachableDFrom src);

      (DCS . 0 ) = ( DIJK:Init src) by Def11;

      then

       A1: ( dom ((DCS . 0 ) `1 )) = {src};

      now

        let k be Nat such that

         A2: ( dom ((DCS . k) `1 )) c= (G .reachableDFrom src);

        set Gk = (DCS . k), NextG = (DCS . (k + 1));

        set BestEdges = ( DIJK:NextBestEdges Gk), e = the Element of BestEdges;

        set NextEG = ((Gk `2 ) \/ {e});

        set v1 = (( the_Source_of G) . e), target = (( the_Target_of G) . e);

        set pc = ((Gk `1 ) . v1), ec = (( the_Weight_of G) . e);

        

         A3: NextG = ( DIJK:Step Gk) by Def11;

        now

          let x be object;

          assume

           A4: x in ( dom ((DCS . (k + 1)) `1 ));

          now

            per cases ;

              suppose BestEdges = {} ;

              then Gk = NextG by A3, Def8;

              hence x in (G .reachableDFrom src) by A2, A4;

            end;

              suppose

               A5: BestEdges <> {} ;

              set xx = x;

              reconsider xx as Vertex of G by A4;

              e DSJoins (( dom (Gk `1 )),(( the_Vertices_of G) \ ( dom (Gk `1 ))),G) by A5, Def7;

              then

               A6: v1 in ( dom (Gk `1 ));

              then

              reconsider v19 = v1 as Vertex of G;

              NextG = [((Gk `1 ) +* (target .--> (pc + ec))), NextEG] by A3, A5, Def8;

              then

               A7: (NextG `1 ) = ((Gk `1 ) +* (target .--> (pc + ec)));

              now

                per cases ;

                  suppose xx in ( dom (Gk `1 ));

                  hence xx in (G .reachableDFrom src) by A2;

                end;

                  suppose

                   A8: not xx in ( dom (Gk `1 ));

                  

                   A9: e in BestEdges by A5;

                  (( the_Target_of G) . e) = xx by A4, A7, A8, Lm2;

                  then e DJoins (v19,xx,G) by A9;

                  hence xx in (G .reachableDFrom src) by A2, A6, GLIB_002: 19;

                end;

              end;

              hence x in (G .reachableDFrom src);

            end;

          end;

          hence x in (G .reachableDFrom src);

        end;

        hence ( dom ((DCS . (k + 1)) `1 )) c= (G .reachableDFrom src);

      end;

      then

       A10: for k be Nat st P[k] holds P[(k + 1)];

      src in (G .reachableDFrom src) by GLIB_002: 18;

      then

       A11: P[ 0 ] by A1, ZFMISC_1: 31;

      for n be Nat holds P[n] from NAT_1:sch 2( A11, A10);

      hence thesis;

    end;

    theorem :: GLIB_004:20

    

     Th20: for G be _finite real-weighted WGraph, src be Vertex of G, n be Nat holds ( DIJK:NextBestEdges (( DIJK:CompSeq src) . n)) = {} iff ( dom ((( DIJK:CompSeq src) . n) `1 )) = (G .reachableDFrom src)

    proof

      let G be _finite real-weighted WGraph, src be Vertex of G, n be Nat;

      set DCS = ( DIJK:CompSeq src), RFS = (G .reachableDFrom src);

      set Gn = (DCS . n), Gn1a = (DCS . (n + 1));

      set BestEdges = ( DIJK:NextBestEdges Gn);

      set SGn = ( the_Source_of G);

      set TGn = ( the_Target_of G);

      hereby

        assume

         A1: BestEdges = {} ;

        now

          defpred P[ set] means (SGn . $1) in ( dom (Gn `1 )) & not (TGn . $1) in ( dom (Gn `1 ));

          assume

           A2: ( dom (Gn `1 )) <> RFS;

          consider BE1 be Subset of ( the_Edges_of G) such that

           A3: for x be set holds x in BE1 iff x in ( the_Edges_of G) & P[x] from SUBSET_1:sch 1;

          ( dom (Gn `1 )) c= RFS by Th19;

          then

           A4: ( dom (Gn `1 )) c< RFS by A2, XBOOLE_0:def 8;

          now

            (DCS . 0 ) = ( DIJK:Init src) by Def11;

            then ( dom ((DCS . 0 ) `1 )) = {src};

            then

             A5: src in ( dom ((DCS . 0 ) `1 )) by TARSKI:def 1;

            assume

             A6: BE1 = {} ;

            consider v be object such that

             A7: v in RFS and

             A8: not v in ( dom (Gn `1 )) by A4, XBOOLE_0: 6;

            reconsider v as Vertex of G by A7;

            consider W be directed Walk of G such that

             A9: W is_Walk_from (src,v) by A7, GLIB_002:def 6;

            defpred P[ Nat] means $1 is odd & $1 <= ( len W) & not ((W . $1) in ( dom (Gn `1 )));

            (W . ( len W)) = (W .last() ) by GLIB_001:def 7

            .= v by A9, GLIB_001:def 23;

            then

             A10: ex k be Nat st P[k] by A8;

            consider k be Nat such that

             A11: P[k] & for m be Nat st P[m] holds k <= m from NAT_1:sch 5( A10);

            

             A12: ( dom ((DCS . 0 ) `1 )) c= ( dom (Gn `1 )) by Th18;

            now

              per cases ;

                suppose k = 1;

                

                then (W . k) = (W .first() ) by GLIB_001:def 6

                .= src by A9, GLIB_001:def 23;

                hence contradiction by A5, A12, A11;

              end;

                suppose

                 A13: k <> 1;

                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 + 1) by XREAL_1: 8;

                then (2 * 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: e DJoins ((W . k2a),(W . (k2a + 2)),G) by GLIB_001: 122;

                then

                 A16: (( the_Target_of G) . e) = (W . (k2a + 2));

                k2a < (k - 0 ) by XREAL_1: 15;

                then

                 A17: (W . k2a) in ( dom (Gn `1 )) by A11, A14;

                e in ( the_Edges_of G) & (( the_Source_of G) . e) = (W . k2a) by A15;

                hence contradiction by A3, A6, A11, A17, A16;

              end;

            end;

            hence contradiction;

          end;

          then

          reconsider BE1 as non empty finite set;

          deffunc F( Element of BE1) = (((Gn `1 ) . (( the_Source_of G) . $1)) + (( the_Weight_of G) . $1));

          consider e1 be Element of BE1 such that

           A18: for e2 be Element of BE1 holds F(e1) <= F(e2) from PRE_CIRC:sch 5;

          

           A19: not (TGn . e1) in ( dom (Gn `1 )) by A3;

          

           A20: e1 in ( the_Edges_of G) by A3;

          then (TGn . e1) in ( the_Vertices_of G) by FUNCT_2: 5;

          then

           A21: (TGn . e1) in (( the_Vertices_of G) \ ( dom (Gn `1 ))) by A19, XBOOLE_0:def 5;

           A22:

          now

            let y be set;

            assume

             A23: y DSJoins (( dom (Gn `1 )),(( the_Vertices_of G) \ ( dom (Gn `1 ))),G);

            then (TGn . y) in (( the_Vertices_of G) \ ( dom (Gn `1 )));

            then

             A24: not (TGn . y) in ( dom (Gn `1 )) by XBOOLE_0:def 5;

            y in ( the_Edges_of G) & (SGn . y) in ( dom (Gn `1 )) by A23;

            then y in BE1 by A3, A24;

            hence (((Gn `1 ) . (( the_Source_of G) . e1)) + (( the_Weight_of G) . e1)) <= (((Gn `1 ) . (( the_Source_of G) . y)) + (( the_Weight_of G) . y)) by A18;

          end;

          (SGn . e1) in ( dom (Gn `1 )) by A3;

          then e1 DSJoins (( dom (Gn `1 )),(( the_Vertices_of G) \ ( dom (Gn `1 ))),G) by A20, A21;

          hence contradiction by A1, A22, Def7;

        end;

        hence ( dom ((DCS . n) `1 )) = RFS;

      end;

      assume

       A25: ( dom ((DCS . n) `1 )) = RFS;

      

       A26: Gn1a = ( DIJK:Step Gn) by Def11;

      now

        assume BestEdges <> {} ;

        then

         A27: ( card ( dom (Gn1a `1 ))) = (( card RFS) + 1) by A26, A25, Th15;

        ( Segm ( card ( dom (Gn1a `1 )))) c= ( Segm ( card RFS)) by Th19, CARD_1: 11;

        then (( card RFS) + 1) <= (( card RFS) + 0 ) by A27, NAT_1: 39;

        hence contradiction by XREAL_1: 6;

      end;

      hence thesis;

    end;

    theorem :: GLIB_004:21

    

     Th21: for G be _finite real-weighted WGraph, s be Vertex of G, n be Nat holds ( card ( dom ((( DIJK:CompSeq s) . n) `1 ))) = ( min ((n + 1),( card (G .reachableDFrom s))))

    proof

      let G be _finite real-weighted WGraph, src be Vertex of G;

      set DCS = ( DIJK:CompSeq src), VL0 = ( dom ((DCS . 0 ) `1 ));

      set RFS = (G .reachableDFrom src);

      defpred P[ Nat] means ( card ( dom ((DCS . $1) `1 ))) = ( min (($1 + 1),( card RFS)));

      src in RFS by GLIB_002: 18;

      then {src} c= RFS by ZFMISC_1: 31;

      then ( card {src}) <= ( card RFS) by NAT_1: 43;

      then

       A1: ( 0 + 1) <= ( card RFS) by CARD_1: 30;

      now

        let k be Nat such that

         A2: ( card ( dom ((DCS . k) `1 ))) = ( min ((k + 1),( card RFS)));

        set Gk = (DCS . k), Gk1b = (DCS . (k + 1));

        set BestEdges = ( DIJK:NextBestEdges Gk);

        

         A3: (DCS . (k + 1)) = ( DIJK:Step (DCS . k)) by Def11;

        now

          per cases ;

            suppose

             A4: BestEdges = {} ;

            then ( card ( dom (Gk `1 ))) = ( card RFS) by Th20;

            then ( card RFS) <= (k + 1) by A2, XXREAL_0:def 9;

            then

             A5: ( card RFS) <= ((k + 1) + 1) by NAT_1: 12;

            ( card ( dom (Gk1b `1 ))) = ( card ( dom (Gk `1 ))) by A3, A4, Th15;

            then ( card ( dom (Gk1b `1 ))) = ( card RFS) by A4, Th20;

            hence ( card ( dom (Gk1b `1 ))) = ( min (((k + 1) + 1),( card RFS))) by A5, XXREAL_0:def 9;

          end;

            suppose

             A6: BestEdges <> {} ;

            then

             A7: ( dom (Gk `1 )) <> RFS by Th20;

             A8:

            now

              ( dom (Gk `1 )) c= RFS by Th19;

              then

               A9: ( dom (Gk `1 )) c< RFS by A7, XBOOLE_0:def 8;

              assume ( card ( dom (Gk `1 ))) = ( card RFS);

              hence contradiction by A9, CARD_2: 48;

            end;

            then (k + 1) <= ( card RFS) by A2, XXREAL_0:def 9;

            then

             A10: ((k + 1) + 1) <= (( card RFS) + 1) by XREAL_1: 6;

            ((k + 1) + 1) <> (( card RFS) + 1) by A2, A8;

            then ((k + 1) + 1) < (( card RFS) + 1) by A10, XXREAL_0: 1;

            then

             A11: ((k + 1) + 1) <= ( card RFS) by NAT_1: 13;

            ( card ( dom (Gk1b `1 ))) = (( card ( dom (Gk `1 ))) + 1) by A3, A6, Th15;

            then ( card ( dom (Gk1b `1 ))) = ((k + 1) + 1) by A2, A8, XXREAL_0: 15;

            hence ( card ( dom (Gk1b `1 ))) = ( min (((k + 1) + 1),( card RFS))) by A11, XXREAL_0:def 9;

          end;

        end;

        hence ( card ( dom ((DCS . (k + 1)) `1 ))) = ( min (((k + 1) + 1),( card RFS)));

      end;

      then

       A12: for k be Nat st P[k] holds P[(k + 1)];

      (DCS . 0 ) = ( DIJK:Init src) by Def11;

      

      then ( card VL0) = ( card {src})

      .= 1 by CARD_1: 30;

      then

       A13: P[ 0 ] by A1, XXREAL_0:def 9;

      for n be Nat holds P[n] from NAT_1:sch 2( A13, A12);

      hence thesis;

    end;

    theorem :: GLIB_004:22

    

     Th22: for G be _finite real-weighted WGraph, src be Vertex of G, n be Nat holds ((( DIJK:CompSeq src) . n) `2 ) c= (G .edgesBetween ( dom ((( DIJK:CompSeq src) . n) `1 )))

    proof

      let G be _finite real-weighted WGraph, src be Vertex of G;

      set DCS = ( DIJK:CompSeq src), D0 = (DCS . 0 );

      defpred P[ Nat] means ((DCS . $1) `2 ) c= (G .edgesBetween ( dom ((DCS . $1) `1 )));

      now

        let n be Nat;

        set Dn = (DCS . n), Dn1 = (DCS . (n + 1));

        set BE = ( DIJK:NextBestEdges Dn), e = the Element of BE;

        set target = (( the_Target_of G) . e);

        set val = (((Dn `1 ) . (( the_Source_of G) . e)) + (( the_Weight_of G) . e));

        set DnE = ((Dn `2 ) \/ {e});

        assume

         A1: (Dn `2 ) c= (G .edgesBetween ( dom (Dn `1 )));

        

         A2: Dn1 = ( DIJK:Step Dn) by Def11;

        now

          let x be object;

          n <= (n + 1) by NAT_1: 12;

          then

           A3: ( dom (Dn `1 )) c= ( dom (Dn1 `1 )) by Th18;

          assume

           A4: x in (Dn1 `2 );

          now

            per cases ;

              suppose BE = {} ;

              then Dn1 = Dn by A2, Def8;

              hence x in (G .edgesBetween ( dom (Dn1 `1 ))) by A1, A4;

            end;

              suppose

               A5: BE <> {} ;

              then

               A6: Dn1 = [((Dn `1 ) +* (target .--> val)), DnE] by A2, Def8;

              then

               A7: (Dn1 `2 ) = DnE;

              (Dn1 `1 ) = ((Dn `1 ) +* (target .--> val)) by A6;

              then

               A8: ( dom (Dn1 `1 )) = (( dom (Dn `1 )) \/ {target}) by Lm1;

              

               A9: e in BE by A5;

              now

                per cases by A4, A7, XBOOLE_0:def 3;

                  suppose

                   A10: x in (Dn `2 );

                  (( the_Source_of G) . x) in ( dom (Dn `1 )) & (( the_Target_of G) . x) in ( dom (Dn `1 )) by A1, A10, GLIB_000: 31;

                  hence x in (G .edgesBetween ( dom (Dn1 `1 ))) by A3, A10, GLIB_000: 31;

                end;

                  suppose x in {e};

                  then

                   A11: x = e by TARSKI:def 1;

                  then (( the_Target_of G) . x) in {target} by TARSKI:def 1;

                  then

                   A12: (( the_Target_of G) . x) in ( dom (Dn1 `1 )) by A8, XBOOLE_0:def 3;

                  e DSJoins (( dom (Dn `1 )),(( the_Vertices_of G) \ ( dom (Dn `1 ))),G) by A5, Def7;

                  then (( the_Source_of G) . x) in ( dom (Dn `1 )) by A11;

                  hence x in (G .edgesBetween ( dom (Dn1 `1 ))) by A3, A9, A11, A12, GLIB_000: 31;

                end;

              end;

              hence x in (G .edgesBetween ( dom (Dn1 `1 )));

            end;

          end;

          hence x in (G .edgesBetween ( dom (Dn1 `1 )));

        end;

        hence (Dn1 `2 ) c= (G .edgesBetween ( dom (Dn1 `1 )));

      end;

      then

       A13: for k be Nat st P[k] holds P[(k + 1)];

      D0 = ( DIJK:Init src) by Def11;

      then for x be object st x in (D0 `2 ) holds x in (G .edgesBetween ( dom (D0 `1 )));

      then

       A14: P[ 0 ] by TARSKI:def 3;

      for n be Nat holds P[n] from NAT_1:sch 2( A14, A13);

      hence thesis;

    end;

    theorem :: GLIB_004:23

    

     Th23: for G be _finite nonnegative-weighted WGraph, s be Vertex of G, n be Nat, G2 be inducedWSubgraph of G, ( dom ((( DIJK:CompSeq s) . n) `1 )), ((( DIJK:CompSeq s) . n) `2 ) holds G2 is_mincost_DTree_rooted_at s & for v be Vertex of G st v in ( dom ((( DIJK:CompSeq s) . n) `1 )) holds (G .min_DPath_cost (s,v)) = (((( DIJK:CompSeq s) . n) `1 ) . v)

    proof

      let G be _finite nonnegative-weighted WGraph, src be Vertex of G;

      set DCS = ( DIJK:CompSeq src), D0 = (DCS . 0 );

      defpred P[ Nat] means for G2 be inducedWSubgraph of G, ( dom ((DCS . $1) `1 )), ((DCS . $1) `2 ) holds G2 is_mincost_DTree_rooted_at src & for v be Vertex of G st v in ( dom ((DCS . $1) `1 )) holds (G .min_DPath_cost (src,v)) = (((DCS . $1) `1 ) . v);

      

       A1: D0 = ( DIJK:Init src) by Def11;

      then

       A2: (D0 `1 ) = (src .--> 0 );

      then

       A3: ( dom (D0 `1 )) = {src};

      now

        let n be Nat;

        set Dn = (DCS . n), Dn1 = (DCS . (n + 1));

        set BE = ( DIJK:NextBestEdges Dn), e = the Element of BE;

        set source = (( the_Source_of G) . e), target = (( the_Target_of G) . e);

        set DnE = ((Dn `2 ) \/ {e});

        set pc = ((Dn `1 ) . source);

        set ec = (( the_Weight_of G) . e);

        set DnW = the inducedWSubgraph of G, ( dom (Dn `1 )), (Dn `2 );

        

         A4: Dn1 = ( DIJK:Step Dn) by Def11;

        assume

         A5: P[n];

        then

         A6: DnW is_mincost_DTree_rooted_at src;

        then

         A7: DnW is Tree-like;

        let Dn1W be inducedWSubgraph of G, ( dom (Dn1 `1 )), (Dn1 `2 );

        

         A8: src in ( dom (D0 `1 )) & ( dom (D0 `1 )) c= ( dom (Dn `1 )) by A3, Th18, TARSKI:def 1;

        

         A9: (Dn `2 ) c= (G .edgesBetween ( dom (Dn `1 ))) by Th22;

        then

         A10: ( card (Dn `2 )) = (DnW .size() ) by A8, GLIB_000:def 37;

        

         A11: (Dn `2 ) c= (G .edgesBetween ( dom (Dn `1 ))) by Th22;

        then

         A12: ( the_Vertices_of DnW) = ( dom (Dn `1 )) by A8, GLIB_000:def 37;

        

         A13: ( the_Edges_of DnW) = (Dn `2 ) by A8, A11, GLIB_000:def 37;

        

         A14: ( card ( dom (Dn `1 ))) = (DnW .order() ) by A8, A9, GLIB_000:def 37;

        now

          per cases ;

            suppose BE = {} ;

            then Dn1 = Dn by A4, Def8;

            hence Dn1W is_mincost_DTree_rooted_at src & for v be Vertex of G st v in ( dom (Dn1 `1 )) holds (G .min_DPath_cost (src,v)) = ((Dn1 `1 ) . v) by A5;

          end;

            suppose

             A15: BE <> {} ;

            set mc = (G .min_DPath_cost (src,target));

            

             A16: ( the_Weight_of Dn1W) = (( the_Weight_of G) | ( the_Edges_of Dn1W)) by GLIB_003:def 10;

            

             A17: e DSJoins (( dom (Dn `1 )),(( the_Vertices_of G) \ ( dom (Dn `1 ))),G) by A15, Def7;

            then

             A18: target in (( the_Vertices_of G) \ ( dom (Dn `1 )));

            then

             A19: src <> target by A8, XBOOLE_0:def 5;

            

             A20: not target in ( dom (Dn `1 )) by A18, XBOOLE_0:def 5;

            then

             A21: ( card (( dom (Dn `1 )) \/ {target})) = (( card ( dom (Dn `1 ))) + 1) by CARD_2: 41;

            

             A22: source in ( dom (Dn `1 )) by A17;

            

             A23: Dn1 = [((Dn `1 ) +* (target .--> (pc + ec))), DnE] by A4, A15, Def8;

            then (Dn1 `1 ) = ((Dn `1 ) +* (target .--> (pc + ec)));

            then

             A24: ( dom (Dn1 `1 )) = (( dom (Dn `1 )) \/ {target}) by Lm1;

            

             A25: (Dn1 `2 ) c= (G .edgesBetween ( dom (Dn1 `1 ))) by Th22;

            then

             A26: ( the_Vertices_of Dn1W) = (( dom (Dn `1 )) \/ {target}) by A24, GLIB_000:def 37;

            (Dn1 `2 ) = DnE by A23;

            then

             A27: ( the_Edges_of Dn1W) = ((Dn `2 ) \/ {e}) by A24, A25, GLIB_000:def 37;

             A28:

            now

              thus ( the_Vertices_of DnW) c= ( the_Vertices_of Dn1W) & ( the_Edges_of DnW) c= ( the_Edges_of Dn1W) by A12, A13, A26, A27, XBOOLE_1: 7;

              let e be set;

              assume

               A29: e in ( the_Edges_of DnW);

              then

               A30: (( the_Target_of DnW) . e) = (( the_Target_of G) . e) by GLIB_000:def 32;

              e in ( the_Edges_of Dn1W) & (( the_Source_of DnW) . e) = (( the_Source_of G) . e) by A13, A27, A29, GLIB_000:def 32, XBOOLE_0:def 3;

              hence (( the_Source_of DnW) . e) = (( the_Source_of Dn1W) . e) & (( the_Target_of DnW) . e) = (( the_Target_of Dn1W) . e) by A30, GLIB_000:def 32;

            end;

            then

            reconsider DnW9 = DnW as [Weighted] Subgraph of Dn1W by GLIB_000:def 32;

            e in {e} by TARSKI:def 1;

            then

             A31: e in ( the_Edges_of Dn1W) by A27, XBOOLE_0:def 3;

            e in BE by A15;

            then e DJoins (source,target,G);

            then

             A32: e DJoins (source,target,Dn1W) by A31, GLIB_000: 73;

            then

             A33: e Joins (source,target,Dn1W);

            

             A34: ( the_Weight_of DnW9) = (( the_Weight_of G) | ( the_Edges_of DnW)) by GLIB_003:def 10;

             A35:

            now

              let y be object;

              assume y in ( dom ( the_Weight_of DnW9));

              then

               A36: y in ( the_Edges_of DnW);

              

              hence (( the_Weight_of DnW9) . y) = (( the_Weight_of G) . y) by A34, FUNCT_1: 49

              .= (( the_Weight_of Dn1W) . y) by A28, A16, A36, FUNCT_1: 49;

            end;

            ( dom ( the_Weight_of Dn1W)) = ( the_Edges_of Dn1W) by PARTFUN1:def 2;

            then (( dom ( the_Weight_of Dn1W)) /\ ( the_Edges_of DnW)) = ( the_Edges_of DnW) by A28, XBOOLE_1: 28;

            then ( dom ( the_Weight_of DnW9)) = (( dom ( the_Weight_of Dn1W)) /\ ( the_Edges_of DnW)) by PARTFUN1:def 2;

            then ( the_Weight_of DnW9) = (( the_Weight_of Dn1W) | ( the_Edges_of DnW)) by A35, FUNCT_1: 46;

            then

             A37: DnW is WSubgraph of Dn1W by GLIB_003:def 10;

            

             A38: DnW is Subgraph of Dn1W by A28, GLIB_000:def 32;

            now

              let u,v be Vertex of Dn1W;

               A39:

              now

                let u,v be set;

                assume u in ( dom (Dn `1 )) & v in ( dom (Dn `1 ));

                then

                reconsider u9 = u, v9 = v as Vertex of DnW by A11, GLIB_000:def 37;

                consider W1 be Walk of DnW such that

                 A40: W1 is_Walk_from (u9,v9) by A7, GLIB_002:def 1;

                reconsider W2 = W1 as Walk of Dn1W by A38, GLIB_001: 167;

                W2 is_Walk_from (u,v) by A40, GLIB_001: 19;

                hence ex W be Walk of Dn1W st W is_Walk_from (u,v);

              end;

              now

                per cases by A26, XBOOLE_0:def 3;

                  suppose u in ( dom (Dn `1 )) & v in ( dom (Dn `1 ));

                  hence ex W be Walk of Dn1W st W is_Walk_from (u,v) by A39;

                end;

                  suppose

                   A41: u in ( dom (Dn `1 )) & v in {target};

                  then

                   A42: v = target by TARSKI:def 1;

                  consider W be Walk of Dn1W such that

                   A43: W is_Walk_from (u,source) by A22, A39, A41;

                  (W .addEdge e) is_Walk_from (u,target) by A33, A43, GLIB_001: 66;

                  hence ex W be Walk of Dn1W st W is_Walk_from (u,v) by A42;

                end;

                  suppose

                   A44: u in {target} & v in ( dom (Dn `1 ));

                  then

                  consider W be Walk of Dn1W such that

                   A45: W is_Walk_from (v,source) by A22, A39;

                  (W .addEdge e) is_Walk_from (v,target) by A33, A45, GLIB_001: 66;

                  then (W .addEdge e) is_Walk_from (v,u) by A44, TARSKI:def 1;

                  then ((W .addEdge e) .reverse() ) is_Walk_from (u,v) by GLIB_001: 23;

                  hence ex W be Walk of Dn1W st W is_Walk_from (u,v);

                end;

                  suppose

                   A46: u in {target} & v in {target};

                  take W = (Dn1W .walkOf u);

                  u = target & v = target by A46, TARSKI:def 1;

                  hence W is_Walk_from (u,v) by GLIB_001: 13;

                end;

              end;

              hence ex W be Walk of Dn1W st W is_Walk_from (u,v);

            end;

            then

             A47: Dn1W is connected by GLIB_002:def 1;

            

             A48: not e in (Dn `2 ) by A9, A20, GLIB_000: 31;

            then (Dn1W .size() ) = ((DnW .size() ) + 1) by A10, A27, CARD_2: 41;

            then (Dn1W .order() ) = ((Dn1W .size() ) + 1) by A14, A7, A26, A21, GLIB_002: 47;

            then

             A49: Dn1W is Tree-like by A47, GLIB_002: 47;

            now

              consider WT be DPath of DnW such that

               A50: WT is_Walk_from (src,source) and

               A51: for W1 be DPath of G st W1 is_Walk_from (src,source) holds (WT .cost() ) <= (W1 .cost() ) by A12, A6, A22;

              reconsider WT9 = WT as DPath of Dn1W by A38, GLIB_001: 175;

              set W2 = (WT9 .addEdge e);

              

               A52: WT9 is_Walk_from (src,source) by A50, GLIB_001: 19;

              then

              reconsider W2 as DWalk of Dn1W by A32, GLIB_001: 123;

              now

                target in {target} by TARSKI:def 1;

                hence target is Vertex of Dn1W by A26, XBOOLE_0:def 3;

                thus e Joins ((WT9 .last() ),target,Dn1W) by A33, A52, GLIB_001:def 23;

                ( not e in ( the_Edges_of DnW)) & (WT .edges() ) = (WT9 .edges() ) by A8, A9, A48, GLIB_000:def 37, GLIB_001: 110;

                hence not e in (WT9 .edges() );

                thus WT9 is trivial or WT9 is open by GLIB_001:def 31, A49, GLIB_002:def 2;

                let n be odd Element of NAT ;

                assume that 1 < n and

                 A53: n <= ( len WT9);

                (WT9 .vertices() ) = (WT .vertices() ) by GLIB_001: 98;

                then not target in (WT9 .vertices() ) by A12, A18, XBOOLE_0:def 5;

                hence (WT9 . n) <> target by A53, GLIB_001: 87;

              end;

              then

              reconsider W2 as DPath of Dn1W by GLIB_001: 150;

              take W2;

              thus W2 is_Walk_from (src,target) by A33, A52, GLIB_001: 66;

              now

                (WT9 .last() ) = source & (( the_Source_of Dn1W) . e) = source by A32, A52, GLIB_001:def 23;

                hence e in ((WT9 .last() ) .edgesInOut() ) by A31, GLIB_000: 61;

                reconsider WTG = WT as DPath of G by GLIB_001: 175;

                

                 A54: WTG is_Walk_from (src,source) by A50, GLIB_001: 19;

                (( the_Weight_of Dn1W) . e) = ((( the_Weight_of G) | ( the_Edges_of Dn1W)) . e) by GLIB_003:def 10;

                hence ec = (( the_Weight_of Dn1W) . e) by A31, FUNCT_1: 49;

                pc = (G .min_DPath_cost (src,source)) by A5, A22;

                then

                consider WX be DPath of G such that

                 A55: WX is_mincost_DPath_from (src,source) and

                 A56: pc = (WX .cost() ) by A54, Def3;

                WX is_Walk_from (src,source) by A55;

                then (WT .cost() ) <= pc by A51, A56;

                then

                 A57: (WT9 .cost() ) <= pc by A37, GLIB_003: 27;

                pc <= (WTG .cost() ) by A54, A55, A56;

                then pc <= (WT9 .cost() ) by GLIB_003: 27;

                hence (WT9 .cost() ) = pc by A57, XXREAL_0: 1;

              end;

              hence (W2 .cost() ) = (pc + ec) by GLIB_003: 25;

            end;

            then

            consider W2 be DPath of Dn1W such that

             A58: W2 is_Walk_from (src,target) and

             A59: (W2 .cost() ) = (pc + ec);

            reconsider W2G = W2 as DPath of G by GLIB_001: 175;

            

             A60: W2G is_Walk_from (src,target) by A58, GLIB_001: 19;

            

             A61: (W2G .cost() ) = (pc + ec) by A59, GLIB_003: 27;

            now

              consider WB be DPath of G such that

               A62: WB is_mincost_DPath_from (src,target) and

               A63: mc = (WB .cost() ) by A60, Def3;

              thus mc <= (pc + ec) by A60, A61, A62, A63;

              

               A64: WB is_Walk_from (src,target) by A62;

              then

              reconsider target9 = target as Vertex of G by GLIB_001: 18;

              (WB .first() ) = src & (WB .last() ) = target by A64, GLIB_001:def 23;

              then

              consider lenWB2h be odd Element of NAT such that

               A65: lenWB2h = (( len WB) - 2) and

               A66: ((WB .cut (1,lenWB2h)) .addEdge (WB . (lenWB2h + 1))) = WB by A19, GLIB_001: 127, GLIB_001: 133;

              

               A67: lenWB2h < (( len WB) - 0 ) by A65, XREAL_1: 15;

              set sa = (WB . lenWB2h), ea = (WB . (lenWB2h + 1));

              set WA = (WB .cut (1,lenWB2h));

              

               A68: 1 <= lenWB2h by ABIAN: 12;

              

               A69: (WB . 1) = (WB .first() ) by GLIB_001:def 6

              .= src by A64, GLIB_001:def 23;

              then WA is_Walk_from (src,sa) by A68, A67, GLIB_001: 37, JORDAN12: 2;

              then

              reconsider sa as Vertex of G by GLIB_001: 18;

              

               A70: ea DJoins (sa,(WB . (lenWB2h + 2)),G) by A67, GLIB_001: 122;

              then

               A71: ea DJoins (sa,(WB .last() ),G) by A65, GLIB_001:def 7;

              then ea DJoins (sa,target,G) by A64, GLIB_001:def 23;

              then ea Joins (sa,target9,G);

              then ea in (sa .edgesInOut() ) by GLIB_000: 62;

              then

               A72: ea in ((WA .last() ) .edgesInOut() ) by A68, A67, GLIB_001: 37, JORDAN12: 2;

              then

               A73: mc = ((WA .cost() ) + (( the_Weight_of G) . ea)) by A63, A66, GLIB_003: 25;

              reconsider WA as DPath of G;

              

               A74: (WA .first() ) = src by A68, A67, A69, GLIB_001: 37, JORDAN12: 2;

              

               A75: (WA .last() ) = sa by A68, A67, GLIB_001: 37, JORDAN12: 2;

              then

               A76: WA is_mincost_DPath_from (src,sa) by A62, A74, Th12;

              

               A77: ea DJoins (sa,target,G) by A64, A71, GLIB_001:def 23;

              

               A78: (WA .cost() ) = (G .min_DPath_cost (src,sa)) by A62, A74, A75, Th12, Th14;

              now

                defpred P[ Nat] means $1 is odd & $1 <= ( len WA) & not (WA . $1) in ( dom (Dn `1 ));

                

                 A79: (( the_Source_of G) . ea) = sa by A70;

                assume

                 A80: mc < (pc + ec);

                 A81:

                now

                  assume

                   A82: not sa in ( dom (Dn `1 ));

                  sa = (WA .last() ) by A68, A67, GLIB_001: 37, JORDAN12: 2

                  .= (WA . ( len WA)) by GLIB_001:def 7;

                  then

                   A83: ex k be Nat st P[k] by A82;

                  consider k be Nat such that

                   A84: P[k] & for m be Nat st P[m] holds k <= m from NAT_1:sch 5( A83);

                  reconsider k as odd Element of NAT by A84, ORDINAL1:def 12;

                  

                   A85: 1 <= k by ABIAN: 12;

                  (WA . 1) = (WA .first() ) by GLIB_001:def 6

                  .= src by A68, A67, A69, GLIB_001: 37, JORDAN12: 2;

                  then k <> 1 by A8, A84;

                  then 1 < k by A85, XXREAL_0: 1;

                  then (1 + 1) < (k + 1) by XREAL_1: 8;

                  then 2 <= k by NAT_1: 13;

                  then

                  reconsider k2a = (k - (2 * 1)) as odd Element of NAT by INT_1: 5;

                  set sk = (WA . k2a), ek = (WA . (k2a + 1)), tk = (WA . k);

                  

                   A86: k2a < (( len WA) - 0 ) by A84, XREAL_1: 15;

                  set WKA = (WA .cut (1,k)), WKB = (WA .cut (k,( len WA)));

                  set WK1 = (WA .cut (1,k2a));

                  reconsider WK1, WKA, WKB as DPath of G;

                  

                   A87: 1 <= k by ABIAN: 12;

                  

                  then

                   A88: (WKA .append WKB) = (WA .cut (1,( len WA))) by A84, GLIB_001: 38, JORDAN12: 2

                  .= WA by GLIB_001: 39;

                  

                   A89: k2a < (k - 0 ) by XREAL_1: 15;

                  then

                   A90: sk in ( dom (Dn `1 )) by A84, A86;

                  then

                  reconsider sk as Vertex of G;

                  

                   A91: 1 <= k2a by ABIAN: 12;

                  then

                   A92: (WK1 .last() ) = sk by A86, GLIB_001: 37, JORDAN12: 2;

                  (WK1 .first() ) = (WA . 1) by A91, A86, GLIB_001: 37, JORDAN12: 2;

                  then WK1 is_mincost_DPath_from ((WA . 1),sk) by A76, A92, Th12;

                  then WK1 is_mincost_DPath_from ((WA .first() ),sk) by GLIB_001:def 6;

                  then (G .min_DPath_cost (src,sk)) = (WK1 .cost() ) by A74, Th14;

                  then

                   A93: ((Dn `1 ) . sk) = (WK1 .cost() ) by A5, A84, A86, A89;

                  reconsider tk as Vertex of G by A84, GLIB_001: 7;

                  

                   A94: tk in (( the_Vertices_of G) \ ( dom (Dn `1 ))) by A84, XBOOLE_0:def 5;

                  tk = (WA . (k2a + 2));

                  then

                   A95: ek DJoins (sk,tk,G) by A86, GLIB_001: 122;

                  then

                   A96: (( the_Source_of G) . ek) = sk;

                  (WKB .first() ) = (WA . k) by A84, GLIB_001: 37

                  .= (WKA .last() ) by A84, A87, GLIB_001: 37, JORDAN12: 2;

                  then

                   A97: (WA .cost() ) = ((WKA .cost() ) + (WKB .cost() )) by A88, GLIB_003: 24;

                   0 <= (WKB .cost() ) by GLIB_003: 29;

                  then

                   A98: ( 0 qua Nat + (WKA .cost() )) <= (WA .cost() ) by A97, XREAL_1: 7;

                  ea in ( the_Edges_of G) by A70;

                  then

                   A99: 0 <= (( the_Weight_of G) . ea) by GLIB_003: 31;

                  ek in ( the_Edges_of G) & (( the_Target_of G) . ek) = tk by A95;

                  then ek DSJoins (( dom (Dn `1 )),(( the_Vertices_of G) \ ( dom (Dn `1 ))),G) by A90, A96, A94;

                  then

                   A100: (pc + ec) <= ((WK1 .cost() ) + (( the_Weight_of G) . ek)) by A15, A96, A93, Def7;

                  ek in ( the_Edges_of G) & (( the_Source_of G) . ek) = sk by A95;

                  then

                   A101: ek in (sk .edgesInOut() ) by GLIB_000: 61;

                  (k2a + 2) = k;

                  then (WK1 .addEdge ek) = WKA by A86, ABIAN: 12, GLIB_001: 41, JORDAN12: 2;

                  then (pc + ec) <= (WKA .cost() ) by A92, A100, A101, GLIB_003: 25;

                  then (pc + ec) <= (WA .cost() ) by A98, XXREAL_0: 2;

                  then ((pc + ec) + 0 qua Nat) <= ((WA .cost() ) + (( the_Weight_of G) . ea)) by A99, XREAL_1: 7;

                  hence contradiction by A63, A66, A72, A80, GLIB_003: 25;

                end;

                then

                 A102: (WA .cost() ) = ((Dn `1 ) . sa) by A5, A78;

                ea in ( the_Edges_of G) & (( the_Target_of G) . ea) = target by A77;

                then ea DSJoins (( dom (Dn `1 )),(( the_Vertices_of G) \ ( dom (Dn `1 ))),G) by A18, A81, A79;

                hence contradiction by A15, A73, A80, A102, A79, Def7;

              end;

              hence mc >= (pc + ec);

            end;

            then

             A103: (G .min_DPath_cost (src,target)) = (pc + ec) by XXREAL_0: 1;

            now

              let x be Vertex of Dn1W;

              now

                per cases by A26, XBOOLE_0:def 3;

                  suppose x in ( dom (Dn `1 ));

                  then

                  reconsider x9 = x as Vertex of DnW by A11, GLIB_000:def 37;

                  DnW is_mincost_DTree_rooted_at src by A5;

                  then

                  consider W2 be DPath of DnW such that

                   A104: W2 is_Walk_from (src,x9) and

                   A105: for W1 be DPath of G st W1 is_Walk_from (src,x9) holds (W2 .cost() ) <= (W1 .cost() );

                  reconsider W29 = W2 as DPath of Dn1W by A38, GLIB_001: 175;

                  take W29;

                  thus W29 is_Walk_from (src,x) by A104, GLIB_001: 19;

                  let W1 be DPath of G;

                  assume W1 is_Walk_from (src,x);

                  then (W2 .cost() ) <= (W1 .cost() ) by A105;

                  hence (W29 .cost() ) <= (W1 .cost() ) by A37, GLIB_003: 27;

                end;

                  suppose

                   A106: x in {target};

                  take W2;

                  thus W2 is_Walk_from (src,x) by A58, A106, TARSKI:def 1;

                  let W1 be DPath of G;

                  assume

                   A107: W1 is_Walk_from (src,x);

                  

                   A108: x = target by A106, TARSKI:def 1;

                  ex WX be DPath of G st WX is_mincost_DPath_from (src,target) & (WX .cost() ) = (W2 .cost() ) by A59, A60, A103, Def3;

                  hence (W2 .cost() ) <= (W1 .cost() ) by A108, A107;

                end;

              end;

              hence ex W2 be DPath of Dn1W st W2 is_Walk_from (src,x) & for W1 be DPath of G st W1 is_Walk_from (src,x) holds (W2 .cost() ) <= (W1 .cost() );

            end;

            hence Dn1W is_mincost_DTree_rooted_at src by A49;

            let v be Vertex of G;

            assume

             A109: v in ( dom (Dn1 `1 ));

            now

              per cases by A24, A109, XBOOLE_0:def 3;

                suppose

                 A110: v in ( dom (Dn `1 ));

                then

                 A111: (G .min_DPath_cost (src,v)) = ((Dn `1 ) . v) by A5;

                

                 A112: (Dn1 `1 ) = ((Dn `1 ) +* (target .--> (pc + ec))) by A23;

                 not v in ( dom (target .--> (pc + ec))) by A20, A110, TARSKI:def 1;

                hence (G .min_DPath_cost (src,v)) = ((Dn1 `1 ) . v) by A24, A109, A111, A112, FUNCT_4:def 1;

              end;

                suppose

                 A114: v in {target};

                (Dn1 `1 ) = ((Dn `1 ) +* (target .--> (pc + ec))) & ( dom (target .--> (pc + ec))) = {target} by A23;

                then

                 A115: ((Dn1 `1 ) . v) = ((target .--> (pc + ec)) . v) by A114, FUNCT_4: 13;

                v = target by A114, TARSKI:def 1;

                hence (G .min_DPath_cost (src,v)) = ((Dn1 `1 ) . v) by A103, A115, FUNCOP_1: 72;

              end;

            end;

            hence (G .min_DPath_cost (src,v)) = ((Dn1 `1 ) . v);

          end;

        end;

        hence Dn1W is_mincost_DTree_rooted_at src & for v be Vertex of G st v in ( dom (Dn1 `1 )) holds (G .min_DPath_cost (src,v)) = ((Dn1 `1 ) . v);

      end;

      then

       A116: for k be Nat st P[k] holds P[(k + 1)];

      

       A117: (D0 `2 ) = {} by A1;

      now

        let D0W be inducedWSubgraph of G, ( dom (D0 `1 )), (D0 `2 );

        

         A118: {} c= (G .edgesBetween ( dom (D0 `1 )));

        then

         A119: ( the_Vertices_of D0W) = {src} by A3, A117, GLIB_000:def 37;

        then ( card ( the_Vertices_of D0W)) = 1 by CARD_1: 30;

        then

         A120: D0W is _trivial;

         A121:

        now

          let x be Vertex of D0W;

          set W2 = (D0W .walkOf x);

          take W2;

          x = src by A119, TARSKI:def 1;

          hence W2 is_Walk_from (src,x) by GLIB_001: 13;

          let W1 be DPath of G;

          assume W1 is_Walk_from (src,x);

           0 <= (W1 .cost() ) by GLIB_003: 29;

          hence (W2 .cost() ) <= (W1 .cost() ) by GLIB_003: 21;

        end;

        ( the_Edges_of D0W) = {} by A2, A117, A118, GLIB_000:def 37;

        then (D0W .order() ) = ((D0W .size() ) + 1) by A119, CARD_1: 30;

        then D0W is Tree-like by A120, GLIB_002: 47;

        hence D0W is_mincost_DTree_rooted_at src by A121;

        let v be Vertex of G;

        assume

         A122: v in ( dom (D0 `1 ));

        then

         A123: v = src by A3, TARSKI:def 1;

         A124:

        now

          set W1 = (G .walkOf v);

          

           A125: W1 is_Walk_from (src,v) by A123, GLIB_001: 13;

          then

          consider W be DPath of G such that

           A126: W is_mincost_DPath_from (src,v) and

           A127: (G .min_DPath_cost (src,v)) = (W .cost() ) by Def3;

          (W1 .cost() ) = 0 by GLIB_003: 21;

          then (W .cost() ) <= 0 by A125, A126;

          hence (G .min_DPath_cost (src,v)) = 0 by A127, GLIB_003: 29;

        end;

        ((D0 `1 ) . src) = 0 by A2;

        hence (G .min_DPath_cost (src,v)) = ((D0 `1 ) . v) by A3, A122, A124, TARSKI:def 1;

      end;

      then

       A128: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A128, A116);

      hence thesis;

    end;

    theorem :: GLIB_004:24

    

     Th24: for G be _finite real-weighted WGraph, s be Vertex of G holds ( DIJK:CompSeq s) is halting

    proof

      let G be _finite real-weighted WGraph, src be Vertex of G;

      set DCS = ( DIJK:CompSeq src);

      now

        set RSize = ( card (G .reachableDFrom src));

        take n = ( card (G .reachableDFrom src));

        set Gn = (DCS . n), Gn1a = (DCS . (n + 1));

        set BestEdges = ( DIJK:NextBestEdges Gn);

        

         A1: Gn1a = ( DIJK:Step Gn) by Def11;

        now

          per cases ;

            suppose BestEdges = {} ;

            hence (DCS . n) = (DCS . (n + 1)) by A1, Def8;

          end;

            suppose

             A2: BestEdges <> {} ;

            ( card ( dom ((DCS . n) `1 ))) = ( min ((n + 1),RSize)) & RSize <= (RSize + 1) by Th21, NAT_1: 11;

            then

             A3: ( card ( dom (Gn `1 ))) = RSize by XXREAL_0:def 9;

            (RSize + 1) <= ((RSize + 1) + 1) & RSize <= (RSize + 1) by NAT_1: 11;

            then

             A4: RSize <= ((n + 1) + 1) by XXREAL_0: 2;

            

             A5: ( card ( dom (Gn1a `1 ))) = ( min (((n + 1) + 1),RSize)) by Th21

            .= RSize by A4, XXREAL_0:def 9;

            ( card ( dom (( DIJK:Step Gn) `1 ))) = (( card ( dom (Gn `1 ))) + 1) by A2, Th15;

            hence (DCS . n) = (DCS . (n + 1)) by A3, A5, Def11;

          end;

        end;

        hence (DCS . n) = (DCS . (n + 1));

      end;

      hence thesis;

    end;

    registration

      let G be _finite real-weighted WGraph, src be Vertex of G;

      cluster ( DIJK:CompSeq src) -> halting;

      coherence by Th24;

    end

    theorem :: GLIB_004:25

    

     Th25: for G be _finite real-weighted WGraph, s be Vertex of G holds ((( DIJK:CompSeq s) .Lifespan() ) + 1) = ( card (G .reachableDFrom s))

    proof

      let G be _finite real-weighted WGraph, src be Vertex of G;

      set DCS = ( DIJK:CompSeq src), RFS = (G .reachableDFrom src);

      consider k be Nat such that

       A1: ( card RFS) = (k + 1) by NAT_1: 6;

      reconsider k as Element of NAT by ORDINAL1:def 12;

       A2:

      now

        let n be Nat;

        set Gn = (DCS . n), Gn1 = (DCS . (n + 1));

        assume

         A3: (DCS . n) = (DCS . (n + 1));

        now

          assume n < k;

          then

           A4: (n + 1) < ( card RFS) by A1, XREAL_1: 8;

          then

           A5: ((n + 1) + 1) <= ( card RFS) by NAT_1: 13;

          ( card ( dom (Gn `1 ))) = ( min ((n + 1),( card RFS))) by Th21;

          then

           A6: ( card ( dom (Gn `1 ))) = (n + 1) by A4, XXREAL_0:def 9;

          ( card ( dom (Gn1 `1 ))) = ( min (((n + 1) + 1),( card RFS))) by Th21;

          then ( 0 + (n + 1)) = (1 + (n + 1)) by A3, A6, A5, XXREAL_0:def 9;

          hence contradiction;

        end;

        hence k <= n;

      end;

      set Gk = (DCS . k), Gk1 = (DCS . (k + 1));

      

       A7: ( card RFS) <= (( card RFS) + 1) by NAT_1: 11;

      

       A8: Gk1 = ( DIJK:Step Gk) by Def11;

      ( card ( dom (Gk1 `1 ))) = ( min ((( card RFS) + 1),( card RFS))) & ( card ( dom (Gk `1 ))) = ( min (( card RFS),( card RFS))) by A1, Th21;

      then ( card ( dom (Gk1 `1 ))) = ( card ( dom (Gk `1 ))) by A7, XXREAL_0:def 9;

      then ( DIJK:NextBestEdges Gk) = {} by A8, Th15;

      then (DCS . k) = (DCS . (k + 1)) by A8, Def8;

      hence thesis by A1, A2, GLIB_000:def 56;

    end;

    theorem :: GLIB_004:26

    

     Th26: for G be _finite real-weighted WGraph, s be Vertex of G holds ( dom (( DIJK:SSSP (G,s)) `1 )) = (G .reachableDFrom s)

    proof

      let G be _finite real-weighted WGraph, src be Vertex of G;

      set Gn = ( DIJK:SSSP (G,src)), RFS = (G .reachableDFrom src);

      set DCS = ( DIJK:CompSeq src), n = (DCS .Lifespan() );

      

       A1: ( card ( dom (Gn `1 ))) = ( min ((n + 1),( card RFS))) by Th21

      .= ( min (( card RFS),( card RFS))) by Th25

      .= ( card RFS);

      now

        assume

         A2: ( dom (Gn `1 )) <> RFS;

        ( dom (Gn `1 )) c= RFS by Th19;

        then ( dom (Gn `1 )) c< RFS by A2, XBOOLE_0:def 8;

        hence contradiction by A1, TREES_1: 6;

      end;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: GLIB_004:27

    for G be _finite nonnegative-weighted WGraph, s be Vertex of G, G2 be inducedWSubgraph of G, ( dom (( DIJK:SSSP (G,s)) `1 )), (( DIJK:SSSP (G,s)) `2 ) holds G2 is_mincost_DTree_rooted_at s & for v be Vertex of G st v in (G .reachableDFrom s) holds v in ( the_Vertices_of G2) & (G .min_DPath_cost (s,v)) = ((( DIJK:SSSP (G,s)) `1 ) . v)

    proof

      let G be _finite nonnegative-weighted WGraph, src be Vertex of G, G2 be inducedWSubgraph of G, ( dom (( DIJK:SSSP (G,src)) `1 )), (( DIJK:SSSP (G,src)) `2 );

      set Res = ( DIJK:SSSP (G,src));

      set dR = ( dom (Res `1 ));

      thus G2 is_mincost_DTree_rooted_at src by Th23;

      let v be Vertex of G;

      assume v in (G .reachableDFrom src);

      then

       A1: v in dR by Th26;

      (Res `2 ) c= (G .edgesBetween dR) by Th22;

      hence v in ( the_Vertices_of G2) by A1, GLIB_000:def 37;

      thus thesis by A1, Th23;

    end;

    begin

    definition

      let G be _Graph;

      mode PRIM:Labeling of G is Element of [:( bool ( the_Vertices_of G)), ( bool ( the_Edges_of G)):];

    end

    registration

      let G be _finite _Graph, L be PRIM:Labeling of G;

      cluster (L `1 ) -> finite;

      coherence ;

      cluster (L `2 ) -> finite;

      coherence ;

    end

    definition

      let G be real-weighted WGraph, L be PRIM:Labeling of G;

      :: GLIB_004:def13

      func PRIM:NextBestEdges (L) -> Subset of ( the_Edges_of G) means

      : Def13: for e1 be set holds e1 in it iff e1 SJoins ((L `1 ),(( the_Vertices_of G) \ (L `1 )),G) & for e2 be set st e2 SJoins ((L `1 ),(( the_Vertices_of G) \ (L `1 )),G) holds (( the_Weight_of G) . e1) <= (( the_Weight_of G) . e2);

      existence

      proof

        defpred P[ set] means $1 SJoins ((L `1 ),(( the_Vertices_of G) \ (L `1 )),G) & for e2 be set st e2 SJoins ((L `1 ),(( the_Vertices_of G) \ (L `1 )),G) holds (( the_Weight_of G) . $1) <= (( the_Weight_of G) . e2);

        consider IT be Subset of ( the_Edges_of G) such that

         A1: for e1 be set holds e1 in IT iff e1 in ( the_Edges_of G) & P[e1] from SUBSET_1:sch 1;

        take IT;

        let e1 be set;

        thus e1 in IT implies P[e1] by A1;

        assume

         A2: P[e1];

        then e1 in ( the_Edges_of G) by GLIB_000:def 15;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        defpred P[ set] means $1 SJoins ((L `1 ),(( the_Vertices_of G) \ (L `1 )),G) & for e2 be set st e2 SJoins ((L `1 ),(( the_Vertices_of G) \ (L `1 )),G) holds (( the_Weight_of G) . $1) <= (( the_Weight_of G) . e2);

        let IT1,IT2 be Subset of ( the_Edges_of G) such that

         A3: for e1 be set holds e1 in IT1 iff e1 SJoins ((L `1 ),(( the_Vertices_of G) \ (L `1 )),G) & for e2 be set st e2 SJoins ((L `1 ),(( the_Vertices_of G) \ (L `1 )),G) holds (( the_Weight_of G) . e1) <= (( the_Weight_of G) . e2) and

         A4: for e1 be set holds e1 in IT2 iff e1 SJoins ((L `1 ),(( the_Vertices_of G) \ (L `1 )),G) & for e2 be set st e2 SJoins ((L `1 ),(( the_Vertices_of G) \ (L `1 )),G) holds (( the_Weight_of G) . e1) <= (( the_Weight_of G) . e2);

        now

          let e1 be object;

          reconsider ee = e1 as set by TARSKI: 1;

          hereby

            assume e1 in IT1;

            then P[ee] by A3;

            hence e1 in IT2 by A4;

          end;

          assume e1 in IT2;

          then P[ee] by A4;

          hence e1 in IT1 by A3;

        end;

        hence thesis by TARSKI: 2;

      end;

    end

    definition

      let G be real-weighted WGraph;

      :: GLIB_004:def14

      func PRIM:Init (G) -> PRIM:Labeling of G equals [ { the Element of ( the_Vertices_of G)}, {} ];

      coherence

      proof

         {} c= ( the_Edges_of G);

        hence thesis by ZFMISC_1:def 2;

      end;

    end

    definition

      let G be real-weighted WGraph, L be PRIM:Labeling of G;

      :: GLIB_004:def15

      func PRIM:Step (L) -> PRIM:Labeling of G equals

      : Def15: L if ( PRIM:NextBestEdges L) = {} ,

[((L `1 ) \/ {(( the_Target_of G) . the Element of ( PRIM:NextBestEdges L))}), ((L `2 ) \/ { the Element of ( PRIM:NextBestEdges L)})] if ( PRIM:NextBestEdges L) <> {} & (( the_Source_of G) . the Element of ( PRIM:NextBestEdges L)) in (L `1 )

      otherwise [((L `1 ) \/ {(( the_Source_of G) . the Element of ( PRIM:NextBestEdges L))}), ((L `2 ) \/ { the Element of ( PRIM:NextBestEdges L)})];

      coherence

      proof

        set V = ( the_Vertices_of G), E = ( the_Edges_of G);

        set BE = ( PRIM:NextBestEdges L), e = the Element of BE;

        set s = (( the_Source_of G) . e), t = (( the_Target_of G) . e);

         A1:

        now

          assume that

           A2: BE <> {} and not (( the_Source_of G) . e) in (L `1 );

          e in BE by A2;

          then

          reconsider s9 = s as Element of V by FUNCT_2: 5;

          

           A3: ((L `1 ) \/ {s9}) c= V;

          

           A4: {e} c= E

          proof

            let x be object;

            assume x in {e};

            then x = e by TARSKI:def 1;

            then x in BE by A2;

            hence thesis;

          end;

          ((L `2 ) \/ {e}) c= E by A4, XBOOLE_1: 8;

          hence [((L `1 ) \/ {s}), ((L `2 ) \/ {e})] is PRIM:Labeling of G by A3, ZFMISC_1:def 2;

        end;

        now

          assume that

           A5: BE <> {} and (( the_Source_of G) . e) in (L `1 );

          e in BE by A5;

          then

          reconsider t9 = t as Element of V by FUNCT_2: 5;

          

           A6: ((L `1 ) \/ {t9}) c= V;

          

           A7: {e} c= E

          proof

            let x be object;

            assume x in {e};

            then x = e by TARSKI:def 1;

            then x in BE by A5;

            hence thesis;

          end;

          ((L `2 ) \/ {e}) c= E by A7, XBOOLE_1: 8;

          hence [((L `1 ) \/ {t}), ((L `2 ) \/ {e})] is PRIM:Labeling of G by A6, ZFMISC_1:def 2;

        end;

        hence thesis by A1;

      end;

      consistency ;

    end

    definition

      let G be real-weighted WGraph;

      :: GLIB_004:def16

      mode PRIM:LabelingSeq of G -> ManySortedSet of NAT means

      : Def16: for n be Nat holds (it . n) is PRIM:Labeling of G;

      existence

      proof

        defpred P[ object, object] means $2 is PRIM:Labeling of G;

         A1:

        now

          let i be object;

          assume i in NAT ;

          reconsider r = [ {} , {} ] as object;

          take r;

           {} c= ( the_Vertices_of G) & {} c= ( the_Edges_of G);

          hence P[i, r] by ZFMISC_1:def 2;

        end;

        consider s be ManySortedSet of NAT such that

         A2: for i be object st i in NAT holds P[i, (s . i)] from PBOOLE:sch 3( A1);

        take s;

        let i be Nat;

        i in NAT by ORDINAL1:def 12;

        hence thesis by A2;

      end;

    end

    definition

      let G be real-weighted WGraph, S be PRIM:LabelingSeq of G, n be Nat;

      :: original: .

      redefine

      func S . n -> PRIM:Labeling of G ;

      coherence by Def16;

    end

    definition

      let G be real-weighted WGraph;

      :: GLIB_004:def17

      func PRIM:CompSeq (G) -> PRIM:LabelingSeq of G means

      : Def17: (it . 0 ) = ( PRIM:Init G) & for n be Nat holds (it . (n + 1)) = ( PRIM:Step (it . n));

      existence

      proof

        defpred P[ set, set, set] means ($2 is PRIM:Labeling of G & ex Gn,Gn1 be PRIM:Labeling of G st $2 = Gn & $3 = Gn1 & Gn1 = ( PRIM:Step Gn)) or ( not $2 is PRIM:Labeling of G & $2 = $3);

        now

          let n be Nat, x be set;

          per cases ;

            suppose x is PRIM:Labeling of G;

            then

            reconsider Gn = x as PRIM:Labeling of G;

             P[n, x, ( PRIM:Step Gn)];

            hence ex y be set st P[n, x, y];

          end;

            suppose not x is PRIM:Labeling of G;

            hence ex y be set st P[n, x, y];

          end;

        end;

        then

         A1: for n be Nat holds for x be set holds ex y be set st P[n, x, y];

        consider IT be Function such that

         A2: ( dom IT) = NAT & (IT . 0 ) = ( PRIM:Init G) & for n be Nat holds P[n, (IT . n), (IT . (n + 1))] from RECDEF_1:sch 1( A1);

        reconsider IT as ManySortedSet of NAT by A2, PARTFUN1:def 2, RELAT_1:def 18;

        defpred P2[ Nat] means (IT . $1) is PRIM:Labeling of G;

         A3:

        now

          let n be Nat;

          reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

          assume P2[n];

          then ex Gn,Gn1 be PRIM:Labeling of G st (IT . n9) = Gn & (IT . (n + 1)) = Gn1 & Gn1 = ( PRIM:Step Gn) by A2;

          hence P2[(n + 1)];

        end;

        

         A4: P2[ 0 ] by A2;

        for n be Nat holds P2[n] from NAT_1:sch 2( A4, A3);

        then

        reconsider IT as PRIM:LabelingSeq of G by Def16;

        take IT;

        thus (IT . 0 ) = ( PRIM:Init G) by A2;

        let n be Nat;

        reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

        ex Gn,Gn1 be PRIM:Labeling of G st (IT . n9) = Gn & (IT . (n + 1)) = Gn1 & Gn1 = ( PRIM:Step Gn) by A2;

        hence thesis;

      end;

      uniqueness

      proof

        let IT1,IT2 be PRIM:LabelingSeq of G such that

         A5: (IT1 . 0 ) = ( PRIM:Init G) and

         A6: for n be Nat holds (IT1 . (n + 1)) = ( PRIM:Step (IT1 . n)) and

         A7: (IT2 . 0 ) = ( PRIM:Init G) and

         A8: for n be Nat holds (IT2 . (n + 1)) = ( PRIM:Step (IT2 . n));

        defpred P[ Nat] means (IT1 . $1) = (IT2 . $1);

        now

          let n be Nat;

          assume P[n];

          

          then (IT1 . (n + 1)) = ( PRIM:Step (IT2 . n)) by A6

          .= (IT2 . (n + 1)) by A8;

          hence P[(n + 1)];

        end;

        then

         A9: for n be Nat st P[n] holds P[(n + 1)];

        

         A10: P[ 0 ] by A5, A7;

        for n be Nat holds P[n] from NAT_1:sch 2( A10, A9);

        then for n be object st n in NAT holds (IT1 . n) = (IT2 . n);

        hence IT1 = IT2 by PBOOLE: 3;

      end;

    end

    definition

      let G be real-weighted WGraph;

      :: GLIB_004:def18

      func PRIM:MST (G) -> PRIM:Labeling of G equals (( PRIM:CompSeq G) .Result() );

      coherence

      proof

        set PCS = ( PRIM:CompSeq G);

        (PCS .Result() ) = (PCS . (PCS .Lifespan() ));

        hence thesis;

      end;

    end

    theorem :: GLIB_004:28

    

     Th28: for G be real-weighted WGraph, L be PRIM:Labeling of G st ( PRIM:NextBestEdges L) <> {} holds ex v be Vertex of G st not v in (L `1 ) & ( PRIM:Step L) = [((L `1 ) \/ {v}), ((L `2 ) \/ { the Element of ( PRIM:NextBestEdges L)})]

    proof

      let G be real-weighted WGraph, L be PRIM:Labeling of G;

      set G2 = ( PRIM:Step L);

      set e = the Element of ( PRIM:NextBestEdges L);

      set src = (( the_Source_of G) . e), tar = (( the_Target_of G) . e);

      assume

       A1: ( PRIM:NextBestEdges L) <> {} ;

      then e in ( PRIM:NextBestEdges L);

      then

      reconsider src, tar as Vertex of G by FUNCT_2: 5;

      

       A2: e SJoins ((L `1 ),(( the_Vertices_of G) \ (L `1 )),G) by A1, Def13;

      now

        per cases ;

          suppose

           A3: src in (L `1 );

          take tar;

           not src in (( the_Vertices_of G) \ (L `1 )) by A3, XBOOLE_0:def 5;

          then tar in (( the_Vertices_of G) \ (L `1 )) by A2;

          hence not tar in (L `1 ) by XBOOLE_0:def 5;

          thus G2 = [((L `1 ) \/ {tar}), ((L `2 ) \/ {e})] by A1, A3, Def15;

        end;

          suppose

           A4: not src in (L `1 );

          take src;

          thus not src in (L `1 ) by A4;

          thus G2 = [((L `1 ) \/ {src}), ((L `2 ) \/ {e})] by A1, A4, Def15;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_004:29

    

     Th29: for G be real-weighted WGraph, L be PRIM:Labeling of G holds (L `1 ) c= (( PRIM:Step L) `1 ) & (L `2 ) c= (( PRIM:Step L) `2 )

    proof

      let G be real-weighted WGraph, L be PRIM:Labeling of G;

      set G2 = ( PRIM:Step L);

      set Next = ( PRIM:NextBestEdges L), e = the Element of Next;

      now

        per cases ;

          suppose Next = {} ;

          hence thesis by Def15;

        end;

          suppose Next <> {} ;

          then

          consider v be Vertex of G such that not v in (L `1 ) and

           A1: G2 = [((L `1 ) \/ {v}), ((L `2 ) \/ {e})] by Th28;

          (G2 `1 ) = ((L `1 ) \/ {v}) by A1;

          hence (L `1 ) c= (G2 `1 ) by XBOOLE_1: 7;

          (G2 `2 ) = ((L `2 ) \/ {e}) by A1;

          hence (L `2 ) c= (G2 `2 ) by XBOOLE_1: 7;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_004:30

    

     Th30: for G be _finite real-weighted WGraph, n be 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 ))

    proof

      let G be _finite real-weighted WGraph;

      set PCS = ( PRIM:CompSeq G);

      defpred P[ Nat] means ((PCS . $1) `1 ) is non empty Subset of ( the_Vertices_of G) & ((PCS . $1) `2 ) c= (G .edgesBetween ((PCS . $1) `1 ));

      

       A1: ((PCS . 0 ) `2 ) = (( PRIM:Init G) `2 ) by Def17

      .= {} ;

      now

        let n be Nat;

        assume

         A2: P[n];

        set Gn = (PCS . n), Gn1 = (PCS . (n + 1));

        set Next = ( PRIM:NextBestEdges Gn), e = the Element of Next;

        

         A3: Gn1 = ( PRIM:Step Gn) by Def17;

        now

          per cases ;

            suppose Next = {} ;

            then Gn1 = Gn by A3, Def15;

            hence P[(n + 1)] by A2;

          end;

            suppose

             A4: Next <> {} ;

            set src = (( the_Source_of G) . e), tar = (( the_Target_of G) . e);

            

             A5: e in Next by A4;

            

             A6: e SJoins ((Gn `1 ),(( the_Vertices_of G) \ (Gn `1 )),G) by A4, Def13;

            now

              per cases ;

                suppose

                 A7: (( the_Source_of G) . e) in (Gn `1 );

                then

                 A8: Gn1 = [((Gn `1 ) \/ {tar}), ((Gn `2 ) \/ {e})] by A3, A4, Def15;

                then

                 A9: (Gn1 `1 ) = ((Gn `1 ) \/ {tar});

                then

                 A10: (G .edgesBetween (Gn `1 )) c= (G .edgesBetween (Gn1 `1 )) by GLIB_000: 36, XBOOLE_1: 7;

                thus (Gn1 `1 ) is non empty Subset of ( the_Vertices_of G) by A8;

                

                 A11: (Gn1 `2 ) = ((Gn `2 ) \/ {e}) by A8;

                

                 A12: (Gn `1 ) c= (Gn1 `1 ) by A9, XBOOLE_1: 7;

                now

                  let x be object;

                  assume

                   A13: x in (Gn1 `2 );

                  now

                    per cases by A11, A13, XBOOLE_0:def 3;

                      suppose x in (Gn `2 );

                      then x in (G .edgesBetween (Gn `1 )) by A2;

                      hence x in (G .edgesBetween (Gn1 `1 )) by A10;

                    end;

                      suppose x in {e};

                      then

                       A14: x = e by TARSKI:def 1;

                      then (( the_Target_of G) . x) in {tar} by TARSKI:def 1;

                      then (( the_Target_of G) . x) in (Gn1 `1 ) by A9, XBOOLE_0:def 3;

                      hence x in (G .edgesBetween (Gn1 `1 )) by A5, A7, A12, A14, GLIB_000: 31;

                    end;

                  end;

                  hence x in (G .edgesBetween (Gn1 `1 ));

                end;

                hence (Gn1 `2 ) c= (G .edgesBetween (Gn1 `1 ));

              end;

                suppose

                 A15: not (( the_Source_of G) . e) in (Gn `1 );

                then

                 A16: tar in (Gn `1 ) by A6;

                

                 A17: Gn1 = [((Gn `1 ) \/ {(( the_Source_of G) . e)}), ((Gn `2 ) \/ {e})] by A3, A4, A15, Def15;

                then

                 A18: (Gn1 `1 ) = ((Gn `1 ) \/ {src});

                then

                 A19: (G .edgesBetween (Gn `1 )) c= (G .edgesBetween (Gn1 `1 )) by GLIB_000: 36, XBOOLE_1: 7;

                thus (Gn1 `1 ) is non empty Subset of ( the_Vertices_of G) by A17;

                

                 A20: (Gn1 `2 ) = ((Gn `2 ) \/ {e}) by A17;

                

                 A21: (Gn `1 ) c= (Gn1 `1 ) by A18, XBOOLE_1: 7;

                now

                  let x be object;

                  assume

                   A22: x in (Gn1 `2 );

                  now

                    per cases by A20, A22, XBOOLE_0:def 3;

                      suppose x in (Gn `2 );

                      then x in (G .edgesBetween (Gn `1 )) by A2;

                      hence x in (G .edgesBetween (Gn1 `1 )) by A19;

                    end;

                      suppose x in {e};

                      then

                       A23: x = e by TARSKI:def 1;

                      then (( the_Source_of G) . x) in {src} by TARSKI:def 1;

                      then (( the_Source_of G) . x) in (Gn1 `1 ) by A18, XBOOLE_0:def 3;

                      hence x in (G .edgesBetween (Gn1 `1 )) by A5, A21, A16, A23, GLIB_000: 31;

                    end;

                  end;

                  hence x in (G .edgesBetween (Gn1 `1 ));

                end;

                hence (Gn1 `2 ) c= (G .edgesBetween (Gn1 `1 ));

              end;

            end;

            hence P[(n + 1)];

          end;

        end;

        hence P[(n + 1)];

      end;

      then

       A24: for n be Nat st P[n] holds P[(n + 1)];

      ((PCS . 0 ) `1 ) = (( PRIM:Init G) `1 ) by Def17

      .= { the Element of ( the_Vertices_of G)};

      then

       A25: P[ 0 ] by A1, XBOOLE_1: 2;

      for n be Nat holds P[n] from NAT_1:sch 2( A25, A24);

      hence thesis;

    end;

    theorem :: GLIB_004:31

    

     Th31: for G1 be _finite real-weighted WGraph, n be Nat, G2 be inducedSubgraph of G1, ((( PRIM:CompSeq G1) . n) `1 ), ((( PRIM:CompSeq G1) . n) `2 ) holds G2 is connected

    proof

      let G1 be _finite real-weighted WGraph;

      defpred P[ Nat] means for G2 be inducedSubgraph of G1, ((( PRIM:CompSeq G1) . $1) `1 ), ((( PRIM:CompSeq G1) . $1) `2 ) holds G2 is connected;

      set G0 = (( PRIM:CompSeq G1) . 0 ), v = the Element of ( the_Vertices_of G1);

      now

        let n be Nat;

        assume

         A1: P[n];

        set Gn = (( PRIM:CompSeq G1) . n), Gn1 = (( PRIM:CompSeq G1) . (n + 1));

        set e = the Element of ( PRIM:NextBestEdges Gn);

        set v1 = (( the_Target_of G1) . e), v2 = (( the_Source_of G1) . e);

        

         A2: Gn1 = ( PRIM:Step Gn) by Def17;

        now

          let Gn1s be inducedSubgraph of G1, (Gn1 `1 ), (Gn1 `2 );

          

           A3: (Gn1 `1 ) is non empty Subset of ( the_Vertices_of G1) & (Gn1 `2 ) c= (G1 .edgesBetween (Gn1 `1 )) by Th30;

          then

           A4: ( the_Vertices_of Gn1s) = (Gn1 `1 ) by GLIB_000:def 37;

          

           A5: ( the_Edges_of Gn1s) = (Gn1 `2 ) by A3, GLIB_000:def 37;

          now

            per cases ;

              suppose ( PRIM:NextBestEdges Gn) = {} ;

              then Gn1 = Gn by A2, Def15;

              hence Gn1s is connected by A1;

            end;

              suppose

               A6: ( PRIM:NextBestEdges Gn) <> {} & v2 in (Gn `1 );

              then

               A7: Gn1 = [((Gn `1 ) \/ {v1}), ((Gn `2 ) \/ {e})] by A2, Def15;

              then

               A8: (Gn1 `2 ) = ((Gn `2 ) \/ {e});

              

               A9: e in ( PRIM:NextBestEdges Gn) by A6;

              then

              reconsider v1 as Vertex of G1 by FUNCT_2: 5;

              

               A10: e Joins (v2,v1,G1) by A9;

              set Gns = the inducedSubgraph of G1, (Gn `1 ), (Gn `2 );

              

               A11: Gns is connected by A1;

              

               A12: (Gn `1 ) is non empty Subset of ( the_Vertices_of G1) & (Gn `2 ) c= (G1 .edgesBetween (Gn `1 )) by Th30;

              then

               A13: ( the_Vertices_of Gns) = (Gn `1 ) by GLIB_000:def 37;

              

               A14: (Gn1 `1 ) = ((Gn `1 ) \/ {v1}) by A7;

              then

               A15: ( the_Vertices_of Gns) c= ( the_Vertices_of Gn1s) by A4, A13, XBOOLE_1: 7;

              ( the_Edges_of Gns) = (Gn `2 ) by A12, GLIB_000:def 37;

              then

              reconsider Gns as Subgraph of Gn1s by A5, A8, A15, GLIB_000: 44, XBOOLE_1: 7;

              set src = the Vertex of Gns;

              reconsider src9 = src as Vertex of Gn1s by GLIB_000: 42;

              e in {e} by TARSKI:def 1;

              then e in ( the_Edges_of Gn1s) by A5, A8, XBOOLE_0:def 3;

              then

               A16: e Joins (v2,v1,Gn1s) by A10, GLIB_000: 73;

              now

                let x be Vertex of Gn1s;

                now

                  per cases ;

                    suppose

                     A17: x = v1;

                    reconsider v29 = v2 as Vertex of Gns by A6, A12, GLIB_000:def 37;

                    consider W be Walk of Gns such that

                     A18: W is_Walk_from (src,v29) by A11, GLIB_002:def 1;

                    reconsider W as Walk of Gn1s by GLIB_001: 167;

                    W is_Walk_from (src9,v2) by A18, GLIB_001: 19;

                    then (W .addEdge e) is_Walk_from (src9,x) by A16, A17, GLIB_001: 66;

                    hence ex W be Walk of Gn1s st W is_Walk_from (src9,x);

                  end;

                    suppose x <> v1;

                    then not x in {v1} by TARSKI:def 1;

                    then

                    reconsider x9 = x as Vertex of Gns by A4, A14, A13, XBOOLE_0:def 3;

                    consider W be Walk of Gns such that

                     A19: W is_Walk_from (src,x9) by A11, GLIB_002:def 1;

                    reconsider W9 = W as Walk of Gn1s by GLIB_001: 167;

                    W9 is_Walk_from (src9,x) by A19, GLIB_001: 19;

                    hence ex W be Walk of Gn1s st W is_Walk_from (src9,x);

                  end;

                end;

                hence ex W be Walk of Gn1s st W is_Walk_from (src9,x);

              end;

              hence Gn1s is connected by GLIB_002: 6;

            end;

              suppose

               A20: ( PRIM:NextBestEdges Gn) <> {} & not v2 in (Gn `1 );

              then

               A21: Gn1 = [((Gn `1 ) \/ {v2}), ((Gn `2 ) \/ {e})] by A2, Def15;

              then

               A22: (Gn1 `2 ) = ((Gn `2 ) \/ {e});

              

               A23: e SJoins ((Gn `1 ),(( the_Vertices_of G1) \ (Gn `1 )),G1) by A20, Def13;

              then

               A24: e in ( the_Edges_of G1);

              then

              reconsider v2 as Vertex of G1 by FUNCT_2: 5;

              

               A25: e Joins (v1,v2,G1) by A24;

              e in {e} by TARSKI:def 1;

              then e in ( the_Edges_of Gn1s) by A5, A22, XBOOLE_0:def 3;

              then

               A26: e Joins (v1,v2,Gn1s) by A25, GLIB_000: 73;

              set Gns = the inducedSubgraph of G1, (Gn `1 ), (Gn `2 );

              

               A27: Gns is connected by A1;

              

               A28: (Gn `1 ) is non empty Subset of ( the_Vertices_of G1) & (Gn `2 ) c= (G1 .edgesBetween (Gn `1 )) by Th30;

              then

               A29: ( the_Vertices_of Gns) = (Gn `1 ) by GLIB_000:def 37;

              

               A30: (Gn1 `1 ) = ((Gn `1 ) \/ {v2}) by A21;

              then

               A31: ( the_Vertices_of Gns) c= ( the_Vertices_of Gn1s) by A4, A29, XBOOLE_1: 7;

              ( the_Edges_of Gns) = (Gn `2 ) by A28, GLIB_000:def 37;

              then

              reconsider Gns as Subgraph of Gn1s by A5, A22, A31, GLIB_000: 44, XBOOLE_1: 7;

              set src = the Vertex of Gns;

              reconsider src9 = src as Vertex of Gn1s by GLIB_000: 42;

              

               A32: v1 in (Gn `1 ) by A20, A23;

              now

                let x be Vertex of Gn1s;

                now

                  per cases ;

                    suppose

                     A33: x = v2;

                    reconsider v19 = v1 as Vertex of Gns by A32, A28, GLIB_000:def 37;

                    consider W be Walk of Gns such that

                     A34: W is_Walk_from (src,v19) by A27, GLIB_002:def 1;

                    reconsider W as Walk of Gn1s by GLIB_001: 167;

                    W is_Walk_from (src9,v1) by A34, GLIB_001: 19;

                    then (W .addEdge e) is_Walk_from (src9,x) by A26, A33, GLIB_001: 66;

                    hence ex W be Walk of Gn1s st W is_Walk_from (src9,x);

                  end;

                    suppose x <> v2;

                    then not x in {v2} by TARSKI:def 1;

                    then

                    reconsider x9 = x as Vertex of Gns by A4, A30, A29, XBOOLE_0:def 3;

                    consider W be Walk of Gns such that

                     A35: W is_Walk_from (src,x9) by A27, GLIB_002:def 1;

                    reconsider W9 = W as Walk of Gn1s by GLIB_001: 167;

                    W9 is_Walk_from (src9,x) by A35, GLIB_001: 19;

                    hence ex W be Walk of Gn1s st W is_Walk_from (src9,x);

                  end;

                end;

                hence ex W be Walk of Gn1s st W is_Walk_from (src9,x);

              end;

              hence Gn1s is connected by GLIB_002: 6;

            end;

          end;

          hence Gn1s is connected;

        end;

        hence P[(n + 1)];

      end;

      then

       A36: for n be Nat st P[n] holds P[(n + 1)];

      now

        let G be inducedSubgraph of G1, (G0 `1 ), (G0 `2 );

        G0 = ( PRIM:Init G1) by Def17;

        then

        reconsider G9 = G as inducedSubgraph of G1, {v}, {} ;

        G9 is connected;

        hence G is connected;

      end;

      then

       A38: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A38, A36);

      hence thesis;

    end;

    theorem :: GLIB_004:32

    

     Th32: for G1 be _finite real-weighted WGraph, n be Nat, G2 be inducedSubgraph of G1, ((( PRIM:CompSeq G1) . n) `1 ) holds G2 is connected

    proof

      let G1 be _finite real-weighted WGraph, n be Nat;

      set V = ((( PRIM:CompSeq G1) . n) `1 );

      let G2 be inducedSubgraph of G1, V;

      reconsider V as non empty Subset of ( the_Vertices_of G1) by Th30;

      set E = ((( PRIM:CompSeq G1) . n) `2 );

      reconsider E as Subset of (G1 .edgesBetween V) by Th30;

      set G3 = the inducedSubgraph of G1, V, E;

      

       A1: ( the_Vertices_of G3) = V & ( the_Vertices_of G2) = V by GLIB_000:def 37;

      ( the_Edges_of G3) = E & ( the_Edges_of G2) = (G1 .edgesBetween V) by GLIB_000:def 37;

      then

      reconsider G3 as Subgraph of G2 by A1, GLIB_000: 44;

      

       A2: G3 is spanning by A1;

      G3 is connected by Th31;

      hence thesis by A2, GLIB_002: 23;

    end;

    registration

      let G1 be _finite real-weighted WGraph, n be Nat;

      cluster -> connected for inducedSubgraph of G1, ((( PRIM:CompSeq G1) . n) `1 );

      coherence by Th32;

    end

    registration

      let G1 be _finite real-weighted WGraph, n be Nat;

      cluster -> connected for inducedSubgraph of G1, ((( PRIM:CompSeq G1) . n) `1 ), ((( PRIM:CompSeq G1) . n) `2 );

      coherence by Th31;

    end

    theorem :: GLIB_004:33

    

     Th33: for G be _finite real-weighted WGraph, n be Nat holds ((( PRIM:CompSeq G) . n) `1 ) c= (G .reachableFrom the Element of ( the_Vertices_of G))

    proof

      let G be _finite real-weighted WGraph;

      set src = the Element of ( the_Vertices_of G);

      defpred P[ Nat] means ((( PRIM:CompSeq G) . $1) `1 ) c= (G .reachableFrom the Element of ( the_Vertices_of G));

      set G0 = (( PRIM:CompSeq G) . 0 );

      G0 = ( PRIM:Init G) by Def17;

      then

       A1: (G0 `1 ) = {src};

       A2:

      now

        let n be Nat;

        assume

         A3: P[n];

        set Gn = (( PRIM:CompSeq G) . n), Gn1 = (( PRIM:CompSeq G) . (n + 1));

        set Next = ( PRIM:NextBestEdges Gn), e = the Element of Next;

        set sc = (( the_Source_of G) . e), tar = (( the_Target_of G) . e);

        

         A4: Gn1 = ( PRIM:Step Gn) by Def17;

        now

          per cases ;

            suppose Next = {} ;

            hence P[(n + 1)] by A3, A4, Def15;

          end;

            suppose

             A5: Next <> {} & sc in (Gn `1 );

            then Gn1 = [((Gn `1 ) \/ {tar}), ((Gn `2 ) \/ {e})] by A4, Def15;

            then

             A6: (Gn1 `1 ) = ((Gn `1 ) \/ {tar});

            

             A7: e in Next by A5;

            now

              let v be object;

              assume

               A8: v in (Gn1 `1 );

              now

                per cases by A6, A8, XBOOLE_0:def 3;

                  suppose v in (Gn `1 );

                  hence v in (G .reachableFrom src) by A3;

                end;

                  suppose v in {tar};

                  then v = tar by TARSKI:def 1;

                  then e Joins (sc,v,G) by A7;

                  hence v in (G .reachableFrom src) by A3, A5, GLIB_002: 10;

                end;

              end;

              hence v in (G .reachableFrom src);

            end;

            hence P[(n + 1)] by TARSKI:def 3;

          end;

            suppose

             A9: Next <> {} & not sc in (Gn `1 );

            then Gn1 = [((Gn `1 ) \/ {sc}), ((Gn `2 ) \/ {e})] by A4, Def15;

            then

             A10: (Gn1 `1 ) = ((Gn `1 ) \/ {sc});

            

             A11: e SJoins ((Gn `1 ),(( the_Vertices_of G) \ (Gn `1 )),G) by A9, Def13;

            then

             A12: e in ( the_Edges_of G);

            

             A13: tar in (Gn `1 ) by A9, A11;

            now

              let v be object;

              assume

               A14: v in (Gn1 `1 );

              now

                per cases by A10, A14, XBOOLE_0:def 3;

                  suppose v in (Gn `1 );

                  hence v in (G .reachableFrom src) by A3;

                end;

                  suppose v in {sc};

                  then v = sc by TARSKI:def 1;

                  then e Joins (tar,v,G) by A12;

                  hence v in (G .reachableFrom src) by A3, A13, GLIB_002: 10;

                end;

              end;

              hence v in (G .reachableFrom src);

            end;

            hence P[(n + 1)] by TARSKI:def 3;

          end;

        end;

        hence P[(n + 1)];

      end;

      src in (G .reachableFrom src) by GLIB_002: 9;

      then

       A15: P[ 0 ] by A1, ZFMISC_1: 31;

      for n be Nat holds P[n] from NAT_1:sch 2( A15, A2);

      hence thesis;

    end;

    theorem :: GLIB_004:34

    

     Th34: for G be _finite real-weighted WGraph, i,j be Nat st i <= j holds ((( PRIM:CompSeq G) . i) `1 ) c= ((( PRIM:CompSeq G) . j) `1 ) & ((( PRIM:CompSeq G) . i) `2 ) c= ((( PRIM:CompSeq G) . j) `2 )

    proof

      let G be _finite real-weighted WGraph, i,j be Nat;

      set PCS = ( PRIM:CompSeq G);

      set vPCS = ((PCS . i) `1 ), ePCS = ((PCS . i) `2 );

      defpred P[ Nat] means vPCS c= ((PCS . (i + $1)) `1 ) & ePCS c= ((PCS . (i + $1)) `2 );

      assume i <= j;

      then

       A1: ex x be Nat st j = (i + x) by NAT_1: 10;

      now

        let k be Nat;

        (PCS . ((i + k) + 1)) = ( PRIM:Step (PCS . (i + k))) by Def17;

        then

         A2: ((PCS . (i + k)) `1 ) c= ((PCS . ((i + k) + 1)) `1 ) & ((PCS . (i + k)) `2 ) c= ((PCS . ((i + k) + 1)) `2 ) by Th29;

        assume vPCS c= ((PCS . (i + k)) `1 ) & ePCS c= ((PCS . (i + k)) `2 );

        hence vPCS c= ((PCS . (i + (k + 1))) `1 ) & ePCS c= ((PCS . (i + (k + 1))) `2 ) by A2;

      end;

      then

       A3: for k be Nat st P[k] holds P[(k + 1)];

      

       A4: P[ 0 ];

      for k be Nat holds P[k] from NAT_1:sch 2( A4, A3);

      hence thesis by A1;

    end;

    theorem :: GLIB_004:35

    

     Th35: for G be _finite real-weighted WGraph, n be Nat holds ( PRIM:NextBestEdges (( PRIM:CompSeq G) . n)) = {} iff ((( PRIM:CompSeq G) . n) `1 ) = (G .reachableFrom the Element of ( the_Vertices_of G))

    proof

      let G be _finite real-weighted WGraph, n be Nat;

      set src = the Element of ( the_Vertices_of G);

      set PCS = ( PRIM:CompSeq G), RFS = (G .reachableFrom src);

      set Gn = (PCS . n);

      set EG = ( the_Edges_of G);

      set Next = ( PRIM:NextBestEdges Gn);

      set GnV = (Gn `1 ), GnVg = (( the_Vertices_of G) \ GnV);

      set e = the Element of Next;

      hereby

        assume

         A1: Next = {} ;

        now

          defpred P1[ set] means $1 SJoins (GnV,GnVg,G);

          assume

           A2: GnV <> RFS;

          consider BE1 be Subset of EG such that

           A3: for x be set holds x in BE1 iff x in EG & P1[x] from SUBSET_1:sch 1;

          GnV c= RFS by Th33;

          then

           A4: GnV c< RFS by A2, XBOOLE_0:def 8;

          now

            src in {src} by TARSKI:def 1;

            then src in (( PRIM:Init G) `1 );

            then

             A5: src in ((PCS . 0 ) `1 ) by Def17;

            assume

             A6: BE1 = {} ;

            consider v be object such that

             A7: v in RFS and

             A8: not v in (Gn `1 ) by A4, XBOOLE_0: 6;

            reconsider v as Vertex of G by A7;

            consider W be Walk of G such that

             A9: W is_Walk_from (src,v) by A7, GLIB_002:def 5;

            defpred P2[ Nat] means $1 is odd & $1 <= ( len W) & not (W . $1) in GnV;

            (W . ( len W)) = (W .last() ) by GLIB_001:def 7

            .= v by A9, GLIB_001:def 23;

            then

             A10: ex k be Nat st P2[k] by A8;

            consider k be Nat such that

             A11: P2[k] & for m be Nat st P2[m] holds k <= m from NAT_1:sch 5( A10);

            

             A12: ((PCS . 0 ) `1 ) c= (Gn `1 ) by Th34;

            now

              per cases ;

                suppose k = 1;

                

                then (W . k) = (W .first() ) by GLIB_001:def 6

                .= src by A9, GLIB_001:def 23;

                hence contradiction by A5, A12, A11;

              end;

                suppose

                 A13: k <> 1;

                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: e Joins ((W . k2a),(W . (k2a + 2)),G) by GLIB_001:def 3;

                then

                 A16: e in EG;

                k2a < (k - 0 ) by XREAL_1: 15;

                then

                 A17: (W . k2a) in GnV by A11, A14;

                (W . k) in ( the_Vertices_of G) by A15, GLIB_000: 13;

                then (W . k) in GnVg by A11, XBOOLE_0:def 5;

                then P1[e] by A17, A15, GLIB_000: 17;

                hence contradiction by A3, A6, A16;

              end;

            end;

            hence contradiction;

          end;

          then

          reconsider BE1 as non empty finite set;

          deffunc F( Element of BE1) = (( the_Weight_of G) . $1);

          consider e1 be Element of BE1 such that

           A18: for e2 be Element of BE1 holds F(e1) <= F(e2) from PRE_CIRC:sch 5;

           A19:

          now

            let e2 be set;

            assume

             A20: e2 SJoins (GnV,GnVg,G);

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

          end;

          e1 SJoins (GnV,GnVg,G) by A3;

          hence contradiction by A1, A19, Def13;

        end;

        hence GnV = RFS;

      end;

      assume

       A21: GnV = RFS;

      now

        assume Next <> {} ;

        then

         A22: e SJoins (GnV,GnVg,G) by Def13;

        then

         A23: e in EG;

        now

          per cases by A22;

            suppose

             A24: (( the_Source_of G) . e) in GnV & (( the_Target_of G) . e) in GnVg;

            

             A25: e Joins ((( the_Source_of G) . e),(( the_Target_of G) . e),G) by A23;

             not (( the_Target_of G) . e) in GnV by A24, XBOOLE_0:def 5;

            hence contradiction by A21, A24, A25, GLIB_002: 10;

          end;

            suppose

             A26: (( the_Source_of G) . e) in GnVg & (( the_Target_of G) . e) in GnV;

            

             A27: e Joins ((( the_Target_of G) . e),(( the_Source_of G) . e),G) by A23;

             not (( the_Source_of G) . e) in GnV by A26, XBOOLE_0:def 5;

            hence contradiction by A21, A26, A27, GLIB_002: 10;

          end;

        end;

        hence contradiction;

      end;

      hence thesis;

    end;

    theorem :: GLIB_004:36

    

     Th36: for G be _finite real-weighted WGraph, n be Nat holds ( card ((( PRIM:CompSeq G) . n) `1 )) = ( min ((n + 1),( card (G .reachableFrom the Element of ( the_Vertices_of G)))))

    proof

      let G be _finite real-weighted WGraph;

      set CS = ( PRIM:CompSeq G), src = the Element of ( the_Vertices_of G);

      defpred P[ Nat] means ( card ((( PRIM:CompSeq G) . $1) `1 )) = ( min (($1 + 1),( card (G .reachableFrom src))));

      set G0 = (CS . 0 );

      src in (G .reachableFrom src) by GLIB_002: 9;

      then {src} c= (G .reachableFrom src) by ZFMISC_1: 31;

      then ( card {src}) <= ( card (G .reachableFrom src)) by NAT_1: 43;

      then

       A1: ( 0 + 1) <= ( card (G .reachableFrom src)) by CARD_1: 30;

       A2:

      now

        let n be Nat;

        assume

         A3: P[n];

        set Gn = (( PRIM:CompSeq G) . n), Gn1 = (( PRIM:CompSeq G) . (n + 1));

        set e = the Element of ( PRIM:NextBestEdges Gn);

        

         A4: Gn1 = ( PRIM:Step Gn) by Def17;

        now

          per cases ;

            suppose

             A5: ( PRIM:NextBestEdges Gn) = {} ;

            then

             A6: ( card (Gn `1 )) = ( card (G .reachableFrom src)) by Th35;

            then ( card (G .reachableFrom src)) <= (n + 1) by A3, XXREAL_0:def 9;

            then

             A7: ( card (G .reachableFrom src)) <= ((n + 1) + 1) by NAT_1: 12;

            ( card (Gn1 `1 )) = ( min ((n + 1),( card (G .reachableFrom src)))) by A3, A4, A5, Def15;

            hence P[(n + 1)] by A3, A6, A7, XXREAL_0:def 9;

          end;

            suppose

             A8: ( PRIM:NextBestEdges Gn) <> {} ;

            

             A9: (Gn `1 ) c= (G .reachableFrom src) by Th33;

            

             A10: (Gn `1 ) <> (G .reachableFrom src) by A8, Th35;

             A11:

            now

              assume

               A12: ( card (Gn `1 )) = ( card (G .reachableFrom src));

              (Gn `1 ) c< (G .reachableFrom src) by A10, A9, XBOOLE_0:def 8;

              hence contradiction by A12, CARD_2: 48;

            end;

            then

             A13: ( card (Gn `1 )) = (n + 1) by A3, XXREAL_0: 15;

            consider v be Vertex of G such that

             A14: not v in (Gn `1 ) and

             A15: Gn1 = [((Gn `1 ) \/ {v}), ((Gn `2 ) \/ {e})] by A4, A8, Th28;

            

             A16: ( card (Gn1 `1 )) = ( card ((Gn `1 ) \/ {v})) by A15

            .= (( card (Gn `1 )) + 1) by A14, CARD_2: 41;

            ( card (Gn `1 )) <= ( card (G .reachableFrom src)) by Th33, NAT_1: 43;

            then (n + 1) < ( card (G .reachableFrom src)) by A11, A13, XXREAL_0: 1;

            then ((n + 1) + 1) <= ( card (G .reachableFrom src)) by NAT_1: 13;

            hence P[(n + 1)] by A16, A13, XXREAL_0:def 9;

          end;

        end;

        hence P[(n + 1)];

      end;

      G0 = ( PRIM:Init G) by Def17;

      then {src} = (G0 `1 );

      then ( card (G0 `1 )) = 1 by CARD_1: 30;

      then

       A17: P[ 0 ] by A1, XXREAL_0:def 9;

      for n be Nat holds P[n] from NAT_1:sch 2( A17, A2);

      hence thesis;

    end;

    theorem :: GLIB_004:37

    

     Th37: for G be _finite real-weighted WGraph holds ( PRIM:CompSeq G) is halting & ((( PRIM:CompSeq G) .Lifespan() ) + 1) = ( card (G .reachableFrom the Element of ( the_Vertices_of G)))

    proof

      let G be _finite real-weighted WGraph;

      set PCS = ( PRIM:CompSeq G);

      set src = the Element of ( the_Vertices_of G), RFS = (G .reachableFrom src);

      consider n be Nat such that

       A1: (n + 1) = ( card RFS) by NAT_1: 6;

      reconsider n as Element of NAT by ORDINAL1:def 12;

      set Gn = (PCS . n), Gn1 = (PCS . (n + 1));

      

       A2: ( card RFS) <= (( card RFS) + 1) by NAT_1: 11;

      

       A3: ( card (Gn1 `1 )) = ( min ((( card RFS) + 1),( card RFS))) by A1, Th36

      .= ( card RFS) by A2, XXREAL_0:def 9;

      set e = the Element of ( PRIM:NextBestEdges Gn);

      

       A4: ( card (Gn `1 )) = ( min (( card RFS),( card RFS))) by A1, Th36

      .= ( card RFS);

      

       A5: Gn1 = ( PRIM:Step Gn) by Def17;

      then

       A6: (Gn `1 ) c= (Gn1 `1 ) by Th29;

       A7:

      now

        assume (Gn `1 ) <> (Gn1 `1 );

        then (Gn `1 ) c< (Gn1 `1 ) by A6, XBOOLE_0:def 8;

        hence contradiction by A4, A3, CARD_2: 48;

      end;

      now

        assume ( PRIM:NextBestEdges Gn) <> {} ;

        then

        consider v be Vertex of G such that

         A8: not v in (Gn `1 ) and

         A9: Gn1 = [((Gn `1 ) \/ {v}), ((Gn `2 ) \/ {e})] by A5, Th28;

        

         A10: v in {v} by TARSKI:def 1;

        (Gn1 `1 ) = ((Gn `1 ) \/ {v}) by A9;

        hence contradiction by A7, A8, A10, XBOOLE_0:def 3;

      end;

      then

       A11: Gn1 = Gn by A5, Def15;

      hence

       A12: PCS is halting;

      now

        let m be Nat;

        set Gm = (PCS . m);

        assume

         A13: (PCS . m) = (PCS . (m + 1));

        now

          assume m < n;

          then

           A14: (m + 1) <= n by NAT_1: 13;

          (n + 0 ) < ( card RFS) by A1, XREAL_1: 8;

          then

           A15: (m + 1) < ( card RFS) by A14, XXREAL_0: 2;

          then

           A16: ((m + 1) + 1) <= ( card RFS) by NAT_1: 13;

          

           A17: ( card (Gm `1 )) = ( min ((m + 1),( card RFS))) by Th36

          .= (m + 1) by A15, XXREAL_0:def 9;

          ( card (Gm `1 )) = ( min (((m + 1) + 1),( card RFS))) by A13, Th36

          .= ((m + 1) + 1) by A16, XXREAL_0:def 9;

          hence contradiction by A17;

        end;

        hence n <= m;

      end;

      hence thesis by A1, A11, A12, GLIB_000:def 56;

    end;

    theorem :: GLIB_004:38

    

     Th38: for G1 be _finite real-weighted WGraph, n be Nat, G2 be inducedSubgraph of G1, ((( PRIM:CompSeq G1) . n) `1 ), ((( PRIM:CompSeq G1) . n) `2 ) holds G2 is Tree-like

    proof

      let G1 be _finite real-weighted WGraph;

      set PCS = ( PRIM:CompSeq G1);

      defpred P[ Nat] means for G2 be inducedSubgraph of G1, ((PCS . $1) `1 ), ((PCS . $1) `2 ) holds G2 is Tree-like;

      set G0 = (PCS . 0 ), src = the Element of ( the_Vertices_of G1);

      now

        let n be Nat;

        set Gn = (PCS . n), Gn1 = (PCS . (n + 1));

        set Next = ( PRIM:NextBestEdges Gn), e = the Element of Next;

        set G3 = the inducedSubgraph of G1, (Gn `1 ), (Gn `2 );

        

         A1: Gn1 = ( PRIM:Step Gn) by Def17;

        

         A2: (Gn `2 ) c= (G1 .edgesBetween (Gn `1 )) by Th30;

        (Gn `1 ) is non empty Subset of ( the_Vertices_of G1) by Th30;

        then

         A3: ( the_Vertices_of G3) = (Gn `1 ) & ( the_Edges_of G3) = (Gn `2 ) by A2, GLIB_000:def 37;

        assume

         A4: P[n];

        then

         A5: G3 is Tree-like;

        now

          

           A6: (G3 .order() ) = ((G3 .size() ) + 1) by A5, GLIB_002: 46;

          let G2 be inducedSubgraph of G1, (Gn1 `1 ), (Gn1 `2 );

          

           A7: (Gn1 `2 ) c= (G1 .edgesBetween (Gn1 `1 )) by Th30;

          (Gn1 `1 ) is non empty Subset of ( the_Vertices_of G1) by Th30;

          then

           A8: ( the_Vertices_of G2) = (Gn1 `1 ) by A7, GLIB_000:def 37;

          now

            per cases ;

              suppose Next = {} ;

              then Gn = Gn1 by A1, Def15;

              hence G2 is Tree-like by A4;

            end;

              suppose

               A9: Next <> {} ;

              set GnV = (Gn `1 ), GnVg = (( the_Vertices_of G1) \ GnV);

              

               A10: e SJoins (GnV,GnVg,G1) by A9, Def13;

               A11:

              now

                assume

                 A12: e in (Gn `2 );

                then (( the_Target_of G1) . e) in GnV by A2, GLIB_000: 31;

                then

                 A13: not (( the_Target_of G1) . e) in GnVg by XBOOLE_0:def 5;

                (( the_Source_of G1) . e) in GnV by A2, A12, GLIB_000: 31;

                then not (( the_Source_of G1) . e) in GnVg by XBOOLE_0:def 5;

                hence contradiction by A10, A13;

              end;

              consider v be Vertex of G1 such that

               A14: not v in (Gn `1 ) and

               A15: Gn1 = [((Gn `1 ) \/ {v}), ((Gn `2 ) \/ {e})] by A1, A9, Th28;

              

               A16: ( card (Gn1 `1 )) = ( card ((Gn `1 ) \/ {v})) by A15

              .= (( card (Gn `1 )) + 1) by A14, CARD_2: 41;

              ( card (Gn1 `2 )) = ( card ((Gn `2 ) \/ {e})) by A15

              .= (( card (Gn `2 )) + 1) by A11, CARD_2: 41;

              then (G2 .order() ) = ((G2 .size() ) + 1) by A3, A7, A8, A6, A16, GLIB_000:def 37;

              hence G2 is Tree-like by GLIB_002: 47;

            end;

          end;

          hence G2 is Tree-like;

        end;

        hence P[(n + 1)];

      end;

      then

       A17: for n be Nat st P[n] holds P[(n + 1)];

      G0 = ( PRIM:Init G1) by Def17;

      then (G0 `1 ) = {src} & (G0 `2 ) = {} ;

      then

       A18: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A18, A17);

      hence thesis;

    end;

    theorem :: GLIB_004:39

    

     Th39: for G be _finite connected real-weighted WGraph holds (( PRIM:MST G) `1 ) = ( the_Vertices_of G)

    proof

      let G be _finite connected real-weighted WGraph;

      set M = ( PRIM:MST G), PCS = ( PRIM:CompSeq G), V = (M `1 );

      set src = the Element of ( the_Vertices_of G), RFS = (G .reachableFrom src);

      ((PCS .Lifespan() ) + 1) = ( card RFS) by Th37;

      then

       A1: ( card V) = ( min (( card RFS),( card RFS))) by Th36;

      

       A2: V c= RFS by Th33;

      now

        assume V <> RFS;

        then V c< RFS by A2, XBOOLE_0:def 8;

        hence contradiction by A1, CARD_2: 48;

      end;

      hence thesis by GLIB_002: 16;

    end;

    registration

      let G be _finite connected real-weighted WGraph;

      cluster spanning Tree-like for WSubgraph of G;

      existence

      proof

        set PCS = ( PRIM:CompSeq G), n = (PCS .Lifespan() );

        set IT = the inducedWSubgraph of G, ((PCS . n) `1 ), ((PCS . n) `2 );

        take IT;

        ( PRIM:MST G) = (PCS . n);

        then

         A1: ((PCS . n) `1 ) = ( the_Vertices_of G) by Th39;

        thus IT is spanning by A1;

        thus thesis by Th38;

      end;

    end

    definition

      let G1 be _finite connected real-weighted WGraph, G2 be spanning Tree-like WSubgraph of G1;

      :: GLIB_004:def19

      attr G2 is min-cost means

      : Def19: for G3 be spanning Tree-like WSubgraph of G1 holds (G2 .cost() ) <= (G3 .cost() );

    end

    registration

      let G1 be _finite connected real-weighted WGraph;

      cluster min-cost for spanning Tree-like WSubgraph of G1;

      existence

      proof

        set GT = the spanning Tree-like WSubgraph of G1;

        set G3 = (GT | WGraphSelectors );

        

         A1: G3 == GT by Lm4;

        ( the_Weight_of G3) = ( the_Weight_of GT) by Lm4;

        then

        reconsider G3 as WSubgraph of G1 by A1, GLIB_003: 8;

        ( the_Vertices_of G3) = ( the_Vertices_of GT) by A1

        .= ( the_Vertices_of G1) by GLIB_000:def 33;

        then

        reconsider G3 as spanning Tree-like WSubgraph of G1 by A1, GLIB_000:def 33, GLIB_002: 48;

        set X = { G2 where G2 be Element of (G1 .allWSubgraphs() ) : G2 is spanning Tree-like WSubgraph of G1 };

        now

          let x be object;

          assume x in X;

          then ex G2 be Element of (G1 .allWSubgraphs() ) st x = G2 & G2 is spanning Tree-like WSubgraph of G1;

          hence x in (G1 .allWSubgraphs() );

        end;

        then

        reconsider X as finite Subset of (G1 .allWSubgraphs() ) by TARSKI:def 3;

        deffunc F( _finite real-weighted WGraph) = ($1 .cost() );

        ( dom G3) = WGraphSelectors by Lm5;

        then G3 in (G1 .allWSubgraphs() ) by Def5;

        then G3 in X;

        then

        reconsider X as finite non empty Subset of (G1 .allWSubgraphs() );

        consider x be Element of X such that

         A2: for y be Element of X holds F(x) <= F(y) from PRE_CIRC:sch 5;

        x in X;

        then ex G2 be Element of (G1 .allWSubgraphs() ) st x = G2 & G2 is spanning Tree-like WSubgraph of G1;

        then

        reconsider x as spanning Tree-like WSubgraph of G1;

        take x;

        now

          let GT be spanning Tree-like WSubgraph of G1;

          set G3 = (GT | WGraphSelectors );

          

           A3: G3 == GT by Lm4;

          

           A4: ( the_Weight_of G3) = ( the_Weight_of GT) by Lm4;

          then

          reconsider G3 as WSubgraph of G1 by A3, GLIB_003: 8;

          ( the_Vertices_of G3) = ( the_Vertices_of GT) by A3

          .= ( the_Vertices_of G1) by GLIB_000:def 33;

          then

          reconsider G3 as spanning Tree-like WSubgraph of G1 by A3, GLIB_000:def 33, GLIB_002: 48;

          ( dom G3) = WGraphSelectors by Lm5;

          then G3 in (G1 .allWSubgraphs() ) by Def5;

          then G3 in X;

          then (x .cost() ) <= (G3 .cost() ) by A2;

          hence (x .cost() ) <= (GT .cost() ) by A3, A4;

        end;

        hence thesis;

      end;

    end

    definition

      let G be _finite connected real-weighted WGraph;

      mode minimumSpanningTree of G is min-cost spanning Tree-like WSubgraph of G;

    end

    begin

    theorem :: GLIB_004:40

    for G1,G2 be _finite connected real-weighted WGraph, G3 be WSubgraph of G1 st G3 is minimumSpanningTree of G1 & G1 == G2 & ( the_Weight_of G1) = ( the_Weight_of G2) holds G3 is minimumSpanningTree of G2

    proof

      let G1,G2 be _finite connected real-weighted WGraph, G3 be WSubgraph of G1;

      assume that

       A1: G3 is minimumSpanningTree of G1 and

       A2: G1 == G2 and

       A3: ( the_Weight_of G1) = ( the_Weight_of G2);

      set G39 = G3;

      reconsider G39 as Tree-like WSubgraph of G2 by A1, A2, A3, GLIB_003: 10;

      ( the_Vertices_of G3) = ( the_Vertices_of G1) by A1, GLIB_000:def 33

      .= ( the_Vertices_of G2) by A2;

      then

      reconsider G39 as spanning Tree-like WSubgraph of G2 by GLIB_000:def 33;

      now

        let G be spanning Tree-like WSubgraph of G2;

        reconsider G9 = G as Tree-like WSubgraph of G1 by A2, A3, GLIB_003: 10;

        ( the_Vertices_of G) = ( the_Vertices_of G2) by GLIB_000:def 33

        .= ( the_Vertices_of G1) by A2;

        then G9 is spanning;

        hence (G3 .cost() ) <= (G .cost() ) by A1, Def19;

      end;

      then G39 is min-cost;

      hence thesis;

    end;

    theorem :: GLIB_004:41

    

     Th41: for G be _finite connected real-weighted WGraph, G1 be minimumSpanningTree of G, G2 be WGraph st G1 == G2 & ( the_Weight_of G1) = ( the_Weight_of G2) holds G2 is minimumSpanningTree of G

    proof

      let G be _finite connected real-weighted WGraph, G1 be minimumSpanningTree of G, G2 be WGraph;

      assume that

       A1: G1 == G2 and

       A2: ( the_Weight_of G1) = ( the_Weight_of G2);

      reconsider G29 = G2 as WSubgraph of G by A1, A2, GLIB_003: 8;

      ( the_Vertices_of G2) = ( the_Vertices_of G1) by A1

      .= ( the_Vertices_of G) by GLIB_000:def 33;

      then

      reconsider G29 as spanning Tree-like WSubgraph of G by A1, GLIB_000:def 33, GLIB_002: 48;

      now

        let G3 be spanning Tree-like WSubgraph of G;

        (G1 .cost() ) <= (G3 .cost() ) by Def19;

        hence (G29 .cost() ) <= (G3 .cost() ) by A1, A2;

      end;

      hence thesis by Def19;

    end;

    theorem :: GLIB_004:42

    

     Th42: for G be _finite connected real-weighted WGraph, n be Nat holds ((( PRIM:CompSeq G) . n) `2 ) c= (( PRIM:MST G) `2 )

    proof

      let G be _finite connected real-weighted WGraph, n be Nat;

      set PCS = ( PRIM:CompSeq G);

      defpred P[ Nat] means (PCS . ((PCS .Lifespan() ) + $1)) = ( PRIM:MST G);

       A1:

      now

        set off = (PCS .Lifespan() );

        let n be Nat;

        set Gn = (PCS . (off + n)), Gn1 = (PCS . ((off + n) + 1));

        set Next = ( PRIM:NextBestEdges Gn), e = the Element of Next;

        

         A2: Gn1 = ( PRIM:Step Gn) by Def17;

        assume

         A3: P[n];

        then

         A4: (Gn `1 ) = ( the_Vertices_of G) by Th39;

        now

          assume Next <> {} ;

          then ex v be Vertex of G st ( not v in (Gn `1 )) & Gn1 = [((Gn `1 ) \/ {v}), ((Gn `2 ) \/ {e})] by A2, Th28;

          hence contradiction by A4;

        end;

        hence P[(n + 1)] by A3, A2, Def15;

      end;

      

       A5: P[ 0 ];

      

       A6: for n be Nat holds P[n] from NAT_1:sch 2( A5, A1);

      now

        per cases ;

          suppose n <= (PCS .Lifespan() );

          hence thesis by Th34;

        end;

          suppose (PCS .Lifespan() ) < n;

          then ex k be Nat st n = ((PCS .Lifespan() ) + k) by NAT_1: 10;

          hence thesis by A6;

        end;

      end;

      hence thesis;

    end;

    ::$Notion-Name

    theorem :: GLIB_004:43

    for G1 be _finite connected real-weighted WGraph, G2 be inducedWSubgraph of G1, (( PRIM:MST G1) `1 ), (( PRIM:MST G1) `2 ) holds G2 is minimumSpanningTree of G1

    proof

      let G1 be _finite connected real-weighted WGraph;

      set PMST = ( PRIM:MST G1);

      let G2 be inducedWSubgraph of G1, (PMST `1 ), (PMST `2 );

      reconsider G29 = G2 as Tree-like _Graph by Th38;

      set VG1 = ( the_Vertices_of G1), EG1 = ( the_Edges_of G1);

      set WG1 = ( the_Weight_of G1);

      set PCS = ( PRIM:CompSeq G1);

      

       A1: (PMST `1 ) = VG1 by Th39;

      (PMST `2 ) c= EG1;

      then

       A2: (PMST `2 ) c= (G1 .edgesBetween (PMST `1 )) by A1, GLIB_000: 34;

      

       A3: ( the_Vertices_of G2) = VG1 by A1, A2, GLIB_000:def 37;

      

       A4: ( the_Edges_of G2) = (PMST `2 ) by A1, A2, GLIB_000:def 37;

      

       A5: G2 is Tree-like by Th38;

      now

        set X = { x where x be Element of (G1 .allWSubgraphs() ) : x is minimumSpanningTree of G1 };

        now

          let x be object;

          assume x in X;

          then ex G2 be Element of (G1 .allWSubgraphs() ) st x = G2 & G2 is minimumSpanningTree of G1;

          hence x in (G1 .allWSubgraphs() );

        end;

        then

        reconsider X as finite Subset of (G1 .allWSubgraphs() ) by TARSKI:def 3;

        defpred Z[ _finite _Graph, Nat] means not ((PCS . ($2 + 1)) `2 ) c= ( the_Edges_of $1) & for n be Nat st n <= $2 holds ((PCS . n) `2 ) c= ( the_Edges_of $1);

        defpred P[ _finite _Graph, _finite _Graph] means ( card (( the_Edges_of $1) /\ ( the_Edges_of G2))) > ( card (( the_Edges_of $2) /\ ( the_Edges_of G2))) or (( card (( the_Edges_of $1) /\ ( the_Edges_of G2))) = ( card (( the_Edges_of $2) /\ ( the_Edges_of G2))) & for k1,k2 be Nat st Z[$1, k1] & Z[$2, k2] holds k1 >= k2);

        

         A6: (G1 .edgesBetween VG1) = EG1 by GLIB_000: 34;

        now

          set M = the minimumSpanningTree of G1;

          set M9 = (M | WGraphSelectors );

          M9 == M & ( the_Weight_of M9) = ( the_Weight_of M) by Lm4;

          then

          reconsider M9 as minimumSpanningTree of G1 by Th41;

          ( dom M9) = WGraphSelectors by Lm5;

          then M9 in (G1 .allWSubgraphs() ) by Def5;

          then M9 in X;

          hence X <> {} ;

        end;

        then

        reconsider X as non empty finite Subset of (G1 .allWSubgraphs() );

        assume

         A7: not G2 is minimumSpanningTree of G1;

         A8:

        now

          let G be Element of X;

          G in X;

          then ex G9 be Element of (G1 .allWSubgraphs() ) st G = G9 & G9 is minimumSpanningTree of G1;

          then

          reconsider G9 = G as minimumSpanningTree of G1;

          defpred P4[ Nat] means not ((PCS . $1) `2 ) c= ( the_Edges_of G9);

          

           A9: ( the_Vertices_of G2) = ( the_Vertices_of G9) by A3, GLIB_000:def 33;

           A10:

          now

            assume

             A11: ( the_Edges_of G2) = ( the_Edges_of G9);

            ( the_Weight_of G2) = (WG1 | ( the_Edges_of G2)) by GLIB_003:def 10

            .= ( the_Weight_of G9) by A11, GLIB_003:def 10;

            hence contradiction by A7, A9, A11, Th41, GLIB_000: 86;

          end;

          now

            assume ( the_Edges_of G2) c= ( the_Edges_of G9);

            then ( the_Edges_of G2) c< ( the_Edges_of G9) by A10, XBOOLE_0:def 8;

            then ((G2 .size() ) + 1) < ((G9 .size() ) + 1) by CARD_2: 48, XREAL_1: 8;

            then

             A12: (G2 .order() ) < ((G9 .size() ) + 1) by A5, GLIB_002: 46;

            (G2 .order() ) = (G9 .order() ) by A3, GLIB_000:def 33;

            hence contradiction by A12, GLIB_002: 46;

          end;

          then

           A13: ex n be Nat st P4[n] by A4;

          consider k3 be Nat such that

           A14: P4[k3] & for n be Nat st P4[n] holds k3 <= n from NAT_1:sch 5( A13);

          now

            assume k3 = 0 ;

            then not (( PRIM:Init G1) `2 ) c= ( the_Edges_of G9) by A14, Def17;

            hence contradiction;

          end;

          then

          consider k2 be Nat such that

           A16: (k2 + 1) = k3 by NAT_1: 6;

          ((k2 + 1) - 1) < (k3 - 0 ) by A16, XREAL_1: 15;

          then

           A17: ((PCS . k2) `2 ) c= ( the_Edges_of G9) by A14;

          now

            let n be Nat;

            assume n <= k2;

            then ((PCS . n) `2 ) c= ((PCS . k2) `2 ) by Th34;

            hence ((PCS . n) `2 ) c= ( the_Edges_of G9) by A17;

          end;

          hence ex k1 be Nat st Z[G, k1] by A14, A16;

        end;

        now

          let x,y,z be Element of X;

          assume that

           A18: P[x, y] and

           A19: P[y, z];

          y in X;

          then

          consider y9 be WSubgraph of G1 such that

           A20: y9 = y and ( dom y9) = WGraphSelectors by Def5;

          set CY = ( card (( the_Edges_of y9) /\ ( the_Edges_of G2)));

          x in X;

          then

          consider x9 be WSubgraph of G1 such that

           A21: x9 = x and ( dom x9) = WGraphSelectors by Def5;

          z in X;

          then

          consider z9 be WSubgraph of G1 such that

           A22: z9 = z and ( dom z9) = WGraphSelectors by Def5;

          set CZ = ( card (( the_Edges_of z9) /\ ( the_Edges_of G2)));

          set CX = ( card (( the_Edges_of x9) /\ ( the_Edges_of G2)));

          now

            per cases by A18, A21, A20;

              suppose

               A23: CX > CY;

              now

                per cases by A19, A20, A22;

                  suppose CY > CZ;

                  hence P[x, z] by A21, A22, A23, XXREAL_0: 2;

                end;

                  suppose CY = CZ & for ky,kz be Nat st Z[y9, ky] & Z[z9, kz] holds ky >= kz;

                  hence P[x, z] by A21, A22, A23;

                end;

              end;

              hence P[x, z];

            end;

              suppose

               A24: CX = CY & for kx,ky be Nat st Z[x9, kx] & Z[y9, ky] holds kx >= ky;

              now

                per cases by A19, A20, A22;

                  suppose CY > CZ;

                  hence P[x, z] by A21, A22, A24;

                end;

                  suppose

                   A25: CY = CZ & for ky,kz be Nat st Z[y9, ky] & Z[z9, kz] holds ky >= kz;

                  consider zy be Nat such that

                   A26: Z[y, zy] by A8;

                  now

                    let kx,kz be Nat;

                    assume Z[x9, kx] & Z[z9, kz];

                    then kx >= zy & zy >= kz by A20, A24, A25, A26;

                    hence kx >= kz by XXREAL_0: 2;

                  end;

                  hence P[x, z] by A21, A22, A24, A25;

                end;

              end;

              hence P[x, z];

            end;

          end;

          hence P[x, z];

        end;

        then

         A27: for x,y,z be Element of X st P[x, y] & P[y, z] holds P[x, z];

         A28:

        now

          let G be Element of X, k1,k2 be Nat;

          assume

           A29: Z[G, k1] & Z[G, k2];

          then (k2 + 1) > k1;

          then

           A30: k2 >= k1 by NAT_1: 13;

          (k1 + 1) > k2 by A29;

          then k1 >= k2 by NAT_1: 13;

          hence k1 = k2 by A30, XXREAL_0: 1;

        end;

        now

          let x,y be Element of X;

          x in X;

          then

          consider x9 be WSubgraph of G1 such that

           A31: x9 = x and ( dom x9) = WGraphSelectors by Def5;

          set CX = ( card (( the_Edges_of x9) /\ ( the_Edges_of G2)));

          y in X;

          then

          consider y9 be WSubgraph of G1 such that

           A32: y9 = y and ( dom y9) = WGraphSelectors by Def5;

          set CY = ( card (( the_Edges_of y9) /\ ( the_Edges_of G2)));

          now

            per cases by XXREAL_0: 1;

              suppose CX < CY;

              hence P[x, y] or P[y, x] by A31, A32;

            end;

              suppose

               A33: CY = CX;

              consider k1 be Nat such that

               A34: Z[x, k1] by A8;

              consider k2 be Nat such that

               A35: Z[y, k2] by A8;

              now

                per cases ;

                  suppose

                   A36: k1 >= k2;

                  now

                    let z1,z2 be Nat;

                    assume that

                     A37: Z[x, z1] and

                     A38: Z[y, z2];

                    z1 = k1 by A28, A34, A37;

                    hence z1 >= z2 by A28, A35, A36, A38;

                  end;

                  hence P[x, y] or P[y, x] by A31, A32, A33;

                end;

                  suppose

                   A39: k1 < k2;

                  now

                    let z1,z2 be Nat;

                    assume that

                     A40: Z[x, z1] and

                     A41: Z[y, z2];

                    z1 = k1 by A28, A34, A40;

                    hence z1 <= z2 by A28, A35, A39, A41;

                  end;

                  hence P[x, y] or P[y, x] by A31, A32, A33;

                end;

              end;

              hence P[x, y] or P[y, x];

            end;

              suppose CX > CY;

              hence P[x, y] or P[y, x] by A31, A32;

            end;

          end;

          hence P[x, y] or P[y, x];

        end;

        then

         A42: for x,y be Element of X holds P[x, y] or P[y, x];

        

         A43: X is finite & X <> {} & X c= X;

        consider M be Element of X such that

         A44: M in X & for y be Element of X st y in X holds P[M, y] from CQC_SIM1:sch 4( A43, A42, A27);

        ex x be Element of (G1 .allWSubgraphs() ) st M = x & x is minimumSpanningTree of G1 by A44;

        then

        reconsider M as minimumSpanningTree of G1;

        defpred P2[ Nat] means not ((PCS . $1) `2 ) c= ( the_Edges_of M);

        

         A45: ( the_Vertices_of G2) = ( the_Vertices_of M) by A3, GLIB_000:def 33;

         A46:

        now

          assume

           A47: ( the_Edges_of G2) = ( the_Edges_of M);

          ( the_Weight_of G2) = (WG1 | ( the_Edges_of G2)) by GLIB_003:def 10

          .= ( the_Weight_of M) by A47, GLIB_003:def 10;

          hence contradiction by A7, A45, A47, Th41, GLIB_000: 86;

        end;

        now

          assume ( the_Edges_of G2) c= ( the_Edges_of M);

          then ( the_Edges_of G2) c< ( the_Edges_of M) by A46, XBOOLE_0:def 8;

          then ((G2 .size() ) + 1) < ((M .size() ) + 1) by CARD_2: 48, XREAL_1: 8;

          then

           A48: (G2 .order() ) < ((M .size() ) + 1) by A5, GLIB_002: 46;

          (G2 .order() ) = (M .order() ) by A3, GLIB_000:def 33;

          hence contradiction by A48, GLIB_002: 46;

        end;

        then

         A49: ex k be Nat st P2[k] by A4;

        consider k be Nat such that

         A50: P2[k] & for n be Nat st P2[n] holds k <= n from NAT_1:sch 5( A49);

        now

          assume k = 0 ;

          then not (( PRIM:Init G1) `2 ) c= ( the_Edges_of M) by A50, Def17;

          hence contradiction;

        end;

        then

        consider k1o be Nat such that

         A52: k = (k1o + 1) by NAT_1: 6;

        set Gk1b = (PCS . k1o), Gk = (PCS . k);

        ((k1o + 1) - 1) < (k - 0 ) by A52, XREAL_1: 15;

        then

         A53: (Gk1b `2 ) c= ( the_Edges_of M) by A50;

        set Next = ( PRIM:NextBestEdges Gk1b), ep = the Element of Next;

        

         A54: Gk = ( PRIM:Step Gk1b) by A52, Def17;

        then

         A55: Next <> {} by A50, A53, Def15;

        then

         A56: ep SJoins ((Gk1b `1 ),(VG1 \ (Gk1b `1 )),G1) by Def13;

        ex v be Vertex of G1 st ( not v in (Gk1b `1 )) & Gk = [((Gk1b `1 ) \/ {v}), ((Gk1b `2 ) \/ {ep})] by A54, A55, Th28;

        then

         A57: (Gk `2 ) = ((Gk1b `2 ) \/ {ep});

        then

         A58: not {ep} c= ( the_Edges_of M) by A50, A53, XBOOLE_1: 8;

        then

         A59: not ep in ( the_Edges_of M) by ZFMISC_1: 31;

        set Mep = the inducedWSubgraph of G1, VG1, (( the_Edges_of M) \/ {ep});

        

         A60: ep in Next by A55;

        then {ep} c= EG1 by ZFMISC_1: 31;

        then (( the_Edges_of M) \/ {ep}) c= EG1 by XBOOLE_1: 8;

        then

         A61: VG1 c= VG1 & (( the_Edges_of M) \/ {ep}) c= (G1 .edgesBetween VG1) by GLIB_000: 34;

        then

         A62: ( the_Vertices_of Mep) = VG1 by GLIB_000:def 37;

        VG1 = ( the_Vertices_of M) by GLIB_000:def 33;

        then VG1 c= VG1 & M is inducedWSubgraph of G1, VG1, ( the_Edges_of M) by A6, GLIB_000:def 37;

        then

         A63: (Mep .cost() ) = ((M .cost() ) + (WG1 . ep)) by A60, A59, A6, Th11;

        set MG2 = (( the_Edges_of M) /\ ( the_Edges_of G2));

        

         A64: (Gk `2 ) c= (PMST `2 ) by Th42;

        ep in {ep} by TARSKI:def 1;

        then

         A65: ep in (Gk `2 ) by A57, XBOOLE_0:def 3;

        then

         A66: ( {ep} /\ ( the_Edges_of G2)) = {ep} by A4, A64, ZFMISC_1: 46;

        now

          assume (MG2 /\ {ep}) <> {} ;

          then

          consider x be object such that

           A67: x in (MG2 /\ {ep}) by XBOOLE_0:def 1;

          x in {ep} by A67, XBOOLE_0:def 4;

          then

           A68: x = ep by TARSKI:def 1;

          x in MG2 by A67, XBOOLE_0:def 4;

          then x in ( the_Edges_of M) by XBOOLE_0:def 4;

          hence contradiction by A58, A68, ZFMISC_1: 31;

        end;

        then

         A69: MG2 misses {ep} by XBOOLE_0:def 7;

        set v1 = (( the_Source_of Mep) . ep), v2 = (( the_Target_of Mep) . ep);

        set V = (Gk1b `1 );

        

         A70: ( the_Weight_of Mep) = (WG1 | ( the_Edges_of Mep)) by GLIB_003:def 10;

        

         A71: VG1 = ( the_Vertices_of M) by GLIB_000:def 33;

        then

        reconsider V as non empty Subset of ( the_Vertices_of M) by Th30;

        

         A72: ( the_Edges_of Mep) = (( the_Edges_of M) \/ {ep}) by A61, GLIB_000:def 37;

        ( the_Vertices_of M) c= ( the_Vertices_of Mep) by A62;

        then

        reconsider M9 = M as connected Subgraph of Mep by A72, GLIB_000: 44, XBOOLE_1: 7;

        ep in {ep} by TARSKI:def 1;

        then

         A73: ep in ( the_Edges_of Mep) by A72, XBOOLE_0:def 3;

        ( the_Vertices_of Mep) = ( the_Vertices_of M) by A62, GLIB_000:def 33;

        then

        reconsider v1, v2 as Vertex of M by A73, FUNCT_2: 5;

        consider W be Walk of M9 such that

         A74: W is_Walk_from (v2,v1) by GLIB_002:def 1;

        set PW = the Path of W;

        reconsider P = PW as Path of Mep by GLIB_001: 175;

        

         A75: PW is_Walk_from (v2,v1) by A74, GLIB_001: 160;

        then

         A76: P is_Walk_from (v2,v1) by GLIB_001: 19;

         A77:

        now

          reconsider PM = P as Walk of M;

          let n be odd Element of NAT ;

          assume that

           A78: 1 < n & n <= ( len P) and

           A79: (P . n) = v2;

          v2 = (P .first() ) by A76, GLIB_001:def 23

          .= (P . ((2 * 0 ) + 1)) by GLIB_001:def 6;

          then n = ( len P) by A78, A79, GLIB_001:def 28;

          

          then (P .last() ) = v2 by A79, GLIB_001:def 7

          .= (P .first() ) by A76, GLIB_001:def 23;

          then P is closed by GLIB_001:def 24;

          then

           A80: PM is closed by GLIB_001: 176;

          PM is non trivial by A78, GLIB_001: 126;

          then PM is Cycle-like by A80, GLIB_001:def 31;

          hence contradiction by GLIB_002:def 2;

        end;

        

         A81: ep Joins (v1,v2,Mep) by A73;

        then

         A82: ep Joins ((P .last() ),v2,Mep) by A76, GLIB_001:def 23;

        ep Joins (v1,v2,G1) by A81, GLIB_000: 72;

        then

         A83: ep Joins (v1,v2,G29) by A4, A65, A64, GLIB_000: 73;

        v1 <> v2 by A83, GLIB_000:def 18;

        then v1 <> (P .first() ) by A76, GLIB_001:def 23;

        then (P .last() ) <> (P .first() ) by A76, GLIB_001:def 23;

        then

         A84: P is open by GLIB_001:def 24;

        (PW .edges() ) c= ( the_Edges_of M);

        then (P .edges() ) c= ( the_Edges_of M) by GLIB_001: 110;

        then not ep in (P .edges() ) by A58, ZFMISC_1: 31;

        then

         A85: (P .addEdge ep) is Path-like by A84, A82, A77, GLIB_001: 150;

        (P .addEdge ep) is_Walk_from (v2,v2) by A76, A81, GLIB_001: 66;

        then

         A86: (P .addEdge ep) is closed by GLIB_001: 119;

        ( the_Vertices_of M) c= ( the_Vertices_of Mep) by A62;

        then

        reconsider M9 = M as connected Subgraph of Mep by A72, GLIB_000: 44, XBOOLE_1: 7;

        ( the_Vertices_of M9) = ( the_Vertices_of Mep) by A62, GLIB_000:def 33;

        then M9 is spanning;

        then

         A87: Mep is connected by GLIB_002: 23;

        

         A88: v2 = (P . 1) by A75, GLIB_001: 17;

        set C = (P .addEdge ep);

        

         A89: v1 = (P . ( len P)) by A75, GLIB_001: 17;

        

         A90: (( the_Source_of G1) . ep) = v1 & (( the_Target_of G1) . ep) = v2 by A73, GLIB_000:def 32;

        now

          per cases by A56, A90;

            suppose

             A91: v1 in (Gk1b `1 ) & v2 in (VG1 \ (Gk1b `1 ));

            

             A92: ( len C) = (( len P) + 2) & (C . (( len P) + 1)) = ep by A82, GLIB_001: 64, GLIB_001: 65;

            defpred P3[ Nat] means $1 is odd & $1 <= ( len P) & (P . $1) in (Gk1b `1 );

            

             A93: ex n be Nat st P3[n] by A89, A91;

            consider m be Nat such that

             A94: P3[m] & for n be Nat st P3[n] holds m <= n from NAT_1:sch 5( A93);

            reconsider m as odd Element of NAT by A94, ORDINAL1:def 12;

            1 <= m & m <> 1 by A88, A91, A94, ABIAN: 12, XBOOLE_0:def 5;

            then 1 < m by XXREAL_0: 1;

            then (1 + 1) <= m by NAT_1: 13;

            then

            reconsider m2k = (m - (2 * 1)) as odd Element of NAT by INT_1: 5;

            

             A95: m2k < (m - 0 ) by XREAL_1: 15;

            then

             A96: m2k < ( len P) by A94, XXREAL_0: 2;

            then

             A97: not (P . m2k) in (Gk1b `1 ) by A94, A95;

            set em = (P . (m2k + 1));

            

             A98: em in (P .edges() ) by A96, GLIB_001: 100;

            then

            consider i be even Element of NAT such that

             A99: 1 <= i and

             A100: i <= ( len P) and

             A101: (P . i) = em by GLIB_001: 99;

            i in ( dom P) by A99, A100, FINSEQ_3: 25;

            then

             A102: (C . i) = em by A82, A101, GLIB_001: 65;

            take em;

            (C .edges() ) = ((P .edges() ) \/ {ep}) by A82, GLIB_001: 111;

            hence em in (C .edges() ) by A98, XBOOLE_0:def 3;

            

             A103: (( len P) + 1) <= (( len P) + 2) by XREAL_1: 7;

            (( len P) + 0 ) < (( len P) + 1) by XREAL_1: 8;

            then i < (( len P) + 1) by A100, XXREAL_0: 2;

            hence em <> ep by A85, A99, A102, A92, A103, GLIB_001: 138;

            (m2k + 2) = m;

            then

             A104: em Joins ((PW . m2k),(PW . m),M) by A96, GLIB_001:def 3;

            then (PW . m2k) in ( the_Vertices_of M) by GLIB_000: 13;

            then (PW . m2k) in (( the_Vertices_of M) \ (Gk1b `1 )) by A97, XBOOLE_0:def 5;

            hence em SJoins (V,(( the_Vertices_of M) \ V),M) by A94, A104;

          end;

            suppose

             A105: v2 in (Gk1b `1 ) & v1 in (VG1 \ (Gk1b `1 ));

            

             A106: ( len C) = (( len P) + 2) & (C . (( len P) + 1)) = ep by A82, GLIB_001: 64, GLIB_001: 65;

            defpred P3[ Nat] means $1 is odd & $1 <= ( len P) & (P . $1) in (VG1 \ (Gk1b `1 ));

            

             A107: ex n be Nat st P3[n] by A89, A105;

            consider m be Nat such that

             A108: P3[m] & for n be Nat st P3[n] holds m <= n from NAT_1:sch 5( A107);

            reconsider m as odd Element of NAT by A108, ORDINAL1:def 12;

            1 <= m & m <> 1 by A88, A105, A108, ABIAN: 12, XBOOLE_0:def 5;

            then 1 < m by XXREAL_0: 1;

            then (1 + 1) <= m by NAT_1: 13;

            then

            reconsider m2k = (m - (2 * 1)) as odd Element of NAT by INT_1: 5;

            

             A109: m2k < (m - 0 ) by XREAL_1: 15;

            then

             A110: m2k < ( len P) by A108, XXREAL_0: 2;

             A111:

            now

              assume

               A112: not (P . m2k) in (Gk1b `1 );

              (P . m2k) in VG1 by A71, A110, GLIB_001: 7;

              then (P . m2k) in (VG1 \ (Gk1b `1 )) by A112, XBOOLE_0:def 5;

              hence contradiction by A108, A109, A110;

            end;

            set em = (P . (m2k + 1));

            

             A113: em in (P .edges() ) by A110, GLIB_001: 100;

            then

            consider i be even Element of NAT such that

             A114: 1 <= i and

             A115: i <= ( len P) and

             A116: (P . i) = em by GLIB_001: 99;

            i in ( dom P) by A114, A115, FINSEQ_3: 25;

            then

             A117: (C . i) = em by A82, A116, GLIB_001: 65;

            take em;

            (C .edges() ) = ((P .edges() ) \/ {ep}) by A82, GLIB_001: 111;

            hence em in (C .edges() ) by A113, XBOOLE_0:def 3;

            

             A118: (( len P) + 1) <= (( len P) + 2) by XREAL_1: 7;

            (( len P) + 0 ) < (( len P) + 1) by XREAL_1: 8;

            then i < (( len P) + 1) by A115, XXREAL_0: 2;

            hence em <> ep by A85, A114, A117, A106, A118, GLIB_001: 138;

            (m2k + 2) = m;

            then em Joins ((PW . m2k),(PW . m),M) by A110, GLIB_001:def 3;

            hence em SJoins (V,(( the_Vertices_of M) \ V),M) by A71, A108, A111;

          end;

        end;

        then

        consider em be set such that

         A119: em in (C .edges() ) and

         A120: em <> ep and

         A121: em SJoins (V,(( the_Vertices_of M) \ V),M);

        set M2 = the weight-inheriting [Weighted] removeEdge of Mep, em;

        reconsider M2 as WSubgraph of G1 by GLIB_003: 9;

        

         A122: (M2 .order() ) = ( card VG1) by A62, GLIB_000: 53

        .= (M .order() ) by GLIB_000:def 33;

        

         A123: em SJoins (V,(VG1 \ V),G1) by A71, A121, GLIB_000: 72;

        then

         A124: (WG1 . ep) <= (WG1 . em) by A55, Def13;

        set M29 = (M2 | WGraphSelectors );

        

         A125: M29 == M2 by Lm4;

        

         A126: ( the_Edges_of M2) = ((( the_Edges_of M) \/ {ep}) \ {em}) by A72, GLIB_000: 51;

        then

         A127: ( the_Edges_of M29) = ((( the_Edges_of M) \/ {ep}) \ {em}) by A125;

         {em} c= (( the_Edges_of M) \/ {ep}) by A72, A119, ZFMISC_1: 31;

        

        then (M2 .size() ) = (( card (( the_Edges_of M) \/ {ep})) - ( card {em})) by A126, CARD_2: 44

        .= (( card (( the_Edges_of M) \/ {ep})) - 1) by CARD_1: 30

        .= ((( card ( the_Edges_of M)) + 1) - 1) by A59, CARD_2: 41

        .= (M .size() );

        then

         A128: (M2 .order() ) = ((M2 .size() ) + 1) by A122, GLIB_002: 46;

        

         A129: ( the_Weight_of M29) = ( the_Weight_of M2) by Lm4;

        then

        reconsider M29 as WSubgraph of G1 by A125, GLIB_003: 8;

        

         A130: ( the_Vertices_of M29) = ( the_Vertices_of M2) by A125

        .= VG1 by A62, GLIB_000: 53;

        (P .addEdge ep) is non trivial by A82, GLIB_001: 132;

        then C is Cycle-like by A85, A86, GLIB_001:def 31;

        then M2 is connected by A119, A87, GLIB_002: 5;

        then M2 is Tree-like by A128, GLIB_002: 47;

        then M29 is Tree-like by Lm4, GLIB_002: 48;

        then

        reconsider M29 as spanning Tree-like WSubgraph of G1 by A130, GLIB_000:def 33;

        ((M2 .cost() ) + (( the_Weight_of Mep) . em)) = (Mep .cost() ) by A119, Th10;

        then (M2 .cost() ) = ((Mep .cost() ) - (( the_Weight_of Mep) . em));

        then (M2 .cost() ) = (((M .cost() ) + (WG1 . ep)) - (WG1 . em)) by A119, A63, A70, FUNCT_1: 49;

        then (M29 .cost() ) = (((M .cost() ) + (WG1 . ep)) - (WG1 . em)) by A125, A129;

        then

         A131: (((M29 .cost() ) + (WG1 . em)) - (WG1 . em)) <= (((M .cost() ) + (WG1 . ep)) - (WG1 . ep)) by A124, XREAL_1: 13;

        now

          let G3 be spanning Tree-like WSubgraph of G1;

          (M .cost() ) <= (G3 .cost() ) by Def19;

          hence (M29 .cost() ) <= (G3 .cost() ) by A131, XXREAL_0: 2;

        end;

        then

        reconsider M29 as minimumSpanningTree of G1 by Def19;

        set MG29 = (( the_Edges_of M29) /\ ( the_Edges_of G2));

        

         A132: MG29 = (((( the_Edges_of M) \/ {ep}) /\ ( the_Edges_of G2)) \ ( {em} /\ ( the_Edges_of G2))) by A127, XBOOLE_1: 50;

        ( dom M29) = WGraphSelectors by Lm5;

        then M29 in (G1 .allWSubgraphs() ) by Def5;

        then

         A133: M29 in X;

         A134:

        now

          thus not ((PCS . (k1o + 1)) `2 ) c= ( the_Edges_of M) by A50, A52;

          let n be Nat;

          assume n <= k1o;

          then ((PCS . n) `2 ) c= (Gk1b `2 ) by Th34;

          hence ((PCS . n) `2 ) c= ( the_Edges_of M) by A53;

        end;

         A135:

        now

          consider k2 be Nat such that

           A136: Z[M29, k2] by A8, A133;

           A137:

          now

            set Vr = (VG1 \ V);

            assume

             A138: em in (Gk1b `2 );

            

             A139: (Gk1b `2 ) c= (G1 .edgesBetween (Gk1b `1 )) by Th30;

            then (( the_Target_of G1) . em) in (Gk1b `1 ) by A138, GLIB_000: 31;

            then

             A140: not (( the_Target_of G1) . em) in Vr by XBOOLE_0:def 5;

            (( the_Source_of G1) . em) in (Gk1b `1 ) by A138, A139, GLIB_000: 31;

            then not (( the_Source_of G1) . em) in Vr by XBOOLE_0:def 5;

            hence contradiction by A123, A140;

          end;

          now

            let x be object;

            assume

             A141: x in (Gk `2 );

            now

              per cases by A57, A141, XBOOLE_0:def 3;

                suppose x in (Gk1b `2 );

                then x in (( the_Edges_of M) \/ {ep}) & not x in {em} by A53, A137, TARSKI:def 1, XBOOLE_0:def 3;

                hence x in ( the_Edges_of M29) by A127, XBOOLE_0:def 5;

              end;

                suppose

                 A142: x in {ep};

                then x = ep by TARSKI:def 1;

                then

                 A143: not x in {em} by A120, TARSKI:def 1;

                x in (( the_Edges_of M) \/ {ep}) by A142, XBOOLE_0:def 3;

                hence x in ( the_Edges_of M29) by A127, A143, XBOOLE_0:def 5;

              end;

            end;

            hence x in ( the_Edges_of M29);

          end;

          then

           A144: (Gk `2 ) c= ( the_Edges_of M29);

           A145:

          now

            assume k2 < k;

            then (k2 + 1) <= k by NAT_1: 13;

            then ((PCS . (k2 + 1)) `2 ) c= (Gk `2 ) by Th34;

            hence contradiction by A136, A144, XBOOLE_1: 1;

          end;

          assume

           A146: em in ( the_Edges_of G2);

          now

            let x be object;

            assume x in {em};

            then x = em by TARSKI:def 1;

            hence x in ((( the_Edges_of M) \/ {ep}) /\ ( the_Edges_of G2)) by A72, A119, A146, XBOOLE_0:def 4;

          end;

          then

           A147: {em} c= ((( the_Edges_of M) \/ {ep}) /\ ( the_Edges_of G2));

          MG29 = (((( the_Edges_of M) \/ {ep}) /\ ( the_Edges_of G2)) \ {em}) by A132, A146, ZFMISC_1: 46;

          

          then ( card MG29) = (( card (( the_Edges_of Mep) /\ ( the_Edges_of G2))) - ( card {em})) by A72, A147, CARD_2: 44

          .= (( card (( the_Edges_of Mep) /\ ( the_Edges_of G2))) - 1) by CARD_1: 30

          .= (( card (MG2 \/ {ep})) - 1) by A72, A66, XBOOLE_1: 23

          .= ((( card MG2) + ( card {ep})) - 1) by A69, CARD_2: 40

          .= ((( card MG2) + 1) - 1) by CARD_1: 30

          .= ( card MG2);

          then

           A148: k1o >= k2 by A44, A133, A134, A136;

          ((k1o + 1) - 1) < (k - 0 ) by A52, XREAL_1: 15;

          hence contradiction by A145, A148, XXREAL_0: 2;

        end;

        now

          assume ( {em} /\ ( the_Edges_of G2)) <> {} ;

          then

          consider x be object such that

           A149: x in ( {em} /\ ( the_Edges_of G2)) by XBOOLE_0:def 1;

          x in {em} & x in ( the_Edges_of G2) by A149, XBOOLE_0:def 4;

          hence contradiction by A135, TARSKI:def 1;

        end;

        then

         A150: MG29 = (MG2 \/ ( {ep} /\ ( the_Edges_of G2))) by A132, XBOOLE_1: 23;

        now

          assume (MG2 /\ {ep}) <> {} ;

          then

          consider x be object such that

           A151: x in (MG2 /\ {ep}) by XBOOLE_0:def 1;

          x in {ep} by A151, XBOOLE_0:def 4;

          then

           A152: x = ep by TARSKI:def 1;

          x in MG2 by A151, XBOOLE_0:def 4;

          then x in ( the_Edges_of M) by XBOOLE_0:def 4;

          hence contradiction by A58, A152, ZFMISC_1: 31;

        end;

        then MG2 misses {ep} by XBOOLE_0:def 7;

        

        then ( card MG29) = (( card MG2) + ( card {ep})) by A66, A150, CARD_2: 40

        .= (( card MG2) + 1) by CARD_1: 30;

        then (( card MG2) + 0 ) >= (( card MG2) + 1) by A44, A133;

        hence contradiction by XREAL_1: 6;

      end;

      hence thesis;

    end;