The Mizar article:

Dijkstra's Shortest Path Algorithm

by
Jing-Chao Chen

Received March 17, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: GRAPHSP
[ MML identifier index ]


environ

 vocabulary ARYTM_1, INT_1, RELAT_1, SCM_1, RLVECT_1, AMI_3, GRAPHSP, FUNCT_1,
      BOOLE, FINSET_1, ORDERS_1, FINSEQ_1, CARD_1, FUNCT_2, GRAPH_1, FINSEQ_4,
      GRAPH_5, GRAPH_4, MSAFREE2, FUNCT_4;
 notation XREAL_0, REAL_1, NAT_1, INT_1, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1,
      FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_4, CARD_1, FINSET_1, GRAPH_1,
      PARTFUN1, FUNCT_2, GRAPH_4, GRAPH_3, GRAPH_5, BINARITH, DOMAIN_1,
      RVSUM_1, GOBOARD1, NUMBERS, FUNCT_7;
 constructors REAL_1, INT_1, FINSEQ_4, GRAPH_5, GRAPH_4, DOMAIN_1, BINARITH,
      GOBOARD1, FUNCT_7, MEMBERED, RELAT_2;
 clusters FRAENKEL, INT_1, GRAPH_5, FINSEQ_1, FINSET_1, RELSET_1, GRAPH_1,
      FUNCT_2, GRAPH_4, XREAL_0, MEMBERED, PARTFUN1, NUMBERS, ORDINAL2;
 requirements NUMERALS, SUBSET, BOOLE, REAL, ARITHM;
 definitions TARSKI;
 theorems FUNCT_2, AXIOMS, FUNCT_1, PARTFUN1, FINSEQ_1, NAT_1, FINSET_1,
      ZFMISC_1, TARSKI, REAL_1, FINSEQ_3, XBOOLE_0, XBOOLE_1, SUBSET_1,
      GRAPH_1, FINSEQ_4, CARD_1, CARD_2, INT_1, GRAPH_5, GRAPH_4, FINSEQ_2,
      ENUMSET1, BINARITH, RVSUM_1, SCMFSA_7, FUNCT_7, XCMPLX_1;
 schemes FUNCT_1, RECDEF_1, NAT_1, GRAPH_5;

begin  :: Preliminaries

reserve x,y,X for set,
        i,j,k,m,n for Nat,
        p for FinSequence of X,
        ii for Integer;

theorem Th1:
 for p being FinSequence,x being 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 p misses rng <*x*> & p is one-to-one & <*x*> is one-to-one
    iff p ^ <*x*> is one-to-one by FINSEQ_3:98;
      rng <*x*> = {x} by FINSEQ_1:55;
    hence thesis by A1,FINSEQ_3:102,ZFMISC_1:54,56;
end;

theorem Th2:
  1 <= ii & ii <= len p implies p.ii in X
proof assume A1:1 <= ii & ii <= len p;
  then 0 <= ii by AXIOMS:22;
  then reconsider ii as Nat by INT_1:16;
    ii in dom p by A1,FINSEQ_3:27;
  hence thesis by PARTFUN1:27;
end;

theorem Th3:
  1 <= ii & ii <= len p implies p/.ii = p.ii
proof assume A1:1 <= ii & ii <= len p;
  then 0 <= ii by AXIOMS:22;
  then reconsider ii as Nat by INT_1:16;
    ii in dom p by A1,FINSEQ_3:27;
  hence thesis by FINSEQ_4:def 4;
end;

reserve G for Graph,
        pe,qe for FinSequence of the Edges 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 Th4:
  W is_weight_of G & len pe = 1 implies cost(pe,W) = W.(pe.1)
proof
     assume A1: W is_weight_of G & len pe = 1;
     set f=RealSequence(pe,W);
A2:  dom f = dom pe & for i st i in dom pe holds f.i=W.(pe.i)
     by A1,GRAPH_5:def 15;
A3:  1 in dom pe by A1,FINSEQ_3:27;
       len f=1 by A1,A2,FINSEQ_3:31;
then A4:  f = <*f.1*> by FINSEQ_1:57;
     thus cost(pe,W) = Sum f by GRAPH_5:def 16
     .= f.1 by A4,RVSUM_1:103
     .= W.(pe.1) by A1,A3,GRAPH_5:def 15;
end;

theorem Th5:
  e in the Edges of G implies <*e*> is Simple (oriented Chain of G)
proof
   assume e in the Edges of G;
then A1:  <*e*> is FinSequence of the Edges of G by SCMFSA_7:22;
     len <*e*> = 1 by FINSEQ_1:57;
   hence thesis by A1,GRAPH_5:18;
end;

Lm1:
 for p,q being FinSequence st 1 <= n & n <= len p holds p.n = (p^q).n
proof
  let p,q be FinSequence;
  assume 1 <= n & n <= len p;
  then n in dom p by FINSEQ_3:27;
  hence p.n = (p^q).n by FINSEQ_1:def 7;
end;

Lm2:
for p,q being 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:27;
  hence thesis by FINSEQ_1:def 7;
end;

theorem Th6:
 for p being 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 A1: p=pe^qe & len pe >= 1 & len qe >= 1;
     consider vs being FinSequence of the Vertices of G such that
A2:  vs is_oriented_vertex_seq_of p &
     (for n,m st 1<=n & n<m & m<=len vs & vs.n=vs.m holds n=1 & m=len vs)
     by GRAPH_4:def 7;
A3:  len vs = len p + 1 &
     for n st 1<=n & n<=len p holds p.n orientedly_joins vs/.n, vs/.(n+1)
     by A2,GRAPH_4:def 5;
       len p = len pe + len qe by A1,FINSEQ_1:35;
then A4:  len p >= len pe+1 by A1,REAL_1:55;
then A5:  len p > len pe by NAT_1:38;
then A6:  len p >= 1 by A1,AXIOMS:22;
A7:  1 <= len vs by A3,NAT_1:37;
       p.len p orientedly_joins vs/.len p, vs/.(len p+1) by A2,A6,GRAPH_4:def 5
;
then A8:  FT.(p.len p)=vs/.(len p+1) by GRAPH_4:def 1
         .=vs.len vs by A3,A7,FINSEQ_4:24;
A9:  1 < len pe +1 by A1,NAT_1:38;
A10:  len pe+1 < len vs by A3,A4,NAT_1:38;
A11:  p.len pe orientedly_joins vs/.len pe, vs/.(len pe+1) by A1,A2,A5,GRAPH_4:
def 5;
   FT.(pe.len pe) = FT.(p.len pe) by A1,Lm1
     .=vs/.(len pe+1) by A11,GRAPH_4:def 1
     .=vs.(len pe +1) by A9,A10,FINSEQ_4:24;
     hence FT.(p.len p) <> FT.(pe.len pe) by A2,A8,A9,A10;
       p.1 orientedly_joins vs/.1, vs/.(1+1) by A2,A6,GRAPH_4:def 5;
then A12:  FS.(p.1)=vs/.1 by GRAPH_4:def 1
         .=vs.1 by A7,FINSEQ_4:24;
A13:  p.(len pe+1) orientedly_joins vs/.(len pe+1), vs/.(len pe+1+1)
      by A2,A4,A9,GRAPH_4:def 5;
A14:  FS.(qe.1) = FS.(p.(len pe+1)) by A1,Lm2
     .=vs/.(len pe+1) by A13,GRAPH_4:def 1
     .=vs.(len pe +1) by A9,A10,FINSEQ_4:24;
     assume FS.(p.1) = FS.(qe.1);
     hence contradiction by A2,A9,A10,A12,A14;
end;

begin :: The fundamental properties of directed paths and shortest paths

theorem Th7:
  p is_orientedpath_of v1,v2,V iff p is_orientedpath_of v1,v2,V \/ {v2}
proof
    set V'=V \/ {v2};
  V c= V' by XBOOLE_1:7;
    hence p is_orientedpath_of v1,v2,V implies
       p is_orientedpath_of v1,v2,V' by GRAPH_5:36;
    assume p is_orientedpath_of v1,v2,V';
then A1:  p is_orientedpath_of v1,v2 & vertices(p) \ {v2} c= V' by GRAPH_5:def
4;
     then vertices(p) \ {v2} \ {v2} c= V by XBOOLE_1:43;
     then vertices(p) \ ({v2} \/ {v2}) c= V by XBOOLE_1:41;
     hence thesis by A1,GRAPH_5:def 4;
end;

theorem Th8:
 p is_shortestpath_of v1,v2,V,W iff p is_shortestpath_of v1,v2,V \/{v2},W
proof
    set V'=V \/ {v2};
    hereby assume A1: p is_shortestpath_of v1,v2,V,W;
   then p is_orientedpath_of v1,v2,V & for q st q is_orientedpath_of v1,v2,V
       holds cost(p,W) <= cost(q,W) by GRAPH_5:def 18;
    then A2: p is_orientedpath_of v1,v2,V' by Th7;
         now let q;
          assume q is_orientedpath_of v1,v2,V';
          then q is_orientedpath_of v1,v2,V by Th7;
          hence cost(p,W) <= cost(q,W) by A1,GRAPH_5:def 18;
        end;
        hence p is_shortestpath_of v1,v2,V',W by A2,GRAPH_5:def 18;
    end;
    assume A3:p is_shortestpath_of v1,v2,V',W;
then p is_orientedpath_of v1,v2,V' & for q st q is_orientedpath_of v1,v2,V'
    holds cost(p,W) <= cost(q,W) by GRAPH_5:def 18;
then A4: p is_orientedpath_of v1,v2,V by Th7;
      now let q;
       assume q is_orientedpath_of v1,v2,V;
       then q is_orientedpath_of v1,v2,V' by Th7;
       hence cost(p,W) <= cost(q,W) by A3,GRAPH_5:def 18;
    end;
    hence thesis by A4,GRAPH_5:def 18;
end;

theorem 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 A1: p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W;
then A2: p is_orientedpath_of v1,v2,V & for r being oriented Chain of G
    st r is_orientedpath_of v1,v2,V holds cost(p,W) <= cost(r,W)
    by GRAPH_5:def 18;
  q is_orientedpath_of v1,v2,V & for r being oriented Chain of G
    st r is_orientedpath_of v1,v2,V holds cost(q,W) <= cost(r,W)
    by A1,GRAPH_5:def 18;
then A3: cost(p,W) <= cost(q,W) by A1,GRAPH_5:def 18;
      cost(q,W) <= cost(p,W) by A1,A2,GRAPH_5:def 18;
    hence thesis by A3,AXIOMS:21;
end;

theorem Th10:
for G being oriented Graph,v1,v2 be Vertex of G,e1,e2 be set
st e1 in the Edges of G & e2 in the Edges 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 A1: e1 in the Edges of G & e2 in the Edges of G &
  e1 orientedly_joins v1,v2 & e2 orientedly_joins v1,v2;
  then (the Source of G).e1 = v1 & (the Target of G).e1 = v2 &
  (the Source of G).e2 = v1 & (the Target of G).e2 = v2 by GRAPH_4:def 1;
  hence thesis by A1,GRAPH_1:def 4;
end;

Lm3:
 1 <= i & i <= len pe implies (the Source of G).(pe.i) in the Vertices of G
   & (the Target of G).(pe.i) in the Vertices of G
proof
   assume 1 <= i & i <= len pe;
   then i in dom pe by FINSEQ_3:27;
   hence thesis by GRAPH_5:11;
end;

theorem Th11:
the Vertices 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 Edges of G & e orientedly_joins v3,v4))
 implies not ex p st p is_orientedpath_of v1,v2
proof
    assume A1: the Vertices 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 Edges of G &
     e orientedly_joins v3,v4));
    given p such that
A2: p is_orientedpath_of v1,v2;
    set FS=the Source of G,
        FT=the Target of G;
A3: p <> {} & FS.(p.1) = v1 & FT.(p.(len p))= v2 by A2,GRAPH_5:def 3;
then A4: len p >= 1 by GRAPH_5:8;
    defpred PP[Nat] means $1 >=1 & $1<=len p & FS.(p.$1) in U;
A5: for k st PP[k] holds k <= len p;
A6: ex k st PP[k] by A1,A3,A4;
    consider k such that
A7: PP[k] & for n st PP[n] holds n <= k from Max(A5,A6);
    reconsider vx=FS.(p.k) as Vertex of G by A7,Lm3;
A8: p.k in the Edges of G by A7,Th2;
    per cases;
    suppose k=len p;
        then p.k orientedly_joins vx,v2 by A3,GRAPH_4:def 1;
        hence contradiction by A1,A7,A8;
    suppose k<>len p;
    then A9: k < len p by A7,REAL_1:def 5;
    then A10: FS.(p.(k+1)) = FT.(p.k) by A7,GRAPH_1:def 12;
    A11: k < k+1 by NAT_1:38;
        A12: now assume A13: FS.(p.(k+1)) in U;
       A14:  k+1 <= len p by A9,INT_1:20;
              1 <= k+1 by NAT_1:37;
            hence contradiction by A7,A11,A13,A14;
        end;
    A15: FT.(p.k) in the Vertices of G by A7,Lm3;
        reconsider vy=FT.(p.k) as Vertex of G by A7,Lm3;
    A16: vy in V by A1,A10,A12,A15,XBOOLE_0:def 2;
          p.k orientedly_joins vx,vy by GRAPH_4:def 1;
        hence contradiction by A1,A7,A8,A16;
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 A1: 1<= i & i <= len pe & (v1=(the Source of G).(pe.i) or
      v1=(the Target of G).(pe.i));
   then i in dom pe by FINSEQ_3:27;
   hence thesis by A1,GRAPH_5:28;
end;

theorem Th12:
the Vertices 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 Edges of G & e orientedly_joins v3,v4)) &
p is_orientedpath_of v1,v2 implies p is_orientedpath_of v1,v2,U
proof
    assume A1: the Vertices 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 Edges of G &
     e orientedly_joins v3,v4)) & p is_orientedpath_of v1,v2;
    set FS=the Source of G,
        FT=the Target of G;
A2: vertices p \ {v2} c= vertices p by XBOOLE_1:36;
      now
      assume not vertices p c= U;
      then consider i being Nat, q,r being FinSequence of the Edges of G such
that
A3:   i+1 <= len p & not vertices(p/.(i+1)) c= U & len q=i & p=q^r &
      vertices q c= U by GRAPH_5:23;
A4:   1 <= i+ 1 by NAT_1:37;
      then p/.(i+1)=p.(i+1) by A3,FINSEQ_4:24;
then A5:   vertices(p/.(i+1))={FS.(p.(i+1)),FT.(p.(i+1))} by GRAPH_5:def 1;
A6:   now
         assume FS.(p.(i+1)) in U & FT.(p.(i+1)) in U;
         then vertices(p/.(i+1)) \/ U = U by A5,ZFMISC_1:48;
         hence contradiction by A3,XBOOLE_1:7;
      end;
A7:   p.(i+1) in the Edges of G by A3,A4,Th2;
A8:   FT.(p.(i+1)) in the Vertices of G by A3,A4,Lm3;
      reconsider vy=FT.(p.(i+1)) as Vertex of G by A3,A4,Lm3;
A9:   vy in U or vy in V by A1,A8,XBOOLE_0:def 2;
      per cases;
      suppose A10: i=0;
     then FS.(p.(i+1))=v1 by A1,GRAPH_5:def 3;
         then p.(i+1) orientedly_joins v1,vy by GRAPH_4:def 1;
        hence contradiction by A1,A6,A7,A9,A10,GRAPH_5:def 3;
      suppose A11: i<>0;
        reconsider vx=FS.(p.(i+1)) as Vertex of G by A3,A4,Lm3;
        hereby
         per cases;
         suppose A12: vx in U;
             p.(i+1) orientedly_joins vx,vy by GRAPH_4:def 1;
           hence contradiction by A1,A6,A7,A9,A12;
         suppose A13: not vx in U;
             i > 0 by A11,NAT_1:19;
    then A14:    i >= 1+0 by INT_1:20;
           then reconsider vq=FT.(q.i) as Vertex of G by A3,Lm3;
           A15: vq in vertices(q) by A3,A14,Lm4;
    A16:    i < len p by A3,NAT_1:38;
             FT.(q.i)=FT.(p.i) by A3,A14,Lm1
           .=FS.(p.(i+1)) by A14,A16,GRAPH_1:def 12;
           hence contradiction by A3,A13,A15;
        end;
    end;
    then vertices(p) \ {v2} c= U by A2,XBOOLE_1:1;
    hence thesis by A1,GRAPH_5:def 4;
end;

begin :: The basic theorems for Dijkstra's shortest path algorithm (continue)

reserve G for finite Graph,
        P,Q for oriented Chain of G,
        v1,v2,v3 for Vertex of G;

theorem 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 Edges of G &
e orientedly_joins v2,v3) & P islongestInShortestpath V,v1,W implies
Q is_shortestpath_of v1,v3,V \/{v2},W
proof
     assume A1: 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 Edges of G & e orientedly_joins v2,v3) &
         P islongestInShortestpath V,v1,W;
       set V'=V \/ {v2},
           FS=the Source of G,
           FT=the Target of G;
