graphsp.miz



    begin

    reserve x,y,X for set,

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

p for FinSequence of X,

ii for Integer;

    theorem :: GRAPHSP:1

    

     Th1: for p be FinSequence, x be set holds not x in ( rng p) & p is one-to-one iff (p ^ <*x*>) is one-to-one

    proof

      let p be FinSequence, x be set;

      

       A1: ( rng <*x*>) = {x} by FINSEQ_1: 38;

      ( rng p) misses ( rng <*x*>) & p is one-to-one & <*x*> is one-to-one iff (p ^ <*x*>) is one-to-one by FINSEQ_3: 91;

      hence thesis by A1, FINSEQ_3: 93, ZFMISC_1: 48, ZFMISC_1: 50;

    end;

    theorem :: GRAPHSP:2

    

     Th2: 1 <= ii & ii <= ( len p) implies (p . ii) in X

    proof

      assume that

       A1: 1 <= ii and

       A2: ii <= ( len p);

      reconsider ii as Element of NAT by A1, INT_1: 3;

      ii in ( dom p) by A1, A2, FINSEQ_3: 25;

      hence thesis by PARTFUN1: 4;

    end;

    theorem :: GRAPHSP:3

    

     Th3: 1 <= ii & ii <= ( len p) implies (p /. ii) = (p . ii)

    proof

      assume that

       A1: 1 <= ii and

       A2: ii <= ( len p);

      reconsider ii as Element of NAT by A1, INT_1: 3;

      ii in ( dom p) by A1, A2, FINSEQ_3: 25;

      hence thesis by PARTFUN1:def 6;

    end;

    reserve G for Graph,

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

p,q for oriented Chain of G,

W for Function,

U,V,e,ee for set,

