:: by Jing-Chao Chen

::

:: Received March 17, 2003

:: Copyright (c) 2003-2017 Association of Mizar Users

theorem Th1: :: GRAPHSP:1

for p being FinSequence

for x being set holds

( ( not x in rng p & p is one-to-one ) iff p ^ <*x*> is one-to-one )

for x being set holds

( ( not x in rng p & p is one-to-one ) iff p ^ <*x*> is one-to-one )

proof end;

theorem Th2: :: GRAPHSP:2

for X being set

for p being FinSequence of X

for ii being Integer st 1 <= ii & ii <= len p holds

p . ii in X

for p being FinSequence of X

for ii being Integer st 1 <= ii & ii <= len p holds

p . ii in X

proof end;

theorem Th3: :: GRAPHSP:3

for X being set

for p being FinSequence of X

for ii being Integer st 1 <= ii & ii <= len p holds

p /. ii = p . ii

for p being FinSequence of X

for ii being Integer st 1 <= ii & ii <= len p holds

p /. ii = p . ii

proof end;

theorem Th4: :: GRAPHSP:4

for G being Graph

for pe being FinSequence of the carrier' of G

for W being Function st W is_weight_of G & len pe = 1 holds

cost (pe,W) = W . (pe . 1)

for pe being FinSequence of the carrier' of G

for W being Function st W is_weight_of G & len pe = 1 holds

cost (pe,W) = W . (pe . 1)

proof end;

theorem Th5: :: GRAPHSP:5

for G being Graph

for e being set st e in the carrier' of G holds

<*e*> is oriented Simple Chain of G

for e being set st e in the carrier' of G holds

<*e*> is oriented Simple Chain of G

proof end;

Lm1: for n being Nat

for p, q being FinSequence st 1 <= n & n <= len p holds

p . n = (p ^ q) . n

proof end;

Lm2: for n being Nat

for p, q being FinSequence st 1 <= n & n <= len q holds

q . n = (p ^ q) . ((len p) + n)

proof end;

theorem Th6: :: GRAPHSP:6

for G being Graph

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

for p being oriented Simple 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) )

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

for p being oriented Simple 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 end;

theorem Th7: :: GRAPHSP:7

for G being Graph

for p being oriented Chain of G

for V being set

for v1, v2 being Vertex of G holds

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

for p being oriented Chain of G

for V being set

for v1, v2 being Vertex of G holds

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

proof end;

theorem Th8: :: GRAPHSP:8

for G being Graph

for p being oriented Chain of G

for W being Function

for V being set

for v1, v2 being Vertex of G holds

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

for p being oriented Chain of G

for W being Function

for V being set

for v1, v2 being Vertex of G holds

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

proof end;

theorem Th9: :: GRAPHSP:9

for G being Graph

for p, q being oriented Chain of G

for W being Function

for V being set

for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W holds

cost (p,W) = cost (q,W)

for p, q being oriented Chain of G

for W being Function

for V being set

for v1, v2 being Vertex of G st p is_shortestpath_of v1,v2,V,W & q is_shortestpath_of v1,v2,V,W holds

cost (p,W) = cost (q,W)

proof end;

theorem Th10: :: GRAPHSP:10

for G being oriented Graph

for v1, v2 being Vertex of G

for e1, e2 being set st e1 in the carrier' of G & e2 in the carrier' of G & e1 orientedly_joins v1,v2 & e2 orientedly_joins v1,v2 holds

e1 = e2

for v1, v2 being Vertex of G

for e1, e2 being set st e1 in the carrier' of G & e2 in the carrier' of G & e1 orientedly_joins v1,v2 & e2 orientedly_joins v1,v2 holds

e1 = e2

proof end;

Lm3: for i being Nat

for G being Graph

for pe being FinSequence of the carrier' of G st 1 <= i & i <= len pe holds

( the Source of G . (pe . i) in the carrier of G & the Target of G . (pe . i) in the carrier of G )

proof end;

theorem Th11: :: GRAPHSP:11

for G being Graph

for U, V being set

for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & v2 in V & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds

for e being set holds

( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) holds

for p being oriented Chain of G holds not p is_orientedpath_of v1,v2

for U, V being set

for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & v2 in V & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds

for e being set holds

( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) holds

for p being oriented Chain of G holds not p is_orientedpath_of v1,v2

proof end;

Lm4: for i being Nat

for G being Graph

for pe being FinSequence of the carrier' of G

for v1 being Vertex of G st 1 <= i & i <= len pe & ( v1 = the Source of G . (pe . i) or v1 = the Target of G . (pe . i) ) holds

v1 in vertices pe

proof end;

theorem Th12: :: GRAPHSP:12

for G being Graph

for p being oriented Chain of G

for U, V being set

for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds

for e being set holds

( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) & p is_orientedpath_of v1,v2 holds

p is_orientedpath_of v1,v2,U

for p being oriented Chain of G

for U, V being set

for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds

for e being set holds

( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) & p is_orientedpath_of v1,v2 holds

p is_orientedpath_of v1,v2,U

proof end;

theorem Th13: :: GRAPHSP:13

for W being Function

for V being set

for G being finite Graph

for P, Q being oriented Chain of G