A2:  W is_weight_of G by A1,GRAPH_5:50;
A3:  now
         let S be oriented Chain of G;
         assume A4: S is_orientedpath_of v1,v3,V';
          then consider s being Simple (oriented Chain of G) such that
      A5: s is_shortestpath_of v1,v3,V',W by A1,GRAPH_5:66;
      A6: s is_orientedpath_of v1,v3,V' by A5,GRAPH_5:def 18;
      then A7: s is_orientedpath_of v1,v3 by GRAPH_5:def 4;
          then s <> {} by GRAPH_5:def 3;
      then len s >=1 by GRAPH_5:8;
          then consider i such that
      A8: len s = 1+i by NAT_1:28;
          consider s1,s2 being FinSequence such that
      A9: len s1 = i & len s2 = 1 & s = s1^s2 by A8,FINSEQ_2:25;
          reconsider s1,s2 as Simple (oriented Chain of G) by A9,GRAPH_5:17;
      A10:  s2.1= s.len s by A8,A9,Lm2;
      A11:  FS.(s.1)=v1 & FT.(s.len s)=v3 by A7,GRAPH_5:def 3;
           reconsider vx=FS.(s2.1) as Vertex of G by A9,Lm3;
      A12:  now
              assume vx=v2;
          then A13:  s2.1 orientedly_joins v2,v3 by A10,A11,GRAPH_4:def 1;
                 1 in dom s2 by A9,FINSEQ_3:27;
               then s2.1 in the Edges of G by FINSEQ_2:13;
               hence contradiction by A1,A13;
           end;
      A14:  vertices(s) \ {v3} c= V' by A6,GRAPH_5:def 4;
      A15:  cost(s,W) <= cost(S,W) by A4,A5,GRAPH_5:def 18;
           per cases;
           suppose A16: not v2 in vertices s or v2=v3;
              set Vs=vertices s;
                (Vs \ {v3}) \ {v2} c= V by A14,XBOOLE_1:43;
         then A17:  Vs \ ({v3} \/ {v2}) c= V by XBOOLE_1:41;
                now
                per cases by A16;
                suppose A18: not v2 in vertices s;
                  (Vs \ {v2}) \ {v3} c= V by A17,XBOOLE_1:41;
                hence Vs \ {v3} c= V by A18,ZFMISC_1:65;
               suppose v2=v3;
                hence Vs \ {v3} c= V by A17;
              end;
              then s is_orientedpath_of v1,v3,V by A7,GRAPH_5:def 4;
              then cost(Q,W) <= cost(s,W) by A1,GRAPH_5:def 18;
              hence cost(Q,W) <= cost(S,W) by A15,AXIOMS:22;

           suppose A19: v2 in vertices s & v2<>v3;
              then consider j such that
          A20: 1<=j & j <= len s & v2 = FT.(s.j) by A1,A11,GRAPH_5:32;
                len s1 <> 0 by A8,A9,A11,A19,A20,AXIOMS:21;
              then len s1 > 0 by NAT_1:19;
          then A21: len s1 >= 0+1 by INT_1:20;
          A22: len s1 < len s by A8,A9,NAT_1:38;
          A23: vx=FS.(s.(len s1+1)) by A9,Lm2
              .=FT.(s.len s1) by A21,A22,GRAPH_1:def 12;
          A24: now
                assume j > len s1;
                then j >= len s1+1 by INT_1:20;
                hence contradiction by A8,A9,A11,A19,A20,AXIOMS:21;
              end;
              then consider k such that
         A25:  len s1 = j+k by NAT_1:28;
              consider t1,t2 being FinSequence such that
         A26:  len t1 = j & len t2 = k & s1 = t1^t2 by A25,FINSEQ_2:25;
          reconsider t1,t2 as Simple (oriented Chain of G) by A26,GRAPH_5:17;
         A27:  FS.(t1.1)=FS.(s1.1) by A20,A26,Lm1
              .=v1 by A9,A11,A21,Lm1;
         A28:  t1 <> {} by A20,A26,GRAPH_5:8;
                FT.(t1.len t1)=FT.(s1.j) by A20,A26,Lm1
              .=v2 by A9,A20,A24,Lm1;
         then A29:  t1 is_orientedpath_of v1,v2 by A27,A28,GRAPH_5:def 3;
              A30: len s2>=1 by A9;
         then A31:  not v3 in vertices (s1) by A1,A9,A11,A21,GRAPH_5:21;
              set Vt=vertices(t1);
                Vt c= vertices (t1^t2) by GRAPH_5:30;
         then A32:  not v3 in Vt by A1,A9,A11,A21,A26,A30,GRAPH_5:21;
                vertices(s1^s2) \ {v3} c= V' by A6,A9,GRAPH_5:def 4;
         then A33:  vertices(t1^t2) \ {v3} c= V' by A26,GRAPH_5:26;
              then Vt \ {v3} c= V' by GRAPH_5:26;
              then Vt c= V' by A32,ZFMISC_1:65;
              then Vt \ {v2} c= V by XBOOLE_1:43;
              then t1 is_orientedpath_of v1,v2,V by A29,GRAPH_5:def 4;
         then A34:  cost(P,W) <= cost(t1,W) by A1,GRAPH_5:def 18;
                vx = FT.(s1.len s1) by A9,A21,A23,Lm1;
         then A35:  vx in vertices(s1) by A21,Lm4;
                not vx in {v2} by A12,TARSKI:def 1;
         then A36:  vx in (vertices(s1) \ {v2}) by A35,XBOOLE_0:def 4;
                vertices(s1) c= V' by A26,A31,A33,ZFMISC_1:65;
              then A37: vertices(s1) \ {v2} c= V by XBOOLE_1:43;
                not v1 in vertices (s2) by A1,A9,A11,A21,GRAPH_5:21;
              then vx <> v1 by A9,Lm4;
              then consider q being oriented Chain of G such that
        A38:   q is_shortestpath_of v1,vx,V,W & cost(q,W) <= cost(P,W)
              by A1,A36,A37,GRAPH_5:def 19;
        A39:   q is_orientedpath_of v1,vx,V by A38,GRAPH_5:def 18;
        A40:   s2.1 orientedly_joins vx,v3 by A10,A11,GRAPH_4:def 1;
        A41:   q is_orientedpath_of v1,vx by A39,GRAPH_5:def 4;
              then q <> {} by GRAPH_5:def 3;
        then A42:   len q >=1 by GRAPH_5:8;
              then consider p being oriented Chain of G such that
        A43:   p=q^s2 & p is_orientedpath_of v1,v3 by A9,A40,A41,GRAPH_5:37;
                p is_orientedpath_of v1,v3,V \/{vx}
              by A9,A39,A40,A42,A43,GRAPH_5:38;
              then p is_orientedpath_of v1,v3,V by A36,A37,ZFMISC_1:46;
              then cost(Q,W) <= cost(p,W) by A1,GRAPH_5:def 18;
        then A44:   cost(Q,W) <= cost(q,W)+cost(s2,W) by A2,A43,GRAPH_5:58;
        A45:   cost(q,W) <= cost(t1,W) by A34,A38,AXIOMS:22;
        A46:   cost(s1,W) = cost(t1,W)+cost(t2,W) by A2,A26,GRAPH_5:58;
                0 <= cost(t2,W) by A1,GRAPH_5:54;
              then 0+cost(t1,W) <= cost(s1,W) by A46,REAL_1:55;
        then A47:   cost(q,W) <= cost(s1,W) by A45,AXIOMS:22;
                cost(s,W) = cost(s1,W)+cost(s2,W) by A2,A9,GRAPH_5:58;
              then cost(q,W)+cost(s2,W) <= cost(s,W) by A47,REAL_1:55;
              then cost(Q,W) <= cost(s,W) by A44,AXIOMS:22;
              hence cost(Q,W) <= cost(S,W) by A15,AXIOMS:22;
     end;
A48:  Q is_orientedpath_of v1,v3,V by A1,GRAPH_5:def 18;
       V c= V' by XBOOLE_1:7;
     then Q is_orientedpath_of v1,v3,V' by A48,GRAPH_5:36;
     hence thesis by A3,GRAPH_5:def 18;
end;

reserve G for finite oriented Graph,
        P,Q for oriented Chain of G,
        W for Function of (the Edges of G), Real>=0,
        v1,v2,v3,v4 for Vertex of G;

theorem Th14:
e in the Edges of G & v1 <> v2 & P=<*e*> & e orientedly_joins v1,v2
implies P is_shortestpath_of v1,v2,{v1},W
proof
     assume A1: e in the Edges of G & v1 <> v2 & P=<*e*> &
      e orientedly_joins v1,v2;
       set FS=the Source of G,
           FT=the Target of G,
           Eg=the Edges of G;
A2:  FS.e = v1 & FT.e = v2 by A1,GRAPH_4:def 1;
A3:  now
         let S be oriented Chain of G;
         assume A4: S is_orientedpath_of v1,v2,{v1};
            W is_weight>=0of G by GRAPH_5:def 13;
          then consider s being Simple (oriented Chain of G) such that
      A5: s is_shortestpath_of v1,v2,{v1},W by A4,GRAPH_5:66;
      A6: s is_orientedpath_of v1,v2,{v1} by A5,GRAPH_5:def 18;
      then A7: s is_orientedpath_of v1,v2 by GRAPH_5:def 4;
          then s <> {} by GRAPH_5:def 3;
      then A8: len s >=1 by GRAPH_5:8;
          set Vs=vertices s;
            Vs \ {v2} c= {v1} by A6,GRAPH_5:def 4;
          then Vs c= {v2} \/ {v1} by XBOOLE_1:44;
      then A9: Vs c= {v1,v2} by ENUMSET1:41;
      A10: FS.(s.1)=v1 & FT.(s.len s)=v2 by A7,GRAPH_5:def 3;
          then v1 in Vs & v2 in Vs by A8,Lm4;
          then {v1} c= Vs & {v2} c= Vs by ZFMISC_1:37;
          then {v1} \/ {v2} c= Vs by XBOOLE_1:8;
          then A11: {v1,v2} c= Vs by ENUMSET1:41;
          consider i such that
      A12: len s = 1+i by A8,NAT_1:28;
          consider s1,s2 being FinSequence such that
      A13: len s1 = i & len s2 = 1 & s = s1^s2 by A12,FINSEQ_2:25;
          reconsider s1,s2 as Simple (oriented Chain of G) by A13,GRAPH_5:17;
            now
             assume s1 <> {};
         then A14: len s1 >=1 by GRAPH_5:8;
               len s2 =1 by A13;
         then A15: FT.(s.len s) <> FT.(s1.len s1) &
             FS.(s.1) <> FS.(s2.1) by A13,A14,Th6;
         A16: len s1 < len s by A12,A13,NAT_1:38;
             A17: FS.(s2.1)=FS.(s.(len s1+1)) by A13,Lm2
           .=FT.(s.len s1) by A14,A16,GRAPH_1:def 12
           .=FT.(s1.len s1) by A13,A14,Lm1;
               vertices(s2) c= vertices(s1^s2) by GRAPH_5:30;
         then A18: vertices(s2) c= {v1,v2} by A9,A11,A13,XBOOLE_0:def 10;
             reconsider vx=FS.(s2.1) as Vertex of G by A13,Lm3;
               vx in vertices(s2) by A13,Lm4;
             hence contradiction by A10,A15,A17,A18,TARSKI:def 2;
           end;
       then A19: len s= 0+1 by A12,A13,FINSEQ_1:25;
             s/.1 in Eg by A1;
           then s.1 in Eg by A19,FINSEQ_4:24;
           then e = s.1 by A1,A2,A10,A19,GRAPH_1:def 4;
           then s = P by A1,A19,FINSEQ_1:57;
          hence cost(P,W) <= cost(S,W) by A4,A5,GRAPH_5:def 18;
     end;
A20:  len P = 1 & P.1=e by A1,FINSEQ_1:57;
     then P <> {} by GRAPH_5:8;
then A21:  P is_orientedpath_of v1,v2 by A2,A20,GRAPH_5:def 3;
A22:  P/.1=e by A20,FINSEQ_4:24;
       vertices(P)=vertices(P/.1) by A20,GRAPH_5:29;
     then vertices(P)={v1,v2} by A2,A22,GRAPH_5:def 1;
     then vertices(P) \ {v2} = ({v1} \/ {v2}) \{v2} by ENUMSET1:41
     .={v1} \ {v2} by XBOOLE_1:40;
     then vertices(P) \ {v2} c= {v1} by XBOOLE_1:36;
     then P is_orientedpath_of v1,v2,{v1} by A21,GRAPH_5:def 4;
     hence thesis by A3,GRAPH_5:def 18;
end;

theorem Th15:
e in the Edges 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 Edges of G & ee orientedly_joins v4,v3)) implies
Q is_shortestpath_of v1,v3,V \/{v2},W
proof
     assume A1: e in the Edges 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 Edges of G &
    ee orientedly_joins v4,v3));
       set V'=V \/ {v2},
           FS=the Source of G,
           FT=the Target of G;
A2:  W is_weight>=0of G by GRAPH_5:def 13;
then A3:  W is_weight_of G by GRAPH_5:50;
      set Eg=the Edges of G;
A4:  now
         let S be oriented Chain of G;
         assume A5: S is_orientedpath_of v1,v3,V';
          then consider s being Simple (oriented Chain of G) such that
      A6: s is_shortestpath_of v1,v3,V',W by A2,GRAPH_5:66;
      A7: s is_orientedpath_of v1,v3,V' by A6,GRAPH_5:def 18;
      then A8: s is_orientedpath_of v1,v3 by GRAPH_5:def 4;
          then s <> {} by GRAPH_5:def 3;
      then A9: len s >=1 by GRAPH_5:8;
          then consider i such that
      A10: len s = 1+i by NAT_1:28;
          consider s1,s2 being FinSequence such that
      A11: len s1 = i & len s2 = 1 & s = s1^s2 by A10,FINSEQ_2:25;
          reconsider s1,s2 as Simple (oriented Chain of G) by A11,GRAPH_5:17;
      A12:  s2.1= s.len s by A10,A11,Lm2;
      A13:  FS.(s.1)=v1 & FT.(s.len s)=v3 by A8,GRAPH_5:def 3;
           reconsider vx=FS.(s2.1) as Vertex of G by A11,Lm3;
      A14:  s1 <> {}
           proof
             assume s1 = {};
          then A15:  len s= 1+ 0 by A10,A11,FINSEQ_1:25;
          then A16:  s.1 orientedly_joins v1,v3 by A13,GRAPH_4:def 1;
                 s.1 in the Edges of G by A15,Th2;
               hence contradiction by A1,A16;
           end;
      then A17:  len s1 >=1 by GRAPH_5:8;
         len s1 < len s by A10,A11,NAT_1:38;
      then A18:  FS.(s.len s)=FT.(s.len s1) by A10,A11,A17,GRAPH_1:def 12
           .=FT.(s1.len s1) by A11,A17,Lm1;
           set Vs=vertices s;
      A19:  Vs \ {v3} c= V' by A7,GRAPH_5:def 4;
      A20:  now
               assume A21: vx <> v2;
            A22: vx in Vs by A9,A12,Lm4;
                  vx <> FT.(s.len s) by A11,A12,A17,A18,Th6;
                then not vx in {v3} by A13,TARSKI:def 1;
                then vx in (Vs \ {v3}) by A22,XBOOLE_0:def 4;
                then A23: vx in V or vx in {v2} by A19,XBOOLE_0:def 2;
            A24: s2.1 orientedly_joins vx,v3 by A12,A13,GRAPH_4:def 1;
                  s2.1 in the Edges of G by A11,Th2;
                hence contradiction by A1,A21,A23,A24,TARSKI:def 1;
           end;
            FS.(s1.1)=v1 by A11,A13,A17,Lm1;
      then A25: s1 is_orientedpath_of v1,v2 by A12,A14,A18,A20,GRAPH_5:def 3;
            len s2 = 1 by A11;
          then not FT.(s.len s) in vertices(s1) by A1,A11,A13,A17,GRAPH_5:21;
      then A26: vertices(s1) \ {v3} = vertices(s1) by A13,ZFMISC_1:65;
            vertices(s1) c= vertices(s1^s2) by GRAPH_5:30;
          then vertices(s1) c= Vs \ {v3} by A11,A26,XBOOLE_1:33;
          then vertices(s1) c= V' by A19,XBOOLE_1:1;
          then vertices(s1) \ {v2} c= V' \ {v2} by XBOOLE_1:33;
      then A27: vertices(s1) \ {v2} c= V \ {v2} by XBOOLE_1:40;
            V \ {v2} c= V by XBOOLE_1:36;
          then vertices(s1) \ {v2} c= V by A27,XBOOLE_1:1;
          then s1 is_orientedpath_of v1,v2,V by A25,GRAPH_5:def 4;
      then A28: cost(P,W) <= cost(s1,W) by A1,GRAPH_5:def 18;
            s2/.1 in Eg by A1;
      then A29: s2.1 in Eg by A11,FINSEQ_4:24;
            FS.e = v2 & FT.e = v3 by A1,GRAPH_4:def 1;
          then e = s2.1 by A1,A12,A13,A20,A29,GRAPH_1:def 4;
      then A30: s2 = <*e*> by A11,FINSEQ_1:57;
      A31: cost(s,W)=cost(s1,W)+cost(s2,W) by A3,A11,GRAPH_5:58;
            cost(Q,W)=cost(P,W)+cost(s2,W) by A1,A3,A30,GRAPH_5:58;
      then A32: cost(Q,W) <= cost(s,W) by A28,A31,REAL_1:55;
            cost(s,W) <= cost(S,W) by A5,A6,GRAPH_5:def 18;
          hence cost(Q,W) <= cost(S,W) by A32,AXIOMS:22;
     end;
A33:  P is_orientedpath_of v1,v2,V by A1,GRAPH_5:def 18;
then P is_orientedpath_of v1,v2 by GRAPH_5:def 4;
     then P <> {} by GRAPH_5:def 3;
then A34:  len P >=1 by GRAPH_5:8;
     reconsider pe=<*e*> as FinSequence of Eg by A1,SCMFSA_7:22;
   len pe = 1 & pe.1=e by FINSEQ_1:57;
     then Q is_orientedpath_of v1,v3,V' by A1,A33,A34,GRAPH_5:38;
     hence thesis by A4,GRAPH_5:def 18;
end;

theorem Th16:
the Vertices 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 Edges 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 Vertices 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 Edges of G & e orientedly_joins v3,v4));
    hereby
       assume A2: P is_shortestpath_of v1,v2,U,W;
 then P is_orientedpath_of v1,v2,U & for Q st Q is_orientedpath_of v1,v2,U
       holds cost(P,W) <= cost(Q,W) by GRAPH_5:def 18;
 then A3:   P is_orientedpath_of v1,v2 by GRAPH_5:def 4;
         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;
       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;
 then P is_orientedpath_of v1,v2 & for Q st Q is_orientedpath_of v1,v2
       holds cost(P,W) <= cost(Q,W) by GRAPH_5:def 17;
 then A5:   P is_orientedpath_of v1,v2,U by A1,Th12;
         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;
       hence P is_shortestpath_of v1,v2,U,W by A5,GRAPH_5:def 18;
    end;
end;

begin  :: The definition of assignment statement

definition let f be Function, i, x be set;
  redefine func f+*(i,x);
  synonym (f,i):=x;
end;

theorem Th17:
  for x,y being set, f being Function holds rng (f,x):=y c= rng f \/ {y}
