glib_003.miz



    begin

    definition

      let D be set, fs be FinSequence of D, fss be Subset of fs;

      :: original: Seq

      redefine

      func Seq fss -> FinSequence of D ;

      correctness

      proof

        now

          let y be object;

          assume y in ( rng ( Seq fss));

          then

          consider x be object such that

           A1: x in ( dom ( Seq fss)) and

           A2: (( Seq fss) . x) = y by FUNCT_1:def 3;

          reconsider x as Element of NAT by A1;

          ex n be Element of NAT st n in ( dom fs) & x <= n & y = (fs . n) by A1, A2, GLIB_001: 4;

          then y in ( rng fs) by FUNCT_1:def 3;

          hence y in D;

        end;

        then ( rng ( Seq fss)) c= D by TARSKI:def 3;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    theorem :: GLIB_003:1

    for x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 be set, p be FinSequence st p = ((((((((( <*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ^ <*x10*>) holds ( len p) = 10 & (p . 1) = x1 & (p . 2) = x2 & (p . 3) = x3 & (p . 4) = x4 & (p . 5) = x5 & (p . 6) = x6 & (p . 7) = x7 & (p . 8) = x8 & (p . 9) = x9 & (p . 10) = x10

    proof

      let x1,x2,x3,x4,x5,x6,x7,x8,x9,x10 be set, p be FinSequence;

      set pa = (((((((( <*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>);

      

       A1: (pa . 1) = x1 & (pa . 2) = x2 by FINSEQ_1: 71;

      

       A2: (pa . 5) = x5 & (pa . 6) = x6 by FINSEQ_1: 71;

      

       A3: (pa . 7) = x7 & (pa . 8) = x8 by FINSEQ_1: 71;

      

       A4: ( len pa) = 9 by FINSEQ_1: 71;

      then

       A5: ( dom pa) = ( Seg 9) by FINSEQ_1:def 3;

      then

       A6: 3 in ( dom pa) & 4 in ( dom pa) by FINSEQ_1: 1;

      

       A7: (pa . 9) = x9 & 9 in ( dom pa) by A5, FINSEQ_1: 1, FINSEQ_1: 71;

      assume

       A8: p = ((((((((( <*x1*> ^ <*x2*>) ^ <*x3*>) ^ <*x4*>) ^ <*x5*>) ^ <*x6*>) ^ <*x7*>) ^ <*x8*>) ^ <*x9*>) ^ <*x10*>);

      

      hence ( len p) = (( len pa) + ( len <*x10*>)) by FINSEQ_1: 22

      .= (9 + 1) by A4, FINSEQ_1: 40

      .= 10;

      

       A9: (pa . 3) = x3 & (pa . 4) = x4 by FINSEQ_1: 71;

      

       A10: 7 in ( dom pa) & 8 in ( dom pa) by A5, FINSEQ_1: 1;

      

       A11: 5 in ( dom pa) & 6 in ( dom pa) by A5, FINSEQ_1: 1;

      1 in ( dom pa) & 2 in ( dom pa) by A5, FINSEQ_1: 1;

      hence (p . 1) = x1 & (p . 2) = x2 & (p . 3) = x3 & (p . 4) = x4 & (p . 5) = x5 & (p . 6) = x6 & (p . 7) = x7 & (p . 8) = x8 & (p . 9) = x9 by A8, A1, A9, A2, A3, A6, A11, A10, A7, FINSEQ_1:def 7;

      

      thus (p . 10) = (p . (( len pa) + 1)) by A4

      .= x10 by A8, FINSEQ_1: 42;

    end;

    theorem :: GLIB_003:2

    

     Th2: for fs be FinSequence of REAL , fss be Subset of fs holds (for i be Element of NAT st i in ( dom fs) holds 0 <= (fs . i)) implies ( Sum ( Seq fss)) <= ( Sum fs)

    proof

      let fs be FinSequence of REAL , fss be Subset of fs;

      defpred P[ Nat] means for fs be FinSequence of REAL , fss be Subset of fs st (for i be Element of NAT st i in ( dom fs) holds 0 <= (fs . i)) & ( len ( Seq fss)) = $1 holds ( Sum ( Seq fss)) <= ( Sum fs);

      assume

       A1: for i be Element of NAT st i in ( dom fs) holds 0 <= (fs . i);

      

       A2: ( len ( Seq fss)) = ( len ( Seq fss));

      now

        let k be Nat;

        assume

         A3: P[k];

        let fs be FinSequence of REAL , fss be Subset of fs;

        assume that

         A4: for i be Element of NAT st i in ( dom fs) holds 0 <= (fs . i) and

         A5: ( len ( Seq fss)) = (k + 1);

        consider q be FinSequence of REAL , z be Element of REAL such that

         A6: ( Seq fss) = (q ^ <*z*>) by A5, FINSEQ_2: 19;

        ( card fss) = (k + 1) by A5, GLIB_001: 5;

        then ( dom fss) <> {} by CARD_1: 27, RELAT_1: 41;

        then

        consider d be object such that

         A7: d in ( dom fss) by XBOOLE_0:def 1;

        

         A8: ( dom fss) c= ( dom fs) by FINSEQ_6: 151;

        then

         A9: d in ( dom fs) by A7;

        defpred P2[ Nat] means $1 in ( dom fss);

        consider L be Nat such that

         A10: ( dom fss) c= ( Seg L) by FINSEQ_1:def 12;

        

         A11: for n be Nat st P2[n] holds n <= L by A10, FINSEQ_1: 1;

        reconsider d as Element of NAT by A9;

        d in ( dom fss) by A7;

        then

         A12: ex d be Nat st P2[d];

        consider x be Nat such that

         A13: P2[x] & for n be Nat st P2[n] holds n <= x from NAT_1:sch 6( A11, A12);

        set y = (fs . x);

        

         A14: ( len ( Seq fss)) = (( len q) + ( len <*z*>)) by A6, FINSEQ_1: 22;

        then

         A15: (k + 1) = (( len q) + 1) by A5, FINSEQ_1: 39;

        now

          set g = ( Sgm ( dom fss));

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

          then

           A16: ( len ( Seq fss)) in ( dom ( Seq fss)) by A5, FINSEQ_3: 25;

          

           A17: ( len ( Seq fss)) = ( card fss) by GLIB_001: 5

          .= ( card ( dom fss)) by CARD_1: 62

          .= ( len ( Sgm ( dom fss))) by A10, FINSEQ_3: 39;

           A18:

          now

            set k2 = (g . ( len g));

            assume

             A19: (g . ( len ( Seq fss))) <> x;

            1 <= ( len g) by A5, A17, NAT_1: 12;

            then ( len g) in ( dom g) by FINSEQ_3: 25;

            then

             A20: k2 in ( rng g) by FUNCT_1:def 3;

            reconsider k2 as Element of NAT ;

            

             A21: ( rng g) = ( dom fss) by A10, FINSEQ_1:def 13;

            then

            consider v be object such that

             A22: v in ( dom g) and

             A23: (g . v) = x by A13, FUNCT_1:def 3;

            reconsider v as Element of NAT by A22;

            v <= ( len g) by A22, FINSEQ_3: 25;

            then

             A24: v < ( len g) by A17, A19, A23, XXREAL_0: 1;

            1 <= v by A22, FINSEQ_3: 25;

            then x < k2 by A10, A23, A24, FINSEQ_1:def 13;

            hence contradiction by A13, A21, A20;

          end;

          (( Seq fss) . ( len ( Seq fss))) = z & ( Seq fss) = (fss * ( Sgm ( dom fss))) by A5, A6, A15, FINSEQ_1: 42, FINSEQ_1:def 14;

          then (fss . (( Sgm ( dom fss)) . ( len ( Seq fss)))) = z by A16, FUNCT_1: 12;

          then [x, z] in fss by A13, A18, FUNCT_1: 1;

          hence y = z by FUNCT_1: 1;

        end;

        then

         A25: ( Sum ( Seq fss)) = (y + ( Sum q)) by A6, RVSUM_1: 74;

        

         A26: x <= ( len fs) by A8, A13, FINSEQ_3: 25;

        then

        consider j be Nat such that

         A27: (x + j) = ( len fs) by NAT_1: 10;

        

         A28: 1 <= x by A8, A13, FINSEQ_3: 25;

        then

        reconsider xx1 = (x - 1) as Element of NAT by INT_1: 5;

        set fssq = (fss | ( Seg xx1));

        reconsider fssq as Subset of fs by FINSEQ_6: 153;

        consider fsD,fsC be FinSequence of REAL such that

         A29: ( len fsD) = x and ( len fsC) = j and

         A30: fs = (fsD ^ fsC) by A27, FINSEQ_2: 23;

        

         A31: (xx1 + 1) = x;

        then

        consider fsA,fsB be FinSequence of REAL such that

         A32: ( len fsA) = xx1 and

         A33: ( len fsB) = 1 and

         A34: fsD = (fsA ^ fsB) by A29, FINSEQ_2: 23;

        x in ( dom fsD) by A28, A29, FINSEQ_3: 25;

        then

         A35: y = (fsD . x) by A30, FINSEQ_1:def 7;

        now

          let z be object;

          assume

           A36: z in fssq;

          then

          consider a,b be object such that

           A37: z = [a, b] by RELAT_1:def 1;

          

           A38: a in ( Seg xx1) by A36, A37, RELAT_1:def 11;

          then

          reconsider a as Element of NAT ;

          

           A39: a <= xx1 by A38, FINSEQ_1: 1;

          

           A40: 1 <= a by A38, FINSEQ_1: 1;

          then

           A41: a in ( dom fsA) by A32, A39, FINSEQ_3: 25;

          

           A42: b = (fs . a) by A36, A37, FUNCT_1: 1;

          (a + 0 ) <= x by A31, A39, XREAL_1: 7;

          then a in ( dom fsD) by A29, A40, FINSEQ_3: 25;

          then b = (fsD . a) by A30, A42, FINSEQ_1:def 7;

          then b = (fsA . a) by A34, A41, FINSEQ_1:def 7;

          hence z in fsA by A37, A41, FUNCT_1: 1;

        end;

        then

        reconsider fssq as Subset of fsA by TARSKI:def 3;

        now

           A43:

          now

            let z be object;

            assume z in { [x, y]};

            then

             A44: z = [x, y] by TARSKI:def 1;

             [x, (fss . x)] in fss by A13, FUNCT_1: 1;

            hence z in fss by A44, FUNCT_1: 1;

          end;

          now

             [x, y] in { [x, y]} by TARSKI:def 1;

            then

             A45: [x, y] in fss by A43;

            let z be object;

            hereby

              assume

               A46: z in fssq;

              then

              consider a,b be object such that

               A47: z = [a, b] by RELAT_1:def 1;

              

               A48: a in ( Seg xx1) by A46, A47, RELAT_1:def 11;

              then

              reconsider a as Element of NAT ;

              a <= xx1 by A48, FINSEQ_1: 1;

              then a < x by A31, NAT_1: 13;

              then [a, b] <> [x, y] by XTUPLE_0: 1;

              then

               A49: not z in { [x, y]} by A47, TARSKI:def 1;

              z in fss by A46, A47, RELAT_1:def 11;

              hence z in (fss \ { [x, y]}) by A49, XBOOLE_0:def 5;

            end;

            assume

             A50: z in (fss \ { [x, y]});

            then

            consider a,b be object such that

             A51: z = [a, b] by RELAT_1:def 1;

            

             A52: a in ( dom fs) by A50, A51, FUNCT_1: 1;

            

             A53: z in fss by A50, XBOOLE_0:def 5;

            then

             A54: a in ( dom fss) by A51, FUNCT_1: 1;

            reconsider a as Element of NAT by A52;

            

             A55: a <= x by A13, A54;

             not z in { [x, y]} by A50, XBOOLE_0:def 5;

            then a <> x or b <> y by A51, TARSKI:def 1;

            then a <> x by A50, A51, A45, FUNCT_1:def 1;

            then a < x by A55, XXREAL_0: 1;

            then (a + 1) <= x by NAT_1: 13;

            then

             A56: ((a + 1) - 1) <= (x - 1) by XREAL_1: 13;

            1 <= a by A52, FINSEQ_3: 25;

            then a in ( Seg xx1) by A56, FINSEQ_1: 1;

            hence z in fssq by A51, A53, RELAT_1:def 11;

          end;

          then

           A57: fssq = (fss \ { [x, y]}) by TARSKI: 2;

          now

            let z be object;

            hereby

              assume

               A58: z in ( dom fss);

              then

               A59: [z, (fss . z)] in fss by FUNCT_1: 1;

              then

               A60: z in ( dom fs) by FUNCT_1: 1;

              then

              reconsider z9 = z as Element of NAT ;

              

               A61: 1 <= z9 by A60, FINSEQ_3: 25;

              

               A62: z9 <= x by A13, A58;

              now

                assume not z in {x};

                then z <> x by TARSKI:def 1;

                then z9 < (xx1 + 1) by A62, XXREAL_0: 1;

                then z9 <= xx1 by NAT_1: 13;

                then z9 in ( Seg xx1) by A61, FINSEQ_1: 1;

                then [z, (fss . z)] in fssq by A59, RELAT_1:def 11;

                hence z in ( dom fssq) by FUNCT_1: 1;

              end;

              hence z in (( dom fssq) \/ {x}) by XBOOLE_0:def 3;

            end;

            assume

             A63: z in (( dom fssq) \/ {x});

            now

              per cases by A63, XBOOLE_0:def 3;

                suppose z in ( dom fssq);

                then [z, (fssq . z)] in fssq by FUNCT_1: 1;

                then [z, (fssq . z)] in fss by RELAT_1:def 11;

                hence z in ( dom fss) by FUNCT_1: 1;

              end;

                suppose z in {x};

                hence z in ( dom fss) by A13, TARSKI:def 1;

              end;

            end;

            hence z in ( dom fss);

          end;

          then

           A64: ( dom fss) = (( dom fssq) \/ {x}) by TARSKI: 2;

          

           A65: ( card fss) = (k + 1) by A5, GLIB_001: 5;

           A66:

          now

            let m,n be Nat;

            assume that

             A67: m in ( dom fssq) and

             A68: n in {x};

             [m, (fssq . m)] in fssq by A67, FUNCT_1: 1;

            then m in ( Seg xx1) by RELAT_1:def 11;

            then

             A69: m <= xx1 by FINSEQ_1: 1;

            n = x by A68, TARSKI:def 1;

            hence m < n by A31, A69, NAT_1: 13;

          end;

           { [x, y]} c= fss by A43, TARSKI:def 3;

          

          then

           A70: ( card fssq) = (( card fss) - ( card { [x, y]})) by A57, CARD_2: 44

          .= ((k + 1) - 1) by A65, CARD_1: 30

          .= k;

          hence ( len q) = ( len ( Seq fssq)) by A15, GLIB_001: 5;

          let n be Nat;

          set x1 = (( Sgm ( dom fss)) . n), x2 = (( Sgm ( dom fssq)) . n);

          assume that

           A71: 1 <= n and

           A72: n <= ( len q);

          n in ( dom q) by A71, A72, FINSEQ_3: 25;

          then

           A73: (q . n) = (( Seq fss) . n) by A6, FINSEQ_1:def 7;

          

           A74: ex lk be Nat st ( dom fssq) c= ( Seg lk) by FINSEQ_1:def 12;

          

          then ( len ( Sgm ( dom fssq))) = ( card ( dom fssq)) by FINSEQ_3: 39

          .= k by A70, CARD_1: 62;

          then

           A75: n in ( dom ( Sgm ( dom fssq))) by A15, A71, A72, FINSEQ_3: 25;

          then x2 in ( rng ( Sgm ( dom fssq))) by FUNCT_1:def 3;

          then x2 in ( dom fssq) by A74, FINSEQ_1:def 13;

          then [x2, (fssq . x2)] in fssq by FUNCT_1: 1;

          then [x2, (fssq . x2)] in fss by RELAT_1:def 11;

          then

           A76: (fss . x2) = (fssq . x2) by FUNCT_1: 1;

          n <= (k + 1) by A5, A14, A72, NAT_1: 12;

          then

           A77: n in ( dom ( Seq fss)) by A5, A71, FINSEQ_3: 25;

          ( Seq fss) = (fss * ( Sgm ( dom fss))) by FINSEQ_1:def 14;

          then

           A78: (q . n) = (fss . x1) by A73, A77, FUNCT_1: 12;

          

           A79: ( Seq fssq) = (fssq * ( Sgm ( dom fssq))) by FINSEQ_1:def 14;

          ( len ( Seq fssq)) = ( card fssq) by GLIB_001: 5;

          then n in ( dom ( Seq fssq)) by A15, A70, A71, A72, FINSEQ_3: 25;

          then

           A80: (( Seq fssq) . n) = (fssq . x2) by A79, FUNCT_1: 12;

          now

            let z be object;

            assume z in {x};

            then z = x by TARSKI:def 1;

            hence z in ( Seg ( len fs)) by A28, A26, FINSEQ_1: 1;

          end;

          then {x} c= ( Seg ( len fs)) by TARSKI:def 3;

          then ( Sgm ( dom fss)) = (( Sgm ( dom fssq)) ^ ( Sgm {x})) by A74, A64, A66, FINSEQ_3: 42;

          hence (q . n) = (( Seq fssq) . n) by A78, A80, A75, A76, FINSEQ_1:def 7;

        end;

        then

         A81: q = ( Seq fssq) by FINSEQ_1: 14;

        now

          

           A82: ( dom fsD) c= ( dom fs) by A30, FINSEQ_1: 26;

          let i be Element of NAT ;

          

           A83: ( dom fsA) c= ( dom fsD) by A34, FINSEQ_1: 26;

          assume

           A84: i in ( dom fsA);

          then (fsA . i) = (fsD . i) by A34, FINSEQ_1:def 7;

          then

           A85: (fsA . i) = (fs . i) by A30, A84, A83, FINSEQ_1:def 7;

          i in ( dom fsD) by A84, A83;

          hence 0 <= (fsA . i) by A4, A85, A82;

        end;

        then ( Sum q) <= ( Sum fsA) by A3, A15, A81;

        then (( Sum ( Seq fss)) + ( Sum q)) <= ((y + ( Sum q)) + ( Sum fsA)) by A25, XREAL_1: 7;

        then (( Sum ( Seq fss)) + ( Sum q)) <= ((y + ( Sum fsA)) + ( Sum q));

        then

         A86: ( Sum ( Seq fss)) <= (( Sum fsA) + y) by XREAL_1: 6;

        now

          let i be Nat;

          assume i in ( dom fsC);

          then (fs . (x + i)) = (fsC . i) & (x + i) in ( dom fs) by A29, A30, FINSEQ_1: 28, FINSEQ_1:def 7;

          hence 0 <= (fsC . i) by A4;

        end;

        then

         A87: 0 <= ( Sum fsC) by RVSUM_1: 84;

        1 in ( dom fsB) by A33, FINSEQ_3: 25;

        then y = (fsB . 1) by A31, A32, A34, A35, FINSEQ_1:def 7;

        then

         A88: fsB = <*y*> by A33, FINSEQ_1: 40;

        reconsider y as Element of REAL by XREAL_0:def 1;

        ( Sum fs) = (( Sum fsD) + ( Sum fsC)) by A30, RVSUM_1: 75

        .= ((( Sum fsA) + ( Sum <*y*>)) + ( Sum fsC)) by A34, A88, RVSUM_1: 75

        .= ((( Sum fsA) + y) + ( Sum fsC)) by FINSOP_1: 11;

        then ((( Sum fsA) + y) + 0 qua Nat) <= ( Sum fs) by A87, XREAL_1: 7;

        hence ( Sum ( Seq fss)) <= ( Sum fs) by A86, XXREAL_0: 2;

      end;

      then

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

      now

        let fs be FinSequence of REAL , fss be Subset of fs;

        assume (for i be Element of NAT st i in ( dom fs) holds 0 <= (fs . i)) & ( len ( Seq fss)) = 0 ;

        then (for i be Nat st i in ( dom fs) holds 0 <= (fs . i)) & ( Seq fss) = ( <*> REAL );

        hence ( Sum ( Seq fss)) <= ( Sum fs) by RVSUM_1: 72, RVSUM_1: 84;

      end;

      then

       A90: P[ 0 ];

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

      hence thesis by A1, A2;

    end;

    begin

    definition

      :: GLIB_003:def1

      func WeightSelector -> Element of NAT equals 5;

      coherence ;

      :: GLIB_003:def2

      func ELabelSelector -> Element of NAT equals 6;

      coherence ;

      :: GLIB_003:def3

      func VLabelSelector -> Element of NAT equals 7;

      coherence ;

    end

    definition

      let G be GraphStruct;

      :: GLIB_003:def4

      attr G is [Weighted] means

      : Def4: WeightSelector in ( dom G) & (G . WeightSelector ) is ManySortedSet of ( the_Edges_of G);

      :: GLIB_003:def5

      attr G is [ELabeled] means

      : Def5: ELabelSelector in ( dom G) & ex f be Function st (G . ELabelSelector ) = f & ( dom f) c= ( the_Edges_of G);

      :: GLIB_003:def6

      attr G is [VLabeled] means

      : Def6: VLabelSelector in ( dom G) & ex f be Function st (G . VLabelSelector ) = f & ( dom f) c= ( the_Vertices_of G);

    end

    registration

      cluster [Graph-like] [Weighted] [ELabeled] [VLabeled] for GraphStruct;

      existence

      proof

        set V5 = {1}, E3 = {} ;

        set S1 = the Function of E3, V5;

        set W1 = the ManySortedSet of E3;

        set EL8 = the PartFunc of E3, REAL ;

        set VL6 = the PartFunc of V5, REAL ;

        set G = (((((( <*V5*> ^ <*E3*>) ^ <*S1*>) ^ <*S1*>) ^ <*W1*>) ^ <*EL8*>) ^ <*VL6*>);

        

         A1: ( dom VL6) c= V5;

        

         A2: ( len G) = 7 by FINSEQ_1: 69;

        reconsider G as GraphStruct;

        

         A3: ( dom G) = ( Seg 7) by A2, FINSEQ_1:def 3;

        then

         A4: SourceSelector in ( dom G) & TargetSelector in ( dom G) by FINSEQ_1: 1;

        

         A5: WeightSelector in ( dom G) & ELabelSelector in ( dom G) by A3, FINSEQ_1: 1;

        

         A6: (G . WeightSelector ) = W1 & (G . ELabelSelector ) = EL8 by FINSEQ_1: 69;

        take G;

        

         A7: ( the_Vertices_of G) = V5 & ( the_Edges_of G) = E3 by FINSEQ_1: 69;

        

         A8: ( the_Source_of G) = S1 & ( the_Target_of G) = S1 by FINSEQ_1: 69;

        

         A9: VLabelSelector in ( dom G) by A3, FINSEQ_1: 1;

        

         A10: (G . VLabelSelector ) = VL6 & ( dom EL8) c= E3 by FINSEQ_1: 69;

         VertexSelector in ( dom G) & EdgeSelector in ( dom G) by A3, FINSEQ_1: 1;

        hence thesis by A4, A5, A9, A7, A8, A6, A10, A1;

      end;

    end

    definition

      mode WGraph is [Weighted] _Graph;

      mode EGraph is [ELabeled] _Graph;

      mode VGraph is [VLabeled] _Graph;

      mode WEGraph is [Weighted] [ELabeled] _Graph;

      mode WVGraph is [Weighted] [VLabeled] _Graph;

      mode EVGraph is [ELabeled] [VLabeled] _Graph;

      mode WEVGraph is [Weighted] [ELabeled] [VLabeled] _Graph;

    end

    definition

      let G be WGraph;

      :: GLIB_003:def7

      func the_Weight_of G -> ManySortedSet of ( the_Edges_of G) equals (G . WeightSelector );

      coherence by Def4;

    end

    definition

      let G be EGraph;

      :: GLIB_003:def8

      func the_ELabel_of G -> Function equals (G . ELabelSelector );

      coherence

      proof

        ex f be Function st (G . ELabelSelector ) = f & ( dom f) c= ( the_Edges_of G) by Def5;

        hence thesis;

      end;

    end

    definition

      let G be VGraph;

      :: GLIB_003:def9

      func the_VLabel_of G -> Function equals (G . VLabelSelector );

      coherence

      proof

        ex f be Function st (G . VLabelSelector ) = f & ( dom f) c= ( the_Vertices_of G) by Def6;

        hence thesis;

      end;

    end

    

     Lm1: for G be EGraph holds ( dom ( the_ELabel_of G)) c= ( the_Edges_of G)

    proof

      let G be EGraph;

      ex f be Function st (G . ELabelSelector ) = f & ( dom f) c= ( the_Edges_of G) by Def5;

      hence thesis;

    end;

    

     Lm2: for G be VGraph holds ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G)

    proof

      let G be VGraph;

      ex f be Function st (G . VLabelSelector ) = f & ( dom f) c= ( the_Vertices_of G) by Def6;

      hence thesis;

    end;

    registration

      let G be _Graph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> [Graph-like];

      coherence

      proof

         not WeightSelector in _GraphSelectors by ENUMSET1:def 2;

        hence thesis by GLIB_000: 10;

      end;

      cluster (G .set ( ELabelSelector ,X)) -> [Graph-like];

      coherence

      proof

         not ELabelSelector in _GraphSelectors by ENUMSET1:def 2;

        hence thesis by GLIB_000: 10;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> [Graph-like];

      coherence

      proof

         not VLabelSelector in _GraphSelectors by ENUMSET1:def 2;

        hence thesis by GLIB_000: 10;

      end;

    end

    

     Lm3: for G be _Graph, X be set holds (G .set ( WeightSelector ,X)) == G & (G .set ( ELabelSelector ,X)) == G & (G .set ( VLabelSelector ,X)) == G

    proof

      set GS = _GraphSelectors ;

      let G be _Graph, X be set;

      set G2 = (G .set ( WeightSelector ,X));

      

       A1: not WeightSelector in GS by ENUMSET1:def 2;

      then

       A2: ( the_Source_of G2) = ( the_Source_of G) & ( the_Target_of G2) = ( the_Target_of G) by GLIB_000: 10;

      ( the_Vertices_of G2) = ( the_Vertices_of G) & ( the_Edges_of G2) = ( the_Edges_of G) by A1, GLIB_000: 10;

      hence G2 == G by A2;

      set G2 = (G .set ( ELabelSelector ,X));

      

       A3: not ELabelSelector in GS by ENUMSET1:def 2;

      then

       A4: ( the_Source_of G2) = ( the_Source_of G) & ( the_Target_of G2) = ( the_Target_of G) by GLIB_000: 10;

      ( the_Vertices_of G2) = ( the_Vertices_of G) & ( the_Edges_of G2) = ( the_Edges_of G) by A3, GLIB_000: 10;

      hence G2 == G by A4;

      set G2 = (G .set ( VLabelSelector ,X));

      

       A5: not VLabelSelector in GS by ENUMSET1:def 2;

      then

       A6: ( the_Source_of G2) = ( the_Source_of G) & ( the_Target_of G2) = ( the_Target_of G) by GLIB_000: 10;

      ( the_Vertices_of G2) = ( the_Vertices_of G) & ( the_Edges_of G2) = ( the_Edges_of G) by A5, GLIB_000: 10;

      hence thesis by A6;

    end;

    registration

      let G be _finite _Graph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> _finite;

      coherence

      proof

        (G .set ( WeightSelector ,X)) == G by Lm3;

        hence thesis;

      end;

      cluster (G .set ( ELabelSelector ,X)) -> _finite;

      coherence

      proof

        (G .set ( ELabelSelector ,X)) == G by Lm3;

        hence thesis;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> _finite;

      coherence

      proof

        (G .set ( VLabelSelector ,X)) == G by Lm3;

        hence thesis;

      end;

    end

    registration

      let G be loopless _Graph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> loopless;

      coherence

      proof

        (G .set ( WeightSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

      cluster (G .set ( ELabelSelector ,X)) -> loopless;

      coherence

      proof

        (G .set ( ELabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> loopless;

      coherence

      proof

        (G .set ( VLabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

    end

    registration

      let G be _trivial _Graph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> _trivial;

      coherence

      proof

        (G .set ( WeightSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

      cluster (G .set ( ELabelSelector ,X)) -> _trivial;

      coherence

      proof

        (G .set ( ELabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> _trivial;

      coherence

      proof

        (G .set ( VLabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

    end

    registration

      let G be non _trivial _Graph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> non _trivial;

      coherence

      proof

        (G .set ( WeightSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

      cluster (G .set ( ELabelSelector ,X)) -> non _trivial;

      coherence

      proof

        (G .set ( ELabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> non _trivial;

      coherence

      proof

        (G .set ( VLabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

    end

    registration

      let G be non-multi _Graph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> non-multi;

      coherence

      proof

        (G .set ( WeightSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

      cluster (G .set ( ELabelSelector ,X)) -> non-multi;

      coherence

      proof

        (G .set ( ELabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> non-multi;

      coherence

      proof

        (G .set ( VLabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

    end

    registration

      let G be non-Dmulti _Graph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> non-Dmulti;

      coherence

      proof

        (G .set ( WeightSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

      cluster (G .set ( ELabelSelector ,X)) -> non-Dmulti;

      coherence

      proof

        (G .set ( ELabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> non-Dmulti;

      coherence

      proof

        (G .set ( VLabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_000: 89;

      end;

    end

    registration

      let G be connected _Graph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> connected;

      coherence

      proof

        (G .set ( WeightSelector ,X)) == G by Lm3;

        hence thesis by GLIB_002: 8;

      end;

      cluster (G .set ( ELabelSelector ,X)) -> connected;

      coherence

      proof

        (G .set ( ELabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_002: 8;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> connected;

      coherence

      proof

        (G .set ( VLabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_002: 8;

      end;

    end

    registration

      let G be acyclic _Graph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> acyclic;

      coherence

      proof

        (G .set ( WeightSelector ,X)) == G by Lm3;

        hence thesis by GLIB_002: 44;

      end;

      cluster (G .set ( ELabelSelector ,X)) -> acyclic;

      coherence

      proof

        (G .set ( ELabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_002: 44;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> acyclic;

      coherence

      proof

        (G .set ( VLabelSelector ,X)) == G by Lm3;

        hence thesis by GLIB_002: 44;

      end;

    end

    registration

      let G be WGraph, X be set;

      cluster (G .set ( ELabelSelector ,X)) -> [Weighted];

      coherence

      proof

        set G1 = (G .set ( ELabelSelector ,X));

        ( dom G) c= ( dom G1) & WeightSelector in ( dom G) by Def4, FUNCT_4: 10;

        hence WeightSelector in ( dom G1);

        G == G1 by Lm3;

        then

         A1: ( the_Edges_of G1) = ( the_Edges_of G);

        (G1 . WeightSelector ) = ( the_Weight_of G) by GLIB_000: 9;

        hence thesis by A1;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> [Weighted];

      coherence

      proof

        set G1 = (G .set ( VLabelSelector ,X));

        ( dom G) c= ( dom G1) & WeightSelector in ( dom G) by Def4, FUNCT_4: 10;

        hence WeightSelector in ( dom G1);

        G == G1 by Lm3;

        then

         A2: ( the_Edges_of G1) = ( the_Edges_of G);

        (G1 . WeightSelector ) = ( the_Weight_of G) by GLIB_000: 9;

        hence thesis by A2;

      end;

    end

    registration

      let G be _Graph, X be ManySortedSet of ( the_Edges_of G);

      cluster (G .set ( WeightSelector ,X)) -> [Weighted];

      coherence

      proof

        set G1 = (G .set ( WeightSelector ,X));

        ( dom G1) = (( dom G) \/ { WeightSelector }) & WeightSelector in { WeightSelector } by GLIB_000: 7, TARSKI:def 1;

        hence WeightSelector in ( dom G1) by XBOOLE_0:def 3;

        G == G1 by Lm3;

        then ( the_Edges_of G) = ( the_Edges_of G1);

        hence thesis by GLIB_000: 8;

      end;

    end

    registration

      let G be _Graph, WL be non empty set, W be Function of ( the_Edges_of G), WL;

      cluster (G .set ( WeightSelector ,W)) -> [Weighted];

      coherence ;

    end

    registration

      let G be EGraph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> [ELabeled];

      coherence

      proof

        set G1 = (G .set ( WeightSelector ,X));

        ( dom G) c= ( dom G1) & ELabelSelector in ( dom G) by Def5, FUNCT_4: 10;

        hence ELabelSelector in ( dom G1);

        G == G1 by Lm3;

        then

         A1: ( the_Edges_of G) = ( the_Edges_of G1);

        (G1 . ELabelSelector ) = ( the_ELabel_of G) & ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1, GLIB_000: 9;

        hence thesis by A1;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> [ELabeled];

      coherence

      proof

        set G1 = (G .set ( VLabelSelector ,X));

        ( dom G) c= ( dom G1) & ELabelSelector in ( dom G) by Def5, FUNCT_4: 10;

        hence ELabelSelector in ( dom G1);

        G == G1 by Lm3;

        then

         A2: ( the_Edges_of G) = ( the_Edges_of G1);

        (G1 . ELabelSelector ) = ( the_ELabel_of G) & ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1, GLIB_000: 9;

        hence thesis by A2;

      end;

    end

    registration

      let G be _Graph, Y be set, X be PartFunc of ( the_Edges_of G), Y;

      cluster (G .set ( ELabelSelector ,X)) -> [ELabeled];

      coherence

      proof

        set G1 = (G .set ( ELabelSelector ,X));

        ( dom G1) = (( dom G) \/ { ELabelSelector }) & ELabelSelector in { ELabelSelector } by GLIB_000: 7, TARSKI:def 1;

        hence ELabelSelector in ( dom G1) by XBOOLE_0:def 3;

        G == G1 by Lm3;

        then

         A1: ( the_Edges_of G) = ( the_Edges_of G1);

        ( dom X) c= ( the_Edges_of G);

        hence thesis by A1, GLIB_000: 8;

      end;

    end

    registration

      let G be _Graph, X be ManySortedSet of ( the_Edges_of G);

      cluster (G .set ( ELabelSelector ,X)) -> [ELabeled];

      coherence

      proof

        set G1 = (G .set ( ELabelSelector ,X));

        ( dom G1) = (( dom G) \/ { ELabelSelector }) & ELabelSelector in { ELabelSelector } by GLIB_000: 7, TARSKI:def 1;

        hence ELabelSelector in ( dom G1) by XBOOLE_0:def 3;

        G == G1 by Lm3;

        then

         A1: ( the_Edges_of G) = ( the_Edges_of G1);

        ( dom X) = ( the_Edges_of G) by PARTFUN1:def 2;

        hence thesis by A1, GLIB_000: 8;

      end;

    end

    registration

      let G be VGraph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> [VLabeled];

      coherence

      proof

        set G1 = (G .set ( WeightSelector ,X));

        ( dom G) c= ( dom G1) & VLabelSelector in ( dom G) by Def6, FUNCT_4: 10;

        hence VLabelSelector in ( dom G1);

        G == G1 by Lm3;

        then

         A1: ( the_Vertices_of G) = ( the_Vertices_of G1);

        (G1 . VLabelSelector ) = ( the_VLabel_of G) & ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2, GLIB_000: 9;

        hence thesis by A1;

      end;

      cluster (G .set ( ELabelSelector ,X)) -> [VLabeled];

      coherence

      proof

        set G1 = (G .set ( ELabelSelector ,X));

        ( dom G) c= ( dom G1) & VLabelSelector in ( dom G) by Def6, FUNCT_4: 10;

        hence VLabelSelector in ( dom G1);

        G == G1 by Lm3;

        then

         A2: ( the_Vertices_of G) = ( the_Vertices_of G1);

        (G1 . VLabelSelector ) = ( the_VLabel_of G) & ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2, GLIB_000: 9;

        hence thesis by A2;

      end;

    end

    registration

      let G be _Graph, Y be set, X be PartFunc of ( the_Vertices_of G), Y;

      cluster (G .set ( VLabelSelector ,X)) -> [VLabeled];

      coherence

      proof

        set G1 = (G .set ( VLabelSelector ,X));

        ( dom G1) = (( dom G) \/ { VLabelSelector }) & VLabelSelector in { VLabelSelector } by GLIB_000: 7, TARSKI:def 1;

        hence VLabelSelector in ( dom G1) by XBOOLE_0:def 3;

        G == G1 by Lm3;

        then

         A1: ( the_Vertices_of G) = ( the_Vertices_of G1);

        ( dom X) c= ( the_Vertices_of G);

        hence thesis by A1, GLIB_000: 8;

      end;

    end

    registration

      let G be _Graph, X be ManySortedSet of ( the_Vertices_of G);

      cluster (G .set ( VLabelSelector ,X)) -> [VLabeled];

      coherence

      proof

        set G1 = (G .set ( VLabelSelector ,X));

        ( dom G1) = (( dom G) \/ { VLabelSelector }) & VLabelSelector in { VLabelSelector } by GLIB_000: 7, TARSKI:def 1;

        hence VLabelSelector in ( dom G1) by XBOOLE_0:def 3;

        G == G1 by Lm3;

        then

         A1: ( the_Vertices_of G) = ( the_Vertices_of G1);

        ( dom X) = ( the_Vertices_of G) by PARTFUN1:def 2;

        hence thesis by A1, GLIB_000: 8;

      end;

    end

    registration

      let G be _Graph;

      cluster (G .set ( ELabelSelector , {} )) -> [ELabeled];

      coherence

      proof

        reconsider X = {} as PartFunc of ( the_Edges_of G), {} by RELSET_1: 12;

        (G .set ( ELabelSelector ,X)) is [ELabeled];

        hence thesis;

      end;

      cluster (G .set ( VLabelSelector , {} )) -> [VLabeled];

      coherence

      proof

        reconsider X = {} as PartFunc of ( the_Vertices_of G), {} by RELSET_1: 12;

        (G .set ( VLabelSelector ,X)) is [VLabeled];

        hence thesis;

      end;

    end

    registration

      let G be _Graph;

      cluster [Weighted] [ELabeled] [VLabeled] for Subgraph of G;

      existence

      proof

        set W = the ManySortedSet of ( the_Edges_of G);

        set G2 = (G .set ( WeightSelector ,W));

        set E = the PartFunc of ( the_Edges_of G2), REAL ;

        set G3 = (G2 .set ( ELabelSelector ,E));

        set V = the PartFunc of ( the_Vertices_of G3), REAL ;

        set G4 = (G3 .set ( VLabelSelector ,V));

        G == G2 & G2 == G3 by Lm3;

        then

         A1: G == G3;

        G3 == G4 by Lm3;

        then G == G4 by A1;

        then G4 is Subgraph of G by GLIB_000: 87;

        hence thesis;

      end;

    end

    definition

      let G be WGraph, G2 be [Weighted] Subgraph of G;

      :: GLIB_003:def10

      attr G2 is weight-inheriting means

      : Def10: ( the_Weight_of G2) = (( the_Weight_of G) | ( the_Edges_of G2));

    end

    definition

      let G be EGraph, G2 be [ELabeled] Subgraph of G;

      :: GLIB_003:def11

      attr G2 is elabel-inheriting means

      : Def11: ( the_ELabel_of G2) = (( the_ELabel_of G) | ( the_Edges_of G2));

    end

    definition

      let G be VGraph, G2 be [VLabeled] Subgraph of G;

      :: GLIB_003:def12

      attr G2 is vlabel-inheriting means

      : Def12: ( the_VLabel_of G2) = (( the_VLabel_of G) | ( the_Vertices_of G2));

    end

    registration

      let G be WGraph;

      cluster weight-inheriting for [Weighted] Subgraph of G;

      existence

      proof

        reconsider GG = G as [Weighted] Subgraph of G by GLIB_000: 40;

        take GG;

        thus thesis;

      end;

    end

    registration

      let G be EGraph;

      cluster elabel-inheriting for [ELabeled] Subgraph of G;

      existence

      proof

        reconsider GG = G as [ELabeled] Subgraph of G by GLIB_000: 40;

        take GG;

        ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1;

        then ( the_ELabel_of GG) = (( the_ELabel_of G) | ( the_Edges_of G)) by RELAT_1: 68;

        hence thesis;

      end;

    end

    registration

      let G be VGraph;

      cluster vlabel-inheriting for [VLabeled] Subgraph of G;

      existence

      proof

        reconsider GG = G as [VLabeled] Subgraph of G by GLIB_000: 40;

        take GG;

        ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2;

        then ( the_VLabel_of GG) = (( the_VLabel_of G) | ( the_Vertices_of G)) by RELAT_1: 68;

        hence thesis;

      end;

    end

    registration

      let G be WEGraph;

      cluster weight-inheriting elabel-inheriting for [Weighted] [ELabeled] Subgraph of G;

      existence

      proof

        reconsider GG = G as [Weighted] [ELabeled] Subgraph of G by GLIB_000: 40;

        take GG;

        thus GG is weight-inheriting;

        ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1;

        then ( the_ELabel_of GG) = (( the_ELabel_of G) | ( the_Edges_of G)) by RELAT_1: 68;

        hence thesis;

      end;

    end

    registration

      let G be WVGraph;

      cluster weight-inheriting vlabel-inheriting for [Weighted] [VLabeled] Subgraph of G;

      existence

      proof

        reconsider GG = G as [Weighted] [VLabeled] Subgraph of G by GLIB_000: 40;

        take GG;

        thus GG is weight-inheriting;

        ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2;

        then ( the_VLabel_of GG) = (( the_VLabel_of G) | ( the_Vertices_of G)) by RELAT_1: 68;

        hence thesis;

      end;

    end

    registration

      let G be EVGraph;

      cluster elabel-inheriting vlabel-inheriting for [ELabeled] [VLabeled] Subgraph of G;

      existence

      proof

        reconsider GG = G as [ELabeled] [VLabeled] Subgraph of G by GLIB_000: 40;

        take GG;

        ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1;

        then ( the_ELabel_of GG) = (( the_ELabel_of G) | ( the_Edges_of G)) by RELAT_1: 68;

        hence GG is elabel-inheriting;

        ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2;

        then ( the_VLabel_of GG) = (( the_VLabel_of G) | ( the_Vertices_of G)) by RELAT_1: 68;

        hence thesis;

      end;

    end

    registration

      let G be WEVGraph;

      cluster weight-inheriting elabel-inheriting vlabel-inheriting for [Weighted] [ELabeled] [VLabeled] Subgraph of G;

      existence

      proof

        reconsider GG = G as [Weighted] [ELabeled] [VLabeled] Subgraph of G by GLIB_000: 40;

        take GG;

        thus GG is weight-inheriting;

        ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1;

        then ( the_ELabel_of GG) = (( the_ELabel_of G) | ( the_Edges_of G)) by RELAT_1: 68;

        hence GG is elabel-inheriting;

        ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2;

        then ( the_VLabel_of GG) = (( the_VLabel_of G) | ( the_Vertices_of G)) by RELAT_1: 68;

        hence thesis;

      end;

    end

    definition

      let G be WGraph;

      mode WSubgraph of G is weight-inheriting [Weighted] Subgraph of G;

    end

    definition

      let G be EGraph;

      mode ESubgraph of G is elabel-inheriting [ELabeled] Subgraph of G;

    end

    definition

      let G be VGraph;

      mode VSubgraph of G is vlabel-inheriting [VLabeled] Subgraph of G;

    end

    definition

      let G be WEGraph;

      mode WESubgraph of G is weight-inheriting elabel-inheriting [Weighted] [ELabeled] Subgraph of G;

    end

    definition

      let G be WVGraph;

      mode WVSubgraph of G is weight-inheriting vlabel-inheriting [Weighted] [VLabeled] Subgraph of G;

    end

    definition

      let G be EVGraph;

      mode EVSubgraph of G is elabel-inheriting vlabel-inheriting [ELabeled] [VLabeled] Subgraph of G;

    end

    definition

      let G be WEVGraph;

      mode WEVSubgraph of G is weight-inheriting elabel-inheriting vlabel-inheriting [Weighted] [ELabeled] [VLabeled] Subgraph of G;

    end

    registration

      let G be _Graph, V,E be set;

      cluster [Weighted] [ELabeled] [VLabeled] for inducedSubgraph of G, V, E;

      existence

      proof

        now

          per cases ;

            suppose

             A1: V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V);

            set X = the inducedSubgraph of G, V, E;

            set W = the ManySortedSet of ( the_Edges_of X);

            set G2 = (X .set ( WeightSelector ,W));

            set EL = the PartFunc of ( the_Edges_of G2), REAL ;

            set G3 = (G2 .set ( ELabelSelector ,EL));

            set VL = the PartFunc of ( the_Vertices_of G3), REAL ;

            set G4 = (G3 .set ( VLabelSelector ,VL));

            X == G2 & G2 == G3 by Lm3;

            then

             A2: X == G3;

            G3 == G4 by Lm3;

            then

             A3: X == G4 by A2;

            then G4 is Subgraph of X by GLIB_000: 87;

            then

            reconsider G4 as Subgraph of G by GLIB_000: 43;

            ( the_Edges_of X) = E by A1, GLIB_000:def 37;

            then

             A4: ( the_Edges_of G4) = E by A3;

            ( the_Vertices_of X) = V by A1, GLIB_000:def 37;

            then ( the_Vertices_of G4) = V by A3;

            then G4 is inducedSubgraph of G, V, E by A1, A4, GLIB_000:def 37;

            hence thesis;

          end;

            suppose

             A5: not (V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V));

            set W = the ManySortedSet of ( the_Edges_of G);

            set G2 = (G .set ( WeightSelector ,W));

            set EL = the PartFunc of ( the_Edges_of G2), REAL ;

            set G3 = (G2 .set ( ELabelSelector ,EL));

            set VL = the PartFunc of ( the_Vertices_of G3), REAL ;

            set G4 = (G3 .set ( VLabelSelector ,VL));

            G == G2 & G2 == G3 by Lm3;

            then

             A6: G == G3;

            G3 == G4 by Lm3;

            then

             A7: G == G4 by A6;

            then

            reconsider G4 as Subgraph of G by GLIB_000: 87;

            G4 is inducedSubgraph of G, V, E by A5, A7, GLIB_000:def 37;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be WGraph, V,E be set;

      cluster weight-inheriting for [Weighted] inducedSubgraph of G, V, E;

      existence

      proof

        now

          per cases ;

            suppose

             A1: V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V);

            set X = the [Weighted] inducedSubgraph of G, V, E;

            set W = (( the_Weight_of G) | ( the_Edges_of X));

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

            then ( dom W) = ( the_Edges_of X) by RELAT_1: 62;

            then

            reconsider W as ManySortedSet of ( the_Edges_of X) by PARTFUN1:def 2;

            set GG = (X .set ( WeightSelector ,W));

            

             A2: GG == X by Lm3;

            then GG is Subgraph of X by GLIB_000: 87;

            then

            reconsider GG as Subgraph of G by GLIB_000: 43;

            

             A3: ( the_Vertices_of GG) = ( the_Vertices_of X) by A2

            .= V by A1, GLIB_000:def 37;

            ( the_Edges_of GG) = ( the_Edges_of X) by A2

            .= E by A1, GLIB_000:def 37;

            then

            reconsider GG as [Weighted] inducedSubgraph of G, V, E by A1, A3, GLIB_000:def 37;

            take GG;

            ( the_Weight_of GG) = W by GLIB_000: 8

            .= (( the_Weight_of G) | ( the_Edges_of GG)) by A2;

            hence GG is weight-inheriting;

          end;

            suppose

             A4: not (V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V));

            reconsider GG = G as Subgraph of G by GLIB_000: 40;

            reconsider GG as [Weighted] inducedSubgraph of G, V, E by A4, GLIB_000:def 37;

            take GG;

            thus GG is weight-inheriting;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be EGraph, V,E be set;

      cluster elabel-inheriting for [ELabeled] inducedSubgraph of G, V, E;

      existence

      proof

        now

          per cases ;

            suppose

             A1: V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V);

            set X = the [ELabeled] inducedSubgraph of G, V, E;

            set EL = (( the_ELabel_of G) | ( the_Edges_of X));

            reconsider EL9 = EL as PartFunc of ( dom EL), ( rng EL) by RELSET_1: 4;

            reconsider EL9 as PartFunc of ( the_Edges_of X), ( rng EL) by RELAT_1: 58, RELSET_1: 5;

            set GG = (X .set ( ELabelSelector ,EL9));

            

             A2: GG == X by Lm3;

            then GG is Subgraph of X by GLIB_000: 87;

            then

            reconsider GG as Subgraph of G by GLIB_000: 43;

            

             A3: ( the_Vertices_of GG) = ( the_Vertices_of X) by A2

            .= V by A1, GLIB_000:def 37;

            ( the_Edges_of GG) = ( the_Edges_of X) by A2

            .= E by A1, GLIB_000:def 37;

            then

            reconsider GG as [ELabeled] inducedSubgraph of G, V, E by A1, A3, GLIB_000:def 37;

            take GG;

            ( the_ELabel_of GG) = EL by GLIB_000: 8

            .= (( the_ELabel_of G) | ( the_Edges_of GG)) by A2;

            hence GG is elabel-inheriting;

          end;

            suppose

             A4: not (V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V));

            reconsider GG = G as Subgraph of G by GLIB_000: 40;

            reconsider GG as [ELabeled] inducedSubgraph of G, V, E by A4, GLIB_000:def 37;

            take GG;

            ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1;

            then ( the_ELabel_of G) = (( the_ELabel_of G) | ( the_Edges_of G)) by RELAT_1: 68;

            hence GG is elabel-inheriting;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be VGraph, V,E be set;

      cluster vlabel-inheriting for [VLabeled] inducedSubgraph of G, V, E;

      existence

      proof

        now

          per cases ;

            suppose

             A1: V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V);

            set X = the [VLabeled] inducedSubgraph of G, V, E;

            set VL = (( the_VLabel_of G) | ( the_Vertices_of X));

            reconsider VL9 = VL as PartFunc of ( dom VL), ( rng VL) by RELSET_1: 4;

            reconsider VL9 as PartFunc of ( the_Vertices_of X), ( rng VL) by RELAT_1: 58, RELSET_1: 5;

            set GG = (X .set ( VLabelSelector ,VL9));

            

             A2: GG == X by Lm3;

            then GG is Subgraph of X by GLIB_000: 87;

            then

            reconsider GG as Subgraph of G by GLIB_000: 43;

            

             A3: ( the_Vertices_of GG) = ( the_Vertices_of X) by A2

            .= V by A1, GLIB_000:def 37;

            ( the_Edges_of GG) = ( the_Edges_of X) by A2

            .= E by A1, GLIB_000:def 37;

            then

            reconsider GG as [VLabeled] inducedSubgraph of G, V, E by A1, A3, GLIB_000:def 37;

            take GG;

            ( the_VLabel_of GG) = VL by GLIB_000: 8

            .= (( the_VLabel_of G) | ( the_Vertices_of GG)) by A2;

            hence GG is vlabel-inheriting;

          end;

            suppose

             A4: not (V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V));

            reconsider GG = G as Subgraph of G by GLIB_000: 40;

            reconsider GG as [VLabeled] inducedSubgraph of G, V, E by A4, GLIB_000:def 37;

            take GG;

            ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2;

            then ( the_VLabel_of G) = (( the_VLabel_of G) | ( the_Vertices_of G)) by RELAT_1: 68;

            hence GG is vlabel-inheriting;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be WEGraph, V,E be set;

      cluster weight-inheriting elabel-inheriting for [Weighted] [ELabeled] inducedSubgraph of G, V, E;

      existence

      proof

        now

          per cases ;

            suppose

             A1: V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V);

            set X = the [Weighted] [ELabeled] inducedSubgraph of G, V, E;

            set W = (( the_Weight_of G) | ( the_Edges_of X));

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

            then ( dom W) = ( the_Edges_of X) by RELAT_1: 62;

            then

            reconsider W as ManySortedSet of ( the_Edges_of X) by PARTFUN1:def 2;

            set G1 = (X .set ( WeightSelector ,W));

            set EL = (( the_ELabel_of G) | ( the_Edges_of G1));

            reconsider EL9 = EL as PartFunc of ( dom EL), ( rng EL) by RELSET_1: 4;

            reconsider EL9 as PartFunc of ( the_Edges_of G1), ( rng EL) by RELAT_1: 58, RELSET_1: 5;

            set G2 = (G1 .set ( ELabelSelector ,EL9));

            

             A2: G2 == G1 by Lm3;

            X == G1 by Lm3;

            then

             A3: G2 == X by A2;

            then G2 is Subgraph of X by GLIB_000: 87;

            then

            reconsider G2 as Subgraph of G by GLIB_000: 43;

            

             A4: ( the_Vertices_of G2) = ( the_Vertices_of X) by A3

            .= V by A1, GLIB_000:def 37;

            ( the_Edges_of G2) = ( the_Edges_of X) by A3

            .= E by A1, GLIB_000:def 37;

            then

            reconsider G2 as [Weighted] [ELabeled] inducedSubgraph of G, V, E by A1, A4, GLIB_000:def 37;

            take G2;

            ( the_Weight_of G2) = (G1 . WeightSelector ) by GLIB_000: 9

            .= W by GLIB_000: 8

            .= (( the_Weight_of G) | ( the_Edges_of G2)) by A3;

            hence G2 is weight-inheriting;

            ( the_ELabel_of G2) = EL by GLIB_000: 8

            .= (( the_ELabel_of G) | ( the_Edges_of G2)) by A2;

            hence G2 is elabel-inheriting;

          end;

            suppose

             A5: not (V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V));

            reconsider GG = G as Subgraph of G by GLIB_000: 40;

            reconsider GG as [Weighted] [ELabeled] inducedSubgraph of G, V, E by A5, GLIB_000:def 37;

            take GG;

            thus GG is weight-inheriting;

            ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1;

            then ( the_ELabel_of G) = (( the_ELabel_of G) | ( the_Edges_of G)) by RELAT_1: 68;

            hence GG is elabel-inheriting;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be WVGraph, V,E be set;

      cluster weight-inheriting vlabel-inheriting for [Weighted] [VLabeled] inducedSubgraph of G, V, E;

      existence

      proof

        now

          per cases ;

            suppose

             A1: V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V);

            set X = the [Weighted] [VLabeled] inducedSubgraph of G, V, E;

            set W = (( the_Weight_of G) | ( the_Edges_of X));

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

            then ( dom W) = ( the_Edges_of X) by RELAT_1: 62;

            then

            reconsider W as ManySortedSet of ( the_Edges_of X) by PARTFUN1:def 2;

            set G1 = (X .set ( WeightSelector ,W));

            set VL = (( the_VLabel_of G) | ( the_Vertices_of G1));

            reconsider VL9 = VL as PartFunc of ( dom VL), ( rng VL) by RELSET_1: 4;

            reconsider VL9 as PartFunc of ( the_Vertices_of G1), ( rng VL) by RELAT_1: 58, RELSET_1: 5;

            set G2 = (G1 .set ( VLabelSelector ,VL9));

            

             A2: G2 == G1 by Lm3;

            X == G1 by Lm3;

            then

             A3: G2 == X by A2;

            then G2 is Subgraph of X by GLIB_000: 87;

            then

            reconsider G2 as Subgraph of G by GLIB_000: 43;

            

             A4: ( the_Vertices_of G2) = ( the_Vertices_of X) by A3

            .= V by A1, GLIB_000:def 37;

            ( the_Edges_of G2) = ( the_Edges_of X) by A3

            .= E by A1, GLIB_000:def 37;

            then

            reconsider G2 as [Weighted] [VLabeled] inducedSubgraph of G, V, E by A1, A4, GLIB_000:def 37;

            take G2;

            ( the_Weight_of G2) = (G1 . WeightSelector ) by GLIB_000: 9

            .= W by GLIB_000: 8

            .= (( the_Weight_of G) | ( the_Edges_of G2)) by A3;

            hence G2 is weight-inheriting;

            ( the_VLabel_of G2) = VL by GLIB_000: 8

            .= (( the_VLabel_of G) | ( the_Vertices_of G2)) by A2;

            hence G2 is vlabel-inheriting;

          end;

            suppose

             A5: not (V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V));

            reconsider GG = G as Subgraph of G by GLIB_000: 40;

            reconsider GG as [Weighted] [VLabeled] inducedSubgraph of G, V, E by A5, GLIB_000:def 37;

            take GG;

            thus GG is weight-inheriting;

            ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2;

            then ( the_VLabel_of G) = (( the_VLabel_of G) | ( the_Vertices_of G)) by RELAT_1: 68;

            hence GG is vlabel-inheriting;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be EVGraph, V,E be set;

      cluster elabel-inheriting vlabel-inheriting for [ELabeled] [VLabeled] inducedSubgraph of G, V, E;

      existence

      proof

        now

          per cases ;

            suppose

             A1: V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V);

            set X = the [ELabeled] [VLabeled] inducedSubgraph of G, V, E;

            set EL = (( the_ELabel_of G) | ( the_Edges_of X));

            reconsider EL9 = EL as PartFunc of ( dom EL), ( rng EL) by RELSET_1: 4;

            reconsider EL9 as PartFunc of ( the_Edges_of X), ( rng EL) by RELAT_1: 58, RELSET_1: 5;

            set G1 = (X .set ( ELabelSelector ,EL9));

            set VL = (( the_VLabel_of G) | ( the_Vertices_of G1));

            reconsider VL9 = VL as PartFunc of ( dom VL), ( rng VL) by RELSET_1: 4;

            reconsider VL9 as PartFunc of ( the_Vertices_of G1), ( rng VL) by RELAT_1: 58, RELSET_1: 5;

            set G2 = (G1 .set ( VLabelSelector ,VL9));

            

             A2: G2 == G1 by Lm3;

            X == G1 by Lm3;

            then

             A3: G2 == X by A2;

            then G2 is Subgraph of X by GLIB_000: 87;

            then

            reconsider G2 as Subgraph of G by GLIB_000: 43;

            

             A4: ( the_Vertices_of G2) = ( the_Vertices_of X) by A3

            .= V by A1, GLIB_000:def 37;

            ( the_Edges_of G2) = ( the_Edges_of X) by A3

            .= E by A1, GLIB_000:def 37;

            then

            reconsider G2 as [ELabeled] [VLabeled] inducedSubgraph of G, V, E by A1, A4, GLIB_000:def 37;

            take G2;

            ( the_ELabel_of G2) = (G1 . ELabelSelector ) by GLIB_000: 9

            .= EL9 by GLIB_000: 8

            .= (( the_ELabel_of G) | ( the_Edges_of G2)) by A3;

            hence G2 is elabel-inheriting;

            ( the_VLabel_of G2) = VL by GLIB_000: 8

            .= (( the_VLabel_of G) | ( the_Vertices_of G2)) by A2;

            hence G2 is vlabel-inheriting;

          end;

            suppose

             A5: not (V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V));

            reconsider GG = G as Subgraph of G by GLIB_000: 40;

            reconsider GG as [ELabeled] [VLabeled] inducedSubgraph of G, V, E by A5, GLIB_000:def 37;

            take GG;

            ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1;

            then ( the_ELabel_of G) = (( the_ELabel_of G) | ( the_Edges_of G)) by RELAT_1: 68;

            hence GG is elabel-inheriting;

            ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2;

            then ( the_VLabel_of G) = (( the_VLabel_of G) | ( the_Vertices_of G)) by RELAT_1: 68;

            hence GG is vlabel-inheriting;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be WEVGraph, V,E be set;

      cluster weight-inheriting elabel-inheriting vlabel-inheriting for [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G, V, E;

      existence

      proof

        now

          per cases ;

            suppose

             A1: V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V);

            set X = the [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G, V, E;

            set W = (( the_Weight_of G) | ( the_Edges_of X));

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

            then ( dom W) = ( the_Edges_of X) by RELAT_1: 62;

            then

            reconsider W as ManySortedSet of ( the_Edges_of X) by PARTFUN1:def 2;

            set G1 = (X .set ( WeightSelector ,W));

            set EL = (( the_ELabel_of G) | ( the_Edges_of G1));

            reconsider EL9 = EL as PartFunc of ( dom EL), ( rng EL) by RELSET_1: 4;

            reconsider EL9 as PartFunc of ( the_Edges_of G1), ( rng EL) by RELAT_1: 58, RELSET_1: 5;

            set G2 = (G1 .set ( ELabelSelector ,EL9));

            set VL = (( the_VLabel_of G) | ( the_Vertices_of G2));

            reconsider VL9 = VL as PartFunc of ( dom VL), ( rng VL) by RELSET_1: 4;

            reconsider VL9 as PartFunc of ( the_Vertices_of G2), ( rng VL) by RELAT_1: 58, RELSET_1: 5;

            set G3 = (G2 .set ( VLabelSelector ,VL9));

            

             A2: G2 == G1 by Lm3;

            

             A3: G3 == G2 by Lm3;

            X == G1 by Lm3;

            then G2 == X by A2;

            then

             A4: G3 == X by A3;

            then G3 is Subgraph of X by GLIB_000: 87;

            then

            reconsider G3 as Subgraph of G by GLIB_000: 43;

            

             A5: ( the_Vertices_of G3) = ( the_Vertices_of X) by A4

            .= V by A1, GLIB_000:def 37;

            ( the_Edges_of G3) = ( the_Edges_of X) by A4

            .= E by A1, GLIB_000:def 37;

            then

            reconsider G3 as [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G, V, E by A1, A5, GLIB_000:def 37;

            

             A6: G3 == G1 by A2, A3;

            take G3;

            ( the_Weight_of G3) = (G2 . WeightSelector ) by GLIB_000: 9

            .= (G1 . WeightSelector ) by GLIB_000: 9

            .= W by GLIB_000: 8

            .= (( the_Weight_of G) | ( the_Edges_of G3)) by A4;

            hence G3 is weight-inheriting;

            ( the_ELabel_of G3) = (G2 . ELabelSelector ) by GLIB_000: 9

            .= EL by GLIB_000: 8

            .= (( the_ELabel_of G) | ( the_Edges_of G3)) by A6;

            hence G3 is elabel-inheriting;

            ( the_VLabel_of G3) = VL by GLIB_000: 8

            .= (( the_VLabel_of G) | ( the_Vertices_of G3)) by A3;

            hence G3 is vlabel-inheriting;

          end;

            suppose

             A7: not (V is non empty Subset of ( the_Vertices_of G) & E c= (G .edgesBetween V));

            reconsider GG = G as Subgraph of G by GLIB_000: 40;

            reconsider GG as [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G, V, E by A7, GLIB_000:def 37;

            take GG;

            thus GG is weight-inheriting;

            ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1;

            then ( the_ELabel_of G) = (( the_ELabel_of G) | ( the_Edges_of G)) by RELAT_1: 68;

            hence GG is elabel-inheriting;

            ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2;

            then ( the_VLabel_of G) = (( the_VLabel_of G) | ( the_Vertices_of G)) by RELAT_1: 68;

            hence GG is vlabel-inheriting;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let G be WGraph, V,E be set;

      mode inducedWSubgraph of G,V,E is weight-inheriting [Weighted] inducedSubgraph of G, V, E;

    end

    definition

      let G be EGraph, V,E be set;

      mode inducedESubgraph of G,V,E is elabel-inheriting [ELabeled] inducedSubgraph of G, V, E;

    end

    definition

      let G be VGraph, V,E be set;

      mode inducedVSubgraph of G,V,E is vlabel-inheriting [VLabeled] inducedSubgraph of G, V, E;

    end

    definition

      let G be WEGraph, V,E be set;

      mode inducedWESubgraph of G,V,E is weight-inheriting elabel-inheriting [Weighted] [ELabeled] inducedSubgraph of G, V, E;

    end

    definition

      let G be WVGraph, V,E be set;

      mode inducedWVSubgraph of G,V,E is weight-inheriting vlabel-inheriting [Weighted] [VLabeled] inducedSubgraph of G, V, E;

    end

    definition

      let G be EVGraph, V,E be set;

      mode inducedEVSubgraph of G,V,E is elabel-inheriting vlabel-inheriting [ELabeled] [VLabeled] inducedSubgraph of G, V, E;

    end

    definition

      let G be WEVGraph, V,E be set;

      mode inducedWEVSubgraph of G,V,E is weight-inheriting elabel-inheriting vlabel-inheriting [Weighted] [ELabeled] [VLabeled] inducedSubgraph of G, V, E;

    end

    definition

      let G be WGraph, V be set;

      mode inducedWSubgraph of G,V is inducedWSubgraph of G, V, (G .edgesBetween V);

    end

    definition

      let G be EGraph, V be set;

      mode inducedESubgraph of G,V is inducedESubgraph of G, V, (G .edgesBetween V);

    end

    definition

      let G be VGraph, V be set;

      mode inducedVSubgraph of G,V is inducedVSubgraph of G, V, (G .edgesBetween V);

    end

    definition

      let G be WEGraph, V be set;

      mode inducedWESubgraph of G,V is inducedWESubgraph of G, V, (G .edgesBetween V);

    end

    definition

      let G be WVGraph, V be set;

      mode inducedWVSubgraph of G,V is inducedWVSubgraph of G, V, (G .edgesBetween V);

    end

    definition

      let G be EVGraph, V be set;

      mode inducedEVSubgraph of G,V is inducedEVSubgraph of G, V, (G .edgesBetween V);

    end

    definition

      let G be WEVGraph, V be set;

      mode inducedWEVSubgraph of G,V is inducedWEVSubgraph of G, V, (G .edgesBetween V);

    end

    definition

      let G be WGraph;

      :: GLIB_003:def13

      attr G is real-weighted means

      : Def13: ( the_Weight_of G) is real-valued;

    end

    definition

      let G be WGraph;

      :: GLIB_003:def14

      attr G is nonnegative-weighted means

      : Def14: ( rng ( the_Weight_of G)) c= Real>=0 ;

    end

    registration

      cluster nonnegative-weighted -> real-weighted for WGraph;

      coherence by XBOOLE_1: 1, VALUED_0:def 3;

    end

    definition

      let G be EGraph;

      :: GLIB_003:def15

      attr G is real-elabeled means

      : Def15: ( the_ELabel_of G) is real-valued;

    end

    definition

      let G be VGraph;

      :: GLIB_003:def16

      attr G is real-vlabeled means

      : Def16: ( the_VLabel_of G) is real-valued;

    end

    definition

      let G be WEVGraph;

      :: GLIB_003:def17

      attr G is real-WEV means G is real-weighted & G is real-elabeled & G is real-vlabeled;

    end

    registration

      cluster real-WEV -> real-weighted real-elabeled real-vlabeled for WEVGraph;

      coherence ;

      cluster real-weighted real-elabeled real-vlabeled -> real-WEV for WEVGraph;

      coherence ;

    end

    registration

      let G be _Graph, X be Function of ( the_Edges_of G), REAL ;

      cluster (G .set ( WeightSelector ,X)) -> real-weighted;

      coherence by GLIB_000: 8;

    end

    registration

      let G be _Graph, X be PartFunc of ( the_Edges_of G), REAL ;

      cluster (G .set ( ELabelSelector ,X)) -> real-elabeled;

      coherence by GLIB_000: 8;

    end

    registration

      let G be _Graph, X be real-valued ManySortedSet of ( the_Edges_of G);

      cluster (G .set ( ELabelSelector ,X)) -> real-elabeled;

      coherence by GLIB_000: 8;

    end

    registration

      let G be _Graph, X be PartFunc of ( the_Vertices_of G), REAL ;

      cluster (G .set ( VLabelSelector ,X)) -> real-vlabeled;

      coherence by GLIB_000: 8;

    end

    registration

      let G be _Graph, X be real-valued ManySortedSet of ( the_Vertices_of G);

      cluster (G .set ( VLabelSelector ,X)) -> real-vlabeled;

      coherence by GLIB_000: 8;

    end

    registration

      let G be _Graph;

      cluster (G .set ( ELabelSelector , {} )) -> real-elabeled;

      coherence

      proof

        reconsider X = {} as PartFunc of ( the_Edges_of G), REAL by RELSET_1: 12;

        (G .set ( ELabelSelector ,X)) is real-elabeled;

        hence thesis;

      end;

      cluster (G .set ( VLabelSelector , {} )) -> real-vlabeled;

      coherence

      proof

        reconsider X = {} as PartFunc of ( the_Vertices_of G), REAL by RELSET_1: 12;

        (G .set ( VLabelSelector ,X)) is real-vlabeled;

        hence thesis;

      end;

    end

    registration

      let G be _Graph, v be Vertex of G, val be Real;

      cluster (G .set ( VLabelSelector ,(v .--> val))) -> [VLabeled];

      coherence

      proof

        set X = (v .--> val);

        reconsider X = (v .--> val) as PartFunc of {v}, {val};

        ( dom (v .--> val)) = {v};

        then

        reconsider X as PartFunc of ( the_Vertices_of G), {val} by RELSET_1: 5;

        ( rng (v .--> val)) = {val} by FUNCOP_1: 8;

        then

        reconsider X as PartFunc of ( the_Vertices_of G), REAL by RELSET_1: 6;

        (G .set ( VLabelSelector ,X)) is real-vlabeled;

        hence thesis;

      end;

    end

    registration

      let G be _Graph, v be Vertex of G, val be Real;

      cluster (G .set ( VLabelSelector ,(v .--> val))) -> real-vlabeled;

      coherence

      proof

        set X = (v .--> val);

        reconsider X = (v .--> val) as PartFunc of {v}, {val};

        ( dom (v .--> val)) = {v};

        then

        reconsider X as PartFunc of ( the_Vertices_of G), {val} by RELSET_1: 5;

        for x be object st x in {val} holds x in REAL by XREAL_0:def 1;

        then {val} c= REAL by TARSKI:def 3;

        then

        reconsider X as PartFunc of ( the_Vertices_of G), REAL by RELSET_1: 7;

        (G .set ( VLabelSelector ,X)) is real-vlabeled;

        hence thesis;

      end;

    end

    registration

      cluster _finite _trivial Tree-like nonnegative-weighted real-WEV for WEVGraph;

      existence

      proof

        set E = {} ;

        set V = {1};

        reconsider S = {} as Function of E, V by RELSET_1: 12;

        set G1 = ( createGraph (V,E,S,S));

        set WL = the Function of ( the_Edges_of G1), REAL ;

        set G2 = (G1 .set ( WeightSelector ,WL));

        set EL = the PartFunc of ( the_Edges_of G2), REAL ;

        set G3 = (G2 .set ( ELabelSelector ,EL));

        set VL = the PartFunc of ( the_Vertices_of G3), REAL ;

        set G4 = (G3 .set ( VLabelSelector ,VL));

        take G4;

        thus G4 is _finite & G4 is _trivial & G4 is Tree-like;

        

         A1: ( the_Weight_of G4) = (G3 . WeightSelector ) by GLIB_000: 9

        .= (G2 . WeightSelector ) by GLIB_000: 9

        .= WL by GLIB_000: 8;

        ( the_Edges_of G1) = {} by GLIB_000: 6;

        then ( rng ( the_Weight_of G4)) = {} by A1;

        then ( rng ( the_Weight_of G4)) c= Real>=0 by XBOOLE_1: 2;

        hence G4 is nonnegative-weighted;

        ( the_ELabel_of G4) = (G3 . ELabelSelector ) by GLIB_000: 9

        .= EL by GLIB_000: 8;

        then

         A2: G4 is real-elabeled;

        G4 is real-weighted by A1;

        hence thesis by A2;

      end;

      cluster _finite non _trivial Tree-like nonnegative-weighted real-WEV for WEVGraph;

      existence

      proof

        set G1 = the _finite non _trivial Tree-like _Graph;

        set W = (( the_Edges_of G1) --> 0 );

        

         A3: ( dom W) = ( the_Edges_of G1);

        

         A4: ( rng W) c= { 0 } by FUNCOP_1: 13;

        then

        reconsider W as Function of ( the_Edges_of G1), REAL by A3, FUNCT_2: 2;

        set G2 = (G1 .set ( WeightSelector ,W));

        reconsider EL = {} as PartFunc of ( the_Edges_of G2), REAL by RELSET_1: 12;

        set G3 = (G2 .set ( ELabelSelector ,EL));

        reconsider VL = {} as PartFunc of ( the_Vertices_of G3), REAL by RELSET_1: 12;

        set G4 = (G3 .set ( VLabelSelector ,VL));

        take G4;

        thus G4 is _finite & G4 is non _trivial & G4 is Tree-like;

        

         A5: ( the_Weight_of G4) = (G3 . WeightSelector ) by GLIB_000: 9

        .= (G2 . WeightSelector ) by GLIB_000: 9

        .= W by GLIB_000: 8;

        for x be object st x in { 0 } holds x in Real>=0 by GRAPH_5:def 12;

        then { 0 } c= Real>=0 by TARSKI:def 3;

        then ( rng W) c= Real>=0 by A4, XBOOLE_1: 1;

        hence G4 is nonnegative-weighted by A5;

        ( the_ELabel_of G4) = (G3 . ELabelSelector ) by GLIB_000: 9

        .= EL by GLIB_000: 8;

        then

         A6: G4 is real-elabeled;

        G4 is real-weighted by A5;

        hence thesis by A6;

      end;

    end

    registration

      let G be _finite WGraph;

      cluster ( the_Weight_of G) -> finite;

      coherence

      proof

        

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

        then ( rng ( the_Weight_of G)) is finite by FINSET_1: 8;

        hence thesis by A1, ORDERS_1: 87;

      end;

    end

    registration

      let G be _finite EGraph;

      cluster ( the_ELabel_of G) -> finite;

      coherence

      proof

        

         A1: ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1;

        then ( rng ( the_ELabel_of G)) is finite by FINSET_1: 8;

        hence thesis by A1, ORDERS_1: 87;

      end;

    end

    registration

      let G be _finite VGraph;

      cluster ( the_VLabel_of G) -> finite;

      coherence

      proof

        

         A1: ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2;

        then ( rng ( the_VLabel_of G)) is finite by FINSET_1: 8;

        hence thesis by A1, ORDERS_1: 87;

      end;

    end

    registration

      let G be real-weighted WGraph;

      cluster ( the_Weight_of G) -> real-valued;

      coherence by Def13;

    end

    registration

      let G be real-elabeled EGraph;

      cluster ( the_ELabel_of G) -> real-valued;

      coherence by Def15;

    end

    registration

      let G be real-vlabeled VGraph;

      cluster ( the_VLabel_of G) -> real-valued;

      coherence by Def16;

    end

    registration

      let G be real-weighted WGraph, X be set;

      cluster (G .set ( ELabelSelector ,X)) -> real-weighted;

      coherence

      proof

        set G2 = (G .set ( ELabelSelector ,X));

        ( the_Weight_of G2) = ( the_Weight_of G) by GLIB_000: 9;

        hence thesis;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> real-weighted;

      coherence

      proof

        set G2 = (G .set ( VLabelSelector ,X));

        ( the_Weight_of G2) = ( the_Weight_of G) by GLIB_000: 9;

        hence thesis;

      end;

    end

    registration

      let G be nonnegative-weighted WGraph, X be set;

      cluster (G .set ( ELabelSelector ,X)) -> nonnegative-weighted;

      coherence

      proof

        set G2 = (G .set ( ELabelSelector ,X));

        ( the_Weight_of G2) = ( the_Weight_of G) & ( rng ( the_Weight_of G)) c= Real>=0 by Def14, GLIB_000: 9;

        hence thesis;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> nonnegative-weighted;

      coherence

      proof

        set G2 = (G .set ( VLabelSelector ,X));

        ( the_Weight_of G2) = ( the_Weight_of G) & ( rng ( the_Weight_of G)) c= Real>=0 by Def14, GLIB_000: 9;

        hence thesis;

      end;

    end

    registration

      let G be real-elabeled EGraph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> real-elabeled;

      coherence

      proof

        set G2 = (G .set ( WeightSelector ,X));

        ( the_ELabel_of G2) = ( the_ELabel_of G) by GLIB_000: 9;

        hence thesis;

      end;

      cluster (G .set ( VLabelSelector ,X)) -> real-elabeled;

      coherence

      proof

        set G2 = (G .set ( VLabelSelector ,X));

        ( the_ELabel_of G2) = ( the_ELabel_of G) by GLIB_000: 9;

        hence thesis;

      end;

    end

    registration

      let G be real-vlabeled VGraph, X be set;

      cluster (G .set ( WeightSelector ,X)) -> real-vlabeled;

      coherence

      proof

        set G2 = (G .set ( WeightSelector ,X));

        ( the_VLabel_of G2) = ( the_VLabel_of G) by GLIB_000: 9;

        hence thesis;

      end;

      cluster (G .set ( ELabelSelector ,X)) -> real-vlabeled;

      coherence

      proof

        set G2 = (G .set ( ELabelSelector ,X));

        ( the_VLabel_of G2) = ( the_VLabel_of G) by GLIB_000: 9;

        hence thesis;

      end;

    end

    definition

      let G be WGraph, W be Walk of G;

      :: GLIB_003:def18

      func W .weightSeq() -> FinSequence means

      : Def18: ( len it ) = ( len (W .edgeSeq() )) & for n be Nat st 1 <= n & n <= ( len it ) holds (it . n) = (( the_Weight_of G) . ((W .edgeSeq() ) . n));

      existence

      proof

        deffunc F( Nat) = (( the_Weight_of G) . ((W .edgeSeq() ) . $1));

        consider IT be FinSequence such that

         A1: ( len IT) = ( len (W .edgeSeq() )) & for k be Nat st k in ( dom IT) holds (IT . k) = F(k) from FINSEQ_1:sch 2;

        take IT;

        thus ( len IT) = ( len (W .edgeSeq() )) by A1;

        let n be Nat;

        assume 1 <= n & n <= ( len IT);

        then n in ( dom IT) by FINSEQ_3: 25;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let IT1,IT2 be FinSequence such that

         A2: ( len IT1) = ( len (W .edgeSeq() )) and

         A3: for n be Nat st 1 <= n & n <= ( len IT1) holds (IT1 . n) = (( the_Weight_of G) . ((W .edgeSeq() ) . n)) and

         A4: ( len IT2) = ( len (W .edgeSeq() )) and

         A5: for n be Nat st 1 <= n & n <= ( len IT2) holds (IT2 . n) = (( the_Weight_of G) . ((W .edgeSeq() ) . n));

        now

          let n be Nat;

          assume

           A6: 1 <= n & n <= ( len IT1);

          

          hence (IT1 . n) = (( the_Weight_of G) . ((W .edgeSeq() ) . n)) by A3

          .= (IT2 . n) by A2, A4, A5, A6;

        end;

        hence thesis by A2, A4, FINSEQ_1: 14;

      end;

    end

    definition

      let G be real-weighted WGraph, W be Walk of G;

      :: original: .weightSeq()

      redefine

      func W .weightSeq() -> FinSequence of REAL ;

      coherence

      proof

        now

          let y be object;

          assume y in ( rng (W .weightSeq() ));

          then

          consider x be Nat such that

           A1: x in ( dom (W .weightSeq() )) and

           A2: y = ((W .weightSeq() ) . x) by FINSEQ_2: 10;

          1 <= x & x <= ( len (W .weightSeq() )) by A1, FINSEQ_3: 25;

          then y = (( the_Weight_of G) . ((W .edgeSeq() ) . x)) by A2, Def18;

          hence y in REAL by XREAL_0:def 1;

        end;

        then ( rng (W .weightSeq() )) c= REAL by TARSKI:def 3;

        hence thesis by FINSEQ_1:def 4;

      end;

    end

    definition

      let G be real-weighted WGraph, W be Walk of G;

      :: GLIB_003:def19

      func W .cost() -> Real equals ( Sum (W .weightSeq() ));

      coherence ;

    end

    

     Lm4: for x,y,X,Y be set, f be PartFunc of X, Y st x in X & y in Y holds (f +* (x .--> y)) is PartFunc of X, Y

    proof

      let x,y,X,Y be set, f be PartFunc of X, Y;

      assume that

       A1: x in X and

       A2: y in Y;

      set F = (f +* (x .--> y));

      

       A3: ( rng F) c= (( rng f) \/ ( rng (x .--> y))) by FUNCT_4: 17;

      now

        let z be object;

        assume

         A4: z in ( rng F);

        now

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

            suppose z in ( rng f);

            hence z in Y;

          end;

            suppose z in ( rng (x .--> y));

            then z in {y} by FUNCOP_1: 8;

            hence z in Y by A2, TARSKI:def 1;

          end;

        end;

        hence z in Y;

      end;

      then ( rng F) c= Y by TARSKI:def 3;

      then

      reconsider F1 = F as PartFunc of ( dom F), Y by RELSET_1: 4;

      now

        let z be object;

        assume z in ( dom F1);

        then

         A5: z in (( dom f) \/ ( dom (x .--> y))) by FUNCT_4:def 1;

        now

          per cases by A5, XBOOLE_0:def 3;

            suppose z in ( dom f);

            hence z in X;

          end;

            suppose z in ( dom (x .--> y));

            then z in {x};

            hence z in X by A1, TARSKI:def 1;

          end;

        end;

        hence z in X;

      end;

      then ( dom F1) c= X by TARSKI:def 3;

      hence thesis by RELSET_1: 7;

    end;

    definition

      let G be EGraph;

      :: GLIB_003:def20

      func G .labeledE() -> Subset of ( the_Edges_of G) equals ( dom ( the_ELabel_of G));

      coherence by Lm1;

    end

    definition

      let G be EGraph, e,x be object;

      :: GLIB_003:def21

      func G .labelEdge (e,x) -> EGraph equals

      : Def21: (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) if e in ( the_Edges_of G)

      otherwise G;

      coherence

      proof

        set EL = (( the_ELabel_of G) +* (e .--> x)), G2 = (G .set ( ELabelSelector ,EL));

        G == G2 by Lm3;

        then

         A1: ( the_Edges_of G) = ( the_Edges_of G2);

        hereby

          

           A2: ( dom EL) = (( dom ( the_ELabel_of G)) \/ ( dom (e .--> x))) by FUNCT_4:def 1

          .= (( dom ( the_ELabel_of G)) \/ {e});

          assume

           A3: e in ( the_Edges_of G);

          now

            let z be object;

            assume

             A4: z in ( dom EL);

            now

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

                suppose

                 A5: z in ( dom ( the_ELabel_of G));

                ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1;

                hence z in ( the_Edges_of G) by A5;

              end;

                suppose z in {e};

                hence z in ( the_Edges_of G) by A3, TARSKI:def 1;

              end;

            end;

            hence z in ( the_Edges_of G);

          end;

          then

           A6: ( dom EL) c= ( the_Edges_of G2) by A1, TARSKI:def 3;

          

           A7: (G2 . ELabelSelector ) = EL by GLIB_000: 8;

           ELabelSelector in ( dom G) & ( dom G) c= ( dom G2) by Def5, FUNCT_4: 10;

          hence G2 is EGraph by A6, A7, Def5;

        end;

        thus thesis;

      end;

      consistency ;

    end

    registration

      let G be _finite EGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> _finite;

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be loopless EGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> loopless;

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be _trivial EGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> _trivial;

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be non _trivial EGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> non _trivial;

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be non-multi EGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> non-multi;

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be non-Dmulti EGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> non-Dmulti;

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be connected EGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> connected;

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be acyclic EGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> acyclic;

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be WEGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> [Weighted];

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be EVGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> [VLabeled];

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be real-weighted WEGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> real-weighted;

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be nonnegative-weighted WEGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> nonnegative-weighted;

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be real-elabeled EGraph, e be set, x be Real;

      cluster (G .labelEdge (e,x)) -> real-elabeled;

      coherence

      proof

        now

          per cases ;

            suppose

             A1: e in ( the_Edges_of G);

            reconsider x as Element of REAL by XREAL_0:def 1;

            set EL = (( the_ELabel_of G) +* (e .--> x));

            ( rng ( the_ELabel_of G)) c= REAL ;

            then ( the_ELabel_of G) is PartFunc of ( dom ( the_ELabel_of G)), REAL by RELSET_1: 4;

            then ( the_ELabel_of G) is PartFunc of ( the_Edges_of G), REAL by Lm1, RELSET_1: 5;

            then

            reconsider EL as PartFunc of ( the_Edges_of G), REAL by A1, Lm4;

            (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,EL)) by A1, Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be real-vlabeled EVGraph, e,x be set;

      cluster (G .labelEdge (e,x)) -> real-vlabeled;

      coherence

      proof

        now

          per cases ;

            suppose e in ( the_Edges_of G);

            then (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

            hence thesis;

          end;

            suppose not e in ( the_Edges_of G);

            hence thesis by Def21;

          end;

        end;

        hence thesis;

      end;

    end

    definition

      let G be VGraph, v,x be object;

      :: GLIB_003:def22

      func G .labelVertex (v,x) -> VGraph equals

      : Def22: (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) if v in ( the_Vertices_of G)

      otherwise G;

      coherence

      proof

        set VL = (( the_VLabel_of G) +* (v .--> x)), G2 = (G .set ( VLabelSelector ,VL));

        hereby

          

           A1: ( dom VL) = (( dom ( the_VLabel_of G)) \/ ( dom (v .--> x))) by FUNCT_4:def 1;

          assume

           A2: v in ( the_Vertices_of G);

          now

            let y be object;

            assume

             A3: y in ( dom VL);

            now

              per cases by A1, A3, XBOOLE_0:def 3;

                suppose

                 A4: y in ( dom ( the_VLabel_of G));

                ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2;

                hence y in ( the_Vertices_of G) by A4;

              end;

                suppose y in ( dom (v .--> x));

                then y in {v};

                hence y in ( the_Vertices_of G) by A2, TARSKI:def 1;

              end;

            end;

            hence y in ( the_Vertices_of G);

          end;

          then ( dom VL) c= ( the_Vertices_of G) by TARSKI:def 3;

          then

          reconsider V1 = VL as PartFunc of ( the_Vertices_of G), ( rng VL) by RELSET_1: 4;

          G2 = (G .set ( VLabelSelector ,V1));

          hence G2 is VGraph;

        end;

        thus thesis;

      end;

      consistency ;

    end

    definition

      let G be VGraph;

      :: GLIB_003:def23

      func G .labeledV() -> Subset of ( the_Vertices_of G) equals ( dom ( the_VLabel_of G));

      coherence by Lm2;

    end

    registration

      let G be _finite VGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> _finite;

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be loopless VGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> loopless;

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be _trivial VGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> _trivial;

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be non _trivial VGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> non _trivial;

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be non-multi VGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> non-multi;

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be non-Dmulti VGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> non-Dmulti;

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be connected VGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> connected;

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be acyclic VGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> acyclic;

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be WVGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> [Weighted];

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be EVGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> [ELabeled];

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be real-weighted WVGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> real-weighted;

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be nonnegative-weighted WVGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> nonnegative-weighted;

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be real-elabeled EVGraph, v,x be set;

      cluster (G .labelVertex (v,x)) -> real-elabeled;

      coherence

      proof

        now

          per cases ;

            suppose v in ( the_Vertices_of G);

            then (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (v .--> x)))) by Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be real-vlabeled VGraph, v be set, x be Real;

      cluster (G .labelVertex (v,x)) -> real-vlabeled;

      coherence

      proof

        now

          per cases ;

            suppose

             A1: v in ( the_Vertices_of G);

            reconsider x as Element of REAL by XREAL_0:def 1;

            set EL = (( the_VLabel_of G) +* (v .--> x));

            ( rng ( the_VLabel_of G)) c= REAL ;

            then ( the_VLabel_of G) is PartFunc of ( dom ( the_VLabel_of G)), REAL by RELSET_1: 4;

            then ( the_VLabel_of G) is PartFunc of ( the_Vertices_of G), REAL by Lm2, RELSET_1: 5;

            then

            reconsider EL as PartFunc of ( the_Vertices_of G), REAL by A1, Lm4;

            (G .labelVertex (v,x)) = (G .set ( VLabelSelector ,EL)) by A1, Def22;

            hence thesis;

          end;

            suppose not v in ( the_Vertices_of G);

            hence thesis by Def22;

          end;

        end;

        hence thesis;

      end;

    end

    registration

      let G be real-weighted WGraph;

      cluster -> real-weighted for WSubgraph of G;

      coherence

      proof

        let G2 be WSubgraph of G;

        set W2 = (( the_Weight_of G) | ( the_Edges_of G2));

        ( the_Weight_of G2) = W2 by Def10;

        hence thesis;

      end;

    end

    registration

      let G be nonnegative-weighted WGraph;

      cluster -> nonnegative-weighted for WSubgraph of G;

      coherence

      proof

        let G2 be WSubgraph of G;

        now

          let x be object;

          

           A1: ( rng ( the_Weight_of G)) c= Real>=0 by Def14;

          assume x in ( rng ( the_Weight_of G2));

          then

           A2: x in ( rng (( the_Weight_of G) | ( the_Edges_of G2))) by Def10;

          ( rng (( the_Weight_of G) | ( the_Edges_of G2))) c= ( rng ( the_Weight_of G)) by RELAT_1: 70;

          then x in ( rng ( the_Weight_of G)) by A2;

          hence x in Real>=0 by A1;

        end;

        hence ( rng ( the_Weight_of G2)) c= Real>=0 by TARSKI:def 3;

      end;

    end

    registration

      let G be real-elabeled EGraph;

      cluster -> real-elabeled for ESubgraph of G;

      coherence

      proof

        let G2 be ESubgraph of G;

        ( the_ELabel_of G2) = (( the_ELabel_of G) | ( the_Edges_of G2)) by Def11;

        hence thesis;

      end;

    end

    registration

      let G be real-vlabeled VGraph;

      cluster -> real-vlabeled for VSubgraph of G;

      coherence

      proof

        let G2 be VSubgraph of G;

        ( the_VLabel_of G2) = (( the_VLabel_of G) | ( the_Vertices_of G2)) by Def12;

        hence thesis;

      end;

    end

    definition

      let GSq be GraphSeq;

      :: GLIB_003:def24

      attr GSq is [Weighted] means

      : Def24: for x be Nat holds (GSq . x) is [Weighted];

      :: GLIB_003:def25

      attr GSq is [ELabeled] means

      : Def25: for x be Nat holds (GSq . x) is [ELabeled];

      :: GLIB_003:def26

      attr GSq is [VLabeled] means

      : Def26: for x be Nat holds (GSq . x) is [VLabeled];

    end

    registration

      cluster [Weighted] [ELabeled] [VLabeled] for GraphSeq;

      existence

      proof

        set G = the _finite loopless _trivial non-multi simple real-WEV nonnegative-weighted WEVGraph;

        set F = ( NAT --> G);

        

         A1: ( dom F) = NAT ;

        reconsider F as ManySortedSet of NAT ;

        reconsider F as GraphSeq;

        take F;

        now

          let x be Nat;

          x in NAT by ORDINAL1:def 12;

          then (F . x) in ( rng F) by A1, FUNCT_1: 3;

          then (F . x) in {G} by FUNCOP_1: 8;

          hence (F . x) is [Weighted] & (F . x) is [ELabeled] & (F . x) is [VLabeled] by TARSKI:def 1;

        end;

        hence thesis;

      end;

    end

    definition

      mode WGraphSeq is [Weighted] GraphSeq;

      mode EGraphSeq is [ELabeled] GraphSeq;

      mode VGraphSeq is [VLabeled] GraphSeq;

      mode WEGraphSeq is [Weighted] [ELabeled] GraphSeq;

      mode WVGraphSeq is [Weighted] [VLabeled] GraphSeq;

      mode EVGraphSeq is [ELabeled] [VLabeled] GraphSeq;

      mode WEVGraphSeq is [Weighted] [ELabeled] [VLabeled] GraphSeq;

    end

    registration

      let GSq be WGraphSeq, x be Nat;

      cluster (GSq . x) -> [Weighted];

      coherence by Def24;

    end

    registration

      let GSq be EGraphSeq, x be Nat;

      cluster (GSq . x) -> [ELabeled];

      coherence by Def25;

    end

    registration

      let GSq be VGraphSeq, x be Nat;

      cluster (GSq . x) -> [VLabeled];

      coherence by Def26;

    end

    definition

      let GSq be WGraphSeq;

      :: GLIB_003:def27

      attr GSq is real-weighted means

      : Def27: for x be Nat holds (GSq . x) is real-weighted;

      :: GLIB_003:def28

      attr GSq is nonnegative-weighted means

      : Def28: for x be Nat holds (GSq . x) is nonnegative-weighted;

    end

    definition

      let GSq be EGraphSeq;

      :: GLIB_003:def29

      attr GSq is real-elabeled means

      : Def29: for x be Nat holds (GSq . x) is real-elabeled;

    end

    definition

      let GSq be VGraphSeq;

      :: GLIB_003:def30

      attr GSq is real-vlabeled means

      : Def30: for x be Nat holds (GSq . x) is real-vlabeled;

    end

    definition

      let GSq be WEVGraphSeq;

      :: GLIB_003:def31

      attr GSq is real-WEV means for x be Nat holds (GSq . x) is real-WEV;

    end

    registration

      cluster real-WEV -> real-weighted real-elabeled real-vlabeled for WEVGraphSeq;

      coherence

      proof

        let GSq be [Weighted] [ELabeled] [VLabeled] GraphSeq;

        assume

         A1: for x be Nat holds (GSq . x) is real-WEV;

        now

          let x be Nat;

          reconsider G = (GSq . x) as real-WEV WEVGraph by A1;

          G is real-WEV;

          hence (GSq . x) is real-weighted;

        end;

        hence GSq is real-weighted;

        now

          let x be Nat;

          reconsider G = (GSq . x) as real-WEV WEVGraph by A1;

          G is real-WEV;

          hence (GSq . x) is real-elabeled;

        end;

        hence GSq is real-elabeled;

        now

          let x be Nat;

          reconsider G = (GSq . x) as real-WEV WEVGraph by A1;

          G is real-WEV;

          hence (GSq . x) is real-vlabeled;

        end;

        hence thesis;

      end;

      cluster real-weighted real-elabeled real-vlabeled -> real-WEV for WEVGraphSeq;

      coherence

      proof

        let GSq be [Weighted] [ELabeled] [VLabeled] GraphSeq;

        assume

         A2: GSq is real-weighted & GSq is real-elabeled & GSq is real-vlabeled;

        let x be Nat;

        reconsider G = (GSq . x) as real-weighted real-elabeled real-vlabeled WEVGraph by A2;

        G is real-WEV;

        hence thesis;

      end;

    end

    registration

      cluster halting _finite loopless _trivial non-multi simple real-WEV nonnegative-weighted Tree-like for WEVGraphSeq;

      existence

      proof

        set G = the _finite loopless _trivial non-multi simple real-WEV acyclic connected Tree-like nonnegative-weighted WEVGraph;

        set F = ( NAT --> G);

        

         A1: ( dom F) = NAT ;

        reconsider F as ManySortedSet of NAT ;

        reconsider F as GraphSeq;

        now

          let x be Nat;

          x in NAT by ORDINAL1:def 12;

          then (F . x) in ( rng F) by A1, FUNCT_1: 3;

          then (F . x) in {G} by FUNCOP_1: 8;

          hence (F . x) is [Weighted] & (F . x) is [ELabeled] & (F . x) is [VLabeled] by TARSKI:def 1;

        end;

        then

        reconsider F as [Weighted] [ELabeled] [VLabeled] GraphSeq by Def24, Def25, Def26;

        

         A2: (F . (1 + 1)) = G;

        take F;

        (F . 1) = G;

        hence F is halting by A2;

        now

          let x be Nat;

          x in NAT by ORDINAL1:def 12;

          then (F . x) in ( rng F) by A1, FUNCT_1: 3;

          then (F . x) in {G} by FUNCOP_1: 8;

          hence (F . x) is _finite & (F . x) is loopless & (F . x) is _trivial & (F . x) is non-multi & (F . x) is simple & (F . x) is real-WEV & (F . x) is nonnegative-weighted & (F . x) is Tree-like by TARSKI:def 1;

        end;

        hence thesis by GLIB_002:def 20;

      end;

    end

    registration

      let GSq be real-weighted WGraphSeq, x be Nat;

      cluster (GSq . x) -> real-weighted;

      coherence by Def27;

    end

    registration

      let GSq be nonnegative-weighted WGraphSeq, x be Nat;

      cluster (GSq . x) -> nonnegative-weighted;

      coherence by Def28;

    end

    registration

      let GSq be real-elabeled EGraphSeq, x be Nat;

      cluster (GSq . x) -> real-elabeled;

      coherence by Def29;

    end

    registration

      let GSq be real-vlabeled VGraphSeq, x be Nat;

      cluster (GSq . x) -> real-vlabeled;

      coherence by Def30;

    end

    begin

    theorem :: GLIB_003:3

     WeightSelector = 5 & ELabelSelector = 6 & VLabelSelector = 7;

    theorem :: GLIB_003:4

    (for G be WGraph holds ( the_Weight_of G) = (G . WeightSelector )) & (for G be EGraph holds ( the_ELabel_of G) = (G . ELabelSelector )) & for G be VGraph holds ( the_VLabel_of G) = (G . VLabelSelector );

    theorem :: GLIB_003:5

    for G be EGraph holds ( dom ( the_ELabel_of G)) c= ( the_Edges_of G) by Lm1;

    theorem :: GLIB_003:6

    for G be VGraph holds ( dom ( the_VLabel_of G)) c= ( the_Vertices_of G) by Lm2;

    theorem :: GLIB_003:7

    for G be _Graph, X be set holds G == (G .set ( WeightSelector ,X)) & G == (G .set ( ELabelSelector ,X)) & G == (G .set ( VLabelSelector ,X)) by Lm3;

    theorem :: GLIB_003:8

    for G1,G2 be WGraph, G3 be WGraph st G1 == G2 & ( the_Weight_of G1) = ( the_Weight_of G2) & G1 is WSubgraph of G3 holds G2 is WSubgraph of G3

    proof

      let G1,G2 be WGraph, G3 be WGraph;

      assume that

       A1: G1 == G2 and

       A2: ( the_Weight_of G1) = ( the_Weight_of G2) and

       A3: G1 is WSubgraph of G3;

      reconsider G29 = G2 as [Weighted] Subgraph of G3 by A1, A3, GLIB_000: 92;

      ( the_Edges_of G1) = ( the_Edges_of G2) by A1;

      then ( the_Weight_of G2) = (( the_Weight_of G3) | ( the_Edges_of G2)) by A2, A3, Def10;

      then G29 is weight-inheriting;

      hence thesis;

    end;

    theorem :: GLIB_003:9

    for G1 be WGraph, G2 be WSubgraph of G1, G3 be WSubgraph of G2 holds G3 is WSubgraph of G1

    proof

      let G1 be WGraph, G2 be WSubgraph of G1, G3 be WSubgraph of G2;

      reconsider G39 = G3 as [Weighted] Subgraph of G1 by GLIB_000: 43;

      ( the_Weight_of G3) = (( the_Weight_of G2) | ( the_Edges_of G3)) by Def10

      .= ((( the_Weight_of G1) | ( the_Edges_of G2)) | ( the_Edges_of G3)) by Def10

      .= (( the_Weight_of G1) | ( the_Edges_of G3)) by RELAT_1: 74;

      then G39 is weight-inheriting;

      hence thesis;

    end;

    theorem :: GLIB_003:10

    for G1,G2 be WGraph, G3 be WSubgraph of G1 st G1 == G2 & ( the_Weight_of G1) = ( the_Weight_of G2) holds G3 is WSubgraph of G2

    proof

      let G1,G2 be WGraph, G3 be WSubgraph of G1;

      assume that

       A1: G1 == G2 and

       A2: ( the_Weight_of G1) = ( the_Weight_of G2);

      reconsider G39 = G3 as [Weighted] Subgraph of G2 by A1, GLIB_000: 91;

      ( the_Weight_of G3) = (( the_Weight_of G2) | ( the_Edges_of G3)) by A2, Def10;

      then G39 is WSubgraph of G2 by Def10;

      hence thesis;

    end;

    theorem :: GLIB_003:11

    for G1 be WGraph, G2 be WSubgraph of G1 holds for x be set st x in ( the_Edges_of G2) holds (( the_Weight_of G2) . x) = (( the_Weight_of G1) . x)

    proof

      let G1 be WGraph, G2 be WSubgraph of G1;

      let x be set;

      assume x in ( the_Edges_of G2);

      then

       A1: x in ( dom ( the_Weight_of G2)) by PARTFUN1:def 2;

      ( the_Weight_of G2) = (( the_Weight_of G1) | ( the_Edges_of G2)) by Def10;

      hence thesis by A1, FUNCT_1: 47;

    end;

    theorem :: GLIB_003:12

    

     Th12: for G be WGraph, W be Walk of G holds W is trivial implies (W .weightSeq() ) = {}

    proof

      let G be WGraph, W be Walk of G;

      assume W is trivial;

      then (W .length() ) = 0 by GLIB_001:def 26;

      then ( len (W .edgeSeq() )) = 0 by GLIB_001:def 18;

      then ( len (W .weightSeq() )) = 0 by Def18;

      hence thesis;

    end;

    theorem :: GLIB_003:13

    for G be WGraph, W be Walk of G holds ( len (W .weightSeq() )) = (W .length() )

    proof

      let G be WGraph, W be Walk of G;

      

      thus ( len (W .weightSeq() )) = ( len (W .edgeSeq() )) by Def18

      .= (W .length() ) by GLIB_001:def 18;

    end;

    theorem :: GLIB_003:14

    

     Th14: for G be WGraph, x,y,e be set st e Joins (x,y,G) holds ((G .walkOf (x,e,y)) .weightSeq() ) = <*(( the_Weight_of G) . e)*>

    proof

      let G be WGraph, x,y,e be set;

      set W = (G .walkOf (x,e,y));

      assume e Joins (x,y,G);

      then

       A1: (W .edgeSeq() ) = <*e*> by GLIB_001: 83;

      then ( len (W .edgeSeq() )) = 1 by FINSEQ_1: 39;

      then

       A2: ( len (W .weightSeq() )) = 1 by Def18;

       A3:

      now

        let n be Nat;

        assume that

         A4: 1 <= n and

         A5: n <= ( len (W .weightSeq() ));

        

         A6: n = 1 by A2, A4, A5, XXREAL_0: 1;

        

        hence ((W .weightSeq() ) . n) = (( the_Weight_of G) . ( <*e*> . 1)) by A1, A5, Def18

        .= (( the_Weight_of G) . e) by FINSEQ_1: 40

        .= ( <*(( the_Weight_of G) . e)*> . n) by A6, FINSEQ_1: 40;

      end;

      ( len (W .weightSeq() )) = ( len <*(( the_Weight_of G) . e)*>) by A2, FINSEQ_1: 39;

      hence thesis by A3, FINSEQ_1: 14;

    end;

    theorem :: GLIB_003:15

    

     Th15: for G be WGraph, W be Walk of G holds ((W .reverse() ) .weightSeq() ) = ( Rev (W .weightSeq() ))

    proof

      let G be WGraph, W be Walk of G;

      set W1 = ((W .reverse() ) .weightSeq() ), W2 = ( Rev (W .weightSeq() ));

      ( len (W .reverse() )) = ( len W) by GLIB_001: 21;

      then ((W .reverse() ) .length() ) = (W .length() ) by GLIB_001: 113;

      

      then ( len ((W .reverse() ) .edgeSeq() )) = (W .length() ) by GLIB_001:def 18

      .= ( len (W .edgeSeq() )) by GLIB_001:def 18;

      then

       A1: ( len W1) = ( len (W .edgeSeq() )) by Def18;

      

       A2: ( len (W .weightSeq() )) = ( len (W .edgeSeq() )) by Def18;

       A3:

      now

        let n be Nat;

        assume that

         A4: 1 <= n and

         A5: n <= ( len W1);

        

         A6: n in ( dom (W .edgeSeq() )) by A1, A4, A5, FINSEQ_3: 25;

        set rn = ((( len (W .weightSeq() )) - n) + 1);

        reconsider rn as Element of NAT by A1, A2, A5, FINSEQ_5: 1;

        n in ( Seg ( len (W .weightSeq() ))) by A1, A2, A4, A5, FINSEQ_1: 1;

        then rn in ( Seg ( len (W .weightSeq() ))) by FINSEQ_5: 2;

        then

         A7: 1 <= rn & rn <= ( len (W .weightSeq() )) by FINSEQ_1: 1;

        (W1 . n) = (( the_Weight_of G) . (((W .reverse() ) .edgeSeq() ) . n)) by A4, A5, Def18

        .= (( the_Weight_of G) . (( Rev (W .edgeSeq() )) . n)) by GLIB_001: 84;

        then

         A8: (W1 . n) = (( the_Weight_of G) . ((W .edgeSeq() ) . ((( len (W .edgeSeq() )) - n) + 1))) by A6, FINSEQ_5: 58;

        n in ( dom (W .weightSeq() )) by A1, A2, A4, A5, FINSEQ_3: 25;

        

        then (W2 . n) = ((W .weightSeq() ) . rn) by FINSEQ_5: 58

        .= (( the_Weight_of G) . ((W .edgeSeq() ) . rn)) by A7, Def18;

        hence (W1 . n) = (W2 . n) by A8, Def18;

      end;

      ( len W1) = ( len W2) by A1, A2, FINSEQ_5:def 3;

      hence thesis by A3, FINSEQ_1: 14;

    end;

    theorem :: GLIB_003:16

    

     Th16: for G be WGraph, W1,W2 be Walk of G st (W1 .last() ) = (W2 .first() ) holds ((W1 .append W2) .weightSeq() ) = ((W1 .weightSeq() ) ^ (W2 .weightSeq() ))

    proof

      let G be WGraph, W1,W2 be Walk of G;

      set W3 = (W1 .append W2), W4 = ((W1 .weightSeq() ) ^ (W2 .weightSeq() ));

      assume

       A1: (W1 .last() ) = (W2 .first() );

      then (W3 .edgeSeq() ) = ((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) by GLIB_001: 85;

      then ( len (W3 .edgeSeq() )) = (( len (W1 .edgeSeq() )) + ( len (W2 .edgeSeq() ))) by FINSEQ_1: 22;

      

      then

       A2: ( len (W3 .weightSeq() )) = (( len (W1 .edgeSeq() )) + ( len (W2 .edgeSeq() ))) by Def18

      .= (( len (W1 .weightSeq() )) + ( len (W2 .edgeSeq() ))) by Def18

      .= (( len (W1 .weightSeq() )) + ( len (W2 .weightSeq() ))) by Def18

      .= ( len W4) by FINSEQ_1: 22;

      now

        let n be Nat;

        assume

         A3: 1 <= n & n <= ( len (W3 .weightSeq() ));

        

        then

         A4: ((W3 .weightSeq() ) . n) = (( the_Weight_of G) . ((W3 .edgeSeq() ) . n)) by Def18

        .= (( the_Weight_of G) . (((W1 .edgeSeq() ) ^ (W2 .edgeSeq() )) . n)) by A1, GLIB_001: 85;

        

         A5: n in ( dom W4) by A2, A3, FINSEQ_3: 25;

        now

          per cases by A5, FINSEQ_1: 25;

            suppose

             A6: n in ( dom (W1 .weightSeq() ));

            then

             A7: 1 <= n by FINSEQ_3: 25;

            

             A8: n <= ( len (W1 .weightSeq() )) by A6, FINSEQ_3: 25;

            then n <= ( len (W1 .edgeSeq() )) by Def18;

            then

             A9: n in ( dom (W1 .edgeSeq() )) by A7, FINSEQ_3: 25;

            (W4 . n) = ((W1 .weightSeq() ) . n) by A6, FINSEQ_1:def 7

            .= (( the_Weight_of G) . ((W1 .edgeSeq() ) . n)) by A7, A8, Def18;

            hence ((W3 .weightSeq() ) . n) = (W4 . n) by A4, A9, FINSEQ_1:def 7;

          end;

            suppose ex k be Nat st k in ( dom (W2 .weightSeq() )) & n = (( len (W1 .weightSeq() )) + k);

            then

            consider k be Nat such that

             A10: k in ( dom (W2 .weightSeq() )) and

             A11: n = (( len (W1 .weightSeq() )) + k);

            

             A12: 1 <= k by A10, FINSEQ_3: 25;

            

             A13: k <= ( len (W2 .weightSeq() )) by A10, FINSEQ_3: 25;

            then k <= ( len (W2 .edgeSeq() )) by Def18;

            then

             A14: k in ( dom (W2 .edgeSeq() )) by A12, FINSEQ_3: 25;

            

             A15: n = (( len (W1 .edgeSeq() )) + k) by A11, Def18;

            (W4 . n) = ((W2 .weightSeq() ) . k) by A10, A11, FINSEQ_1:def 7

            .= (( the_Weight_of G) . ((W2 .edgeSeq() ) . k)) by A12, A13, Def18;

            hence ((W3 .weightSeq() ) . n) = (W4 . n) by A4, A14, A15, FINSEQ_1:def 7;

          end;

        end;

        hence ((W3 .weightSeq() ) . n) = (W4 . n);

      end;

      hence thesis by A2, FINSEQ_1: 14;

    end;

    theorem :: GLIB_003:17

    

     Th17: for G be WGraph, W be Walk of G, e be set st e in ((W .last() ) .edgesInOut() ) holds ((W .addEdge e) .weightSeq() ) = ((W .weightSeq() ) ^ <*(( the_Weight_of G) . e)*>)

    proof

      let G be WGraph, W be Walk of G, e be set;

      set W2 = (W .addEdge e), WA = (G .walkOf ((W .last() ),e,((W .last() ) .adj e)));

      assume e in ((W .last() ) .edgesInOut() );

      then

       A1: e Joins ((W .last() ),((W .last() ) .adj e),G) by GLIB_000: 67;

      then W2 = (W .append WA) & (W .last() ) = (WA .first() ) by GLIB_001: 15, GLIB_001:def 13;

      

      hence (W2 .weightSeq() ) = ((W .weightSeq() ) ^ (WA .weightSeq() )) by Th16

      .= ((W .weightSeq() ) ^ <*(( the_Weight_of G) . e)*>) by A1, Th14;

    end;

    theorem :: GLIB_003:18

    

     Th18: for G be real-weighted WGraph, W1 be Walk of G, W2 be Subwalk of W1 holds ex ws be Subset of (W1 .weightSeq() ) st (W2 .weightSeq() ) = ( Seq ws)

    proof

      let G be real-weighted WGraph, W1 be Walk of G, W2 be Subwalk of W1;

      consider es be Subset of (W1 .edgeSeq() ) such that

       A1: (W2 .edgeSeq() ) = ( Seq es) by GLIB_001:def 32;

      deffunc F( object) = (( the_Weight_of G) . (es . $1));

      consider ws be Function such that

       A2: ( dom ws) = ( dom es) & for x be object st x in ( dom es) holds (ws . x) = F(x) from FUNCT_1:sch 3;

      

       A3: ex k be Nat st ( dom ws) c= ( Seg k) by A2, FINSEQ_1:def 12;

      then

      reconsider ws as FinSubsequence by FINSEQ_1:def 12;

      now

        let z be object;

        assume

         A4: z in ws;

        then

        consider x,y be object such that

         A5: z = [x, y] by RELAT_1:def 1;

        

         A6: x in ( dom es) by A2, A4, A5, FUNCT_1: 1;

        then

         A7: [x, (es . x)] in es by FUNCT_1: 1;

        then

         A8: x in ( dom (W1 .edgeSeq() )) by FUNCT_1: 1;

        

         A9: (ws . x) = y by A4, A5, FUNCT_1: 1;

        reconsider x as Element of NAT by A8;

        x <= ( len (W1 .edgeSeq() )) by A8, FINSEQ_3: 25;

        then

         A10: x <= ( len (W1 .weightSeq() )) by Def18;

        

         A11: 1 <= x by A8, FINSEQ_3: 25;

        then

         A12: ((W1 .weightSeq() ) . x) = (( the_Weight_of G) . ((W1 .edgeSeq() ) . x)) by A10, Def18;

        x in ( dom (W1 .weightSeq() )) by A11, A10, FINSEQ_3: 25;

        then

         A13: [x, ((W1 .weightSeq() ) . x)] in (W1 .weightSeq() ) by FUNCT_1: 1;

        y = (( the_Weight_of G) . (es . x)) by A2, A6, A9;

        hence z in (W1 .weightSeq() ) by A5, A7, A13, A12, FUNCT_1: 1;

      end;

      then

      reconsider ws as Subset of (W1 .weightSeq() ) by TARSKI:def 3;

      take ws;

      

       A14: ( len ( Seq es)) = ( card es) by GLIB_001: 5

      .= ( card ( dom ws)) by A2, CARD_1: 62

      .= ( card ws) by CARD_1: 62

      .= ( len ( Seq ws)) by GLIB_001: 5;

      then

       A15: ( len (W2 .weightSeq() )) = ( len ( Seq ws)) by A1, Def18;

      now

        

         A16: ( rng ( Sgm ( dom es))) = ( dom es) by A2, A3, FINSEQ_1:def 13;

        let n be Nat;

        

         A17: ( Seq ws) = (ws * ( Sgm ( dom es))) by A2, FINSEQ_1:def 14;

        assume

         A18: 1 <= n & n <= ( len (W2 .weightSeq() ));

        then

         A19: ( Seq es) = (es * ( Sgm ( dom es))) & n in ( dom ( Seq es)) by A14, A15, FINSEQ_1:def 14, FINSEQ_3: 25;

        

         A20: n in ( dom ( Seq ws)) by A15, A18, FINSEQ_3: 25;

        then n in ( dom ( Sgm ( dom es))) by A17, FUNCT_1: 11;

        then

         A21: (( Sgm ( dom es)) . n) in ( dom es) by A16, FUNCT_1:def 3;

        (( Seq ws) . n) = (ws . (( Sgm ( dom es)) . n)) by A17, A20, FUNCT_1: 12

        .= (( the_Weight_of G) . (es . (( Sgm ( dom es)) . n))) by A2, A21

        .= (( the_Weight_of G) . (( Seq es) . n)) by A19, FUNCT_1: 12;

        hence ((W2 .weightSeq() ) . n) = (( Seq ws) . n) by A1, A18, Def18;

      end;

      hence thesis by A15, FINSEQ_1: 14;

    end;

    theorem :: GLIB_003:19

    

     Th19: for G1,G2 be WGraph, W1 be Walk of G1, W2 be Walk of G2 st W1 = W2 & ( the_Weight_of G1) = ( the_Weight_of G2) holds (W1 .weightSeq() ) = (W2 .weightSeq() )

    proof

      let G1,G2 be WGraph, W1 be Walk of G1, W2 be Walk of G2;

      assume that

       A1: W1 = W2 and

       A2: ( the_Weight_of G1) = ( the_Weight_of G2);

      set WS1 = (W1 .weightSeq() ), WS2 = (W2 .weightSeq() );

      

       A3: (W1 .edgeSeq() ) = (W2 .edgeSeq() ) by A1, GLIB_001: 86;

      now

        thus ( len WS1) = ( len WS1);

        

        thus

         A4: ( len WS2) = ( len (W1 .edgeSeq() )) by A3, Def18

        .= ( len WS1) by Def18;

        let x be Nat;

        assume

         A5: x in ( dom WS1);

        then

         A6: 1 <= x by FINSEQ_3: 25;

        

         A7: x <= ( len WS1) by A5, FINSEQ_3: 25;

        x <= ( len WS2) by A4, A5, FINSEQ_3: 25;

        

        hence (WS2 . x) = (( the_Weight_of G2) . ((W2 .edgeSeq() ) . x)) by A6, Def18

        .= (( the_Weight_of G1) . ((W1 .edgeSeq() ) . x)) by A1, A2, GLIB_001: 86

        .= (WS1 . x) by A6, A7, Def18;

      end;

      hence thesis by FINSEQ_2: 9;

    end;

    theorem :: GLIB_003:20

    

     Th20: for G1 be WGraph, G2 be WSubgraph of G1, W1 be Walk of G1, W2 be Walk of G2 st W1 = W2 holds (W1 .weightSeq() ) = (W2 .weightSeq() )

    proof

      let G1 be WGraph, G2 be WSubgraph of G1, W1 be Walk of G1, W2 be Walk of G2;

      set WS1 = (W1 .weightSeq() ), WS2 = (W2 .weightSeq() );

      assume W1 = W2;

      then

       A1: (W1 .edgeSeq() ) = (W2 .edgeSeq() ) by GLIB_001: 86;

      now

        thus ( len WS1) = ( len WS1);

        

        thus

         A2: ( len WS2) = ( len (W1 .edgeSeq() )) by A1, Def18

        .= ( len WS1) by Def18;

        let x be Nat;

        assume

         A3: x in ( dom WS1);

        then

         A4: 1 <= x by FINSEQ_3: 25;

        

         A5: x <= ( len WS2) by A2, A3, FINSEQ_3: 25;

        then x <= ( len (W2 .edgeSeq() )) by Def18;

        then

         A6: x in ( dom (W2 .edgeSeq() )) by A4, FINSEQ_3: 25;

        

         A7: x <= ( len WS1) by A3, FINSEQ_3: 25;

        

        thus (WS2 . x) = (( the_Weight_of G2) . ((W2 .edgeSeq() ) . x)) by A4, A5, Def18

        .= ((( the_Weight_of G1) | ( the_Edges_of G2)) . ((W2 .edgeSeq() ) . x)) by Def10

        .= (( the_Weight_of G1) . ((W1 .edgeSeq() ) . x)) by A1, A6, FUNCT_1: 49, GLIB_001: 79

        .= (WS1 . x) by A4, A7, Def18;

      end;

      hence thesis by FINSEQ_2: 9;

    end;

    theorem :: GLIB_003:21

    for G be real-weighted WGraph, W be Walk of G holds W is trivial implies (W .cost() ) = 0 by Th12, RVSUM_1: 72;

    theorem :: GLIB_003:22

    for G be real-weighted WGraph, v1,v2 be Vertex of G, e be set st e Joins (v1,v2,G) holds ((G .walkOf (v1,e,v2)) .cost() ) = (( the_Weight_of G) . e)

    proof

      let G be real-weighted WGraph, v1,v2 be Vertex of G, e be set;

      set W = (G .walkOf (v1,e,v2));

      reconsider We = (( the_Weight_of G) . e) as Element of REAL by XREAL_0:def 1;

      assume e Joins (v1,v2,G);

      then (W .weightSeq() ) = <*We*> by Th14;

      hence thesis by FINSOP_1: 11;

    end;

    theorem :: GLIB_003:23

    for G be real-weighted WGraph, W be Walk of G holds (W .cost() ) = ((W .reverse() ) .cost() )

    proof

      let G be real-weighted WGraph, W be Walk of G;

      

      thus (W .cost() ) = ( Sum ( Rev (W .weightSeq() ))) by POLYNOM3: 3

      .= ((W .reverse() ) .cost() ) by Th15;

    end;

    theorem :: GLIB_003:24

    for G be real-weighted WGraph, W1,W2 be Walk of G st (W1 .last() ) = (W2 .first() ) holds ((W1 .append W2) .cost() ) = ((W1 .cost() ) + (W2 .cost() ))

    proof

      let G be real-weighted WGraph, W1,W2 be Walk of G;

      set W3 = (W1 .append W2);

      assume (W1 .last() ) = (W2 .first() );

      then (W3 .weightSeq() ) = ((W1 .weightSeq() ) ^ (W2 .weightSeq() )) by Th16;

      hence thesis by RVSUM_1: 75;

    end;

    theorem :: GLIB_003:25

    for G be real-weighted WGraph, W be Walk of G, e be set st e in ((W .last() ) .edgesInOut() ) holds ((W .addEdge e) .cost() ) = ((W .cost() ) + (( the_Weight_of G) . e))

    proof

      let G be real-weighted WGraph, W be Walk of G, e be set;

      set W2 = (W .addEdge e);

      reconsider We = (( the_Weight_of G) . e) as Element of REAL by XREAL_0:def 1;

      assume e in ((W .last() ) .edgesInOut() );

      then (W2 .weightSeq() ) = ((W .weightSeq() ) ^ <*(( the_Weight_of G) . e)*>) by Th17;

      then ( Sum (W2 .weightSeq() )) = (( Sum (W .weightSeq() )) + ( Sum <*We*>)) by RVSUM_1: 75;

      hence thesis by FINSOP_1: 11;

    end;

    theorem :: GLIB_003:26

    for G1,G2 be real-weighted WGraph, W1 be Walk of G1, W2 be Walk of G2 st W1 = W2 & ( the_Weight_of G1) = ( the_Weight_of G2) holds (W1 .cost() ) = (W2 .cost() ) by Th19;

    theorem :: GLIB_003:27

    for G1 be real-weighted WGraph, G2 be WSubgraph of G1, W1 be Walk of G1, W2 be Walk of G2 st W1 = W2 holds (W1 .cost() ) = (W2 .cost() ) by Th20;

    theorem :: GLIB_003:28

    

     Th28: for G be nonnegative-weighted WGraph, W be Walk of G, n be Element of NAT st n in ( dom (W .weightSeq() )) holds 0 <= ((W .weightSeq() ) . n)

    proof

      let G be nonnegative-weighted WGraph, W be Walk of G, n be Element of NAT ;

      set WS = (W .weightSeq() );

      assume

       A1: n in ( dom (W .weightSeq() ));

      then

       A2: 1 <= n by FINSEQ_3: 25;

      

       A3: n <= ( len WS) by A1, FINSEQ_3: 25;

      then n <= ( len (W .edgeSeq() )) by Def18;

      then ( dom ( the_Weight_of G)) = ( the_Edges_of G) & n in ( dom (W .edgeSeq() )) by A2, FINSEQ_3: 25, PARTFUN1:def 2;

      then

       A4: ((W .edgeSeq() ) . n) in ( dom ( the_Weight_of G)) by GLIB_001: 79;

      (WS . n) = (( the_Weight_of G) . ((W .edgeSeq() ) . n)) by A2, A3, Def18;

      then

       A5: (WS . n) in ( rng ( the_Weight_of G)) by A4, FUNCT_1:def 3;

      ( rng ( the_Weight_of G)) c= Real>=0 by Def14;

      then (WS . n) in Real>=0 by A5;

      then ex r be Real st r = (WS . n) & r >= 0 by GRAPH_5:def 12;

      hence thesis;

    end;

    theorem :: GLIB_003:29

    for G be nonnegative-weighted WGraph, W be Walk of G holds 0 <= (W .cost() )

    proof

      let G be nonnegative-weighted WGraph, W be Walk of G;

      for i be Nat st i in ( dom (W .weightSeq() )) holds 0 <= ((W .weightSeq() ) . i) by Th28;

      hence thesis by RVSUM_1: 84;

    end;

    theorem :: GLIB_003:30

    for G be nonnegative-weighted WGraph, W1 be Walk of G, W2 be Subwalk of W1 holds (W2 .cost() ) <= (W1 .cost() )

    proof

      let G be nonnegative-weighted WGraph, W1 be Walk of G, W2 be Subwalk of W1;

      (ex ws be Subset of (W1 .weightSeq() ) st (W2 .weightSeq() ) = ( Seq ws)) & for i be Element of NAT st i in ( dom (W1 .weightSeq() )) holds 0 <= ((W1 .weightSeq() ) . i) by Th18, Th28;

      hence thesis by Th2;

    end;

    theorem :: GLIB_003:31

    for G be nonnegative-weighted WGraph, e be set holds e in ( the_Edges_of G) implies 0 <= (( the_Weight_of G) . e)

    proof

      let G be nonnegative-weighted WGraph, e be set;

      assume e in ( the_Edges_of G);

      then e in ( dom ( the_Weight_of G)) by PARTFUN1:def 2;

      then

       A1: (( the_Weight_of G) . e) in ( rng ( the_Weight_of G)) by FUNCT_1: 3;

      ( rng ( the_Weight_of G)) c= Real>=0 by Def14;

      then (( the_Weight_of G) . e) in Real>=0 by A1;

      then ex r be Real st (( the_Weight_of G) . e) = r & r >= 0 by GRAPH_5:def 12;

      hence thesis;

    end;

    theorem :: GLIB_003:32

    

     Th32: for G be EGraph, e,x be set st e in ( the_Edges_of G) holds ( the_ELabel_of (G .labelEdge (e,x))) = (( the_ELabel_of G) +* (e .--> x))

    proof

      let G be EGraph, e,x be set;

      assume e in ( the_Edges_of G);

      then ( the_ELabel_of (G .labelEdge (e,x))) = ((G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) . ELabelSelector ) by Def21;

      hence thesis by GLIB_000: 8;

    end;

    theorem :: GLIB_003:33

    for G be EGraph, e,x be set st e in ( the_Edges_of G) holds (( the_ELabel_of (G .labelEdge (e,x))) . e) = x

    proof

      let G be EGraph, e,x be set;

      e in {e} by TARSKI:def 1;

      then

       A1: e in ( dom (e .--> x));

      assume e in ( the_Edges_of G);

      then ( the_ELabel_of (G .labelEdge (e,x))) = (( the_ELabel_of G) +* (e .--> x)) by Th32;

      

      then (( the_ELabel_of (G .labelEdge (e,x))) . e) = ((e .--> x) . e) by A1, FUNCT_4: 13

      .= x by FUNCOP_1: 72;

      hence thesis;

    end;

    theorem :: GLIB_003:34

    for G be EGraph, e,x be set holds G == (G .labelEdge (e,x))

    proof

      let G be EGraph, e,x be set;

      now

        per cases ;

          suppose

           A1: e in ( the_Edges_of G);

          

           A2: not ELabelSelector in _GraphSelectors by ENUMSET1:def 2;

          

           A3: (G .labelEdge (e,x)) = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by A1, Def21;

          then

           A4: ( the_Source_of G) = ( the_Source_of (G .labelEdge (e,x))) & ( the_Target_of G) = ( the_Target_of (G .labelEdge (e,x))) by A2, GLIB_000: 10;

          ( the_Vertices_of G) = ( the_Vertices_of (G .labelEdge (e,x))) & ( the_Edges_of G) = ( the_Edges_of (G .labelEdge (e,x))) by A3, A2, GLIB_000: 10;

          hence thesis by A4;

        end;

          suppose not e in ( the_Edges_of G);

          hence thesis by Def21;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_003:35

    for G be WEGraph, e,x be set holds ( the_Weight_of G) = ( the_Weight_of (G .labelEdge (e,x)))

    proof

      let G be WEGraph, e,x be set;

      set G2 = (G .labelEdge (e,x));

      now

        per cases ;

          suppose e in ( the_Edges_of G);

          then G2 = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

          hence thesis by GLIB_000: 9;

        end;

          suppose not e in ( the_Edges_of G);

          hence thesis by Def21;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_003:36

    

     Th36: for G be EVGraph, e,x be set holds ( the_VLabel_of G) = ( the_VLabel_of (G .labelEdge (e,x)))

    proof

      let G be EVGraph, e,x be set;

      set G2 = (G .labelEdge (e,x));

      now

        per cases ;

          suppose e in ( the_Edges_of G);

          then G2 = (G .set ( ELabelSelector ,(( the_ELabel_of G) +* (e .--> x)))) by Def21;

          hence thesis by GLIB_000: 9;

        end;

          suppose not e in ( the_Edges_of G);

          hence thesis by Def21;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_003:37

    for G be EGraph, e1,e2,x be set st e1 <> e2 holds (( the_ELabel_of (G .labelEdge (e1,x))) . e2) = (( the_ELabel_of G) . e2)

    proof

      let G be EGraph, e1,e2,x be set;

      set G2 = (G .labelEdge (e1,x));

      assume

       A1: e1 <> e2;

      now

        per cases ;

          suppose

           A2: e1 in ( the_Edges_of G);

           not e2 in {e1} by A1, TARSKI:def 1;

          then

           A3: not e2 in ( dom (e1 .--> x));

          ( the_ELabel_of G2) = (( the_ELabel_of G) +* (e1 .--> x)) by A2, Th32;

          hence thesis by A3, FUNCT_4: 11;

        end;

          suppose not e1 in ( the_Edges_of G);

          hence thesis by Def21;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_003:38

    

     Th38: for G be VGraph, v,x be set st v in ( the_Vertices_of G) holds ( the_VLabel_of (G .labelVertex (v,x))) = (( the_VLabel_of G) +* (v .--> x))

    proof

      let G be VGraph, e,x be set;

      assume e in ( the_Vertices_of G);

      then ( the_VLabel_of (G .labelVertex (e,x))) = ((G .set ( VLabelSelector ,(( the_VLabel_of G) +* (e .--> x)))) . VLabelSelector ) by Def22;

      hence thesis by GLIB_000: 8;

    end;

    theorem :: GLIB_003:39

    for G be VGraph, v,x be set st v in ( the_Vertices_of G) holds (( the_VLabel_of (G .labelVertex (v,x))) . v) = x

    proof

      let G be VGraph, e,x be set;

      e in {e} by TARSKI:def 1;

      then

       A1: e in ( dom (e .--> x));

      assume e in ( the_Vertices_of G);

      then ( the_VLabel_of (G .labelVertex (e,x))) = (( the_VLabel_of G) +* (e .--> x)) by Th38;

      

      then (( the_VLabel_of (G .labelVertex (e,x))) . e) = ((e .--> x) . e) by A1, FUNCT_4: 13

      .= x by FUNCOP_1: 72;

      hence thesis;

    end;

    theorem :: GLIB_003:40

    for G be VGraph, v,x be set holds G == (G .labelVertex (v,x))

    proof

      let G be VGraph, e,x be set;

      now

        per cases ;

          suppose

           A1: e in ( the_Vertices_of G);

          

           A2: not VLabelSelector in _GraphSelectors by ENUMSET1:def 2;

          

           A3: (G .labelVertex (e,x)) = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (e .--> x)))) by A1, Def22;

          then

           A4: ( the_Source_of G) = ( the_Source_of (G .labelVertex (e,x))) & ( the_Target_of G) = ( the_Target_of (G .labelVertex (e,x))) by A2, GLIB_000: 10;

          ( the_Vertices_of G) = ( the_Vertices_of (G .labelVertex (e,x))) & ( the_Edges_of G) = ( the_Edges_of (G .labelVertex (e,x))) by A3, A2, GLIB_000: 10;

          hence thesis by A4;

        end;

          suppose not e in ( the_Vertices_of G);

          hence thesis by Def22;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_003:41

    for G be WVGraph, v,x be set holds ( the_Weight_of G) = ( the_Weight_of (G .labelVertex (v,x)))

    proof

      let G be WVGraph, e,x be set;

      set G2 = (G .labelVertex (e,x));

      now

        per cases ;

          suppose e in ( the_Vertices_of G);

          then G2 = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (e .--> x)))) by Def22;

          hence thesis by GLIB_000: 9;

        end;

          suppose not e in ( the_Vertices_of G);

          hence thesis by Def22;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_003:42

    

     Th42: for G be EVGraph, v,x be set holds ( the_ELabel_of G) = ( the_ELabel_of (G .labelVertex (v,x)))

    proof

      let G be EVGraph, e,x be set;

      set G2 = (G .labelVertex (e,x));

      now

        per cases ;

          suppose e in ( the_Vertices_of G);

          then G2 = (G .set ( VLabelSelector ,(( the_VLabel_of G) +* (e .--> x)))) by Def22;

          hence thesis by GLIB_000: 9;

        end;

          suppose not e in ( the_Vertices_of G);

          hence thesis by Def22;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_003:43

    for G be VGraph, v1,v2,x be set st v1 <> v2 holds (( the_VLabel_of (G .labelVertex (v1,x))) . v2) = (( the_VLabel_of G) . v2)

    proof

      let G be VGraph, v1,v2,x be set;

      set G2 = (G .labelVertex (v1,x));

      assume

       A1: v1 <> v2;

      now

        per cases ;

          suppose

           A2: v1 in ( the_Vertices_of G);

           not v2 in {v1} by A1, TARSKI:def 1;

          then

           A3: not v2 in ( dom (v1 .--> x));

          ( the_VLabel_of G2) = (( the_VLabel_of G) +* (v1 .--> x)) by A2, Th38;

          hence thesis by A3, FUNCT_4: 11;

        end;

          suppose not v1 in ( the_Vertices_of G);

          hence thesis by Def22;

        end;

      end;

      hence thesis;

    end;

    theorem :: GLIB_003:44

    for G1,G2 be EGraph st ( the_ELabel_of G1) = ( the_ELabel_of G2) holds (G1 .labeledE() ) = (G2 .labeledE() );

    theorem :: GLIB_003:45

    

     Th45: for G be EGraph, e,x be set st e in ( the_Edges_of G) holds ((G .labelEdge (e,x)) .labeledE() ) = ((G .labeledE() ) \/ {e})

    proof

      let G be EGraph, e,val be set;

      set G2 = (G .labelEdge (e,val)), EG = ( the_ELabel_of G), EG2 = ( the_ELabel_of G2);

      assume e in ( the_Edges_of G);

      then EG2 = (EG +* (e .--> val)) by Th32;

      then ( dom EG2) = (( dom EG) \/ ( dom (e .--> val))) by FUNCT_4:def 1;

      hence thesis;

    end;

    theorem :: GLIB_003:46

    for G be EGraph, e,x be set st e in ( the_Edges_of G) holds (G .labeledE() ) c= ((G .labelEdge (e,x)) .labeledE() )

    proof

      let G be EGraph, e,x be set;

      assume e in ( the_Edges_of G);

      then ((G .labelEdge (e,x)) .labeledE() ) = ((G .labeledE() ) \/ {e}) by Th45;

      hence thesis by XBOOLE_1: 7;

    end;

    theorem :: GLIB_003:47

    for G be _finite EGraph, e,x be set st e in ( the_Edges_of G) & not e in (G .labeledE() ) holds ( card ((G .labelEdge (e,x)) .labeledE() )) = (( card (G .labeledE() )) + 1)

    proof

      let G be _finite EGraph, e,val be set;

      set G2 = (G .labelEdge (e,val));

      set ECurr = ( the_ELabel_of G), ENext = ( the_ELabel_of G2);

      assume e in ( the_Edges_of G) & not e in (G .labeledE() );

      then

       A1: ( card (( dom ECurr) \/ {e})) = (( card ( dom ECurr)) + 1) & ENext = (ECurr +* (e .--> val)) by Th32, CARD_2: 41;

      ( dom (e .--> val)) = {e};

      hence thesis by A1, FUNCT_4:def 1;

    end;

    theorem :: GLIB_003:48

    for G be EGraph, e1,e2,x be set st not e2 in (G .labeledE() ) & e2 in ((G .labelEdge (e1,x)) .labeledE() ) holds e1 = e2 & e1 in ( the_Edges_of G)

    proof

      let G be EGraph, e1,e2,val be set;

      set Gn = (G .labelEdge (e1,val));

      assume that

       A1: not e2 in (G .labeledE() ) and

       A2: e2 in (Gn .labeledE() );

      e1 in ( the_Edges_of G) by A1, A2, Def21;

      then ( the_ELabel_of Gn) = (( the_ELabel_of G) +* (e1 .--> val)) by Th32;

      then e2 in ( dom ( the_ELabel_of G)) or e2 in ( dom (e1 .--> val)) by A2, FUNCT_4: 12;

      then e2 in {e1} by A1;

      hence e1 = e2 by TARSKI:def 1;

      thus thesis by A1, A2, Def21;

    end;

    theorem :: GLIB_003:49

    for G be EVGraph, v,x be set holds (G .labeledE() ) = ((G .labelVertex (v,x)) .labeledE() ) by Th42;

    theorem :: GLIB_003:50

    for G be EGraph, e,x be set st e in ( the_Edges_of G) holds e in ((G .labelEdge (e,x)) .labeledE() )

    proof

      let G be EGraph, e,x be set;

      assume e in ( the_Edges_of G);

      then

       A1: ((G .labelEdge (e,x)) .labeledE() ) = ((G .labeledE() ) \/ {e}) by Th45;

      e in {e} by TARSKI:def 1;

      hence thesis by A1, XBOOLE_0:def 3;

    end;

    theorem :: GLIB_003:51

    for G1,G2 be VGraph st ( the_VLabel_of G1) = ( the_VLabel_of G2) holds (G1 .labeledV() ) = (G2 .labeledV() );

    theorem :: GLIB_003:52

    

     Th52: for G be VGraph, v,x be set st v in ( the_Vertices_of G) holds ((G .labelVertex (v,x)) .labeledV() ) = ((G .labeledV() ) \/ {v})

    proof

      let G be VGraph, e,val be set;

      set G2 = (G .labelVertex (e,val)), EG = ( the_VLabel_of G), EG2 = ( the_VLabel_of G2);

      assume e in ( the_Vertices_of G);

      then EG2 = (EG +* (e .--> val)) by Th38;

      then ( dom EG2) = (( dom EG) \/ ( dom (e .--> val))) by FUNCT_4:def 1;

      hence thesis;

    end;

    theorem :: GLIB_003:53

    for G be VGraph, v,x be set st v in ( the_Vertices_of G) holds (G .labeledV() ) c= ((G .labelVertex (v,x)) .labeledV() )

    proof

      let G be VGraph, e,x be set;

      assume e in ( the_Vertices_of G);

      then ((G .labelVertex (e,x)) .labeledV() ) = ((G .labeledV() ) \/ {e}) by Th52;

      hence thesis by XBOOLE_1: 7;

    end;

    theorem :: GLIB_003:54

    for G be _finite VGraph, v,x be set st v in ( the_Vertices_of G) & not v in (G .labeledV() ) holds ( card ((G .labelVertex (v,x)) .labeledV() )) = (( card (G .labeledV() )) + 1)

    proof

      let G be _finite VGraph, e,val be set;

      set G2 = (G .labelVertex (e,val));

      set ECurr = ( the_VLabel_of G), ENext = ( the_VLabel_of G2);

      assume e in ( the_Vertices_of G) & not e in (G .labeledV() );

      then

       A1: ( card (( dom ECurr) \/ {e})) = (( card ( dom ECurr)) + 1) & ENext = (ECurr +* (e .--> val)) by Th38, CARD_2: 41;

      ( dom (e .--> val)) = {e};

      hence thesis by A1, FUNCT_4:def 1;

    end;

    theorem :: GLIB_003:55

    for G be VGraph, v1,v2,x be set st not v2 in (G .labeledV() ) & v2 in ((G .labelVertex (v1,x)) .labeledV() ) holds v1 = v2 & v1 in ( the_Vertices_of G)

    proof

      let G be VGraph, e1,e2,val be set;

      set Gn = (G .labelVertex (e1,val));

      assume that

       A1: not e2 in (G .labeledV() ) and

       A2: e2 in (Gn .labeledV() );

      e1 in ( the_Vertices_of G) by A1, A2, Def22;

      then ( the_VLabel_of Gn) = (( the_VLabel_of G) +* (e1 .--> val)) by Th38;

      then e2 in ( dom ( the_VLabel_of G)) or e2 in ( dom (e1 .--> val)) by A2, FUNCT_4: 12;

      then e2 in {e1} by A1;

      hence e1 = e2 by TARSKI:def 1;

      thus thesis by A1, A2, Def22;

    end;

    theorem :: GLIB_003:56

    for G be EVGraph, e,x be set holds (G .labeledV() ) = ((G .labelEdge (e,x)) .labeledV() ) by Th36;

    theorem :: GLIB_003:57

    for G be VGraph, v be Vertex of G, x be set holds v in ((G .labelVertex (v,x)) .labeledV() )

    proof

      let G be VGraph, v be Vertex of G, x be set;

      ((G .labelVertex (v,x)) .labeledV() ) = ((G .labeledV() ) \/ {v}) & v in {v} by Th52, TARSKI:def 1;

      hence thesis by XBOOLE_0:def 3;

    end;