for v1, v2, v3 being Vertex of G st 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 & ( for e being set holds

( not e in the carrier' of G or not e orientedly_joins v2,v3 ) ) & P islongestInShortestpath V,v1,W holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

for V being set

for G being finite Graph

for P, Q being oriented Chain of G

for v1, v2, v3 being Vertex of G st 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 & ( for e being set holds

( not e in the carrier' of G or not e orientedly_joins v2,v3 ) ) & P islongestInShortestpath V,v1,W holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

proof end;

theorem Th14: :: GRAPHSP:14

for e being set

for G being oriented finite Graph

for P being oriented Chain of G

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

for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds

P is_shortestpath_of v1,v2,{v1},W

for G being oriented finite Graph

for P being oriented Chain of G

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

for v1, v2 being Vertex of G st e in the carrier' of G & P = <*e*> & e orientedly_joins v1,v2 holds

P is_shortestpath_of v1,v2,{v1},W

proof end;

theorem Th15: :: GRAPHSP:15

for V, e being set

for G being oriented finite Graph

for P, Q being oriented Chain of G

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

for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

for G being oriented finite Graph

for P, Q being oriented Chain of G

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

for v1, v2, v3 being Vertex of G st e in the carrier' of G & P is_shortestpath_of v1,v2,V,W & v1 <> v3 & Q = P ^ <*e*> & e orientedly_joins v2,v3 & v1 in V & ( for v4 being Vertex of G st v4 in V holds

for ee being set holds

( not ee in the carrier' of G or not ee orientedly_joins v4,v3 ) ) holds

Q is_shortestpath_of v1,v3,V \/ {v2},W

proof end;

theorem Th16: :: GRAPHSP:16

for U, V being set

for G being oriented finite Graph

for P being oriented Chain of G

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

for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds

for e being set holds

( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) holds

( P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W )

for G being oriented finite Graph

for P being oriented Chain of G

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

for v1, v2 being Vertex of G st the carrier of G = U \/ V & v1 in U & ( for v3, v4 being Vertex of G st v3 in U & v4 in V holds

for e being set holds

( not e in the carrier' of G or not e orientedly_joins v3,v4 ) ) holds

( P is_shortestpath_of v1,v2,U,W iff P is_shortestpath_of v1,v2,W )

proof end;

definition

let f be FinSequence of REAL ;

let x be object ;

let r be Real;

:: original: :=

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

coherence

(f,x) := r is FinSequence of REAL

end;
let x be object ;

let r be Real;

:: original: :=

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

coherence

(f,x) := r is FinSequence of REAL

proof end;

definition

let i, k be Nat;

let f be FinSequence of REAL ;

let r be Real;

coherence

(((f,i) := k),k) := r is FinSequence of REAL ;

end;
let f be FinSequence of REAL ;

let r be Real;

coherence

(((f,i) := k),k) := r is FinSequence of REAL ;

:: deftheorem defines := GRAPHSP:def 1 :

for i, k being Nat

for f being FinSequence of REAL

for r being Real holds (f,i) := (k,r) = (((f,i) := k),k) := r;

for i, k being Nat

for f being FinSequence of REAL

for r being Real holds (f,i) := (k,r) = (((f,i) := k),k) := r;

theorem Th17: :: GRAPHSP:17

for i, k being Nat

for f being Element of REAL *

for r being Real st i <> k & i in dom f holds

((f,i) := (k,r)) . i = k

for f being Element of REAL *

for r being Real st i <> k & i in dom f holds

((f,i) := (k,r)) . i = k

proof end;

theorem Th18: :: GRAPHSP:18

for i, k, m being Nat

for f being Element of REAL *

for r being Real st m <> i & m <> k holds

((f,i) := (k,r)) . m = f . m

for f being Element of REAL *

for r being Real st m <> i & m <> k holds

((f,i) := (k,r)) . m = f . m

proof end;

theorem Th19: :: GRAPHSP:19

for i, k being Nat

for f being Element of REAL *

for r being Real st k in dom f holds

((f,i) := (k,r)) . k = r

for f being Element of REAL *

for r being Real st k in dom f holds

((f,i) := (k,r)) . k = r

proof end;

theorem Th20: :: GRAPHSP:20

for i, k being Nat

for f being Element of REAL *

for r being Real holds dom ((f,i) := (k,r)) = dom f

for f being Element of REAL *

for r being Real holds dom ((f,i) := (k,r)) = dom f

proof end;

definition

let X be set ;

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

:: original: *

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

coherence

f * g is Element of Funcs (X,X)

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

:: original: *

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

coherence

f * g is Element of Funcs (X,X)

proof end;

definition

let X be set ;

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

let g be Element of X;

:: original: .

redefine func f . g -> Element of X;

coherence

f . g is Element of X

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

let g be Element of X;

:: original: .

redefine func f . g -> Element of X;

coherence

f . g is Element of X

proof end;

definition

let X be set ;

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

ex b_{1} being sequence of (Funcs (X,X)) st

( b_{1} . 0 = id X & ( for i being Nat holds b_{1} . (i + 1) = f * (b_{1} . i) ) )

for b_{1}, b_{2} being sequence of (Funcs (X,X)) st b_{1} . 0 = id X & ( for i being Nat holds b_{1} . (i + 1) = f * (b_{1} . i) ) & b_{2} . 0 = id X & ( for i being Nat holds b_{2} . (i + 1) = f * (b_{2} . i) ) holds

b_{1} = b_{2}

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

func repeat f -> sequence of (Funcs (X,X)) means :Def2: :: GRAPHSP:def 2

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

existence ( it . 0 = id X & ( for i being Nat holds it . (i + 1) = f * (it . i) ) );

ex b

( b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines repeat GRAPHSP:def 2 :

for X being set

for f being Element of Funcs (X,X)

for b_{3} being sequence of (Funcs (X,X)) holds

( b_{3} = repeat f iff ( b_{3} . 0 = id X & ( for i being Nat holds b_{3} . (i + 1) = f * (b_{3} . i) ) ) );

for X being set

for f being Element of Funcs (X,X)

for b

( b

theorem Th21: :: GRAPHSP:21

for F being Element of Funcs ((REAL *),(REAL *))

for f being Element of REAL *

for n, i being Element of NAT holds ((repeat F) . 0) . f = f

for f being Element of REAL *

for n, i being Element of NAT holds ((repeat F) . 0) . f = f

proof end;

Lm5: for X being set

for f being Element of Funcs (X,X) holds dom f = X

proof end;

theorem Th22: :: GRAPHSP:22

for F, G being Element of Funcs ((REAL *),(REAL *))

for f being Element of REAL *

for i being Nat holds ((repeat (F * G)) . (i + 1)) . f = F . (G . (((repeat (F * G)) . i) . f))

for f being Element of REAL *

for i being Nat holds ((repeat (F * G)) . (i + 1)) . f = F . (G . (((repeat (F * G)) . i) . f))

proof end;

definition

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

let f be Element of REAL * ;

:: original: .

redefine func g . f -> Element of REAL * ;

coherence

g . f is Element of REAL *

end;
let f be Element of REAL * ;

:: original: .

redefine func g . f -> Element of REAL * ;

coherence

g . f is Element of REAL *

proof end;

definition

let f be Element of REAL * ;

let n be Nat;

{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 & f . (n + i) <> - 1 ) } is Subset of NAT

end;
let n be Nat;

func OuterVx (f,n) -> Subset of NAT equals :: GRAPHSP:def 3

{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 & f . (n + i) <> - 1 ) } ;

coherence { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 & f . (n + i) <> - 1 ) } ;

{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 & f . (n + i) <> - 1 ) } is Subset of NAT

proof end;

:: deftheorem defines OuterVx GRAPHSP:def 3 :

for f being Element of REAL *

for n being Nat holds OuterVx (f,n) = { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 & f . (n + i) <> - 1 ) } ;

for f being Element of REAL *

for n being Nat holds OuterVx (f,n) = { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 & f . (n + i) <> - 1 ) } ;

definition

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

let g be Element of REAL * ;

let n be Nat;

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

ex b_{1} being Element of NAT st

( OuterVx ((((repeat f) . b_{1}) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds

b_{1} <= k ) )

for b_{1}, b_{2} being Element of NAT st OuterVx ((((repeat f) . b_{1}) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds

b_{1} <= k ) & OuterVx ((((repeat f) . b_{2}) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds

b_{2} <= k ) holds

b_{1} = b_{2}

end;
let g be Element of REAL * ;

let n be Nat;

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

func LifeSpan (f,g,n) -> Element of NAT means :Def4: :: GRAPHSP:def 4

( OuterVx ((((repeat f) . it) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds

it <= k ) );

existence ( OuterVx ((((repeat f) . it) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds

it <= k ) );

ex b

( OuterVx ((((repeat f) . b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def4 defines LifeSpan GRAPHSP:def 4 :

for f being Element of Funcs ((REAL *),(REAL *))

for g being Element of REAL *

for n being Nat st ex i being Nat st OuterVx ((((repeat f) . i) . g),n) = {} holds

for b_{4} being Element of NAT holds

( b_{4} = LifeSpan (f,g,n) iff ( OuterVx ((((repeat f) . b_{4}) . g),n) = {} & ( for k being Nat st OuterVx ((((repeat f) . k) . g),n) = {} holds

b_{4} <= k ) ) );

for f being Element of Funcs ((REAL *),(REAL *))

for g being Element of REAL *

for n being Nat st ex i being Nat st OuterVx ((((repeat f) . i) . g),n) = {} holds

for b

( b

b

definition

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

let n be Nat;

ex b_{1} being Element of Funcs ((REAL *),(REAL *)) st

( dom b_{1} = REAL * & ( for h being Element of REAL * holds b_{1} . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) )

for b_{1}, b_{2} being Element of Funcs ((REAL *),(REAL *)) st dom b_{1} = REAL * & ( for h being Element of REAL * holds b_{1} . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) & dom b_{2} = REAL * & ( for h being Element of REAL * holds b_{2} . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) holds

b_{1} = b_{2}

end;
let n be Nat;

func while_do (f,n) -> Element of Funcs ((REAL *),(REAL *)) means :Def5: :: GRAPHSP:def 5

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

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

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def5 defines while_do GRAPHSP:def 5 :

for f being Element of Funcs ((REAL *),(REAL *))

for n being Nat

for b_{3} being Element of Funcs ((REAL *),(REAL *)) holds

( b_{3} = while_do (f,n) iff ( dom b_{3} = REAL * & ( for h being Element of REAL * holds b_{3} . h = ((repeat f) . (LifeSpan (f,h,n))) . h ) ) );

for f being Element of Funcs ((REAL *),(REAL *))

for n being Nat

for b

( b

definition

let G be oriented Graph;

let v1, v2 be Vertex of G;

assume A1: ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) ;

ex b_{1}, e being set st

( b_{1} = e & e in the carrier' of G & e orientedly_joins v1,v2 )
by A1;

uniqueness

for b_{1}, b_{2} being set st ex e being set st

( b_{1} = e & e in the carrier' of G & e orientedly_joins v1,v2 ) & ex e being set st

( b_{2} = e & e in the carrier' of G & e orientedly_joins v1,v2 ) holds

b_{1} = b_{2}
by Th10;

end;
let v1, v2 be Vertex of G;

assume A1: ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) ;

func XEdge (v1,v2) -> set means :Def6: :: GRAPHSP:def 6

ex e being set st

( it = e & e in the carrier' of G & e orientedly_joins v1,v2 );

existence ex e being set st

( it = e & e in the carrier' of G & e orientedly_joins v1,v2 );

ex b

( b

uniqueness

for b

( b

( b

b

:: deftheorem Def6 defines XEdge GRAPHSP:def 6 :

for G being oriented Graph

for v1, v2 being Vertex of G st ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) holds

for b_{4} being set holds

( b_{4} = XEdge (v1,v2) iff ex e being set st

( b_{4} = e & e in the carrier' of G & e orientedly_joins v1,v2 ) );

for G being oriented Graph

for v1, v2 being Vertex of G st ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) holds

for b

( b

( b

definition

let G be oriented Graph;

let v1, v2 be Vertex of G;

let W be Function;

coherence

( ( ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) implies W . (XEdge (v1,v2)) is set ) & ( ( for e being set holds

( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ) implies - 1 is set ) );

consistency

for b_{1} being set holds verum;

by TARSKI:1;

end;
let v1, v2 be Vertex of G;

let W be Function;

func Weight (v1,v2,W) -> set equals :Def7: :: GRAPHSP:def 7

W . (XEdge (v1,v2)) if ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 )

otherwise - 1;

correctness W . (XEdge (v1,v2)) if ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 )

otherwise - 1;

coherence

( ( ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) implies W . (XEdge (v1,v2)) is set ) & ( ( for e being set holds

( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ) implies - 1 is set ) );

consistency

for b

by TARSKI:1;

:: deftheorem Def7 defines Weight GRAPHSP:def 7 :

for G being oriented Graph

for v1, v2 being Vertex of G

for W being Function holds

( ( ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) implies Weight (v1,v2,W) = W . (XEdge (v1,v2)) ) & ( ( for e being set holds

( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ) implies Weight (v1,v2,W) = - 1 ) );

for G being oriented Graph

for v1, v2 being Vertex of G

for W being Function holds

( ( ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) implies Weight (v1,v2,W) = W . (XEdge (v1,v2)) ) & ( ( for e being set holds

( not e in the carrier' of G or not e orientedly_joins v1,v2 ) ) implies Weight (v1,v2,W) = - 1 ) );

registration

let G be oriented Graph;

let v1, v2 be Vertex of G;

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

coherence

Weight (v1,v2,W) is real

end;
let v1, v2 be Vertex of G;

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

coherence

Weight (v1,v2,W) is real

proof end;

theorem Th23: :: GRAPHSP:23

for G being oriented Graph

for v1, v2 being Vertex of G

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

( Weight (v1,v2,W) >= 0 iff ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) )

for v1, v2 being Vertex of G

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

( Weight (v1,v2,W) >= 0 iff ex e being set st

( e in the carrier' of G & e orientedly_joins v1,v2 ) )

proof end;

theorem :: GRAPHSP:24

theorem Th25: :: GRAPHSP:25

for e being set

for G being oriented Graph

for v1, v2 being Vertex of G

for W being Function of the carrier' of G,Real>=0 st e in the carrier' of G & e orientedly_joins v1,v2 holds

Weight (v1,v2,W) = W . e

for G being oriented Graph

for v1, v2 being Vertex of G

for W being Function of the carrier' of G,Real>=0 st e in the carrier' of G & e orientedly_joins v1,v2 holds

Weight (v1,v2,W) = W . e

proof end;

definition

let f be Element of REAL * ;

let n be Nat;

{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } is Subset of NAT

end;
let n be Nat;

func UnusedVx (f,n) -> Subset of NAT equals :: GRAPHSP:def 8

{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } ;

coherence { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } ;

{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } is Subset of NAT

proof end;

:: deftheorem defines UnusedVx GRAPHSP:def 8 :

for f being Element of REAL *

for n being Nat holds UnusedVx (f,n) = { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } ;

for f being Element of REAL *

for n being Nat holds UnusedVx (f,n) = { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i <> - 1 ) } ;

definition

let f be Element of REAL * ;

let n be Nat;

{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i = - 1 ) } is Subset of NAT

end;
let n be Nat;

func UsedVx (f,n) -> Subset of NAT equals :: GRAPHSP:def 9

{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i = - 1 ) } ;

coherence { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i = - 1 ) } ;

{ i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i = - 1 ) } is Subset of NAT

proof end;

:: deftheorem defines UsedVx GRAPHSP:def 9 :

for f being Element of REAL *

for n being Nat holds UsedVx (f,n) = { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i = - 1 ) } ;

for f being Element of REAL *

for n being Nat holds UsedVx (f,n) = { i where i is Nat : ( i in dom f & 1 <= i & i <= n & f . i = - 1 ) } ;

registration
end;

registration
end;

definition

let X be finite Subset of NAT;

let f be Element of REAL * ;

let n be Nat;

ex b_{1} being Nat st

( ( X <> {} implies ex i being Nat st

( i = b_{1} & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b_{1} = 0 ) )

for b_{1}, b_{2} being Nat st ( X <> {} implies ex i being Nat st

( i = b_{1} & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b_{1} = 0 ) & ( X <> {} implies ex i being Nat st

( i = b_{2} & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b_{2} = 0 ) holds

b_{1} = b_{2}

end;
let f be Element of REAL * ;

let n be Nat;

func Argmin (X,f,n) -> Nat means :Def10: :: GRAPHSP:def 10

( ( X <> {} implies ex i being Nat st

( i = it & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies it = 0 ) );

existence ( ( X <> {} implies ex i being Nat st

( i = it & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies it = 0 ) );

ex b

( ( X <> {} implies ex i being Nat st

( i = b

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b

proof end;

uniqueness for b

( i = b

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b

( i = b

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b

b

proof end;

:: deftheorem Def10 defines Argmin GRAPHSP:def 10 :

for X being finite Subset of NAT

for f being Element of REAL *

for n, b_{4} being Nat holds

( b_{4} = Argmin (X,f,n) iff ( ( X <> {} implies ex i being Nat st

( i = b_{4} & i in X & ( for k being Nat st k in X holds

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b_{4} = 0 ) ) );

for X being finite Subset of NAT

for f being Element of REAL *

for n, b

( b

( i = b

f /. ((2 * n) + i) <= f /. ((2 * n) + k) ) & ( for k being Nat st k in X & f /. ((2 * n) + i) = f /. ((2 * n) + k) holds

i <= k ) ) ) & ( X = {} implies b

theorem Th29: :: GRAPHSP:29

for j, n being Nat

for f being Element of REAL * st OuterVx (f,n) <> {} & j = Argmin ((OuterVx (f,n)),f,n) holds

( j in dom f & 1 <= j & j <= n & f . j <> - 1 & f . (n + j) <> - 1 )

for f being Element of REAL * st OuterVx (f,n) <> {} & j = Argmin ((OuterVx (f,n)),f,n) holds

( j in dom f & 1 <= j & j <= n & f . j <> - 1 & f . (n + j) <> - 1 )

proof end;

definition

let n be Nat;

ex b_{1} being Element of Funcs ((REAL *),(REAL *)) st

( dom b_{1} = REAL * & ( for f being Element of REAL * holds b_{1} . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) )

for b_{1}, b_{2} being Element of Funcs ((REAL *),(REAL *)) st dom b_{1} = REAL * & ( for f being Element of REAL * holds b_{1} . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) & dom b_{2} = REAL * & ( for f being Element of REAL * holds b_{2} . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) holds

b_{1} = b_{2}

end;
func findmin n -> Element of Funcs ((REAL *),(REAL *)) means :Def11: :: GRAPHSP:def 11

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

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

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def11 defines findmin GRAPHSP:def 11 :

for n being Nat

for b_{2} being Element of Funcs ((REAL *),(REAL *)) holds

( b_{2} = findmin n iff ( dom b_{2} = REAL * & ( for f being Element of REAL * holds b_{2} . f = (f,(((n * n) + (3 * n)) + 1)) := ((Argmin ((OuterVx (f,n)),f,n)),(- 1)) ) ) );

for n being Nat

for b

( b

reconsider jj = 1 as Real ;

theorem Th31: :: GRAPHSP:31

for i, n being Nat

for f being Element of REAL * st i > n & i <> ((n * n) + (3 * n)) + 1 holds

((findmin n) . f) . i = f . i

for f being Element of REAL * st i > n & i <> ((n * n) + (3 * n)) + 1 holds

((findmin n) . f) . i = f . i

proof end;

theorem Th32: :: GRAPHSP:32

for i, n being Nat

for f being Element of REAL * st i in dom f & f . i = - 1 & i <> ((n * n) + (3 * n)) + 1 holds

((findmin n) . f) . i = - 1

for f being Element of REAL * st i in dom f & f . i = - 1 & i <> ((n * n) + (3 * n)) + 1 holds

((findmin n) . f) . i = - 1

proof end;

Lm6: for k, n being Nat st k >= 1 holds

n <= k * n

proof end;

Lm7: for n being Nat holds

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

proof end;

Lm8: for k, n being Nat holds

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

proof end;

theorem Th34: :: GRAPHSP:34

for n being Nat

for f being Element of REAL * st OuterVx (f,n) <> {} holds

ex j being Nat st

( j in OuterVx (f,n) & 1 <= j & j <= n & ((findmin n) . f) . j = - 1 )

for f being Element of REAL * st OuterVx (f,n) <> {} holds

ex j being Nat st

( j in OuterVx (f,n) & 1 <= j & j <= n & ((findmin n) . f) . j = - 1 )

proof end;

definition

let f be Element of REAL * ;

let n, k be Nat;

coherence

(f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k)) is Real;

;

end;
let n, k be Nat;

func newpathcost (f,n,k) -> Real equals :: GRAPHSP:def 12

(f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k));

correctness (f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k));

coherence

(f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k)) is Real;

;

:: deftheorem defines newpathcost GRAPHSP:def 12 :

for f being Element of REAL *

for n, k being Nat holds newpathcost (f,n,k) = (f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k));

for f being Element of REAL *

for n, k being Nat holds newpathcost (f,n,k) = (f /. ((2 * n) + (f /. (((n * n) + (3 * n)) + 1)))) + (f /. (((2 * n) + (n * (f /. (((n * n) + (3 * n)) + 1)))) + k));

:: deftheorem defines hasBetterPathAt GRAPHSP:def 13 :

for n, k being Nat

for f being Element of REAL * holds

( f hasBetterPathAt n,k iff ( ( 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 ) );

for n, k being Nat

for f being Element of REAL * holds

( f hasBetterPathAt n,k iff ( ( 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 ) );

definition

let f be Element of REAL * ;

let n be Nat;

ex b_{1} being Element of REAL * st

( dom b_{1} = dom f & ( for k being Nat st k in dom f holds

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b_{1} . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies b_{1} . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b_{1} . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies b_{1} . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies b_{1} . k = f . k ) ) ) )

for b_{1}, b_{2} being Element of REAL * st dom b_{1} = dom f & ( for k being Nat st k in dom f holds

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b_{1} . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies b_{1} . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b_{1} . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies b_{1} . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies b_{1} . k = f . k ) ) ) & dom b_{2} = dom f & ( for k being Nat st k in dom f holds

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b_{2} . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies b_{2} . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b_{2} . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies b_{2} . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies b_{2} . k = f . k ) ) ) holds

b_{1} = b_{2}

end;
let n be Nat;

func Relax (f,n) -> Element of REAL * means :Def14: :: GRAPHSP:def 14

( dom it = dom f & ( for k being 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 ( dom it = dom f & ( for k being 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 ) ) ) );

ex b

( dom b

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b

proof end;

uniqueness for b

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b

b

proof end;

:: deftheorem Def14 defines Relax GRAPHSP:def 14 :

for f being Element of REAL *

for n being Nat

for b_{3} being Element of REAL * holds

( b_{3} = Relax (f,n) iff ( dom b_{3} = dom f & ( for k being Nat st k in dom f holds

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b_{3} . k = f /. (((n * n) + (3 * n)) + 1) ) & ( not f hasBetterPathAt n,k -' n implies b_{3} . k = f . k ) ) ) & ( 2 * n < k & k <= 3 * n implies ( ( f hasBetterPathAt n,k -' (2 * n) implies b_{3} . k = newpathcost (f,n,(k -' (2 * n))) ) & ( not f hasBetterPathAt n,k -' (2 * n) implies b_{3} . k = f . k ) ) ) & ( ( k <= n or k > 3 * n ) implies b_{3} . k = f . k ) ) ) ) );

for f being Element of REAL *

for n being Nat

for b

( b

( ( n < k & k <= 2 * n implies ( ( f hasBetterPathAt n,k -' n implies b

definition

let n be Nat;

ex b_{1} being Element of Funcs ((REAL *),(REAL *)) st

( dom b_{1} = REAL * & ( for f being Element of REAL * holds b_{1} . f = Relax (f,n) ) )

for b_{1}, b_{2} being Element of Funcs ((REAL *),(REAL *)) st dom b_{1} = REAL * & ( for f being Element of REAL * holds b_{1} . f = Relax (f,n) ) & dom b_{2} = REAL * & ( for f being Element of REAL * holds b_{2} . f = Relax (f,n) ) holds

b_{1} = b_{2}

end;
func Relax n -> Element of Funcs ((REAL *),(REAL *)) means :Def15: :: GRAPHSP:def 15

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

existence ( dom it = REAL * & ( for f being Element of REAL * holds it . f = Relax (f,n) ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def15 defines Relax GRAPHSP:def 15 :

for n being Nat

for b_{2} being Element of Funcs ((REAL *),(REAL *)) holds

( b_{2} = Relax n iff ( dom b_{2} = REAL * & ( for f being Element of REAL * holds b_{2} . f = Relax (f,n) ) ) );

for n being Nat

for b

( b

theorem Th36: :: GRAPHSP:36

for i, n being Nat

for f being Element of REAL * st ( i <= n or i > 3 * n ) & i in dom f holds

((Relax n) . f) . i = f . i

for f being Element of REAL * st ( i <= n or i > 3 * n ) & i in dom f holds

((Relax n) . f) . i = f . i

proof end;

theorem Th37: :: GRAPHSP:37

for i, n being Nat

for f being Element of REAL * holds dom (((repeat ((Relax n) * (findmin n))) . i) . f) = dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f)

for f being Element of REAL * holds dom (((repeat ((Relax n) * (findmin n))) . i) . f) = dom (((repeat ((Relax n) * (findmin n))) . (i + 1)) . f)

proof end;

theorem Th38: :: GRAPHSP:38

for i, n being Nat

for f being Element of REAL * st OuterVx ((((repeat ((Relax n) * (findmin n))) . i) . f),n) <> {} holds

UnusedVx ((((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n) c< UnusedVx ((((repeat ((Relax n) * (findmin n))) . i) . f),n)

for f being Element of REAL * st OuterVx ((((repeat ((Relax n) * (findmin n))) . i) . f),n) <> {} holds

UnusedVx ((((repeat ((Relax n) * (findmin n))) . (i + 1)) . f),n) c< UnusedVx ((((repeat ((Relax n) * (findmin n))) . i) . f),n)

proof end;

theorem Th39: :: GRAPHSP:39

for i, k, n being Nat

for f, g, h being Element of REAL * st 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) <> {} holds

( UsedVx (h,n) = (UsedVx (g,n)) \/ {k} & not k in UsedVx (g,n) )

for f, g, h being Element of REAL * st 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) <> {} holds

( UsedVx (h,n) = (UsedVx (g,n)) \/ {k} & not k in UsedVx (g,n) )

proof end;

theorem Th40: :: GRAPHSP:40

for n being Nat

for f being Element of REAL * ex i being Nat st

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

for f being Element of REAL * ex i being Nat st

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

proof end;

Lm9: for k, n being Nat holds n - k <= n

proof end;

Lm10: for p, q being FinSequence of NAT

for f being Element of REAL *

for i, n being Element of NAT st ( for k being Nat st 1 <= k & k < len p holds

p . ((len p) - k) = f . ((p /. (((len p) - k) + 1)) + n) ) & ( for k being Nat 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 being Nat st 1 <= k & k < len p holds

p . ((len p) - k) = q . ((len q) - k)

proof end;

theorem Th41: :: GRAPHSP:41

for i, n being Nat

for f being Element of REAL * holds dom f = dom (((repeat ((Relax n) * (findmin n))) . i) . f)

for f being Element of REAL * holds dom f = dom (((repeat ((Relax n) * (findmin n))) . i) . f)

proof end;

:: deftheorem defines equal_at GRAPHSP:def 16 :

for f, g being Element of REAL *

for m, n being Nat holds

( f,g equal_at m,n iff ( dom f = dom g & ( for k being Nat st k in dom f & m <= k & k <= n holds

f . k = g . k ) ) );

for f, g being Element of REAL *

for m, n being Nat holds

( f,g equal_at m,n iff ( dom f = dom g & ( for k being Nat st k in dom f & m <= k & k <= n holds

f . k = g . k ) ) );

theorem Th43: :: GRAPHSP:43

for m, n being Nat

for f, g, h being Element of REAL * st f,g equal_at m,n & g,h equal_at m,n holds

f,h equal_at m,n

for f, g, h being Element of REAL * st f,g equal_at m,n & g,h equal_at m,n holds

f,h equal_at m,n

proof end;

theorem Th44: :: GRAPHSP:44

for i, n being Nat

for f being Element of REAL * holds ((repeat ((Relax n) * (findmin n))) . i) . f,((repeat ((Relax n) * (findmin n))) . (i + 1)) . f equal_at (3 * n) + 1,(n * n) + (3 * n)

for f being Element of REAL * holds ((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 end;

theorem :: GRAPHSP:45

theorem Th46: :: GRAPHSP:46

for i, n being Nat

for f being Element of REAL * holds f,((repeat ((Relax n) * (findmin n))) . i) . f equal_at (3 * n) + 1,(n * n) + (3 * n)

for f being Element of REAL * holds f,((repeat ((Relax n) * (findmin n))) . i) . f equal_at (3 * n) + 1,(n * n) + (3 * n)

proof end;

theorem Th47: :: GRAPHSP:47

for n being Nat

for f being Element of REAL * st 1 <= n & 1 in dom f & f . (n + 1) <> - 1 & ( for i being Nat st 1 <= i & i <= n holds

f . i = 1 ) & ( for i being Nat st 2 <= i & i <= n holds

f . (n + i) = - 1 ) holds

( 1 = Argmin ((OuterVx (f,n)),f,n) & UsedVx (f,n) = {} & {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) )

for f being Element of REAL * st 1 <= n & 1 in dom f & f . (n + 1) <> - 1 & ( for i being Nat st 1 <= i & i <= n holds

f . i = 1 ) & ( for i being Nat st 2 <= i & i <= n holds

f . (n + i) = - 1 ) holds

( 1 = Argmin ((OuterVx (f,n)),f,n) & UsedVx (f,n) = {} & {1} = UsedVx ((((repeat ((Relax n) * (findmin n))) . 1) . f),n) )

proof end;

theorem Th48: :: GRAPHSP:48

for i, m, n being Nat

for f, g, h being Element of REAL * st 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) holds

m in UsedVx (h,n)

for f, g, h being Element of REAL * st 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) holds

m in UsedVx (h,n)

proof end;

:: deftheorem defines is_vertex_seq_at GRAPHSP:def 17 :

for p being FinSequence of NAT

for f being Element of REAL *

for i, n being Nat holds

( p is_vertex_seq_at f,i,n iff ( p . (len p) = i & ( for k being Nat st 1 <= k & k < len p holds

p . ((len p) - k) = f . (n + (p /. (((len p) - k) + 1))) ) ) );

for p being FinSequence of NAT

for f being Element of REAL *

for i, n being Nat holds

( p is_vertex_seq_at f,i,n iff ( p . (len p) = i & ( for k being Nat st 1 <= k & k < len p holds

p . ((len p) - k) = f . (n + (p /. (((len p) - k) + 1))) ) ) );

definition

let p be FinSequence of NAT ;

let f be Element of REAL * ;

let i, n be Nat;

end;
let f be Element of REAL * ;

let i, n be Nat;

pred p is_simple_vertex_seq_at f,i,n means :: GRAPHSP:def 18

( p . 1 = 1 & len p > 1 & p is_vertex_seq_at f,i,n & p is one-to-one );

( p . 1 = 1 & len p > 1 & p is_vertex_seq_at f,i,n & p is one-to-one );

:: deftheorem defines is_simple_vertex_seq_at GRAPHSP:def 18 :

for p being FinSequence of NAT

for f being Element of REAL *

for i, n being Nat holds

( p is_simple_vertex_seq_at f,i,n iff ( p . 1 = 1 & len p > 1 & p is_vertex_seq_at f,i,n & p is one-to-one ) );

for p being FinSequence of NAT

for f being Element of REAL *

for i, n being Nat holds

( p is_simple_vertex_seq_at f,i,n iff ( p . 1 = 1 & len p > 1 & p is_vertex_seq_at f,i,n & p is one-to-one ) );

theorem :: GRAPHSP:49

for p, q being FinSequence of NAT

for f being Element of REAL *

for i, n being Element of NAT st p is_simple_vertex_seq_at f,i,n & q is_simple_vertex_seq_at f,i,n holds

p = q

for f being Element of REAL *

for i, n being Element of NAT st p is_simple_vertex_seq_at f,i,n & q is_simple_vertex_seq_at f,i,n holds

p = q

proof end;

:: deftheorem defines is_oriented_edge_seq_of GRAPHSP:def 19 :

for G being Graph

for p being FinSequence of the carrier' of G

for vs being FinSequence holds

( p is_oriented_edge_seq_of vs iff ( len vs = (len p) + 1 & ( for n being Nat st 1 <= n & n <= len p holds

( the Source of G . (p . n) = vs . n & the Target of G . (p . n) = vs . (n + 1) ) ) ) );

for G being Graph

for p being FinSequence of the carrier' of G

for vs being FinSequence holds

( p is_oriented_edge_seq_of vs iff ( len vs = (len p) + 1 & ( for n being Nat st 1 <= n & n <= len p holds

( the Source of G . (p . n) = vs . n & the Target of G . (p . n) = vs . (n + 1) ) ) ) );

theorem :: GRAPHSP:50

for G being oriented Graph

for vs being FinSequence

for 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

for vs being FinSequence

for 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 end;

theorem :: GRAPHSP:51

for G being Graph

for vs1, vs2 being FinSequence

for 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

for vs1, vs2 being FinSequence

for 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 end;

Lm11: for i, n being Nat st 1 <= i & i <= n holds

( 1 < (2 * n) + i & (2 * n) + i < ((n * n) + (3 * n)) + 1 & i < (2 * n) + i )

proof end;

Lm12: for i, n being Nat st 1 <= i & i <= n holds

( 1 < n + i & n + i <= 2 * n & n + i < ((n * n) + (3 * n)) + 1 )

proof end;

Lm13: for i, j, n being Nat st 1 <= i & i <= n & j <= n holds

( 1 < ((2 * n) + (n * i)) + j & i < ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j < ((n * n) + (3 * n)) + 1 )

proof end;

Lm14: for i, j, n being Nat st 1 <= i & i <= n & 1 <= j & j <= n holds

( (3 * n) + 1 <= ((2 * n) + (n * i)) + j & ((2 * n) + (n * i)) + j <= (n * n) + (3 * n) )

proof end;

definition

let f be Element of REAL * ;

let G be oriented Graph;

let n be Nat;

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

end;
let G be oriented Graph;

let n be Nat;

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

pred f is_Input_of_Dijkstra_Alg G,n,W means :: GRAPHSP:def 20

( len f = ((n * n) + (3 * n)) + 1 & Seg n = the carrier of G & ( for i being Nat st 1 <= i & i <= n holds

( f . i = 1 & f . ((2 * n) + i) = 0 ) ) & f . (n + 1) = 0 & ( for i being Nat st 2 <= i & i <= n holds

f . (n + i) = - 1 ) & ( for i, j being Vertex of G

for k, m being Nat st k = i & m = j holds

f . (((2 * n) + (n * k)) + m) = Weight (i,j,W) ) );

( len f = ((n * n) + (3 * n)) + 1 & Seg n = the carrier of G & ( for i being Nat st 1 <= i & i <= n holds

( f . i = 1 & f . ((2 * n) + i) = 0 ) ) & f . (n + 1) = 0 & ( for i being Nat st 2 <= i & i <= n holds

f . (n + i) = - 1 ) & ( for i, j being Vertex of G

for k, m being Nat st k = i & m = j holds

f . (((2 * n) + (n * k)) + m) = Weight (i,j,W) ) );

:: deftheorem defines is_Input_of_Dijkstra_Alg GRAPHSP:def 20 :

for f being Element of REAL *

for G being oriented Graph

for n being Nat

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

( f is_Input_of_Dijkstra_Alg G,n,W iff ( len f = ((n * n) + (3 * n)) + 1 & Seg n = the carrier of G & ( for i being Nat st 1 <= i & i <= n holds

( f . i = 1 & f . ((2 * n) + i) = 0 ) ) & f . (n + 1) = 0 & ( for i being Nat st 2 <= i & i <= n holds

f . (n + i) = - 1 ) & ( for i, j being Vertex of G

for k, m being Nat st k = i & m = j holds

f . (((2 * n) + (n * k)) + m) = Weight (i,j,W) ) ) );

for f being Element of REAL *

for G being oriented Graph

for n being Nat

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

( f is_Input_of_Dijkstra_Alg G,n,W iff ( len f = ((n * n) + (3 * n)) + 1 & Seg n = the carrier of G & ( for i being Nat st 1 <= i & i <= n holds

( f . i = 1 & f . ((2 * n) + i) = 0 ) ) & f . (n + 1) = 0 & ( for i being Nat st 2 <= i & i <= n holds

f . (n + i) = - 1 ) & ( for i, j being Vertex of G

for k, m being Nat st k = i & m = j holds

f . (((2 * n) + (n * k)) + m) = Weight (i,j,W) ) ) );

definition

let n be Nat;

while_do (((Relax n) * (findmin n)),n) is Element of Funcs ((REAL *),(REAL *)) ;

end;
func DijkstraAlgorithm n -> Element of Funcs ((REAL *),(REAL *)) equals :: GRAPHSP:def 21

while_do (((Relax n) * (findmin n)),n);

coherence while_do (((Relax n) * (findmin n)),n);

while_do (((Relax n) * (findmin n)),n) is Element of Funcs ((REAL *),(REAL *)) ;

:: deftheorem defines DijkstraAlgorithm GRAPHSP:def 21 :

for n being Nat holds DijkstraAlgorithm n = while_do (((Relax n) * (findmin n)),n);

for n being Nat holds DijkstraAlgorithm n = while_do (((Relax n) * (findmin n)),n);

Lm15: for n being Nat

for f, h being Element of REAL *

for G being oriented finite Graph

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

for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & h = ((repeat ((Relax n) * (findmin n))) . 1) . f holds

( ( for v3 being Vertex of G

for j being Nat st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds

ex p being FinSequence of NAT ex P being oriented Chain of G st

( p is_simple_vertex_seq_at h,j,n & ( for i being Nat 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 being Nat st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (h,n) holds

f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx (h,n) holds

h . (n + m) <> - 1 ) )

proof end;

Lm16: for i, k, n being Nat

for f, g, h being Element of REAL * st 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 holds

h . (n + i) = g . (n + i)

proof end;

Lm17: for j, k, n being Nat

for f, g, h being Element of REAL *

for p being FinSequence of NAT st 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 being Nat st 1 <= i & i < len p holds

p . i in UsedVx (g,n) ) holds

p is_simple_vertex_seq_at h,j,n

proof end;

Lm18: for j, k, m, n being Nat

for f, g, h being Element of REAL *

for p being FinSequence of NAT st 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 being Nat st 1 <= i & i < len p holds

p . i in UsedVx (g,n) ) holds

for q being FinSequence of NAT st q = p ^ <*j*> holds

q is_simple_vertex_seq_at h,j,n

proof end;

Lm19: for i, n being Nat

for V being set

for f, g being Element of REAL *

for G being oriented finite Graph

for P being oriented Chain of G

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

for v1, v2 being Vertex of G st 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 being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in V holds

f . (((2 * n) + (n * m)) + j) = - 1 ) holds

g . (n + i) <> - 1

proof end;

Lm20: for k, n being Nat

for f, g, h being Element of REAL *

for G being oriented finite Graph

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

for v1 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & n >= 1 & g = ((repeat ((Relax n) * (findmin n))) . k) . f & h = ((repeat ((Relax n) * (findmin n))) . (k + 1)) . f & OuterVx (g,n) <> {} & 1 in UsedVx (g,n) & ( for v3 being Vertex of G

for j being Nat st v3 <> v1 & v3 = j & g . (n + j) <> - 1 holds

ex p being FinSequence of NAT ex P being oriented Chain of G st

( p is_simple_vertex_seq_at g,j,n & ( for i being Nat 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 being Nat st g . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (g,n) holds

f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx (g,n) holds

g . (n + m) <> - 1 ) holds

( ( for v3 being Vertex of G

for j being Nat st v3 <> v1 & v3 = j & h . (n + j) <> - 1 holds

ex p being FinSequence of NAT ex P being oriented Chain of G st

( p is_simple_vertex_seq_at h,j,n & ( for i being Nat 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 being Nat st h . (n + j) = - 1 & 1 <= j & j <= n & m in UsedVx (h,n) holds

f . (((2 * n) + (n * m)) + j) = - 1 ) & ( for m being Nat st m in UsedVx (h,n) holds

h . (n + m) <> - 1 ) )

proof end;

theorem :: GRAPHSP:52

for i, n being Nat

for f, g being Element of REAL *

for G being oriented finite Graph

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

for v1, v2 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & 1 <> v2 & v2 = i & n >= 1 & g = (DijkstraAlgorithm n) . f holds

( the carrier of G = (UsedVx (g,n)) \/ (UnusedVx (g,n)) & ( v2 in UsedVx (g,n) implies ex p being FinSequence of NAT ex P being oriented Chain of G 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 for Q being oriented Chain of G holds not Q is_orientedpath_of v1,v2 ) )

for f, g being Element of REAL *

for G being oriented finite Graph

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

for v1, v2 being Vertex of G st f is_Input_of_Dijkstra_Alg G,n,W & v1 = 1 & 1 <> v2 & v2 = i & n >= 1 & g = (DijkstraAlgorithm n) . f holds

( the carrier of G = (UsedVx (g,n)) \/ (UnusedVx (g,n)) & ( v2 in UsedVx (g,n) implies ex p being FinSequence of NAT ex P being oriented Chain of G 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 for Q being oriented Chain of G holds not Q is_orientedpath_of v1,v2 ) )

proof end;

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