proof
   let x,y be set,f be Function;
   set TT=(f, x):=y;
   let z be set;
       assume z in rng TT;
       then consider w be set such that
 A1:   w in dom TT & z = TT.w by FUNCT_1:def 5;
 A2:   w in dom f by A1,FUNCT_7:32;
       per cases;
       suppose w<>x;
          then z=f.w by A1,FUNCT_7:34;
          then z in rng f or z in {y} by A2,FUNCT_1:def 5;
          hence z in rng f \/ {y} by XBOOLE_0:def 2;
       suppose w=x;
          then z=y by A1,A2,FUNCT_7:33;
          then z in rng f or z in {y} by TARSKI:def 1;
          hence z in rng f \/ {y} by XBOOLE_0:def 2;
end;

definition let f be FinSequence of REAL, x be set, r be Real;
  redefine func (f, x):=r -> FinSequence of REAL;
  coherence
  proof
       dom ((f, x):=r) = dom f by FUNCT_7:32
     .= Seg (len f) by FINSEQ_1:def 3;
then A1: (f, x):=r is FinSequence by FINSEQ_1:def 2;
      rng ((f, x):=r) c= REAL
    proof let y;
       assume A2: y in rng ((f, x):=r);
         rng ((f, x):=r) c= rng f \/ {r} by Th17;
   then A3: y in rng f or y in {r} by A2,XBOOLE_0:def 2;
         rng f c= REAL by FINSEQ_1:def 4;
       hence y in REAL by A3;
    end;
    hence thesis by A1,FINSEQ_1:def 4;
  end;
end;

definition let i,k be Nat,f be FinSequence of REAL,r be Real;
  func (f,i):=(k,r) -> FinSequence of REAL equals :Def1:
   ((f,i):=k,k):=r;
  coherence;
end;

reserve f,g,h for Element of REAL*,
        r for Real;

theorem Th18:
   i <> k & i in dom f implies ((f,i):=(k,r)).i = k
proof
   assume A1: i <> k & i in dom f;
   set fik = (f,i):=k;
   thus ((f,i):=(k,r)).i = ((fik,k):=r).i by Def1
   .=fik.i by A1,FUNCT_7:34
   .=k by A1,FUNCT_7:33;
end;

theorem Th19:
  m <> i & m <> k & m in dom f implies ((f,i):=(k,r)).m = f.m
proof
     assume A1: m <> i & m <> k & m in dom f;
     set fik = (f,i):=k;
     thus ((f,i):=(k,r)).m = ((fik,k):=r).m by Def1
     .=fik.m by A1,FUNCT_7:34
     .=f.m by A1,FUNCT_7:34;
end;

theorem Th20:
  k in dom f implies ((f,i):=(k,r)).k = r
proof
     assume A1: k in dom f;
     set fik = (f,i):=k;
A2:  dom fik = dom f by FUNCT_7:32;
     thus ((f,i):=(k,r)).k = ((fik,k):=r).k by Def1
     .=r by A1,A2,FUNCT_7:33;
end;

theorem Th21:
 dom ((f,i):=(k,r)) = dom f
proof
   set fik = (f,i):=k;
   thus dom ((f,i):=(k,r)) = dom (((fik,k):=r)) by Def1
   .=dom fik by FUNCT_7:32
   .=dom f by FUNCT_7:32;
end;

begin  :: The definition of Pascal-like while-do statement

definition let X be set;
  redefine func id X -> Element of Funcs(X,X);
  coherence
  proof
      id X in Funcs(X,X) by FUNCT_2:12;
    hence thesis;
  end;
end;

definition let X be set,f,g be Function of X,X;
  redefine func g*f -> Function of X,X;
  coherence proof X <> {} or X = {}; hence thesis by FUNCT_2:19;end;
end;

definition let X be set,f,g be Element of Funcs(X,X);
  redefine func g*f -> Element of Funcs(X,X);
  coherence
  proof
     reconsider f,g as Function of X,X by FUNCT_2:121;
       g*f in Funcs(X,X) by FUNCT_2:12;
     hence thesis;
  end;
end;

definition let X be set,f be Element of Funcs(X,X),g be Element of X;
 redefine func f.g -> Element of X;
 coherence
   proof
A1:  f is Function of X,X by FUNCT_2:121;
     per cases;
     suppose A2: X = {};
        then {} = dom f by A1,FUNCT_2:def 1;
        then f.g = {} by FUNCT_1:def 4;
        hence thesis by A2,SUBSET_1:def 2;
     suppose X <> {};
        hence f.g is Element of X by A1,FUNCT_2:7;
   end;
 end;

definition let X be set, f be Element of Funcs(X,X);
  func repeat(f) -> Function of NAT,Funcs(X,X) means :Def2:
   it.0 = id X & for i being Nat holds it.(i+1)=f*(it.i);
   existence
   proof
     deffunc G(Nat,Element of Funcs(X,X)) = f*$2;
     ex F being Function of NAT,Funcs(X,X) st
      F.0 = id X & for n being Element of NAT holds F.(n+1) = G(n,F.n)
       from LambdaRecExD;
     hence thesis;
   end;
   uniqueness
   proof
    deffunc R(Nat,Element of Funcs(X,X)) = f*$2;
    let F1,F2 be Function of NAT,Funcs(X,X) such that
A1: F1.0 = id X & for i being Nat holds F1.(i+1)=R(i,F1.i) and
A2: F2.0 = id X & for i being Nat holds F2.(i+1)=R(i,F2.i);
    thus F1 = F2 from LambdaRecUnD(A1,A2);
   end;
end;

theorem Th22:
for F being Element of Funcs(REAL*,REAL*),f being Element of REAL*,n,i be Nat
holds (repeat F).0 .f = f
proof
    let F be Element of Funcs(REAL*,REAL*),f be Element of REAL*,n,i be Nat;
    thus (repeat F).0 .f = (id (REAL*)).f by Def2
      .= f by FUNCT_1:35;
end;

Lm5:
for X being set,f being Element of Funcs(X,X) holds dom f=X
proof
     let X be set, f be Element of Funcs(X,X);
     consider ff being Function such that
A1:  f = ff & dom ff = X & rng ff c= X by FUNCT_2:def 2;
     thus thesis by A1;
end;

theorem Th23:
for F,G being Element of Funcs(REAL*,REAL*),f being 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:22
    .=F.(G.ff) by A1,FUNCT_1:22;
end;

definition let g be Element of Funcs(REAL*,REAL*),f be Element of REAL*;
  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;
  func OuterVx(f,n) -> Subset of NAT equals :Def3:
  {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 set;
        assume x in NS;
        then consider k being Nat such that
    A1: x=k & k in dom f & 1 <= k & k <= n & f.k <> -1 & f.(n+k) <> -1;
         thus x in NAT by A1;
     end;
     hence NS is Subset of NAT;
  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) = {};
  func LifeSpan(f,g,n) -> Nat means :Def4:
    OuterVx((repeat f).it.g,n) = {} &
    for k being 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 st P[k] by A1;
     ex k st P[k] & for n st P[n] holds k <= n from Min(A2);
     hence thesis;
   end;
   uniqueness
   proof let it1, it2 be Nat;
     assume A3: not thesis;
     then it1 <= it2 & it2 <= it1;
     hence contradiction by A3,AXIOMS:21;
  end;
end;

definition let f be Element of Funcs(REAL*,REAL*), n be Nat;
  func while_do(f,n) -> Element of Funcs(REAL*,REAL*) means :Def5:
   dom it=REAL* & for h being Element of REAL* holds
   it.h=(repeat f).LifeSpan(f,h,n).h;
   existence
   proof
      set X=REAL*;
      consider ff being Function such that
A1:   f = ff & dom ff = X & rng ff c= X by FUNCT_2:def 2;
      defpred P[set,set] means
          for h being Element of X st $1=h holds
          $2=(repeat f).LifeSpan(f,h,n).h;
A2:    now
          let xx,y1,y2 be set;
          assume A3: xx in dom f & P[xx,y1] & P[xx,y2];
          then reconsider xx as Element of X by A1;
            y1=(repeat f).LifeSpan(f,xx,n).xx &
          y2=(repeat f).LifeSpan(f,xx,n).xx by A3;
          hence y1=y2;
       end;
A4:    now
           let xx be set;
           assume xx in dom f;
           then reconsider h'=xx as Element of X by A1;
             now
               take yy=(repeat f).LifeSpan(f,h',n).h';
               let h be Element of X;
               assume xx=h;
               hence yy=(repeat f).LifeSpan(f,h,n).h;
           end;
          hence ex y1 being set st P[xx,y1];
        end;
       consider f' being Function such that
A5:    dom f'=dom f & for xx being set st xx in dom f holds P[xx, f'.xx]
       from FuncEx(A2,A4);
        rng f' c= X
      proof let y;
           assume y in rng f';
           then consider xx being set such that
      A6:  xx in dom f' & y = f'.xx by FUNCT_1:def 5;
           reconsider h'=xx as Element of X by A1,A5,A6;
             y=(repeat f).LifeSpan(f,h',n).h' by A5,A6;
           hence y in X;
      end;
      then reconsider f' as Element of Funcs(X,X) by A1,A5,FUNCT_2:def 2;
      take f';
      thus dom f' = X by A1,A5;
      let h be Element of X;
      thus f'.h=(repeat f).LifeSpan(f,h,n).h by A1,A5;
   end;
   uniqueness
   proof
       set X=REAL*;
       let g1,g2 be Element of Funcs(X,X) such that
A7:    dom g1 = X & for h being Element of X holds
       g1.h=(repeat f).LifeSpan(f,h,n).h and
A8:    dom g2 = X & for h being Element of X holds
       g2.h=(repeat f).LifeSpan(f,h,n).h;
         now
          let xx be set;
          assume xx in dom g1;
          then reconsider h=xx as Element of X by A7;
          thus g1.xx=(repeat f).LifeSpan(f,h,n).h by A7
                .=g2.xx by A8;
        end;
        hence g1=g2 by A7,A8,FUNCT_1:9;
   end;
end;

begin :: Defining a weight function for an oriented graph

definition
   let G be oriented Graph,v1,v2 be Vertex of G;
   assume A1: ex e be set st e in the Edges of G & e orientedly_joins v1,v2;
   func Edge(v1,v2) means :Def6:
    ex e be set st it = e & e in the Edges 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;
   func Weight(v1,v2,W) equals :Def7:
      W.Edge(v1,v2) if ex e be set st e in the Edges of G &
      e orientedly_joins v1,v2 otherwise -1;
   correctness;
end;

definition
   let G be oriented Graph,v1,v2 be Vertex of G,
       W be Function of (the Edges of G), Real>=0;
   redefine func Weight(v1,v2,W) -> Real;
   coherence
   proof
       per cases;
       suppose A1: ex e be set st e in the Edges of G &
               e orientedly_joins v1,v2;
       then consider e being set such that
   A2:   Edge(v1,v2) = e & e in the Edges of G & e orientedly_joins v1,v2
         by Def6;
           e in dom W by A2,FUNCT_2:def 1;
         then W.Edge(v1,v2) in Real>=0 by A2,PARTFUN1:27;
         hence thesis by A1,Def7;
       suppose not ex e be set st e in the Edges of G &
               e orientedly_joins v1,v2;
         hence thesis by Def7;
   end;
end;

reserve G for oriented Graph,
        v1,v2 for Vertex of G,
        W for Function of (the Edges of G), Real>=0;

theorem Th24:
  Weight(v1,v2,W) >= 0 iff ex e be set st e in the Edges of G &
  e orientedly_joins v1,v2
proof
   set EG=the Edges of G;
   hereby
      assume A1: Weight(v1,v2,W) >= 0;
      assume not ex e be set st e in EG & e orientedly_joins v1,v2;
      then Weight(v1,v2,W) = -1 by Def7;
      hence contradiction by A1;
   end;
   assume ex e be set st e in the Edges of G &
      e orientedly_joins v1,v2;
   then consider e being set such that
A2:  Edge(v1,v2) = e & e in EG & 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:27;
     then consider r being Real such that
A3:  W.e=r & r >=0 by GRAPH_5:def 12;
     thus thesis by A2,A3,Def7;
end;

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

theorem Th26:
  e in the Edges of G & e orientedly_joins v1,v2 implies Weight(v1,v2,W)=W.e
proof
   set EG=the Edges of G;
   assume A1: e in EG & e orientedly_joins v1,v2;
    then consider e1 being set such that
A2: Edge(v1,v2) = e1 & e1 in EG & e1 orientedly_joins v1,v2 by Def6;
     e=e1 by A1,A2,Th10;
   hence thesis by A2,Def7;
end;

begin :: Basic operations for Dijkstra's shortest path algorithm

definition let f be Element of REAL*, n be Nat;
  func UnusedVx(f,n) -> Subset of NAT equals :Def8:
  {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 set;
        assume x in NS;
        then consider k being Nat such that
    A1: x=k & k in dom f & 1 <= k & k <= n & f.k <> -1;
        thus x in NAT by A1;
     end;
     hence NS is Subset of NAT;
  end;
end;

definition let f be Element of REAL*, n be Nat;
  func UsedVx(f,n) -> Subset of NAT equals :Def9:
  {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 set;
        assume x in NS;
        then consider k being Nat such that
    A1: x=k & k in dom f & 1 <= k & k <= n & f.k = -1;
         thus x in NAT by A1;
     end;
     hence NS is Subset of NAT;
  end;
end;

theorem Th27:
  UnusedVx(f,n) c= Seg n
proof
    let x;
    assume x in UnusedVx(f,n);
    then x in {i: i in dom f & 1 <= i & i <= n & f.i <> -1} by Def8;
    then consider i such that
A1: x=i & i in dom f & 1 <= i & i <= n & f.i <> -1;
      x in {k: 1 <= k & k <= n } by A1;
    hence x in Seg n by FINSEQ_1:def 1;
end;

definition let f be Element of REAL*, n be Nat;
 cluster UnusedVx(f,n) -> finite;
 coherence
 proof
     UnusedVx(f,n) c= Seg n by Th27;
   hence thesis by FINSET_1:13;
 end;
end;

theorem Th28:
  OuterVx(f,n) c= UnusedVx(f,n)
proof
     let x;
     assume x in OuterVx(f,n);
     then x in {k: k in dom f & 1 <= k & k <= n & f.k <> -1 & f.(n+k) <> -1}
     by Def3;
     then consider k such that
A1:  x=k & k in dom f & 1 <= k & k <= n & f.k <> -1 & f.(n+k) <> -1;
       x in {i: i in dom f & 1 <= i & i <= n & f.i <> -1} by A1;
     hence x in UnusedVx(f,n) by Def8;
end;

theorem Th29:
  OuterVx(f,n) c= Seg n
proof
A1: OuterVx(f,n) c= UnusedVx(f,n) by Th28;
      UnusedVx(f,n) c= Seg n by Th27;
    hence thesis by A1,XBOOLE_1:1;
end;

definition let f be Element of REAL*, n be Nat;
 cluster OuterVx(f,n) -> finite;
 coherence
 proof
     OuterVx(f,n) c= Seg n by Th29;
   hence thesis by FINSET_1:13;
 end;
end;

definition let X be finite Subset of NAT,f be Element of REAL*,n;
  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 F=0;
        thus (X<>{} implies ex i st i=F & 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 F=0) by A1;
      suppose A2: X<>{};
        then reconsider X'=X as non empty finite Subset of NAT;
         deffunc F(Element of X')= f/.(2*n+$1);
          consider x being Element of X' such that
     A3:  for y being Element of X' holds F(x) <= F(y) from MinValue;
          reconsider x as Nat;
          defpred P[Nat] means
            $1 in X & f/.(2*n+x) = f/.(2*n+$1);
     A4:  ex i st P[i];
          consider i such that
     A5:  P[i] & for k st P[k] holds i <= k from Min(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 X={} implies F=0 by A2;
   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)) &
    (X={} implies F1=0) and
A7: (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)) &
    (X={} implies F2=0);
    per cases;
    suppose A8: X<>{};
       then consider i such that
A9:    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) by A6;
       consider j such that
A10:    j=F2 & j in X & (for k st k in X holds f/.(2*n+j) <= f/.(2*n+k)) &
       for k st k in X & f/.(2*n+j) = f/.(2*n+k) holds j <= k by A7,A8;
A11:    f/.(2*n+i) <= f/.(2*n+j) by A9,A10;
         f/.(2*n+j) <= f/.(2*n+i) by A9,A10;
then A12:    f/.(2*n+j) = f/.(2*n+i) by A11,AXIOMS:21;
then A13:    i <= j by A9,A10;
         j <= i by A9,A10,A12;
       hence F1=F2 by A9,A10,A13,AXIOMS:21;
    suppose X={};
       hence F1=F2 by A6,A7;
   end;
end;

theorem Th30:
 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 consider i such that
A1:  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;
       j in {k: k in dom f & 1 <= k & k<= n & f.k <> -1 & f.(n+k) <> -1}
     by A1,Def3;
     then consider k such that
A2:  j=k & k in dom f & 1 <= k & k<= n & f.k <> -1 & f.(n+k) <> -1;
     thus thesis by A2;
end;

theorem Th31:
  Argmin(OuterVx(f,n),f,n) <= n
proof
    set IN=OuterVx(f,n),
        Ak=Argmin(IN,f,n);
    per cases;
    suppose IN <> {};
      hence Ak <= n by Th30;
    suppose IN = {};
      then Ak=0 by Def10;
      hence Ak <= n by NAT_1:18;
end;

definition let n be Nat;
  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[set,set] 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,y1,y2 be set;
          assume A2: xx in X & P[xx,y1] & P[xx,y2];
          then reconsider h=xx as Element of REAL*;
          thus y1= (h,mi):=(Argmin(OuterVx(h,n),h,n),-1) by A2
          .=y2 by A2;
       end;
A3:    now
           let xx be set;
           assume xx in X;
           then reconsider h=xx as Element of REAL*;
           reconsider y= (h,mi):=(Argmin(OuterVx(h,n),h,n),-1) as set;
           take y;
           thus P[xx,y];
       end;
       consider F being Function such that
A4:    dom F=X & for x st x in X holds P[x,F.x] from FuncEx(A1,A3);
         rng F c= X
       proof let y;
           assume y in rng F;
           then consider xx being set such that
      A5:  xx in dom F & y = F.xx by FUNCT_1:def 5;
           reconsider h=xx as Element of REAL* by A4,A5;
             y = (h,mi):=(Argmin(OuterVx(h,n),h,n),-1) by A4,A5;
           hence y in X by FINSEQ_1:def 11;
       end;
       then reconsider F as Element of Funcs(X,X) by A4,FUNCT_2:def 2;
       take F;
       thus dom F = X by A4;
       let f be Element of REAL*;
       thus F.f = (f,mi):=(Argmin(OuterVx(f,n),f,n),-1) by A4;
   end;
   uniqueness
   proof
     set X=REAL*,
         mi=n*n+3*n+1;
     let F1,F2 be Element of Funcs(X,X) such that
A6:  dom F1= X & for f be Element of REAL* holds
     F1.f= (f,mi):=(Argmin(OuterVx(f,n),f,n),-1) and
A7:  dom F2= X & for f be Element of REAL* holds
     F2.f= (f,mi):=(Argmin(OuterVx(f,n),f,n),-1);
       now
        let xx be set;
        assume xx in dom F1;
        then reconsider h=xx as Element of REAL* by A6;
        thus F1.xx= (h,mi):=(Argmin(OuterVx(h,n),h,n),-1) by A6
        .=F2.xx by A7;
     end;
     hence F1=F2 by A6,A7,FUNCT_1:9;
   end;
end;

theorem Th32:
  i in dom f & 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 in dom f & i > n & i <> mi;
A2: (findmin n).f.i = ((f,mi):=(k,-1)).i by Def11;
      k <= n by Th31;
    hence (findmin n).f.i=f.i by A1,A2,Th19;
end;

theorem Th33:
  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 A1: i in dom f & f.i=-1 & i <> mi;
A2: (findmin n).f.i = ((f,mi):=(k,-1)).i by Def11;
    per cases;
    suppose i=k;
      hence (findmin n).f.i=-1 by A1,A2,Th20;
    suppose i<>k;
      hence (findmin n).f.i=-1 by A1,A2,Th19;
end;

theorem Th34:
  dom ((findmin n).f) = dom f
proof
      (findmin n).f = (f,n*n+3*n+1):=(Argmin(OuterVx(f,n),f,n),-1) by Def11;
    hence thesis by Th21;
end;

Lm6:
  k>=1 implies n <= k*n
proof
  assume k >= 1;
  then 1*n <= k*n by NAT_1:20;
  hence n <= k*n;
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:37;
     hence
A1:  3*n < n*n+3*n +1 by NAT_1:38;
       n <= 3*n by Lm6;
     hence n < n*n+3*n+1 by A1,AXIOMS:22;
       2*n <= 3*n by NAT_1:20;
     hence thesis by A1,AXIOMS:22;
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:20;
    A2: 2*n = n+n by XCMPLX_1:11;
    thus n<k & k <= 2*n implies
      (not (2*n<k & k <= 3*n)) &
      not (k <= n or k > 3*n) by A1,AXIOMS:22;
    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:37;
       thus not (n<k & k <= 2*n) by A4;
     suppose A5:k > 3*n;
       hence not (2*n<k & k <= 3*n);
       thus not (n<k & k <= 2*n) by A1,A5,AXIOMS:22;
    end;
    assume A6: 2*n<k & k <= 3*n;
    hence not (n<k & k <= 2*n);
    thus not (k <=n or k > 3*n) by A2,A6,NAT_1:37;
end;

theorem Th35:
  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) & i in IX &
    (for k st k in IX holds f/.(2*n+i) <= f/.(2*n+k)) &
    (for k st k in IX & f/.(2*n+i) = f/.(2*n+k) holds i <= k) by Def10;
      i in {k: k in dom f & 1 <= k & k <= n & f.k <> -1 & f.(n+k) <> -1}
    by A1,Def3;
     then consider k such that
