graph_5.miz



    begin

    reserve n,m,i,j,k for Nat,

x,y,e,X,V,U for set,

W,f,g for Function;

    theorem :: GRAPH_5:1

    ( rng f) c= ( rng g) & x in ( dom f) implies ex y be object st y in ( dom g) & (f . x) = (g . y)

    proof

      assume that

       A1: ( rng f) c= ( rng g) and

       A2: x in ( dom f);

      (f . x) in ( rng f) by A2, FUNCT_1: 3;

      hence thesis by A1, FUNCT_1:def 3;

    end;

    theorem :: GRAPH_5:2

    

     Th2: for D be finite set, n be Element of NAT , X be set st X = { x where x be Element of (D * ) : 1 <= ( len x) & ( len x) <= n } holds X is finite

    proof

      let D be finite set, n be Element of NAT , X be set;

      deffunc F( Element of NAT ) = ($1 -tuples_on D);

      consider f be Function such that

       A1: ( dom f) = ( Seg n) & for x be Element of NAT st x in ( Seg n) holds (f . x) = F(x) from CLASSES1:sch 2;

      assume

       A2: X = { x where x be Element of (D * ) : 1 <= ( len x) & ( len x) <= n };

      

       A3: X c= ( Union f)

      proof

        let x be object;

        assume x in X;

        then

        consider y be Element of (D * ) such that

         A4: x = y and

         A5: 1 <= ( len y) & ( len y) <= n by A2;

        consider m be Nat such that

         A6: ( dom y) = ( Seg m) by FINSEQ_1:def 2;

        m in NAT by ORDINAL1:def 12;

        then

         A7: ( len y) = m by A6, FINSEQ_1:def 3;

        then

         A8: m in ( dom f) by A1, A5, FINSEQ_1: 1;

        y in { s where s be Element of (D * ) : ( len s) = m } by A7;

        then y in (m -tuples_on D) by FINSEQ_2:def 4;

        then y in (f . m) by A1, A8;

        hence thesis by A4, A8, CARD_5: 2;

      end;

      now

        let x be object;

        assume

         A9: x in ( dom f);

        then

        reconsider z = x as Element of NAT by A1;

        (f . z) = F(z) by A1, A9;

        hence (f . x) is finite;

      end;

      then ( Union f) is finite by A1, CARD_2: 88;

      hence thesis by A3;

    end;

    theorem :: GRAPH_5:3

    

     Th3: for D be finite set, n be Element of NAT , X be set st X = { x where x be Element of (D * ) : ( len x) <= n } holds X is finite

    proof

      let D be finite set, n be Element of NAT , X be set;

      set B = { x where x be Element of (D * ) : 1 <= ( len x) & ( len x) <= n };

      assume

       A1: X = { x where x be Element of (D * ) : ( len x) <= n };

      

       A2: X c= ( { {} } \/ B)

      proof

        let y be object;

        assume y in X;

        then

        consider x be Element of (D * ) such that

         A3: y = x and

         A4: ( len x) <= n by A1;

        per cases ;

          suppose ( len x) < ( 0 + 1);

          then x = {} by NAT_1: 13;

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

          hence thesis by A3, XBOOLE_0:def 3;

        end;

          suppose ( len x) >= ( 0 + 1);

          then x in B by A4;

          hence thesis by A3, XBOOLE_0:def 3;

        end;

      end;

      B is finite by Th2;

      hence thesis by A2;

    end;

    ::$Canceled

    definition

      let D be set, X be non empty Subset of (D * );

      :: original: Element

      redefine

      mode Element of X -> FinSequence of D ;

      coherence

      proof

        let x be Element of X;

        reconsider y = x as Element of (D * );

        y is FinSequence of D;

        hence thesis;

      end;

    end

    begin

    reserve p,q for FinSequence;

    

     Lm1: 1 <= n & n <= ( len p) implies (p . n) = ((p ^ q) . n)

    proof

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

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

      hence thesis by FINSEQ_1:def 7;

    end;

    

     Lm2: 1 <= n & n <= ( len q) implies (q . n) = ((p ^ q) . (( len p) + n))

    proof

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

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

      hence thesis by FINSEQ_1:def 7;

    end;

    theorem :: GRAPH_5:6

    

     Th4: (for n, m st 1 <= n & n < m & m <= ( len p) holds (p . n) <> (p . m)) iff p is one-to-one

    proof

      hereby

        assume

         A1: for n, m st 1 <= n & n < m & m <= ( len p) holds (p . n) <> (p . m);

        thus p is one-to-one

        proof

          let x1,x2 be object;

          assume that

           A2: x1 in ( dom p) & x2 in ( dom p) and

           A3: (p . x1) = (p . x2);

          reconsider n = x1, m = x2 as Element of NAT by A2;

          

           A4: n <= ( len p) & 1 <= m by A2, FINSEQ_3: 25;

          

           A5: 1 <= n & m <= ( len p) by A2, FINSEQ_3: 25;

          assume

           A6: x1 <> x2;

          per cases ;

            suppose m <= n;

            then m < n by A6, XXREAL_0: 1;

            hence contradiction by A1, A3, A4;

          end;

            suppose m > n;

            hence contradiction by A1, A3, A5;

          end;

        end;

      end;

      assume

       A7: p is one-to-one;

      let n, m;

      assume that

       A8: 1 <= n and

       A9: n < m and

       A10: m <= ( len p);

      n <= ( len p) by A9, A10, XXREAL_0: 2;

      then

       A11: n in ( dom p) by A8, FINSEQ_3: 25;

      1 <= m by A8, A9, XXREAL_0: 2;

      then

       A12: m in ( dom p) by A10, FINSEQ_3: 25;

      assume (p . n) = (p . m);

      hence contradiction by A7, A9, A11, A12;

    end;

    theorem :: GRAPH_5:7

    

     Th5: (for n, m st 1 <= n & n < m & m <= ( len p) holds (p . n) <> (p . m)) iff ( card ( rng p)) = ( len p) by Th4, FINSEQ_4: 62;

    reserve G for Graph,