v1,v2,v3,v4 for Vertex of G;

    theorem :: GRAPHSP:4

    

     Th4: W is_weight_of G & ( len pe) = 1 implies ( cost (pe,W)) = (W . (pe . 1))

    proof

      assume that

       A1: W is_weight_of G and

       A2: ( len pe) = 1;

      

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

      set f = ( RealSequence (pe,W));

      reconsider f1 = (f . 1) as Element of REAL by XREAL_0:def 1;

      ( dom f) = ( dom pe) by A1, GRAPH_5:def 15;

      then ( len f) = 1 by A2, FINSEQ_3: 29;

      then

       A4: f = <*f1*> by FINSEQ_1: 40;

      

      thus ( cost (pe,W)) = ( Sum f) by GRAPH_5:def 16

      .= (f . 1) by A4, FINSOP_1: 11

      .= (W . (pe . 1)) by A1, A3, GRAPH_5:def 15;

    end;

    theorem :: GRAPHSP:5

    

     Th5: e in the carrier' of G implies <*e*> is Simple oriented Chain of G

    proof

      assume e in the carrier' of G;

      then

       A1: <*e*> is FinSequence of the carrier' of G by FINSEQ_1: 74;

      ( len <*e*>) = 1 by FINSEQ_1: 40;

      hence thesis by A1, GRAPH_5: 15;

    end;

    

     Lm1: for n be Nat holds for p,q be FinSequence st 1 <= n & n <= ( len p) holds (p . n) = ((p ^ q) . n)

    proof

      let n be Nat;

      let p,q be FinSequence;

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

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

      hence thesis by FINSEQ_1:def 7;

    end;

    

     Lm2: for p,q be FinSequence st 1 <= n & n <= ( len q) holds (q . n) = ((p ^ q) . (( len p) + n))

    proof

      let p,q be FinSequence;

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

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

      hence thesis by FINSEQ_1:def 7;

    end;

    theorem :: GRAPHSP:6

    

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

    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;

      consider vs be FinSequence of the carrier of G such that

       A4: vs is_oriented_vertex_seq_of p and

       A5: 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;

      

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

      then

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

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

      then

       A8: ( len p) >= (( len pe) + 1) by A3, XREAL_1: 7;

      then

       A9: (( len pe) + 1) < ( len vs) by A6, NAT_1: 13;

      

       A10: ( len p) > ( len pe) by A8, NAT_1: 13;

      then

       A11: ( len p) >= 1 by A2, XXREAL_0: 2;

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

      

      then

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

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

      

       A13: (p . ( len pe)) orientedly_joins ((vs /. ( len pe)),(vs /. (( len pe) + 1))) by A2, A4, A10, GRAPH_4:def 5;

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

      

      then

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

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

      

       A15: 1 < (( len pe) + 1) by A2, NAT_1: 13;

      then

       A16: (p . (( len pe) + 1)) orientedly_joins ((vs /. (( len pe) + 1)),(vs /. ((( len pe) + 1) + 1))) by A4, A8, GRAPH_4:def 5;

      (FT . (pe . ( len pe))) = (FT . (p . ( len pe))) by A1, A2, Lm1

      .= (vs /. (( len pe) + 1)) by A13, GRAPH_4:def 1

      .= (vs . (( len pe) + 1)) by A15, A9, FINSEQ_4: 15;

      hence (FT . (p . ( len p))) <> (FT . (pe . ( len pe))) by A5, A14, A15, A9;

      assume

       A17: (FS . (p . 1)) = (FS . (qe . 1));

      (FS . (qe . 1)) = (FS . (p . (( len pe) + 1))) by A1, A3, Lm2

      .= (vs /. (( len pe) + 1)) by A16, GRAPH_4:def 1

      .= (vs . (( len pe) + 1)) by A15, A9, FINSEQ_4: 15;

      hence contradiction by A5, A15, A9, A12, A17;

    end;

    begin

    theorem :: GRAPHSP:7

    

     Th7: p is_orientedpath_of (v1,v2,V) iff p is_orientedpath_of (v1,v2,(V \/ {v2}))

    proof

      set V9 = (V \/ {v2});

      thus p is_orientedpath_of (v1,v2,V) implies p is_orientedpath_of (v1,v2,V9) by GRAPH_5: 32, XBOOLE_1: 7;

      assume

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

      then (( vertices p) \ {v2}) c= V9 by GRAPH_5:def 4;

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

      then

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

      p is_orientedpath_of (v1,v2) by A1, GRAPH_5:def 4;

      hence thesis by A2, GRAPH_5:def 4;

    end;

    theorem :: GRAPHSP:8

    

     Th8: p is_shortestpath_of (v1,v2,V,W) iff p is_shortestpath_of (v1,v2,(V \/ {v2}),W)

    proof

      set V9 = (V \/ {v2});

      hereby

        assume

         A1: p is_shortestpath_of (v1,v2,V,W);

         A2:

        now

          let q;

          assume q is_orientedpath_of (v1,v2,V9);

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

          hence ( cost (p,W)) <= ( cost (q,W)) by A1, GRAPH_5:def 18;

        end;

        p is_orientedpath_of (v1,v2,V) by A1, GRAPH_5:def 18;

        then p is_orientedpath_of (v1,v2,V9) by Th7;

        hence p is_shortestpath_of (v1,v2,V9,W) by A2, GRAPH_5:def 18;

      end;

      assume

       A3: p is_shortestpath_of (v1,v2,V9,W);

       A4:

      now

        let q;

        assume q is_orientedpath_of (v1,v2,V);

        then q is_orientedpath_of (v1,v2,V9) by Th7;

        hence ( cost (p,W)) <= ( cost (q,W)) by A3, GRAPH_5:def 18;

      end;

      p is_orientedpath_of (v1,v2,V9) by A3, GRAPH_5:def 18;

      then p is_orientedpath_of (v1,v2,V) by Th7;

      hence thesis by A4, GRAPH_5:def 18;

    end;

    theorem :: GRAPHSP:9

    

     Th9: p is_shortestpath_of (v1,v2,V,W) & q is_shortestpath_of (v1,v2,V,W) implies ( cost (p,W)) = ( cost (q,W))

    proof

      assume that

       A1: p is_shortestpath_of (v1,v2,V,W) and

       A2: q is_shortestpath_of (v1,v2,V,W);

      q is_orientedpath_of (v1,v2,V) by A2, GRAPH_5:def 18;

      then

       A3: ( cost (p,W)) <= ( cost (q,W)) by A1, GRAPH_5:def 18;

      p is_orientedpath_of (v1,v2,V) by A1, GRAPH_5:def 18;

      then ( cost (q,W)) <= ( cost (p,W)) by A2, GRAPH_5:def 18;

      hence thesis by A3, XXREAL_0: 1;

    end;

    theorem :: GRAPHSP:10

    

     Th10: for G be oriented Graph, v1,v2 be Vertex of G, e1,e2 be set st e1 in the carrier' of G & e2 in the carrier' of G & e1 orientedly_joins (v1,v2) & e2 orientedly_joins (v1,v2) holds e1 = e2

    proof

      let G be oriented Graph, v1,v2 be Vertex of G, e1,e2 be set;

      assume that

       A1: e1 in the carrier' of G & e2 in the carrier' of G and

       A2: e1 orientedly_joins (v1,v2) and

       A3: e2 orientedly_joins (v1,v2);

      

       A4: (the Source of G . e2) = v1 & (the Target of G . e2) = v2 by A3, GRAPH_4:def 1;

      (the Source of G . e1) = v1 & (the Target of G . e1) = v2 by A2, GRAPH_4:def 1;

      hence thesis by A1, A4, GRAPH_1:def 7;

    end;

    

     Lm3: 1 <= i & i <= ( len pe) implies (the Source of G . (pe . i)) in the carrier of G & (the Target of G . (pe . i)) in the carrier of G

    proof

      assume 1 <= i & i <= ( len pe);

      then i in ( dom pe) by FINSEQ_3: 25;

      hence thesis by GRAPH_5: 8;

    end;

    theorem :: GRAPHSP:11

    

     Th11: the carrier of G = (U \/ V) & v1 in U & v2 in V & (for v3, v4 st v3 in U & v4 in V holds not (ex e st e in the carrier' of G & e orientedly_joins (v3,v4))) implies not ex p st p is_orientedpath_of (v1,v2)

    proof

      assume that

       A1: the carrier of G = (U \/ V) and

       A2: v1 in U and

       A3: v2 in V and

       A4: for v3, v4 st v3 in U & v4 in V holds not (ex e st e in the carrier' of G & e orientedly_joins (v3,v4));

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

      given p such that

       A5: p is_orientedpath_of (v1,v2);

      p <> {} by A5, GRAPH_5:def 3;

      then

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

      defpred PP[ Nat] means $1 >= 1 & $1 <= ( len p) & (FS . (p . $1)) in U;

      

       A7: for k be Nat st PP[k] holds k <= ( len p);

      (FS . (p . 1)) = v1 by A5, GRAPH_5:def 3;

      then

       A8: ex k be Nat st PP[k] by A2, A6;

      consider k be Nat such that

       A9: PP[k] & for n be Nat st PP[n] holds n <= k from NAT_1:sch 6( A7, A8);

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

      reconsider vx = (FS . (p . k)) as Vertex of G by A9, Lm3;

      

       A10: (p . k) in the carrier' of G by A9, Th2;

      

       A11: (FT . (p . ( len p))) = v2 by A5, GRAPH_5:def 3;

      per cases ;

        suppose k = ( len p);

        then (p . k) orientedly_joins (vx,v2) by A11, GRAPH_4:def 1;

        hence contradiction by A3, A4, A9, A10;

      end;

        suppose k <> ( len p);

        then

         A12: k < ( len p) by A9, XXREAL_0: 1;

        

         A13: k < (k + 1) by NAT_1: 13;

         A14:

        now

          assume

           A15: (FS . (p . (k + 1))) in U;

          (k + 1) <= ( len p) & 1 <= (k + 1) by A12, INT_1: 7, NAT_1: 12;

          hence contradiction by A9, A13, A15;

        end;

        reconsider vy = (FT . (p . k)) as Vertex of G by A9, Lm3;

        

         A16: (p . k) orientedly_joins (vx,vy) by GRAPH_4:def 1;

        (FS . (p . (k + 1))) = (FT . (p . k)) by A9, A12, GRAPH_1:def 15;

        then vy in V by A1, A2, A14, XBOOLE_0:def 3;

        hence contradiction by A4, A9, A10, A16;

      end;

    end;

    

     Lm4: 1 <= i & i <= ( len pe) & (v1 = (the Source of G . (pe . i)) or v1 = (the Target of G . (pe . i))) implies v1 in ( vertices pe)

    proof

      assume that

       A1: 1 <= i & i <= ( len pe) and

       A2: v1 = (the Source of G . (pe . i)) or v1 = (the Target of G . (pe . i));

      i in ( dom pe) by A1, FINSEQ_3: 25;

      hence thesis by A2, GRAPH_5: 24;

    end;

    theorem :: GRAPHSP:12

    

     Th12: the carrier of G = (U \/ V) & v1 in U & (for v3, v4 st v3 in U & v4 in V holds not (ex e st e in the carrier' of G & e orientedly_joins (v3,v4))) & p is_orientedpath_of (v1,v2) implies p is_orientedpath_of (v1,v2,U)

    proof

      assume that

       A1: the carrier of G = (U \/ V) and

       A2: v1 in U and

       A3: for v3, v4 st v3 in U & v4 in V holds not (ex e st e in the carrier' of G & e orientedly_joins (v3,v4)) and

       A4: p is_orientedpath_of (v1,v2);

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

       A5:

      now

        assume not ( vertices p) c= U;

        then

        consider i be Element of NAT , q,r be FinSequence of the carrier' of G such that

         A6: (i + 1) <= ( len p) and

         A7: not ( vertices (p /. (i + 1))) c= U and

         A8: ( len q) = i and

         A9: p = (q ^ r) and

         A10: ( vertices q) c= U by GRAPH_5: 20;

        

         A11: (p . (i + 1)) in the carrier' of G by A6, Th2, NAT_1: 12;

        (p /. (i + 1)) = (p . (i + 1)) by A6, FINSEQ_4: 15, NAT_1: 12;

        then

         A12: ( vertices (p /. (i + 1))) = {(FS . (p . (i + 1))), (FT . (p . (i + 1)))} by GRAPH_5:def 1;

         A13:

        now

          assume (FS . (p . (i + 1))) in U & (FT . (p . (i + 1))) in U;

          then (( vertices (p /. (i + 1))) \/ U) = U by A12, ZFMISC_1: 42;

          hence contradiction by A7, XBOOLE_1: 7;

        end;

        

         A14: 1 <= (i + 1) by NAT_1: 12;

        then

        reconsider vy = (FT . (p . (i + 1))) as Vertex of G by A6, Lm3;

        

         A15: vy in U or vy in V by A1, A2, XBOOLE_0:def 3;

        per cases ;

          suppose

           A16: i = 0 ;

          then (FS . (p . (i + 1))) = v1 by A4, GRAPH_5:def 3;

          then (p . (i + 1)) orientedly_joins (v1,vy) by GRAPH_4:def 1;

          hence contradiction by A2, A3, A4, A13, A11, A15, A16, GRAPH_5:def 3;

        end;

          suppose

           A17: i <> 0 ;

          reconsider vx = (FS . (p . (i + 1))) as Vertex of G by A6, A14, Lm3;

          hereby

            per cases ;

              suppose

               A18: vx in U;

              (p . (i + 1)) orientedly_joins (vx,vy) by GRAPH_4:def 1;

              hence contradiction by A3, A6, A14, A13, A15, A18, Th2;

            end;

              suppose

               A19: not vx in U;

              

               A20: i < ( len p) by A6, NAT_1: 13;

              

               A21: i >= (1 + 0 ) by A17, INT_1: 7;

              then

              reconsider vq = (FT . (q . i)) as Vertex of G by A8, Lm3;

              

               A22: vq in ( vertices q) by A8, A21, Lm4;

              (FT . (q . i)) = (FT . (p . i)) by A8, A9, A21, Lm1

              .= (FS . (p . (i + 1))) by A21, A20, GRAPH_1:def 15;

              hence contradiction by A10, A19, A22;

            end;

          end;

        end;

      end;

      (( vertices p) \ {v2}) c= ( vertices p) by XBOOLE_1: 36;

      then (( vertices p) \ {v2}) c= U by A5;

      hence thesis by A4, GRAPH_5:def 4;

    end;

    begin

    reserve G for finite Graph,

P,Q for oriented Chain of G,

v1,v2,v3 for Vertex of G;

    theorem :: GRAPHSP:13

    

     Th13: W is_weight>=0of G & P is_shortestpath_of (v1,v2,V,W) & v1 <> v2 & v1 <> v3 & Q is_shortestpath_of (v1,v3,V,W) & not (ex e st e in the carrier' of G & e orientedly_joins (v2,v3)) & P islongestInShortestpath (V,v1,W) implies Q is_shortestpath_of (v1,v3,(V \/ {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: v1 <> v3 and

       A5: Q is_shortestpath_of (v1,v3,V,W) and

       A6: not (ex e st e in the carrier' of G & e orientedly_joins (v2,v3)) and

       A7: P islongestInShortestpath (V,v1,W);

      set V9 = (V \/ {v2}), FS = the Source of G, FT = the Target of G;

       A8:

      now

        let S be oriented Chain of G;

        assume

         A9: S is_orientedpath_of (v1,v3,V9);

        then

        consider s be Simple oriented Chain of G such that

         A10: s is_shortestpath_of (v1,v3,V9,W) by A1, GRAPH_5: 62;

        

         A11: ( cost (s,W)) <= ( cost (S,W)) by A9, A10, GRAPH_5:def 18;

        

         A12: s is_orientedpath_of (v1,v3,V9) by A10, GRAPH_5:def 18;

        then

         A13: s is_orientedpath_of (v1,v3) by GRAPH_5:def 4;

        then

         A14: (FS . (s . 1)) = v1 by GRAPH_5:def 3;

        s <> {} by A13, GRAPH_5:def 3;

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

        then

        consider i be Nat such that

         A15: ( len s) = (1 + i) by NAT_1: 10;

        

         A16: (( vertices s) \ {v3}) c= V9 by A12, GRAPH_5:def 4;

        

         A17: (FT . (s . ( len s))) = v3 by A13, GRAPH_5:def 3;

        consider s1,s2 be FinSequence such that

         A18: ( len s1) = i and

         A19: ( len s2) = 1 and

         A20: s = (s1 ^ s2) by A15, FINSEQ_2: 22;

        reconsider s1, s2 as Simple oriented Chain of G by A20, GRAPH_5: 14;

        reconsider vx = (FS . (s2 . 1)) as Vertex of G by A19, Lm3;

        

         A21: (s2 . 1) = (s . ( len s)) by A15, A18, A19, A20, Lm2;

         A22:

        now

          assume vx = v2;

          then

           A23: (s2 . 1) orientedly_joins (v2,v3) by A21, A17, GRAPH_4:def 1;

          1 in ( dom s2) by A19, FINSEQ_3: 25;

          hence contradiction by A6, A23, FINSEQ_2: 11;

        end;

        per cases ;

          suppose

           A24: not v2 in ( vertices s) or v2 = v3;

          set Vs = ( vertices s);

          ((Vs \ {v3}) \ {v2}) c= V by A16, XBOOLE_1: 43;

          then

           A25: (Vs \ ( {v3} \/ {v2})) c= V by XBOOLE_1: 41;

          now

            per cases by A24;

              suppose

               A26: not v2 in ( vertices s);

              ((Vs \ {v2}) \ {v3}) c= V by A25, XBOOLE_1: 41;

              hence (Vs \ {v3}) c= V by A26, ZFMISC_1: 57;

            end;

              suppose v2 = v3;

              hence (Vs \ {v3}) c= V by A25;

            end;

          end;

          then s is_orientedpath_of (v1,v3,V) by A13, GRAPH_5:def 4;

          then ( cost (Q,W)) <= ( cost (s,W)) by A5, GRAPH_5:def 18;

          hence ( cost (Q,W)) <= ( cost (S,W)) by A11, XXREAL_0: 2;

        end;

          suppose

           A27: v2 in ( vertices s) & v2 <> v3;

          

           A28: ( len s1) < ( len s) by A15, A18, NAT_1: 13;

          consider j such that

           A29: 1 <= j and

           A30: j <= ( len s) and

           A31: v2 = (FT . (s . j)) by A3, A14, A27, GRAPH_5: 28;

          ( len s1) <> 0 by A15, A18, A17, A27, A29, A30, A31, XXREAL_0: 1;

          then

           A32: ( len s1) >= ( 0 + 1) by INT_1: 7;

          vx = (FS . (s . (( len s1) + 1))) by A19, A20, Lm2

          .= (FT . (s . ( len s1))) by A32, A28, GRAPH_1:def 15;

          then vx = (FT . (s1 . ( len s1))) by A20, A32, Lm1;

          then

           A33: vx in ( vertices s1) by A32, Lm4;

           not vx in {v2} by A22, TARSKI:def 1;

          then

           A34: vx in (( vertices s1) \ {v2}) by A33, XBOOLE_0:def 5;

           A35:

          now

            assume j > ( len s1);

            then j >= (( len s1) + 1) by INT_1: 7;

            hence contradiction by A15, A18, A17, A27, A30, A31, XXREAL_0: 1;

          end;

          then

          consider k be Nat such that

           A36: ( len s1) = (j + k) by NAT_1: 10;

          consider t1,t2 be FinSequence such that

           A37: ( len t1) = j and ( len t2) = k and

           A38: s1 = (t1 ^ t2) by A36, FINSEQ_2: 22;

          reconsider t1, t2 as Simple oriented Chain of G by A38, GRAPH_5: 14;

          

           A39: t1 <> {} by A29, A37;

          set Vt = ( vertices t1);

          (( vertices (s1 ^ s2)) \ {v3}) c= V9 by A12, A20, GRAPH_5:def 4;

          then

           A40: (( vertices (t1 ^ t2)) \ {v3}) c= V9 by A38, GRAPH_5: 23;

          then

           A41: (Vt \ {v3}) c= V9 by GRAPH_5: 23;

          

           A42: ( len s2) >= 1 by A19;

          then not v3 in ( vertices s1) by A4, A20, A14, A17, A32, GRAPH_5: 18;

          then ( vertices s1) c= V9 by A38, A40, ZFMISC_1: 57;

          then

           A43: (( vertices s1) \ {v2}) c= V by XBOOLE_1: 43;

           not v1 in ( vertices s2) by A4, A19, A20, A14, A17, A32, GRAPH_5: 18;

          then vx <> v1 by A19, Lm4;

          then

          consider q be oriented Chain of G such that

           A44: q is_shortestpath_of (v1,vx,V,W) and

           A45: ( cost (q,W)) <= ( cost (P,W)) by A7, A34, A43, GRAPH_5:def 19;

          

           A46: 0 <= ( cost (t2,W)) by A1, GRAPH_5: 50;

          Vt c= ( vertices (t1 ^ t2)) by GRAPH_5: 26;

          then not v3 in Vt by A4, A20, A14, A17, A32, A38, A42, GRAPH_5: 18;

          then Vt c= V9 by A41, ZFMISC_1: 57;

          then

           A47: (Vt \ {v2}) c= V by XBOOLE_1: 43;

          

           A48: (FS . (t1 . 1)) = (FS . (s1 . 1)) by A29, A37, A38, Lm1

          .= v1 by A20, A14, A32, Lm1;

          ( cost (s1,W)) = (( cost (t1,W)) + ( cost (t2,W))) by A1, A38, GRAPH_5: 46, GRAPH_5: 54;

          then

           A49: ( 0 + ( cost (t1,W))) <= ( cost (s1,W)) by A46, XREAL_1: 7;

          (FT . (t1 . ( len t1))) = (FT . (s1 . j)) by A29, A37, A38, Lm1

          .= v2 by A20, A29, A31, A35, Lm1;

          then t1 is_orientedpath_of (v1,v2) by A48, A39, GRAPH_5:def 3;

          then t1 is_orientedpath_of (v1,v2,V) by A47, GRAPH_5:def 4;

          then ( cost (P,W)) <= ( cost (t1,W)) by A2, GRAPH_5:def 18;

          then ( cost (q,W)) <= ( cost (t1,W)) by A45, XXREAL_0: 2;

          then

           A50: ( cost (q,W)) <= ( cost (s1,W)) by A49, XXREAL_0: 2;

          

           A51: (s2 . 1) orientedly_joins (vx,v3) by A21, A17, GRAPH_4:def 1;

          

           A52: q is_orientedpath_of (v1,vx,V) by A44, GRAPH_5:def 18;

          then

           A53: q is_orientedpath_of (v1,vx) by GRAPH_5:def 4;

          then q <> {} by GRAPH_5:def 3;

          then

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

          then

          consider p be oriented Chain of G such that

           A55: p = (q ^ s2) and p is_orientedpath_of (v1,v3) by A19, A51, A53, GRAPH_5: 33;

          p is_orientedpath_of (v1,v3,(V \/ {vx})) by A19, A52, A51, A54, A55, GRAPH_5: 34;

          then p is_orientedpath_of (v1,v3,V) by A34, A43, ZFMISC_1: 40;

          then ( cost (Q,W)) <= ( cost (p,W)) by A5, GRAPH_5:def 18;

          then

           A56: ( cost (Q,W)) <= (( cost (q,W)) + ( cost (s2,W))) by A1, A55, GRAPH_5: 46, GRAPH_5: 54;

          ( cost (s,W)) = (( cost (s1,W)) + ( cost (s2,W))) by A1, A20, GRAPH_5: 46, GRAPH_5: 54;

          then (( cost (q,W)) + ( cost (s2,W))) <= ( cost (s,W)) by A50, XREAL_1: 7;

          then ( cost (Q,W)) <= ( cost (s,W)) by A56, XXREAL_0: 2;

          hence ( cost (Q,W)) <= ( cost (S,W)) by A11, XXREAL_0: 2;

        end;

      end;

      Q is_orientedpath_of (v1,v3,V) by A5, GRAPH_5:def 18;

      then Q is_orientedpath_of (v1,v3,V9) by GRAPH_5: 32, XBOOLE_1: 7;

      hence thesis by A8, GRAPH_5:def 18;

    end;

    reserve G for finite oriented Graph,

P,Q for oriented Chain of G,

W for Function of the carrier' of G, Real>=0 ,

v1,v2,v3,v4 for Vertex of G;

    theorem :: GRAPHSP:14

    

     Th14: e in the carrier' of G & P = <*e*> & e orientedly_joins (v1,v2) implies P is_shortestpath_of (v1,v2, {v1},W)

    proof

      assume that

       A1: e in the carrier' of G and

       A2: P = <*e*> and

       A3: e orientedly_joins (v1,v2);

      

       A4: ( len P) = 1 by A2, FINSEQ_1: 40;

      then

       A5: ( vertices P) = ( vertices (P /. 1)) by GRAPH_5: 25;

      set FS = the Source of G, FT = the Target of G, Eg = the carrier' of G;

      

       A6: (FS . e) = v1 & (FT . e) = v2 by A3, GRAPH_4:def 1;

       A7:

      now

        let S be oriented Chain of G;

        assume

         A8: S is_orientedpath_of (v1,v2, {v1});

        W is_weight>=0of G by GRAPH_5:def 13;

        then

        consider s be Simple oriented Chain of G such that

         A9: s is_shortestpath_of (v1,v2, {v1},W) by A8, GRAPH_5: 62;

        set Vs = ( vertices s);

        

         A10: s is_orientedpath_of (v1,v2, {v1}) by A9, GRAPH_5:def 18;

        then

         A11: s is_orientedpath_of (v1,v2) by GRAPH_5:def 4;

        then s <> {} by GRAPH_5:def 3;

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

        then

        consider i be Nat such that

         A12: ( len s) = (1 + i) by NAT_1: 10;

        

         A13: (FT . (s . ( len s))) = v2 by A11, GRAPH_5:def 3;

        

         A14: (FS . (s . 1)) = v1 by A11, GRAPH_5:def 3;

        consider s1,s2 be FinSequence such that

         A15: ( len s1) = i and

         A16: ( len s2) = 1 and

         A17: s = (s1 ^ s2) by A12, FINSEQ_2: 22;

        reconsider s1, s2 as Simple oriented Chain of G by A17, GRAPH_5: 14;

        (Vs \ {v2}) c= {v1} by A10, GRAPH_5:def 4;

        then Vs c= ( {v2} \/ {v1}) by XBOOLE_1: 44;

        then

         A18: Vs c= {v1, v2} by ENUMSET1: 1;

        now

          reconsider vx = (FS . (s2 . 1)) as Vertex of G by A16, Lm3;

          

           A19: ( len s1) < ( len s) by A12, A15, NAT_1: 13;

          

           A20: vx in ( vertices s2) by A16, Lm4;

          ( vertices s2) c= ( vertices (s1 ^ s2)) by GRAPH_5: 26;

          then

           A21: ( vertices s2) c= {v1, v2} by A18, A17;

          assume s1 <> {} ;

          then

           A22: ( len s1) >= 1 by FINSEQ_1: 20;

          then

           A23: (FS . (s . 1)) <> (FS . (s2 . 1)) by A16, A17, Th6;

          ( len s2) = 1 by A16;

          then

           A24: (FT . (s . ( len s))) <> (FT . (s1 . ( len s1))) by A17, A22, Th6;

          (FS . (s2 . 1)) = (FS . (s . (( len s1) + 1))) by A16, A17, Lm2

          .= (FT . (s . ( len s1))) by A22, A19, GRAPH_1:def 15

          .= (FT . (s1 . ( len s1))) by A17, A22, Lm1;

          hence contradiction by A14, A13, A24, A23, A21, A20, TARSKI:def 2;

        end;

        then

         A25: ( len s) = ( 0 + 1) by A12, A15;

        (s /. 1) in Eg by A1;

        then (s . 1) in Eg by A25, FINSEQ_4: 15;

        then e = (s . 1) by A1, A6, A14, A13, A25, GRAPH_1:def 7;

        then s = P by A2, A25, FINSEQ_1: 40;

        hence ( cost (P,W)) <= ( cost (S,W)) by A8, A9, GRAPH_5:def 18;

      end;

      

       A26: (P . 1) = e by A2, FINSEQ_1: 40;

      then (P /. 1) = e by A4, FINSEQ_4: 15;

      then ( vertices P) = {v1, v2} by A6, A5, GRAPH_5:def 1;

      

      then

       A27: (( vertices P) \ {v2}) = (( {v1} \/ {v2}) \ {v2}) by ENUMSET1: 1

      .= ( {v1} \ {v2}) by XBOOLE_1: 40;

      P is_orientedpath_of (v1,v2) by A2, A6, A4, A26, GRAPH_5:def 3;

      then P is_orientedpath_of (v1,v2, {v1}) by A27, GRAPH_5:def 4;

      hence thesis by A7, GRAPH_5:def 18;

    end;

    theorem :: GRAPHSP:15

    

     Th15: e in the carrier' of G & P is_shortestpath_of (v1,v2,V,W) & v1 <> v3 & Q = (P ^ <*e*>) & e orientedly_joins (v2,v3) & v1 in V & (for v4 st v4 in V holds not (ex ee st ee in the carrier' of G & ee orientedly_joins (v4,v3))) implies Q is_shortestpath_of (v1,v3,(V \/ {v2}),W)

    proof

      assume that

       A1: e in the carrier' of G and

       A2: P is_shortestpath_of (v1,v2,V,W) and

       A3: v1 <> v3 and

       A4: Q = (P ^ <*e*>) and

       A5: e orientedly_joins (v2,v3) and

       A6: v1 in V and

       A7: for v4 st v4 in V holds not (ex ee st ee in the carrier' of G & ee orientedly_joins (v4,v3));

      set Eg = the carrier' of G;

      reconsider pe = <*e*> as FinSequence of Eg by A1, FINSEQ_1: 74;

      

       A8: P is_orientedpath_of (v1,v2,V) by A2, GRAPH_5:def 18;

      then P is_orientedpath_of (v1,v2) by GRAPH_5:def 4;

      then P <> {} by GRAPH_5:def 3;

      then

       A9: ( len P) >= 1 by FINSEQ_1: 20;

      set V9 = (V \/ {v2}), FS = the Source of G, FT = the Target of G;

      

       A10: W is_weight>=0of G by GRAPH_5:def 13;

       A11:

      now

        let S be oriented Chain of G;

        assume

         A12: S is_orientedpath_of (v1,v3,V9);

        then

        consider s be Simple oriented Chain of G such that

         A13: s is_shortestpath_of (v1,v3,V9,W) by A10, GRAPH_5: 62;

        set Vs = ( vertices s);

        

         A14: s is_orientedpath_of (v1,v3,V9) by A13, GRAPH_5:def 18;

        then

         A15: s is_orientedpath_of (v1,v3) by GRAPH_5:def 4;

        then

         A16: (FT . (s . ( len s))) = v3 by GRAPH_5:def 3;

        

         A17: (Vs \ {v3}) c= V9 by A14, GRAPH_5:def 4;

        s <> {} by A15, GRAPH_5:def 3;

        then

         A18: ( len s) >= 1 by FINSEQ_1: 20;

        then

        consider i be Nat such that

         A19: ( len s) = (1 + i) by NAT_1: 10;

        consider s1,s2 be FinSequence such that

         A20: ( len s1) = i and

         A21: ( len s2) = 1 and

         A22: s = (s1 ^ s2) by A19, FINSEQ_2: 22;

        reconsider s1, s2 as Simple oriented Chain of G by A22, GRAPH_5: 14;

        reconsider vx = (FS . (s2 . 1)) as Vertex of G by A21, Lm3;

        

         A23: (s2 . 1) = (s . ( len s)) by A19, A20, A21, A22, Lm2;

        

         A24: (FS . (s . 1)) = v1 by A15, GRAPH_5:def 3;

        

         A25: s1 <> {}

        proof

          assume s1 = {} ;

          then

           A26: ( len s) = (1 + 0 ) by A19, A20;

          then (s . 1) orientedly_joins (v1,v3) by A24, A16, GRAPH_4:def 1;

          hence contradiction by A6, A7, A26, Th2;

        end;

        then

         A27: ( len s1) >= 1 by FINSEQ_1: 20;

        ( len s1) < ( len s) by A19, A20, NAT_1: 13;

        

        then

         A28: (FS . (s . ( len s))) = (FT . (s . ( len s1))) by A19, A20, A27, GRAPH_1:def 15

        .= (FT . (s1 . ( len s1))) by A22, A27, Lm1;

         A29:

        now

          vx <> (FT . (s . ( len s))) by A21, A22, A23, A27, A28, Th6;

          then

           A30: not vx in {v3} by A16, TARSKI:def 1;

          vx in Vs by A18, A23, Lm4;

          then vx in (Vs \ {v3}) by A30, XBOOLE_0:def 5;

          then

           A31: vx in V or vx in {v2} by A17, XBOOLE_0:def 3;

          assume

           A32: vx <> v2;

          (s2 . 1) orientedly_joins (vx,v3) & (s2 . 1) in the carrier' of G by A21, A23, A16, Th2, GRAPH_4:def 1;

          hence contradiction by A7, A32, A31, TARSKI:def 1;

        end;

        ( len s2) = 1 by A21;

        then not (FT . (s . ( len s))) in ( vertices s1) by A3, A22, A24, A16, A27, GRAPH_5: 18;

        then

         A33: (( vertices s1) \ {v3}) = ( vertices s1) by A16, ZFMISC_1: 57;

        ( vertices s1) c= ( vertices (s1 ^ s2)) by GRAPH_5: 26;

        then ( vertices s1) c= (Vs \ {v3}) by A22, A33, XBOOLE_1: 33;

        then ( vertices s1) c= V9 by A17;

        then (( vertices s1) \ {v2}) c= (V9 \ {v2}) by XBOOLE_1: 33;

        then (( vertices s1) \ {v2}) c= (V \ {v2}) by XBOOLE_1: 40;

        then

         A34: (( vertices s1) \ {v2}) c= V by XBOOLE_1: 1;

        (s2 /. 1) in Eg by A1;

        then

         A35: (s2 . 1) in Eg by A21, FINSEQ_4: 15;

        (FS . e) = v2 & (FT . e) = v3 by A5, GRAPH_4:def 1;

        then e = (s2 . 1) by A1, A23, A16, A29, A35, GRAPH_1:def 7;

        then s2 = <*e*> by A21, FINSEQ_1: 40;

        then

         A36: ( cost (Q,W)) = (( cost (P,W)) + ( cost (s2,W))) by A4, A10, GRAPH_5: 46, GRAPH_5: 54;

        (FS . (s1 . 1)) = v1 by A22, A24, A27, Lm1;

        then s1 is_orientedpath_of (v1,v2) by A23, A25, A28, A29, GRAPH_5:def 3;

        then s1 is_orientedpath_of (v1,v2,V) by A34, GRAPH_5:def 4;

        then

         A37: ( cost (P,W)) <= ( cost (s1,W)) by A2, GRAPH_5:def 18;

        

         A38: ( cost (s,W)) <= ( cost (S,W)) by A12, A13, GRAPH_5:def 18;

        ( cost (s,W)) = (( cost (s1,W)) + ( cost (s2,W))) by A10, A22, GRAPH_5: 46, GRAPH_5: 54;

        then ( cost (Q,W)) <= ( cost (s,W)) by A37, A36, XREAL_1: 7;

        hence ( cost (Q,W)) <= ( cost (S,W)) by A38, XXREAL_0: 2;

      end;

      ( len pe) = 1 & (pe . 1) = e by FINSEQ_1: 40;

      then Q is_orientedpath_of (v1,v3,V9) by A4, A5, A8, A9, GRAPH_5: 34;

      hence thesis by A11, GRAPH_5:def 18;

    end;

    theorem :: GRAPHSP:16

    

     Th16: the carrier of G = (U \/ V) & v1 in U & (for v3, v4 st v3 in U & v4 in V holds not (ex e st e in the carrier' of G & e orientedly_joins (v3,v4))) implies (P is_shortestpath_of (v1,v2,U,W) iff P is_shortestpath_of (v1,v2,W))

    proof

      assume

       A1: the carrier of G = (U \/ V) & v1 in U & for v3, v4 st v3 in U & v4 in V holds not (ex e st e in the carrier' of G & e orientedly_joins (v3,v4));

      hereby

        assume

         A2: P is_shortestpath_of (v1,v2,U,W);

         A3:

        now

          let Q;

          assume Q is_orientedpath_of (v1,v2);

          then Q is_orientedpath_of (v1,v2,U) by A1, Th12;

          hence ( cost (P,W)) <= ( cost (Q,W)) by A2, GRAPH_5:def 18;

        end;

        P is_orientedpath_of (v1,v2,U) by A2, GRAPH_5:def 18;

        then P is_orientedpath_of (v1,v2) by GRAPH_5:def 4;

        hence P is_shortestpath_of (v1,v2,W) by A3, GRAPH_5:def 17;

      end;

      hereby

        assume

         A4: P is_shortestpath_of (v1,v2,W);

         A5:

        now

          let Q;

          assume Q is_orientedpath_of (v1,v2,U);

          then Q is_orientedpath_of (v1,v2) by GRAPH_5:def 4;

          hence ( cost (P,W)) <= ( cost (Q,W)) by A4, GRAPH_5:def 17;

        end;

        P is_orientedpath_of (v1,v2) by A4, GRAPH_5:def 17;

        then P is_orientedpath_of (v1,v2,U) by A1, Th12;

        hence P is_shortestpath_of (v1,v2,U,W) by A5, GRAPH_5:def 18;

      end;

    end;

    begin

    notation

      let f be Function, i,x be object;

      synonym (f,i) := x for f +* (i,x);

    end

    definition

      let f be FinSequence of REAL , x be object, r be Real;

      :: original: :=

      redefine

      func (f,x) := r -> FinSequence of REAL ;

      coherence

      proof

        

         A1: ( rng ((f,x) := r)) c= REAL

        proof

          let y be object;

          

           A2: ( rng ((f,x) := r)) c= (( rng f) \/ {r}) by FUNCT_7: 100;

          

           A3: r in REAL by XREAL_0:def 1;

          assume y in ( rng ((f,x) := r));

          then y in ( rng f) or y in {r} by A2, XBOOLE_0:def 3;

          hence thesis by A3, TARSKI:def 1;

        end;

        ( dom ((f,x) := r)) = ( dom f) by FUNCT_7: 30

        .= ( Seg ( len f)) by FINSEQ_1:def 3;

        then ((f,x) := r) is FinSequence by FINSEQ_1:def 2;

        hence thesis by A1, FINSEQ_1:def 4;

      end;

    end

    definition

      let i,k be Nat, f be FinSequence of REAL , r be Real;

      :: GRAPHSP:def1

      func (f,i) := (k,r) -> FinSequence of REAL equals ((((f,i) := k),k) := r);

      coherence ;

    end

    reserve f,g,h for Element of ( REAL * ),

r for Real;

    theorem :: GRAPHSP:17

    

     Th17: i <> k & i in ( dom f) implies (((f,i) := (k,r)) . i) = k

    proof

      assume that

       A1: i <> k and

       A2: i in ( dom f);

      set fik = ((f,i) := k);

      

      thus (((f,i) := (k,r)) . i) = (fik . i) by A1, FUNCT_7: 32

      .= k by A2, FUNCT_7: 31;

    end;

    theorem :: GRAPHSP:18

    

     Th18: m <> i & m <> k implies (((f,i) := (k,r)) . m) = (f . m)

    proof

      assume that

       A1: m <> i and

       A2: m <> k;

      set fik = ((f,i) := k);

      

      thus (((f,i) := (k,r)) . m) = (fik . m) by A2, FUNCT_7: 32

      .= (f . m) by A1, FUNCT_7: 32;

    end;

    theorem :: GRAPHSP:19

    

     Th19: k in ( dom f) implies (((f,i) := (k,r)) . k) = r

    proof

      set fik = ((f,i) := k);

      

       A1: ( dom fik) = ( dom f) by FUNCT_7: 30;

      assume k in ( dom f);

      hence thesis by A1, FUNCT_7: 31;

    end;

    theorem :: GRAPHSP:20

    

     Th20: ( dom ((f,i) := (k,r))) = ( dom f)

    proof

      set fik = ((f,i) := k);

      

      thus ( dom ((f,i) := (k,r))) = ( dom fik) by FUNCT_7: 30

      .= ( dom f) by FUNCT_7: 30;

    end;

    begin

    definition

      let X be set, f,g be Element of ( Funcs (X,X));

      :: original: *

      redefine

      func g * f -> Element of ( Funcs (X,X)) ;

      coherence

      proof

        reconsider f, g as Function of X, X by FUNCT_2: 66;

        (g * f) in ( Funcs (X,X)) by FUNCT_2: 9;

        hence thesis;

      end;

    end

    definition

      let X be set, f be Element of ( Funcs (X,X)), g be Element of X;

      :: original: .

      redefine

      func f . g -> Element of X ;

      coherence

      proof

        

         A1: f is Function of X, X by FUNCT_2: 66;

        per cases ;

          suppose

           A2: X = {} ;

          then {} = ( dom f) by A1;

          then (f . g) = {} by FUNCT_1:def 2;

          hence thesis by A2, SUBSET_1:def 1;

        end;

          suppose X <> {} ;

          hence thesis by A1, FUNCT_2: 5;

        end;

      end;

    end

    definition

      let X be set, f be Element of ( Funcs (X,X));

      :: GRAPHSP:def2

      func repeat (f) -> sequence of ( Funcs (X,X)) means

      : Def2: (it . 0 ) = ( id X) & for i be Nat holds (it . (i + 1)) = (f * (it . i));

      existence

      proof

        deffunc G( Nat, Element of ( Funcs (X,X))) = (f * $2);

        ex F be sequence of ( Funcs (X,X)) st (F . 0 ) = ( id X) & for n be Nat holds (F . (n + 1)) = G(n,.) from NAT_1:sch 12;

        hence thesis;

      end;

      uniqueness

      proof

        deffunc R( Nat, Element of ( Funcs (X,X))) = (f * $2);

        let F1,F2 be sequence of ( Funcs (X,X)) such that

         A1: (F1 . 0 ) = ( id X) and

         A2: for i be Nat holds (F1 . (i + 1)) = R(i,.) and

         A3: (F2 . 0 ) = ( id X) and

         A4: for i be Nat holds (F2 . (i + 1)) = R(i,.);

        thus F1 = F2 from NAT_1:sch 16( A1, A2, A3, A4);

      end;

    end

    theorem :: GRAPHSP:21

    

     Th21: for F be Element of ( Funcs (( REAL * ),( REAL * ))), f be Element of ( REAL * ), n,i be Element of NAT holds ((( repeat F) . 0 ) . f) = f

    proof

      let F be Element of ( Funcs (( REAL * ),( REAL * ))), f be Element of ( REAL * ), n,i be Element of NAT ;

      

      thus ((( repeat F) . 0 ) . f) = (( id ( REAL * )) . f) by Def2

      .= f;

    end;

    

     Lm5: for X be set, f be Element of ( Funcs (X,X)) holds ( dom f) = X

    proof

      let X be set, f be Element of ( Funcs (X,X));

      ex ff be Function st f = ff & ( dom ff) = X & ( rng ff) c= X by FUNCT_2:def 2;

      hence thesis;

    end;

    theorem :: GRAPHSP:22

    

     Th22: for F,G be Element of ( Funcs (( REAL * ),( REAL * ))), f be Element of ( REAL * ), i be Nat holds ((( repeat (F * G)) . (i + 1)) . f) = (F . (G . ((( repeat (F * G)) . i) . f)))

    proof

      let F,G be Element of ( Funcs (( REAL * ),( REAL * ))), f be Element of ( REAL * ), i;

      set Fi = (( repeat (F * G)) . i), ff = (Fi . f), FFi = ((F * G) * Fi);

      

       A1: ( dom (F * G)) = ( REAL * ) by Lm5;

      

       A2: ( dom FFi) = ( REAL * ) by Lm5;

      

      thus ((( repeat (F * G)) . (i + 1)) . f) = (FFi . f) by Def2

      .= ((F * G) . ff) by A2, FUNCT_1: 12

      .= (F . (G . ff)) by A1, FUNCT_1: 12;

    end;

    definition

      let g be Element of ( Funcs (( REAL * ),( REAL * ))), f be Element of ( REAL * );

      :: original: .

      redefine

      func g . f -> Element of ( REAL * ) ;

      coherence

      proof

        (g . f) in ( REAL * );

        hence thesis;

      end;

    end

    definition

      let f be Element of ( REAL * ), n be Nat;

      :: GRAPHSP:def3

      func OuterVx (f,n) -> Subset of NAT equals { i : i in ( dom f) & 1 <= i & i <= n & (f . i) <> ( - 1) & (f . (n + i)) <> ( - 1) };

      coherence

      proof

        set NS = { i : i in ( dom f) & 1 <= i & i <= n & (f . i) <> ( - 1) & (f . (n + i)) <> ( - 1) };

        NS c= NAT

        proof

          let x be object;

          assume x in NS;

          then ex k be Nat st x = k & k in ( dom f) & 1 <= k & k <= n & (f . k) <> ( - 1) & (f . (n + k)) <> ( - 1);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let f be Element of ( Funcs (( REAL * ),( REAL * ))), g be Element of ( REAL * ), n be Nat;

      assume

       A1: ex i st ( OuterVx (((( repeat f) . i) . g),n)) = {} ;

      :: GRAPHSP:def4

      func LifeSpan (f,g,n) -> Element of NAT means

      : Def4: ( OuterVx (((( repeat f) . it ) . g),n)) = {} & for k be Nat st ( OuterVx (((( repeat f) . k) . g),n)) = {} holds it <= k;

      existence

      proof

        defpred P[ Nat] means ( OuterVx (((( repeat f) . $1) . g),n)) = {} ;

        

         A2: ex k be Nat st P[k] by A1;

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

        then

        consider k be Nat such that

         A3: P[k] & for n be Nat st P[n] holds k <= n;

        k in NAT by ORDINAL1:def 12;

        hence thesis by A3;

      end;

      uniqueness

      proof

        let it1,it2 be Element of NAT ;

        assume

         A4: not thesis;

        then it1 <= it2 & it2 <= it1;

        hence contradiction by A4, XXREAL_0: 1;

      end;

    end

    definition

      let f be Element of ( Funcs (( REAL * ),( REAL * ))), n be Nat;

      :: GRAPHSP:def5

      func while_do (f,n) -> Element of ( Funcs (( REAL * ),( REAL * ))) means

      : Def5: ( dom it ) = ( REAL * ) & for h be Element of ( REAL * ) holds (it . h) = ((( repeat f) . ( LifeSpan (f,h,n))) . h);

      existence

      proof

        set X = ( REAL * );

        defpred P[ object, object] means for h be Element of X st $1 = h holds $2 = ((( repeat f) . ( LifeSpan (f,h,n))) . h);

        

         A1: ex ff be Function st f = ff & ( dom ff) = X & ( rng ff) c= X by FUNCT_2:def 2;

         A2:

        now

          let xx be object;

          assume xx in ( dom f);

          then

          reconsider h9 = xx as Element of X by A1;

          now

            take yy = ((( repeat f) . ( LifeSpan (f,h9,n))) . h9);

            let h be Element of X;

            assume xx = h;

            hence yy = ((( repeat f) . ( LifeSpan (f,h,n))) . h);

          end;

          hence ex y1 be object st P[xx, y1];

        end;

        consider f9 be Function such that

         A3: ( dom f9) = ( dom f) & for xx be object st xx in ( dom f) holds P[xx, (f9 . xx)] from CLASSES1:sch 1( A2);

        ( rng f9) c= X

        proof

          let y be object;

          assume y in ( rng f9);

          then

          consider xx be object such that

           A4: xx in ( dom f9) and

           A5: y = (f9 . xx) by FUNCT_1:def 3;

          reconsider h9 = xx as Element of X by A1, A3, A4;

          y = ((( repeat f) . ( LifeSpan (f,h9,n))) . h9) by A3, A4, A5;

          hence thesis;

        end;

        then

        reconsider f9 as Element of ( Funcs (X,X)) by A1, A3, FUNCT_2:def 2;

        take f9;

        thus ( dom f9) = X by A1, A3;

        let h be Element of X;

        thus thesis by A1, A3;

      end;

      uniqueness

      proof

        set X = ( REAL * );

        let g1,g2 be Element of ( Funcs (X,X)) such that

         A6: ( dom g1) = X and

         A7: for h be Element of X holds (g1 . h) = ((( repeat f) . ( LifeSpan (f,h,n))) . h) and

         A8: ( dom g2) = X and

         A9: for h be Element of X holds (g2 . h) = ((( repeat f) . ( LifeSpan (f,h,n))) . h);

        now

          let xx be object;

          assume xx in ( dom g1);

          then

          reconsider h = xx as Element of X by A6;

          

          thus (g1 . xx) = ((( repeat f) . ( LifeSpan (f,h,n))) . h) by A7

          .= (g2 . xx) by A9;

        end;

        hence thesis by A6, A8, FUNCT_1: 2;

      end;

    end

    begin

    definition

      let G be oriented Graph, v1,v2 be Vertex of G;

      assume

       A1: ex e be set st e in the carrier' of G & e orientedly_joins (v1,v2);

      :: GRAPHSP:def6

      func XEdge (v1,v2) -> set means

      : Def6: ex e be set st it = e & e in the carrier' of G & e orientedly_joins (v1,v2);

      existence by A1;

      uniqueness by Th10;

    end

    definition

      let G be oriented Graph, v1,v2 be Vertex of G, W be Function;

      :: GRAPHSP:def7

      func Weight (v1,v2,W) -> set equals

      : Def7: (W . ( XEdge (v1,v2))) if ex e be set st e in the carrier' of G & e orientedly_joins (v1,v2)

      otherwise ( - 1);

      correctness by TARSKI: 1;

    end

    registration

      let G be oriented Graph, v1,v2 be Vertex of G, W be Function of the carrier' of G, Real>=0 ;

      cluster ( Weight (v1,v2,W)) -> real;

      coherence

      proof

        per cases ;

          suppose

           A1: ex e be set st e in the carrier' of G & e orientedly_joins (v1,v2);

          then

          consider e be set such that

           A2: ( XEdge (v1,v2)) = e and

           A3: e in the carrier' of G and e orientedly_joins (v1,v2) by Def6;

          e in ( dom W) by A3, FUNCT_2:def 1;

          then (W . ( XEdge (v1,v2))) in Real>=0 by A2, PARTFUN1: 4;

          hence thesis by A1, Def7;

        end;

          suppose not ex e be set st e in the carrier' of G & e orientedly_joins (v1,v2);

          hence thesis by Def7;

        end;

      end;

    end

    reserve G for oriented Graph,

v1,v2 for Vertex of G,

W for Function of the carrier' of G, Real>=0 ;

    theorem :: GRAPHSP:23

    

     Th23: ( Weight (v1,v2,W)) >= 0 iff ex e be set st e in the carrier' of G & e orientedly_joins (v1,v2)

    proof

      set EG = the carrier' of G;

      thus ( Weight (v1,v2,W)) >= 0 implies ex e be set st e in EG & e orientedly_joins (v1,v2) by Def7;

      assume ex e be set st e in the carrier' of G & e orientedly_joins (v1,v2);

      then

      consider e be set such that

       A1: ( XEdge (v1,v2)) = e and

       A2: e in EG and

       A3: e orientedly_joins (v1,v2) by Def6;

      e in ( dom W) by A2, FUNCT_2:def 1;

      then (W . e) in Real>=0 by PARTFUN1: 4;

      then ex r be Real st (W . e) = r & r >= 0 by GRAPH_5:def 12;

      hence thesis by A1, A2, A3, Def7;

    end;

    theorem :: GRAPHSP:24

    ( Weight (v1,v2,W)) = ( - 1) iff not ex e be set st e in the carrier' of G & e orientedly_joins (v1,v2) by Def7, Th23;

    theorem :: GRAPHSP:25

    

     Th25: e in the carrier' of G & e orientedly_joins (v1,v2) implies ( Weight (v1,v2,W)) = (W . e)

    proof

      set EG = the carrier' of G;

      assume

       A1: e in EG & e orientedly_joins (v1,v2);

      then

      consider e1 be set such that

       A2: ( XEdge (v1,v2)) = e1 and

       A3: e1 in EG & e1 orientedly_joins (v1,v2) by Def6;

      e = e1 by A1, A3, Th10;

      hence thesis by A2, A3, Def7;

    end;

    begin

    definition

      let f be Element of ( REAL * ), n be Nat;

      :: GRAPHSP:def8

      func UnusedVx (f,n) -> Subset of NAT equals { i : i in ( dom f) & 1 <= i & i <= n & (f . i) <> ( - 1) };

      coherence

      proof

        set NS = { i : i in ( dom f) & 1 <= i & i <= n & (f . i) <> ( - 1) };

        NS c= NAT

        proof

          let x be object;

          assume x in NS;

          then ex k be Nat st x = k & k in ( dom f) & 1 <= k & k <= n & (f . k) <> ( - 1);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    definition

      let f be Element of ( REAL * ), n be Nat;

      :: GRAPHSP:def9

      func UsedVx (f,n) -> Subset of NAT equals { i : i in ( dom f) & 1 <= i & i <= n & (f . i) = ( - 1) };

      coherence

      proof

        set NS = { i : i in ( dom f) & 1 <= i & i <= n & (f . i) = ( - 1) };

        NS c= NAT

        proof

          let x be object;

          assume x in NS;

          then ex k be Nat st x = k & k in ( dom f) & 1 <= k & k <= n & (f . k) = ( - 1);

          hence thesis;

        end;

        hence thesis;

      end;

    end

    theorem :: GRAPHSP:26

    

     Th26: ( UnusedVx (f,n)) c= ( Seg n)

    proof

      let x be object;

      assume x in ( UnusedVx (f,n));

      then ex i st x = i & i in ( dom f) & 1 <= i & i <= n & (f . i) <> ( - 1);

      then x in { k where k be Nat : 1 <= k & k <= n };

      hence thesis by FINSEQ_1:def 1;

    end;

    registration

      let f be Element of ( REAL * ), n be Nat;

      cluster ( UnusedVx (f,n)) -> finite;

      coherence

      proof

        ( UnusedVx (f,n)) c= ( Seg n) by Th26;

        hence thesis;

      end;

    end

    theorem :: GRAPHSP:27

    

     Th27: ( OuterVx (f,n)) c= ( UnusedVx (f,n))

    proof

      let x be object;

      assume x in ( OuterVx (f,n));

      then ex k st x = k & k in ( dom f) & 1 <= k & k <= n & (f . k) <> ( - 1) & (f . (n + k)) <> ( - 1);

      hence thesis;

    end;

    theorem :: GRAPHSP:28

    

     Th28: ( OuterVx (f,n)) c= ( Seg n)

    proof

      ( OuterVx (f,n)) c= ( UnusedVx (f,n)) & ( UnusedVx (f,n)) c= ( Seg n) by Th26, Th27;

      hence thesis;

    end;

    registration

      let f be Element of ( REAL * ), n be Nat;

      cluster ( OuterVx (f,n)) -> finite;

      coherence

      proof

        ( OuterVx (f,n)) c= ( Seg n) by Th28;

        hence thesis;

      end;

    end

    definition

      let X be finite Subset of NAT , f be Element of ( REAL * ), n;

      :: GRAPHSP:def10

      func Argmin (X,f,n) -> Nat means

      : Def10: (X <> {} implies ex i st i = it & i in X & (for k st k in X holds (f /. ((2 * n) + i)) <= (f /. ((2 * n) + k))) & for k st k in X & (f /. ((2 * n) + i)) = (f /. ((2 * n) + k)) holds i <= k) & (X = {} implies it = 0 );

      existence

      proof

        per cases ;

          suppose

           A1: X = {} ;

          take 0 ;

          thus thesis by A1;

        end;

          suppose

           A2: X <> {} ;

          then

          reconsider X9 = X as non empty finite Subset of NAT ;

          deffunc F( Element of X9) = (f /. ((2 * n) + $1));

          consider x be Element of X9 such that

           A3: for y be Element of X9 holds F(x) <= F(y) from PRE_CIRC:sch 5;

          reconsider x as Element of NAT ;

          defpred P[ Nat] means $1 in X & (f /. ((2 * n) + x)) = (f /. ((2 * n) + $1));

          

           A4: ex i be Nat st P[i];

          consider i be Nat such that

           A5: P[i] & for k be Nat st P[k] holds i <= k from NAT_1:sch 5( A4);

          take F = i;

          hereby

            assume X <> {} ;

            take i = F;

            thus i = F & i in X by A5;

            thus for k st k in X holds (f /. ((2 * n) + i)) <= (f /. ((2 * n) + k)) by A3, A5;

            thus for k st k in X & (f /. ((2 * n) + i)) = (f /. ((2 * n) + k)) holds i <= k by A5;

          end;

          thus thesis by A2;

        end;

      end;

      uniqueness

      proof

        let F1,F2 be Nat such that

         A6: X <> {} implies ex i st i = F1 & i in X & (for k st k in X holds (f /. ((2 * n) + i)) <= (f /. ((2 * n) + k))) & for k st k in X & (f /. ((2 * n) + i)) = (f /. ((2 * n) + k)) holds i <= k and

         A7: X = {} implies F1 = 0 and

         A8: X <> {} implies ex i st i = F2 & i in X & (for k st k in X holds (f /. ((2 * n) + i)) <= (f /. ((2 * n) + k))) & for k st k in X & (f /. ((2 * n) + i)) = (f /. ((2 * n) + k)) holds i <= k and

         A9: X = {} implies F2 = 0 ;

        per cases ;

          suppose

           A10: X <> {} ;

          then

          consider j such that

           A11: j = F2 and

           A12: j in X and

           A13: for k st k in X holds (f /. ((2 * n) + j)) <= (f /. ((2 * n) + k)) and

           A14: for k st k in X & (f /. ((2 * n) + j)) = (f /. ((2 * n) + k)) holds j <= k by A8;

          consider i such that

           A15: i = F1 and

           A16: i in X and

           A17: for k st k in X holds (f /. ((2 * n) + i)) <= (f /. ((2 * n) + k)) and

           A18: for k st k in X & (f /. ((2 * n) + i)) = (f /. ((2 * n) + k)) holds i <= k by A6, A10;

          (f /. ((2 * n) + i)) <= (f /. ((2 * n) + j)) & (f /. ((2 * n) + j)) <= (f /. ((2 * n) + i)) by A16, A17, A12, A13;

          then (f /. ((2 * n) + j)) = (f /. ((2 * n) + i)) by XXREAL_0: 1;

          then i <= j & j <= i by A16, A18, A12, A14;

          hence thesis by A15, A11, XXREAL_0: 1;

        end;

          suppose X = {} ;

          hence thesis by A7, A9;

        end;

      end;

    end

    theorem :: GRAPHSP:29

    

     Th29: ( OuterVx (f,n)) <> {} & j = ( Argmin (( OuterVx (f,n)),f,n)) implies j in ( dom f) & 1 <= j & j <= n & (f . j) <> ( - 1) & (f . (n + j)) <> ( - 1)

    proof

      set IN = ( OuterVx (f,n));

      assume IN <> {} & j = ( Argmin (IN,f,n));

      then ex i st i = j & i in IN & (for k st k in IN holds (f /. ((2 * n) + i)) <= (f /. ((2 * n) + k))) & for k st k in IN & (f /. ((2 * n) + i)) = (f /. ((2 * n) + k)) holds i <= k by Def10;

      then ex k st j = k & k in ( dom f) & 1 <= k & k <= n & (f . k) <> ( - 1) & (f . (n + k)) <> ( - 1);

      hence thesis;

    end;

    theorem :: GRAPHSP:30

    

     Th30: ( Argmin (( OuterVx (f,n)),f,n)) <= n

    proof

      set IN = ( OuterVx (f,n));

      per cases ;

        suppose IN <> {} ;

        hence thesis by Th29;

      end;

        suppose IN = {} ;

        hence thesis by Def10;

      end;

    end;

    definition

      let n be Nat;

      :: GRAPHSP:def11

      func findmin (n) -> Element of ( Funcs (( REAL * ),( REAL * ))) means

      : Def11: ( dom it ) = ( REAL * ) & for f be Element of ( REAL * ) holds (it . f) = ((f,(((n * n) + (3 * n)) + 1)) := (( Argmin (( OuterVx (f,n)),f,n)),( - 1)));

      existence

      proof

        set X = ( REAL * ), mi = (((n * n) + (3 * n)) + 1);

        defpred P[ object, object] means for f be Element of ( REAL * ) st $1 = f holds $2 = ((f,mi) := (( Argmin (( OuterVx (f,n)),f,n)),( - 1)));

         A1:

        now

          let xx be object;

          assume xx in X;

          then

          reconsider h = xx as Element of ( REAL * );

          reconsider y = ((h,mi) := (( Argmin (( OuterVx (h,n)),h,n)),( - 1))) as object;

          take y;

          thus P[xx, y];

        end;

        consider F be Function such that

         A2: ( dom F) = X & for x be object st x in X holds P[x, (F . x)] from CLASSES1:sch 1( A1);

        ( rng F) c= X

        proof

          let y be object;

          assume y in ( rng F);

          then

          consider xx be object such that

           A3: xx in ( dom F) and

           A4: y = (F . xx) by FUNCT_1:def 3;

          reconsider h = xx as Element of ( REAL * ) by A2, A3;

          y = ((h,mi) := (( Argmin (( OuterVx (h,n)),h,n)),( - 1))) by A2, A4;

          hence thesis by FINSEQ_1:def 11;

        end;

        then

        reconsider F as Element of ( Funcs (X,X)) by A2, FUNCT_2:def 2;

        take F;

        thus ( dom F) = X by A2;

        let f be Element of ( REAL * );

        thus thesis by A2;

      end;

      uniqueness

      proof

        set X = ( REAL * ), mi = (((n * n) + (3 * n)) + 1);

        let F1,F2 be Element of ( Funcs (X,X)) such that

         A5: ( dom F1) = X and

         A6: for f be Element of ( REAL * ) holds (F1 . f) = ((f,mi) := (( Argmin (( OuterVx (f,n)),f,n)),( - 1))) and

         A7: ( dom F2) = X and

         A8: for f be Element of ( REAL * ) holds (F2 . f) = ((f,mi) := (( Argmin (( OuterVx (f,n)),f,n)),( - 1)));

        now

          let xx be object;

          assume xx in ( dom F1);

          then

          reconsider h = xx as Element of ( REAL * ) by A5;

          

          thus (F1 . xx) = ((h,mi) := (( Argmin (( OuterVx (h,n)),h,n)),( - 1))) by A6

          .= (F2 . xx) by A8;

        end;

        hence thesis by A5, A7, FUNCT_1: 2;

      end;

    end

    reconsider jj = 1 as Real;

    theorem :: GRAPHSP:31

    

     Th31: i > n & i <> (((n * n) + (3 * n)) + 1) implies ((( findmin n) . f) . i) = (f . i)

    proof

      set k = ( Argmin (( OuterVx (f,n)),f,n)), mi = (((n * n) + (3 * n)) + 1);

      assume

       A1: i > n & i <> mi;

      ((( findmin n) . f) . i) = (((f,mi) := (k,( - jj))) . i) & k <= n by Def11, Th30;

      hence thesis by A1, Th18;

    end;

    theorem :: GRAPHSP:32

    

     Th32: i in ( dom f) & (f . i) = ( - 1) & i <> (((n * n) + (3 * n)) + 1) implies ((( findmin n) . f) . i) = ( - 1)

    proof

      set k = ( Argmin (( OuterVx (f,n)),f,n)), mi = (((n * n) + (3 * n)) + 1);

      assume that

       A1: i in ( dom f) and

       A2: (f . i) = ( - 1) & i <> mi;

      

       A3: ((( findmin n) . f) . i) = (((f,mi) := (k,( - jj))) . i) by Def11;

      per cases ;

        suppose i = k;

        hence thesis by A1, A3, Th19;

      end;

        suppose i <> k;

        hence thesis by A2, A3, Th18;

      end;

    end;

    theorem :: GRAPHSP:33

    

     Th33: ( dom (( findmin n) . f)) = ( dom f)

    proof

      (( findmin n) . f) = ((f,(((n * n) + (3 * n)) + 1)) := (( Argmin (( OuterVx (f,n)),f,n)),( - jj))) by Def11;

      hence thesis by Th20;

    end;

    

     Lm6: k >= 1 implies n <= (k * n)

    proof

      assume k >= 1;

      then (1 * n) <= (k * n) by NAT_1: 4;

      hence thesis;

    end;

    

     Lm7: (3 * n) < (((n * n) + (3 * n)) + 1) & n < (((n * n) + (3 * n)) + 1) & (2 * n) < (((n * n) + (3 * n)) + 1)

    proof

      (3 * n) <= ((n * n) + (3 * n)) by NAT_1: 12;

      hence

       A1: (3 * n) < (((n * n) + (3 * n)) + 1) by NAT_1: 13;

      n <= (3 * n) by Lm6;

      hence n < (((n * n) + (3 * n)) + 1) by A1, XXREAL_0: 2;

      (2 * n) <= (3 * n) by NAT_1: 4;

      hence thesis by A1, XXREAL_0: 2;

    end;

    

     Lm8: (n < k & k <= (2 * n) implies not ((2 * n) < k & k <= (3 * n)) & not (k <= n or k > (3 * n))) & ((k <= n or k > (3 * n)) implies not ((2 * n) < k & k <= (3 * n)) & not (n < k & k <= (2 * n))) & ((2 * n) < k & k <= (3 * n) implies not (n < k & k <= (2 * n)) & not (k <= n or k > (3 * n)))

    proof

      

       A1: (2 * n) <= (3 * n) by NAT_1: 4;

      hence n < k & k <= (2 * n) implies ( not ((2 * n) < k & k <= (3 * n))) & not (k <= n or k > (3 * n)) by XXREAL_0: 2;

      

       A2: (2 * n) = (n + n);

      hereby

        assume

         A3: k <= n or k > (3 * n);

        per cases by A3;

          suppose

           A4: k <= n;

          hence not ((2 * n) < k & k <= (3 * n)) by A2, NAT_1: 12;

          thus not (n < k & k <= (2 * n)) by A4;

        end;

          suppose

           A5: k > (3 * n);

          hence not ((2 * n) < k & k <= (3 * n));

          thus not (n < k & k <= (2 * n)) by A1, A5, XXREAL_0: 2;

        end;

      end;

      assume that

       A6: (2 * n) < k and

       A7: k <= (3 * n);

      thus not (n < k & k <= (2 * n)) by A6;

      thus thesis by A2, A6, A7, NAT_1: 12;

    end;

    theorem :: GRAPHSP:34

    

     Th34: ( OuterVx (f,n)) <> {} implies ex j st j in ( OuterVx (f,n)) & 1 <= j & j <= n & ((( findmin n) . f) . j) = ( - 1)

    proof

      set IX = ( OuterVx (f,n));

      assume IX <> {} ;

      then

      consider i such that

       A1: i = ( Argmin (IX,f,n)) and

       A2: i in IX and for k st k in IX holds (f /. ((2 * n) + i)) <= (f /. ((2 * n) + k)) and for k st k in IX & (f /. ((2 * n) + i)) = (f /. ((2 * n) + k)) holds i <= k by Def10;

      take i;

      thus i in IX by A2;

      

       A3: ex k st i = k & k in ( dom f) & 1 <= k & k <= n & (f . k) <> ( - 1) & (f . (n + k)) <> ( - 1) by A2;

      hence 1 <= i & i <= n;

      

      thus ((( findmin n) . f) . i) = (((f,(((n * n) + (3 * n)) + 1)) := (i,( - jj))) . i) by A1, Def11

      .= ( - 1) by A3, Th19;

    end;

    definition

      let f be Element of ( REAL * ), n,k be Nat;

      :: GRAPHSP:def12

      func newpathcost (f,n,k) -> Real equals ((f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k)));

      correctness ;

    end

    definition

      let n,k be Nat, f be Element of ( REAL * );

      :: GRAPHSP:def13

      pred f hasBetterPathAt n,k means ((f . (n + k)) = ( - 1) or (f /. ((2 * n) + k)) > ( newpathcost (f,n,k))) & (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k)) >= 0 & (f . k) <> ( - 1);

    end

    definition

      let f be Element of ( REAL * ), n be Nat;

      :: GRAPHSP:def14

      func Relax (f,n) -> Element of ( REAL * ) means

      : Def14: ( dom it ) = ( dom f) & for k be Nat st k in ( dom f) holds (n < k & k <= (2 * n) implies (f hasBetterPathAt (n,(k -' n)) implies (it . k) = (f /. (((n * n) + (3 * n)) + 1))) & ( not f hasBetterPathAt (n,(k -' n)) implies (it . k) = (f . k))) & ((2 * n) < k & k <= (3 * n) implies (f hasBetterPathAt (n,(k -' (2 * n))) implies (it . k) = ( newpathcost (f,n,(k -' (2 * n))))) & ( not f hasBetterPathAt (n,(k -' (2 * n))) implies (it . k) = (f . k))) & (k <= n or k > (3 * n) implies (it . k) = (f . k));

      existence

      proof

        defpred P2[ Nat] means f hasBetterPathAt (n,($1 -' (2 * n)));

        defpred P1[ Nat] means f hasBetterPathAt (n,($1 -' n));

        set X = ( dom f);

        defpred P[ object, object] means for k st $1 = k & k in X holds (n < k & k <= (2 * n) implies ( P1[k] implies $2 = (f /. (((n * n) + (3 * n)) + 1))) & ( not P1[k] implies $2 = (f . k))) & ((2 * n) < k & k <= (3 * n) implies ( P2[k] implies $2 = ( newpathcost (f,n,(k -' (2 * n))))) & ( not P2[k] implies $2 = (f . k))) & (k <= n or k > (3 * n) implies $2 = (f . k));

         A1:

        now

          let xx be object;

          assume xx in X;

          then

          reconsider k = xx as Element of NAT ;

          per cases ;

            suppose

             A2: n < k & k <= (2 * n);

            thus ex y1 be object st P[xx, y1]

            proof

              per cases ;

                suppose

                 A3: P1[k];

                take y1 = (f /. (((n * n) + (3 * n)) + 1));

                thus thesis by A2, A3, Lm8;

              end;

                suppose

                 A4: not P1[k];

                take y1 = (f . k);

                thus thesis by A2, A4;

              end;

            end;

          end;

            suppose

             A5: (2 * n) < k & k <= (3 * n);

            thus ex y1 be object st P[xx, y1]

            proof

              per cases ;

                suppose

                 A6: P2[k];

                take y1 = ( newpathcost (f,n,(k -' (2 * n))));

                thus thesis by A5, A6, Lm8;

              end;

                suppose

                 A7: not P2[k];

                take y1 = (f . k);

                thus thesis by A5, A7;

              end;

            end;

          end;

            suppose

             A8: k <= n or k > (3 * n);

            thus ex y1 be object st P[xx, y1]

            proof

              take y1 = (f . k);

              thus thesis by A8, Lm8;

            end;

          end;

        end;

        consider F be Function such that

         A9: ( dom F) = X & for x be object st x in X holds P[x, (F . x)] from CLASSES1:sch 1( A1);

        

         A10: ( rng F) c= REAL

        proof

          let y1 be object;

          assume y1 in ( rng F);

          then

          consider xx be object such that

           A11: xx in ( dom F) and

           A12: y1 = (F . xx) by FUNCT_1:def 3;

          reconsider k = xx as Element of NAT by A9, A11;

          per cases ;

            suppose

             A13: n < k & k <= (2 * n);

            hereby

              per cases ;

                suppose P1[k];

                then y1 = (f /. (((n * n) + (3 * n)) + 1)) by A9, A11, A12, A13;

                hence thesis;

              end;

                suppose not P1[k];

                

                then y1 = (f . k) by A9, A11, A12, A13

                .= (f /. k) by A9, A11, PARTFUN1:def 6;

                hence thesis;

              end;

            end;

          end;

            suppose

             A14: (2 * n) < k & k <= (3 * n);

            hereby

              per cases ;

                suppose P2[k];

                then y1 = ( newpathcost (f,n,(k -' (2 * n)))) by A9, A11, A12, A14;

                hence thesis;

              end;

                suppose not P2[k];

                

                then y1 = (f . k) by A9, A11, A12, A14

                .= (f /. k) by A9, A11, PARTFUN1:def 6;

                hence thesis;

              end;

            end;

          end;

            suppose k <= n or k > (3 * n);

            

            then y1 = (f . k) by A9, A11, A12

            .= (f /. k) by A9, A11, PARTFUN1:def 6;

            hence thesis;

          end;

        end;

        X = ( Seg ( len f)) by FINSEQ_1:def 3;

        then F is FinSequence by A9, FINSEQ_1:def 2;

        then F is FinSequence of REAL by A10, FINSEQ_1:def 4;

        then

        reconsider F as Element of ( REAL * ) by FINSEQ_1:def 11;

        take F;

        thus ( dom F) = X by A9;

        let k;

        assume k in X;

        hence thesis by A9;

      end;

      uniqueness

      proof

        let F1,F2 be Element of ( REAL * ) such that

         A15: ( dom F1) = ( dom f) and

         A16: for k be Nat st k in ( dom f) holds (n < k & k <= (2 * n) implies (f hasBetterPathAt (n,(k -' n)) implies (F1 . k) = (f /. (((n * n) + (3 * n)) + 1))) & ( not f hasBetterPathAt (n,(k -' n)) implies (F1 . k) = (f . k))) & ((2 * n) < k & k <= (3 * n) implies (f hasBetterPathAt (n,(k -' (2 * n))) implies (F1 . k) = ( newpathcost (f,n,(k -' (2 * n))))) & ( not f hasBetterPathAt (n,(k -' (2 * n))) implies (F1 . k) = (f . k))) & (k <= n or k > (3 * n) implies (F1 . k) = (f . k)) and

         A17: ( dom F2) = ( dom f) and

         A18: for k be Nat st k in ( dom f) holds (n < k & k <= (2 * n) implies (f hasBetterPathAt (n,(k -' n)) implies (F2 . k) = (f /. (((n * n) + (3 * n)) + 1))) & ( not f hasBetterPathAt (n,(k -' n)) implies (F2 . k) = (f . k))) & ((2 * n) < k & k <= (3 * n) implies (f hasBetterPathAt (n,(k -' (2 * n))) implies (F2 . k) = ( newpathcost (f,n,(k -' (2 * n))))) & ( not f hasBetterPathAt (n,(k -' (2 * n))) implies (F2 . k) = (f . k))) & (k <= n or k > (3 * n) implies (F2 . k) = (f . k));

        now

          let xx be object;

          assume

           A19: xx in ( dom F1);

          then

          reconsider k = xx as Element of NAT ;

          defpred P2[] means f hasBetterPathAt (n,(k -' (2 * n)));

          defpred P1[] means f hasBetterPathAt (n,(k -' n));

          per cases ;

            suppose

             A20: n < k & k <= (2 * n);

            hereby

              per cases ;

                suppose

                 A21: P1[];

                

                hence (F1 . xx) = (f /. (((n * n) + (3 * n)) + 1)) by A15, A16, A19, A20

                .= (F2 . xx) by A15, A18, A19, A20, A21;

              end;

                suppose

                 A22: not P1[];

                

                hence (F1 . xx) = (f . k) by A15, A16, A19, A20

                .= (F2 . xx) by A15, A18, A19, A20, A22;

              end;

            end;

          end;

            suppose

             A23: (2 * n) < k & k <= (3 * n);

            hereby

              per cases ;

                suppose

                 A24: P2[];

                

                hence (F1 . xx) = ( newpathcost (f,n,(k -' (2 * n)))) by A15, A16, A19, A23

                .= (F2 . xx) by A15, A18, A19, A23, A24;

              end;

                suppose

                 A25: not P2[];

                

                hence (F1 . xx) = (f . k) by A15, A16, A19, A23

                .= (F2 . xx) by A15, A18, A19, A23, A25;

              end;

            end;

          end;

            suppose

             A26: k <= n or k > (3 * n);

            

            hence (F1 . xx) = (f . k) by A15, A16, A19

            .= (F2 . xx) by A15, A18, A19, A26;

          end;

        end;

        hence thesis by A15, A17, FUNCT_1: 2;

      end;

    end

    definition

      let n be Nat;

      :: GRAPHSP:def15

      func Relax (n) -> Element of ( Funcs (( REAL * ),( REAL * ))) means

      : Def15: ( dom it ) = ( REAL * ) & for f be Element of ( REAL * ) holds (it . f) = ( Relax (f,n));

      existence

      proof

        defpred P[ object, object] means for f be Element of ( REAL * ) st $1 = f holds $2 = ( Relax (f,n));

        set X = ( REAL * );

         A1:

        now

          let xx be object;

          assume xx in X;

          then

          reconsider h = xx as Element of ( REAL * );

          thus ex y1 be object st P[xx, y1]

          proof

            take y1 = ( Relax (h,n));

            thus thesis;

          end;

        end;

        consider F be Function such that

         A2: ( dom F) = X & for x be object st x in X holds P[x, (F . x)] from CLASSES1:sch 1( A1);

        now

          let y1 be object;

          assume y1 in ( rng F);

          then

          consider xx be object such that

           A3: xx in ( dom F) and

           A4: y1 = (F . xx) by FUNCT_1:def 3;

          reconsider h = xx as Element of ( REAL * ) by A2, A3;

          y1 = ( Relax (h,n)) by A2, A4;

          hence y1 in X;

        end;

        then ( rng F) c= X;

        then

        reconsider F as Element of ( Funcs (X,X)) by A2, FUNCT_2:def 2;

        take F;

        thus ( dom F) = X by A2;

        let f be Element of ( REAL * );

        thus thesis by A2;

      end;

      uniqueness

      proof

        set X = ( REAL * );

        let F1,F2 be Element of ( Funcs (X,X)) such that

         A5: ( dom F1) = X and

         A6: for f be Element of ( REAL * ) holds (F1 . f) = ( Relax (f,n)) and

         A7: ( dom F2) = X and

         A8: for f be Element of ( REAL * ) holds (F2 . f) = ( Relax (f,n));

        now

          let xx be object;

          assume xx in ( dom F1);

          then

          reconsider h = xx as Element of ( REAL * ) by A5;

          

          thus (F1 . xx) = ( Relax (h,n)) by A6

          .= (F2 . xx) by A8;

        end;

        hence thesis by A5, A7, FUNCT_1: 2;

      end;

    end

    theorem :: GRAPHSP:35

    

     Th35: ( dom (( Relax n) . f)) = ( dom f)

    proof

      

      thus ( dom (( Relax n) . f)) = ( dom ( Relax (f,n))) by Def15

      .= ( dom f) by Def14;

    end;

    theorem :: GRAPHSP:36

    

     Th36: (i <= n or i > (3 * n)) & i in ( dom f) implies ((( Relax n) . f) . i) = (f . i)

    proof

      assume

       A1: (i <= n or i > (3 * n)) & i in ( dom f);

      

      thus ((( Relax n) . f) . i) = (( Relax (f,n)) . i) by Def15

      .= (f . i) by A1, Def14;

    end;

    theorem :: GRAPHSP:37

    

     Th37: ( dom ((( repeat (( Relax n) * ( findmin n))) . i) . f)) = ( dom ((( repeat (( Relax n) * ( findmin n))) . (i + 1)) . f))

    proof

      set R = ( Relax n), M = ( findmin n), ff = ((( repeat (R * M)) . i) . f);

      

      thus ( dom ((( repeat (R * M)) . (i + 1)) . f)) = ( dom (R . (M . ff))) by Th22

      .= ( dom (M . ff)) by Th35

      .= ( dom ff) by Th33;

    end;

    theorem :: GRAPHSP:38

    

     Th38: ( OuterVx (((( repeat (( Relax n) * ( findmin n))) . i) . f),n)) <> {} implies ( UnusedVx (((( repeat (( Relax n) * ( findmin n))) . (i + 1)) . f),n)) c< ( UnusedVx (((( repeat (( Relax n) * ( findmin n))) . i) . f),n))

    proof

      set R = ( Relax n), M = ( findmin n), ff = ((( repeat (R * M)) . i) . f);

      set Fi1 = ((( repeat (R * M)) . (i + 1)) . f);

      assume ( OuterVx (ff,n)) <> {} ;

      then

       A1: ex j st j in ( OuterVx (ff,n)) & 1 <= j & j <= n & ((M . ff) . j) = ( - 1) by Th34;

      

       A2: ( dom Fi1) = ( dom ff) by Th37

      .= ( dom (M . ff)) by Th33;

       A3:

      now

        let x;

        assume x in ( UnusedVx (Fi1,n));

        then

        consider k such that

         A4: x = k and

         A5: k in ( dom Fi1) and 1 <= k and

         A6: k <= n and

         A7: (Fi1 . k) <> ( - 1);

        (Fi1 . k) = ((R . (M . ff)) . k) by Th22

        .= ((M . ff) . k) by A2, A5, A6, Th36;

        hence ((M . ff) . x) <> ( - 1) by A4, A7;

      end;

      

       A8: ( UnusedVx (Fi1,n)) c= ( UnusedVx (ff,n))

      proof

        

         A9: n < (((n * n) + (3 * n)) + 1) by Lm7;

        let x be object;

        assume x in ( UnusedVx (Fi1,n));

        then

        consider k such that

         A10: x = k and

         A11: k in ( dom Fi1) and

         A12: 1 <= k and

         A13: k <= n and

         A14: (Fi1 . k) <> ( - 1);

        

         A15: k in ( dom ff) by A11, Th37;

        (Fi1 . k) = ((R . (M . ff)) . k) by Th22

        .= ((M . ff) . k) by A2, A11, A13, Th36;

        then (ff . k) <> ( - 1) by A13, A14, A15, A9, Th32;

        hence thesis by A10, A12, A13, A15;

      end;

      ( OuterVx (ff,n)) c= ( UnusedVx (ff,n)) by Th27;

      then ( UnusedVx (Fi1,n)) <> ( UnusedVx (ff,n)) by A1, A3;

      hence thesis by A8, XBOOLE_0:def 8;

    end;

    theorem :: GRAPHSP:39

    

     Th39: g = ((( repeat (( Relax n) * ( findmin n))) . i) . f) & h = ((( repeat (( Relax n) * ( findmin n))) . (i + 1)) . f) & k = ( Argmin (( OuterVx (g,n)),g,n)) & ( OuterVx (g,n)) <> {} implies ( UsedVx (h,n)) = (( UsedVx (g,n)) \/ {k}) & not k in ( UsedVx (g,n))

    proof

      set R = ( Relax n), M = ( findmin n), ff = ((( repeat (R * M)) . i) . f), Fi1 = ((( repeat (R * M)) . (i + 1)) . f), mi = (((n * n) + (3 * n)) + 1);

      assume that

       A1: g = ff and

       A2: h = Fi1 and

       A3: k = ( Argmin (( OuterVx (g,n)),g,n)) and

       A4: ( OuterVx (g,n)) <> {} ;

      

       A5: (M . ff) = ((ff,mi) := (k,( - jj))) by A1, A3, Def11;

      

       A6: ( dom h) = ( dom ff) by A2, Th37;

      

       A7: ( dom g) = ( dom (M . ff)) by A1, Th33;

       A8:

      now

        let x be object;

        assume

         A9: x in (( UsedVx (g,n)) \/ {k});

        per cases by A9, XBOOLE_0:def 3;

          suppose

           A10: x in ( UsedVx (g,n));

          

           A11: n < mi by Lm7;

          consider m such that

           A12: x = m and

           A13: m in ( dom g) and

           A14: 1 <= m and

           A15: m <= n and

           A16: (g . m) = ( - 1) by A10;

          (h . m) = ((R . (M . ff)) . m) by A2, Th22

          .= ((M . ff) . m) by A7, A13, A15, Th36

          .= ( - 1) by A1, A13, A15, A16, A11, Th32;

          hence x in ( UsedVx (h,n)) by A1, A6, A12, A13, A14, A15;

        end;

          suppose x in {k};

          then

           A17: x = k by TARSKI:def 1;

          

           A18: k in ( dom g) by A3, A4, Th29;

          

           A19: 1 <= k by A3, A4, Th29;

          

           A20: k <= n by A3, A4, Th29;

          (h . k) = ((R . (M . ff)) . k) by A2, Th22

          .= ((M . ff) . k) by A7, A18, A20, Th36

          .= ( - jj) by A1, A5, A18, Th19;

          hence x in ( UsedVx (h,n)) by A1, A6, A17, A18, A19, A20;

        end;

      end;

      

       A21: ( dom h) = ( dom (M . ff)) by A6, Th33;

      now

        let x be object;

        assume x in ( UsedVx (h,n));

        then

        consider m such that

         A22: x = m and

         A23: m in ( dom h) and

         A24: 1 <= m and

         A25: m <= n and

         A26: (h . m) = ( - 1);

        per cases ;

          suppose m = k;

          then x in {k} by A22, TARSKI:def 1;

          hence x in (( UsedVx (g,n)) \/ {k}) by XBOOLE_0:def 3;

        end;

          suppose

           A27: m <> k;

          

           A28: n < mi by Lm7;

          ( - 1) = ((R . (M . ff)) . m) by A2, A26, Th22

          .= ((M . ff) . m) by A21, A23, A25, Th36

          .= (ff . m) by A5, A25, A27, A28, Th18;

          then m in { j : j in ( dom ff) & 1 <= j & j <= n & (ff . j) = ( - 1) } by A6, A23, A24, A25;

          hence x in (( UsedVx (g,n)) \/ {k}) by A1, A22, XBOOLE_0:def 3;

        end;

      end;

      hence ( UsedVx (h,n)) = (( UsedVx (g,n)) \/ {k}) by A8, TARSKI: 2;

      assume k in ( UsedVx (g,n));

      then ex j st j = k & j in ( dom g) & 1 <= j & j <= n & (g . j) = ( - 1);

      hence contradiction by A3, A4, Th29;

    end;

    theorem :: GRAPHSP:40

    

     Th40: ex i st i <= n & ( OuterVx (((( repeat (( Relax n) * ( findmin n))) . i) . f),n)) = {}

    proof

      set R = ( Relax n), M = ( findmin n);

      defpred P[ Nat] means $1 <= n implies ( card ( UnusedVx (((( repeat (R * M)) . $1) . f),n))) <= (n - $1);

      set nf = ((( repeat (R * M)) . n) . f);

      assume

       A1: not ex i st i <= n & ( OuterVx (((( repeat (R * M)) . i) . f),n)) = {} ;

      

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

      proof

        let k;

        assume

         A3: P[k];

        now

          set fk = ( UnusedVx (((( repeat (R * M)) . k) . f),n)), fk1 = ( UnusedVx (((( repeat (R * M)) . (k + 1)) . f),n));

          

           A4: k <= (k + 1) by NAT_1: 11;

          assume

           A5: (k + 1) <= n;

          then ( OuterVx (((( repeat (R * M)) . k) . f),n)) <> {} by A1, A4, XXREAL_0: 2;

          then fk1 c< fk by Th38;

          then ( card fk1) < (n - k) by A3, A5, A4, CARD_2: 48, XXREAL_0: 2;

          then (( card fk1) + 1) <= (n - k) by INT_1: 7;

          then ( card fk1) <= ((n - k) - 1) by XREAL_1: 19;

          hence ( card fk1) <= (n - (k + 1));

        end;

        hence thesis;

      end;

      

       A6: P[ 0 ]

      proof

        set f0 = ((( repeat (R * M)) . 0 ) . f);

        assume 0 <= n;

        ( card ( UnusedVx (f0,n))) <= ( card ( Seg n)) by Th26, NAT_1: 43;

        hence thesis by FINSEQ_1: 57;

      end;

      for k holds P[k] from NAT_1:sch 2( A6, A2);

      then P[n];

      then

       A7: ( UnusedVx (nf,n)) = {} ;

      ( OuterVx (nf,n)) c= ( UnusedVx (nf,n)) by Th27;

      hence contradiction by A1, A7, XBOOLE_1: 3;

    end;

    

     Lm9: (n - k) <= n

    proof

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

      hence thesis by XREAL_1: 20;

    end;

    

     Lm10: for p,q be FinSequence of NAT , f be Element of ( REAL * ), i,n be Element of NAT st (for k st 1 <= k & k < ( len p) holds (p . (( len p) - k)) = (f . ((p /. ((( len p) - k) + 1)) + n))) & (for k st 1 <= k & k < ( len q) holds (q . (( len q) - k)) = (f . ((q /. ((( len q) - k) + 1)) + n))) & ( len p) <= ( len q) & (p . ( len p)) = (q . ( len q)) holds for k st 1 <= k & k < ( len p) holds (p . (( len p) - k)) = (q . (( len q) - k))

    proof

      let p,q be FinSequence of NAT , f be Element of ( REAL * ), i,n be Element of NAT ;

      assume that

       A1: for k st 1 <= k & k < ( len p) holds (p . (( len p) - k)) = (f . ((p /. ((( len p) - k) + 1)) + n)) and

       A2: for k st 1 <= k & k < ( len q) holds (q . (( len q) - k)) = (f . ((q /. ((( len q) - k) + 1)) + n)) and

       A3: ( len p) <= ( len q) and

       A4: (p . ( len p)) = (q . ( len q));

      defpred P[ Nat] means $1 < ( len p) implies (p . (( len p) - $1)) = (q . (( len q) - $1));

      

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

      proof

        let k;

        assume

         A6: P[k];

        now

          

           A7: k <= (k + 1) & (( len q) - k) <= ( len q) by Lm9, NAT_1: 11;

          assume

           A8: (k + 1) < ( len p);

          then

           A9: 1 <= (( len p) - k) by XREAL_1: 19;

          (( len p) - k) <= (( len q) - k) by A3, XREAL_1: 9;

          then

           A10: 1 <= (( len q) - k) by A9, XXREAL_0: 2;

          

           A11: (k + 1) < ( len q) by A3, A8, XXREAL_0: 2;

          

           A12: (p /. (( len p) - k)) = (p . (( len p) - k)) by A9, Lm9, Th3

          .= (q /. (( len q) - k)) by A6, A8, A7, A10, Th3, XXREAL_0: 2;

          

          thus (p . (( len p) - (k + 1))) = (f . ((p /. ((( len p) - (k + 1)) + 1)) + n)) by A1, A8, NAT_1: 11

          .= (f . ((q /. ((( len q) - (k + 1)) + 1)) + n)) by A12

          .= (q . (( len q) - (k + 1))) by A2, A11, NAT_1: 11;

        end;

        hence thesis;

      end;

      

       A13: P[ 0 ] by A4;

      for k holds P[k] from NAT_1:sch 2( A13, A5);

      hence thesis;

    end;

    theorem :: GRAPHSP:41

    

     Th41: ( dom f) = ( dom ((( repeat (( Relax n) * ( findmin n))) . i) . f))

    proof

      set R = ( Relax n), M = ( findmin n);

      defpred P[ Nat] means ( dom f) = ( dom ((( repeat (R * M)) . $1) . f));

      ( dom ((( repeat (R * M)) . 0 ) . f)) = ( dom (( id ( REAL * )) . f)) by Def2

      .= ( dom f);

      then

       A1: P[ 0 ];

      

       A2: for k st P[k] holds P[(k + 1)] by Th37;

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

      hence thesis;

    end;

    definition

      let f,g be Element of ( REAL * ), m,n be Nat;

      :: GRAPHSP:def16

      pred f,g equal_at m,n means ( dom f) = ( dom g) & for k st k in ( dom f) & m <= k & k <= n holds (f . k) = (g . k);

    end

    theorem :: GRAPHSP:42

    

     Th42: (f,f) equal_at (m,n);

    theorem :: GRAPHSP:43

    

     Th43: (f,g) equal_at (m,n) & (g,h) equal_at (m,n) implies (f,h) equal_at (m,n)

    proof

      assume that

       A1: (f,g) equal_at (m,n) and

       A2: (g,h) equal_at (m,n);

      

       A3: ( dom f) = ( dom g) by A1;

       A4:

      now

        let k;

        assume

         A5: k in ( dom f) & m <= k & k <= n;

        

        hence (f . k) = (g . k) by A1

        .= (h . k) by A2, A3, A5;

      end;

      ( dom g) = ( dom h) by A2;

      hence thesis by A3, A4;

    end;

    theorem :: GRAPHSP:44

    

     Th44: (((( repeat (( Relax n) * ( findmin n))) . i) . f),((( repeat (( Relax n) * ( findmin n))) . (i + 1)) . f)) equal_at (((3 * n) + 1),((n * n) + (3 * n)))

    proof

      set R = ( Relax n), M = ( findmin n), ff = ((( repeat (R * M)) . i) . f);

      set Fi1 = ((( repeat (R * M)) . (i + 1)) . f);

       A1:

      now

        let k;

        assume that

         A2: k in ( dom ff) and

         A3: ((3 * n) + 1) <= k and

         A4: k <= ((n * n) + (3 * n));

        

         A5: k > (3 * n) by A3, NAT_1: 13;

        

         A6: k in ( dom (M . ff)) by A2, Th33;

        

         A7: k < (((n * n) + (3 * n)) + 1) by A4, NAT_1: 13;

        (3 * n) >= n by Lm6;

        then

         A8: k > n by A5, XXREAL_0: 2;

        

        thus (Fi1 . k) = ((R . (M . ff)) . k) by Th22

        .= ((M . ff) . k) by A5, A6, Th36

        .= (ff . k) by A7, A8, Th31;

      end;

      ( dom Fi1) = ( dom ff) by Th37;

      hence thesis by A1;

    end;

    theorem :: GRAPHSP:45

    for F be Element of ( Funcs (( REAL * ),( REAL * ))), f be Element of ( REAL * ), n,i be Element of NAT st i < ( LifeSpan (F,f,n)) holds ( OuterVx (((( repeat F) . i) . f),n)) <> {} by Def4;

    theorem :: GRAPHSP:46

    

     Th46: (f,((( repeat (( Relax n) * ( findmin n))) . i) . f)) equal_at (((3 * n) + 1),((n * n) + (3 * n)))

    proof

      set R = ( Relax n), M = ( findmin n), m = ((3 * n) + 1), mm = ((n * n) + (3 * n));

      defpred P[ Nat] means (f,((( repeat (R * M)) . $1) . f)) equal_at (m,mm);

      

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

      proof

        let k;

        assume

         A2: P[k];

        (((( repeat (R * M)) . k) . f),((( repeat (R * M)) . (k + 1)) . f)) equal_at (m,mm) by Th44;

        hence thesis by A2, Th43;

      end;

      ((( repeat (R * M)) . 0 ) . f) = f by Th21;

      then

       A3: P[ 0 ] by Th42;

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

      hence thesis;

    end;

    theorem :: GRAPHSP:47

    

     Th47: 1 <= n & 1 in ( dom f) & (f . (n + 1)) <> ( - 1) & (for i st 1 <= i & i <= n holds (f . i) = 1) & (for i st 2 <= i & i <= n holds (f . (n + i)) = ( - 1)) implies 1 = ( Argmin (( OuterVx (f,n)),f,n)) & ( UsedVx (f,n)) = {} & {1} = ( UsedVx (((( repeat (( Relax n) * ( findmin n))) . 1) . f),n))

    proof

      set R = ( Relax n), M = ( findmin n), f0 = ((( repeat (R * M)) . 0 ) . f), RT = ( repeat (R * M));

      assume that

       A1: 1 <= n and

       A2: 1 in ( dom f) & (f . (n + 1)) <> ( - 1) and

       A3: for i st 1 <= i & i <= n holds (f . i) = 1 and

       A4: for i st 2 <= i & i <= n holds (f . (n + i)) = ( - 1);

      set k = ( Argmin (( OuterVx (f,n)),f,n));

      (f . 1) = 1 by A1, A3;

      then

       A5: 1 in { j : j in ( dom f) & 1 <= j & j <= n & (f . j) <> ( - 1) & (f . (n + j)) <> ( - 1) } by A1, A2;

      thus

       A6: k = 1

      proof

        assume

         A7: k <> 1;

        1 <= k by A5, Th29;

        then 1 < k by A7, XXREAL_0: 1;

        then

         A8: (1 + 1) <= k by INT_1: 7;

        k <= n & (f . (n + k)) <> ( - 1) by A5, Th29;

        hence contradiction by A4, A8;

      end;

      thus

       A9: ( UsedVx (f,n)) = {}

      proof

        assume ( UsedVx (f,n)) <> {} ;

        then

        consider x be object such that

         A10: x in ( UsedVx (f,n)) by XBOOLE_0:def 1;

        ex j st x = j & j in ( dom f) & 1 <= j & j <= n & (f . j) = ( - 1) by A10;

        hence contradiction by A3;

      end;

      ( OuterVx (f,n)) <> {} by A5;

      then

       A11: ( OuterVx (f0,n)) <> {} by Th21;

      

       A12: ( Argmin (( OuterVx (f0,n)),f0,n)) = ( Argmin (( OuterVx (f,n)),f0,n)) by Th21

      .= 1 by A6, Th21;

      

      thus ( UsedVx (((RT . 1) . f),n)) = ( UsedVx (((RT . ( 0 + 1)) . f),n))

      .= (( UsedVx (f0,n)) \/ {1}) by A11, A12, Th39

      .= (( UsedVx (f,n)) \/ {1}) by Th21

      .= {1} by A9;

    end;

    theorem :: GRAPHSP:48

    

     Th48: g = ((( repeat (( Relax n) * ( findmin n))) . 1) . f) & h = ((( repeat (( Relax n) * ( findmin n))) . i) . f) & 1 <= i & i <= ( LifeSpan ((( Relax n) * ( findmin n)),f,n)) & m in ( UsedVx (g,n)) implies m in ( UsedVx (h,n))

    proof

      set RF = (( Relax n) * ( findmin n)), RT = ( repeat RF), cn = ( LifeSpan (RF,f,n));

      assume that

       A1: g = ((RT . 1) . f) and

       A2: h = ((RT . i) . f) & 1 <= i & i <= cn and

       A3: m in ( UsedVx (g,n));

      defpred P[ Nat] means 1 <= $1 & $1 <= cn implies m in ( UsedVx (((RT . $1) . f),n));

      

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

      proof

        let k;

        assume

         A5: P[k];

        hereby

          assume that 1 <= (k + 1) and

           A6: (k + 1) <= cn;

          per cases ;

            suppose k = 0 ;

            hence m in ( UsedVx (((RT . (k + 1)) . f),n)) by A1, A3;

          end;

            suppose

             A7: k <> 0 ;

            k < cn by A6, NAT_1: 13;

            then ( OuterVx (((RT . k) . f),n)) <> {} by Def4;

            then ( UsedVx (((RT . (k + 1)) . f),n)) = (( UsedVx (((RT . k) . f),n)) \/ {( Argmin (( OuterVx (((RT . k) . f),n)),((RT . k) . f),n))}) by Th39;

            then

             A8: ( UsedVx (((RT . k) . f),n)) c= ( UsedVx (((RT . (k + 1)) . f),n)) by XBOOLE_1: 7;

            k >= (1 + 0 ) by A7, INT_1: 7;

            hence m in ( UsedVx (((RT . (k + 1)) . f),n)) by A5, A6, A8, NAT_1: 13;

          end;

        end;

      end;

      

       A9: P[ 0 ];

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

      hence thesis by A2;

    end;

    definition

      let p be FinSequence of NAT , f be Element of ( REAL * ), i,n be Nat;

      :: GRAPHSP:def17

      pred p is_vertex_seq_at f,i,n means (p . ( len p)) = i & for k st 1 <= k & k < ( len p) holds (p . (( len p) - k)) = (f . (n + (p /. ((( len p) - k) + 1))));

    end

    definition

      let p be FinSequence of NAT , f be Element of ( REAL * ), i,n be Nat;

      :: GRAPHSP:def18

      pred p is_simple_vertex_seq_at f,i,n means (p . 1) = 1 & ( len p) > 1 & p is_vertex_seq_at (f,i,n) & p is one-to-one;

    end

    theorem :: GRAPHSP:49

    for p,q be FinSequence of NAT , f be Element of ( REAL * ), i,n be Element of NAT st p is_simple_vertex_seq_at (f,i,n) & q is_simple_vertex_seq_at (f,i,n) holds p = q

    proof

      let p,q be FinSequence of NAT , f be Element of ( REAL * ), i,n be Element of NAT ;

      assume that

       A1: p is_simple_vertex_seq_at (f,i,n) and

       A2: q is_simple_vertex_seq_at (f,i,n);

      

       A3: (p . 1) = 1 by A1;

      

       A4: (q . 1) = 1 by A2;

      

       A5: p is_vertex_seq_at (f,i,n) by A1;

      then

       A6: (p . ( len p)) = i & for k st 1 <= k & k < ( len p) holds (p . (( len p) - k)) = (f . ((p /. ((( len p) - k) + 1)) + n));

      

       A7: q is_vertex_seq_at (f,i,n) by A2;

      then

       A8: (q . ( len q)) = i;

      

       A9: for k st 1 <= k & k < ( len q) holds (q . (( len q) - k)) = (f . ((q /. ((( len q) - k) + 1)) + n)) by A7;

      

       A10: ( len p) > 1 by A1;

       A11:

      now

        assume

         A12: ( len p) <> ( len q);

        per cases ;

          suppose

           A13: ( len p) < ( len q);

          

           A14: (( len p) - 1) > (1 - 1) by A10, XREAL_1: 14;

          then

          reconsider k = (( len p) - 1) as Element of NAT by INT_1: 3;

          

           A15: (( len p) - k) = ( 0 + 1);

          then

           A16: (( len q) - k) > 1 by A13, XREAL_1: 14;

          then

          reconsider m = (( len q) - k) as Element of NAT by INT_1: 3;

          

           A17: k < ( len p) by XREAL_1: 146;

          k >= ( 0 + 1) by A14, INT_1: 7;

          then

           A18: 1 = (q . (( len q) - k)) by A3, A6, A8, A9, A13, A15, A17, Lm10;

          q is one-to-one & m <= ( len q) by A2, Lm9;

          hence contradiction by A4, A18, A16, GRAPH_5: 6;

        end;

          suppose

           A19: ( len p) >= ( len q);

          

           A20: p is one-to-one by A1;

          

           A21: ( len p) > ( len q) by A12, A19, XXREAL_0: 1;

          hereby

            per cases ;

              suppose ( len q) <= 1;

              hence contradiction by A2;

            end;

              suppose ( len q) > 1;

              then

               A22: (( len q) - 1) > (1 - 1) by XREAL_1: 14;

              then

              reconsider k = (( len q) - 1) as Element of NAT by INT_1: 3;

              

               A23: k < ( len q) by XREAL_1: 146;

              

               A24: (( len q) - k) = ( 0 + 1);

              then

               A25: (( len p) - k) > 1 by A21, XREAL_1: 14;

              then

              reconsider m = (( len p) - k) as Element of NAT by INT_1: 3;

              k >= ( 0 + 1) by A22, INT_1: 7;

              then

               A26: 1 = (p . (( len p) - k)) by A6, A4, A8, A9, A19, A24, A23, Lm10;

              m <= ( len p) by Lm9;

              hence contradiction by A3, A20, A26, A25, GRAPH_5: 6;

            end;

          end;

        end;

      end;

      now

        let k be Nat;

        assume that

         A27: 1 <= k and

         A28: k <= ( len p);

        per cases ;

          suppose k = ( len p);

          hence (p . k) = (q . k) by A5, A8, A11;

        end;

          suppose k <> ( len p);

          then k < ( len p) by A28, XXREAL_0: 1;

          then

           A29: (( len p) - k) > (k - k) by XREAL_1: 14;

          then

          reconsider m = (( len p) - k) as Element of NAT by INT_1: 3;

          

           A30: (( len q) - m) = ( 0 + k) by A11;

          (( len p) - k) <= (( len p) - 1) by A27, XREAL_1: 13;

          then

           A31: m < ( len p) by XREAL_1: 146, XXREAL_0: 2;

          m >= ( 0 + 1) by A29, INT_1: 7;

          hence (p . k) = (q . k) by A6, A8, A9, A30, A31, Lm10;

        end;

      end;

      hence thesis by A11, FINSEQ_1: 14;

    end;

    definition

      let G be Graph, p be FinSequence of the carrier' of G, vs be FinSequence;

      :: GRAPHSP:def19

      pred p is_oriented_edge_seq_of vs means ( len vs) = (( len p) + 1) & for n be Nat st 1 <= n & n <= ( len p) holds (the Source of G . (p . n)) = (vs . n) & (the Target of G . (p . n)) = (vs . (n + 1));

    end

    theorem :: GRAPHSP:50

    for G be oriented Graph, vs be FinSequence, p,q be oriented Chain of G st p is_oriented_edge_seq_of vs & q is_oriented_edge_seq_of vs holds p = q

    proof

      let G be oriented Graph, vs be FinSequence, p,q be oriented Chain of G;

      assume that

       A1: p is_oriented_edge_seq_of vs and

       A2: q is_oriented_edge_seq_of vs;

      

       A3: (( len p) + 1) = ( len vs) by A1

      .= (( len q) + 1) by A2;

      now

        let k be Nat;

        assume

         A4: 1 <= k & k <= ( len p);

        

        then

         A5: (the Target of G . (p . k)) = (vs . (k + 1)) by A1

        .= (the Target of G . (q . k)) by A2, A3, A4;

        

         A6: (p . k) in the carrier' of G & (q . k) in the carrier' of G by A3, A4, Th2;

        (the Source of G . (p . k)) = (vs . k) by A1, A4

        .= (the Source of G . (q . k)) by A2, A3, A4;

        hence (p . k) = (q . k) by A5, A6, GRAPH_1:def 7;

      end;

      hence thesis by A3, FINSEQ_1: 14;

    end;

    theorem :: GRAPHSP:51

    for G be Graph, vs1,vs2 be FinSequence, p be oriented Chain of G st p is_oriented_edge_seq_of vs1 & p is_oriented_edge_seq_of vs2 & ( len p) >= 1 holds vs1 = vs2

    proof

      let G be Graph, vs1,vs2 be FinSequence, p be oriented Chain of G;

      assume that

       A1: p is_oriented_edge_seq_of vs1 and

       A2: p is_oriented_edge_seq_of vs2 and

       A3: ( len p) >= 1;

       A4:

      now

        let k be Nat;

        assume that

         A5: 1 <= k and

         A6: k <= ( len vs1);

        per cases ;

          suppose k = ( len vs1);

          then

           A7: k = (( len p) + 1) by A1;

          

          hence (vs1 . k) = (the Target of G . (p . ( len p))) by A1, A3

          .= (vs2 . k) by A2, A3, A7;

        end;

          suppose k <> ( len vs1);

          then k < ( len vs1) by A6, XXREAL_0: 1;

          then (k + 1) <= ( len vs1) by INT_1: 7;

          then (k + 1) <= (( len p) + 1) by A1;

          then

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

          

          hence (vs1 . k) = (the Source of G . (p . k)) by A1, A5

          .= (vs2 . k) by A2, A5, A8;

        end;

      end;

      ( len vs1) = (( len p) + 1) by A1

      .= ( len vs2) by A2;

      hence thesis by A4, FINSEQ_1: 14;

    end;

    

     Lm11: 1 <= i & i <= n implies 1 < ((2 * n) + i) & ((2 * n) + i) < (((n * n) + (3 * n)) + 1) & i < ((2 * n) + i)

    proof

      assume that

       A1: 1 <= i and

       A2: i <= n;

      set m2 = ((2 * n) + i);

      ((2 * n) + 1) <= m2 by A1, XREAL_1: 7;

      then

       A3: (2 * n) < m2 by NAT_1: 13;

      1 <= n by A1, A2, XXREAL_0: 2;

      then (2 * 1) <= (2 * n) by XREAL_1: 64;

      then 2 < m2 by A3, XXREAL_0: 2;

      hence 1 < m2 by XXREAL_0: 2;

      

       A4: (3 * n) < (((n * n) + (3 * n)) + 1) by Lm7;

      ((2 * n) + n) = ((2 + 1) * n);

      then m2 <= (3 * n) by A2, XREAL_1: 7;

      hence m2 < (((n * n) + (3 * n)) + 1) by A4, XXREAL_0: 2;

      n <= (2 * n) by Lm6;

      then i <= (2 * n) by A2, XXREAL_0: 2;

      hence thesis by A3, XXREAL_0: 2;

    end;

    

     Lm12: 1 <= i & i <= n implies 1 < (n + i) & (n + i) <= (2 * n) & (n + i) < (((n * n) + (3 * n)) + 1)

    proof

      assume that

       A1: 1 <= i and

       A2: i <= n;

      set ni = (n + i);

      1 <= n by A1, A2, XXREAL_0: 2;

      then (1 + 1) <= ni by A1, XREAL_1: 7;

      hence 1 < ni by NAT_1: 13;

      

       A3: ni <= (n + n) by A2, XREAL_1: 7;

      hence ni <= (2 * n);

      (2 * n) < (((n * n) + (3 * n)) + 1) by Lm7;

      hence thesis by A3, XXREAL_0: 2;

    end;

    

     Lm13: 1 <= i & i <= n & j <= n implies 1 < (((2 * n) + (n * i)) + j) & i < (((2 * n) + (n * i)) + j) & (((2 * n) + (n * i)) + j) < (((n * n) + (3 * n)) + 1)

    proof

      assume that

       A1: 1 <= i and

       A2: i <= n and

       A3: j <= n;

      

       A4: 1 <= n by A1, A2, XXREAL_0: 2;

      then (2 * 1) <= (2 * n) by XREAL_1: 64;

      then

       A5: 1 < (2 * n) by XXREAL_0: 2;

      set m3 = (((2 * n) + (n * i)) + j);

      

       A6: m3 = (((2 * n) + j) + (n * i)) & (n * i) <= (n * n) by A2, XREAL_1: 64;

      m3 = ((2 * n) + ((n * i) + j));

      then (2 * n) <= m3 by NAT_1: 12;

      hence 1 < m3 by A5, XXREAL_0: 2;

      

       A7: ((2 * n) + (n * i)) <= m3 by NAT_1: 12;

      (1 * i) <= (n * i) by A4, XREAL_1: 64;

      then (1 + i) < ((2 * n) + (n * i)) by A5, XREAL_1: 8;

      then (1 + i) < m3 by A7, XXREAL_0: 2;

      hence i < m3 by NAT_1: 13;

      ((2 * n) + n) = ((2 + 1) * n);

      then ((2 * n) + j) <= (3 * n) by A3, XREAL_1: 7;

      then m3 <= ((n * n) + (3 * n)) by A6, XREAL_1: 7;

      hence thesis by NAT_1: 13;

    end;

    

     Lm14: 1 <= i & i <= n & 1 <= j & j <= n implies ((3 * n) + 1) <= (((2 * n) + (n * i)) + j) & (((2 * n) + (n * i)) + j) <= ((n * n) + (3 * n))

    proof

      assume that

       A1: 1 <= i and

       A2: i <= n and

       A3: 1 <= j and

       A4: j <= n;

      set m3 = (((2 * n) + (n * i)) + j);

      

       A5: m3 = (((2 * n) + j) + (n * i)) & (n * i) <= (n * n) by A2, XREAL_1: 64;

      (n * 1) <= (n * i) by A1, XREAL_1: 64;

      then ((2 * n) + n) <= ((2 * n) + (n * i)) by XREAL_1: 7;

      hence ((3 * n) + 1) <= m3 by A3, XREAL_1: 7;

      ((2 * n) + n) = ((2 + 1) * n);

      then ((2 * n) + j) <= (3 * n) by A4, XREAL_1: 7;

      hence thesis by A5, XREAL_1: 7;

    end;

    begin

    definition

      let f be Element of ( REAL * ), G be oriented Graph, n be Nat, W be Function of the carrier' of G, Real>=0 ;

      :: GRAPHSP:def20

      pred f is_Input_of_Dijkstra_Alg G,n,W means ( len f) = (((n * n) + (3 * n)) + 1) & ( Seg n) = the carrier of G & (for i st 1 <= i & i <= n holds (f . i) = 1 & (f . ((2 * n) + i)) = 0 ) & (f . (n + 1)) = 0 & (for i st 2 <= i & i <= n holds (f . (n + i)) = ( - 1)) & for i,j be Vertex of G, k, m st k = i & m = j holds (f . (((2 * n) + (n * k)) + m)) = ( Weight (i,j,W));

    end

    begin

    definition

      let n be Nat;

      :: GRAPHSP:def21

      func DijkstraAlgorithm n -> Element of ( Funcs (( REAL * ),( REAL * ))) equals ( while_do ((( Relax n) * ( findmin n)),n));

      coherence ;

    end

    begin

    reserve p,q for FinSequence of NAT ,

G for finite oriented Graph,

P,Q,R for oriented Chain of G,

W for Function of the carrier' of G, Real>=0 ,

v1,v2,v3,v4 for Vertex of G;

    

     Lm15: f is_Input_of_Dijkstra_Alg (G,n,W) & v1 = 1 & n >= 1 & h = ((( repeat (( Relax n) * ( findmin n))) . 1) . f) implies (for v3, j st v3 <> v1 & v3 = j & (h . (n + j)) <> ( - 1) holds ex p, P st p is_simple_vertex_seq_at (h,j,n) & (for i st 1 <= i & i < ( len p) holds (p . i) in ( UsedVx (h,n))) & P is_oriented_edge_seq_of p & P is_shortestpath_of (v1,v3,( UsedVx (h,n)),W) & ( cost (P,W)) = (h . ((2 * n) + j)) & ( not v3 in ( UsedVx (h,n)) implies P islongestInShortestpath (( UsedVx (h,n)),v1,W))) & (for m, j st (h . (n + j)) = ( - 1) & 1 <= j & j <= n & m in ( UsedVx (h,n)) holds (f . (((2 * n) + (n * m)) + j)) = ( - 1)) & for m st m in ( UsedVx (h,n)) holds (h . (n + m)) <> ( - 1)

    proof

      set R = ( Relax n), M = ( findmin n), f0 = ((( repeat (R * M)) . 0 ) . f), mi = (((n * n) + (3 * n)) + 1);

      assume that

       A1: f is_Input_of_Dijkstra_Alg (G,n,W) and

       A2: v1 = 1 and

       A3: n >= 1 and

       A4: h = ((( repeat (( Relax n) * ( findmin n))) . 1) . f);

      

       A5: ( len f) = mi by A1;

      set nk = (n + 1);

      

       A6: ((2 * n) + n) = ((2 + 1) * n);

      

       A7: (f . (n + 1)) = 0 by A1;

      

       A8: 1 <= mi by NAT_1: 12;

      then

       A9: 1 in ( dom f) by A5, FINSEQ_3: 25;

      

       A10: (for j st 1 <= j & j <= n holds (f . j) = 1) & for j st 2 <= j & j <= n holds (f . (n + j)) = ( - 1) by A1;

      then

       A11: {1} = ( UsedVx (h,n)) by A3, A4, A7, A9, Th47;

      h = ((( repeat (R * M)) . ( 0 + 1)) . f) by A4;

      then h = (R . (M . f0)) by Th22;

      then

       A12: h = ( Relax ((M . f0),n)) by Def15;

      

       A13: ( Seg n) = the carrier of G by A1;

      then

      reconsider VG = the carrier of G as non empty Subset of NAT by A3;

      set Ak = ( Argmin (( OuterVx (f,n)),f,n));

      

       A14: ( dom (M . f0)) = ( dom f0) by Th33

      .= ( dom f) by Th21;

      

       A15: 1 = Ak by A3, A7, A10, A9, Th47;

      

       A16: (M . f0) = (M . f) by Th21

      .= ((f,mi) := (1,( - jj))) by A15, Def11;

      then ((M . f0) . 1) = ( - jj) by A9, Th19;

      then not (M . f0) hasBetterPathAt (n,1);

      then

       A17: not (M . f0) hasBetterPathAt (n,(nk -' n)) by NAT_D: 34;

      

       A18: nk < mi by A3, Lm12;

      

       A19: W is_weight>=0of G by GRAPH_5:def 13;

      hereby

        set w1 = ((2 * n) + 1);

        let v3, j;

        set nj = (n + j);

        assume that

         A20: v3 <> v1 and

         A21: v3 = j and

         A22: (h . (n + j)) <> ( - 1);

        set m2 = ((2 * n) + j);

        

         A23: j in VG by A21;

        then

         A24: 1 <= j by A13, FINSEQ_1: 1;

        then (n + 1) <= nj by XREAL_1: 7;

        then

         A25: n < nj by NAT_1: 13;

        

         A26: j <= n by A13, A23, FINSEQ_1: 1;

        then

         A27: 1 < m2 & m2 < mi by A24, Lm11;

        j > 1 by A2, A20, A21, A24, XXREAL_0: 1;

        then j >= (1 + 1) by INT_1: 7;

        then

         A28: (f . nj) = ( - 1) by A1, A26;

        

         A29: nj <= (2 * n) by A24, A26, Lm12;

        

         A30: mi in ( dom f) by A8, A5, FINSEQ_3: 25;

        

        then

         A31: ((M . f0) /. mi) = ((M . f0) . mi) by A14, PARTFUN1:def 6

        .= jj by A16, A27, A30, Th17;

        

         A32: 1 < w1 & w1 < mi by A3, Lm11;

        then w1 in ( dom f) by A5, FINSEQ_3: 25;

        

        then

         A33: ((M . f0) /. ((2 * n) + ((M . f0) /. mi))) = ((M . f0) . w1) by A14, A31, PARTFUN1:def 6

        .= (f . w1) by A16, A32, Th18

        .= 0 by A1, A3;

        

         A34: m2 <= (3 * n) by A6, A26, XREAL_1: 7;

        

         A35: 1 < nj & nj < mi by A24, A26, Lm12;

        then

         A36: nj in ( dom f) by A5, FINSEQ_3: 25;

        ((M . f0) . nj) = (f . nj) by A16, A35, Th18;

        then

         A37: (M . f0) hasBetterPathAt (n,(nj -' n)) by A14, A12, A22, A29, A36, A25, A28, Def14;

        ((2 * n) + 1) <= m2 by A24, XREAL_1: 7;

        then

         A38: (2 * n) < m2 by NAT_1: 13;

        set m3 = (((2 * n) + (n * 1)) + j);

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

        reconsider p = <*1, jj*> as FinSequence of NAT ;

        

         A39: (p . 1) = 1 by FINSEQ_1: 44;

        

         A40: 1 < m3 & m3 < mi by A3, A26, Lm13;

        then m3 in ( dom f) by A5, FINSEQ_3: 25;

        

        then

         A41: ((M . f0) /. (((2 * n) + (n * ((M . f0) /. mi))) + j)) = ((M . f0) . m3) by A14, A31, PARTFUN1:def 6

        .= (f . m3) by A16, A40, Th18

        .= ( Weight (v1,v3,W)) by A1, A2, A21;

        

         A42: (nj -' n) = j by NAT_D: 34;

        then ((M . f0) /. (((2 * n) + (n * ((M . f0) /. mi))) + j)) >= 0 by A37;

        then

        consider e be set such that

         A43: e in the carrier' of G and

         A44: e orientedly_joins (v1,v3) by A41, Th23;

        reconsider pe = <*e*> as oriented Chain of G by A43, Th5;

        

         A45: ( len pe) = 1 by FINSEQ_1: 40;

        

         A46: ( len p) = 2 by FINSEQ_1: 44;

        then

         A47: (p . ( len p)) = j by FINSEQ_1: 44;

         A48:

        now

          let k be Nat;

          assume 1 <= k & k <= ( len pe);

          then

           A49: k = 1 by A45, XXREAL_0: 1;

          

          hence (the Source of G . (pe . k)) = (the Source of G . e) by FINSEQ_1: 40

          .= (p . k) by A2, A44, A39, A49, GRAPH_4:def 1;

          

          thus (the Target of G . (pe . k)) = (the Target of G . e) by A49, FINSEQ_1: 40

          .= (p . (k + 1)) by A21, A44, A46, A47, A49, GRAPH_4:def 1;

        end;

        

         A50: (h . nj) = 1 by A14, A12, A29, A36, A25, A37, A31, Def14;

        now

          let k;

          assume that

           A51: 1 <= k and

           A52: k < ( len p);

          k < (1 + 1) by A52, FINSEQ_1: 44;

          then k <= 1 by NAT_1: 13;

          then k = 1 by A51, XXREAL_0: 1;

          hence (p . (( len p) - k)) = (h . (n + (p /. ((( len p) - k) + 1)))) by A50, A39, A46, A47, FINSEQ_4: 15;

        end;

        then

         A53: p is_vertex_seq_at (h,j,n) by A47;

        (m2 -' (2 * n)) = j & m2 in ( dom (M . f0)) by A5, A14, A27, FINSEQ_3: 25, NAT_D: 34;

        

        then

         A54: (( Relax ((M . f0),n)) . m2) = ( newpathcost ((M . f0),n,(m2 -' (2 * n)))) by A42, A37, A34, A38, Def14

        .= ( 0 + ((M . f0) /. (((2 * n) + (n * ((M . f0) /. mi))) + j))) by A33, NAT_D: 34;

        take p, pe;

        p is one-to-one by A2, A20, A21, FINSEQ_3: 94;

        hence p is_simple_vertex_seq_at (h,j,n) by A39, A46, A53;

        hereby

          let i;

          assume that

           A55: 1 <= i and

           A56: i < ( len p);

          (i + 1) <= (1 + 1) by A46, A56, INT_1: 7;

          then i <= 1 by XREAL_1: 6;

          then i = 1 by A55, XXREAL_0: 1;

          hence (p . i) in ( UsedVx (h,n)) by A11, A39, TARSKI:def 1;

        end;

        ( len p) = (( len pe) + 1) by A45, FINSEQ_1: 44;

        hence pe is_oriented_edge_seq_of p by A48;

        thus pe is_shortestpath_of (v1,v3,( UsedVx (h,n)),W) by A2, A11, A43, A44, Th14;

        

        thus ( cost (pe,W)) = (W . (pe . 1)) by A19, A45, Th4, GRAPH_5: 46

        .= (W . e) by FINSEQ_1: 40

        .= (h . ((2 * n) + j)) by A12, A41, A54, A43, A44, Th25;

        assume not v3 in ( UsedVx (h,n));

        for v2 st v2 in ( UsedVx (h,n)) & v2 <> v1 & not ex Q st Q is_shortestpath_of (v1,v2,( UsedVx (h,n)),W) & ( cost (Q,W)) <= ( cost (pe,W)) holds contradiction by A2, A11, TARSKI:def 1;

        hence pe islongestInShortestpath (( UsedVx (h,n)),v1,W) by GRAPH_5:def 19;

      end;

      

       A57: (2 * n) < mi by Lm7;

      

       A58: (2 * 1) <= (2 * n) by A3, XREAL_1: 64;

      1 < nk by A3, Lm12;

      then

       A59: nk in ( dom f) by A5, A18, FINSEQ_3: 25;

      

       A60: n < nk by NAT_1: 13;

      nk <= (2 * n) by A3, Lm12;

      

      then

       A61: (h . nk) = ((M . f0) . nk) by A14, A12, A60, A59, A17, Def14

      .= (f0 . nk) by A18, A60, Th31

      .= 0 by A7, Th21;

      

       A62: (n * 1) <= (n * n) by A3, XREAL_1: 64;

      hereby

        

         A63: n < mi by Lm7;

        let m, j;

        assume that

         A64: (h . (n + j)) = ( - 1) and

         A65: 1 <= j and

         A66: j <= n and

         A67: m in ( UsedVx (h,n));

        reconsider v2 = j as Vertex of G by A13, A65, A66, FINSEQ_1: 1;

        

         A68: (3 * n) < mi by Lm7;

        set m2 = ((2 * n) + j);

        m2 <= (3 * n) by A6, A66, XREAL_1: 7;

        then

         A69: m2 < mi by A68, XXREAL_0: 2;

        ((2 * n) + 1) <= m2 by A65, XREAL_1: 7;

        then (2 * n) < m2 by NAT_1: 13;

        then 2 < m2 by A58, XXREAL_0: 2;

        then

         A70: 1 < m2 by XXREAL_0: 2;

        j <> 1 by A61, A64;

        

        then

         A71: ((M . f0) . j) = (f . j) by A16, A66, A63, Th18

        .= 1 by A1, A65, A66;

        

         A72: mi in ( dom f) by A8, A5, FINSEQ_3: 25;

        

        then

         A73: ((M . f0) /. mi) = ((M . f0) . mi) by A14, PARTFUN1:def 6

        .= 1 by A16, A69, A70, A72, Th17;

        set nj = (n + j);

        (1 + 1) <= nj by A3, A65, XREAL_1: 7;

        then

         A74: 1 < nj by NAT_1: 13;

        

         A75: nj <= (n + n) by A66, XREAL_1: 7;

        then nj < mi by A57, XXREAL_0: 2;

        then

         A76: nj in ( dom f) by A5, A74, FINSEQ_3: 25;

        (n + 1) <= nj by A65, XREAL_1: 7;

        then

         A77: n < nj by NAT_1: 13;

        

         A78: nj <= (2 * n) by A75;

        then

         A79: not (M . f0) hasBetterPathAt (n,(nj -' n)) by A14, A12, A64, A76, A77, A73, Def14;

        then (nj -' n) = j & ((M . f0) . nj) = ( - 1) by A14, A12, A64, A78, A76, A77, Def14, NAT_D: 34;

        then

         A80: not ((M . f0) /. (((2 * n) + (n * ((M . f0) /. mi))) + j)) >= 0 by A79, A71;

        set m3 = (((2 * n) + (n * 1)) + j);

        m3 = ((2 * n) + ((n * 1) + j));

        then 2 <= m3 by A58, NAT_1: 12;

        then

         A81: 1 < m3 by XXREAL_0: 2;

        j <= (n * n) by A62, A66, XXREAL_0: 2;

        then m3 <= ((3 * n) + (n * n)) by XREAL_1: 7;

        then

         A82: m3 < mi by NAT_1: 13;

        then m3 in ( dom f) by A5, A81, FINSEQ_3: 25;

        then

         A83: ((M . f0) /. (((2 * n) + (n * ((M . f0) /. mi))) + j)) = ((M . f0) . m3) by A14, A73, PARTFUN1:def 6;

        ((M . f0) . m3) = (f . m3) by A16, A81, A82, Th18

        .= ( Weight (v1,v2,W)) by A1, A2;

        then not ex e be set st e in the carrier' of G & e orientedly_joins (v1,v2) by A80, A83, Th23;

        then

         A84: ( Weight (v1,v2,W)) = ( - 1) by Def7;

        m = 1 by A11, A67, TARSKI:def 1;

        hence (f . (((2 * n) + (n * m)) + j)) = ( - 1) by A1, A2, A84;

      end;

      let m;

      assume m in ( UsedVx (h,n));

      then m = 1 by A11, TARSKI:def 1;

      hence thesis by A61;

    end;

    

     Lm16: g = ((( repeat (( Relax n) * ( findmin n))) . k) . f) & h = ((( repeat (( Relax n) * ( findmin n))) . (k + 1)) . f) & ( OuterVx (g,n)) <> {} & i in ( UsedVx (g,n)) & ( len f) = (((n * n) + (3 * n)) + 1) implies (h . (n + i)) = (g . (n + i))

    proof

      set R = ( Relax n), M = ( findmin n), RF = ( repeat (R * M));

      set mi = (((n * n) + (3 * n)) + 1), Ak = ( Argmin (( OuterVx (g,n)),g,n));

      assume that

       A1: g = ((RF . k) . f) and

       A2: h = ((RF . (k + 1)) . f) and

       A3: ( OuterVx (g,n)) <> {} and

       A4: i in ( UsedVx (g,n)) and

       A5: ( len f) = mi;

      

       A6: h = (R . (M . g)) by A1, A2, Th22

      .= ( Relax ((M . g),n)) by Def15;

      set ni = (n + i);

      

       A7: ex j st i = j & j in ( dom g) & 1 <= j & j <= n & (g . j) = ( - 1) by A4;

      then

       A8: ni <= (n + n) by XREAL_1: 7;

      

       A9: 1 <= ni by A7, NAT_1: 12;

      

       A10: (2 * n) < mi by Lm7;

      then ni < mi by A8, XXREAL_0: 2;

      then ni in ( dom f) by A5, A9, FINSEQ_3: 25;

      then ni in ( dom g) by A1, Th41;

      then

       A11: (ni -' n) = i & ni in ( dom (M . g)) by Th33, NAT_D: 34;

      

       A12: Ak <= n by A3, Th29;

      

       A13: n < mi by Lm7;

      

       A14: (M . g) = ((g,mi) := (Ak,( - jj))) by Def11;

      (g . Ak) <> ( - 1) by A3, Th29;

      then

       A15: not (M . g) hasBetterPathAt (n,i) by A14, A7, A13, Th18;

      (n + 1) <= ni by A7, XREAL_1: 7;

      then

       A16: n < ni by NAT_1: 13;

      ni <= (2 * n) by A8;

      

      hence (h . ni) = ((M . g) . ni) by A6, A16, A11, A15, Def14

      .= (g . ni) by A14, A12, A8, A16, A10, Th18;

    end;

    

     Lm17: g = ((( repeat (( Relax n) * ( findmin n))) . k) . f) & h = ((( repeat (( Relax n) * ( findmin n))) . (k + 1)) . f) & ( OuterVx (g,n)) <> {} & ( len f) = (((n * n) + (3 * n)) + 1) & p is_simple_vertex_seq_at (g,j,n) & (g . (n + j)) = (h . (n + j)) & (for i st 1 <= i & i < ( len p) holds (p . i) in ( UsedVx (g,n))) implies p is_simple_vertex_seq_at (h,j,n)

    proof

      set RT = ( repeat (( Relax n) * ( findmin n)));

      assume that

       A1: g = ((RT . k) . f) & h = ((RT . (k + 1)) . f) & ( OuterVx (g,n)) <> {} & ( len f) = (((n * n) + (3 * n)) + 1) and

       A2: p is_simple_vertex_seq_at (g,j,n) and

       A3: (g . (n + j)) = (h . (n + j)) and

       A4: for i st 1 <= i & i < ( len p) holds (p . i) in ( UsedVx (g,n));

      

       A5: ( len p) > 1 by A2;

      

       A6: p is_vertex_seq_at (g,j,n) by A2;

      then

       A7: (p . ( len p)) = j;

      now

        let k;

        assume that

         A8: 1 <= k and

         A9: k < ( len p);

        

         A10: (k - k) < (( len p) - k) by A9, XREAL_1: 14;

        then

        reconsider m = (( len p) - k) as Element of NAT by INT_1: 3;

        m <= (( len p) - 1) by A8, XREAL_1: 13;

        then

         A11: (m + 1) <= ((( len p) - 1) + 1) by XREAL_1: 7;

        

         A12: (1 + 0 ) < (m + 1) by A10, XREAL_1: 8;

        then

         A13: (p /. (m + 1)) = (p . (m + 1)) by A11, FINSEQ_4: 15;

        per cases ;

          suppose (m + 1) = ( len p);

          hence (p . (( len p) - k)) = (h . (n + (p /. ((( len p) - k) + 1)))) by A3, A5, A6, A13;

        end;

          suppose (m + 1) <> ( len p);

          then

           A14: (m + 1) < ( len p) by A11, XXREAL_0: 1;

          

          thus (p . (( len p) - k)) = (g . (n + (p /. ((( len p) - k) + 1)))) by A6, A8, A9

          .= (h . (n + (p /. ((( len p) - k) + 1)))) by A1, A4, A12, A13, A14, Lm16;

        end;

      end;

      then

       A15: p is_vertex_seq_at (h,j,n) by A7;

      (p . 1) = 1 & p is one-to-one by A2;

      hence thesis by A5, A15;

    end;

    

     Lm18: g = ((( repeat (( Relax n) * ( findmin n))) . k) . f) & h = ((( repeat (( Relax n) * ( findmin n))) . (k + 1)) . f) & ( OuterVx (g,n)) <> {} & ( len f) = (((n * n) + (3 * n)) + 1) & p is_simple_vertex_seq_at (g,m,n) & m = (h . (n + j)) & (g . (n + m)) = (h . (n + m)) & m <> j & not j in ( UsedVx (g,n)) & (for i st 1 <= i & i < ( len p) holds (p . i) in ( UsedVx (g,n))) implies for q be FinSequence of NAT st q = (p ^ <*j*>) holds q is_simple_vertex_seq_at (h,j,n)

    proof

      set RT = ( repeat (( Relax n) * ( findmin n)));

      assume that

       A1: g = ((RT . k) . f) & h = ((RT . (k + 1)) . f) & ( OuterVx (g,n)) <> {} & ( len f) = (((n * n) + (3 * n)) + 1) and

       A2: p is_simple_vertex_seq_at (g,m,n) and

       A3: m = (h . (n + j)) and

       A4: (g . (n + m)) = (h . (n + m)) and

       A5: m <> j and

       A6: not j in ( UsedVx (g,n)) and

       A7: for i st 1 <= i & i < ( len p) holds (p . i) in ( UsedVx (g,n));

      

       A8: p is_vertex_seq_at (g,m,n) by A2;

      then

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

      let q be FinSequence of NAT such that

       A10: q = (p ^ <*j*>);

      

       A11: ( len p) > 1 by A2;

      

       A12: ( len q) = (( len p) + 1) by FINSEQ_2: 16, A10;

      then

       A13: (q . ( len q)) = j by FINSEQ_1: 42, A10;

      now

        let ii be Nat;

        assume that

         A14: 1 <= ii and

         A15: ii < ( len q);

        

         A16: (ii - ii) < (( len q) - ii) by A15, XREAL_1: 14;

        then

        reconsider mm = (( len q) - ii) as Element of NAT by INT_1: 3;

        

         A17: (1 + 0 ) < (mm + 1) by A16, XREAL_1: 8;

        mm <= (( len q) - 1) by A14, XREAL_1: 13;

        then

         A18: (mm + 1) <= ((( len q) - 1) + 1) by XREAL_1: 7;

        then

         A19: (q /. (mm + 1)) = (q . (mm + 1)) by A17, FINSEQ_4: 15;

        per cases ;

          suppose (mm + 1) = ( len q);

          hence (q . (( len q) - ii)) = (h . (n + (q /. ((( len q) - ii) + 1)))) by A3, A11, A9, A12, A13, A19, Lm1, A10;

        end;

          suppose (mm + 1) <> ( len q);

          then

           A20: (mm + 1) < ( len q) by A18, XXREAL_0: 1;

          then

           A21: (mm + 1) <= ( len p) by A12, INT_1: 7;

          

           A22: (1 + 0 ) <= mm by A16, INT_1: 7;

          mm < ( len p) by A12, A20, XREAL_1: 7;

          then

           A23: (q . (( len q) - ii)) = (p . mm) by A22, Lm1, A10;

          hereby

            per cases ;

              suppose

               A24: (mm + 1) = ( len p);

              

               A25: (p /. ((( len p) - 1) + 1)) = m by A11, A9, FINSEQ_4: 15;

              (q /. ((( len q) - ii) + 1)) = m by A11, A9, A19, A24, Lm1, A10;

              hence (q . (( len q) - ii)) = (h . (n + (q /. ((( len q) - ii) + 1)))) by A4, A11, A8, A23, A24, A25;

            end;

              suppose

               A26: (mm + 1) <> ( len p);

              set i2 = (ii - 1);

              

               A27: (mm + 1) < ( len p) by A21, A26, XXREAL_0: 1;

               A28:

              now

                assume i2 <= 1;

                then (( len p) - 1) <= (( len p) - i2) by XREAL_1: 13;

                hence contradiction by A12, A27, XREAL_1: 20;

              end;

              then

              reconsider i3 = i2 as Element of NAT by INT_1: 3;

              

               A29: (p /. (mm + 1)) = (p . (mm + 1)) by A17, A21, FINSEQ_4: 15;

              

               A30: (q /. ((( len q) - ii) + 1)) = (q . (mm + 1)) by A17, A18, FINSEQ_4: 15

              .= (p /. (mm + 1)) by A17, A21, A29, Lm1, A10;

              i2 < (( len q) - 1) by A15, XREAL_1: 14;

              

              hence (q . (( len q) - ii)) = (g . (n + (p /. ((( len p) - i3) + 1)))) by A8, A12, A23, A28

              .= (h . (n + (q /. ((( len q) - ii) + 1)))) by A1, A7, A12, A17, A27, A29, A30, Lm16;

            end;

          end;

        end;

      end;

      then

       A31: q is_vertex_seq_at (h,j,n) by A13;

       A32:

      now

        assume j in ( rng p);

        then

        consider i be Nat such that

         A33: i in ( dom p) and

         A34: j = (p . i) by FINSEQ_2: 10;

        

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

        

         A36: i <= ( len p) by A33, FINSEQ_3: 25;

        per cases ;

          suppose i = ( len p);

          hence contradiction by A5, A8, A34;

        end;

          suppose i <> ( len p);

          then i < ( len p) by A36, XXREAL_0: 1;

          hence contradiction by A6, A7, A34, A35;

        end;

      end;

      p is one-to-one by A2;

      then

       A37: q is one-to-one by A32, Th1, A10;

      (p . 1) = 1 by A2;

      then

       A38: (q . 1) = 1 by A11, Lm1, A10;

      ( len q) > 1 by A11, A12, NAT_1: 13;

      hence thesis by A38, A31, A37;

    end;

    

     Lm19: f is_Input_of_Dijkstra_Alg (G,n,W) & W is_weight>=0of G & v2 = i & v1 <> v2 & 1 <= i & i <= n & P is_shortestpath_of (v1,v2,V,W) & (for m, j st (g . (n + j)) = ( - 1) & 1 <= j & j <= n & m in V holds (f . (((2 * n) + (n * m)) + j)) = ( - 1)) implies (g . (n + i)) <> ( - 1)

    proof

      assume that

       A1: f is_Input_of_Dijkstra_Alg (G,n,W) and

       A2: W is_weight>=0of G and

       A3: v2 = i and

       A4: v1 <> v2 and

       A5: 1 <= i & i <= n and

       A6: P is_shortestpath_of (v1,v2,V,W) and

       A7: for m, j st (g . (n + j)) = ( - 1) & 1 <= j & j <= n & m in V holds (f . (((2 * n) + (n * m)) + j)) = ( - 1);

      P is_orientedpath_of (v1,v2,V) by A6, GRAPH_5:def 18;

      then

      consider q be Simple oriented Chain of G such that

       A8: q is_shortestpath_of (v1,v2,V,W) by A2, GRAPH_5: 62;

      set FT = the Target of G;

      assume

       A9: (g . (n + i)) = ( - 1);

      set e = (q . ( len q));

      consider vs be FinSequence of the carrier of G such that

       A10: vs is_oriented_vertex_seq_of q and

       A11: for n1,m1 be Nat st 1 <= n1 & n1 < m1 & m1 <= ( len vs) & (vs . n1) = (vs . m1) holds n1 = 1 & m1 = ( len vs) by GRAPH_4:def 7;

      

       A12: q is_orientedpath_of (v1,v2,V) by A8, GRAPH_5:def 18;

      then

       A13: q is_orientedpath_of (v1,v2) by GRAPH_5:def 4;

      then q <> {} by GRAPH_5:def 3;

      then

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

      then

       A15: e orientedly_joins ((vs /. ( len q)),(vs /. (( len q) + 1))) by A10, GRAPH_4:def 5;

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

      then

       A16: e in the carrier' of G by FINSEQ_2: 11;

      

       A17: ( len vs) = (( len q) + 1) by A10, GRAPH_4:def 5;

      then

       A18: ( len q) < ( len vs) by NAT_1: 13;

      then

       A19: ( len q) in ( dom vs) by A14, FINSEQ_3: 25;

      

       A20: (vs /. ( len q)) = (vs . ( len q)) by A14, A18, FINSEQ_4: 15;

      then

      reconsider v3 = (vs . ( len q)) as Vertex of G;

      (FT . (q . ( len q))) = v2 by A13, GRAPH_5:def 3;

      then

       A21: v2 = (vs /. (( len q) + 1)) by A15, GRAPH_4:def 1;

      

       A22: 1 < (( len q) + 1) by A14, NAT_1: 13;

      then

       A23: v2 = (vs . ( len vs)) by A17, A21, FINSEQ_4: 15;

      now

        

         A24: (q . 1) orientedly_joins ((vs /. 1),(vs /. (1 + 1))) by A10, A14, GRAPH_4:def 5;

        assume

         A25: v3 = v2;

        v1 = (the Source of G . (q . 1)) by A13, GRAPH_5:def 3

        .= (vs /. 1) by A24, GRAPH_4:def 1

        .= (vs . 1) by A17, A22, FINSEQ_4: 15

        .= v3 by A11, A14, A18, A23, A25;

        hence contradiction by A4, A25;

      end;

      then

       A26: not v3 in {v2} by TARSKI:def 1;

      ( Seg n) = the carrier of G by A1;

      then v3 in ( Seg n) by A19, FINSEQ_2: 11;

      then

      reconsider m = v3 as Element of NAT ;

      

       A27: (f . (((2 * n) + (n * m)) + i)) = ( Weight (v3,v2,W)) by A1, A3;

      v3 = (the Source of G . e) by A15, A20, GRAPH_4:def 1;

      then v3 in ( vertices q) by A14, Lm4;

      then

       A28: m in (( vertices q) \ {v2}) by A26, XBOOLE_0:def 5;

      (( vertices q) \ {v2}) c= V by A12, GRAPH_5:def 4;

      then (f . (((2 * n) + (n * m)) + i)) = ( - 1) by A5, A7, A9, A28;

      hence contradiction by A15, A16, A20, A21, A27, Th23;

    end;

    

     Lm20: f is_Input_of_Dijkstra_Alg (G,n,W) & v1 = 1 & n >= 1 & g = ((( repeat (( Relax n) * ( findmin n))) . k) . f) & h = ((( repeat (( Relax n) * ( findmin n))) . (k + 1)) . f) & ( OuterVx (g,n)) <> {} & 1 in ( UsedVx (g,n)) & (for v3, j st v3 <> v1 & v3 = j & (g . (n + j)) <> ( - 1) holds ex p, P st p is_simple_vertex_seq_at (g,j,n) & (for i st 1 <= i & i < ( len p) holds (p . i) in ( UsedVx (g,n))) & P is_oriented_edge_seq_of p & P is_shortestpath_of (v1,v3,( UsedVx (g,n)),W) & ( cost (P,W)) = (g . ((2 * n) + j)) & ( not v3 in ( UsedVx (g,n)) implies P islongestInShortestpath (( UsedVx (g,n)),v1,W))) & (for m, j st (g . (n + j)) = ( - 1) & 1 <= j & j <= n & m in ( UsedVx (g,n)) holds (f . (((2 * n) + (n * m)) + j)) = ( - 1)) & (for m st m in ( UsedVx (g,n)) holds (g . (n + m)) <> ( - 1)) implies (for v3, j st v3 <> v1 & v3 = j & (h . (n + j)) <> ( - 1) holds ex p, P st p is_simple_vertex_seq_at (h,j,n) & (for i st 1 <= i & i < ( len p) holds (p . i) in ( UsedVx (h,n))) & P is_oriented_edge_seq_of p & P is_shortestpath_of (v1,v3,( UsedVx (h,n)),W) & ( cost (P,W)) = (h . ((2 * n) + j)) & ( not v3 in ( UsedVx (h,n)) implies P islongestInShortestpath (( UsedVx (h,n)),v1,W))) & (for m, j st (h . (n + j)) = ( - 1) & 1 <= j & j <= n & m in ( UsedVx (h,n)) holds (f . (((2 * n) + (n * m)) + j)) = ( - 1)) & for m st m in ( UsedVx (h,n)) holds (h . (n + m)) <> ( - 1)

    proof

      set R = ( Relax n), M = ( findmin n), IN = ( OuterVx (g,n)), Ug = ( UsedVx (g,n));

      assume that

       A1: f is_Input_of_Dijkstra_Alg (G,n,W) and

       A2: v1 = 1 and

       A3: n >= 1 and

       A4: g = ((( repeat (R * M)) . k) . f) and

       A5: h = ((( repeat (R * M)) . (k + 1)) . f) and

       A6: IN <> {} and

       A7: 1 in Ug;

      assume

       A8: for v3, j st v3 <> v1 & v3 = j & (g . (n + j)) <> ( - 1) holds ex p, P st p is_simple_vertex_seq_at (g,j,n) & (for i st 1 <= i & i < ( len p) holds (p . i) in Ug) & P is_oriented_edge_seq_of p & P is_shortestpath_of (v1,v3,Ug,W) & ( cost (P,W)) = (g . ((2 * n) + j)) & ( not v3 in Ug implies P islongestInShortestpath (Ug,v1,W));

      assume that

       A9: for m, j st (g . (n + j)) = ( - 1) & 1 <= j & j <= n & m in Ug holds (f . (((2 * n) + (n * m)) + j)) = ( - 1) and

       A10: for m st m in ( UsedVx (g,n)) holds (g . (n + m)) <> ( - 1);

      set mi = (((n * n) + (3 * n)) + 1), Ak = ( Argmin (IN,g,n));

      

       A11: 1 <= mi by NAT_1: 12;

      

       A12: ( len f) = mi by A1;

      

       A13: (M . g) = ((g,mi) := (Ak,( - jj))) by Def11;

      

       A14: ( dom (M . g)) = ( dom g) by Th33;

      h = (R . (M . g)) by A4, A5, Th22;

      then

       A15: h = ( Relax ((M . g),n)) by Def15;

      

       A16: ( Seg n) = the carrier of G by A1;

      then

      reconsider VG = the carrier of G as non empty Subset of NAT by A3;

      

       A17: W is_weight>=0of G by GRAPH_5:def 13;

      

       A18: ((2 * n) + n) = ((2 + 1) * n);

      

       A19: ( dom f) = ( dom g) by A4, Th41;

      

       A20: 1 <= Ak by A6, Th29;

      

       A21: Ak <= n by A6, Th29;

      

       A22: (g . (n + Ak)) <> ( - 1) by A6, Th29;

      set Uh = ( UsedVx (h,n));

      

       A23: Uh = (Ug \/ {Ak}) & not Ak in Ug by A4, A5, A6, Th39;

      then

       A24: Ug c= Uh by XBOOLE_1: 7;

      

       A25: n < mi by Lm7;

      

       A26: ( dom f) = ( dom h) by A5, Th41;

      reconsider vk = Ak as Vertex of G by A16, A20, A21, FINSEQ_1: 1;

      consider pk be FinSequence of NAT , PK be oriented Chain of G such that

       A27: pk is_simple_vertex_seq_at (g,Ak,n) and

       A28: for i st 1 <= i & i < ( len pk) holds (pk . i) in Ug and

       A29: PK is_oriented_edge_seq_of pk and

       A30: PK is_shortestpath_of (v1,vk,Ug,W) and

       A31: ( cost (PK,W)) = (g . ((2 * n) + Ak)) and

       A32: not vk in Ug implies PK islongestInShortestpath (Ug,v1,W) by A2, A7, A8, A22, A23;

      

       A33: ex kk be Nat st (kk = Ak) & (kk in IN) & (for i st i in IN holds (g /. ((2 * n) + kk)) <= (g /. ((2 * n) + i))) & (for i st i in IN & (g /. ((2 * n) + kk)) = (g /. ((2 * n) + i)) holds kk <= i) by A6, Def10;

      set nAk = ((2 * n) + Ak);

      

       A34: 1 < nAk by A20, A21, Lm11;

      

       A35: nAk < mi by A20, A21, Lm11;

      

       A36: Ak < nAk by A20, A21, Lm11;

      

       A37: nAk in ( dom g) by A12, A19, A34, A35, FINSEQ_3: 25;

      

       A38: (f,g) equal_at (((3 * n) + 1),((n * n) + (3 * n))) by A4, Th46;

      PK is_orientedpath_of (v1,vk,Ug) by A30, GRAPH_5:def 18;

      then

       A39: PK is_orientedpath_of (v1,vk) by GRAPH_5:def 4;

      then PK <> {} by GRAPH_5:def 3;

      then

       A40: ( len PK) >= 1 by FINSEQ_1: 20;

      

       A41: mi in ( dom g) by A11, A12, A19, FINSEQ_3: 25;

      

      then

       A42: ((M . g) /. mi) = ((M . g) . mi) by A14, PARTFUN1:def 6

      .= Ak by A13, A21, A25, A41, Th17;

      

       A43: ((M . g) /. nAk) = ((M . g) . nAk) by A14, A37, PARTFUN1:def 6

      .= ( cost (PK,W)) by A13, A31, A35, A36, Th18;

      set nk = (n + Ak);

      

       A44: 1 < nk by A20, A21, Lm12;

      

       A45: nk <= (2 * n) by A20, A21, Lm12;

      

       A46: nk < mi by A20, A21, Lm12;

      (n + 1) <= nk by A20, XREAL_1: 7;

      then

       A47: n < nk by NAT_1: 13;

      

       A48: nk in ( dom g) by A12, A19, A44, A46, FINSEQ_3: 25;

      

       A49: ((M . g) . nk) = (g . nk) by A46, A47, Th31;

      now

        set Wke = ((M . g) /. (((2 * n) + (n * ((M . g) /. mi))) + Ak));

        assume

         A50: (M . g) hasBetterPathAt (n,Ak);

        then

         A51: ((M . g) . nk) = ( - 1) or ((M . g) /. nAk) > ( newpathcost ((M . g),n,Ak));

        Wke >= 0 by A50;

        then (((M . g) /. nAk) + Wke) >= (((M . g) /. nAk) + 0 ) by XREAL_1: 7;

        hence contradiction by A6, A42, A49, A51, Th29;

      end;

      then not (M . g) hasBetterPathAt (n,(nk -' n)) by NAT_D: 34;

      then

       A52: (h . nk) = (g . nk) by A14, A15, A45, A47, A48, A49, Def14;

      hereby

        let v3, j;

        assume that

         A53: v3 <> v1 and

         A54: v3 = j and

         A55: (h . (n + j)) <> ( - 1);

        set nj = (n + j);

        

         A56: j in VG by A54;

        then

         A57: 1 <= j by A16, FINSEQ_1: 1;

        

         A58: j <= n by A16, A56, FINSEQ_1: 1;

        then

         A59: 1 < nj by A57, Lm12;

        

         A60: nj <= (2 * n) by A57, A58, Lm12;

        

         A61: nj < mi by A57, A58, Lm12;

        then

         A62: nj in ( dom g) by A12, A19, A59, FINSEQ_3: 25;

        

         A63: (nj -' n) = j by NAT_D: 34;

        (n + 1) <= nj by A57, XREAL_1: 7;

        then

         A64: n < nj by NAT_1: 13;

        set m2 = ((2 * n) + j);

        

         A65: m2 <= (3 * n) by A18, A58, XREAL_1: 7;

        ((2 * n) + 1) <= m2 by A57, XREAL_1: 7;

        then

         A66: (2 * n) < m2 by NAT_1: 13;

        

         A67: (m2 -' (2 * n)) = j by NAT_D: 34;

        

         A68: 1 < m2 by A57, A58, Lm11;

        

         A69: m2 < mi by A57, A58, Lm11;

        then

         A70: m2 in ( dom g) by A12, A19, A68, FINSEQ_3: 25;

        

         A71: m2 in ( dom (M . g)) by A12, A14, A19, A68, A69, FINSEQ_3: 25;

        

         A72: ((M . g) . nj) = (g . nj) by A13, A21, A61, A64, Th18;

        n <= (2 * n) by Lm6;

        then n < m2 by A66, XXREAL_0: 2;

        then

         A73: ((M . g) . m2) = (g . m2) by A13, A21, A69, Th18;

        

         A74: j < mi by A25, A58, XXREAL_0: 2;

        then

         A75: j in ( dom g) by A12, A19, A57, FINSEQ_3: 25;

        

         A76: j in ( dom h) by A12, A26, A57, A74, FINSEQ_3: 25;

        set Akj = (((2 * n) + (n * Ak)) + j);

        

         A77: 1 < Akj by A20, A21, A58, Lm13;

        

         A78: Ak < Akj by A20, A21, A58, Lm13;

        

         A79: Akj < mi by A20, A21, A58, Lm13;

        then

         A80: Akj in ( dom g) by A12, A19, A77, FINSEQ_3: 25;

        

         A81: ((3 * n) + 1) <= Akj by A20, A21, A57, A58, Lm14;

        

         A82: Akj <= ((n * n) + (3 * n)) by A20, A21, A57, A58, Lm14;

        

         A83: ((M . g) /. (((2 * n) + (n * ((M . g) /. mi))) + j)) = ((M . g) . Akj) by A14, A42, A80, PARTFUN1:def 6

        .= (g . Akj) by A13, A78, A79, Th18

        .= (f . Akj) by A38, A80, A81, A82

        .= ( Weight (vk,v3,W)) by A1, A54;

        

         A84: ((M . g) /. m2) = (g . m2) by A14, A70, A73, PARTFUN1:def 6;

        per cases ;

          suppose

           A85: not (M . g) hasBetterPathAt (n,(nj -' n));

          then

           A86: (h . nj) = (g . nj) by A14, A15, A60, A62, A64, A72, Def14;

          then

          consider p, P such that

           A87: p is_simple_vertex_seq_at (g,j,n) and

           A88: for i st 1 <= i & i < ( len p) holds (p . i) in Ug and

           A89: P is_oriented_edge_seq_of p and

           A90: P is_shortestpath_of (v1,v3,Ug,W) and

           A91: ( cost (P,W)) = (g . m2) and

           A92: not v3 in Ug implies P islongestInShortestpath (Ug,v1,W) by A8, A53, A54, A55;

          take p, P;

          thus p is_simple_vertex_seq_at (h,j,n) by A4, A5, A6, A12, A86, A87, A88, Lm17;

          thus for i st 1 <= i & i < ( len p) holds (p . i) in Uh by A24, A88;

          thus P is_oriented_edge_seq_of p by A89;

          hereby

            per cases ;

              suppose ((M . g) . j) = ( - 1);

              then (( Relax ((M . g),n)) . j) = ( - 1) by A14, A58, A75, Def14;

              then j in { i : i in ( dom h) & 1 <= i & i <= n & (h . i) = ( - 1) } by A15, A57, A58, A76;

              then

               A93: j in Ug or j in {Ak} by A23, XBOOLE_0:def 3;

              now

                let Q, v4;

                assume that

                 A94: not v4 in Ug and

                 A95: Q is_shortestpath_of (v1,v4,Ug,W);

                

                 A96: v4 in VG;

                then

                reconsider j4 = v4 as Element of NAT ;

                

                 A97: 1 <= j4 by A16, A96, FINSEQ_1: 1;

                

                 A98: j4 <= n by A16, A96, FINSEQ_1: 1;

                then

                 A99: (g . (n + j4)) <> ( - 1) by A1, A2, A7, A9, A17, A94, A95, A97, Lm19;

                then

                consider q, R such that q is_simple_vertex_seq_at (g,j4,n) and for i st 1 <= i & i < ( len q) holds (q . i) in Ug and R is_oriented_edge_seq_of q and

                 A100: R is_shortestpath_of (v1,v4,Ug,W) and

                 A101: ( cost (R,W)) = (g . ((2 * n) + j4)) and

                 A102: not v4 in Ug implies R islongestInShortestpath (Ug,v1,W) by A2, A7, A8, A94;

                

                 A103: ( cost (R,W)) = ( cost (Q,W)) by A95, A100, Th9;

                per cases by A93, TARSKI:def 1;

                  suppose j in Ug;

                  then ex PP be oriented Chain of G st (PP is_shortestpath_of (v1,v3,Ug,W)) & (( cost (PP,W)) <= ( cost (R,W))) by A53, A54, A94, A102, GRAPH_5:def 19;

                  hence ( cost (P,W)) <= ( cost (Q,W)) by A90, A103, Th9;

                end;

                  suppose

                   A104: j = Ak;

                  j4 <= mi by A25, A98, XXREAL_0: 2;

                  then

                   A105: j4 in ( dom g) by A12, A19, A97, FINSEQ_3: 25;

                  then (g . j4) <> ( - 1) by A94, A97, A98;

                  then j4 in { i : i in ( dom g) & 1 <= i & i <= n & (g . i) <> ( - 1) & (g . (n + i)) <> ( - 1) } by A97, A98, A99, A105;

                  then

                   A106: (g /. ((2 * n) + Ak)) <= (g /. ((2 * n) + j4)) by A33;

                  

                   A107: (g /. ((2 * n) + Ak)) = (g . ((2 * n) + Ak)) by A37, PARTFUN1:def 6;

                  

                   A108: 1 < ((2 * n) + j4) by A97, A98, Lm11;

                  ((2 * n) + j4) < mi by A97, A98, Lm11;

                  then ((2 * n) + j4) in ( dom g) by A12, A19, A108, FINSEQ_3: 25;

                  hence ( cost (P,W)) <= ( cost (Q,W)) by A91, A101, A103, A104, A106, A107, PARTFUN1:def 6;

                end;

              end;

              hence P is_shortestpath_of (v1,v3,Uh,W) by A17, A24, A53, A90, GRAPH_5: 64;

            end;

              suppose

               A109: ((M . g) . j) <> ( - 1);

              hereby

                per cases ;

                  suppose

                   A110: ((M . g) /. (((2 * n) + (n * ((M . g) /. mi))) + j)) >= 0 ;

                  then

                   A111: ((M . g) /. m2) <= ( newpathcost ((M . g),n,j)) by A63, A85, A109;

                  

                   A112: ((M . g) /. m2) = ( cost (P,W)) by A71, A73, A91, PARTFUN1:def 6;

                  consider e be set such that

                   A113: e in the carrier' of G and

                   A114: e orientedly_joins (vk,v3) by A83, A110, Th23;

                  reconsider pe = <*e*> as oriented Chain of G by A113, Th5;

                  

                   A115: ( len pe) = 1 by FINSEQ_1: 40;

                  

                   A116: (pe . 1) = e by FINSEQ_1: 40;

                  then

                  consider Q such that

                   A117: Q = (PK ^ pe) and Q is_orientedpath_of (v1,v3) by A39, A40, A114, A115, GRAPH_5: 33;

                  ( cost (pe,W)) = (W . (pe . 1)) by A17, A115, Th4, GRAPH_5: 46

                  .= ( Weight (vk,v3,W)) by A113, A114, A116, Th25;

                  then ( cost (Q,W)) = ( newpathcost ((M . g),n,j)) by A17, A42, A43, A83, A117, GRAPH_5: 46, GRAPH_5: 54;

                  hence P is_shortestpath_of (v1,v3,Uh,W) by A2, A7, A17, A23, A30, A32, A40, A53, A90, A111, A112, A113, A114, A117, GRAPH_5: 65;

                end;

                  suppose ((M . g) /. (((2 * n) + (n * ((M . g) /. mi))) + j)) < 0 ;

                  then not ex e be set st e in the carrier' of G & e orientedly_joins (vk,v3) by A83, Th23;

                  hence P is_shortestpath_of (v1,v3,Uh,W) by A2, A7, A17, A23, A30, A32, A53, A90, Th13;

                end;

              end;

            end;

          end;

          thus ( cost (P,W)) = (h . m2) by A15, A63, A65, A66, A67, A71, A73, A85, A91, Def14;

          hereby

            assume

             A118: not v3 in Uh;

            then

             A119: not v3 in Ug by A23, XBOOLE_0:def 3;

            now

              let v2;

              assume that

               A120: v2 in Uh and

               A121: v2 <> v1;

              per cases by A23, A120, XBOOLE_0:def 3;

                suppose v2 in {Ak};

                then

                 A122: v2 = vk by TARSKI:def 1;

                take PK;

                thus PK is_shortestpath_of (v1,v2,Uh,W) by A23, A30, A122, Th8;

                (g . j) <> ( - 1) by A54, A57, A58, A75, A119;

                then j in { i : i in ( dom g) & 1 <= i & i <= n & (g . i) <> ( - 1) & (g . (n + i)) <> ( - 1) } by A55, A57, A58, A75, A86;

                then

                 A123: (g /. nAk) <= (g /. m2) by A33;

                (g /. nAk) = ( cost (PK,W)) by A31, A37, PARTFUN1:def 6;

                hence ( cost (PK,W)) <= ( cost (P,W)) by A70, A91, A123, PARTFUN1:def 6;

              end;

                suppose

                 A124: v2 in Ug;

                then

                consider Q such that

                 A125: Q is_shortestpath_of (v1,v2,Ug,W) and

                 A126: ( cost (Q,W)) <= ( cost (P,W)) by A23, A92, A118, A121, GRAPH_5:def 19, XBOOLE_0:def 3;

                 A127:

                now

                  let R, v4;

                  assume that

                   A128: not v4 in Ug and

                   A129: R is_shortestpath_of (v1,v4,Ug,W);

                  

                   A130: v4 in VG;

                  then

                  reconsider j4 = v4 as Element of NAT ;

                  

                   A131: 1 <= j4 by A16, A130, FINSEQ_1: 1;

                  j4 <= n by A16, A130, FINSEQ_1: 1;

                  then (g . (n + j4)) <> ( - 1) by A1, A2, A7, A9, A17, A128, A129, A131, Lm19;

                  then

                  consider rn be FinSequence of NAT , RR be oriented Chain of G such that rn is_simple_vertex_seq_at (g,j4,n) and for i st 1 <= i & i < ( len rn) holds (rn . i) in Ug and RR is_oriented_edge_seq_of rn and

                   A132: RR is_shortestpath_of (v1,v4,Ug,W) and ( cost (RR,W)) = (g . ((2 * n) + j4)) and

                   A133: not v4 in Ug implies RR islongestInShortestpath (Ug,v1,W) by A2, A7, A8, A128;

                  consider QQ be oriented Chain of G such that

                   A134: QQ is_shortestpath_of (v1,v2,Ug,W) and

                   A135: ( cost (QQ,W)) <= ( cost (RR,W)) by A121, A124, A128, A133, GRAPH_5:def 19;

                  ( cost (QQ,W)) = ( cost (Q,W)) by A125, A134, Th9;

                  hence ( cost (Q,W)) <= ( cost (R,W)) by A129, A132, A135, Th9;

                end;

                take Q;

                thus Q is_shortestpath_of (v1,v2,Uh,W) by A17, A24, A121, A125, A127, GRAPH_5: 64;

                thus ( cost (Q,W)) <= ( cost (P,W)) by A126;

              end;

            end;

            hence P islongestInShortestpath (Uh,v1,W) by GRAPH_5:def 19;

          end;

        end;

          suppose

           A136: (M . g) hasBetterPathAt (n,(nj -' n));

          then

           A137: (( Relax ((M . g),n)) . nj) = Ak by A14, A42, A60, A62, A64, Def14;

          

           A138: ((M . g) . nj) = ( - 1) or ((M . g) /. m2) > ( newpathcost ((M . g),n,j)) by A63, A136;

          

           A139: ((M . g) /. (((2 * n) + (n * ((M . g) /. mi))) + j)) >= 0 by A63, A136;

          

           A140: ((M . g) . j) <> ( - 1) by A63, A136;

          

           A141: ( newpathcost ((M . g),n,j)) = (((M . g) /. nAk) + ( Weight (vk,v3,W))) by A42, A83;

           A142:

          now

            assume

             A143: Ak = j;

            then

             A144: ((M . g) . nj) <> ( - 1) by A13, A21, A22, A61, A64, Th18;

            (((M . g) /. m2) + ( Weight (vk,v3,W))) >= (((M . g) /. m2) + 0 ) by A83, A139, XREAL_1: 7;

            hence contradiction by A63, A136, A141, A143, A144;

          end;

           A145:

          now

            assume j in ( UsedVx (g,n));

            then ex i st (j = i) & (i in ( dom g)) & (1 <= i) & (i <= n) & ((g . i) = ( - 1));

            hence contradiction by A25, A140, Th32;

          end;

          consider e be set such that

           A146: e in the carrier' of G & e orientedly_joins (vk,v3) by A83, A139, Th23;

          reconsider pe = <*e*> as oriented Chain of G by A146, Th5;

          

           A147: ( len pe) = 1 by FINSEQ_1: 40;

          

           A148: (pe . 1) = e by FINSEQ_1: 40;

          then

          consider Q such that

           A149: Q = (PK ^ pe) and Q is_orientedpath_of (v1,v3) by A39, A40, A146, A147, GRAPH_5: 33;

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

          reconsider q = (pk ^ <*jj*>) as FinSequence of NAT ;

          take q, Q;

          thus q is_simple_vertex_seq_at (h,j,n) by A4, A5, A6, A12, A15, A27, A28, A52, A137, A142, A145, Lm18;

          

           A150: ( len pk) > 1 by A27;

          

           A151: pk is_vertex_seq_at (g,Ak,n) by A27;

          

           A152: (q . ( len pk)) = (pk . ( len pk)) by A150, Lm1

          .= Ak by A151;

          hereby

            let i;

            assume that

             A153: 1 <= i and

             A154: i < ( len q);

            i < (( len pk) + 1) by A154, FINSEQ_2: 16;

            then

             A155: i <= ( len pk) by NAT_1: 13;

            now

              per cases ;

                suppose i = ( len pk);

                hence (q . i) in {Ak} or (q . i) in Ug by A152, TARSKI:def 1;

              end;

                suppose i <> ( len pk);

                then

                 A156: i < ( len pk) by A155, XXREAL_0: 1;

                (q . i) = (pk . i) by A153, A155, Lm1;

                hence (q . i) in {Ak} or (q . i) in Ug by A28, A153, A156;

              end;

            end;

            hence (q . i) in Uh by A23, XBOOLE_0:def 3;

          end;

          

           A157: ( len Q) = (( len PK) + 1) by A147, A149, FINSEQ_1: 22;

          

           A158: ( len pk) = (( len PK) + 1) by A29;

          then

           A159: ( len q) = (( len Q) + 1) by A157, FINSEQ_2: 16;

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

          now

            let i be Nat;

            assume that

             A160: 1 <= i and

             A161: i <= ( len Q);

            per cases ;

              suppose

               A162: i = ( len Q);

              then

               A163: (Q . i) = e by A147, A148, A149, A157, Lm2;

              then

               A164: (FT . (Q . i)) = v3 by A146, GRAPH_4:def 1;

              thus (FS . (Q . i)) = (q . i) by A146, A152, A157, A158, A162, A163, GRAPH_4:def 1;

              thus (FT . (Q . i)) = (q . (i + 1)) by A54, A157, A158, A162, A164, FINSEQ_1: 42;

            end;

              suppose i <> ( len Q);

              then

               A165: i < ( len Q) by A161, XXREAL_0: 1;

              then

               A166: i <= ( len PK) by A157, NAT_1: 13;

              then

               A167: (FS . (PK . i)) = (pk . i) by A29, A160;

              

               A168: (FT . (PK . i)) = (pk . (i + 1)) by A29, A160, A166;

              

               A169: (Q . i) = (PK . i) by A149, A160, A166, Lm1;

              

               A170: (i + 1) <= ( len pk) by A157, A158, A165, NAT_1: 13;

              thus (FS . (Q . i)) = (q . i) by A157, A158, A160, A161, A167, A169, Lm1;

              thus (FT . (Q . i)) = (q . (i + 1)) by A168, A169, A170, Lm1, NAT_1: 12;

            end;

          end;

          hence Q is_oriented_edge_seq_of q by A159;

          

           A171: (( cost (PK,W)) + ( cost (pe,W))) = ( cost (Q,W)) by A17, A149, GRAPH_5: 46, GRAPH_5: 54;

          

           A172: ( cost (pe,W)) = (W . (pe . 1)) by A17, A147, Th4, GRAPH_5: 46

          .= ( Weight (vk,v3,W)) by A146, A148, Th25;

          then

           A173: ( newpathcost ((M . g),n,j)) = ( cost (Q,W)) by A17, A42, A43, A83, A149, GRAPH_5: 46, GRAPH_5: 54;

          hereby

            per cases ;

              suppose

               A174: (g . nj) = ( - 1);

              now

                let v2;

                assume

                 A175: v2 in Ug;

                then

                reconsider m = v2 as Element of NAT ;

                ( - 1) = (f . (((2 * n) + (n * m)) + j)) by A9, A57, A58, A174, A175

                .= ( Weight (v2,v3,W)) by A1, A54;

                hence not ex e be set st e in the carrier' of G & e orientedly_joins (v2,v3) by Th23;

              end;

              hence Q is_shortestpath_of (v1,v3,Uh,W) by A2, A7, A23, A30, A53, A146, A149, Th15;

            end;

              suppose

               A176: (g . nj) <> ( - 1);

              then ex p, P st (p is_simple_vertex_seq_at (g,j,n)) & (for i st 1 <= i & i < ( len p) holds (p . i) in Ug) & (P is_oriented_edge_seq_of p) & (P is_shortestpath_of (v1,v3,Ug,W)) & (( cost (P,W)) = (g . m2)) & ( not v3 in Ug implies P islongestInShortestpath (Ug,v1,W)) by A8, A53, A54;

              hence Q is_shortestpath_of (v1,v3,Uh,W) by A2, A7, A13, A17, A21, A23, A30, A32, A40, A42, A43, A53, A61, A64, A83, A84, A138, A146, A149, A171, A172, A176, Th18, GRAPH_5: 65;

            end;

          end;

          thus ( cost (Q,W)) = (h . m2) by A15, A63, A65, A66, A67, A71, A136, A173, Def14;

           0 <= ( cost (pe,W)) by A17, GRAPH_5: 50;

          then

           A177: (( cost (PK,W)) + 0 ) <= ( cost (Q,W)) by A171, XREAL_1: 7;

          hereby

            assume not v3 in Uh;

            now

              let v2;

              assume that

               A178: v2 in Uh and

               A179: v2 <> v1;

              per cases by A23, A178, XBOOLE_0:def 3;

                suppose v2 in {Ak};

                then

                 A180: v2 = Ak by TARSKI:def 1;

                take PK;

                thus PK is_shortestpath_of (v1,v2,Uh,W) by A23, A30, A180, Th8;

                thus ( cost (PK,W)) <= ( cost (Q,W)) by A177;

              end;

                suppose

                 A181: v2 in Ug;

                then

                consider P such that

                 A182: P is_shortestpath_of (v1,v2,Ug,W) and

                 A183: ( cost (P,W)) <= ( cost (PK,W)) by A4, A5, A6, A32, A179, Th39, GRAPH_5:def 19;

                 A184:

                now

                  let R, v4;

                  assume that

                   A185: not v4 in Ug and

                   A186: R is_shortestpath_of (v1,v4,Ug,W);

                  

                   A187: v4 in VG;

                  then

                  reconsider j4 = v4 as Element of NAT ;

                  

                   A188: 1 <= j4 by A16, A187, FINSEQ_1: 1;

                  j4 <= n by A16, A187, FINSEQ_1: 1;

                  then (g . (n + j4)) <> ( - 1) by A1, A2, A7, A9, A17, A185, A186, A188, Lm19;

                  then

                  consider rn be FinSequence of NAT , RR be oriented Chain of G such that rn is_simple_vertex_seq_at (g,j4,n) and for i st 1 <= i & i < ( len rn) holds (rn . i) in Ug and RR is_oriented_edge_seq_of rn and

                   A189: RR is_shortestpath_of (v1,v4,Ug,W) and ( cost (RR,W)) = (g . ((2 * n) + j4)) and

                   A190: not v4 in Ug implies RR islongestInShortestpath (Ug,v1,W) by A2, A7, A8, A185;

                  consider PP be oriented Chain of G such that

                   A191: PP is_shortestpath_of (v1,v2,Ug,W) and

                   A192: ( cost (PP,W)) <= ( cost (RR,W)) by A179, A181, A185, A190, GRAPH_5:def 19;

                  ( cost (PP,W)) = ( cost (P,W)) by A182, A191, Th9;

                  hence ( cost (P,W)) <= ( cost (R,W)) by A186, A189, A192, Th9;

                end;

                take P;

                thus P is_shortestpath_of (v1,v2,Uh,W) by A17, A24, A179, A182, A184, GRAPH_5: 64;

                thus ( cost (P,W)) <= ( cost (Q,W)) by A177, A183, XXREAL_0: 2;

              end;

            end;

            hence Q islongestInShortestpath (Uh,v1,W) by GRAPH_5:def 19;

          end;

        end;

      end;

      hereby

        let m, j;

        assume that

         A193: (h . (n + j)) = ( - 1) and

         A194: 1 <= j and

         A195: j <= n and

         A196: m in Uh;

        set nj = (n + j);

        

         A197: 1 < nj by A194, A195, Lm12;

        

         A198: nj <= (2 * n) by A194, A195, Lm12;

        

         A199: nj < mi by A194, A195, Lm12;

        then

         A200: nj in ( dom g) by A12, A19, A197, FINSEQ_3: 25;

        (n + 1) <= nj by A194, XREAL_1: 7;

        then

         A201: n < nj by NAT_1: 13;

        

         A202: (M . g) hasBetterPathAt (n,(nj -' n)) implies contradiction by A193, A14, A15, A42, A198, A200, A201, Def14;

        

         A203: ((M . g) . nj) = (g . nj) by A13, A21, A199, A201, Th18;

        then

         A204: (g . nj) = ( - 1) by A14, A15, A193, A198, A200, A201, A202, Def14;

        then

         A205: not j in Ug by A10;

        j < mi by A25, A195, XXREAL_0: 2;

        then j in ( dom g) by A12, A19, A194, FINSEQ_3: 25;

        then (g . j) <> ( - 1) by A194, A195, A205;

        then

         A206: ((M . g) . j) <> ( - 1) by A13, A22, A25, A195, A204, Th18;

         not (M . g) hasBetterPathAt (n,j) by A202, NAT_D: 34;

        then

         A207: ((M . g) /. (((2 * n) + (n * ((M . g) /. mi))) + j)) < 0 by A203, A204, A206;

        reconsider v3 = j as Vertex of G by A16, A194, A195, FINSEQ_1: 1;

        set Akj = (((2 * n) + (n * Ak)) + j);

        

         A208: 1 < Akj by A20, A21, A195, Lm13;

        

         A209: Ak < Akj by A20, A21, A195, Lm13;

        

         A210: Akj < mi by A20, A21, A195, Lm13;

        then

         A211: Akj in ( dom g) by A12, A19, A208, FINSEQ_3: 25;

        

         A212: ((3 * n) + 1) <= Akj by A20, A21, A194, A195, Lm14;

        

         A213: Akj <= ((n * n) + (3 * n)) by A20, A21, A194, A195, Lm14;

        

         A214: (f . Akj) = ( Weight (vk,v3,W)) by A1;

        

         A215: ((M . g) /. (((2 * n) + (n * ((M . g) /. mi))) + j)) = ((M . g) . Akj) by A14, A42, A211, PARTFUN1:def 6

        .= (g . Akj) by A13, A209, A210, Th18

        .= ( Weight (vk,v3,W)) by A38, A211, A212, A213, A214;

        per cases by A23, A196, XBOOLE_0:def 3;

          suppose m in {Ak};

          then

           A216: m = Ak by TARSKI:def 1;

           not ex e be set st e in the carrier' of G & e orientedly_joins (vk,v3) by A207, A215, Th23;

          then ( Weight (vk,v3,W)) = ( - 1) by Def7;

          hence (f . (((2 * n) + (n * m)) + j)) = ( - 1) by A1, A216;

        end;

          suppose m in Ug;

          hence (f . (((2 * n) + (n * m)) + j)) = ( - 1) by A9, A194, A195, A204;

        end;

      end;

      let m;

      assume

       A217: m in Uh;

      per cases by A23, A217, XBOOLE_0:def 3;

        suppose

         A218: m in Ug;

        then (h . (n + m)) = (g . (n + m)) by A4, A5, A6, A12, Lm16;

        hence thesis by A10, A218;

      end;

        suppose m in {Ak};

        hence thesis by A22, A52, TARSKI:def 1;

      end;

    end;

    theorem :: GRAPHSP:52

    f is_Input_of_Dijkstra_Alg (G,n,W) & v1 = 1 & 1 <> v2 & v2 = i & n >= 1 & g = (( DijkstraAlgorithm n) . f) implies the carrier of G = (( UsedVx (g,n)) \/ ( UnusedVx (g,n))) & (v2 in ( UsedVx (g,n)) implies ex p, P st p is_simple_vertex_seq_at (g,i,n) & P is_oriented_edge_seq_of p & P is_shortestpath_of (v1,v2,W) & ( cost (P,W)) = (g . ((2 * n) + i))) & (v2 in ( UnusedVx (g,n)) implies not ex Q st Q is_orientedpath_of (v1,v2))

    proof

      assume that

       A1: f is_Input_of_Dijkstra_Alg (G,n,W) and

       A2: v1 = 1 and

       A3: 1 <> v2 and

       A4: v2 = i and

       A5: n >= 1 and

       A6: g = (( DijkstraAlgorithm n) . f);

      

       A7: ( Seg n) = the carrier of G by A1;

      then

      reconsider VG = the carrier of G as non empty Subset of NAT by A5;

      

       A8: (f . (n + 1)) = 0 by A1;

      set Ug = ( UsedVx (g,n)), Vg = ( UnusedVx (g,n));

      set R = ( Relax n), M = ( findmin n), RM = ( repeat (R * M)), cn = ( LifeSpan ((R * M),f,n)), mi = (((n * n) + (3 * n)) + 1);

      

       A9: g = ((RM . cn) . f) by A6, Def5;

      

       A10: (Ug \/ Vg) c= VG

      proof

        let x be object;

        assume

         A11: x in (Ug \/ Vg);

        per cases by A11, XBOOLE_0:def 3;

          suppose x in Ug;

          then ex k st x = k & k in ( dom g) & 1 <= k & k <= n & (g . k) = ( - 1);

          hence thesis by A7, FINSEQ_1: 1;

        end;

          suppose x in Vg;

          then ex k st x = k & k in ( dom g) & 1 <= k & k <= n & (g . k) <> ( - 1);

          hence thesis by A7, FINSEQ_1: 1;

        end;

      end;

      

       A12: ( len f) = mi by A1;

      VG c= (Ug \/ Vg)

      proof

        let x be object;

        assume

         A13: x in VG;

        then

        reconsider j = x as Element of NAT ;

        

         A14: 1 <= j by A7, A13, FINSEQ_1: 1;

        

         A15: j <= n by A7, A13, FINSEQ_1: 1;

        n < mi by Lm7;

        then j < mi by A15, XXREAL_0: 2;

        then j in ( dom f) by A12, A14, FINSEQ_3: 25;

        then

         A16: j in ( dom g) by A9, Th41;

        per cases ;

          suppose (g . j) = ( - 1);

          then j in { k : k in ( dom g) & 1 <= k & k <= n & (g . k) = ( - 1) } by A14, A15, A16;

          hence thesis by XBOOLE_0:def 3;

        end;

          suppose (g . j) <> ( - 1);

          then j in { k : k in ( dom g) & 1 <= k & k <= n & (g . k) <> ( - 1) } by A14, A15, A16;

          hence thesis by XBOOLE_0:def 3;

        end;

      end;

      hence

       A17: the carrier of G = (Ug \/ Vg) by A10, XBOOLE_0:def 10;

      defpred P[ Nat] means $1 <= cn implies (for v3, j st v3 <> v1 & v3 = j & (((RM . $1) . f) . (n + j)) <> ( - 1) holds ex p, P st p is_simple_vertex_seq_at (((RM . $1) . f),j,n) & (for m st 1 <= m & m < ( len p) holds (p . m) in ( UsedVx (((RM . $1) . f),n))) & P is_oriented_edge_seq_of p & P is_shortestpath_of (v1,v3,( UsedVx (((RM . $1) . f),n)),W) & ( cost (P,W)) = (((RM . $1) . f) . ((2 * n) + j)) & ( not v3 in ( UsedVx (((RM . $1) . f),n)) implies P islongestInShortestpath (( UsedVx (((RM . $1) . f),n)),v1,W))) & (for m, j st (((RM . $1) . f) . (n + j)) = ( - 1) & 1 <= j & j <= n & m in ( UsedVx (((RM . $1) . f),n)) holds (f . (((2 * n) + (n * m)) + j)) = ( - 1)) & (for m st m in ( UsedVx (((RM . $1) . f),n)) holds (((RM . $1) . f) . (n + m)) <> ( - 1));

      1 <= mi by NAT_1: 12;

      then

       A18: 1 in ( dom f) by A12, FINSEQ_3: 25;

      

       A19: (for m st 1 <= m & m <= n holds (f . m) = 1) & for m st 2 <= m & m <= n holds (f . (n + m)) = ( - 1) by A1;

      then {1} = ( UsedVx (((RM . 1) . f),n)) by A5, A8, A18, Th47;

      then

       A20: 1 in ( UsedVx (((RM . 1) . f),n)) by TARSKI:def 1;

      

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

      proof

        let k;

        assume

         A22: P[k];

        now

          set FK1 = ((RM . (k + 1)) . f), UV1 = ( UsedVx (FK1,n));

          set FK = ((RM . k) . f);

          assume

           A23: (k + 1) <= cn;

          then

           A24: k < cn by NAT_1: 13;

          then

           A25: ( OuterVx (FK,n)) <> {} by Def4;

          per cases ;

            suppose k = 0 ;

            hence (for v3, j st v3 <> v1 & v3 = j & (FK1 . (n + j)) <> ( - 1) holds ex p, P st p is_simple_vertex_seq_at (FK1,j,n) & (for m st 1 <= m & m < ( len p) holds (p . m) in UV1) & P is_oriented_edge_seq_of p & P is_shortestpath_of (v1,v3,UV1,W) & ( cost (P,W)) = (FK1 . ((2 * n) + j)) & ( not v3 in UV1 implies P islongestInShortestpath (UV1,v1,W))) & (for m, j st (FK1 . (n + j)) = ( - 1) & 1 <= j & j <= n & m in UV1 holds (f . (((2 * n) + (n * m)) + j)) = ( - 1)) & for m st m in UV1 holds (FK1 . (n + m)) <> ( - 1) by A1, A2, A5, Lm15;

          end;

            suppose k <> 0 ;

            then k >= (1 + 0 ) by INT_1: 7;

            then 1 in ( UsedVx (FK,n)) by A20, A24, Th48;

            hence (for v3, j st v3 <> v1 & v3 = j & (FK1 . (n + j)) <> ( - 1) holds ex p, P st p is_simple_vertex_seq_at (FK1,j,n) & (for m st 1 <= m & m < ( len p) holds (p . m) in UV1) & P is_oriented_edge_seq_of p & P is_shortestpath_of (v1,v3,UV1,W) & ( cost (P,W)) = (FK1 . ((2 * n) + j)) & ( not v3 in UV1 implies P islongestInShortestpath (UV1,v1,W))) & (for m, j st (FK1 . (n + j)) = ( - 1) & 1 <= j & j <= n & m in UV1 holds (f . (((2 * n) + (n * m)) + j)) = ( - 1)) & for m st m in UV1 holds (FK1 . (n + m)) <> ( - 1) by A1, A2, A5, A22, A23, A25, Lm20, NAT_1: 13;

          end;

        end;

        hence thesis;

      end;

      

       A26: ((RM . 0 ) . f) = f by Th21;

      

       A27: P[ 0 ]

      proof

        set UV = ( UsedVx (((RM . 0 ) . f),n)), h = ((RM . 0 ) . f);

        assume 0 <= cn;

        hereby

          let v3, j;

          assume that

           A28: v3 <> v1 and

           A29: v3 = j and

           A30: (h . (n + j)) <> ( - 1);

          

           A31: v3 in VG;

          then 1 <= j by A7, A29, FINSEQ_1: 1;

          then 1 < j by A2, A28, A29, XXREAL_0: 1;

          then

           A32: (1 + 1) <= j by INT_1: 7;

          assume not (ex p, P st p is_simple_vertex_seq_at (h,j,n) & (for m st 1 <= m & m < ( len p) holds (p . m) in UV) & P is_oriented_edge_seq_of p & P is_shortestpath_of (v1,v3,UV,W) & ( cost (P,W)) = (h . ((2 * n) + j)) & ( not v3 in UV implies P islongestInShortestpath (UV,v1,W)));

          j <= n by A7, A29, A31, FINSEQ_1: 1;

          hence contradiction by A1, A26, A30, A32;

        end;

        thus for m, j st (h . (n + j)) = ( - 1) & 1 <= j & j <= n & m in UV & not (f . (((2 * n) + (n * m)) + j)) = ( - 1) holds contradiction by A5, A26, A8, A19, A18, Th47;

        let m;

        assume

         A33: m in ( UsedVx (h,n));

        assume (h . (n + m)) = ( - 1);

        thus contradiction by A5, A26, A8, A19, A18, A33, Th47;

      end;

      

       A34: for k holds P[k] from NAT_1:sch 2( A27, A21);

      ex ii be Nat st ii <= n & ( OuterVx (((RM . ii) . f),n)) = {} by Th40;

      then

       A35: ( OuterVx (g,n)) = {} by A9, Def4;

       A36:

      now

        let v3, v4;

        assume that

         A37: v3 in Ug and

         A38: v4 in Vg;

        v3 in VG;

        then

        reconsider m = v3 as Element of NAT ;

        consider j such that

         A39: v4 = j and

         A40: j in ( dom g) and

         A41: 1 <= j & j <= n and

         A42: (g . j) <> ( - 1) by A38;

        now

          assume (g . (n + j)) <> ( - 1);

          then j in { k : k in ( dom g) & 1 <= k & k <= n & (g . k) <> ( - 1) & (g . (n + k)) <> ( - 1) } by A40, A41, A42;

          hence contradiction by A35;

        end;

        

        then ( - 1) = (f . (((2 * n) + (n * m)) + j)) by A9, A34, A37, A41

        .= ( Weight (v3,v4,W)) by A1, A39;

        hence not ex e st e in the carrier' of G & e orientedly_joins (v3,v4) by Th23;

      end;

      

       A43: (f . 1) = 1 by A1, A5;

      now

        assume

         A44: cn = 0 ;

        1 in { k : k in ( dom f) & 1 <= k & k <= n & (f . k) <> ( - 1) & (f . (n + k)) <> ( - 1) } by A5, A43, A8, A18;

        hence contradiction by A9, A26, A35, A44;

      end;

      then cn >= (1 + 0 ) by INT_1: 7;

      then

       A45: v1 in Ug by A2, A9, A20, Th48;

      hereby

        assume v2 in Ug;

        then (g . (n + i)) <> ( - 1) by A4, A9, A34;

        then

        consider p, P such that

         A46: p is_simple_vertex_seq_at (g,i,n) and for m st 1 <= m & m < ( len p) holds (p . m) in Ug and

         A47: P is_oriented_edge_seq_of p and

         A48: P is_shortestpath_of (v1,v2,Ug,W) and

         A49: ( cost (P,W)) = (g . ((2 * n) + i)) and not v2 in Ug implies P islongestInShortestpath (Ug,v1,W) by A2, A3, A4, A9, A34;

        take p, P;

        thus p is_simple_vertex_seq_at (g,i,n) by A46;

        thus P is_oriented_edge_seq_of p by A47;

        thus P is_shortestpath_of (v1,v2,W) by A17, A36, A45, A48, Th16;

        thus ( cost (P,W)) = (g . ((2 * n) + i)) by A49;

      end;

      thus thesis by A17, A36, A45, Th11;

    end;