A2: i=k & k in dom f & 1 <= k & k <= n & f.k <> -1 & f.(n+k) <> -1;
    take i;
    thus i in IX by A1;
    thus 1 <= i & i <= n by A2;
    thus (findmin n).f.i = ((f,n*n+3*n+1):=(i,-1)).i by A1,Def11
    .=-1 by A2,Th20;
end;

definition let f be Element of REAL*,n,k be Nat;
  func newpathcost(f,n,k) -> Real equals :Def12:
   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*;
  pred f hasBetterPathAt n,k means :Def13:
   (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;
  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
     set X=dom f;
A1:  X=Seg len f by FINSEQ_1:def 3;
     defpred P1[Nat] means f hasBetterPathAt n,($1-'n);
     defpred P2[Nat] means f hasBetterPathAt n,($1-'2*n);
     defpred P[set,set] 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);
A2:    now
          let xx,y1,y2 be set;
          assume A3: xx in X & P[xx,y1] & P[xx,y2];
          then reconsider k=xx as Nat;
          per cases;
          suppose A4: n<k & k <= 2*n;
            hereby
               per cases;
               suppose A5: P1[k];
                hence y1 = f/.(n*n+3*n+1) by A3,A4
                   .=y2 by A3,A4,A5;
               suppose A6: not P1[k];
                hence y1 = f.k by A3,A4
                   .=y2 by A3,A4,A6;
            end;
          suppose A7: 2*n<k & k <= 3*n;
            hereby
               per cases;
               suppose A8: P2[k];
                hence y1 = newpathcost(f,n,k-'2*n) by A3,A7
                   .=y2 by A3,A7,A8;
               suppose A9: not P2[k];
                hence y1 = f.k by A3,A7
                   .=y2 by A3,A7,A9;
            end;
          suppose A10: k <=n or k > 3*n;
           hence y1=f.k by A3
                 .=y2 by A3,A10;
       end;
A11:    now
           let xx be set;
           assume xx in X;
           then reconsider k=xx as Nat;
           per cases;
           suppose A12: n<k & k <= 2*n;
              thus ex y1 being set st P[xx,y1]
              proof
               per cases;
               suppose A13: P1[k];
                take y1 = f/.(n*n+3*n+1);
                thus P[xx,y1] by A12,A13,Lm8;
             suppose A14: not P1[k];
                take y1 = f.k;
                 thus P[xx,y1] by A12,A14;
              end;
           suppose A15: 2*n<k & k <= 3*n;
              thus ex y1 being set st P[xx,y1]
              proof
               per cases;
               suppose A16: P2[k];
                take y1 = newpathcost(f,n,k-'2*n);
                thus P[xx,y1] by A15,A16,Lm8;
               suppose A17: not P2[k];
                take y1 = f.k;
                 thus P[xx,y1] by A15,A17;
              end;
           suppose A18: k <=n or k > 3*n;
              thus ex y1 being set st P[xx,y1]
              proof
                take y1=f.k;
                thus P[xx,y1] by A18,Lm8;
              end;
       end;
       consider F being Function such that
A19:    dom F=X & for x st x in X holds P[x,F.x] from FuncEx(A2,A11);
  A20:  rng F c= REAL
       proof let y1 be set;
           assume y1 in rng F;
           then consider xx being set such that
      A21:  xx in dom F & y1 = F.xx by FUNCT_1:def 5;
           reconsider k=xx as Nat by A19,A21;
           per cases;
            suppose A22: n<k & k <= 2*n;
              hereby
               per cases;
               suppose P1[k];
                 then y1 = f/.(n*n+3*n+1) by A19,A21,A22;
                 hence y1 in REAL;
               suppose not P1[k];
                 then y1 = f.k by A19,A21,A22
                    .=f/.k by A19,A21,FINSEQ_4:def 4;
                 hence y1 in REAL;
              end;
            suppose A23: 2*n<k & k <= 3*n;
              hereby
               per cases;
               suppose P2[k];
                 then y1 = newpathcost(f,n,k-'2*n) by A19,A21,A23;
                 hence y1 in REAL;
               suppose not P2[k];
                 then y1 = f.k by A19,A21,A23
                    .=f/.k by A19,A21,FINSEQ_4:def 4;
                 hence y1 in REAL;
              end;
            suppose k <=n or k > 3*n;
                 then y1 = f.k by A19,A21
                    .=f/.k by A19,A21,FINSEQ_4:def 4;
                 hence y1 in REAL;
       end;
         F is FinSequence by A1,A19,FINSEQ_1:def 2;
       then F is FinSequence of REAL by A20,FINSEQ_1:def 4;
       then reconsider F as Element of REAL* by FINSEQ_1:def 11;
       take F;
       thus dom F = X by A19;
       let k;
          assume k in X;
          hence (n<k & k <= 2*n implies (P1[k] implies F.k=f/.(n*n+3*n+1)) &
           (not P1[k] implies F.k=f.k)) & (2*n <k & k <=3*n implies
           (P2[k] implies F.k=newpathcost(f,n,k-'2*n)) &
           (not P2[k] implies F.k=f.k)) & (k<=n or k > 3*n implies
           F.k=f.k) by A19;
   end;
   uniqueness
   proof
     let F1,F2 be Element of REAL* such that
A24: dom F1 = dom f & 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
A25: dom F2 = dom f & 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 set;
         assume A26:xx in dom F1;
         then reconsider k=xx as Nat;
         defpred P1[] means f hasBetterPathAt n,(k-'n);
         defpred P2[] means f hasBetterPathAt n,(k-'2*n);
         per cases;
          suppose A27: n<k & k <= 2*n;
            hereby
               per cases;
               suppose A28: P1[];
                hence F1.xx = f/.(n*n+3*n+1) by A24,A26,A27
                   .=F2.xx by A24,A25,A26,A27,A28;
               suppose A29: not P1[];
                hence F1.xx = f.k by A24,A26,A27
                   .=F2.xx by A24,A25,A26,A27,A29;
            end;
          suppose A30: 2*n<k & k <= 3*n;
            hereby
               per cases;
               suppose A31: P2[];
                hence F1.xx = newpathcost(f,n,k-'2*n) by A24,A26,A30
                   .=F2.xx by A24,A25,A26,A30,A31;
               suppose A32: not P2[];
                hence F1.xx = f.k by A24,A26,A30
                   .=F2.xx by A24,A25,A26,A30,A32;
            end;
          suppose A33: k <=n or k > 3*n;
           hence F1.xx=f.k by A24,A26
                 .=F2.xx by A24,A25,A26,A33;
    end;
     hence F1=F2 by A24,A25,FUNCT_1:9;
   end;
end;

definition let n be Nat;
  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
      set X=REAL*;
      defpred P[set,set] means
       for f be Element of REAL* st $1=f holds
       $2=Relax(f,n);
A1:    now
          let xx,y1,y2 be set;
          assume A2: xx in X & P[xx,y1] & P[xx,y2];
          then reconsider h=xx as Element of REAL*;
          thus y1 = Relax(h,n) by A2
               .=y2 by A2;
       end;
A3:    now
           let xx be set;
           assume xx in X;
           then reconsider h=xx as Element of REAL*;
           thus ex y1 being set st P[xx,y1]
           proof
             take y1 = Relax(h,n);
             thus P[xx,y1];
           end;
       end;
       consider F being Function such that
A4:    dom F=X & for x st x in X holds P[x,F.x] from FuncEx(A1,A3);
         now
           let y1 be set;
           assume y1 in rng F;
           then consider xx being set such that
      A5:  xx in dom F & y1 = F.xx by FUNCT_1:def 5;
           reconsider h=xx as Element of REAL* by A4,A5;
             y1 = Relax(h,n) by A4,A5;
           hence y1 in X;
       end;
       then rng F c= X by TARSKI:def 3;
       then reconsider F as Element of Funcs(X,X) by A4,FUNCT_2:def 2;
       take F;
       thus dom F = X by A4;
       let f be Element of REAL*;
       thus F.f=Relax(f,n) by A4;
   end;
   uniqueness
   proof
     set X=REAL*;
     let F1,F2 be Element of Funcs(X,X) such that
A6:  dom F1= X & for f be Element of REAL* holds
     F1.f=Relax(f,n) and
A7:  dom F2= X & for f be Element of REAL* holds
     F2.f=Relax(f,n);
       now
         let xx be set;
         assume xx in dom F1;
         then reconsider h=xx as Element of REAL* by A6;
         thus F1.xx= Relax(h,n) by A6
         .=F2.xx by A7;
     end;
     hence F1=F2 by A6,A7,FUNCT_1:9;
   end;
end;

theorem Th36:
    dom ((Relax n).f) = dom f
proof
    thus dom ((Relax n).f) = dom Relax(f,n) by Def15
    .= dom f by Def14;
end;

theorem Th37:
 (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 Th38:
   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 Th23
    .= dom (M.ff) by Th36
    .= dom ff by Th34;
end;

theorem Th39:
 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;
    assume A1: OuterVx(ff,n) <> {};
    set Fi1=(repeat (R*M)).(i+1).f;
A2: dom Fi1 = dom ff by Th38
    .= dom (M.ff) by Th34;
    consider j such that
A3: j in OuterVx(ff,n) & 1 <= j & j <= n & (M.ff).j=-1 by A1,Th35;
    A4: OuterVx(ff,n) c= UnusedVx(ff,n) by Th28;
A5: UnusedVx(Fi1,n) c= UnusedVx(ff,n)
    proof let x;
        assume x in UnusedVx(Fi1,n);
        then x in {k: k in dom Fi1 & 1 <= k & k <= n & Fi1.k <> -1}
        by Def8;
        then consider k such that
   A6:   x=k & k in dom Fi1 & 1 <= k & k <= n & Fi1.k <> -1;
   A7:   k in dom ff by A6,Th38;
         A8: n < n*n+3*n+1 by Lm7;
           Fi1.k=(R.(M.ff)).k by Th23
         .=(M.ff).k by A2,A6,Th37;
         then ff.k <> -1 by A6,A7,A8,Th33;
         then x in {m: m in dom ff & 1 <= m & m <= n & ff.m <> -1} by A6,A7;
         hence x in UnusedVx(ff,n) by Def8;
    end;
      now
        let x;
        assume x in UnusedVx(Fi1,n);
        then x in {k: k in dom Fi1 & 1 <= k & k <= n & Fi1.k <> -1}
        by Def8;
        then consider k such that
   A9:   x=k & k in dom Fi1 & 1 <= k & k <= n & Fi1.k <> -1;
           Fi1.k=(R.(M.ff)).k by Th23
         .=(M.ff).k by A2,A9,Th37;
         hence (M.ff).x <> -1 by A9;
    end;
    then UnusedVx(Fi1,n) <> UnusedVx(ff,n) by A3,A4;
    hence UnusedVx(Fi1,n) c< UnusedVx(ff,n) by A5,XBOOLE_0:def 8;
end;

theorem Th40:
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 A1: g=ff & h=Fi1 & k=Argmin(OuterVx(g,n),g,n) & OuterVx(g,n) <> {};
then A2: dom h = dom ff by Th38;
then A3: dom h = dom (M.ff) by Th34;
A4: M.ff = (ff,mi):=(k,-1) by A1,Def11;
A5: dom g=dom (M.ff) by A1,Th34;
A6: now let x;
        assume x in UsedVx(h,n);
        then x in {m: m in dom h & 1 <= m & m <= n & h.m = -1} by Def9;
        then consider m such that
  A7:   x=m & m in dom h & 1 <= m & m <= n & h.m = -1;
        per cases;
        suppose m=k;
           then x in {k} by A7,TARSKI:def 1;
           hence x in (UsedVx(g,n) \/ {k}) by XBOOLE_0:def 2;
        suppose A8: m<>k;
         A9: n < mi by Lm7;
   A10:   m in dom ff by A1,A7,Th38;
           -1=(R.(M.ff)).m by A1,A7,Th23
         .=(M.ff).m by A3,A7,Th37
         .=ff.m by A4,A7,A8,A9,A10,Th19;
         then m in {j: j in dom ff & 1 <= j & j <= n & ff.j=-1} by A2,A7;
         then x in UsedVx(ff,n) by A7,Def9;
         hence x in (UsedVx(g,n) \/ {k}) by A1,XBOOLE_0:def 2;
    end;
      now let x;
        assume A11: x in (UsedVx(g,n) \/ {k});
        per cases by A11,XBOOLE_0:def 2;
        suppose x in UsedVx(g,n);
         then x in {m: m in dom g & 1 <= m & m <= n & g.m = -1} by Def9;
         then consider m such that
    A12:  x=m & m in dom g & 1 <= m & m <= n & g.m = -1;
         A13: n < mi by Lm7;
           h.m=(R.(M.ff)).m by A1,Th23
         .=(M.ff).m by A5,A12,Th37
         .=-1 by A1,A12,A13,Th33;
         then m in {j: j in dom h & 1 <= j & j <= n & h.j=-1} by A1,A2,A12;
         hence x in UsedVx(h,n) by A12,Def9;
        suppose x in {k};
    then A14:  x = k by TARSKI:def 1;
    A15:  k in dom g & 1 <= k & k <= n by A1,Th30;
           h.k=(R.(M.ff)).k by A1,Th23
         .=(M.ff).k by A5,A15,Th37
         .=-1 by A1,A4,A15,Th20;
         then k in {j: j in dom h & 1 <= j & j <= n & h.j=-1} by A1,A2,A15;
         hence x in UsedVx(h,n) by A14,Def9;
    end;
    hence UsedVx(h,n)=UsedVx(g,n) \/ {k} by A6,TARSKI:2;
    assume k in UsedVx(g,n);
    then k in {j: j in dom g & 1 <= j & j <= n & g.j=-1} by Def9;
    then consider j such that
A16: j=k & j in dom g & 1 <= j & j <= n & g.j=-1;
    thus contradiction by A1,A16,Th30;
end;

theorem Th41:
 ex i st i<=n & OuterVx((repeat(Relax(n)*findmin(n))).i.f,n) = {}
proof
    set R=Relax n,
        M=findmin n;
    assume A1:not ex i st i<=n & OuterVx((repeat(R*M)).i.f,n) = {};
    defpred P[Nat] means
       $1<=n implies card UnusedVx((repeat(R*M)).$1.f,n) <= n-$1;
A2: P[0]
    proof
      assume 0<=n;
      set f0=(repeat(R*M)).0 .f;
        UnusedVx(f0,n) c= Seg n by Th27;
      then card UnusedVx(f0,n) <= card Seg n by CARD_1:80;
      hence card UnusedVx(f0,n) <= n-0 by FINSEQ_1:78;
    end;
A3: for k st P[k] holds P[k+1]
    proof
        let k;
        assume A4: P[k];
          now
            assume A5: k+1 <= n;
            A6: k <= k+1 by NAT_1:29;
       then A7:  k <= n by A5,AXIOMS:22;
        set fk=UnusedVx((repeat(R*M)).k.f,n),
            fk1=UnusedVx((repeat(R*M)).(k+1).f,n);
              OuterVx((repeat(R*M)).k.f,n) <> {} by A1,A7;
            then fk1 c< fk by Th39;
            then card fk1 < card fk by CARD_2:67;
            then card fk1 < n-k by A4,A5,A6,AXIOMS:22;
            then card fk1 + 1 <= n-k by INT_1:20;
            then card fk1 <= n-k-1 by REAL_1:84;
            hence card fk1 <= n-(k+1) by XCMPLX_1:36;
        end;
        hence P[k+1];
    end;
      for k holds P[k] from Ind(A2,A3);
then A8: P[n];
    set nf=(repeat(R*M)).n.f;
      n-n=0 by XCMPLX_1:14;
    then card UnusedVx(nf,n) = 0 by A8,NAT_1:19;
then A9: UnusedVx(nf,n) = {} by GRAPH_5:5;
      OuterVx(nf,n) c= UnusedVx(nf,n) by Th28;
    then OuterVx(nf,n) = {} by A9,XBOOLE_1:3;
    hence contradiction by A1;
end;

Lm9:
    n-(k+1)+1=n-k
proof
    thus n-(k+1)+1=n-k-1+1 by XCMPLX_1:36
    .=(n-k)+1-1 by XCMPLX_1:29
    .=n-k by XCMPLX_1:26;
end;

Lm10:
    n-k <= n
proof
      n <= n+k by NAT_1:29;
    hence n - k <= n by REAL_1:86;
end;

Lm11:
for p,q being FinSequence of NAT,f be Element of REAL*,i,n be 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 Nat;
    assume A1:(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;
      defpred P[Nat] means
        $1 < len p implies p.(len p-$1)=q.(len q-$1);
A2:  P[0] by A1;
A3:  for k st P[k] holds P[k+1]
     proof
        let k;
        assume A4: P[k];
          now
            assume A5: k+1 < len p;
            A6: k <= k+1 by NAT_1:29;
       A7:  len p-k <= len p by Lm10;
       A8:  1 <= len p-k by A5,REAL_1:84;
       A9:  len q-k <= len q by Lm10;
              len p - k <= len q - k by A1,REAL_1:49;
       then A10:  1 <= len q- k by A8,AXIOMS:22;
       A11:  p/.(len p-k)=p.(len p-k) by A7,A8,Th3
            .=q/.(len q-k) by A4,A5,A6,A9,A10,Th3,AXIOMS:22;
       A12:  1 <= k+1 by NAT_1:29;
       A13:  k+1 < len q by A1,A5,AXIOMS:22;
       thus p.(len p-(k+1))=f.(p/.(len p-(k+1)+1)+n) by A1,A5,A12
            .=f.(p/.(len p-k)+n) by Lm9
            .=f.(q/.(len q-(k+1)+1)+n) by A11,Lm9
            .=q.(len q-(k+1)) by A1,A12,A13;
       end;
       hence P[k+1];
     end;
       for k holds P[k] from Ind(A2,A3);
     hence thesis;
end;

theorem Th42:
   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);
A1: P[0]
    proof
      thus dom ((repeat(R*M)).0 .f)= dom ((id (REAL*)).f) by Def2
      .= dom f by FUNCT_1:35;
    end;
A2:  for k st P[k] holds P[k+1] by Th38;
       for k holds P[k] from Ind(A1,A2);
     hence thesis;
end;

definition
   let f,g be Element of REAL*,m,n;
   pred f,g equal_at m,n means :Def16:
     dom f = dom g & for k st k in dom f & m <=k & k <= n holds f.k=g.k;
end;

theorem Th43:
   f,f equal_at m,n
proof
      dom f = dom f & for k st k in dom f & m <=k & k <= n holds f.k=f.k;
    hence thesis by Def16;
end;

theorem Th44:
   f,g equal_at m,n & g,h equal_at m,n implies f,h equal_at m,n
proof
    assume A1:f,g equal_at m,n & g,h equal_at m,n;
then A2: dom f = dom g & for k st k in dom f & m <=k & k <= n holds f.k=g.k
    by Def16;
A3: dom g = dom h & for k st k in dom g & m <=k & k <= n holds g.k=h.k
    by A1,Def16;
      now let k;
        assume A4:k in dom f & m <=k & k <= n;
        hence f.k=g.k by A1,Def16
        .=h.k by A1,A2,A4,Def16;
    end;
    hence thesis by A2,A3,Def16;
end;

theorem Th45:
 (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: dom (Fi1) = dom ff by Th38;
      now let k;
         assume A2: k in dom ff & 3*n+1 <= k & k <= n*n+3*n;
   then A3:   k > 3*n by NAT_1:38;
   A4:   k in dom (M.ff) by A2,Th34;
   A5:   k < n*n+3*n+1 by A2,NAT_1:38;
           3*n >= n by Lm6;
   then A6:   k > n by A3,AXIOMS:22;
      thus Fi1.k=(R.(M.ff)).k by Th23
         .=(M.ff).k by A3,A4,Th37
         .=ff.k by A2,A5,A6,Th32;
    end;
    hence thesis by A1,Def16;
end;

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

theorem Th47:
  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: P[0]
    proof
        (repeat(R*M)).0 .f =f by Th22;
      hence thesis by Th43;
    end;
A2:  for k st P[k] holds P[k+1]
     proof
        let k;
        assume A3: P[k];
          (repeat(R*M)).k.f, (repeat(R*M)).(k+1).f equal_at m,mm by Th45;
        hence thesis by A3,Th44;
     end;
       for k holds P[k] from Ind(A1,A2);
     hence thesis;
end;

theorem Th48:
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 A1: 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;
A2:  OuterVx(f,n) <> {}
     proof
          f.1=1 by A1;
        then 1 in {j: j in dom f & 1 <= j & j <= n & f.j <> -1 & f.(n+j) <> -1
}
        by A1;
       hence thesis by Def3;
     end;
    set k=Argmin(OuterVx(f,n),f,n);
    thus
A3: k=1
    proof
       assume A4: k<>1;
    A5:  1<=k & k<=n & f.k <> -1 & f.(n+k) <> -1 by A2,Th30;
         then 1 < k by A4,REAL_1:def 5;
         then 1+1 <= k by INT_1:20;
         hence contradiction by A1,A5;
    end;thus
A6: UsedVx(f,n)={}
     proof
       assume UsedVx(f,n)<>{};
          then consider x such that
     A7:  x in UsedVx(f,n) by XBOOLE_0:def 1;
            x in {j: j in dom f & 1 <= j & j <= n & f.j = -1} by A7,Def9;
          then consider j such that
     A8:  x=j & j in dom f & 1 <= j & j <= n & f.j = -1;
          thus contradiction by A1,A8;
     end;
A9:  OuterVx(f0,n) <> {} by A2,Th22;
A10:  Argmin(OuterVx(f0,n),f0,n) = Argmin(OuterVx(f,n),f0,n) by Th22
     .=1 by A3,Th22;
   thus UsedVx(RT.1.f,n) = UsedVx(RT.(0+1).f,n)
    .=UsedVx(f0,n) \/ {1} by A9,A10,Th40
    .= UsedVx(f,n) \/ {1} by Th22
    .={1} by A6;
end;

theorem Th49:
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 A1: g=RT.1.f & h=RT.i.f & 1<=i & i <= cn & m in UsedVx(g,n);
    defpred P[Nat] means
     1<=$1 & $1<=cn implies m in UsedVx(RT.$1.f ,n);
A2: P[0];
A3:  for k st P[k] holds P[k+1]
     proof
        let k;
        assume A4: P[k];
        hereby
            assume A5: 1<=k+1 & k+1 <= cn;
            per cases;
            suppose k=0;
              hence m in UsedVx(RT.(k+1).f ,n) by A1;
            suppose k<>0;
              then k > 0 by NAT_1:19;
          then A6: k >= 1+ 0 by INT_1:20;
            k < cn by A5,NAT_1:38;
              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 Th40;
              then UsedVx(RT.k.f,n) c= UsedVx(RT.(k+1).f,n) by XBOOLE_1:7;
              hence m in UsedVx(RT.(k+1).f ,n) by A4,A5,A6,NAT_1:38;
        end;
     end;
       for k holds P[k] from Ind(A2,A3);
     hence thesis by A1;
end;

definition
   let p be FinSequence of NAT,f be Element of REAL*,i,n be Nat;
  pred p is_vertex_seq_at f,i,n means :Def17:
   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;
  pred p is_simple_vertex_seq_at f,i,n means :Def18:
   (p.1=1 & len p > 1 & p is_vertex_seq_at f,i,n) & p is one-to-one;
end;

theorem
  for p,q being FinSequence of NAT,f be Element of REAL*,i,n be 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 Nat;
    assume A1: p is_simple_vertex_seq_at f,i,n &
    q is_simple_vertex_seq_at f,i,n;
  then A2: p.1=1 & len p > 1 & p is_vertex_seq_at f,i,n by Def18;
  then A3: p.(len p)=i & for k st 1<=k & k < len p holds
      p.(len p-k)=f.(p/.(len p-k+1)+n) by Def17;
  A4: q.1=1 & len q > 1 & q is_vertex_seq_at f,i,n by A1,Def18;
  then A5: q.(len q)=i & for k st 1<=k & k < len q holds
      q.(len q-k)=f.(q/.(len q-k+1)+n) by Def17;
      A6: now
          assume A7: len p <> len q;
          per cases;
          suppose A8: len p < len q;
            A9: q is one-to-one by A1,Def18;
                A10: len p -1 > 1-1 by A2,REAL_1:92;
                then reconsider k=len p -1 as Nat by INT_1:16;
          A11:   k >= 0+1 by A10,INT_1:20;
          A12:   len p - k = len p - len p +1 by XCMPLX_1:37
                .=0+1 by XCMPLX_1:14;
                  k < len p by INT_1:26;
          then A13:   1=q.(len q-k) by A2,A3,A5,A8,A11,A12,Lm11;
          A14:   len q - k > 1 by A8,A12,REAL_1:92;
                then len q - k > 0 by AXIOMS:22;
                then reconsider m=len q -k as Nat by INT_1:16;
                  m <= len q by Lm10;
                hence contradiction by A4,A9,A13,A14,GRAPH_5:9;
          suppose A15: len p >= len q;
          then A16: len p > len q by A7,REAL_1:def 5;
          A17: p is one-to-one by A1,Def18;
            hereby
               per cases;
               suppose len q <=1;
                  hence contradiction by A1,Def18;
               suppose len q > 1;
                  then A18: len q -1 > 1-1 by REAL_1:92;
                  then reconsider k=len q -1 as Nat by INT_1:16;
            A19:   k >= 0+1 by A18,INT_1:20;
            A20:   len q - k = len q - len q +1 by XCMPLX_1:37
                  .=0+1 by XCMPLX_1:14;
                    k < len q by INT_1:26;
            then A21:   1=p.(len p-k) by A3,A4,A5,A15,A19,A20,Lm11;
            A22:   len p - k > 1 by A16,A20,REAL_1:92;
                  then len p - k > 0 by AXIOMS:22;
                  then reconsider m=len p -k as Nat by INT_1:16;
                    m <= len p by Lm10;
                  hence contradiction by A2,A17,A21,A22,GRAPH_5:9;
            end;
      end;
          now let k;
          assume A23: 1 <=k & k <= len p;
          per cases;
          suppose k=len p;
            hence p.k=q.k by A2,A5,A6,Def17;
          suppose k <> len p;
            then k < len p by A23,REAL_1:def 5;
            then len p-k > k-k by REAL_1:92;
        then A24: len p-k > 0 by XCMPLX_1:14;
            then reconsider m=len p-k as Nat by INT_1:16;
        A25: m >= 0+1 by A24,INT_1:20;
        A26: len q - m = len q - len p +k by XCMPLX_1:37
            .=0+k by A6,XCMPLX_1:14;
        A27: len p - k <= len p -1 by A23,REAL_1:92;
              len p-1 < len p by INT_1:26;
            then m < len p by A27,AXIOMS:22;
            hence p.k=q.k by A3,A5,A6,A25,A26,Lm11;
       end;
       hence p=q by A6,FINSEQ_1:18;
end;

definition
  let G be Graph,p be FinSequence of the Edges of G,vs be FinSequence;
 pred p is_oriented_edge_seq_of vs means :Def19:
    len vs = len p + 1 &
    for n 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
  for G being oriented Graph,vs be FinSequence,p,q being 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 A1: p is_oriented_edge_seq_of vs & q is_oriented_edge_seq_of vs;
     then len p+1 = len vs by Def19
     .= len q +1 by A1,Def19;
then A2:  len p = len q by XCMPLX_1:2;
       now let k;
        assume A3: 1<=k & k <= len p;
     then A4: (the Source of G).(p.k) = vs.k by A1,Def19
         .=(the Source of G).(q.k) by A1,A2,A3,Def19;
     A5: (the Target of G).(p.k) = vs.(k+1) by A1,A3,Def19
         .=(the Target of G).(q.k) by A1,A2,A3,Def19;
            p.k in the Edges of G & q.k in the Edges of G by A2,A3,Th2;
         hence p.k=q.k by A4,A5,GRAPH_1:def 4;
     end;
     hence thesis by A2,FINSEQ_1:18;
end;

theorem
  for G being Graph,vs1,vs2 be FinSequence,p being 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 A1: p is_oriented_edge_seq_of vs1 & p is_oriented_edge_seq_of vs2
     & len p >= 1;
then A2:  len vs1 = len p+1 by Def19
     .= len vs2 by A1,Def19;
       now let k;
        assume A3: 1<=k & k <= len vs1;
        per cases;
        suppose k = len vs1;
     then A4:  k = len p + 1 by A1,Def19;
          hence vs1.k=(the Target of G).(p.len p) by A1,Def19
                .=vs2.k by A1,A4,Def19;
        suppose k <> len vs1;
          then k < len vs1 by A3,REAL_1:def 5;
          then k+1 <= len vs1 by INT_1:20;
          then k+1 <= len p+1 by A1,Def19;
     then A5:  k <= len p by REAL_1:53;
          hence vs1.k=(the Source of G).(p.k) by A1,A3,Def19
                .=vs2.k by A1,A3,A5,Def19;
     end;
     hence thesis by A2,FINSEQ_1:18;
end;

Lm12:
  1<= i & i <= n implies 1 < 2*n+i & 2*n+i < n*n+3*n+1 & i < 2*n + i
proof
   assume A1: 1<= i & i <= n;
   set m2=2*n+i;
     2*n+n=2*n+1*n
     .=(2+1)*n by XCMPLX_1:8;
then A2:  m2 <= 3*n by A1,REAL_1:55;
       2*n+1 <= m2 by A1,REAL_1:55;
then A3:  2*n < m2 by NAT_1:38;
       1 <= n by A1,AXIOMS:22;
     then 2*1 <= 2*n by AXIOMS:25;
     then 2 < m2 by A3,AXIOMS:22;
    hence 1 < m2 by AXIOMS:22;
       3*n < n*n+3*n+1 by Lm7;
    hence m2 < n*n+3*n+1 by A2,AXIOMS:22;
       n <= 2*n by Lm6;
     then i <= 2*n by A1,AXIOMS:22;
     hence i < m2 by A3,AXIOMS:22;
end;

Lm13:
   1<= i & i <= n implies 1 < n+i & n+i <= 2*n & n+i < n*n+3*n+1
proof
   assume A1: 1<= i & i <= n;
   set ni=n+i;
       1 <= n by A1,AXIOMS:22;
     then 1+1 <= ni by A1,REAL_1:55;
     hence 1 < ni by NAT_1:38;
       ni <= n+n by A1,REAL_1:55;
     hence
A2:  ni <= 2*n by XCMPLX_1:11;
       2*n < n*n+3*n+1 by Lm7;
     hence thesis by A2,AXIOMS:22;
end;

Lm14:
    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 A1: 1<= i & i <= n & j<=n;
   set m3=2*n+n*i+j;
A2:  m3=2*n+(n*i+j) by XCMPLX_1:1;
A3:  1 <= n by A1,AXIOMS:22;
     then 2*1 <= 2*n by AXIOMS:25;
then A4:  1 < 2*n by AXIOMS:22;
       2*n <= m3 by A2,NAT_1:37;
     hence 1 < m3 by A4,AXIOMS:22;
       0 < i by A1,AXIOMS:22;
     then 1*i <= n*i by A3,AXIOMS:25;
then A5:  1+i < 2*n+n*i by A4,REAL_1:67;
       2*n+n*i <= m3 by NAT_1:37;
     then 1+i < m3 by A5,AXIOMS:22;
     hence i < m3 by NAT_1:38;
       2*n+n=2*n+1*n
     .=(2+1)*n by XCMPLX_1:8;
then A6:  2*n+j <= 3*n by A1,REAL_1:55;
A7:  m3 = 2*n+j+n*i by XCMPLX_1:1;
       0 < n by A1,AXIOMS:22;
     then n*i <= n*n by A1,AXIOMS:25;
     then m3 <= n*n+3*n by A6,A7,REAL_1:55;
     hence thesis by NAT_1:38;
end;

Lm15:
    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 A1: 1<= i & i <= n & 1<=j & j<=n;
   set m3=2*n+n*i+j;
A2:  2*n+n=2*n+1*n
     .=(2+1)*n by XCMPLX_1:8;
A3:  0 < n by A1,AXIOMS:22;
     then n*1 <= n*i by A1,AXIOMS:25;
     then 2*n + n <= 2*n +n*i by REAL_1:55;
     hence 3*n+1 <= m3 by A1,A2,REAL_1:55;
A4:  2*n+j <= 3*n by A1,A2,REAL_1:55;
A5:  m3 = 2*n + j + n*i by XCMPLX_1:1;
       n*i <= n*n by A1,A3,AXIOMS:25;
     hence thesis by A4,A5,REAL_1:55;
end;

begin :: Data structure for Dijkstra's shortest path algorithm
:: address  possible value  init. value   comment
::   1         1 or -1         1          -1 if node v1 is used
::   2         1 or -1         1          -1 if node v2 is used
::   :            :            :                  :
::   n         1  or -1        1          -1 if node vn is used
::   n+1       0               0          preceding-node of v1 toward v1
::   n+2       -1 or Node No.  -1         preceding-node of v2 toward v1
::   :             :           :                  :
::   2*n       -1 or Node No.  -1         preceding-node of vn toward v1
::   2*n+1     0               0          cost from v1 to v1
::   2*n+2     >=0             0          minimum cost from v2 to v1
::   :            :            :                  :
::   3*n       >=0             0          minimum cost from vn to v1
::   3*n+1     weight(v1,v1)              the weight of edge(v1,v1)
::   3*n+2     weight(v1,v2)              the weight of edge(v1,v2)
::   :            :                                :
::   4*n       weight(v1,vn)              the weight of edge(v1,vn)
::   :            :                                :
::   n*n+3*n   weight(vn,vn)              the weight of edge(vn,vn)
::   n*n+3n+1   Node No.                  current node with the shortest path

definition
   let f be Element of REAL*,G be oriented Graph,n be Nat,
   W be Function of (the Edges of G), Real>=0;
  pred f is_Input_of_Dijkstra_Alg G,n,W means :Def20:
   len f=n*n+3*n+1 & Seg n=the Vertices 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 being Vertex of G,k,m st k=i & m=j holds
   f.(2*n+n*k+m)=Weight(i,j,W));
end;

begin :: The definition of Dijkstra's shortest path algorithm

definition let n be Nat;
  func DijkstraAlgorithm n -> Element of Funcs(REAL*,REAL*) equals :Def21:
  while_do(Relax(n)*findmin(n),n);
  coherence;
end;

begin :: Justifying the correctness of Dijkstra's shortest path algorithm

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 Edges of G), Real>=0,
        v1,v2,v3,v4 for Vertex of G;

Lm16:
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 A1: f is_Input_of_Dijkstra_Alg G,n,W & v1=1 & n >= 1 &
               h=(repeat(Relax(n)*findmin(n))).1.f;
    set Ak=Argmin(OuterVx(f,n),f,n);
A2:  1 <= mi by NAT_1:37;
A3:  len f=mi & f.(n+1) =0 & (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,Def20;
then A4:  1 in dom f by A2,FINSEQ_3:27;
then A5:  1 = Ak & UsedVx(f,n)={} & {1} = UsedVx(h,n) by A1,A3,Th48;
A6:  M.f0= M.f by Th22
     .= (f,mi):=(1,-1) by A5,Def11;
A7:  dom (M.f0) = dom f0 by Th34
     .= dom f by Th22;
   h=(repeat (R*M)).(0+1).f by A1;
     then h=R.(M.f0) by Th23;
then A8:  h=Relax(M.f0,n) by Def15;
A9:  Seg n=the Vertices of G by A1,Def20;
     then reconsider VG=the Vertices of G as non empty Subset of NAT by A1,
FINSEQ_1:3;
       W is_weight>=0of G by GRAPH_5:def 13;
then A10:  W is_weight_of G by GRAPH_5:50;
A11:  2*1 <= 2*n by A1,AXIOMS:25;
       0 <= n by A1,AXIOMS:22;
then A12:  n*1 <= n*n by A1,AXIOMS:25;
A13:  2*n < mi by Lm7;
A14:  2*n+n=2*n+1*n
     .=(2+1)*n by XCMPLX_1:8;
    hereby
         let v3,j;
         set nj=n+j;
         assume A15: v3<>v1 & v3=j & h.(n+j)<>-1;
         then j in VG;
    then A16:  1<=j & j <= n by A9,FINSEQ_1:3;
    then A17:  1 < nj & nj <= 2*n & nj < mi by Lm13;
    then A18:  nj in dom f by A3,FINSEQ_3:27;
    then A19:  (M.f0).nj = f.nj by A6,A17,Th19;
    A20:  nj -' n=j by BINARITH:39;
           n+1 <= nj by A16,REAL_1:55;
    then A21:  n < nj by NAT_1:38;
           j > 1 by A1,A15,A16,REAL_1:def 5;
         then j >= 1+1 by INT_1:20;
    then f.nj=-1 by A1,A16,Def20;
    then A22:  M.f0 hasBetterPathAt n,(nj -' n) by A7,A8,A15,A17,A18,A19,A21,
Def14;
         set m2=2*n+j;
    A23:  m2 <= 3*n by A14,A16,REAL_1:55;
           2*n+1 <= m2 by A16,REAL_1:55;
    then A24:  2*n < m2 by NAT_1:38;
    A25:  m2 -' 2*n = j by BINARITH:39;
    A26:  1 < m2 & m2 < mi by A16,Lm12;
    then A27:  m2 in dom (M.f0) by A3,A7,FINSEQ_3:27;
    A28:  mi in dom f by A2,A3,FINSEQ_3:27;
    then A29:  M.f0/.mi = M.f0.mi by A7,FINSEQ_4:def 4
         .=1 by A6,A26,A28,Th18;
         set m3=2*n+n*1+j;
    A30:  1 < m3 & m3 < mi by A1,A16,Lm14;
    then A31:  m3 in dom f by A3,FINSEQ_3:27;
    then A32:  M.f0/.(2*n+n*(M.f0/.mi)+j)=M.f0.m3 by A7,A29,FINSEQ_4:def 4
         .=f.m3 by A6,A30,A31,Th19
         .=Weight(v1,v3,W) by A1,A15,Def20;
         set w1=2*n+1;
    A33:  1 < w1 & w1 < mi by A1,Lm12;
    then A34:  w1 in dom f by A3,FINSEQ_3:27;
    then A35:  M.f0/.(2*n+M.f0/.mi)=M.f0.w1 by A7,A29,FINSEQ_4:def 4
         .=f.w1 by A6,A33,A34,Th19
         .=0 by A1,Def20;
    A36:  Relax(M.f0,n).m2=newpathcost(M.f0,n,m2-'2*n)
           by A20,A22,A23,A24,A25,A27,Def14
         .=0 + M.f0/.(2*n+n*(M.f0/.mi)+j) by A25,A35,Def12;
    A37:  h.nj=1 by A7,A8,A17,A18,A21,A22,A29,Def14;
           M.f0/.(2*n+n*(M.f0/.mi)+j) >= 0 by A20,A22,Def13;
         then consider e being set such that
    A38:  e in the Edges of G & e orientedly_joins v1,v3 by A32,Th24;
        reconsider pe= <*e*> as (oriented Chain of G) by A38,Th5;
        reconsider p=<*1,j*> as FinSequence of NAT;
        take p,pe;
    A39: p.1=1 & len p = 2 by FINSEQ_1:61;
    then A40: p.(len p)=j by FINSEQ_1:61;
          now let k;
           assume A41: 1 <= k & k < len p;
           then k < 1+1 by FINSEQ_1:61;
           then k <= 1 by NAT_1:38;
       then k=1 by A41,AXIOMS:21;
           hence p.(len p-k)=h.(n+p/.(len p-k+1)) by A37,A39,A40,FINSEQ_4:24;
        end;
    then A42: p is_vertex_seq_at h,j,n by A40,Def17;
          p is one-to-one by A1,A15,FINSEQ_3:103;
        hence p is_simple_vertex_seq_at h,j,n by A39,A42,Def18;
        hereby let i;
          assume A43: 1<=i & i<len p;
            then i + 1 <= 1 + 1 by A39,INT_1:20;
            then i <= 1 by REAL_1:53;
            then i = 1 by A43,AXIOMS:21;
            hence p.i in UsedVx(h,n) by A5,A39,TARSKI:def 1;
        end;
    A44: len pe = 1 by FINSEQ_1:57;
    then A45: len p = len pe + 1 by FINSEQ_1:61;
          now let k;
           assume 1<=k & k<=len pe;
       then A46: k=1 by A44,AXIOMS:21;
          hence (the Source of G).(pe.k)=(the Source of G).e by FINSEQ_1:57
          .= p.k by A1,A38,A39,A46,GRAPH_4:def 1;
          thus (the Target of G).(pe.k)=(the Target of G).e by A46,FINSEQ_1:57
          .= p.(k+1) by A15,A38,A39,A40,A46,GRAPH_4:def 1;
        end;
        hence pe is_oriented_edge_seq_of p by A45,Def19;
        thus pe is_shortestpath_of v1,v3,UsedVx(h,n),W by A1,A5,A15,A38,Th14;
        thus cost(pe,W)=W.(pe.1) by A10,A44,Th4
        .=W.e by FINSEQ_1:57
        .=h.(2*n+j) by A8,A32,A36,A38,Th26;
        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 A1,A5,TARSKI:def 1;
         hence pe islongestInShortestpath UsedVx(h,n),v1,W
           by GRAPH_5:def 19;
     end;
     set nk=n+1;
A47:  1 < nk & nk <= 2*n & nk < mi by A1,Lm13;
A48:  n < nk by NAT_1:38;
A49:  nk in dom f by A3,A47,FINSEQ_3:27;
then A50:  nk in dom f0 by Th22;
       M.f0.1=-1 by A4,A6,Th20;
     then not M.f0 hasBetterPathAt n,1 by Def13;
     then not M.f0 hasBetterPathAt n,nk-'n by BINARITH:39;
then A51:  h.nk=M.f0.nk by A7,A8,A47,A48,A49,Def14
     .=f0.nk by A47,A48,A50,Th32
     .=0 by A3,Th22;
     hereby let m,j;
       assume A52: h.(n+j) = -1 & 1<=j & j <= n & m in UsedVx(h,n);
         set nj=n+j;
           nj <= n+n by A52,REAL_1:55;
    then A53:  nj <= 2*n by XCMPLX_1:11;
    then A54:  nj < mi by A13,AXIOMS:22;
           1+1 <= nj by A1,A52,REAL_1:55;
    then 1 < nj by NAT_1:38;
    then A55:  nj in dom f by A3,A54,FINSEQ_3:27;
    A56:  nj -' n=j by BINARITH:39;
           n+1 <= nj by A52,REAL_1:55;
    then A57:  n < nj by NAT_1:38;
         set m2=2*n+j;
    A58:  m2 <= 3*n by A14,A52,REAL_1:55;
           2*n+1 <= m2 by A52,REAL_1:55;
    then A59:  2*n < m2 by NAT_1:38;
           3*n < mi by Lm7;
    then A60:  m2 < mi by A58,AXIOMS:22;
           2 < m2 by A11,A59,AXIOMS:22;
    then A61:  1 < m2 by AXIOMS:22;
    A62:  mi in dom f by A2,A3,FINSEQ_3:27;
    then A63:  M.f0/.mi = M.f0.mi by A7,FINSEQ_4:def 4
         .=1 by A6,A60,A61,A62,Th18;
    then A64:  not M.f0 hasBetterPathAt n,(nj-'n) by A7,A8,A52,A53,A55,A57,
Def14
;
         A65: n < mi by Lm7;
    then A66:  j < mi by A52,AXIOMS:22;
    A67:  j <> 1 by A51,A52;
           j in dom f by A3,A52,A66,FINSEQ_3:27;
    then A68:  M.f0.j=f.j by A6,A52,A65,A67,Th19
         .=1 by A1,A52,Def20;
           M.f0.nj=-1 by A7,A8,A52,A53,A55,A57,A64,Def14;
    then A69:  not M.f0/.(2*n+n*(M.f0/.mi)+j) >= 0 by A56,A64,A68,Def13;
         set m3=2*n+n*1+j;
           m3 = 2*n+(n*1+j) by XCMPLX_1:1;
         then 2 <= m3 by A11,NAT_1:37;
    then A70:  1 < m3 by AXIOMS:22;
    A71:  m3=(1+2)*n+j by XCMPLX_1:8;
           j <= n*n by A12,A52,AXIOMS:22;
         then m3 <= 3*n + n*n by A71,REAL_1:55;
    then A72:  m3 < mi by NAT_1:38;
    then A73:  m3 in dom f by A3,A70,FINSEQ_3:27;
         reconsider v2=j as Vertex of G by A9,A52,FINSEQ_1:3;
    A74:  M.f0/.(2*n+n*(M.f0/.mi)+j)=M.f0.m3 by A7,A63,A73,FINSEQ_4:def 4;
       M.f0.m3=f.m3 by A6,A70,A72,A73,Th19
         .=Weight(v1,v2,W) by A1,Def20;
         then not ex e be set st e in the Edges of G & e orientedly_joins v1,
v2
         by A69,A74,Th24;
    then A75:  Weight(v1,v2,W)=-1 by Def7;
           m=1 by A5,A52,TARSKI:def 1;
         hence f.(2*n+n*m+j) = -1 by A1,A75,Def20;
    end;
    let m;
    assume m in UsedVx(h,n);
    then m=1 by A5,TARSKI:def 1;
    hence h.(n+m) <> -1 by A51;
end;

Lm17:
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 A1: g=RF.k.f & h=RF.(k+1).f & OuterVx(g,n) <> {} & i in UsedVx(g,n)
      & len f= mi;
A2:  M.g= (g,mi):=(Ak,-1) by Def11;
A3:  h=R.(M.g) by A1,Th23
     .=Relax(M.g,n) by Def15;
A4:  Ak<=n & g.Ak <> -1 by A1,Th30;
       i in {j: j in dom g & 1 <= j & j <= n & g.j = -1} by A1,Def9;
         then consider j such that
A5:  i=j & j in dom g & 1 <= j & j <= n & g.j = -1;
     set ni=n+i;
       ni <= n+n by A5,REAL_1:55;
then A6:  ni <= 2*n by XCMPLX_1:11;
A7:  ni -' n=i by BINARITH:39;
       n+1 <= ni by A5,REAL_1:55;
then A8:  n < ni by NAT_1:38;
     A9: n < mi by Lm7;
     A10: 2*n < mi by Lm7;
then A11:  ni < mi by A6,AXIOMS:22;
       1 <= ni by A5,NAT_1:37;
     then ni in dom f by A1,A11,FINSEQ_3:27;
then A12:  ni in dom g by A1,Th42;
then A13:  ni in dom (M.g) by Th34;
       now
        assume M.g hasBetterPathAt n,i;
        then M.g.i<>-1 by Def13;
        hence contradiction by A2,A4,A5,A9,Th19;
     end;
     hence h.ni=M.g.ni by A3,A6,A7,A8,A13,Def14
     .=g.ni by A2,A4,A6,A8,A10,A12,Th19;
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,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 A1: g=RT.k.f & h=RT.(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));
then A2: (p.1=1 & len p > 1 & p is_vertex_seq_at g,j,n) & p is one-to-one
    by Def18;
then A3:  p.(len p)=j by Def17;
       now let k;
        assume A4:1<=k & k < len p;
        then k - k < len p - k by REAL_1:92;
    then A5: 0 < len p - k by XCMPLX_1:14;
        then reconsider m=len p - k as Nat by INT_1:16;
    A6: 1+0 < m + 1 by A5,REAL_1:67;
          m <= len p - 1 by A4,REAL_1:92;
        then m +1 <= len p-1+1 by REAL_1:55;
        then m +1 <= len p+1-1 by XCMPLX_1:29;
    then A7: m+1 <= len p by XCMPLX_1:26;
    then A8: p/.(m+1)=p.(m+1) by A6,FINSEQ_4:24;
        per cases;
        suppose m+1=len p;
           hence p.(len p-k)=h.(n+p/.(len p-k+1)) by A1,A2,A3,A4,A8,Def17;
        suppose m+1<>len p;
            then m+1 < len p by A7,REAL_1:def 5;
        then A9: p/.(m+1) in UsedVx(g,n) by A1,A6,A8;
           thus p.(len p-k)=g.(n+p/.(len p-k+1)) by A2,A4,Def17
           .=h.(n+p/.(len p-k+1)) by A1,A9,Lm17;
     end;
     then p is_vertex_seq_at h,j,n by A3,Def17;
     hence thesis by A2,Def18;
end;

Lm19:
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
p^<*j*> is_simple_vertex_seq_at h,j,n
proof
     set RT=repeat(Relax(n)*findmin(n));
     assume A1: g=RT.k.f & h=RT.(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));
then A2: (p.1=1 & len p > 1 & p is_vertex_seq_at g,m,n) & p is one-to-one
     by Def18;
then A3:  p.(len p)=m by Def17;
     set q=p^<*j*>;
A4:  len q=len p+ 1 by FINSEQ_2:19;
then A5:  len q > 1 by A2,NAT_1:38;
A6:  q.1=1 by A2,Lm1;
A7:  q.(len q)=j by A4,FINSEQ_1:59;
       now let ii be Nat;
        assume A8:1<=ii & ii < len q;
        then ii - ii < len q - ii by REAL_1:92;
    then A9: 0 < len q - ii by XCMPLX_1:14;
        then reconsider mm=len q - ii as Nat by INT_1:16;
    A10: 1+0 < mm + 1 by A9,REAL_1:67;
          mm <= len q - 1 by A8,REAL_1:92;
        then mm +1 <= len q-1+1 by REAL_1:55;
        then mm +1 <= len q+1-1 by XCMPLX_1:29;
    then A11: mm+1 <= len q by XCMPLX_1:26;
    then A12: q/.(mm+1)=q.(mm+1) by A10,FINSEQ_4:24;
        per cases;
        suppose A13: mm+1=len q;
           then mm=len p by A4,XCMPLX_1:2;
           hence q.(len q-ii)=h.(n+q/.(len q-ii+1))
             by A1,A2,A3,A7,A12,A13,Lm1;
        suppose mm+1<>len q;
            then A14: mm+1 < len q by A11,REAL_1:def 5;
        then A15: mm < len p by A4,REAL_1:55;
        A16: mm+1 <= len p by A4,A14,INT_1:20;
              1+0 <= mm by A9,INT_1:20;
        then A17: q.(len q-ii)=p.mm by A15,Lm1;
            hereby
               per cases;
               suppose A18: mm+1=len p;
                 then mm+1=len p-1+1 by XCMPLX_1:27;
           then A19:   mm=len p-1 by XCMPLX_1:2;
           A20:   p/.(len p-1+1)=p/.len p by XCMPLX_1:27
                 .=m by A2,A3,FINSEQ_4:24;
               q/.(len q-ii+1)=m by A2,A3,A12,A18,Lm1;
                hence q.(len q-ii)=h.(n+q/.(len q-ii+1)) by A1,A2,A17,A19,A20,
Def17;
               suppose mm+1<>len p;
           then A21:  mm+1 < len p by A16,REAL_1:def 5;
           A22:  p/.(mm+1)=p.(mm+1) by A10,A16,FINSEQ_4:24;
           then A23:  p/.(mm+1) in UsedVx(g,n) by A1,A10,A21;
                set i2=ii-1;
           A24:  mm=len p+(1-ii) by A4,XCMPLX_1:29
                .=len p-i2 by XCMPLX_1:38;
           A25:  now assume i2 <= 1;
                   then len p - 1 <= len p -i2 by REAL_1:92;
                   hence contradiction by A21,A24,REAL_1:86;
                 end;
           A26:  q/.(len q-ii+1)= q.(mm+1) by A10,A11,FINSEQ_4:24
                 .=p/.(mm+1) by A10,A16,A22,Lm1;
                   i2 > 0 by A25,AXIOMS:22;
                 then reconsider i3=i2 as Nat by INT_1:16;
                   i2 < len q -1 by A8,REAL_1:92;
                 then i2 < len p by A4,XCMPLX_1:26;
                 hence q.(len q-ii)
                 = g.(n+p/.(len p-i3+1)) by A2,A17,A24,A25,Def17
                 .=h.(n+q/.(len q-ii+1)) by A1,A23,A24,A26,Lm17;
           end;
     end;
then A27:  q is_vertex_seq_at h,j,n by A7,Def17;
       now assume j in rng p;
          then consider i such that
     A28:  i in dom p & j = p.i by FINSEQ_2:11;
     A29:  1<=i & i <= len p by A28,FINSEQ_3:27;
          per cases;
          suppose i = len p;
          hence contradiction by A1,A2,A28,Def17;
          suppose i <> len p;
             then i < len p by A29,REAL_1:def 5;
          hence contradiction by A1,A28,A29;
    end;
    then q is one-to-one by A2,Th1;
    hence thesis by A5,A6,A27,Def18;
end;

Lm20:
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 A1: 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);
    assume A2:g.(n+i)=-1;
       P is_orientedpath_of v1,v2,V by A1,GRAPH_5:def 18;
     then consider q being Simple(oriented Chain of G) such that
A3:  q is_shortestpath_of v1,v2,V,W by A1,GRAPH_5:66;
       q is_orientedpath_of v1,v2,V by A3,GRAPH_5:def 18;
then A4:  q is_orientedpath_of v1,v2 & vertices(q) \ {v2} c= V by GRAPH_5:def 4
;
     set FT=the Target of G;
A5:  q <> {} & FT.(q.(len q))= v2 by A4,GRAPH_5:def 3;
     consider vs being FinSequence of the Vertices of G such that
A6:  vs is_oriented_vertex_seq_of q &
     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;
A7:  len vs = len q + 1 & for n1 be Nat st 1<=n1 & n1<=len q holds
     q.n1 orientedly_joins vs/.n1, vs/.(n1+1) by A6,GRAPH_4:def 5;
A8:  len q >= 1 by A5,GRAPH_5:8;
     set e=q.len q;
A9:  e orientedly_joins vs/.len q, vs/.(len q+1) by A6,A8,GRAPH_4:def 5;
       len q in dom q by A8,FINSEQ_3:27;
then A10:  e in the Edges of G by FINSEQ_2:13;
A11:  len q < len vs by A7,NAT_1:38;
A12:  1 < len q+1 by A8,NAT_1:38;
A13:  vs/.len q=vs.len q by A8,A11,FINSEQ_4:24;
     then reconsider v3=vs.len q as Vertex of G;
A14:  v2=vs/.(len q+1) by A5,A9,GRAPH_4:def 1;
then A15:  v2=vs.len vs by A7,A12,FINSEQ_4:24;
A16:  now
        assume A17: v3=v2;
     A18: q.1 orientedly_joins vs/.1, vs/.(1+1) by A6,A8,GRAPH_4:def 5;
           v1 =(the Source of G).(q.1) by A4,GRAPH_5:def 3
         .=vs/.1 by A18,GRAPH_4:def 1
         .=vs.1 by A7,A12,FINSEQ_4:24
         .=v3 by A6,A8,A11,A15,A17;
         hence contradiction by A1,A17;
      end;
A19:  Seg n=the Vertices of G by A1,Def20;
       len q in dom vs by A8,A11,FINSEQ_3:27;
     then v3 in Seg n by A19,FINSEQ_2:13;
     then reconsider m=v3 as Nat;
A20:  f.(2*n+n*m+i)=Weight(v3,v2,W) by A1,Def20;
A21:  not v3 in {v2} by A16,TARSKI:def 1;
       v3=(the Source of G).e by A9,A13,GRAPH_4:def 1;
     then v3 in vertices(q) by A8,Lm4;
     then m in (vertices(q) \ {v2}) by A21,XBOOLE_0:def 4;
     then f.(2*n+n*m+i)=-1 by A1,A2,A4;
     hence contradiction by A9,A10,A13,A14,A20,Th24;
end;

Lm21:
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) <> {} & k >=1 &
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 A1: f is_Input_of_Dijkstra_Alg G,n,W & v1=1 & n >= 1 &
    g=(repeat(R*M)).k.f & h=(repeat(R*M)).(k+1).f & IN <> {} & k >=1 &
    1 in Ug;
    assume A2: 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 A3: (for m,j st g.(n+j) = -1 & 1<=j & j<=n & m in Ug holds
      f.(2*n+n*m+j) = -1) & (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);
A4:  1 <= mi by NAT_1:37;
A5:  len f=mi by A1,Def20;
A6:  M.g= (g,mi):=(Ak,-1) by Def11;
A7:  dom (M.g) = dom g by Th34;
   h=R.(M.g) by A1,Th23;
then A8:  h=Relax(M.g,n) by Def15;
A9:  Seg n=the Vertices of G by A1,Def20;
     then reconsider VG=the Vertices of G as non empty Subset of NAT by A1,
FINSEQ_1:3;
A10:  W is_weight>=0of G by GRAPH_5:def 13;
then A11:  W is_weight_of G by GRAPH_5:50;
A12:  2*n+n=2*n+1*n
     .=(2+1)*n by XCMPLX_1:8;
A13:  dom f=dom g by A1,Th42;
A14:  Ak in dom g & 1<=Ak & Ak<=n & g.Ak <> -1 & g.(n+Ak) <> -1 by A1,Th30;
     set Uh=UsedVx(h,n);
A15:  Uh=Ug \/ {Ak} & not Ak in Ug by A1,Th40;
then A16:  Ug c= Uh by XBOOLE_1:7;
A17:  n < mi by Lm7;
A18:  dom f=dom h by A1,Th42;
     reconsider vk=Ak as Vertex of G by A9,A14,FINSEQ_1:3;
     consider pk being FinSequence of NAT,PK be oriented Chain of G such that
A19:  pk is_simple_vertex_seq_at g,Ak,n & (for i st 1<=i & i<len pk holds
     pk.i in Ug) & PK is_oriented_edge_seq_of pk & PK is_shortestpath_of
     v1,vk,Ug,W & cost(PK,W)=g.(2*n+Ak) & (not vk in Ug implies PK
     islongestInShortestpath Ug,v1,W) by A1,A2,A14,A15;
     consider kk being Nat such that
A20:  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 A1,Def10;
     set nAk=2*n+Ak;
A21: 1 < nAk & nAk < mi & Ak < nAk by A14,Lm12;
then A22: nAk in dom g by A5,A13,FINSEQ_3:27;
     A23: f,g equal_at 3*n+1,n*n+3*n by A1,Th47;
       PK is_orientedpath_of v1,vk,Ug by A19,GRAPH_5:def 18;
then A24: PK is_orientedpath_of v1,vk by GRAPH_5:def 4;
     then PK <> {} by GRAPH_5:def 3;
then A25: len PK >= 1 by GRAPH_5:8;
A26:  mi in dom g by A4,A5,A13,FINSEQ_3:27;
then A27:  M.g/.mi = M.g.mi by A7,FINSEQ_4:def 4
    .=Ak by A6,A14,A17,A26,Th18;
A28: M.g/.nAk=M.g.nAk by A7,A22,FINSEQ_4:def 4
     .=cost(PK,W) by A6,A19,A21,A22,Th19;
     set nk=n+Ak;
A29:  1 < nk & nk <= 2*n & nk < mi by A14,Lm13;
       n+1 <= nk by A14,REAL_1:55;
then A30:  n < nk by NAT_1:38;
A31:  nk in dom g by A5,A13,A29,FINSEQ_3:27;
then A32:  M.g.nk=g.nk by A29,A30,Th32;
       now
        set Wke=M.g/.(2*n+n*(M.g/.mi)+Ak);
         assume M.g hasBetterPathAt n,Ak;
     then A33: (M.g.nk=-1 or M.g/.nAk > newpathcost(M.g,n,Ak)) & Wke >= 0 by
Def13;
         then M.g/.nAk+Wke >= M.g/.nAk+0 by REAL_1:55;
         hence contradiction by A1,A27,A32,A33,Def12,Th30;
     end;
     then not M.g hasBetterPathAt n,nk-'n by BINARITH:39;
then A34: h.nk=g.nk by A7,A8,A29,A30,A31,A32,Def14;
    hereby let v3,j;
    assume A35: v3<>v1 & v3=j & h.(n+j)<>-1;
         set nj=n+j;
           j in VG by A35;
    then A36:  1<=j & j <= n by A9,FINSEQ_1:3;
    then A37:  1 < nj & nj <= 2*n & nj < mi by Lm13;
    then A38:  nj in dom g by A5,A13,FINSEQ_3:27;
    A39:  nj -' n=j by BINARITH:39;
           n+1 <= nj by A36,REAL_1:55;
    then A40:  n < nj by NAT_1:38;
         set m2=2*n+j;
    A41:  m2 <= 3*n by A12,A36,REAL_1:55;
           2*n+1 <= m2 by A36,REAL_1:55;
    then A42:  2*n < m2 by NAT_1:38;
    A43:  m2 -' 2*n = j by BINARITH:39;
    A44:  1 < m2 & m2 < mi by A36,Lm12;
    then A45:  m2 in dom g by A5,A13,FINSEQ_3:27;
    A46:  m2 in dom (M.g) by A5,A7,A13,A44,FINSEQ_3:27;
    A47:  M.g.nj = g.nj by A6,A14,A37,A38,A40,Th19;
           n <= 2*n by Lm6;
         then n < m2 by A42,AXIOMS:22;
    then A48:  M.g.m2 = g.m2 by A6,A14,A44,A45,Th19;
   A49:  j < mi by A17,A36,AXIOMS:22;
   then A50:  j in dom g by A5,A13,A36,FINSEQ_3:27;
    A51:  j in dom h by A5,A18,A36,A49,FINSEQ_3:27;
         set Akj=2*n+n*Ak+j;
    A52:  1 < Akj & Ak < Akj & Akj < mi by A14,A36,Lm14;
    then A53:  Akj in dom g by A5,A13,FINSEQ_3:27;
    A54:  3*n+1 <=Akj & Akj <= n*n+3*n by A14,A36,Lm15;
    A55:  M.g/.(2*n+n*(M.g/.mi)+j)=M.g.Akj by A7,A27,A53,FINSEQ_4:def 4
         .=g.Akj by A6,A52,A53,Th19
         .=f.Akj by A13,A23,A53,A54,Def16
        .=Weight(vk,v3,W) by A1,A35,Def20;
    A56:  M.g/.m2 = g.m2 by A7,A45,A48,FINSEQ_4:def 4;
         per cases;
         suppose A57: not M.g hasBetterPathAt n,(nj-'n);
       then A58: h.nj=g.nj by A7,A8,A37,A38,A40,A47,Def14;
           then consider p,P such that
       A59: 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 A2,A35;
           take p,P;
           thus p is_simple_vertex_seq_at h,j,n by A1,A5,A58,A59,Lm18;
           hereby let i;
              assume 1<=i & i<len p;
              then p.i in Ug by A59;
              hence p.i in Uh by A16;
           end;
           thus P is_oriented_edge_seq_of p by A59;
           hereby
             per cases;
             suppose M.g.j=-1;
               then Relax(M.g,n).j=-1 by A7,A36,A50,Def14;
               then j in {i: i in dom h & 1 <= i & i <= n & h.i = -1}
                 by A8,A36,A51;
               then j in Uh by Def9;
               then A60: j in Ug or j in {Ak} by A15,XBOOLE_0:def 2;
                 now let Q,v4;
                  assume A61:not v4 in Ug & Q is_shortestpath_of v1,v4,Ug,W;
              A62: v4 in VG;
                  then reconsider j4=v4 as Nat;
              A63: 1<=j4 & j4<=n by A9,A62,FINSEQ_1:3;
              then A64: g.(n+j4) <> -1 by A1,A3,A10,A61,Lm20;
                  then consider q,R such that
              A65: q is_simple_vertex_seq_at g,j4,n & (for i st 1<=i & i<len q
                  holds q.i in Ug) & R is_oriented_edge_seq_of q &
                  R is_shortestpath_of v1,v4,Ug,W & cost(R,W)=g.(2*n+j4) &
                  (not v4 in Ug implies R islongestInShortestpath Ug,v1,W)
                  by A1,A2,A61;
              A66: cost(R,W)=cost(Q,W) by A61,A65,Th9;
                  per cases by A60,TARSKI:def 1;
                  suppose j in Ug;
                     then consider PP being oriented Chain of G such that
                A67: PP is_shortestpath_of v1,v3,Ug,W & cost(PP,W) <= cost(R,W)
                    by A35,A61,A65,GRAPH_5:def 19;
                    thus cost(P,W) <= cost(Q,W) by A59,A66,A67,Th9;
                  suppose A68: j = Ak;
                      j4 <= mi by A17,A63,AXIOMS:22;
                then A69: j4 in dom g by A5,A13,A63,FINSEQ_3:27;
                      now assume g.j4=-1;
                      then j4 in {i: i in dom g & 1 <= i & i <= n & g.i = -1}
                      by A63,A69;
                      hence contradiction by A61,Def9;
                    end;
                    then j4 in {i: i in dom g & 1 <= i & i <= n & g.i <> -1 &
                    g.(n+i) <> -1} by A63,A64,A69;
                    then j4 in IN by Def3;
                then A70: g/.(2*n+Ak) <= g/.(2*n+j4) by A20;
                A71: g/.(2*n+Ak) = g.(2*n+Ak) by A22,FINSEQ_4:def 4;
                      1 < 2*n+j4 & 2*n+j4 < mi by A63,Lm12;
                    then 2*n+j4 in dom g by A5,A13,FINSEQ_3:27;
                    hence cost(P,W) <= cost(Q,W)
                      by A59,A65,A66,A68,A70,A71,FINSEQ_4:def 4;
               end;
               hence P is_shortestpath_of v1,v3,Uh,W
               by A10,A16,A35,A59,GRAPH_5:68;

            suppose A72: M.g.j <> -1;
               hereby
                 per cases;
                  suppose A73: M.g/.(2*n+n*(M.g/.mi)+j) >= 0;
             then A74:  M.g/.m2 <= newpathcost(M.g,n,j) by A39,A57,A72,Def13;
             A75:  M.g/.m2 = cost(P,W) by A46,A48,A59,FINSEQ_4:def 4;
             A76:  newpathcost(M.g,n,j)=M.g/.(2*n+M.g/.mi)
                    + M.g/.(2*n+n*(M.g/.mi)+j) by Def12;
                  consider e be set such that
            A77:  e in the Edges of G & e orientedly_joins vk,v3 by A55,A73,
Th24;
                 reconsider pe= <*e*> as (oriented Chain of G) by A77,Th5;
            A78:  len pe = 1 & pe.1=e by FINSEQ_1:57;
                 then consider Q such that
            A79: Q=PK^pe & Q is_orientedpath_of v1,v3 by A24,A25,A77,GRAPH_5:37
;
                  cost(pe,W) = W.(pe.1) by A11,A78,Th4
                .=Weight(vk,v3,W) by A77,A78,Th26;
                then cost(Q,W)=newpathcost(M.g,n,j) by A11,A27,A28,A55,A76,A79,
GRAPH_5:58;
                hence P is_shortestpath_of v1,v3,Uh,W
                  by A1,A10,A15,A19,A25,A35,A59,A74,A75,A77,A79,GRAPH_5:69;

              suppose M.g/.(2*n+n*(M.g/.mi)+j) < 0;
               then not ex e be set st e in the Edges of G &
                e orientedly_joins vk,v3 by A55,Th24;
               hence P is_shortestpath_of v1,v3,Uh,W
                 by A1,A10,A15,A19,A35,A59,Th13;
             end;
           end;
           thus cost(P,W)=h.m2 by A8,A39,A41,A42,A43,A46,A48,A57,A59,Def14;
           hereby
              assume A80: not v3 in Uh;
         then A81:  not v3 in Ug by A15,XBOOLE_0:def 2;
                now let v2;
                  assume A82:v2 in Uh & v2 <> v1;
                   per cases by A15,A82,XBOOLE_0:def 2;
                 suppose v2 in {Ak};
               then A83: v2 = vk by TARSKI:def 1;
                   take PK;
                  thus PK is_shortestpath_of v1,v2,Uh,W by A15,A19,A83,Th8;
                 now assume g.j = -1;
                     then j in {i: i in dom g & 1 <= i & i <= n & g.i = -1}
                     by A36,A50;
                     hence contradiction by A35,A81,Def9;
                   end;
                  then j in {i: i in dom g & 1 <= i & i <= n & g.i <> -1 &
                    g.(n+i) <> -1} by A35,A36,A50,A58;
                  then j in IN by Def3;
              then A84: g/.nAk <= g/.m2 by A20;
                    g/.nAk=cost(PK,W) by A19,A22,FINSEQ_4:def 4;
                  hence cost(PK,W) <= cost(P,W) by A45,A59,A84,FINSEQ_4:def 4;
                 suppose A85: v2 in Ug;
                   then consider Q such that
               A86: Q is_shortestpath_of v1,v2,Ug,W & cost(Q,W) <= cost(P,W)
                   by A15,A59,A80,A82,GRAPH_5:def 19,XBOOLE_0:def 2;
               A87: now let R,v4;
                    assume A88: not v4 in Ug & R is_shortestpath_of v1,v4,Ug,W;
                      A89: v4 in VG;
                      then reconsider j4=v4 as Nat;
                        1<=j4 & j4<=n by A9,A89,FINSEQ_1:3;
                  then g.(n+j4) <> -1 by A1,A3,A10,A88,Lm20;
                      then consider rn being FinSequence of NAT,RR
                      be oriented Chain of G such that
                  A90: rn is_simple_vertex_seq_at g,j4,n & (for i st 1<=i &
                      i<len rn holds rn.i in Ug) & RR is_oriented_edge_seq_of
                      rn & RR is_shortestpath_of v1,v4,Ug,W & cost(RR,W)
                      =g.(2*n+j4) & (not v4 in Ug implies
                      RR islongestInShortestpath Ug,v1,W) by A1,A2,A88;
                      consider QQ being oriented Chain of G such that
                  A91: QQ is_shortestpath_of v1,v2,Ug,W &
                      cost(QQ,W) <= cost(RR,W) by A82,A85,A88,A90,GRAPH_5:def
19;
                        cost(QQ,W)= cost(Q,W) by A86,A91,Th9;
                     hence cost(Q,W) <= cost(R,W) by A88,A90,A91,Th9;
                  end;
                  take Q;
                  thus Q is_shortestpath_of v1,v2,Uh,W
                  by A10,A16,A82,A86,A87,GRAPH_5:68;
                  thus cost(Q,W) <= cost(P,W) by A86;
             end;
             hence P islongestInShortestpath Uh,v1,W by GRAPH_5:def 19;
          end;

        suppose A92: M.g hasBetterPathAt n,(nj-'n);
           then A93: Relax(M.g,n).nj=Ak by A7,A27,A37,A38,A40,Def14;
      A94:  (M.g.nj=-1 or M.g/.m2 > newpathcost(M.g,n,j)) &
           M.g/.(2*n+n*(M.g/.mi)+j) >= 0 & M.g.j <> -1 by A39,A92,Def13;
      A95:  newpathcost(M.g,n,j)
           =M.g/.nAk+Weight(vk,v3,W) by A27,A55,Def12;
      A96:  now assume A97: Ak = j;
                then A98: M.g.nj <> -1 by A6,A14,A37,A38,A40,Th19;
                  M.g/.m2+Weight(vk,v3,W) >= M.g/.m2+0 by A55,A94,REAL_1:55;
                hence contradiction by A39,A92,A95,A97,A98,Def13;
           end;
      A99:   now assume j in UsedVx(g,n);
               then j in {i: i in dom g & 1 <= i & i <= n & g.i = -1} by Def9;
               then consider i such that
           A100: j=i & i in dom g & 1 <= i & i <= n & g.i = -1;
               thus contradiction by A17,A94,A100,Th33;
            end;
           consider e being set such that
      A101:  e in the Edges of G & e orientedly_joins vk,v3 by A55,A94,Th24;
           reconsider pe= <*e*> as (oriented Chain of G) by A101,Th5;
      A102:  len pe = 1 & pe.1=e by FINSEQ_1:57;
           then consider Q such that
      A103:  Q=PK^pe & Q is_orientedpath_of v1,v3 by A24,A25,A101,GRAPH_5:37;
           take q=pk^<*j*>,Q;
           thus q is_simple_vertex_seq_at h,j,n by A1,A5,A8,A19,A34,A93,A96,A99
,Lm19;
      A104:  len pk > 1 & pk is_vertex_seq_at g,Ak,n by A19,Def18;
      then A105:  q.len pk=pk.len pk by Lm1
           .= Ak by A104,Def17;
           hereby
              let i;
              assume A106: 1<=i & i<len q;
              then i < len pk +1 by FINSEQ_2:19;
          then A107: i <= len pk by NAT_1:38;
                now per cases;
                suppose i=len pk;
                  hence q.i in {Ak} or q.i in Ug by A105,TARSKI:def 1;
                suppose i<>len pk;
              then A108: i < len pk by A107,REAL_1:def 5;
                    q.i=pk.i by A106,A107,Lm1;
                  hence q.i in {Ak} or q.i in Ug by A19,A106,A108;
              end;
              hence q.i in Uh by A15,XBOOLE_0:def 2;
           end;
       A109: len Q =len PK+1 by A102,A103,FINSEQ_1:35;
       A110: len pk=len PK+1 by A19,Def19;
       then A111: len q=len Q + 1 by A109,FINSEQ_2:19;
           set FS=the Source of G,
               FT=the Target of G;
              now let i;
                 assume A112: 1<=i & i<=len Q;
                 per cases;
                 suppose A113: i=len Q;
                 then A114: Q.i=e by A102,A103,A109,Lm2;
              then A115: FS.(Q.i)= vk & FT.(Q.i) = v3 by A101,GRAPH_4:def 1;
                 thus FS.(Q.i)=q.i by A101,A105,A109,A110,A113,A114,GRAPH_4:def
1;
                 thus FT.(Q.i) = q.(i+1) by A35,A109,A110,A113,A115,FINSEQ_1:59
;
                 suppose i<>len Q;
                 then A116: i < len Q by A112,REAL_1:def 5;
             then A117: i <= len PK by A109,NAT_1:38;
             then A118: FS.(PK.i) = pk.i & FT.(PK.i) = pk.(i+1) by A19,A112,
Def19;
             A119: Q.i=PK.i by A103,A112,A117,Lm1;
             A120: i+1 <= len pk by A109,A110,A116,NAT_1:38;
                 thus FS.(Q.i) = q.i by A109,A110,A112,A118,A119,Lm1;
                   1 <= i+1 by NAT_1:37;
                 hence FT.(Q.i)=q.(i+1) by A118,A119,A120,Lm1;
           end;
           hence Q is_oriented_edge_seq_of q by A111,Def19;
      A121:  cost(PK,W)+cost(pe,W)=cost(Q,W) by A11,A103,GRAPH_5:58;
           A122: cost(pe,W) = W.(pe.1) by A11,A102,Th4
           .=Weight(vk,v3,W) by A101,A102,Th26;
      then A123:  newpathcost(M.g,n,j)=cost(Q,W) by A27,A28,A55,A121,Def12;
           hereby
               per cases;
               suppose A124: g.nj=-1;
                 now let v2;
                    assume A125: v2 in Ug;
                    then reconsider m=v2 as Nat;
                      -1= f.(2*n+n*m+j) by A3,A36,A124,A125
                    .=Weight(v2,v3,W) by A1,A35,Def20;
                    hence not ex e be set st e in the Edges of G &
                    e orientedly_joins v2,v3 by Th24;
                end;
                hence Q is_shortestpath_of v1,v3,Uh,W
                  by A1,A15,A19,A35,A101,A103,Th15;

               suppose A126: g.nj <> -1;
                 then consider p,P such that
             A127: 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 A2,A35;
                  thus Q is_shortestpath_of v1,v3,Uh,W by A1,A6,A10,A14,A15,A19
,A25,A28,A35,A37,A38,A40,A56,A94,A95,A101,A103,A121,A122,A126,A127,Th19,GRAPH_5
:69;
           end;
           thus cost(Q,W)=h.m2 by A8,A39,A41,A42,A43,A46,A92,A123,Def14;
             0 <= cost(pe,W) by A10,GRAPH_5:54;
      then A128:  cost(PK,W)+0 <= cost(Q,W) by A121,REAL_1:55;
           hereby
              assume not v3 in Uh;
                now let v2;
                  assume A129:v2 in Uh & v2 <> v1;
                   per cases by A15,A129,XBOOLE_0:def 2;
                 suppose v2 in {Ak};
              then A130:  v2 = Ak by TARSKI:def 1;
                   take PK;
                  thus PK is_shortestpath_of v1,v2,Uh,W by A15,A19,A130,Th8;
                  thus cost(PK,W) <= cost(Q,W) by A128;
                 suppose A131: v2 in Ug;
                   then consider P such that
               A132: P is_shortestpath_of v1,v2,Ug,W & cost(P,W) <= cost(PK,W)
                   by A1,A19,A129,Th40,GRAPH_5:def 19;
               A133: now let R,v4;
                    assume A134: not v4 in Ug & R is_shortestpath_of v1,v4,Ug,W
;
                      A135: v4 in VG;
                      then reconsider j4=v4 as Nat;
                        1<=j4 & j4<=n by A9,A135,FINSEQ_1:3;
                  then g.(n+j4) <> -1 by A1,A3,A10,A134,Lm20;
                      then consider rn being FinSequence of NAT,RR
                      be oriented Chain of G such that
                  A136: rn is_simple_vertex_seq_at g,j4,n & (for i st 1<=i &
                      i<len rn holds rn.i in Ug) & RR is_oriented_edge_seq_of
                      rn & RR is_shortestpath_of v1,v4,Ug,W & cost(RR,W)
                      =g.(2*n+j4) & (not v4 in Ug implies
                      RR islongestInShortestpath Ug,v1,W) by A1,A2,A134;
                      consider PP being oriented Chain of G such that
                  A137: PP is_shortestpath_of v1,v2,Ug,W &
                      cost(PP,W) <= cost(RR,W) by A129,A131,A134,A136,GRAPH_5:
def 19;
                        cost(PP,W)= cost(P,W) by A132,A137,Th9;
                     hence cost(P,W) <= cost(R,W) by A134,A136,A137,Th9;
                  end;
                  take P;
                  thus P is_shortestpath_of v1,v2,Uh,W
                  by A10,A16,A129,A132,A133,GRAPH_5:68;
                  thus cost(P,W) <= cost(Q,W) by A128,A132,AXIOMS:22;
              end;
              hence Q islongestInShortestpath Uh,v1,W by GRAPH_5:def 19;
          end;
    end;
    hereby let m,j;
       assume A138: h.(n+j) = -1 & 1<=j & j<=n & m in Uh;
       set nj=n+j;
  A139:  1 < nj & nj <= 2*n & nj < mi by A138,Lm13;
  then A140:  nj in dom g by A5,A13,FINSEQ_3:27;
         n+1 <= nj by A138,REAL_1:55;
  then A141:  n < nj by NAT_1:38;
  A142:  now
         assume M.g hasBetterPathAt n,nj-'n;
           then h.nj=Ak by A7,A8,A27,A139,A140,A141,Def14;
           hence contradiction by A138,NAT_1:18;
       end;
  A143:  M.g.nj=g.nj by A6,A14,A139,A140,A141,Th19;
  then A144:  g.nj=-1 by A7,A8,A138,A139,A140,A141,A142,Def14;
  then A145:  not j in Ug by A3;
     j < mi by A17,A138,AXIOMS:22;
  then A146:  j in dom g by A5,A13,A138,FINSEQ_3:27;
         now
           assume g.j=-1;
           then j in {i: i in dom g & 1 <= i & i <= n & g.i = -1} by A138,A146
;
           hence contradiction by A145,Def9;
        end;
  then A147:   M.g.j <> -1 by A6,A14,A17,A138,A144,A146,Th19;
          not M.g hasBetterPathAt n,j by A142,BINARITH:39;
  then A148:   M.g/.(2*n+n*(M.g/.mi)+j) < 0 by A143,A144,A147,Def13;
        reconsider v3=j as Vertex of G by A9,A138,FINSEQ_1:3;
        set Akj=2*n+n*Ak+j;
    A149:  1 < Akj & Ak < Akj & Akj < mi by A14,A138,Lm14;
    then A150:  Akj in dom g by A5,A13,FINSEQ_3:27;
    A151:  3*n+1 <=Akj & Akj <= n*n+3*n by A14,A138,Lm15;
    A152:  f.Akj=Weight(vk,v3,W) by A1,Def20;
    A153:  M.g/.(2*n+n*(M.g/.mi)+j)=M.g.Akj by A7,A27,A150,FINSEQ_4:def 4
         .=g.Akj by A6,A149,A150,Th19
         .=Weight(vk,v3,W) by A13,A23,A150,A151,A152,Def16;
         per cases by A15,A138,XBOOLE_0:def 2;
         suppose m in {Ak};
       then A154:  m=Ak by TARSKI:def 1;
              not ex e be set st e in the Edges of G & e orientedly_joins vk,v3
            by A148,A153,Th24;
            then Weight(vk,v3,W)=-1 by Def7;
            hence f.(2*n+n*m+j) = -1 by A1,A154,Def20;
         suppose m in Ug;
            hence f.(2*n+n*m+j) = -1 by A3,A138,A144;
    end;
    let m;
    assume A155: m in Uh;
    per cases by A15,A155,XBOOLE_0:def 2;
    suppose A156: m in Ug;
      then h.(n+m)=g.(n+m) by A1,A5,Lm17;
      hence h.(n+m) <> -1 by A3,A156;
    suppose m in {Ak};
      hence h.(n+m) <> -1 by A14,A34,TARSKI:def 1;
end;

theorem
  f is_Input_of_Dijkstra_Alg G,n,W & v1=1 & 1 <> v2 & v2=i & n >= 1 &
g=(DijkstraAlgorithm(n)).f implies the Vertices 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 A1: f is_Input_of_Dijkstra_Alg G,n,W & v1=1 & 1 <> v2 & v2=i &
        n >= 1 & g=(DijkstraAlgorithm(n)).f;
     set R=Relax(n),
         M=findmin(n),
         RM=repeat (R*M),
         cn=LifeSpan(R*M,f,n),
         mi=n*n+3*n+1;
A2:  g = while_do(R*M,n).f by A1,Def21
     .= RM.cn.f by Def5;
     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);
A3:  RM.0 .f = f by Th22;
A4:  Seg n=the Vertices of G by A1,Def20;
     then reconsider VG=the Vertices of G as non empty Subset of NAT by A1,
FINSEQ_1:3;
A5:  1 <= mi by NAT_1:37;
A6:  len f=mi & f.1=1 & f.(n+1) =0 & (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,Def20;
then A7:  1 in dom f by A5,FINSEQ_3:27;
then UsedVx(f,n)={} & {1} = UsedVx(RM.1.f,n) by A1,A6,Th48;
then A8:  1 in UsedVx(RM.1.f,n) by TARSKI:def 1;
A9:  P[0]
     proof
        assume 0 <= cn;
        set UV=UsedVx(RM.0 .f,n),
            h=RM.0 .f;
        hereby let v3,j;
          assume A10: v3<>v1 & v3=j & h.(n+j)<>-1;
          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));
            v3 in VG;
      then A11: 1<=j & j<=n by A4,A10,FINSEQ_1:3;
          then 1 < j by A1,A10,REAL_1:def 5;
          then 1+1 <= j by INT_1:20;
          hence contradiction by A1,A3,A10,A11,Def20;
        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 A1,A3,A6,A7,Th48;
        let m;
        assume A12: m in UsedVx(h,n);
        assume h.(n+m) = -1;
        thus contradiction by A1,A3,A6,A7,A12,Th48;
     end;
A13:  for k st P[k] holds P[k+1]
     proof
        let k;
        assume A14: P[k];
          now
          assume A15: k+1 <= cn;
      then A16: k < cn by NAT_1:38;
          set FK=RM.k.f;
          set FK1=RM.(k+1).f,
              UV1=UsedVx(FK1,n);
      A17: OuterVx(FK,n) <> {} by A16,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,Lm16;
          suppose k<>0;
                then k > 0 by NAT_1:19;
            then A18: k >= 1+0 by INT_1:20;
                then 1 in UsedVx(FK,n) by A8,A16,Th49;
           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,A14,A15,A17,A18,Lm21
,NAT_1:38;
       end;
       hence P[k+1];
     end;
     set Ug=UsedVx(g,n),
         Vg=UnusedVx(g,n);
     A19: for k holds P[k] from Ind(A9,A13);
A20:  VG c= Ug \/ Vg
     proof let x;
          assume A21: x in VG;
          then reconsider j=x as Nat;
     A22:  1 <= j & j <= n by A4,A21,FINSEQ_1:3;
            n < mi by Lm7;
          then j < mi by A22,AXIOMS:22;
          then j in dom f by A6,A22,FINSEQ_3:27;
     then A23:  j in dom g by A2,Th42;
          per cases;
          suppose g.j=-1;
            then j in {k: k in dom g & 1 <= k & k <= n & g.k = -1} by A22,A23;
            then x in Ug by Def9;
            hence x in Ug \/ Vg by XBOOLE_0:def 2;
          suppose g.j<>-1;
            then j in {k: k in dom g & 1 <= k & k <= n & g.k <> -1} by A22,A23
;
            then x in Vg by Def8;
            hence x in Ug \/ Vg by XBOOLE_0:def 2;
     end;
       Ug \/ Vg c= VG
     proof let x;
          assume A24: x in Ug \/ Vg;
          per cases by A24,XBOOLE_0:def 2;
          suppose x in Ug;
            then x in {k: k in dom g & 1 <= k & k <= n & g.k = -1} by Def9;
            then consider k such that
      A25:   x = k & k in dom g & 1 <= k & k <= n & g.k = -1;
           thus x in VG by A4,A25,FINSEQ_1:3;
          suppose x in Vg;
            then x in {k: k in dom g & 1 <= k & k <= n & g.k <> -1} by Def8;
            then consider k such that
      A26:   x = k & k in dom g & 1 <= k & k <= n & g.k <> -1;
            thus x in VG by A4,A26,FINSEQ_1:3;
     end;
     hence
A27:  the Vertices of G = Ug \/ Vg by A20,XBOOLE_0:def 10;
    consider ii being Nat such that
A28:  ii<=n & OuterVx(RM.ii.f,n) = {} by Th41;
A29:  OuterVx(g,n) = {} by A2,A28,Def4;
A30:  now let v3,v4;
        assume A31: v3 in Ug & v4 in Vg;
            v3 in VG;
          then reconsider m=v3 as Nat;
            v4 in {k: k in dom g & 1 <= k & k <= n & g.k <> -1} by A31,Def8;
          then consider j such that
      A32: v4 = j & j in dom g & 1 <= j & j <= n & g.j <> -1;
            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 A32;
             hence contradiction by A29,Def3;
          end;
          then -1=f.(2*n+n*m+j) by A2,A19,A31,A32
          .=Weight(v3,v4,W) by A1,A32,Def20;
          hence not ex e st e in the Edges of G &
                e orientedly_joins v3,v4 by Th24;
     end;
       now assume A33: cn=0;
         1 in {k: k in dom f & 1 <= k & k <= n &
       f.k <> -1 & f.(n+k) <> -1} by A1,A6,A7;
       hence contradiction by A2,A3,A29,A33,Def3;
     end;
     then cn > 0 by NAT_1:19;
     then cn >= 1+0 by INT_1:20;
then A34:  v1 in Ug by A1,A2,A8,Th49;
     hereby
        assume v2 in Ug;
        then g.(n+i) <> -1 by A1,A2,A19;
        then consider p,P such that
A35:    p is_simple_vertex_seq_at g,i,n & (for m st 1<=m & m<len p holds p.m
       in Ug) & P is_oriented_edge_seq_of p & P is_shortestpath_of v1,v2,Ug,W
       & cost(P,W)=g.(2*n+i) & (not v2 in Ug implies P
       islongestInShortestpath Ug,v1,W ) by A1,A2,A19;
       take p,P;
       thus p is_simple_vertex_seq_at g,i,n by A35;
       thus P is_oriented_edge_seq_of p by A35;
       thus P is_shortestpath_of v1,v2,W by A27,A30,A34,A35,Th16;
       thus cost(P,W)=g.(2*n+i) by A35;
     end;
     thus thesis by A27,A30,A34,Th11;
end;

Back to top