pe,qe for FinSequence of the carrier' of G;

    theorem :: GRAPH_5:8

    i in ( dom pe) implies (the Source of G . (pe . i)) in the carrier of G & (the Target of G . (pe . i)) in the carrier of G by FINSEQ_2: 11, FUNCT_2: 5;

    theorem :: GRAPH_5:9

    

     Th7: for x be object holds (q ^ <*x*>) is one-to-one & ( rng (q ^ <*x*>)) c= ( rng p) implies ex p1,p2 be FinSequence st p = ((p1 ^ <*x*>) ^ p2) & ( rng q) c= ( rng (p1 ^ p2))

    proof

      let x be object;

      set r = (q ^ <*x*>), i = (( len q) + 1);

      assume that

       A1: r is one-to-one and

       A2: ( rng r) c= ( rng p);

      

       A3: (r . i) = x by FINSEQ_1: 42;

      ( rng q) c= ( rng r) by FINSEQ_1: 29;

      then

       A4: ( rng q) c= ( rng p) by A2;

      ( len r) = i & 1 <= i by FINSEQ_2: 16, NAT_1: 11;

      then

       A5: i in ( dom r) by FINSEQ_3: 25;

      then

      consider y be object such that

       A6: y in ( dom p) and

       A7: (r . i) = (p . y) by A2, FUNCT_1: 114;

      reconsider j = y as Element of NAT by A6;

      j <= ( len p) by A6, FINSEQ_3: 25;

      then

      consider k be Nat such that

       A8: ( len p) = (j + k) by NAT_1: 10;

      reconsider k as Element of NAT by ORDINAL1:def 12;

      consider s,p2 be FinSequence such that

       A9: ( len s) = j and ( len p2) = k and

       A10: p = (s ^ p2) by A8, FINSEQ_2: 22;

      

       A11: 1 <= j by A6, FINSEQ_3: 25;

      then ex m be Nat st j = (1 + m) by NAT_1: 10;

      then

      consider p1 be FinSequence, d be object such that

       A12: s = (p1 ^ <*d*>) by A9, FINSEQ_2: 18;

      j in ( dom s) by A9, A11, FINSEQ_3: 25;

      then

       A13: (s . j) = x by A7, A10, A3, FINSEQ_1:def 7;

      take p1, p2;

      

       A14: j = (( len p1) + 1) by A9, A12, FINSEQ_2: 16;

      hence p = ((p1 ^ <*x*>) ^ p2) by A10, A12, A13, FINSEQ_1: 42;

      let y be object;

      assume

       A15: y in ( rng q);

      now

        let y be set;

        assume

         A16: y in ( rng q);

        assume y = x;

        then

        consider z be object such that

         A17: z in ( dom q) and

         A18: x = (q . z) by A16, FUNCT_1:def 3;

        reconsider n = z as Element of NAT by A17;

        n <= ( len q) by A17, FINSEQ_3: 25;

        then

         A19: n <> i by XREAL_1: 29;

        n in ( dom r) & (r . n) = (r . i) by A3, A17, A18, FINSEQ_1:def 7, FINSEQ_2: 15;

        hence contradiction by A1, A5, A19;

      end;

      then

       A20: y <> x by A15;

      s = (p1 ^ <*x*>) by A12, A14, A13, FINSEQ_1: 42;

      

      then ( rng p) = (( rng (p1 ^ <*x*>)) \/ ( rng p2)) by A10, FINSEQ_1: 31

      .= ((( rng p1) \/ ( rng <*x*>)) \/ ( rng p2)) by FINSEQ_1: 31

      .= ((( rng p1) \/ ( rng p2)) \/ ( rng <*x*>)) by XBOOLE_1: 4

      .= (( rng (p1 ^ p2)) \/ ( rng <*x*>)) by FINSEQ_1: 31

      .= (( rng (p1 ^ p2)) \/ {x}) by FINSEQ_1: 38;

      then y in ( rng (p1 ^ p2)) or y in {x} by A15, A4, XBOOLE_0:def 3;

      hence thesis by A20, TARSKI:def 1;

    end;

    begin

    theorem :: GRAPH_5:10

    

     Th8: (p ^ q) is Chain of G implies p is Chain of G & q is Chain of G

    proof

      set r = (p ^ q), D = the carrier' of G, V = the carrier of G;

      assume

       A1: (p ^ q) is Chain of G;

      then

      consider f be FinSequence such that

       A2: ( len f) = (( len r) + 1) and

       A3: for n st 1 <= n & n <= ( len f) holds (f . n) in V and

       A4: for n st 1 <= n & n <= ( len r) holds ex x,y be Element of V st x = (f . n) & y = (f . (n + 1)) & (r . n) joins (x,y) by GRAPH_1:def 14;

      

       A5: ( len r) = (( len p) + ( len q)) by FINSEQ_1: 22;

      then ( len f) = (( len p) + (( len q) + 1)) by A2;

      then

      consider h1,h2 be FinSequence such that

       A6: ( len h1) = ( len p) and

       A7: ( len h2) = (( len q) + 1) and

       A8: f = (h1 ^ h2) by FINSEQ_2: 22;

       A9:

      now

        take h2;

        thus ( len h2) = (( len q) + 1) by A7;

        hereby

          let n;

          assume that

           A10: 1 <= n and

           A11: n <= ( len h2);

          n <= (( len h1) + n) by NAT_1: 11;

          then

           A12: 1 <= (( len h1) + n) by A10, XXREAL_0: 2;

          (( len h1) + n) <= (( len h1) + ( len h2)) by A11, XREAL_1: 7;

          then

           A13: (( len h1) + n) <= ( len f) by A8, FINSEQ_1: 22;

          n in ( dom h2) by A10, A11, FINSEQ_3: 25;

          then (h2 . n) = (f . (( len h1) + n)) by A8, FINSEQ_1:def 7;

          hence (h2 . n) in V by A3, A13, A12;

        end;

        hereby

          let n;

          assume that

           A14: 1 <= n and

           A15: n <= ( len q);

          set m = (( len p) + n);

          n <= m by NAT_1: 11;

          then 1 <= m by A14, XXREAL_0: 2;

          then

          consider x,y be Element of V such that

           A16: x = (f . m) and

           A17: y = (f . (m + 1)) and

           A18: (r . m) joins (x,y) by A4, A5, A15, XREAL_1: 7;

          take x, y;

          ( len q) <= ( len h2) by A7, NAT_1: 11;

          then n <= ( len h2) by A15, XXREAL_0: 2;

          hence x = (h2 . n) by A6, A8, A14, A16, Lm2;

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

          

          hence (h2 . (n + 1)) = (f . (( len h1) + (n + 1))) by A7, A8, A15, Lm2, XREAL_1: 7

          .= y by A6, A17;

          thus (q . n) joins (x,y) by A14, A15, A18, Lm2;

        end;

      end;

      

       A19: ( len f) = ((( len p) + 1) + ( len q)) by A2, A5;

      then

      consider f1,f2 be FinSequence such that

       A20: ( len f1) = (( len p) + 1) and ( len f2) = ( len q) and

       A21: f = (f1 ^ f2) by FINSEQ_2: 22;

       A22:

      now

        take f1;

        thus ( len f1) = (( len p) + 1) by A20;

        hereby

          let n;

          assume that

           A23: 1 <= n and

           A24: n <= ( len f1);

          ( len f1) <= ( len f) by A19, A20, NAT_1: 11;

          then n <= ( len f) by A24, XXREAL_0: 2;

          then

           A25: (f . n) in V by A3, A23;

          n in ( dom f1) by A23, A24, FINSEQ_3: 25;

          hence (f1 . n) in V by A21, A25, FINSEQ_1:def 7;

        end;

        hereby

          let n;

          assume that

           A26: 1 <= n and

           A27: n <= ( len p);

          ( len p) <= ( len r) by A5, NAT_1: 11;

          then n <= ( len r) by A27, XXREAL_0: 2;

          then

          consider x,y be Element of V such that

           A28: x = (f . n) and

           A29: y = (f . (n + 1)) and

           A30: (r . n) joins (x,y) by A4, A26;

          take x, y;

          ( len p) <= ( len f1) by A20, NAT_1: 11;

          then n <= ( len f1) by A27, XXREAL_0: 2;

          hence x = (f1 . n) by A21, A26, A28, Lm1;

          1 <= (n + 1) & (n + 1) <= ( len f1) by A20, A27, NAT_1: 11, XREAL_1: 7;

          then (n + 1) in ( dom f1) by FINSEQ_3: 25;

          hence y = (f1 . (n + 1)) by A21, A29, FINSEQ_1:def 7;

          thus (p . n) joins (x,y) by A26, A27, A30, Lm1;

        end;

      end;

      

       A31: p is FinSequence of D by A1, FINSEQ_1: 36;

      now

        let n;

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

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

        hence (p . n) in D by A31, FINSEQ_2: 11;

      end;

      hence p is Chain of G by A22, GRAPH_1:def 14;

      

       A32: q is FinSequence of D by A1, FINSEQ_1: 36;

      now

        let n;

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

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

        hence (q . n) in D by A32, FINSEQ_2: 11;

      end;

      hence thesis by A9, GRAPH_1:def 14;

    end;

    theorem :: GRAPH_5:11

    

     Th9: (p ^ q) is oriented Chain of G implies p is oriented Chain of G & q is oriented Chain of G

    proof

      assume

       A1: (p ^ q) is oriented Chain of G;

      set r = (p ^ q);

      

       A2: ( len r) = (( len p) + ( len q)) by FINSEQ_1: 22;

       A3:

      now

        let n;

        assume that

         A4: 1 <= n and

         A5: n < ( len q);

        set m = (( len p) + n);

        n <= m by NAT_1: 11;

        then

         A6: 1 <= m by A4, XXREAL_0: 2;

        (n + 1) <= ( len q) by A5, NAT_1: 13;

        

        then

         A7: (q . (n + 1)) = (r . (( len p) + (n + 1))) by Lm2, NAT_1: 11

        .= (r . (m + 1));

        m < ( len r) by A2, A5, XREAL_1: 8;

        then (the Source of G . (r . (m + 1))) = (the Target of G . (r . m)) by A1, A6, GRAPH_1:def 15;

        hence (the Source of G . (q . (n + 1))) = (the Target of G . (q . n)) by A4, A5, A7, Lm2;

      end;

      now

        let n;

        assume that

         A8: 1 <= n and

         A9: n < ( len p);

        (n + 1) <= ( len p) by A9, NAT_1: 13;

        then

         A10: (p . (n + 1)) = (r . (n + 1)) by Lm1, NAT_1: 11;

        ( len p) <= ( len r) by A2, NAT_1: 11;

        then n < ( len r) by A9, XXREAL_0: 2;

        then (the Source of G . (r . (n + 1))) = (the Target of G . (r . n)) by A1, A8, GRAPH_1:def 15;

        hence (the Source of G . (p . (n + 1))) = (the Target of G . (p . n)) by A8, A9, A10, Lm1;

      end;

      hence thesis by A1, A3, Th8, GRAPH_1:def 15;

    end;

    theorem :: GRAPH_5:12

    

     Th10: for p,q be oriented Chain of G st (the Target of G . (p . ( len p))) = (the Source of G . (q . 1)) holds (p ^ q) is oriented Chain of G

    proof

      let p,q be oriented Chain of G;

      assume

       A1: (the Target of G . (p . ( len p))) = (the Source of G . (q . 1));

      per cases ;

        suppose

         A2: p = {} or q = {} ;

        hereby

          per cases by A2;

            suppose p = {} ;

            hence thesis by FINSEQ_1: 34;

          end;

            suppose q = {} ;

            hence thesis by FINSEQ_1: 34;

          end;

        end;

      end;

        suppose

         A3: not (p = {} or q = {} );

        consider vs2 be FinSequence of the carrier of G such that

         A4: vs2 is_oriented_vertex_seq_of q by GRAPH_4: 9;

        ( len vs2) = (( len q) + 1) by A4, GRAPH_4:def 5;

        then

         A5: ( len vs2) >= 1 by NAT_1: 12;

        ( len q) >= 1 by A3, FINSEQ_1: 20;

        then (q . 1) orientedly_joins ((vs2 /. 1),(vs2 /. (1 + 1))) by A4, GRAPH_4:def 5;

        

        then

         A6: (the Source of G . (q . 1)) = (vs2 /. 1) by GRAPH_4:def 1

        .= (vs2 . 1) by A5, FINSEQ_4: 15;

        consider vs1 be FinSequence of the carrier of G such that

         A7: vs1 is_oriented_vertex_seq_of p by GRAPH_4: 9;

        

         A8: ( len vs1) = (( len p) + 1) by A7, GRAPH_4:def 5;

        then

         A9: ( len vs1) >= 1 by NAT_1: 12;

        ( len p) >= 1 by A3, FINSEQ_1: 20;

        then (p . ( len p)) orientedly_joins ((vs1 /. ( len p)),(vs1 /. (( len p) + 1))) by A7, GRAPH_4:def 5;

        

        then (the Target of G . (p . ( len p))) = (vs1 /. ( len vs1)) by A8, GRAPH_4:def 1

        .= (vs1 . ( len vs1)) by A9, FINSEQ_4: 15;

        hence thesis by A1, A7, A4, A6, GRAPH_4: 14;

      end;

    end;

    begin

    theorem :: GRAPH_5:13

    

     Th11: {} is Simple oriented Chain of G

    proof

      set v = the Element of G;

      set vs = <*v*>;

       A1:

      now

        let n, m;

        assume that

         A2: 1 <= n & n < m & m <= ( len vs) and (vs . n) = (vs . m);

        assume not (n = 1 & m = ( len vs));

        ( len vs) = 1 by FINSEQ_1: 39;

        hence contradiction by A2, XXREAL_0: 2;

      end;

      vs is_oriented_vertex_seq_of {} qua FinSequence by GRAPH_4: 8;

      hence thesis by A1, GRAPH_1: 14, GRAPH_4:def 7;

    end;

    theorem :: GRAPH_5:14

    

     Th12: (p ^ q) is Simple oriented Chain of G implies p is Simple oriented Chain of G & q is Simple oriented Chain of G

    proof

      assume

       A1: (p ^ q) is Simple oriented Chain of G;

      set r = (p ^ q);

      per cases ;

        suppose

         A2: p = {} or q = {} ;

        hereby

          per cases by A2;

            suppose p = {} ;

            hence thesis by A1, Th11, FINSEQ_1: 34;

          end;

            suppose q = {} ;

            hence thesis by A1, Th11, FINSEQ_1: 34;

          end;

        end;

      end;

        suppose

         A3: not (p = {} or q = {} );

        consider vs be FinSequence of the carrier of G such that

         A4: vs is_oriented_vertex_seq_of r and

         A5: for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs) by A1, GRAPH_4:def 7;

        

         A6: ( len vs) = (( len r) + 1) by A4, GRAPH_4:def 5;

        

         A7: ( len r) = (( len p) + ( len q)) by FINSEQ_1: 22;

        then

         A8: ( len vs) = ((( len p) + 1) + ( len q)) by A6;

        then

        consider f1,f2 be FinSequence such that

         A9: ( len f1) = (( len p) + 1) and ( len f2) = ( len q) and

         A10: vs = (f1 ^ f2) by FINSEQ_2: 22;

        

         A11: ( len vs) = (( len p) + (( len q) + 1)) by A6, A7;

        then

        consider h1,h2 be FinSequence such that

         A12: ( len h1) = ( len p) and

         A13: ( len h2) = (( len q) + 1) and

         A14: vs = (h1 ^ h2) by FINSEQ_2: 22;

        reconsider f1 as FinSequence of the carrier of G by A10, FINSEQ_1: 36;

         A15:

        now

          let n, m;

          assume that

           A16: 1 <= n and

           A17: n < m and

           A18: m <= ( len f1) and

           A19: (f1 . n) = (f1 . m);

          n <= ( len f1) by A17, A18, XXREAL_0: 2;

          then

           A20: (f1 . n) = (vs . n) by A10, A16, Lm1;

          1 <= m by A16, A17, XXREAL_0: 2;

          then

           A21: (f1 . m) = (vs . m) by A10, A18, Lm1;

          assume not (n = 1 & m = ( len f1));

          (( len f1) + 0 ) < ( len vs) by A3, A8, A9, XREAL_1: 8;

          then m < ( len vs) by A18, XXREAL_0: 2;

          hence contradiction by A5, A16, A17, A19, A20, A21;

        end;

        reconsider h2 as FinSequence of the carrier of G by A14, FINSEQ_1: 36;

        now

          let n;

          assume that

           A22: 1 <= n and

           A23: n <= ( len q);

          set m = (( len p) + n);

          

           A24: m <= ( len r) by A7, A23, XREAL_1: 7;

          then 1 <= (m + 1) & (m + 1) <= ( len vs) by A6, NAT_1: 11, XREAL_1: 7;

          then

           A25: (m + 1) in ( dom vs) by FINSEQ_3: 25;

          

           A26: 1 <= (n + 1) by NAT_1: 11;

          (n + 1) <= ( len h2) by A13, A23, XREAL_1: 7;

          then (n + 1) in ( dom h2) by A26, FINSEQ_3: 25;

          

          then

           A27: (h2 /. (n + 1)) = (h2 . (n + 1)) by PARTFUN1:def 6

          .= (vs . (( len h1) + (n + 1))) by A13, A14, A23, A26, Lm2, XREAL_1: 7

          .= (vs /. (m + 1)) by A12, A25, PARTFUN1:def 6;

          n <= m by NAT_1: 11;

          then

           A28: 1 <= m by A22, XXREAL_0: 2;

          ( len r) <= ( len vs) by A6, NAT_1: 11;

          then m <= ( len vs) by A24, XXREAL_0: 2;

          then

           A29: m in ( dom vs) by A28, FINSEQ_3: 25;

          

           A30: (n + 0 ) <= ( len h2) by A13, A23, XREAL_1: 7;

          then n in ( dom h2) by A22, FINSEQ_3: 25;

          

          then

           A31: (h2 /. n) = (h2 . n) by PARTFUN1:def 6

          .= (vs . m) by A12, A14, A22, A30, Lm2

          .= (vs /. m) by A29, PARTFUN1:def 6;

          (r . m) orientedly_joins ((vs /. m),(vs /. (m + 1))) by A4, A24, A28, GRAPH_4:def 5;

          hence (q . n) orientedly_joins ((h2 /. n),(h2 /. (n + 1))) by A22, A23, A31, A27, Lm2;

        end;

        then

         A32: h2 is_oriented_vertex_seq_of q by A13, GRAPH_4:def 5;

        now

          let n;

          assume that

           A33: 1 <= n and

           A34: n <= ( len p);

          

           A35: 1 <= (n + 1) by NAT_1: 11;

          ( len p) <= ( len r) by A7, NAT_1: 11;

          then

           A36: n <= ( len r) by A34, XXREAL_0: 2;

          then (n + 1) <= ( len vs) by A6, XREAL_1: 7;

          then

           A37: (n + 1) in ( dom vs) by A35, FINSEQ_3: 25;

          ( len p) <= ( len vs) by A11, NAT_1: 11;

          then n <= ( len vs) by A34, XXREAL_0: 2;

          then

           A38: n in ( dom vs) by A33, FINSEQ_3: 25;

          

           A39: (n + 0 ) <= ( len f1) by A9, A34, XREAL_1: 7;

          then n in ( dom f1) by A33, FINSEQ_3: 25;

          

          then

           A40: (f1 /. n) = (f1 . n) by PARTFUN1:def 6

          .= (vs . n) by A10, A33, A39, Lm1

          .= (vs /. n) by A38, PARTFUN1:def 6;

          (n + 1) <= ( len f1) by A9, A34, XREAL_1: 7;

          then (n + 1) in ( dom f1) by A35, FINSEQ_3: 25;

          

          then

           A41: (f1 /. (n + 1)) = (f1 . (n + 1)) by PARTFUN1:def 6

          .= (vs . (n + 1)) by A9, A10, A34, A35, Lm1, XREAL_1: 7

          .= (vs /. (n + 1)) by A37, PARTFUN1:def 6;

          (r . n) orientedly_joins ((vs /. n),(vs /. (n + 1))) by A4, A33, A36, GRAPH_4:def 5;

          hence (p . n) orientedly_joins ((f1 /. n),(f1 /. (n + 1))) by A33, A34, A40, A41, Lm1;

        end;

        then f1 is_oriented_vertex_seq_of p by A9, GRAPH_4:def 5;

        hence p is Simple oriented Chain of G by A1, A15, Th9, GRAPH_4:def 7;

        now

          let n, m;

          assume that

           A42: 1 <= n and

           A43: n < m and

           A44: m <= ( len h2) and

           A45: (h2 . n) = (h2 . m);

          n <= ( len h2) by A43, A44, XXREAL_0: 2;

          then

           A46: (h2 . n) = (vs . (( len h1) + n)) by A14, A42, Lm2;

          assume not (n = 1 & m = ( len h2));

          

           A47: (( len h1) + m) <= ( len vs) by A11, A12, A13, A44, XREAL_1: 7;

          1 <= m by A42, A43, XXREAL_0: 2;

          then

           A48: (h2 . m) = (vs . (( len h1) + m)) by A14, A44, Lm2;

          ( 0 + 1) < (( len h1) + n) & (( len h1) + n) < (( len h1) + m) by A3, A12, A42, A43, XREAL_1: 8;

          hence contradiction by A5, A45, A46, A48, A47;

        end;

        hence thesis by A1, A32, Th9, GRAPH_4:def 7;

      end;

    end;

    theorem :: GRAPH_5:15

    

     Th13: ( len pe) = 1 implies pe is Simple oriented Chain of G

    proof

      set p = pe;

      set v1 = (the Source of G . (p . 1)), v2 = (the Target of G . (p . 1));

       A1:

      now

        let n;

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

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

        hence (p . n) in the carrier' of G by FINSEQ_2: 11;

      end;

      assume

       A2: ( len p) = 1;

      then 1 in ( dom p) by FINSEQ_3: 25;

      then

      reconsider v1, v2 as Element of G by FINSEQ_2: 11, FUNCT_2: 5;

      set vs = <*v1, v2*>;

      

       A3: ( len vs) = (( len p) + 1) by A2, FINSEQ_1: 44;

       A4:

      now

        let n;

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

        then

         A5: n = 1 by A2, XXREAL_0: 1;

        take v1, v2;

        thus v1 = (vs . n) & v2 = (vs . (n + 1)) by A5, FINSEQ_1: 44;

        thus (p . n) joins (v1,v2) by A5, GRAPH_1:def 12;

      end;

      

       A6: ( len vs) = 2 by FINSEQ_1: 44;

       A7:

      now

        let n, m;

        assume that

         A8: 1 <= n and

         A9: n < m and

         A10: m <= ( len vs) and (vs . n) = (vs . m);

        n < (1 + 1) by A6, A9, A10, XXREAL_0: 2;

        then n <= 1 by NAT_1: 13;

        hence n = 1 by A8, XXREAL_0: 1;

        1 < m by A8, A9, XXREAL_0: 2;

        then (1 + 1) < (m + 1) by XREAL_1: 8;

        then 2 <= m by NAT_1: 13;

        hence m = ( len vs) by A6, A10, XXREAL_0: 1;

      end;

       A11:

      now

        let n;

        assume that

         A12: 1 <= n and

         A13: n <= ( len vs);

        per cases ;

          suppose n < (1 + 1);

          then n <= 1 by NAT_1: 13;

          then n = 1 by A12, XXREAL_0: 1;

          then (vs . n) = v1 by FINSEQ_1: 44;

          hence (vs . n) in the carrier of G;

        end;

          suppose n >= 2;

          then n = 2 by A6, A13, XXREAL_0: 1;

          then (vs . n) = v2 by FINSEQ_1: 44;

          hence (vs . n) in the carrier of G;

        end;

      end;

      

       A14: for n st 1 <= n & n < ( len p) & (the Source of G . (p . (n + 1))) <> (the Target of G . (p . n)) holds contradiction by A2;

      now

        let n;

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

        then

         A15: n = 1 by A2, XXREAL_0: 1;

        (vs /. 1) = v1 & (vs /. (1 + 1)) = v2 by FINSEQ_4: 17;

        hence (p . n) orientedly_joins ((vs /. n),(vs /. (n + 1))) by A15, GRAPH_4:def 1;

      end;

      then vs is_oriented_vertex_seq_of p by A3, GRAPH_4:def 5;

      hence thesis by A3, A7, A1, A11, A4, A14, GRAPH_1:def 14, GRAPH_1:def 15, GRAPH_4:def 7;

    end;

    theorem :: GRAPH_5:16

    

     Th14: for p be Simple oriented Chain of G, q be FinSequence of the carrier' of G st ( len p) >= 1 & ( len q) = 1 & (the Source of G . (q . 1)) = (the Target of G . (p . ( len p))) & (the Source of G . (p . 1)) <> (the Target of G . (p . ( len p))) & not ex k st 1 <= k & k <= ( len p) & (the Target of G . (p . k)) = (the Target of G . (q . 1)) holds (p ^ q) is Simple oriented Chain of G

    proof

      let p be Simple oriented Chain of G, q be FinSequence of the carrier' of G;

      set FS = the Source of G, FT = the Target of G, v1 = (FS . (q . 1)), v2 = (FT . (q . 1)), vp = (the Target of G . (p . ( len p))), E = the carrier' of G, V = the carrier of G;

      assume that

       A1: ( len p) >= 1 and

       A2: ( len q) = 1 and

       A3: v1 = vp and

       A4: (FS . (p . 1)) <> vp and

       A5: not ex k st 1 <= k & k <= ( len p) & (FT . (p . k)) = v2;

      set lp = ( len p);

      1 in ( dom q) by A2, FINSEQ_3: 25;

      then

      reconsider v1, v2 as Element of V by FINSEQ_2: 11, FUNCT_2: 5;

      consider r be FinSequence of V such that

       A6: r is_oriented_vertex_seq_of p and

       A7: for n, m st 1 <= n & n < m & m <= ( len r) & (r . n) = (r . m) holds n = 1 & m = ( len r) by GRAPH_4:def 7;

      set pq = (p ^ q);

      set rv = (r ^ <*v2*>);

      

       A8: ( len r) = (( len p) + 1) by A6, GRAPH_4:def 5;

      

       A9: for n st 1 <= n & n <= ( len p) holds (p . n) joins ((r /. n),(r /. (n + 1))) by A6, GRAPH_4: 1, GRAPH_4:def 5;

       A10:

      now

        let n;

        assume that

         A11: 1 <= n and

         A12: n <= ( len pq);

        per cases ;

          suppose

           A13: n = ( len pq);

          set m = ( len p);

          take v1, v2;

          (p . m) orientedly_joins ((r /. m),(r /. (m + 1))) by A1, A6, GRAPH_4:def 5;

          then

           A14: vp = (r /. (m + 1)) by GRAPH_4:def 1;

          

           A15: n = ( len r) by A2, A8, A13, FINSEQ_1: 22;

          then n in ( dom r) by A11, FINSEQ_3: 25;

          

          hence v1 = (r . n) by A3, A8, A15, A14, PARTFUN1:def 6

          .= (rv . n) by A11, A15, Lm1;

          thus v2 = (rv . (n + 1)) by A15, FINSEQ_1: 42;

          (q . 1) joins (v1,v2) by GRAPH_1:def 12;

          hence (pq . n) joins (v1,v2) by A2, A8, A15, Lm2;

        end;

          suppose

           A16: n <> ( len pq);

          take x = (r /. n);

          take y = (r /. (n + 1));

          n < ( len pq) by A12, A16, XXREAL_0: 1;

          then

           A17: n < (( len p) + 1) by A2, FINSEQ_1: 22;

          then

           A18: (n + 1) <= ( len r) by A8, NAT_1: 13;

          n in ( dom r) by A8, A11, A17, FINSEQ_3: 25;

          

          hence x = (r . n) by PARTFUN1:def 6

          .= (rv . n) by A8, A11, A17, Lm1;

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

          then (n + 1) in ( dom r) by A18, FINSEQ_3: 25;

          

          hence y = (r . (n + 1)) by PARTFUN1:def 6

          .= (rv . (n + 1)) by A18, Lm1, NAT_1: 12;

          

           A19: n <= ( len p) by A17, NAT_1: 13;

          then (p . n) joins ((r /. n),(r /. (n + 1))) by A9, A11;

          hence (pq . n) joins (x,y) by A11, A19, Lm1;

        end;

      end;

       A20:

      now

        let n;

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

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

        then (pq . n) in ( rng pq) by FUNCT_1:def 3;

        then

         A21: (pq . n) in (( rng p) \/ ( rng q)) by FINSEQ_1: 31;

        ( rng p) c= E & ( rng q) c= E by FINSEQ_1:def 4;

        then (( rng p) \/ ( rng q)) c= E by XBOOLE_1: 8;

        hence (pq . n) in E by A21;

      end;

      

       A22: ( len rv) = (( len r) + 1) by FINSEQ_2: 16;

      then

       A23: ( len rv) = (( len pq) + 1) by A2, A8, FINSEQ_1: 22;

      (p . lp) orientedly_joins ((r /. lp),(r /. (lp + 1))) by A1, A6, GRAPH_4:def 5;

      then

       A24: vp = (r /. (lp + 1)) by GRAPH_4:def 1;

       A25:

      now

        let n, m;

        assume that

         A26: 1 <= n and

         A27: n < m and

         A28: m <= ( len rv) and

         A29: (rv . n) = (rv . m);

        assume

         A30: not (n = 1 & m = ( len rv));

        per cases ;

          suppose m < ( len rv);

          then

           A31: m <= ( len r) by A22, NAT_1: 13;

          

           A32: 1 <= m by A26, A27, XXREAL_0: 2;

          then

           A33: m in ( dom r) by A31, FINSEQ_3: 25;

          n < ( len r) by A27, A31, XXREAL_0: 2;

          

          then

           A34: (r . n) = (rv . n) by A26, Lm1

          .= (r . m) by A29, A31, A32, Lm1;

          then

           A35: m = ( len r) by A7, A26, A27, A31;

          

           A36: n = 1 by A7, A26, A27, A31, A34;

          then

           A37: 1 in ( dom r) by A27, A35, FINSEQ_3: 25;

          (p . 1) orientedly_joins ((r /. 1),(r /. (1 + 1))) by A1, A6, GRAPH_4:def 5;

          

          then (FS . (p . 1)) = (r /. 1) by GRAPH_4:def 1

          .= (r . m) by A34, A36, A37, PARTFUN1:def 6

          .= vp by A8, A24, A35, A33, PARTFUN1:def 6;

          hence contradiction by A4;

        end;

          suppose

           A38: m >= ( len rv);

          then m = ( len rv) by A28, XXREAL_0: 1;

          then

           A39: v2 = (rv . m) by A22, FINSEQ_1: 42;

          consider k be Nat such that

           A40: n = (k + 1) by A26, NAT_1: 6;

          reconsider k as Element of NAT by ORDINAL1:def 12;

          1 < n by A26, A28, A30, A38, XXREAL_0: 1;

          then

           A41: 1 <= k by A40, NAT_1: 13;

          (k + 1) < (( len r) + 1) by A22, A27, A28, A40, XXREAL_0: 2;

          then

           A42: (k + 1) <= ( len r) by NAT_1: 13;

          then

           A43: (k + 1) in ( dom r) by A26, A40, FINSEQ_3: 25;

          

           A44: k <= ( len p) by A8, A42, XREAL_1: 6;

          then (p . k) orientedly_joins ((r /. k),(r /. (k + 1))) by A6, A41, GRAPH_4:def 5;

          

          then (FT . (p . k)) = (r /. (k + 1)) by GRAPH_4:def 1

          .= (r . (k + 1)) by A43, PARTFUN1:def 6

          .= v2 by A26, A29, A39, A40, A42, Lm1;

          hence contradiction by A5, A41, A44;

        end;

      end;

       A45:

      now

        let n;

        assume that

         A46: 1 <= n and

         A47: n < ( len pq);

        per cases ;

          suppose

           A48: n < ( len p);

          then

           A49: (n + 1) <= ( len p) by NAT_1: 13;

          (FS . (p . (n + 1))) = (FT . (p . n)) & (p . n) = (pq . n) by A46, A48, Lm1, GRAPH_1:def 15;

          hence (FS . (pq . (n + 1))) = (FT . (pq . n)) by A49, Lm1, NAT_1: 12;

        end;

          suppose

           A50: n >= ( len p);

          n < (( len p) + 1) by A2, A47, FINSEQ_1: 22;

          then n <= ( len p) by NAT_1: 13;

          then

           A51: n = ( len p) by A50, XXREAL_0: 1;

          then (pq . n) = (p . ( len p)) by A1, Lm1;

          hence (FS . (pq . (n + 1))) = (FT . (pq . n)) by A2, A3, A51, Lm2;

        end;

      end;

       A52:

      now

        let n;

        assume that

         A53: 1 <= n and

         A54: n <= ( len rv);

        per cases ;

          suppose n = ( len rv);

          then (rv . n) = v2 by A22, FINSEQ_1: 42;

          hence (rv . n) in V;

        end;

          suppose n <> ( len rv);

          then n < ( len rv) by A54, XXREAL_0: 1;

          then

           A55: n <= ( len r) by A22, NAT_1: 13;

          then n in ( dom r) by A53, FINSEQ_3: 25;

          then (r . n) in V by FINSEQ_2: 11;

          hence (rv . n) in V by A53, A55, Lm1;

        end;

      end;

      now

        

         A56: ( dom r) c= ( dom rv) by FINSEQ_1: 26;

        let n;

        assume that

         A57: 1 <= n and

         A58: n <= ( len pq);

        per cases ;

          suppose

           A59: n <= ( len p);

          then

           A60: (n + 1) <= ( len r) by A8, XREAL_1: 7;

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

          then

           A61: (n + 1) in ( dom r) by A60, FINSEQ_3: 25;

          

          then

           A62: (r /. (n + 1)) = (r . (n + 1)) by PARTFUN1:def 6

          .= (rv . (n + 1)) by A60, Lm1, NAT_1: 12

          .= (rv /. (n + 1)) by A56, A61, PARTFUN1:def 6;

          

           A63: (p . n) orientedly_joins ((r /. n),(r /. (n + 1))) by A6, A57, A59, GRAPH_4:def 5;

          

           A64: n <= ( len r) by A8, A59, NAT_1: 12;

          then

           A65: n in ( dom r) by A57, FINSEQ_3: 25;

          

          then (r /. n) = (r . n) by PARTFUN1:def 6

          .= (rv . n) by A57, A64, Lm1

          .= (rv /. n) by A56, A65, PARTFUN1:def 6;

          hence (pq . n) orientedly_joins ((rv /. n),(rv /. (n + 1))) by A57, A59, A63, A62, Lm1;

        end;

          suppose

           A66: n > ( len p);

          

           A67: (( len p) + 1) >= n by A2, A58, FINSEQ_1: 22;

          (( len p) + 1) <= n by A66, NAT_1: 13;

          then

           A68: n = ( len r) by A8, A67, XXREAL_0: 1;

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

          then

           A69: (n + 1) in ( dom rv) by A22, A68, FINSEQ_3: 25;

          

           A70: v2 = (rv . (n + 1)) by A68, FINSEQ_1: 42

          .= (rv /. (n + 1)) by A69, PARTFUN1:def 6;

          

           A71: (q . 1) orientedly_joins (v1,v2) by GRAPH_4:def 1;

          

           A72: n in ( dom r) by A8, A57, A67, FINSEQ_3: 25;

          

          then v1 = (r . n) by A3, A8, A24, A68, PARTFUN1:def 6

          .= (rv . n) by A8, A57, A67, Lm1

          .= (rv /. n) by A56, A72, PARTFUN1:def 6;

          hence (pq . n) orientedly_joins ((rv /. n),(rv /. (n + 1))) by A2, A8, A68, A70, A71, Lm2;

        end;

      end;

      then rv is_oriented_vertex_seq_of pq by A23, GRAPH_4:def 5;

      hence thesis by A20, A23, A52, A10, A45, A25, GRAPH_1:def 14, GRAPH_1:def 15, GRAPH_4:def 7;

    end;

    theorem :: GRAPH_5:17

    

     Th15: for p be Simple oriented Chain of G holds p is one-to-one

    proof

      let p be Simple oriented Chain of G;

      set VV = the carrier of G;

      consider vs be FinSequence of VV such that

       A1: vs is_oriented_vertex_seq_of p and

       A2: for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs) by GRAPH_4:def 7;

      

       A3: ( len vs) = (( len p) + 1) by A1, GRAPH_4:def 5;

      now

        let n, m;

        assume that

         A4: 1 <= n and

         A5: n < m and

         A6: m <= ( len p);

        

         A7: 1 <= m by A4, A5, XXREAL_0: 2;

        then

         A8: (p . m) orientedly_joins ((vs /. m),(vs /. (m + 1))) by A1, A6, GRAPH_4:def 5;

        assume

         A9: (p . n) = (p . m);

        

         A10: n <= ( len p) by A5, A6, XXREAL_0: 2;

        then (p . n) orientedly_joins ((vs /. n),(vs /. (n + 1))) by A1, A4, GRAPH_4:def 5;

        

        then

         A11: (vs /. n) = (the Source of G . (p . m)) by A9, GRAPH_4:def 1

        .= (vs /. m) by A8, GRAPH_4:def 1;

        

         A12: ( len p) < ( len vs) by A3, XREAL_1: 29;

        then n <= ( len vs) by A10, XXREAL_0: 2;

        then n in ( dom vs) by A4, FINSEQ_3: 25;

        then

         A13: (vs . n) = (vs /. n) by PARTFUN1:def 6;

        

         A14: m <= ( len vs) by A6, A12, XXREAL_0: 2;

        then m in ( dom vs) by A7, FINSEQ_3: 25;

        then (vs . m) = (vs . n) by A11, A13, PARTFUN1:def 6;

        then m = ( len vs) by A2, A4, A5, A14;

        hence contradiction by A3, A6, XREAL_1: 29;

      end;

      hence thesis by Th4;

    end;

    begin

    definition

      let G be Graph, e be Element of the carrier' of G;

      :: GRAPH_5:def1

      func vertices e -> set equals {(the Source of G . e), (the Target of G . e)};

      coherence ;

    end

    definition

      let G, pe;

      :: GRAPH_5:def2

      func vertices pe -> Subset of the carrier of G equals { v where v be Vertex of G : ex i st i in ( dom pe) & v in ( vertices (pe /. i)) };

      coherence

      proof

        set VT = { v where v be Vertex of G : ex i st i in ( dom pe) & v in ( vertices (pe /. i)) };

        VT c= the carrier of G

        proof

          let x be object;

          assume x in VT;

          then ex v be Vertex of G st x = v & ex i st i in ( dom pe) & v in ( vertices (pe /. i));

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: GRAPH_5:18

    

     Th16: for p be Simple oriented Chain of G st p = (pe ^ qe) & ( len pe) >= 1 & ( len qe) >= 1 & (the Source of G . (p . 1)) <> (the Target of G . (p . ( len p))) holds not (the Source of G . (p . 1)) in ( vertices qe) & not (the Target of G . (p . ( len p))) in ( vertices pe)

    proof

      let p be Simple oriented Chain of G;

      set FT = the Target of G, FS = the Source of G;

      assume that

       A1: p = (pe ^ qe) and

       A2: ( len pe) >= 1 and

       A3: ( len qe) >= 1 and

       A4: (FS . (p . 1)) <> (FT . (p . ( len p)));

      consider vs be FinSequence of the carrier of G such that

       A5: vs is_oriented_vertex_seq_of p and

       A6: for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs) by GRAPH_4:def 7;

      

       A7: ( len vs) = (( len p) + 1) by A5, GRAPH_4:def 5;

      then

       A8: 1 <= ( len vs) by NAT_1: 12;

      

       A9: ( len p) = (( len pe) + ( len qe)) by A1, FINSEQ_1: 22;

      then

       A10: ( len p) >= 1 by A2, NAT_1: 12;

      then (p . 1) orientedly_joins ((vs /. 1),(vs /. (1 + 1))) by A5, GRAPH_4:def 5;

      

      then

       A11: (FS . (p . 1)) = (vs /. 1) by GRAPH_4:def 1

      .= (vs . 1) by A8, FINSEQ_4: 15;

      (p . ( len p)) orientedly_joins ((vs /. ( len p)),(vs /. (( len p) + 1))) by A5, A10, GRAPH_4:def 5;

      

      then

       A12: (FT . (p . ( len p))) = (vs /. (( len p) + 1)) by GRAPH_4:def 1

      .= (vs . ( len vs)) by A7, A8, FINSEQ_4: 15;

      hereby

        assume (FS . (p . 1)) in ( vertices qe);

        then

        consider x be Vertex of G such that

         A13: (FS . (p . 1)) = x and

         A14: ex i st i in ( dom qe) & x in ( vertices (qe /. i));

        consider i such that

         A15: i in ( dom qe) and

         A16: x in ( vertices (qe /. i)) by A14;

        set k = (( len pe) + i);

        

         A17: (qe /. i) = (qe . i) by A15, PARTFUN1:def 6

        .= (p . k) by A1, A15, FINSEQ_1:def 7;

        1 <= i by A15, FINSEQ_3: 25;

        then

         A18: 1 < (i + 1) by NAT_1: 13;

        i <= ( len qe) by A15, FINSEQ_3: 25;

        then

         A19: k <= ( len p) by A9, XREAL_1: 7;

        then

         A20: k <= ( len vs) by A7, NAT_1: 13;

        (1 + i) <= k by A2, XREAL_1: 7;

        then

         A21: 1 < k by A18, XXREAL_0: 2;

        then

         A22: (p . k) orientedly_joins ((vs /. k),(vs /. (k + 1))) by A5, A19, GRAPH_4:def 5;

        per cases by A16, A17, TARSKI:def 2;

          suppose

           A23: x = (FS . (p . k));

          (FS . (p . k)) = (vs /. k) by A22, GRAPH_4:def 1

          .= (vs . k) by A21, A20, FINSEQ_4: 15;

          hence contradiction by A4, A6, A11, A12, A13, A21, A20, A23;

        end;

          suppose

           A24: x = (FT . (p . k));

          

           A25: 1 < (k + 1) by A21, NAT_1: 13;

          

           A26: (k + 1) <= ( len vs) by A7, A19, XREAL_1: 7;

          (FT . (p . k)) = (vs /. (k + 1)) by A22, GRAPH_4:def 1

          .= (vs . (k + 1)) by A26, FINSEQ_4: 15, NAT_1: 12;

          hence contradiction by A4, A6, A11, A12, A13, A24, A26, A25;

        end;

      end;

      hereby

        assume (FT . (p . ( len p))) in ( vertices pe);

        then

        consider x be Vertex of G such that

         A27: (FT . (p . ( len p))) = x and

         A28: ex i st i in ( dom pe) & x in ( vertices (pe /. i));

        consider i such that

         A29: i in ( dom pe) and

         A30: x in ( vertices (pe /. i)) by A28;

        

         A31: (pe /. i) = (pe . i) by A29, PARTFUN1:def 6

        .= (p . i) by A1, A29, FINSEQ_1:def 7;

        

         A32: i <= ( len pe) by A29, FINSEQ_3: 25;

        then

         A33: i <= ( len p) by A9, NAT_1: 12;

        then

         A34: i < ( len vs) by A7, NAT_1: 13;

        

         A35: 1 <= i by A29, FINSEQ_3: 25;

        then

         A36: (p . i) orientedly_joins ((vs /. i),(vs /. (i + 1))) by A5, A33, GRAPH_4:def 5;

        per cases by A30, A31, TARSKI:def 2;

          suppose

           A37: x = (FS . (p . i));

          (FS . (p . i)) = (vs /. i) by A36, GRAPH_4:def 1

          .= (vs . i) by A35, A34, FINSEQ_4: 15;

          hence contradiction by A4, A6, A12, A27, A35, A34, A37;

        end;

          suppose

           A38: x = (FT . (p . i));

          

           A39: (i + 1) <= ( len vs) by A7, A33, XREAL_1: 7;

          (( len pe) + 1) <= (( len pe) + ( len qe)) & (i + 1) <= (( len pe) + 1) by A3, A32, XREAL_1: 7;

          then (i + 1) <= ( len p) by A9, XXREAL_0: 2;

          then

           A40: 1 <= (i + 1) & (i + 1) < ( len vs) by A7, NAT_1: 12, NAT_1: 13;

          (FT . (p . i)) = (vs /. (i + 1)) by A36, GRAPH_4:def 1

          .= (vs . (i + 1)) by A39, FINSEQ_4: 15, NAT_1: 12;

          hence contradiction by A4, A6, A11, A12, A27, A38, A40;

        end;

      end;

    end;

    theorem :: GRAPH_5:19

    

     Th17: ( vertices pe) c= V iff for i be Nat st i in ( dom pe) holds ( vertices (pe /. i)) c= V

    proof

      set FS = the Source of G, FT = the Target of G;

      hereby

        assume

         A1: ( vertices pe) c= V;

        hereby

          let i be Nat;

          assume

           A2: i in ( dom pe);

          then

           A3: 1 <= i & i <= ( len pe) by FINSEQ_3: 25;

          thus ( vertices (pe /. i)) c= V

          proof

            let x be object;

            assume

             A4: x in ( vertices (pe /. i));

            then x = (FS . (pe /. i)) or x = (FT . (pe /. i)) by TARSKI:def 2;

            then x = (FS . (pe . i)) or x = (FT . (pe . i)) by A3, FINSEQ_4: 15;

            then

            reconsider y = x as Vertex of G by A2, FINSEQ_2: 11, FUNCT_2: 5;

            y in { v where v be Vertex of G : ex i st i in ( dom pe) & v in ( vertices (pe /. i)) } by A2, A4;

            hence thesis by A1;

          end;

        end;

      end;

      assume

       A5: for i be Nat st i in ( dom pe) holds ( vertices (pe /. i)) c= V;

      let x be object;

      assume x in ( vertices pe);

      then

      consider y be Vertex of G such that

       A6: y = x and

       A7: ex i st i in ( dom pe) & y in ( vertices (pe /. i));

      consider i such that

       A8: i in ( dom pe) and

       A9: y in ( vertices (pe /. i)) by A7;

      ( vertices (pe /. i)) c= V by A5, A8;

      hence thesis by A6, A9;

    end;

    theorem :: GRAPH_5:20

    

     Th18: not ( vertices pe) c= V implies ex i be Element of NAT , q,r be FinSequence of the carrier' of G st (i + 1) <= ( len pe) & not ( vertices (pe /. (i + 1))) c= V & ( len q) = i & pe = (q ^ r) & ( vertices q) c= V

    proof

      defpred P[ Nat] means $1 in ( dom pe) & not ( vertices (pe /. $1)) c= V;

      assume not ( vertices pe) c= V;

      then

       A1: ex i be Nat st P[i] by Th17;

      consider k be Nat such that

       A2: P[k] & for n be Nat st P[n] holds k <= n from NAT_1:sch 5( A1);

      k <= ( len pe) by A2, FINSEQ_3: 25;

      then

      consider j be Nat such that

       A3: ( len pe) = (k + j) by NAT_1: 10;

      reconsider j as Element of NAT by ORDINAL1:def 12;

      1 <= k by A2, FINSEQ_3: 25;

      then

      consider i be Nat such that

       A4: k = (1 + i) by NAT_1: 10;

      reconsider i as Element of NAT by ORDINAL1:def 12;

      ( len pe) = (i + (1 + j)) by A4, A3;

      then

      consider q,r be FinSequence such that

       A5: ( len q) = i and ( len r) = (1 + j) and

       A6: pe = (q ^ r) by FINSEQ_2: 22;

      reconsider q, r as FinSequence of the carrier' of G by A6, FINSEQ_1: 36;

      take i, q, r;

      thus (i + 1) <= ( len pe) & not ( vertices (pe /. (i + 1))) c= V by A2, A4, FINSEQ_3: 25;

      thus ( len q) = i & pe = (q ^ r) by A5, A6;

      now

        let m be Nat;

        assume

         A7: m in ( dom q);

        then

         A8: m <= ( len q) by FINSEQ_3: 25;

        

         A9: ( dom q) c= ( dom pe) by A6, FINSEQ_1: 26;

        assume

         A10: not ( vertices (q /. m)) c= V;

        (q /. m) = (q . m) by A7, PARTFUN1:def 6

        .= (pe . m) by A6, A7, FINSEQ_1:def 7

        .= (pe /. m) by A7, A9, PARTFUN1:def 6;

        then k <= m by A2, A7, A10, A9;

        hence contradiction by A4, A5, A8, NAT_1: 13;

      end;

      hence thesis by Th17;

    end;

    theorem :: GRAPH_5:21

    

     Th19: ( rng qe) c= ( rng pe) implies ( vertices qe) c= ( vertices pe)

    proof

      assume

       A1: ( rng qe) c= ( rng pe);

      let x be object;

      assume x in ( vertices qe);

      then

      consider v be Vertex of G such that

       A2: x = v and

       A3: ex i st i in ( dom qe) & v in ( vertices (qe /. i));

      consider i such that

       A4: i in ( dom qe) and

       A5: v in ( vertices (qe /. i)) by A3;

      (qe . i) in ( rng qe) by A4, FUNCT_1:def 3;

      then

      consider j be object such that

       A6: j in ( dom pe) and

       A7: (qe . i) = (pe . j) by A1, FUNCT_1:def 3;

      reconsider j as Element of NAT by A6;

      (qe /. i) = (qe . i) by A4, PARTFUN1:def 6;

      then (pe /. j) = (qe /. i) by A6, A7, PARTFUN1:def 6;

      hence thesis by A2, A5, A6;

    end;

    theorem :: GRAPH_5:22

    

     Th20: ( rng qe) c= ( rng pe) & (( vertices pe) \ X) c= V implies (( vertices qe) \ X) c= V

    proof

      assume that

       A1: ( rng qe) c= ( rng pe) and

       A2: (( vertices pe) \ X) c= V;

      ( vertices qe) c= ( vertices pe) by A1, Th19;

      then (( vertices qe) \ X) c= (( vertices pe) \ X) by XBOOLE_1: 35;

      hence thesis by A2;

    end;

    theorem :: GRAPH_5:23

    

     Th21: (( vertices (pe ^ qe)) \ X) c= V implies (( vertices pe) \ X) c= V & (( vertices qe) \ X) c= V

    proof

      

       A1: ( rng pe) c= ( rng (pe ^ qe)) & ( rng qe) c= ( rng (pe ^ qe)) by FINSEQ_1: 29, FINSEQ_1: 30;

      assume (( vertices (pe ^ qe)) \ X) c= V;

      hence thesis by A1, Th20;

    end;

    reserve v,v1,v2,v3 for Element of G;

    theorem :: GRAPH_5:24

    

     Th22: i in ( dom pe) & (v = (the Source of G . (pe . i)) or v = (the Target of G . (pe . i))) implies v in ( vertices pe)

    proof

      set FS = the Source of G, FT = the Target of G;

      assume that

       A1: i in ( dom pe) and

       A2: v = (FS . (pe . i)) or v = (FT . (pe . i));

      v = (FS . (pe /. i)) or v = (FT . (pe /. i)) by A1, A2, PARTFUN1:def 6;

      then v in ( vertices (pe /. i)) by TARSKI:def 2;

      hence thesis by A1;

    end;

    theorem :: GRAPH_5:25

    

     Th23: ( len pe) = 1 implies ( vertices pe) = ( vertices (pe /. 1))

    proof

      set FS = the Source of G, FT = the Target of G;

      assume

       A1: ( len pe) = 1;

      then

       A2: 1 in ( dom pe) by FINSEQ_3: 25;

      now

        let x be object;

        hereby

          assume x in ( vertices pe);

          then

          consider y be Vertex of G such that

           A3: y = x and

           A4: ex i st i in ( dom pe) & y in ( vertices (pe /. i));

          consider i such that

           A5: i in ( dom pe) and

           A6: y in ( vertices (pe /. i)) by A4;

          1 <= i & i <= ( len pe) by A5, FINSEQ_3: 25;

          hence x in ( vertices (pe /. 1)) by A1, A3, A6, XXREAL_0: 1;

        end;

        assume

         A7: x in ( vertices (pe /. 1));

        then x = (FS . (pe /. 1)) or x = (FT . (pe /. 1)) by TARSKI:def 2;

        then x = (FS . (pe . 1)) or x = (FT . (pe . 1)) by A1, FINSEQ_4: 15;

        then

        reconsider y = x as Vertex of G by A2, FINSEQ_2: 11, FUNCT_2: 5;

        y in { v where v be Vertex of G : ex i st i in ( dom pe) & v in ( vertices (pe /. i)) } by A2, A7;

        hence x in ( vertices pe);

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GRAPH_5:26

    

     Th24: ( vertices pe) c= ( vertices (pe ^ qe)) & ( vertices qe) c= ( vertices (pe ^ qe))

    proof

      ( rng pe) c= ( rng (pe ^ qe)) & ( rng qe) c= ( rng (pe ^ qe)) by FINSEQ_1: 29, FINSEQ_1: 30;

      hence thesis by Th19;

    end;

    reserve p,q for oriented Chain of G;

    theorem :: GRAPH_5:27

    

     Th25: p = (q ^ pe) & ( len q) >= 1 & ( len pe) = 1 implies ( vertices p) = (( vertices q) \/ {(the Target of G . (pe . 1))})

    proof

      assume that

       A1: p = (q ^ pe) and

       A2: ( len q) >= 1 and

       A3: ( len pe) = 1;

      set FS = the Source of G, FT = the Target of G, V3 = {(FT . (pe . 1))};

      

       A4: ( len p) = (( len q) + 1) by A1, A3, FINSEQ_1: 22;

      now

        let x be object;

        hereby

          assume x in ( vertices p);

          then

          consider y be Vertex of G such that

           A5: y = x and

           A6: ex i st i in ( dom p) & y in ( vertices (p /. i));

          consider i such that

           A7: i in ( dom p) and

           A8: y in ( vertices (p /. i)) by A6;

          

           A9: 1 <= i by A7, FINSEQ_3: 25;

          

           A10: i <= ( len p) by A7, FINSEQ_3: 25;

          per cases ;

            suppose

             A11: i <= ( len q);

            then

             A12: i in ( dom q) by A9, FINSEQ_3: 25;

            (p /. i) = (p . i) by A9, A10, FINSEQ_4: 15

            .= (q . i) by A1, A9, A11, Lm1

            .= (q /. i) by A9, A11, FINSEQ_4: 15;

            then y in { v where v be Vertex of G : ex j st j in ( dom q) & v in ( vertices (q /. j)) } by A8, A12;

            hence x in (( vertices q) \/ V3) by A5, XBOOLE_0:def 3;

          end;

            suppose

             A13: i > ( len q);

            reconsider z = y as Vertex of G;

            i >= (( len q) + 1) by A13, NAT_1: 13;

            then

             A14: i = (( len q) + 1) by A4, A10, XXREAL_0: 1;

            

             A15: y = (FS . (p /. i)) or y = (FT . (p /. i)) by A8, TARSKI:def 2;

            hereby

              per cases by A9, A10, A15, FINSEQ_4: 15;

                suppose

                 A16: z = (FS . (p . i));

                ( len q) < ( len p) by A4, NAT_1: 13;

                

                then z = (FT . (p . ( len q))) by A2, A14, A16, GRAPH_1:def 15

                .= (FT . (q . ( len q))) by A1, A2, Lm1

                .= (FT . (q /. ( len q))) by A2, FINSEQ_4: 15;

                then

                 A17: z in ( vertices (q /. ( len q))) by TARSKI:def 2;

                ( len q) in ( dom q) by A2, FINSEQ_3: 25;

                then z in { v where v be Vertex of G : ex j st j in ( dom q) & v in ( vertices (q /. j)) } by A17;

                hence x in (( vertices q) \/ V3) by A5, XBOOLE_0:def 3;

              end;

                suppose z = (FT . (p . i));

                then z = (FT . (pe . 1)) by A1, A3, A14, Lm2;

                then z in V3 by TARSKI:def 1;

                hence x in (( vertices q) \/ V3) by A5, XBOOLE_0:def 3;

              end;

            end;

          end;

        end;

        assume

         A18: x in (( vertices q) \/ V3);

        per cases by A18, XBOOLE_0:def 3;

          suppose

           A19: x in ( vertices q);

          ( vertices q) c= ( vertices p) by A1, Th24;

          hence x in ( vertices p) by A19;

        end;

          suppose

           A20: x in V3;

          1 in ( dom pe) by A3, FINSEQ_3: 25;

          then

          reconsider y = (FT . (pe . 1)) as Vertex of G by FINSEQ_2: 11, FUNCT_2: 5;

          

           A21: 1 <= ( len p) by A4, NAT_1: 12;

          then

           A22: ( len p) in ( dom p) by FINSEQ_3: 25;

          y = (FT . (p . ( len p))) by A1, A3, A4, Lm2

          .= (FT . (p /. ( len p))) by A21, FINSEQ_4: 15;

          then

           A23: y in ( vertices (p /. ( len p))) by TARSKI:def 2;

          x = (FT . (pe . 1)) by A20, TARSKI:def 1;

          hence x in ( vertices p) by A23, A22;

        end;

      end;

      hence thesis by TARSKI: 2;

    end;

    theorem :: GRAPH_5:28

    

     Th26: v <> (the Source of G . (p . 1)) & v in ( vertices p) implies ex i st 1 <= i & i <= ( len p) & v = (the Target of G . (p . i))

    proof

      set FT = the Target of G, FS = the Source of G;

      assume that

       A1: v <> (FS . (p . 1)) and

       A2: v in ( vertices p);

      consider u be Vertex of G such that

       A3: v = u and

       A4: ex i st i in ( dom p) & u in ( vertices (p /. i)) by A2;

      consider i such that

       A5: i in ( dom p) and

       A6: u in ( vertices (p /. i)) by A4;

      

       A7: u = (FS . (p /. i)) or u = (FT . (p /. i)) by A6, TARSKI:def 2;

      

       A8: 1 <= i by A5, FINSEQ_3: 25;

      

       A9: i <= ( len p) by A5, FINSEQ_3: 25;

      per cases by A3, A7, A8, A9, FINSEQ_4: 15;

        suppose

         A10: v = (FT . (p . i));

        take i;

        thus thesis by A5, A10, FINSEQ_3: 25;

      end;

        suppose

         A11: v = (FS . (p . i));

        consider j be Nat such that

         A12: i = (1 + j) by A8, NAT_1: 10;

        reconsider j as Element of NAT by ORDINAL1:def 12;

        

         A13: j < ( len p) by A9, A12, NAT_1: 13;

        take j;

        i > 1 by A1, A8, A11, XXREAL_0: 1;

        then j >= 1 by A12, NAT_1: 13;

        hence thesis by A11, A12, A13, GRAPH_1:def 15;

      end;

    end;

    begin

    definition

      let G, p, v1, v2;

      :: GRAPH_5:def3

      pred p is_orientedpath_of v1,v2 means p <> {} & (the Source of G . (p . 1)) = v1 & (the Target of G . (p . ( len p))) = v2;

    end

    definition

      let G, v1, v2, p, V;

      :: GRAPH_5:def4

      pred p is_orientedpath_of v1,v2,V means p is_orientedpath_of (v1,v2) & (( vertices p) \ {v2}) c= V;

    end

    definition

      let G be Graph, v1,v2 be Element of G;

      :: GRAPH_5:def5

      func OrientedPaths (v1,v2) -> Subset of (the carrier' of G * ) equals { p where p be oriented Chain of G : p is_orientedpath_of (v1,v2) };

      coherence

      proof

        set PT = { p where p be oriented Chain of G : p is_orientedpath_of (v1,v2) };

        PT c= (the carrier' of G * )

        proof

          let e be object;

          assume e in PT;

          then ex p be oriented Chain of G st e = p & p is_orientedpath_of (v1,v2);

          hence thesis by FINSEQ_1:def 11;

        end;

        hence thesis;

      end;

    end

    theorem :: GRAPH_5:29

    

     Th27: p is_orientedpath_of (v1,v2) implies v1 in ( vertices p) & v2 in ( vertices p)

    proof

      assume

       A1: p is_orientedpath_of (v1,v2);

      then p <> {} ;

      then 1 <= ( len p) by FINSEQ_1: 20;

      then

       A2: 1 in ( dom p) & ( len p) in ( dom p) by FINSEQ_3: 25;

      (the Source of G . (p . 1)) = v1 & (the Target of G . (p . ( len p))) = v2 by A1;

      hence thesis by A2, Th22;

    end;

    theorem :: GRAPH_5:30

    x in ( OrientedPaths (v1,v2)) iff ex p st p = x & p is_orientedpath_of (v1,v2);

    theorem :: GRAPH_5:31

    

     Th29: p is_orientedpath_of (v1,v2,V) & v1 <> v2 implies v1 in V

    proof

      assume that

       A1: p is_orientedpath_of (v1,v2,V) and

       A2: v1 <> v2;

      p is_orientedpath_of (v1,v2) by A1;

      then

       A3: v1 in ( vertices p) by Th27;

       not v1 in {v2} by A2, TARSKI:def 1;

      then

       A4: v1 in (( vertices p) \ {v2}) by A3, XBOOLE_0:def 5;

      (( vertices p) \ {v2}) c= V by A1;

      hence thesis by A4;

    end;

    theorem :: GRAPH_5:32

    

     Th30: p is_orientedpath_of (v1,v2,V) & V c= U implies p is_orientedpath_of (v1,v2,U)

    proof

      assume that

       A1: p is_orientedpath_of (v1,v2,V) and

       A2: V c= U;

      (( vertices p) \ {v2}) c= V by A1;

      then

       A3: (( vertices p) \ {v2}) c= U by A2;

      p is_orientedpath_of (v1,v2) by A1;

      hence thesis by A3;

    end;

    theorem :: GRAPH_5:33

    

     Th31: ( len p) >= 1 & p is_orientedpath_of (v1,v2) & (pe . 1) orientedly_joins (v2,v3) & ( len pe) = 1 implies ex q st q = (p ^ pe) & q is_orientedpath_of (v1,v3)

    proof

      assume that

       A1: ( len p) >= 1 and

       A2: p is_orientedpath_of (v1,v2) and

       A3: (pe . 1) orientedly_joins (v2,v3) and

       A4: ( len pe) = 1;

      set FT = the Target of G, FS = the Source of G;

      

       A5: pe is oriented Chain of G by A4, Th13;

      (FT . (p . ( len p))) = v2 & (FS . (pe . 1)) = v2 by A2, A3, GRAPH_4:def 1;

      then

      reconsider q = (p ^ pe) as oriented Chain of G by A5, Th10;

      

       A6: ( len q) = (( len p) + 1) by A4, FINSEQ_1: 22;

      (FT . (pe . 1)) = v3 by A3, GRAPH_4:def 1;

      then

       A7: (FT . (q . ( len q))) = v3 by A4, A6, Lm2;

      (FS . (p . 1)) = v1 by A2;

      then

       A8: (FS . (q . 1)) = v1 by A1, Lm1;

      take q;

      q <> {} by A6;

      hence thesis by A8, A7;

    end;

    theorem :: GRAPH_5:34

    

     Th32: q = (p ^ pe) & ( len p) >= 1 & ( len pe) = 1 & p is_orientedpath_of (v1,v2,V) & (pe . 1) orientedly_joins (v2,v3) implies q is_orientedpath_of (v1,v3,(V \/ {v2}))

    proof

      assume that

       A1: q = (p ^ pe) and

       A2: ( len p) >= 1 & ( len pe) = 1 and

       A3: p is_orientedpath_of (v1,v2,V) and

       A4: (pe . 1) orientedly_joins (v2,v3);

      p is_orientedpath_of (v1,v2) by A3;

      then

       A5: ex r be oriented Chain of G st r = (p ^ pe) & r is_orientedpath_of (v1,v3) by A2, A4, Th31;

      set FT = the Target of G;

      (FT . (pe . 1)) = v3 by A4, GRAPH_4:def 1;

      

      then (( vertices q) \ {v3}) = ((( vertices p) \/ {v3}) \ {v3}) by A1, A2, Th25

      .= (( vertices p) \ {v3}) by XBOOLE_1: 40;

      then

       A6: (( vertices q) \ {v3}) c= ( vertices p) by XBOOLE_1: 36;

      (( vertices p) \ {v2}) c= V by A3;

      then ( vertices p) c= (V \/ {v2}) by XBOOLE_1: 44;

      then (( vertices q) \ {v3}) c= (V \/ {v2}) by A6;

      hence thesis by A1, A5;

    end;

    begin

    definition

      let G be Graph, p be oriented Chain of G, v1,v2 be Element of G;

      :: GRAPH_5:def6

      pred p is_acyclicpath_of v1,v2 means p is Simple & p is_orientedpath_of (v1,v2);

    end

    definition

      let G be Graph, p be oriented Chain of G, v1,v2 be Element of G, V be set;

      :: GRAPH_5:def7

      pred p is_acyclicpath_of v1,v2,V means p is Simple & p is_orientedpath_of (v1,v2,V);

    end

    definition

      let G be Graph, v1,v2 be Element of G;

      :: GRAPH_5:def8

      func AcyclicPaths (v1,v2) -> Subset of (the carrier' of G * ) equals { p where p be Simple oriented Chain of G : p is_acyclicpath_of (v1,v2) };

      coherence

      proof

        set PT = { p where p be Simple oriented Chain of G : p is_acyclicpath_of (v1,v2) };

        PT c= (the carrier' of G * )

        proof

          let e be object;

          assume e in PT;

          then ex p be Simple oriented Chain of G st (e = p) & (p is_acyclicpath_of (v1,v2));

          hence thesis by FINSEQ_1:def 11;

        end;

        hence thesis;

      end;

    end

    definition

      let G be Graph, v1,v2 be Element of G, V be set;

      :: GRAPH_5:def9

      func AcyclicPaths (v1,v2,V) -> Subset of (the carrier' of G * ) equals { p where p be Simple oriented Chain of G : p is_acyclicpath_of (v1,v2,V) };

      coherence

      proof

        set PT = { p where p be Simple oriented Chain of G : p is_acyclicpath_of (v1,v2,V) };

        PT c= (the carrier' of G * )

        proof

          let e be object;

          assume e in PT;

          then ex p be Simple oriented Chain of G st (e = p) & (p is_acyclicpath_of (v1,v2,V));

          hence thesis by FINSEQ_1:def 11;

        end;

        hence thesis;

      end;

    end

    definition

      let G be Graph, p be oriented Chain of G;

      :: GRAPH_5:def10

      func AcyclicPaths (p) -> Subset of (the carrier' of G * ) equals { q where q be Simple oriented Chain of G : q <> {} & (the Source of G . (q . 1)) = (the Source of G . (p . 1)) & (the Target of G . (q . ( len q))) = (the Target of G . (p . ( len p))) & ( rng q) c= ( rng p) };

      coherence

      proof

        set PT = { q where q be Simple oriented Chain of G : q <> {} & (the Source of G . (q . 1)) = (the Source of G . (p . 1)) & (the Target of G . (q . ( len q))) = (the Target of G . (p . ( len p))) & ( rng q) c= ( rng p) };

        PT c= (the carrier' of G * )

        proof

          let e be object;

          assume e in PT;

          then ex q be Simple oriented Chain of G st (e = q) & (q <> {} ) & ((the Source of G . (q . 1)) = (the Source of G . (p . 1))) & ((the Target of G . (q . ( len q))) = (the Target of G . (p . ( len p)))) & (( rng q) c= ( rng p));

          hence thesis by FINSEQ_1:def 11;

        end;

        hence thesis;

      end;

    end

    definition

      let G be Graph;

      :: GRAPH_5:def11

      func AcyclicPaths (G) -> Subset of (the carrier' of G * ) equals the set of all q where q be Simple oriented Chain of G;

      coherence

      proof

        set PT = the set of all q where q be Simple oriented Chain of G;

        PT c= (the carrier' of G * )

        proof

          let e be object;

          assume e in PT;

          then ex q be Simple oriented Chain of G st (e = q);

          hence thesis by FINSEQ_1:def 11;

        end;

        hence thesis;

      end;

    end

    theorem :: GRAPH_5:35

    p = {} implies not p is_acyclicpath_of (v1,v2)

    proof

      assume p = {} ;

      then not p is_orientedpath_of (v1,v2);

      hence thesis;

    end;

    theorem :: GRAPH_5:36

    p is_acyclicpath_of (v1,v2) implies p is_orientedpath_of (v1,v2);

    theorem :: GRAPH_5:37

    ( AcyclicPaths (v1,v2)) c= ( OrientedPaths (v1,v2))

    proof

      let x be object;

      assume x in ( AcyclicPaths (v1,v2));

      then

      consider p be Simple oriented Chain of G such that

       A1: x = p and

       A2: p is_acyclicpath_of (v1,v2);

      p is_orientedpath_of (v1,v2) by A2;

      hence thesis by A1;

    end;

    theorem :: GRAPH_5:38

    

     Th36: ( AcyclicPaths p) c= ( AcyclicPaths G)

    proof

      let e be object;

      assume e in ( AcyclicPaths p);

      then ex q be Simple oriented Chain of G st (e = q) & (q <> {} ) & ((the Source of G . (q . 1)) = (the Source of G . (p . 1))) & ((the Target of G . (q . ( len q))) = (the Target of G . (p . ( len p)))) & (( rng q) c= ( rng p));

      hence thesis;

    end;

    theorem :: GRAPH_5:39

    

     Th37: ( AcyclicPaths (v1,v2)) c= ( AcyclicPaths G)

    proof

      let e be object;

      assume e in ( AcyclicPaths (v1,v2));

      then ex q be Simple oriented Chain of G st (e = q) & (q is_acyclicpath_of (v1,v2));

      hence thesis;

    end;

    theorem :: GRAPH_5:40

    

     Th38: p is_orientedpath_of (v1,v2) implies ( AcyclicPaths p) c= ( AcyclicPaths (v1,v2))

    proof

      assume p is_orientedpath_of (v1,v2);

      then

       A1: (the Source of G . (p . 1)) = v1 & (the Target of G . (p . ( len p))) = v2;

      let x be object;

      assume x in ( AcyclicPaths p);

      then

      consider q be Simple oriented Chain of G such that

       A2: x = q and

       A3: q <> {} & (the Source of G . (q . 1)) = (the Source of G . (p . 1)) & (the Target of G . (q . ( len q))) = (the Target of G . (p . ( len p))) and ( rng q) c= ( rng p);

      q is_orientedpath_of (v1,v2) by A1, A3;

      then q is_acyclicpath_of (v1,v2);

      hence thesis by A2;

    end;

    theorem :: GRAPH_5:41

    

     Th39: p is_orientedpath_of (v1,v2,V) implies ( AcyclicPaths p) c= ( AcyclicPaths (v1,v2,V))

    proof

      assume

       A1: p is_orientedpath_of (v1,v2,V);

      let x be object;

      assume x in ( AcyclicPaths p);

      then

      consider q be Simple oriented Chain of G such that

       A2: x = q and

       A3: q <> {} & (the Source of G . (q . 1)) = (the Source of G . (p . 1)) & (the Target of G . (q . ( len q))) = (the Target of G . (p . ( len p))) and

       A4: ( rng q) c= ( rng p);

      (( vertices p) \ {v2}) c= V by A1;

      then

       A5: (( vertices q) \ {v2}) c= V by A4, Th20;

      p is_orientedpath_of (v1,v2) by A1;

      then (the Source of G . (p . 1)) = v1 & (the Target of G . (p . ( len p))) = v2;

      then q is_orientedpath_of (v1,v2) by A3;

      then q is_orientedpath_of (v1,v2,V) by A5;

      then q is_acyclicpath_of (v1,v2,V);

      hence thesis by A2;

    end;

    theorem :: GRAPH_5:42

    q in ( AcyclicPaths p) implies ( len q) <= ( len p)

    proof

      

       A1: ( card ( rng p)) <= ( card ( dom p)) by CARD_2: 47;

      

       A2: ( card ( dom p)) = ( card ( Seg ( len p))) by FINSEQ_1:def 3

      .= ( len p) by FINSEQ_1: 57;

      assume q in ( AcyclicPaths p);

      then

      consider x be Simple oriented Chain of G such that

       A3: q = x and x <> {} and (the Source of G . (x . 1)) = (the Source of G . (p . 1)) and (the Target of G . (x . ( len x))) = (the Target of G . (p . ( len p))) and

       A4: ( rng x) c= ( rng p);

      x is one-to-one by Th15;

      then

       A5: ( card ( rng x)) = ( len x) by FINSEQ_4: 62;

      ( card ( rng x)) <= ( card ( rng p)) by A4, NAT_1: 43;

      hence thesis by A3, A5, A1, A2, XXREAL_0: 2;

    end;

    theorem :: GRAPH_5:43

    

     Th41: p is_orientedpath_of (v1,v2) implies ( AcyclicPaths p) <> {} & ( AcyclicPaths (v1,v2)) <> {}

    proof

      defpred P[ Nat] means for p, v1, v2 st ($1 + 1) = ( len p) & p is_orientedpath_of (v1,v2) holds ( AcyclicPaths p) <> {} ;

      set FS = the Source of G, FT = the Target of G;

      

       A1: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        assume

         A2: P[k];

        now

          let p, v1, v2;

          assume that

           A3: ((k + 1) + 1) = ( len p) and p is_orientedpath_of (v1,v2);

          consider p1,p2 be FinSequence such that

           A4: ( len p1) = (k + 1) and

           A5: ( len p2) = 1 and

           A6: p = (p1 ^ p2) by A3, FINSEQ_2: 22;

          reconsider p1 as oriented Chain of G by A6, Th9;

          

           A7: 1 <= ( len p1) by A4, NAT_1: 11;

          then 1 in ( dom p1) by FINSEQ_3: 25;

          then

          reconsider x = (FS . (p1 . 1)) as Element of G by FINSEQ_2: 11, FUNCT_2: 5;

          

           A8: (p1 . 1) = (p . 1) by A6, A7, Lm1;

          ( len p1) in ( dom p1) by A7, FINSEQ_3: 25;

          then

          reconsider y = (FT . (p1 . ( len p1))) as Element of G by FINSEQ_2: 11, FUNCT_2: 5;

          p1 <> {} by A4;

          then p1 is_orientedpath_of (x,y);

          then ( AcyclicPaths p1) <> {} by A2, A4;

          then

          consider r be object such that

           A9: r in ( AcyclicPaths p1) by XBOOLE_0:def 1;

          

           A10: ( rng p1) c= ( rng p) by A6, FINSEQ_1: 29;

          

           A11: ( rng p2) c= ( rng p) by A6, FINSEQ_1: 30;

          

           A12: 1 in ( dom p2) by A5, FINSEQ_3: 25;

          then

           A13: (p . (( len p1) + 1)) = (p2 . 1) by A6, FINSEQ_1:def 7;

          consider q be Simple oriented Chain of G such that r = q and

           A14: q <> {} and

           A15: (FS . (q . 1)) = x and

           A16: (FT . (q . ( len q))) = y and

           A17: ( rng q) c= ( rng p1) by A9;

          ( len p1) < ( len p) by A3, A4, NAT_1: 13;

          

          then

           A18: (FS . (p . (( len p1) + 1))) = (FT . (p . ( len p1))) by A7, GRAPH_1:def 15

          .= (FT . (q . ( len q))) by A6, A7, A16, Lm1;

          then

           A19: (FS . (p2 . 1)) = (FT . (q . ( len q))) by A6, A12, FINSEQ_1:def 7;

          per cases ;

            suppose ex k st 1 <= k & k <= ( len q) & (FT . (q . k)) = (FT . (p2 . 1));

            then

            consider k such that

             A20: 1 <= k and

             A21: k <= ( len q) and

             A22: (FT . (q . k)) = (FT . (p2 . 1));

            consider i be Nat such that

             A23: ( len q) = (k + i) by A21, NAT_1: 10;

            consider q1,q2 be FinSequence such that

             A24: ( len q1) = k and ( len q2) = i and

             A25: q = (q1 ^ q2) by A23, FINSEQ_2: 22;

            reconsider q1 as Simple oriented Chain of G by A25, Th12;

            

             A26: q1 <> {} & (FS . (q1 . 1)) = (FS . (p . 1)) by A8, A15, A20, A24, A25, Lm1;

            ( rng q1) c= ( rng q) by A25, FINSEQ_1: 29;

            then ( rng q1) c= ( rng p1) by A17;

            then

             A27: ( rng q1) c= ( rng p) by A10;

            (FT . (q1 . ( len q1))) = (FT . (p . ( len p))) by A3, A4, A13, A20, A22, A24, A25, Lm1;

            then q1 in { w where w be Simple oriented Chain of G : w <> {} & (FS . (w . 1)) = (FS . (p . 1)) & (FT . (w . ( len w))) = (FT . (p . ( len p))) & ( rng w) c= ( rng p) } by A27, A26;

            hence ( AcyclicPaths p) <> {} ;

          end;

            suppose

             A28: not ex k st 1 <= k & k <= ( len q) & (FT . (q . k)) = (FT . (p2 . 1));

            reconsider p2 as oriented Chain of G by A6, Th9;

            hereby

              per cases ;

                suppose

                 A29: (FS . (q . 1)) <> (FT . (q . ( len q)));

                set qp = (q ^ p2);

                ( rng qp) = (( rng q) \/ ( rng p2)) & ( rng q) c= ( rng p) by A17, A10, FINSEQ_1: 31;

                then

                 A30: ( rng qp) c= (( rng p) \/ ( rng p)) by A11, XBOOLE_1: 13;

                

                 A31: ( len q) >= 1 by A14, FINSEQ_1: 20;

                then

                 A32: (FS . (qp . 1)) = (FS . (p . 1)) by A8, A15, Lm1;

                ( len qp) = (( len q) + 1) by A5, FINSEQ_1: 22;

                then

                 A33: qp <> {} & (FT . (qp . ( len qp))) = (FT . (p . ( len p))) by A3, A4, A5, A13, Lm2;

                qp is Simple oriented Chain of G by A5, A13, A18, A28, A29, A31, Th14;

                then qp in { w where w be Simple oriented Chain of G : w <> {} & (FS . (w . 1)) = (FS . (p . 1)) & (FT . (w . ( len w))) = (FT . (p . ( len p))) & ( rng w) c= ( rng p) } by A32, A33, A30;

                hence ( AcyclicPaths p) <> {} ;

              end;

                suppose

                 A34: (FS . (q . 1)) = (FT . (q . ( len q)));

                reconsider p2 as Simple oriented Chain of G by A5, Th13;

                p2 <> {} & (FT . (p2 . ( len p2))) = (FT . (p . ( len p))) by A3, A4, A5, A6, Lm2;

                then p2 in { w where w be Simple oriented Chain of G : w <> {} & (FS . (w . 1)) = (FS . (p . 1)) & (FT . (w . ( len w))) = (FT . (p . ( len p))) & ( rng w) c= ( rng p) } by A8, A15, A11, A19, A34;

                hence ( AcyclicPaths p) <> {} ;

              end;

            end;

          end;

        end;

        hence thesis;

      end;

      

       A35: P[ 0 ]

      proof

        let p, v1, v2;

        assume that

         A36: ( 0 + 1) = ( len p) and p is_orientedpath_of (v1,v2);

        reconsider r = p as Simple oriented Chain of G by A36, Th13;

        r <> {} by A36;

        then r in { q where q be Simple oriented Chain of G : q <> {} & (FS . (q . 1)) = (FS . (p . 1)) & (FT . (q . ( len q))) = (FT . (p . ( len p))) & ( rng q) c= ( rng p) };

        hence thesis;

      end;

      

       A37: for k holds P[k] from NAT_1:sch 2( A35, A1);

      assume

       A38: p is_orientedpath_of (v1,v2);

      then p <> {} ;

      then ( len p) >= 1 by FINSEQ_1: 20;

      then ((( len p) -' 1) + 1) = ( len p) by XREAL_1: 235;

      hence ( AcyclicPaths p) <> {} by A38, A37;

      then

       A39: ex x be object st x in ( AcyclicPaths p) by XBOOLE_0:def 1;

      ( AcyclicPaths p) c= ( AcyclicPaths (v1,v2)) by A38, Th38;

      hence thesis by A39;

    end;

    theorem :: GRAPH_5:44

    

     Th42: p is_orientedpath_of (v1,v2,V) implies ( AcyclicPaths p) <> {} & ( AcyclicPaths (v1,v2,V)) <> {}

    proof

      defpred P[ Nat] means for p, v1, v2 st ( len p) <= ($1 + 1) & p is_orientedpath_of (v1,v2,V) holds ( AcyclicPaths p) <> {} ;

      set FS = the Source of G, FT = the Target of G;

      assume

       A1: p is_orientedpath_of (v1,v2,V);

      then p is_orientedpath_of (v1,v2);

      then p <> {} ;

      then ( len p) >= 1 by FINSEQ_1: 20;

      then

       A2: ((( len p) -' 1) + 1) = ( len p) by XREAL_1: 235;

      

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

      proof

        let k;

        assume

         A4: P[k];

        now

          let p, v1, v2;

          assume that

           A5: ( len p) <= ((k + 1) + 1) and

           A6: p is_orientedpath_of (v1,v2,V);

          consider vs be FinSequence of the carrier of G such that

           A7: vs is_oriented_vertex_seq_of p by GRAPH_4: 9;

          

           A8: (( vertices p) \ {v2}) c= V by A6;

          

           A9: ( len vs) = (( len p) + 1) by A7, GRAPH_4:def 5;

          then

           A10: ( len vs) >= 1 by NAT_1: 12;

          

           A11: p is_orientedpath_of (v1,v2) by A6;

          then

           A12: p <> {} ;

          then

           A13: ( len p) >= 1 by FINSEQ_1: 20;

          then (p . ( len p)) orientedly_joins ((vs /. ( len p)),(vs /. (( len p) + 1))) by A7, GRAPH_4:def 5;

          then (FT . (p . ( len p))) = (vs /. (( len p) + 1)) by GRAPH_4:def 1;

          then

           A14: (FT . (p . ( len p))) = (vs . ( len vs)) by A9, A10, FINSEQ_4: 15;

          per cases ;

            suppose for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs);

            then p is Simple by A7, GRAPH_4:def 7;

            then p in { w where w be Simple oriented Chain of G : w <> {} & (FS . (w . 1)) = (FS . (p . 1)) & (FT . (w . ( len w))) = (FT . (p . ( len p))) & ( rng w) c= ( rng p) } by A12;

            hence ( AcyclicPaths p) <> {} ;

          end;

            suppose not for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs);

            then

            consider n, m such that

             A15: 1 <= n and

             A16: n < m and

             A17: m <= ( len vs) and

             A18: (vs . n) = (vs . m) and

             A19: not (n = 1 & m = ( len vs));

            consider i be Nat such that

             A20: m = (1 + i) by A15, A16, NAT_1: 10, XXREAL_0: 2;

            reconsider i as Element of NAT by ORDINAL1:def 12;

            

             A21: m >= 1 by A15, A16, XXREAL_0: 2;

            hereby

              per cases ;

                suppose

                 A22: n = 1;

                then m < ( len vs) by A17, A19, XXREAL_0: 1;

                then

                 A23: m <= ( len p) by A9, NAT_1: 13;

                then

                consider j be Nat such that

                 A24: ( len p) = (m + j) by NAT_1: 10;

                

                 A25: (p . 1) orientedly_joins ((vs /. 1),(vs /. (1 + 1))) by A7, A13, GRAPH_4:def 5;

                

                 A26: n <= ( len vs) by A16, A17, XXREAL_0: 2;

                (p . m) orientedly_joins ((vs /. m),(vs /. (m + 1))) by A7, A16, A22, A23, GRAPH_4:def 5;

                

                then

                 A27: (FS . (p . m)) = (vs /. m) by GRAPH_4:def 1

                .= (vs . m) by A16, A17, A22, FINSEQ_4: 15

                .= (vs /. n) by A15, A18, A26, FINSEQ_4: 15

                .= (FS . (p . 1)) by A22, A25, GRAPH_4:def 1

                .= v1 by A11;

                reconsider j as Element of NAT by ORDINAL1:def 12;

                

                 A28: ( len p) = (i + (1 + j)) by A20, A24;

                then

                consider p1,p2 be FinSequence such that

                 A29: ( len p1) = i and

                 A30: ( len p2) = (1 + j) and

                 A31: p = (p1 ^ p2) by FINSEQ_2: 22;

                

                 A32: 1 <= ( len p2) by A30, NAT_1: 11;

                then

                 A33: (p2 . 1) = (p . m) by A20, A29, A31, Lm2;

                (p2 . ( len p2)) = (p . ( len p)) by A28, A29, A30, A31, A32, Lm2;

                then

                 A34: (FT . (p2 . ( len p2))) = v2 by A11;

                reconsider p1, p2 as oriented Chain of G by A31, Th9;

                ((i + 1) + ( - 1)) > (1 + ( - 1)) by A16, A20, A22, XREAL_1: 8;

                then ( len p2) < ( len p) by A28, A30, XREAL_1: 29;

                then ( len p2) < ((k + 1) + 1) by A5, XXREAL_0: 2;

                then

                 A35: ( len p2) <= (k + 1) by NAT_1: 13;

                (( vertices (p1 ^ p2)) \ {v2}) c= V by A6, A31;

                then

                 A36: (( vertices p2) \ {v2}) c= V by Th21;

                p2 <> {} by A30;

                then p2 is_orientedpath_of (v1,v2) by A27, A33, A34;

                then p2 is_orientedpath_of (v1,v2,V) by A36;

                then ( AcyclicPaths p2) <> {} by A4, A35;

                then

                consider r be object such that

                 A37: r in ( AcyclicPaths p2) by XBOOLE_0:def 1;

                consider q be Simple oriented Chain of G such that r = q and

                 A38: q <> {} and

                 A39: (FS . (q . 1)) = v1 & (FT . (q . ( len q))) = v2 and

                 A40: ( rng q) c= ( rng p2) by A27, A33, A34, A37;

                ( rng p2) c= ( rng p) by A31, FINSEQ_1: 30;

                then

                 A41: ( rng q) c= ( rng p) by A40;

                (FS . (q . 1)) = (FS . (p . 1)) & (FT . (q . ( len q))) = (FT . (p . ( len p))) by A11, A39;

                then q in { w where w be Simple oriented Chain of G : w <> {} & (FS . (w . 1)) = (FS . (p . 1)) & (FT . (w . ( len w))) = (FT . (p . ( len p))) & ( rng w) c= ( rng p) } by A38, A41;

                hence ( AcyclicPaths p) <> {} ;

              end;

                suppose

                 A42: n <> 1;

                consider n1 be Nat such that

                 A43: n = (1 + n1) by A15, NAT_1: 10;

                reconsider n1 as Element of NAT by ORDINAL1:def 12;

                

                 A44: n < ( len vs) by A16, A17, XXREAL_0: 2;

                then

                 A45: n1 < ( len p) by A9, A43, XREAL_1: 7;

                then

                consider j be Nat such that

                 A46: ( len p) = (n1 + j) by NAT_1: 10;

                reconsider j as Element of NAT by ORDINAL1:def 12;

                consider p1,p2 be FinSequence such that

                 A47: ( len p1) = n1 and ( len p2) = j and

                 A48: p = (p1 ^ p2) by A46, FINSEQ_2: 22;

                

                 A49: n > 1 by A15, A42, XXREAL_0: 1;

                then

                 A50: n1 >= 1 by A43, NAT_1: 13;

                then

                 A51: (p1 . ( len p1)) = (p . n1) by A47, A48, Lm1;

                (p1 . 1) = (p . 1) by A47, A48, A50, Lm1;

                then

                 A52: (FS . (p1 . 1)) = v1 by A11;

                

                 A53: ( rng p1) c= ( rng p) by A48, FINSEQ_1: 29;

                reconsider p1, p2 as oriented Chain of G by A48, Th9;

                (p . n1) orientedly_joins ((vs /. n1),(vs /. (n1 + 1))) by A7, A45, A50, GRAPH_4:def 5;

                

                then

                 A54: (FT . (p . n1)) = (vs /. n) by A43, GRAPH_4:def 1

                .= (vs . n) by A15, A44, FINSEQ_4: 15;

                hereby

                  per cases ;

                    suppose m = ( len vs);

                    then

                     A55: (FT . (p1 . ( len p1))) = v2 by A11, A14, A18, A54, A51;

                    (( vertices (p1 ^ p2)) \ {v2}) c= V by A6, A48;

                    then

                     A56: (( vertices p1) \ {v2}) c= V by Th21;

                    n1 < ((k + 1) + 1) by A5, A45, XXREAL_0: 2;

                    then

                     A57: ( len p1) <= (k + 1) by A47, NAT_1: 13;

                    p1 <> {} by A49, A43, A47;

                    then p1 is_orientedpath_of (v1,v2) by A52, A55;

                    then p1 is_orientedpath_of (v1,v2,V) by A56;

                    then ( AcyclicPaths p1) <> {} by A4, A57;

                    then

                    consider r be object such that

                     A58: r in ( AcyclicPaths p1) by XBOOLE_0:def 1;

                    consider q be Simple oriented Chain of G such that r = q and

                     A59: q <> {} and

                     A60: (FS . (q . 1)) = v1 and

                     A61: (FT . (q . ( len q))) = v2 and

                     A62: ( rng q) c= ( rng p1) by A52, A55, A58;

                    

                     A63: (FT . (q . ( len q))) = (FT . (p . ( len p))) by A11, A61;

                    ( rng q) c= ( rng p) & (FS . (q . 1)) = (FS . (p . 1)) by A11, A53, A60, A62;

                    then q in { w where w be Simple oriented Chain of G : w <> {} & (FS . (w . 1)) = (FS . (p . 1)) & (FT . (w . ( len w))) = (FT . (p . ( len p))) & ( rng w) c= ( rng p) } by A59, A63;

                    hence ( AcyclicPaths p) <> {} ;

                  end;

                    suppose m <> ( len vs);

                    then m < ( len vs) by A17, XXREAL_0: 1;

                    then

                     A64: m <= ( len p) by A9, NAT_1: 13;

                    then

                    consider h be Nat such that

                     A65: ( len p) = (m + h) by NAT_1: 10;

                    (p . m) orientedly_joins ((vs /. m),(vs /. (m + 1))) by A7, A21, A64, GRAPH_4:def 5;

                    

                    then

                     A66: (FS . (p . m)) = (vs /. m) by GRAPH_4:def 1

                    .= (FT . (p1 . ( len p1))) by A17, A18, A21, A54, A51, FINSEQ_4: 15;

                    reconsider h as Element of NAT by ORDINAL1:def 12;

                    

                     A67: ( len p) = (i + (1 + h)) by A20, A65;

                    then

                    consider q1,q2 be FinSequence such that

                     A68: ( len q1) = i and

                     A69: ( len q2) = (1 + h) and

                     A70: p = (q1 ^ q2) by FINSEQ_2: 22;

                    reconsider q2 as oriented Chain of G by A70, Th9;

                    

                     A71: 1 <= ( len q2) by A69, NAT_1: 12;

                    then (q2 . 1) = (p . m) by A20, A68, A70, Lm2;

                    then

                    reconsider pq = (p1 ^ q2) as oriented Chain of G by A66, Th10;

                    (pq . ( len pq)) = (pq . (( len p1) + ( len q2))) by FINSEQ_1: 22

                    .= (q2 . ( len q2)) by A71, Lm2

                    .= (p . ( len p)) by A67, A68, A69, A70, A71, Lm2;

                    then

                     A72: (FT . (pq . ( len pq))) = v2 by A11;

                    

                     A73: ( rng pq) = (( rng p1) \/ ( rng q2)) by FINSEQ_1: 31;

                    ( rng q2) c= ( rng p) by A70, FINSEQ_1: 30;

                    then

                     A74: ( rng pq) c= ( rng p) by A53, A73, XBOOLE_1: 8;

                    then

                     A75: (( vertices pq) \ {v2}) c= V by A8, Th20;

                    

                     A76: ( len pq) = (n1 + (1 + h)) by A47, A69, FINSEQ_1: 22;

                    (m + h) > (n + h) by A16, XREAL_1: 8;

                    then ( len pq) < ((k + 1) + 1) by A5, A43, A65, A76, XXREAL_0: 2;

                    then

                     A77: ( len pq) <= (k + 1) by NAT_1: 13;

                    

                     A78: (FS . (pq . 1)) = v1 by A47, A50, A52, Lm1;

                    pq <> {} by A76;

                    then pq is_orientedpath_of (v1,v2) by A78, A72;

                    then pq is_orientedpath_of (v1,v2,V) by A75;

                    then ( AcyclicPaths pq) <> {} by A4, A77;

                    then

                    consider r be object such that

                     A79: r in ( AcyclicPaths pq) by XBOOLE_0:def 1;

                    consider q be Simple oriented Chain of G such that r = q and

                     A80: q <> {} and

                     A81: (FS . (q . 1)) = v1 & (FT . (q . ( len q))) = v2 and

                     A82: ( rng q) c= ( rng pq) by A78, A72, A79;

                    

                     A83: ( rng q) c= ( rng p) by A74, A82;

                    (FS . (q . 1)) = (FS . (p . 1)) & (FT . (q . ( len q))) = (FT . (p . ( len p))) by A11, A81;

                    then q in { w where w be Simple oriented Chain of G : w <> {} & (FS . (w . 1)) = (FS . (p . 1)) & (FT . (w . ( len w))) = (FT . (p . ( len p))) & ( rng w) c= ( rng p) } by A80, A83;

                    hence ( AcyclicPaths p) <> {} ;

                  end;

                end;

              end;

            end;

          end;

        end;

        hence thesis;

      end;

      

       A84: P[ 0 ]

      proof

        let p, v1, v2;

        assume that

         A85: ( len p) <= ( 0 + 1) and

         A86: p is_orientedpath_of (v1,v2,V);

        p is_orientedpath_of (v1,v2) by A86;

        then

         A87: p <> {} ;

        then ( len p) >= 1 by FINSEQ_1: 20;

        then

        reconsider r = p as Simple oriented Chain of G by A85, Th13, XXREAL_0: 1;

        r in { q where q be Simple oriented Chain of G : q <> {} & (FS . (q . 1)) = (FS . (p . 1)) & (FT . (q . ( len q))) = (FT . (p . ( len p))) & ( rng q) c= ( rng p) } by A87;

        hence thesis;

      end;

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

      hence ( AcyclicPaths p) <> {} by A1, A2;

      then

       A88: ex x be object st x in ( AcyclicPaths p) by XBOOLE_0:def 1;

      ( AcyclicPaths p) c= ( AcyclicPaths (v1,v2,V)) by A1, Th39;

      hence thesis by A88;

    end;

    theorem :: GRAPH_5:45

    

     Th43: ( AcyclicPaths (v1,v2,V)) c= ( AcyclicPaths G)

    proof

      let e be object;

      assume e in ( AcyclicPaths (v1,v2,V));

      then ex q be Simple oriented Chain of G st (e = q) & (q is_acyclicpath_of (v1,v2,V));

      hence thesis;

    end;

    begin

    notation

      synonym Real>=0 for REAL+ ;

    end

    definition

      :: original: Real>=0

      redefine

      :: GRAPH_5:def12

      func Real>=0 -> Subset of REAL equals { r where r be Real : r >= 0 };

      compatibility by REAL_1: 1;

      coherence by ARYTM_0: 1;

    end

    registration

      cluster Real>=0 -> non empty;

      coherence ;

    end

    definition

      let G be Graph, W be Function;

      :: GRAPH_5:def13

      pred W is_weight>=0of G means W is Function of the carrier' of G, Real>=0 ;

    end

    definition

      let G be Graph, W be Function;

      :: GRAPH_5:def14

      pred W is_weight_of G means W is Function of the carrier' of G, REAL ;

    end

    definition

      let G be Graph, p be FinSequence of the carrier' of G, W be Function;

      assume

       A1: W is_weight_of G;

      :: GRAPH_5:def15

      func RealSequence (p,W) -> FinSequence of REAL means

      : Def15: ( dom p) = ( dom it ) & for i be Nat st i in ( dom p) holds (it . i) = (W . (p . i));

      existence

      proof

        deffunc F( object) = (W . (p . $1));

        consider f such that

         A2: ( dom f) = ( dom p) & for x be object st x in ( dom p) holds (f . x) = F(x) from FUNCT_1:sch 3;

         A3:

        now

          let i be Nat;

          

           A4: W is Function of the carrier' of G, REAL by A1;

          assume

           A5: i in ( dom f);

          then (f . i) = (W . (p . i)) by A2;

          hence (f . i) in REAL by A2, A5, A4, FINSEQ_2: 11, FUNCT_2: 5;

        end;

        ( dom f) = ( Seg ( len p)) by A2, FINSEQ_1:def 3;

        then f is FinSequence by FINSEQ_1:def 2;

        then

        reconsider g = f as FinSequence of REAL by A3, FINSEQ_2: 12;

        take g;

        thus ( dom p) = ( dom g) by A2;

        let i;

        assume i in ( dom p);

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f1,f2 be FinSequence of REAL ;

        assume that

         A6: ( dom p) = ( dom f1) and

         A7: for i be Nat st i in ( dom p) holds (f1 . i) = (W . (p . i));

        assume that

         A8: ( dom p) = ( dom f2) and

         A9: for i be Nat st i in ( dom p) holds (f2 . i) = (W . (p . i));

        now

          let i be Nat;

          assume

           A10: i in ( dom f1);

          

          hence (f1 . i) = (W . (p . i)) by A6, A7

          .= (f2 . i) by A6, A9, A10;

        end;

        hence thesis by A6, A8;

      end;

    end

    definition

      let G be Graph, p be FinSequence of the carrier' of G, W be Function;

      :: GRAPH_5:def16

      func cost (p,W) -> Real equals ( Sum ( RealSequence (p,W)));

      coherence ;

    end

    theorem :: GRAPH_5:46

    

     Th44: W is_weight>=0of G implies W is_weight_of G by FUNCT_2: 7;

    theorem :: GRAPH_5:47

    

     Th45: for f be FinSequence of REAL st W is_weight>=0of G & f = ( RealSequence (pe,W)) holds for i st i in ( dom f) holds (f . i) >= 0

    proof

      let f be FinSequence of REAL ;

      assume that

       A1: W is_weight>=0of G and

       A2: f = ( RealSequence (pe,W));

      

       A3: W is Function of the carrier' of G, Real>=0 by A1;

      let i;

      assume

       A4: i in ( dom f);

      

       A5: W is_weight_of G by A1, Th44;

      then

       A6: ( dom pe) = ( dom f) by A2, Def15;

      then (f . i) = (W . (pe . i)) by A2, A5, A4, Def15;

      then (f . i) in Real>=0 by A6, A3, A4, FINSEQ_2: 11, FUNCT_2: 5;

      then ex r be Real st (f . i) = r & r >= 0 ;

      hence thesis;

    end;

    theorem :: GRAPH_5:48

    

     Th46: ( rng qe) c= ( rng pe) & W is_weight_of G & i in ( dom qe) implies ex j st j in ( dom pe) & (( RealSequence (pe,W)) . j) = (( RealSequence (qe,W)) . i)

    proof

      assume that

       A1: ( rng qe) c= ( rng pe) and

       A2: W is_weight_of G and

       A3: i in ( dom qe);

      set g = ( RealSequence (qe,W));

      consider y be object such that

       A4: y in ( dom pe) and

       A5: (qe . i) = (pe . y) by A1, A3, FUNCT_1: 114;

      reconsider j = y as Element of NAT by A4;

      take j;

      thus j in ( dom pe) by A4;

      (g . i) = (W . (qe . i)) by A2, A3, Def15;

      hence thesis by A2, A4, A5, Def15;

    end;

    

     Lm3: for f be FinSequence of REAL holds (for y be Real st y in ( rng f) holds y >= 0 ) iff for i be Nat st i in ( dom f) holds (f . i) >= 0

    proof

      let f be FinSequence of REAL ;

      hereby

        assume

         A1: for y be Real st y in ( rng f) holds y >= 0 ;

        hereby

          let i be Nat;

          assume i in ( dom f);

          then (f . i) in ( rng f) by FUNCT_1:def 3;

          hence (f . i) >= 0 by A1;

        end;

      end;

      assume

       A2: for i be Nat st i in ( dom f) holds (f . i) >= 0 ;

      hereby

        let x be Real;

        assume x in ( rng f);

        then

        consider y be object such that

         A3: y in ( dom f) and

         A4: x = (f . y) by FUNCT_1:def 3;

        thus x >= 0 by A2, A3, A4;

      end;

    end;

    

     Lm4: for p,q,r be FinSequence of REAL st r = (p ^ q) & (for x be Real st x in ( rng r) holds x >= 0 ) holds (for i st i in ( dom p) holds (p . i) >= 0 ) & for i st i in ( dom q) holds (q . i) >= 0

    proof

      let p,q,r be FinSequence of REAL ;

      assume that

       A1: r = (p ^ q) and

       A2: for x be Real st x in ( rng r) holds x >= 0 ;

      ( rng p) c= ( rng r) by A1, FINSEQ_1: 29;

      then for y be Real st y in ( rng p) holds y >= 0 by A2;

      hence for i st i in ( dom p) holds (p . i) >= 0 by Lm3;

      ( rng q) c= ( rng r) by A1, FINSEQ_1: 30;

      then for y be Real st y in ( rng q) holds y >= 0 by A2;

      hence thesis by Lm3;

    end;

    theorem :: GRAPH_5:49

    ( len qe) = 1 & ( rng qe) c= ( rng pe) & W is_weight>=0of G implies ( cost (qe,W)) <= ( cost (pe,W))

    proof

      assume that

       A1: ( len qe) = 1 and

       A2: ( rng qe) c= ( rng pe) and

       A3: W is_weight>=0of G;

      set f = ( RealSequence (pe,W)), g = ( RealSequence (qe,W));

      1 in ( dom qe) by A1, FINSEQ_3: 25;

      then

      consider j such that

       A4: j in ( dom pe) and

       A5: (f . j) = (g . 1) by A2, A3, Th44, Th46;

      

       A6: W is_weight_of G by A3, Th44;

      then ( dom pe) = ( dom f) by Def15;

      then

       A7: ( len pe) = ( len f) by FINSEQ_3: 29;

      reconsider g1 = (g . 1) as Element of REAL by XREAL_0:def 1;

      ( dom g) = ( dom qe) by A6, Def15;

      then ( len g) = ( len qe) by FINSEQ_3: 29;

      then g = <*g1*> by A1, FINSEQ_1: 40;

      then ( Sum g) = g1 by RVSUM_1: 73;

      then

       A8: ( cost (qe,W)) = g1;

      j <= ( len pe) by A4, FINSEQ_3: 25;

      then

      consider m be Nat such that

       A9: ( len f) = (j + m) by A7, NAT_1: 10;

      reconsider m as Element of NAT by ORDINAL1:def 12;

      consider f1,f2 be FinSequence of REAL such that

       A10: ( len f1) = j and ( len f2) = m and

       A11: f = (f1 ^ f2) by A9, FINSEQ_2: 23;

      

       A12: 1 <= j by A4, FINSEQ_3: 25;

      then

      consider h be FinSequence of REAL , d be Element of REAL such that

       A13: f1 = (h ^ <*d*>) by A10, FINSEQ_2: 19;

      j in ( dom f1) by A12, A10, FINSEQ_3: 25;

      then

       A14: (f1 . j) = (g . 1) by A5, A11, FINSEQ_1:def 7;

      j = (( len h) + 1) by A10, A13, FINSEQ_2: 16;

      then

       A15: d = (g . 1) by A13, A14, FINSEQ_1: 42;

      for i be Nat st i in ( dom f) holds (f . i) >= 0 by A3, Th45;

      then

       A16: for y be Real st y in ( rng f) holds y >= 0 by Lm3;

      then for i be Nat st i in ( dom f2) holds (f2 . i) >= 0 by A11, Lm4;

      then

       A17: ( Sum f2) >= 0 by RVSUM_1: 84;

      for i be Nat st i in ( dom f1) holds (f1 . i) >= 0 by A11, A16, Lm4;

      then for y be Real st y in ( rng f1) holds y >= 0 by Lm3;

      then for i be Nat st i in ( dom h) holds (h . i) >= 0 by A13, Lm4;

      then

       A18: ( Sum h) >= 0 by RVSUM_1: 84;

      reconsider d as Element of REAL ;

      reconsider dd = <*d*> as FinSequence of REAL ;

      ( Sum f1) = (( Sum h) + ( Sum dd)) by A13, RVSUM_1: 75

      .= (( Sum h) + d) by RVSUM_1: 73

      .= (( Sum h) + (g . 1)) by A15;

      then

       A19: ( Sum f1) >= ( 0 qua Nat + (g . 1)) by A18, XREAL_1: 7;

      ( Sum f) = (( Sum f1) + ( Sum f2)) by A11, RVSUM_1: 75;

      hence thesis by A8, A17, A19, XREAL_1: 7;

    end;

    theorem :: GRAPH_5:50

    

     Th48: W is_weight>=0of G implies ( cost (pe,W)) >= 0

    proof

      set f = ( RealSequence (pe,W));

      assume W is_weight>=0of G;

      then for i be Nat st i in ( dom f) holds (f . i) >= 0 by Th45;

      hence thesis by RVSUM_1: 84;

    end;

    theorem :: GRAPH_5:51

    

     Th49: pe = {} & W is_weight_of G implies ( cost (pe,W)) = 0

    proof

      assume that

       A1: pe = {} and

       A2: W is_weight_of G;

      set f = ( RealSequence (pe,W));

      ( dom f) = ( dom pe) by A2, Def15;

      

      then ( len f) = ( len pe) by FINSEQ_3: 29

      .= 0 by A1;

      then f = ( <*> REAL );

      hence thesis by RVSUM_1: 72;

    end;

    theorem :: GRAPH_5:52

    

     Th50: for D be non empty finite Subset of (the carrier' of G * ) st D = ( AcyclicPaths (v1,v2)) holds ex pe st pe in D & for qe st qe in D holds ( cost (pe,W)) <= ( cost (qe,W))

    proof

      let D be non empty finite Subset of (the carrier' of G * );

      deffunc F( Element of D) = ( cost ($1,W));

      consider x be Element of D such that

       A1: for y be Element of D holds F(x) <= F(y) from PRE_CIRC:sch 5;

      assume D = ( AcyclicPaths (v1,v2));

      then x in ( AcyclicPaths (v1,v2));

      then

      consider p be Simple oriented Chain of G such that

       A2: x = p and p is_acyclicpath_of (v1,v2);

      take p;

      thus p in D by A2;

      let pe be FinSequence of the carrier' of G;

      assume pe in D;

      then

      reconsider y = pe as Element of D;

       F(x) <= F(y) by A1;

      hence thesis by A2;

    end;

    theorem :: GRAPH_5:53

    

     Th51: for D be non empty finite Subset of (the carrier' of G * ) st D = ( AcyclicPaths (v1,v2,V)) holds ex pe st pe in D & for qe st qe in D holds ( cost (pe,W)) <= ( cost (qe,W))

    proof

      let D be non empty finite Subset of (the carrier' of G * );

      deffunc F( Element of D) = ( cost ($1,W));

      consider x be Element of D such that

       A1: for y be Element of D holds F(x) <= F(y) from PRE_CIRC:sch 5;

      assume D = ( AcyclicPaths (v1,v2,V));

      then x in ( AcyclicPaths (v1,v2,V));

      then

      consider p be Simple oriented Chain of G such that

       A2: x = p and p is_acyclicpath_of (v1,v2,V);

      take p;

      thus p in D by A2;

      let pe;

      assume pe in D;

      then

      reconsider y = pe as Element of D;

       F(x) <= F(y) by A1;

      hence thesis by A2;

    end;

    theorem :: GRAPH_5:54

    

     Th52: W is_weight_of G implies ( cost ((pe ^ qe),W)) = (( cost (pe,W)) + ( cost (qe,W)))

    proof

      set r = (pe ^ qe), f = ( RealSequence ((pe ^ qe),W)), g = ( RealSequence (pe,W)), h = ( RealSequence (qe,W));

      assume

       A1: W is_weight_of G;

      then

       A2: ( dom pe) = ( dom g) by Def15;

      then

       A3: ( len pe) = ( len g) by FINSEQ_3: 29;

      

       A4: ( dom qe) = ( dom h) by A1, Def15;

      then

       A5: ( len qe) = ( len h) by FINSEQ_3: 29;

      

       A6: ( dom r) = ( dom f) by A1, Def15;

      then ( len f) = ( len r) by FINSEQ_3: 29;

      then

       A7: ( len f) = (( len g) + ( len h)) by A3, A5, FINSEQ_1: 22;

       A8:

      now

        let i be Nat;

        assume

         A9: i in ( dom h);

        then 1 <= i by FINSEQ_3: 25;

        then

         A10: 1 <= (( len g) + i) by NAT_1: 12;

        i <= ( len h) by A9, FINSEQ_3: 25;

        then (( len g) + i) <= ( len f) by A7, XREAL_1: 7;

        then

         A11: (( len g) + i) in ( dom f) by A10, FINSEQ_3: 25;

        (h . i) = (W . (qe . i)) & (r . (( len g) + i)) = (qe . i) by A1, A4, A3, A9, Def15, FINSEQ_1:def 7;

        hence (f . (( len g) + i)) = (h . i) by A1, A6, A11, Def15;

      end;

      now

        let i be Nat;

        assume

         A12: i in ( dom g);

        then i <= ( len g) by FINSEQ_3: 25;

        then

         A13: i <= ( len f) by A7, NAT_1: 12;

        1 <= i by A12, FINSEQ_3: 25;

        then

         A14: i in ( dom f) by A13, FINSEQ_3: 25;

        (g . i) = (W . (pe . i)) & (r . i) = (pe . i) by A1, A2, A12, Def15, FINSEQ_1:def 7;

        hence (f . i) = (g . i) by A1, A6, A14, Def15;

      end;

      then f = (g ^ h) by A7, A8, FINSEQ_3: 38;

      hence thesis by RVSUM_1: 75;

    end;

    theorem :: GRAPH_5:55

    

     Th53: qe is one-to-one & ( rng qe) c= ( rng pe) & W is_weight>=0of G implies ( cost (qe,W)) <= ( cost (pe,W))

    proof

      set D = the carrier' of G;

      assume that

       A1: qe is one-to-one & ( rng qe) c= ( rng pe) and

       A2: W is_weight>=0of G;

      defpred P[ Nat] means for p,q be FinSequence of D st q is one-to-one & ( rng q) c= ( rng p) & ( len q) = $1 holds ( cost (q,W)) <= ( cost (p,W));

      

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

      proof

        let k be Nat;

        assume

         A4: P[k];

        now

          let p,q be FinSequence of D;

          assume that

           A5: q is one-to-one and

           A6: ( rng q) c= ( rng p) and

           A7: ( len q) = (k + 1);

          consider q1 be FinSequence, x be object such that

           A8: q = (q1 ^ <*x*>) by A7, FINSEQ_2: 18;

          

           A9: (k + 1) = (( len q1) + 1) by A7, A8, FINSEQ_2: 16;

          consider p1,p2 be FinSequence such that

           A10: p = ((p1 ^ <*x*>) ^ p2) and

           A11: ( rng q1) c= ( rng (p1 ^ p2)) by A5, A6, A8, Th7;

          reconsider q1 as FinSequence of D by A8, FINSEQ_1: 36;

          

           A12: (p1 ^ <*x*>) is FinSequence of D by A10, FINSEQ_1: 36;

          then

          reconsider y = <*x*> as FinSequence of D by FINSEQ_1: 36;

          reconsider p2 as FinSequence of D by A10, FINSEQ_1: 36;

          reconsider p1 as FinSequence of D by A12, FINSEQ_1: 36;

          q1 is one-to-one by A5, A8, FINSEQ_3: 91;

          then

           A13: ( cost (q1,W)) <= ( cost ((p1 ^ p2),W)) by A4, A11, A9;

          

           A14: ( cost (q,W)) = (( cost (q1,W)) + ( cost (y,W))) by A2, A8, Th44, Th52;

          ( cost (p,W)) = (( cost ((p1 ^ y),W)) + ( cost (p2,W))) by A2, A10, Th44, Th52

          .= ((( cost (p1,W)) + ( cost (y,W))) + ( cost (p2,W))) by A2, Th44, Th52

          .= ((( cost (p1,W)) + ( cost (p2,W))) + ( cost (y,W)))

          .= (( cost ((p1 ^ p2),W)) + ( cost (y,W))) by A2, Th44, Th52;

          hence ( cost (q,W)) <= ( cost (p,W)) by A14, A13, XREAL_1: 7;

        end;

        hence thesis;

      end;

      

       A15: P[ 0 ]

      proof

        let p,q be FinSequence of D;

        assume that q is one-to-one and ( rng q) c= ( rng p) and

         A16: ( len q) = 0 ;

        q = {} by A16;

        then ( cost (q,W)) = 0 by A2, Th44, Th49;

        hence thesis by A2, Th48;

      end;

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

      then P[( len qe)];

      hence thesis by A1;

    end;

    theorem :: GRAPH_5:56

    

     Th54: pe in ( AcyclicPaths p) & W is_weight>=0of G implies ( cost (pe,W)) <= ( cost (p,W))

    proof

      assume that

       A1: pe in ( AcyclicPaths p) and

       A2: W is_weight>=0of G;

      

       A3: ex r be Simple oriented Chain of G st (r = pe) & (r <> {} ) & ((the Source of G . (r . 1)) = (the Source of G . (p . 1))) & ((the Target of G . (r . ( len r))) = (the Target of G . (p . ( len p)))) & (( rng r) c= ( rng p)) by A1;

      then pe is one-to-one by Th15;

      hence thesis by A2, A3, Th53;

    end;

    begin

    definition

      let G be Graph, v1,v2 be Vertex of G, p be oriented Chain of G, W be Function;

      :: GRAPH_5:def17

      pred p is_shortestpath_of v1,v2,W means p is_orientedpath_of (v1,v2) & for q be oriented Chain of G st q is_orientedpath_of (v1,v2) holds ( cost (p,W)) <= ( cost (q,W));

    end

    definition

      let G be Graph, v1,v2 be Vertex of G, p be oriented Chain of G, V be set, W be Function;

      :: GRAPH_5:def18

      pred p is_shortestpath_of v1,v2,V,W means p is_orientedpath_of (v1,v2,V) & for q be oriented Chain of G st q is_orientedpath_of (v1,v2,V) holds ( cost (p,W)) <= ( cost (q,W));

    end

    begin

    reserve G for finite Graph,

ps for Simple oriented Chain of G,

P,Q for oriented Chain of G,

v1,v2,v3 for Element of G,

pe,qe for FinSequence of the carrier' of G;

    theorem :: GRAPH_5:57

    ( len ps) <= ( VerticesCount G)

    proof

      set VV = the carrier of G;

      consider vs be FinSequence of VV such that

       A1: vs is_oriented_vertex_seq_of ps and

       A2: for n, m st 1 <= n & n < m & m <= ( len vs) & (vs . n) = (vs . m) holds n = 1 & m = ( len vs) by GRAPH_4:def 7;

      reconsider V = VV as finite set;

      

       A3: ( len vs) = (( len ps) + 1) by A1, GRAPH_4:def 5;

      then vs <> {} ;

      then

      consider q be FinSequence, x be object such that

       A4: vs = (q ^ <*x*>) by FINSEQ_1: 46;

      

       A5: (( len ps) + 1) = (( len q) + ( len <*x*>)) by A3, A4, FINSEQ_1: 22

      .= (( len q) + 1) by FINSEQ_1: 39;

      now

        let n, m;

        assume that

         A6: 1 <= n and

         A7: n < m and

         A8: m <= ( len q);

        1 <= m by A6, A7, XXREAL_0: 2;

        then

         A9: m in ( dom q) by A8, FINSEQ_3: 25;

        n <= ( len q) by A7, A8, XXREAL_0: 2;

        then n in ( dom q) by A6, FINSEQ_3: 25;

        then

         A10: (vs . n) = (q . n) by A4, FINSEQ_1:def 7;

        ( len q) < ( len vs) by A3, A5, XREAL_1: 29;

        then

         A11: m < ( len vs) by A8, XXREAL_0: 2;

        assume (q . n) = (q . m);

        then (vs . m) = (vs . n) by A4, A10, A9, FINSEQ_1:def 7;

        hence contradiction by A2, A6, A7, A11;

      end;

      then

       A12: ( card ( rng q)) = ( len q) by Th5;

      ( rng vs) c= VV & ( rng q) c= ( rng vs) by A4, FINSEQ_1: 29, FINSEQ_1:def 4;

      then ( card ( rng q)) <= ( card V) by NAT_1: 43, XBOOLE_1: 1;

      hence thesis by A5, A12, GRAPH_1:def 19;

    end;

    theorem :: GRAPH_5:58

    

     Th56: ( len ps) <= ( EdgesCount G)

    proof

      reconsider V = the carrier' of G as finite set;

      ( rng ps) c= the carrier' of G by FINSEQ_1:def 4;

      then

       A1: ( card ( rng ps)) <= ( card V) by NAT_1: 43;

      ps is one-to-one by Th15;

      then ( card ( rng ps)) = ( len ps) by FINSEQ_4: 62;

      hence thesis by A1, GRAPH_1:def 20;

    end;

    

     Lm5: ( AcyclicPaths G) is finite

    proof

      set n = ( EdgesCount G), D = the carrier' of G, A = { x where x be Element of (D * ) : ( len x) <= n };

      

       A1: ( AcyclicPaths G) c= A

      proof

        let x be object;

        assume x in ( AcyclicPaths G);

        then

        consider p be Simple oriented Chain of G such that

         A2: x = p;

        p is Element of (D * ) & ( len p) <= n by Th56, FINSEQ_1:def 11;

        hence thesis by A2;

      end;

      A is finite by Th3;

      hence thesis by A1;

    end;

    registration

      let G;

      cluster ( AcyclicPaths G) -> finite;

      coherence by Lm5;

    end

    

     Lm6: ( AcyclicPaths P) is finite

    proof

      ( AcyclicPaths P) c= ( AcyclicPaths G) by Th36;

      hence thesis;

    end;

    

     Lm7: ( AcyclicPaths (v1,v2)) is finite

    proof

      ( AcyclicPaths (v1,v2)) c= ( AcyclicPaths G) by Th37;

      hence thesis;

    end;

    

     Lm8: ( AcyclicPaths (v1,v2,V)) is finite

    proof

      ( AcyclicPaths (v1,v2,V)) c= ( AcyclicPaths G) by Th43;

      hence thesis;

    end;

    registration

      let G, P;

      cluster ( AcyclicPaths P) -> finite;

      coherence by Lm6;

    end

    registration

      let G, v1, v2;

      cluster ( AcyclicPaths (v1,v2)) -> finite;

      coherence by Lm7;

    end

    registration

      let G, v1, v2, V;

      cluster ( AcyclicPaths (v1,v2,V)) -> finite;

      coherence by Lm8;

    end

    theorem :: GRAPH_5:59

    ( AcyclicPaths (v1,v2)) <> {} implies ex pe st pe in ( AcyclicPaths (v1,v2)) & for qe st qe in ( AcyclicPaths (v1,v2)) holds ( cost (pe,W)) <= ( cost (qe,W)) by Th50;

    theorem :: GRAPH_5:60

    ( AcyclicPaths (v1,v2,V)) <> {} implies ex pe st pe in ( AcyclicPaths (v1,v2,V)) & for qe st qe in ( AcyclicPaths (v1,v2,V)) holds ( cost (pe,W)) <= ( cost (qe,W)) by Th51;

    theorem :: GRAPH_5:61

    P is_orientedpath_of (v1,v2) & W is_weight>=0of G implies ex q be Simple oriented Chain of G st q is_shortestpath_of (v1,v2,W)

    proof

      assume that

       A1: P is_orientedpath_of (v1,v2) and

       A2: W is_weight>=0of G;

      ( AcyclicPaths (v1,v2)) <> {} by A1, Th41;

      then

      consider r be FinSequence of the carrier' of G such that

       A3: r in ( AcyclicPaths (v1,v2)) and

       A4: for s be FinSequence of the carrier' of G st s in ( AcyclicPaths (v1,v2)) holds ( cost (r,W)) <= ( cost (s,W)) by Th50;

      consider t be Simple oriented Chain of G such that

       A5: r = t and

       A6: t is_acyclicpath_of (v1,v2) by A3;

      take t;

      thus t is_orientedpath_of (v1,v2) by A6;

      hereby

        let s be oriented Chain of G;

        assume

         A7: s is_orientedpath_of (v1,v2);

        then

        consider x be Element of (the carrier' of G * ) such that

         A8: x in ( AcyclicPaths s) by Th41, SUBSET_1: 4;

        ( AcyclicPaths s) c= ( AcyclicPaths (v1,v2)) by A7, Th38;

        then

         A9: ( cost (r,W)) <= ( cost (x,W)) by A4, A8;

        ( cost (x,W)) <= ( cost (s,W)) by A2, A8, Th54;

        hence ( cost (t,W)) <= ( cost (s,W)) by A5, A9, XXREAL_0: 2;

      end;

    end;

    theorem :: GRAPH_5:62

    

     Th60: P is_orientedpath_of (v1,v2,V) & W is_weight>=0of G implies ex q be Simple oriented Chain of G st q is_shortestpath_of (v1,v2,V,W)

    proof

      assume that

       A1: P is_orientedpath_of (v1,v2,V) and

       A2: W is_weight>=0of G;

      ( AcyclicPaths (v1,v2,V)) <> {} by A1, Th42;

      then

      consider r be FinSequence of the carrier' of G such that

       A3: r in ( AcyclicPaths (v1,v2,V)) and

       A4: for s be FinSequence of the carrier' of G st s in ( AcyclicPaths (v1,v2,V)) holds ( cost (r,W)) <= ( cost (s,W)) by Th51;

      consider t be Simple oriented Chain of G such that

       A5: r = t and

       A6: t is_acyclicpath_of (v1,v2,V) by A3;

      take t;

      thus t is_orientedpath_of (v1,v2,V) by A6;

      hereby

        let s be oriented Chain of G;

        assume

         A7: s is_orientedpath_of (v1,v2,V);

        then

        consider x be Element of (the carrier' of G * ) such that

         A8: x in ( AcyclicPaths s) by Th42, SUBSET_1: 4;

        ( AcyclicPaths s) c= ( AcyclicPaths (v1,v2,V)) by A7, Th39;

        then

         A9: ( cost (r,W)) <= ( cost (x,W)) by A4, A8;

        ( cost (x,W)) <= ( cost (s,W)) by A2, A8, Th54;

        hence ( cost (t,W)) <= ( cost (s,W)) by A5, A9, XXREAL_0: 2;

      end;

    end;

    begin

    theorem :: GRAPH_5:63

    

     Th61: W is_weight>=0of G & P is_shortestpath_of (v1,v2,V,W) & v1 <> v2 & (for Q, v3 st not v3 in V & Q is_shortestpath_of (v1,v3,V,W) holds ( cost (P,W)) <= ( cost (Q,W))) implies P is_shortestpath_of (v1,v2,W)

    proof

      assume that

       A1: W is_weight>=0of G and

       A2: P is_shortestpath_of (v1,v2,V,W) and

       A3: v1 <> v2 and

       A4: for Q, v3 st not v3 in V & Q is_shortestpath_of (v1,v3,V,W) holds ( cost (P,W)) <= ( cost (Q,W));

      

       A5: P is_orientedpath_of (v1,v2,V) by A2;

      then

       A6: v1 in V by A3, Th29;

       A7:

      now

        let r be oriented Chain of G;

        assume

         A8: r is_orientedpath_of (v1,v2);

        per cases ;

          suppose

           A9: not ( vertices r) c= V;

          set FT = the Target of G, FS = the Source of G;

          consider i be Element of NAT , s,t be FinSequence of the carrier' of G such that

           A10: (i + 1) <= ( len r) and

           A11: not ( vertices (r /. (i + 1))) c= V and

           A12: ( len s) = i and

           A13: r = (s ^ t) and

           A14: ( vertices s) c= V by A9, Th18;

          (i + 1) <= (( len s) + ( len t)) by A10, A13, FINSEQ_1: 22;

          then

           A15: 1 <= ( len t) by A12, XREAL_1: 6;

          then

          consider j be Nat such that

           A16: ( len t) = (1 + j) by NAT_1: 10;

          reconsider s, t as oriented Chain of G by A13, Th9;

          reconsider j as Element of NAT by ORDINAL1:def 12;

          consider t1,t2 be FinSequence such that

           A17: ( len t1) = 1 and ( len t2) = j and

           A18: t = (t1 ^ t2) by A16, FINSEQ_2: 22;

          reconsider t1, t2 as oriented Chain of G by A18, Th9;

          

           A19: (r . (i + 1)) = (t . 1) by A12, A13, A15, Lm2

          .= (t1 . 1) by A17, A18, Lm1;

          

           A20: ( cost (t2,W)) >= 0 by A1, Th48;

          

           A21: r = ((s ^ t1) ^ t2) by A13, A18, FINSEQ_1: 32;

          then ( cost (r,W)) = (( cost ((s ^ t1),W)) + ( cost (t2,W))) by A1, Th44, Th52;

          then

           A22: ( cost (r,W)) >= (( cost ((s ^ t1),W)) + 0 qua Nat) by A20, XREAL_1: 7;

          set e = (r /. (i + 1));

          

           A23: e = (r . (i + 1)) by A10, FINSEQ_4: 15, NAT_1: 11;

          consider x be object such that

           A24: x in ( vertices e) and

           A25: not x in V by A11;

          

           A26: x = (FS . e) or x = (FT . e) by A24, TARSKI:def 2;

          1 in ( dom t1) by A17, FINSEQ_3: 25;

          then

          reconsider v3 = x as Vertex of G by A23, A19, A26, FINSEQ_2: 11, FUNCT_2: 5;

          

           A27: v1 = (FS . (r . 1)) by A8;

          hereby

            per cases ;

              suppose

               A28: i = 0 ;

              then

               A29: (FS . (t1 . 1)) = v1 by A8, A19;

              

               A30: (( vertices t1) \ {v3}) c= V

              proof

                let x be object;

                assume

                 A31: x in (( vertices t1) \ {v3});

                then

                 A32: not x in {v3} by XBOOLE_0:def 5;

                x in ( vertices t1) by A31, XBOOLE_0:def 5;

                then x in ( vertices (t1 /. 1)) by A17, Th23;

                then

                 A33: x = (FS . (t1 /. 1)) or x = (FT . (t1 /. 1)) by TARSKI:def 2;

                (FT . (t1 /. 1)) = v3 by A3, A5, A17, A23, A19, A25, A26, A27, A28, Th29, FINSEQ_4: 15;

                hence thesis by A6, A17, A29, A32, A33, FINSEQ_4: 15, TARSKI:def 1;

              end;

              v1 = (FS . e) by A8, A23, A28;

              then t1 is_orientedpath_of (v1,v3) by A3, A5, A17, A23, A19, A25, A26, Th29;

              then

               A34: t1 is_orientedpath_of (v1,v3,V) by A30;

              then

              consider q be Simple oriented Chain of G such that

               A35: q is_shortestpath_of (v1,v3,V,W) by A1, Th60;

              s = {} by A12, A28;

              then

               A36: (s ^ t1) = t1 by FINSEQ_1: 34;

              

               A37: ( cost (q,W)) <= ( cost (t1,W)) by A34, A35;

              ( cost (P,W)) <= ( cost (q,W)) by A4, A25, A35;

              then ( cost (P,W)) <= ( cost (t1,W)) by A37, XXREAL_0: 2;

              hence ( cost (P,W)) <= ( cost (r,W)) by A22, A36, XXREAL_0: 2;

            end;

              suppose

               A38: i <> 0 ;

              reconsider u = (s ^ t1) as oriented Chain of G by A21, Th9;

              

               A39: i < ( len r) by A10, NAT_1: 13;

              (i + 1) > ( 0 + 1) by A38, XREAL_1: 8;

              then

               A40: i >= 1 by NAT_1: 13;

              then

               A41: i in ( dom s) by A12, FINSEQ_3: 25;

               A42:

              now

                assume (FS . (r . (i + 1))) = v3;

                then

                 A43: v3 = (FT . (r . i)) by A40, A39, GRAPH_1:def 15;

                (r . i) = (s . i) by A12, A13, A40, Lm1;

                then v3 in ( vertices s) by A41, A43, Th22;

                hence contradiction by A14, A25;

              end;

              

               A44: (( vertices u) \ {v3}) c= V

              proof

                set V3 = {(FT . (t1 . 1))};

                let x be object;

                assume

                 A45: x in (( vertices u) \ {v3});

                then

                 A46: x in ( vertices u) by XBOOLE_0:def 5;

                ( vertices u) = (( vertices s) \/ V3) by A12, A17, A40, Th25;

                then

                 A47: x in ( vertices s) or x in V3 by A46, XBOOLE_0:def 3;

                 not x in {v3} by A45, XBOOLE_0:def 5;

                hence thesis by A10, A14, A19, A26, A42, A47, FINSEQ_4: 15, NAT_1: 11;

              end;

              ( len u) = (( len s) + ( len t1)) by FINSEQ_1: 22;

              then

               A48: u <> {} & (u . ( len u)) = (t1 . 1) by A17, Lm2;

              (u . 1) = (s . 1) by A12, A40, Lm1

              .= (r . 1) by A12, A13, A40, Lm1;

              then (FS . (u . 1)) = v1 by A8;

              then u is_orientedpath_of (v1,v3) by A23, A19, A26, A42, A48;

              then

               A49: u is_orientedpath_of (v1,v3,V) by A44;

              then

              consider q be Simple oriented Chain of G such that

               A50: q is_shortestpath_of (v1,v3,V,W) by A1, Th60;

              

               A51: ( cost (q,W)) <= ( cost (u,W)) by A49, A50;

              ( cost (P,W)) <= ( cost (q,W)) by A4, A25, A50;

              then ( cost (P,W)) <= ( cost (u,W)) by A51, XXREAL_0: 2;

              hence ( cost (P,W)) <= ( cost (r,W)) by A22, XXREAL_0: 2;

            end;

          end;

        end;

          suppose ( vertices r) c= V;

          then (( vertices r) \ {v2}) c= (V \ {v2}) by XBOOLE_1: 33;

          then (( vertices r) \ {v2}) c= V by XBOOLE_1: 1;

          then r is_orientedpath_of (v1,v2,V) by A8;

          hence ( cost (P,W)) <= ( cost (r,W)) by A2;

        end;

      end;

      P is_orientedpath_of (v1,v2) by A5;

      hence thesis by A7;

    end;

    theorem :: GRAPH_5:64

    W is_weight>=0of G & P is_shortestpath_of (v1,v2,V,W) & v1 <> v2 & V c= U & (for Q, v3 st not v3 in V & Q is_shortestpath_of (v1,v3,V,W) holds ( cost (P,W)) <= ( cost (Q,W))) implies P is_shortestpath_of (v1,v2,U,W)

    proof

      assume that

       A1: W is_weight>=0of G and

       A2: P is_shortestpath_of (v1,v2,V,W) and

       A3: v1 <> v2 and

       A4: V c= U and

       A5: for Q, v3 st not v3 in V & Q is_shortestpath_of (v1,v3,V,W) holds ( cost (P,W)) <= ( cost (Q,W));

      P is_shortestpath_of (v1,v2,W) by A1, A2, A3, A5, Th61;

      then

       A6: for q be oriented Chain of G st q is_orientedpath_of (v1,v2,U) holds ( cost (P,W)) <= ( cost (q,W));

      P is_orientedpath_of (v1,v2,V) by A2;

      then P is_orientedpath_of (v1,v2,U) by A4, Th30;

      hence thesis by A6;

    end;

    definition

      let G be Graph, pe be FinSequence of the carrier' of G, V be set, v1 be Vertex of G, W be Function;

      :: GRAPH_5:def19

      pred pe islongestInShortestpath V,v1,W means for v be Vertex of G st v in V & v <> v1 holds ex q be oriented Chain of G st q is_shortestpath_of (v1,v,V,W) & ( cost (q,W)) <= ( cost (pe,W));

    end

    ::$Notion-Name

    theorem :: GRAPH_5:65

    for G be finite oriented Graph, P,Q,R be oriented Chain of G, v1,v2,v3 be Element of G st e in the carrier' of G & W is_weight>=0of G & ( len P) >= 1 & P is_shortestpath_of (v1,v2,V,W) & v1 <> v2 & v1 <> v3 & R = (P ^ <*e*>) & Q is_shortestpath_of (v1,v3,V,W) & e orientedly_joins (v2,v3) & P islongestInShortestpath (V,v1,W) holds (( cost (Q,W)) <= ( cost (R,W)) implies Q is_shortestpath_of (v1,v3,(V \/ {v2}),W)) & (( cost (Q,W)) >= ( cost (R,W)) implies R is_shortestpath_of (v1,v3,(V \/ {v2}),W))

    proof

      let G be finite oriented Graph, P,Q,R be oriented Chain of G, v1,v2,v3 be Element of G;

      assume that

       A1: e in the carrier' of G and

       A2: W is_weight>=0of G and

       A3: ( len P) >= 1 and

       A4: P is_shortestpath_of (v1,v2,V,W) and

       A5: v1 <> v2 and

       A6: v1 <> v3 and

       A7: R = (P ^ <*e*>) and

       A8: Q is_shortestpath_of (v1,v3,V,W) and

       A9: e orientedly_joins (v2,v3) and

       A10: P islongestInShortestpath (V,v1,W);

      

       A11: P is_orientedpath_of (v1,v2,V) by A4;

      then

       A12: v1 in V by A5, Th29;

      set Eg = the carrier' of G;

      reconsider pe = <*e*> as FinSequence of Eg by A1, FINSEQ_1: 74;

      set V9 = (V \/ {v2});

      Q is_orientedpath_of (v1,v3,V) by A8;

      then

       A13: Q is_orientedpath_of (v1,v3,V9) by Th30, XBOOLE_1: 7;

      

       A14: ( len pe) = 1 & (pe . 1) = e by FINSEQ_1: 40;

      then

      consider s be Simple oriented Chain of G such that

       A15: s is_shortestpath_of (v1,v3,V9,W) by A2, A3, A7, A9, A11, Th32, Th60;

      

       A16: R is_orientedpath_of (v1,v3,V9) by A3, A7, A9, A11, A14, Th32;

       A17:

      now

        assume

         A18: ( cost (Q,W)) <= ( cost (s,W));

        hereby

          assume ( cost (Q,W)) <= ( cost (R,W));

          now

            let u be oriented Chain of G;

            assume u is_orientedpath_of (v1,v3,V9);

            then ( cost (s,W)) <= ( cost (u,W)) by A15;

            hence ( cost (Q,W)) <= ( cost (u,W)) by A18, XXREAL_0: 2;

          end;

          hence Q is_shortestpath_of (v1,v3,V9,W) by A13;

        end;

        hereby

          assume

           A19: ( cost (Q,W)) >= ( cost (R,W));

          now

            let u be oriented Chain of G;

            assume u is_orientedpath_of (v1,v3,V9);

            then ( cost (s,W)) <= ( cost (u,W)) by A15;

            then ( cost (Q,W)) <= ( cost (u,W)) by A18, XXREAL_0: 2;

            hence ( cost (R,W)) <= ( cost (u,W)) by A19, XXREAL_0: 2;

          end;

          hence R is_shortestpath_of (v1,v3,V9,W) by A16;

        end;

      end;

      set FT = the Target of G, FS = the Source of G;

      

       A20: (FS . e) = v2 & (FT . e) = v3 by A9, GRAPH_4:def 1;

      

       A21: s is_orientedpath_of (v1,v3,V9) by A15;

      then

       A22: s is_orientedpath_of (v1,v3);

      then

       A23: (FT . (s . ( len s))) = v3;

      s <> {} by A22;

      then

       A24: ( len s) >= 1 by FINSEQ_1: 20;

      per cases ;

        suppose ( len s) >= 2;

        then

        consider k be Nat such that

         A25: ( len s) = ((1 + 1) + k) by NAT_1: 10;

        

         A26: (V9 \ {v2}) = (V \ {v2}) by XBOOLE_1: 40;

        reconsider k as Element of NAT by ORDINAL1:def 12;

        

         A27: ( len s) = (1 + (1 + k)) by A25;

        then

        consider s1,s2 be FinSequence such that

         A28: ( len s1) = (1 + k) and

         A29: ( len s2) = 1 and

         A30: s = (s1 ^ s2) by FINSEQ_2: 22;

        reconsider s1, s2 as Simple oriented Chain of G by A30, Th12;

        

         A31: ( len s1) >= 1 by A28, NAT_1: 12;

        

         A32: (FS . (s . 1)) = v1 by A22;

        then

         A33: (FS . (s1 . 1)) = v1 by A30, A31, Lm1;

        ( len s2) = 1 by A29;

        then

         A34: not v3 in ( vertices s1) by A6, A23, A30, A31, A32, Th16;

        

         A35: (s2 . 1) = (s . ( len s)) by A27, A28, A29, A30, Lm2;

        

        then

         A36: (( vertices s) \ {v3}) = ((( vertices s1) \/ {v3}) \ {v3}) by A23, A28, A29, A30, Th25, NAT_1: 12

        .= (( vertices s1) \ {v3}) by XBOOLE_1: 40

        .= ( vertices s1) by A34, ZFMISC_1: 57;

        then ( vertices s1) c= V9 by A21;

        then (( vertices s1) \ {v2}) c= (V9 \ {v2}) by XBOOLE_1: 33;

        then

         A37: (( vertices s1) \ {v2}) c= V by A26, XBOOLE_1: 1;

        

         A38: ( len s1) < ( len s) by A27, A28, NAT_1: 13;

        then

         A39: (FS . (s . (( len s1) + 1))) = (FT . (s . ( len s1))) by A31, GRAPH_1:def 15;

        

         A40: (s1 . ( len s1)) = (s . ( len s1)) by A30, A31, Lm1;

        then

         A41: (FS . (s2 . 1)) = (FT . (s1 . ( len s1))) by A27, A28, A35, A31, A38, GRAPH_1:def 15;

        

         A42: ( cost (s,W)) = (( cost (s1,W)) + ( cost (s2,W))) by A2, A30, Th44, Th52;

        

         A43: not v1 in ( vertices s2) by A6, A23, A29, A30, A31, A32, Th16;

        hereby

          per cases ;

            suppose v2 in ( vertices s1);

            then

            consider i such that

             A44: 1 <= i and

             A45: i <= ( len s1) and

             A46: v2 = (FT . (s1 . i)) by A5, A33, Th26;

            (s2 /. 1) in Eg by A1;

            then

             A47: (s2 . 1) in Eg by A29, FINSEQ_4: 15;

            hereby

              per cases ;

                suppose

                 A48: (FS . (s2 . 1)) = v2;

                s1 <> {} by A28;

                then s1 is_orientedpath_of (v1,v2) by A33, A41, A48;

                then s1 is_orientedpath_of (v1,v2,V) by A37;

                then

                 A49: ( cost (P,W)) <= ( cost (s1,W)) by A4;

                (s2 . 1) = e by A1, A23, A20, A35, A47, A48, GRAPH_1:def 7;

                then s2 = pe by A29, FINSEQ_1: 40;

                then ( cost (R,W)) = (( cost (P,W)) + ( cost (s2,W))) by A2, A7, Th44, Th52;

                then

                 A50: ( cost (R,W)) <= ( cost (s,W)) by A42, A49, XREAL_1: 7;

                hereby

                  assume ( cost (Q,W)) <= ( cost (R,W));

                  then

                   A51: ( cost (Q,W)) <= ( cost (s,W)) by A50, XXREAL_0: 2;

                  now

                    let u be oriented Chain of G;

                    assume u is_orientedpath_of (v1,v3,V9);

                    then ( cost (s,W)) <= ( cost (u,W)) by A15;

                    hence ( cost (Q,W)) <= ( cost (u,W)) by A51, XXREAL_0: 2;

                  end;

                  hence Q is_shortestpath_of (v1,v3,V9,W) by A13;

                end;

                hereby

                  assume ( cost (Q,W)) >= ( cost (R,W));

                  now

                    let u be oriented Chain of G;

                    assume u is_orientedpath_of (v1,v3,V9);

                    then ( cost (s,W)) <= ( cost (u,W)) by A15;

                    hence ( cost (R,W)) <= ( cost (u,W)) by A50, XXREAL_0: 2;

                  end;

                  hence R is_shortestpath_of (v1,v3,V9,W) by A16;

                end;

              end;

                suppose

                 A52: (FS . (s2 . 1)) <> v2;

                ( len s1) in ( dom s1) by A31, FINSEQ_3: 25;

                then

                reconsider vx = (FT . (s1 . ( len s1))) as Vertex of G by FINSEQ_2: 11, FUNCT_2: 5;

                

                 A53: not vx in {v2} by A41, A52, TARSKI:def 1;

                ( len s1) in ( dom s1) by A31, FINSEQ_3: 25;

                then

                 A54: vx in ( vertices s1) by Th22;

                ( vertices s1) c= V9 by A21, A36;

                then

                 A55: vx in V by A54, A53, XBOOLE_0:def 3;

                 {vx} c= V by A55, TARSKI:def 1;

                then

                 A56: (V \/ {vx}) c= V by XBOOLE_1: 8;

                1 in ( dom s2) by A29, FINSEQ_3: 25;

                then vx <> v1 by A25, A28, A35, A40, A43, A39, Th22;

                then

                consider q9 be oriented Chain of G such that

                 A57: q9 is_shortestpath_of (v1,vx,V,W) and

                 A58: ( cost (q9,W)) <= ( cost (P,W)) by A10, A55;

                consider j be Nat such that

                 A59: ( len s1) = (i + j) by A45, NAT_1: 10;

                

                 A60: q9 is_orientedpath_of (v1,vx,V) by A57;

                then

                 A61: q9 is_orientedpath_of (v1,vx);

                then q9 <> {} ;

                then

                 A62: ( len q9) >= 1 by FINSEQ_1: 20;

                (FT . (q9 . ( len q9))) = vx by A61;

                then

                reconsider qx = (q9 ^ s2) as oriented Chain of G by A25, A28, A35, A40, A39, Th10;

                ( len qx) = (( len q9) + 1) by A29, FINSEQ_1: 22;

                then

                 A63: qx <> {} & (FT . (qx . ( len qx))) = v3 by A23, A29, A35, Lm2;

                (FS . (q9 . 1)) = v1 by A61;

                then (FS . (qx . 1)) = v1 by A62, Lm1;

                then

                 A64: qx is_orientedpath_of (v1,v3) by A63;

                (( vertices q9) \ {vx}) c= V by A60;

                then ( vertices q9) c= (V \/ {vx}) by XBOOLE_1: 44;

                then ( vertices q9) c= V by A56;

                then

                 A65: (( vertices q9) \ {v3}) c= (V \ {v3}) by XBOOLE_1: 33;

                ( vertices qx) = (( vertices q9) \/ {v3}) by A23, A29, A35, A62, Th25;

                then (( vertices qx) \ {v3}) = (( vertices q9) \ {v3}) by XBOOLE_1: 40;

                then (( vertices qx) \ {v3}) c= V by A65, XBOOLE_1: 1;

                then qx is_orientedpath_of (v1,v3,V) by A64;

                then

                 A66: ( cost (Q,W)) <= ( cost (qx,W)) by A8;

                reconsider j as Element of NAT by ORDINAL1:def 12;

                consider t1,t2 be FinSequence such that

                 A67: ( len t1) = i and ( len t2) = j and

                 A68: s1 = (t1 ^ t2) by A59, FINSEQ_2: 22;

                reconsider t1, t2 as Simple oriented Chain of G by A68, Th12;

                

                 A69: (FT . (t1 . ( len t1))) = v2 by A44, A46, A67, A68, Lm1;

                ( vertices t1) c= ( vertices (t1 ^ t2)) by Th24;

                then (( vertices t1) \ {v2}) c= (( vertices s1) \ {v2}) by A68, XBOOLE_1: 33;

                then

                 A70: (( vertices t1) \ {v2}) c= V by A37;

                t1 <> {} & (FS . (t1 . 1)) = v1 by A33, A44, A67, A68, Lm1;

                then t1 is_orientedpath_of (v1,v2) by A69;

                then t1 is_orientedpath_of (v1,v2,V) by A70;

                then

                 A71: ( cost (P,W)) <= ( cost (t1,W)) by A4;

                

                 A72: ( cost (t2,W)) >= 0 by A2, Th48;

                ( cost (s1,W)) = (( cost (t1,W)) + ( cost (t2,W))) by A2, A68, Th44, Th52;

                then (( cost (t1,W)) + 0 qua Nat) <= ( cost (s1,W)) by A72, XREAL_1: 7;

                then ( cost (P,W)) <= ( cost (s1,W)) by A71, XXREAL_0: 2;

                then

                 A73: ( cost (q9,W)) <= ( cost (s1,W)) by A58, XXREAL_0: 2;

                ( cost (qx,W)) = (( cost (q9,W)) + ( cost (s2,W))) by A2, Th44, Th52;

                then ( cost (qx,W)) <= ( cost (s,W)) by A42, A73, XREAL_1: 7;

                then

                 A74: ( cost (Q,W)) <= ( cost (s,W)) by A66, XXREAL_0: 2;

                hereby

                  assume ( cost (Q,W)) <= ( cost (R,W));

                  now

                    let u be oriented Chain of G;

                    assume u is_orientedpath_of (v1,v3,V9);

                    then ( cost (s,W)) <= ( cost (u,W)) by A15;

                    hence ( cost (Q,W)) <= ( cost (u,W)) by A74, XXREAL_0: 2;

                  end;

                  hence Q is_shortestpath_of (v1,v3,V9,W) by A13;

                end;

                hereby

                  assume ( cost (Q,W)) >= ( cost (R,W));

                  then

                   A75: ( cost (R,W)) <= ( cost (s,W)) by A74, XXREAL_0: 2;

                  now

                    let u be oriented Chain of G;

                    assume u is_orientedpath_of (v1,v3,V9);

                    then ( cost (s,W)) <= ( cost (u,W)) by A15;

                    hence ( cost (R,W)) <= ( cost (u,W)) by A75, XXREAL_0: 2;

                  end;

                  hence R is_shortestpath_of (v1,v3,V9,W) by A16;

                end;

              end;

            end;

          end;

            suppose not v2 in ( vertices s1);

            then

             A76: (( vertices s1) \ {v2}) = ( vertices s1) by ZFMISC_1: 57;

            then (( vertices s1) \ {v2}) c= V9 by A21, A36;

            then (( vertices s) \ {v3}) c= V by A36, A76, XBOOLE_1: 43;

            then s is_orientedpath_of (v1,v3,V) by A22;

            hence thesis by A8, A17;

          end;

        end;

      end;

        suppose ( len s) < (1 + 1);

        then

         A77: ( len s) <= 1 by NAT_1: 13;

        then

         A78: ( len s) = 1 by A24, XXREAL_0: 1;

        

         A79: ( vertices s) = ( vertices (s /. 1)) by A24, A77, Th23, XXREAL_0: 1;

        (( vertices s) \ {v3}) c= V

        proof

          let x be object;

          assume

           A80: x in (( vertices s) \ {v3});

          then

           A81: not x in {v3} by XBOOLE_0:def 5;

          x in ( vertices (s /. 1)) by A79, A80, XBOOLE_0:def 5;

          then

           A82: x = (FS . (s /. 1)) or x = (FT . (s /. 1)) by TARSKI:def 2;

          

           A83: (s /. 1) = (s . 1) by A24, FINSEQ_4: 15;

          v3 = (FT . (s . ( len s))) by A22

          .= (FT . (s /. 1)) by A78, FINSEQ_4: 15;

          hence thesis by A22, A12, A81, A82, A83, TARSKI:def 1;

        end;

        then s is_orientedpath_of (v1,v3,V) by A22;

        hence thesis by A8, A17;

      end;

    end;