:: by Jingchao Chen and Yatsuka Nakamura

::

:: Received January 7, 2003

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

begin

theorem Th1: :: GRAPH_5:1

for x being set

for f, g being Function st rng f c= rng g & x in dom f holds

ex y being set st

( y in dom g & f . x = g . y )

for f, g being Function st rng f c= rng g & x in dom f holds

ex y being set st

( y in dom g & f . x = g . y )

proof end;

theorem Th2: :: GRAPH_5:2

for D being finite set

for n being Element of NAT

for X being set st X = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } holds

X is finite

for n being Element of NAT

for X being set st X = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } holds

X is finite

proof end;

theorem Th3: :: GRAPH_5:3

for D being finite set

for n being Element of NAT

for X being set st X = { x where x is Element of D * : len x <= n } holds

X is finite

for n being Element of NAT

for X being set st X = { x where x is Element of D * : len x <= n } holds

X is finite

proof end;

theorem Th4: :: GRAPH_5:4

for D being finite set

for k being Element of NAT st card D = k + 1 holds

ex x being Element of D ex C being Subset of D st

( D = C \/ {x} & card C = k )

for k being Element of NAT st card D = k + 1 holds

ex x being Element of D ex C being Subset of D st

( D = C \/ {x} & card C = k )

proof end;

definition

let D be set ;

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

:: original: Element

redefine mode Element of X -> FinSequence of D;

coherence

for b_{1} being Element of X holds b_{1} is FinSequence of D

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

:: original: Element

redefine mode Element of X -> FinSequence of D;

coherence

for b

proof end;

begin

Lm1: for n being Element of NAT

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

p . n = (p ^ q) . n

proof end;

Lm2: for n being Element of NAT

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

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

proof end;

theorem Th6: :: GRAPH_5:6

for p being FinSequence holds

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

p . n <> p . m ) iff p is one-to-one )

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

p . n <> p . m ) iff p is one-to-one )

proof end;

theorem Th7: :: GRAPH_5:7

for p being FinSequence holds

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

p . n <> p . m ) iff card (rng p) = len p )

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

p . n <> p . m ) iff card (rng p) = len p )

proof end;

theorem :: GRAPH_5:8

theorem Th9: :: GRAPH_5:9

for x being set

for q, p being FinSequence st q ^ <*x*> is one-to-one & rng (q ^ <*x*>) c= rng p holds

ex p1, p2 being FinSequence st

( p = (p1 ^ <*x*>) ^ p2 & rng q c= rng (p1 ^ p2) )

for q, p being FinSequence st q ^ <*x*> is one-to-one & rng (q ^ <*x*>) c= rng p holds

ex p1, p2 being FinSequence st

( p = (p1 ^ <*x*>) ^ p2 & rng q c= rng (p1 ^ p2) )

proof end;

begin

theorem Th10: :: GRAPH_5:10

for p, q being FinSequence

for G being Graph st p ^ q is Chain of G holds

( p is Chain of G & q is Chain of G )

for G being Graph st p ^ q is Chain of G holds

( p is Chain of G & q is Chain of G )

proof end;

theorem Th11: :: GRAPH_5:11

for p, q being FinSequence

for G being Graph st p ^ q is oriented Chain of G holds

( p is oriented Chain of G & q is oriented Chain of G )

for G being Graph st p ^ q is oriented Chain of G holds

( p is oriented Chain of G & q is oriented Chain of G )

proof end;

theorem Th12: :: GRAPH_5:12

for G being Graph

for p, q being oriented Chain of G st the Target of G . (p . (len p)) = the Source of G . (q . 1) holds

p ^ q is oriented Chain of G

for p, q being oriented Chain of G st the Target of G . (p . (len p)) = the Source of G . (q . 1) holds

p ^ q is oriented Chain of G

proof end;

begin

theorem Th14: :: GRAPH_5:14

for p, q being FinSequence

for G being Graph st p ^ q is oriented Simple Chain of G holds

( p is oriented Simple Chain of G & q is oriented Simple Chain of G )

for G being Graph st p ^ q is oriented Simple Chain of G holds

( p is oriented Simple Chain of G & q is oriented Simple Chain of G )

proof end;

theorem Th15: :: GRAPH_5:15

for G being Graph

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

pe is oriented Simple Chain of G

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

pe is oriented Simple Chain of G

proof end;

theorem Th16: :: GRAPH_5:16

for G being Graph

for p being oriented Simple Chain of G

for q being FinSequence of the carrier' of G st len p >= 1 & len q = 1 & the Source of G . (q . 1) = the Target of G . (p . (len p)) & the Source of G . (p . 1) <> the Target of G . (p . (len p)) & ( for k being Element of NAT holds

( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ) holds

p ^ q is oriented Simple Chain of G

for p being oriented Simple Chain of G

for q being FinSequence of the carrier' of G st len p >= 1 & len q = 1 & the Source of G . (q . 1) = the Target of G . (p . (len p)) & the Source of G . (p . 1) <> the Target of G . (p . (len p)) & ( for k being Element of NAT holds

( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ) holds

p ^ q is oriented Simple Chain of G

proof end;

begin

definition

let G be Graph;

let e be Element of the carrier' of G;

coherence

{( the Source of G . e),( the Target of G . e)} is set ;

end;
let e be Element of the carrier' of G;

coherence

{( the Source of G . e),( the Target of G . e)} is set ;

:: deftheorem defines vertices GRAPH_5:def 1 :

for G being Graph

for e being Element of the carrier' of G holds vertices e = {( the Source of G . e),( the Target of G . e)};

for G being Graph

for e being Element of the carrier' of G holds vertices e = {( the Source of G . e),( the Target of G . e)};

definition

let G be Graph;

let pe be FinSequence of the carrier' of G;

{ v where v is Vertex of G : ex i being Element of NAT st

( i in dom pe & v in vertices (pe /. i) ) } is Subset of the carrier of G

end;
let pe be FinSequence of the carrier' of G;

func vertices pe -> Subset of the carrier of G equals :: GRAPH_5:def 2

{ v where v is Vertex of G : ex i being Element of NAT st

( i in dom pe & v in vertices (pe /. i) ) } ;

coherence { v where v is Vertex of G : ex i being Element of NAT st

( i in dom pe & v in vertices (pe /. i) ) } ;

{ v where v is Vertex of G : ex i being Element of NAT st

( i in dom pe & v in vertices (pe /. i) ) } is Subset of the carrier of G

proof end;

:: deftheorem defines vertices GRAPH_5:def 2 :

for G being Graph

for pe being FinSequence of the carrier' of G holds vertices pe = { v where v is Vertex of G : ex i being Element of NAT st

( i in dom pe & v in vertices (pe /. i) ) } ;

for G being Graph

for pe being FinSequence of the carrier' of G holds vertices pe = { v where v is Vertex of G : ex i being Element of NAT st

( i in dom pe & v in vertices (pe /. i) ) } ;

theorem Th18: :: GRAPH_5:18

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 & the Source of G . (p . 1) <> the Target of G . (p . (len p)) holds

( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe )

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 & the Source of G . (p . 1) <> the Target of G . (p . (len p)) holds

( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe )

proof end;

theorem Th19: :: GRAPH_5:19

for V being set

for G being Graph

for pe being FinSequence of the carrier' of G holds

( vertices pe c= V iff for i being Nat st i in dom pe holds

vertices (pe /. i) c= V )

for G being Graph

for pe being FinSequence of the carrier' of G holds

( vertices pe c= V iff for i being Nat st i in dom pe holds

vertices (pe /. i) c= V )

proof end;

theorem Th20: :: GRAPH_5:20

for V being set

for G being Graph

for pe being FinSequence of the carrier' of G st not vertices pe c= V holds

ex i being Element of NAT ex q, r being FinSequence of the carrier' of G st

( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V & len q = i & pe = q ^ r & vertices q c= V )

for G being Graph

for pe being FinSequence of the carrier' of G st not vertices pe c= V holds

ex i being Element of NAT ex q, r being FinSequence of the carrier' of G st

( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V & len q = i & pe = q ^ r & vertices q c= V )

proof end;

theorem Th21: :: GRAPH_5:21

for G being Graph

for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe holds

vertices qe c= vertices pe

for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe holds

vertices qe c= vertices pe

proof end;

theorem Th22: :: GRAPH_5:22

for X, V being set

for G being Graph

for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & (vertices pe) \ X c= V holds

(vertices qe) \ X c= V

for G being Graph

for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & (vertices pe) \ X c= V holds

(vertices qe) \ X c= V

proof end;

theorem Th23: :: GRAPH_5:23

for X, V being set

for G being Graph

for pe, qe being FinSequence of the carrier' of G st (vertices (pe ^ qe)) \ X c= V holds

( (vertices pe) \ X c= V & (vertices qe) \ X c= V )

for G being Graph

for pe, qe being FinSequence of the carrier' of G st (vertices (pe ^ qe)) \ X c= V holds

( (vertices pe) \ X c= V & (vertices qe) \ X c= V )

proof end;

theorem Th24: :: GRAPH_5:24

for i being Element of NAT

for G being Graph

for pe being FinSequence of the carrier' of G

for v being Element of G st i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) holds

v in vertices pe

for G being Graph

for pe being FinSequence of the carrier' of G

for v being Element of G st i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) holds

v in vertices pe

proof end;

theorem Th25: :: GRAPH_5:25

for G being Graph

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

vertices pe = vertices (pe /. 1)

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

vertices pe = vertices (pe /. 1)

proof end;

theorem Th26: :: GRAPH_5:26

for G being Graph

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

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

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

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

proof end;

theorem Th27: :: GRAPH_5:27

for G being Graph

for pe being FinSequence of the carrier' of G

for p, q being oriented Chain of G st p = q ^ pe & len q >= 1 & len pe = 1 holds

vertices p = (vertices q) \/ {( the Target of G . (pe . 1))}

for pe being FinSequence of the carrier' of G

for p, q being oriented Chain of G st p = q ^ pe & len q >= 1 & len pe = 1 holds

vertices p = (vertices q) \/ {( the Target of G . (pe . 1))}

proof end;

theorem Th28: :: GRAPH_5:28

for G being Graph

for v being Element of G

for p being oriented Chain of G st v <> the Source of G . (p . 1) & v in vertices p holds

ex i being Element of NAT st

( 1 <= i & i <= len p & v = the Target of G . (p . i) )

for v being Element of G

for p being oriented Chain of G st v <> the Source of G . (p . 1) & v in vertices p holds

ex i being Element of NAT st

( 1 <= i & i <= len p & v = the Target of G . (p . i) )

proof end;

begin

:: deftheorem Def3 defines is_orientedpath_of GRAPH_5:def 3 :

for G being Graph

for p being oriented Chain of G

for v1, v2 being Element of G holds

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

for G being Graph

for p being oriented Chain of G

for v1, v2 being Element of G holds

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

definition

let G be Graph;

let v1, v2 be Element of G;

let p be oriented Chain of G;

let V be set ;

end;
let v1, v2 be Element of G;

let p be oriented Chain of G;

let V be set ;

pred p is_orientedpath_of v1,v2,V means :Def4: :: GRAPH_5:def 4

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

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

:: deftheorem Def4 defines is_orientedpath_of GRAPH_5:def 4 :

for G being Graph

for v1, v2 being Element of G

for p being oriented Chain of G

for V being set holds

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

for G being Graph

for v1, v2 being Element of G

for p being oriented Chain of G

for V being set holds

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

definition

let G be Graph;

let v1, v2 be Element of G;

{ p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } is Subset of ( the carrier' of G *)

end;
let v1, v2 be Element of G;

func OrientedPaths (v1,v2) -> Subset of ( the carrier' of G *) equals :: GRAPH_5:def 5

{ p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } ;

coherence { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } ;

{ p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } is Subset of ( the carrier' of G *)

proof end;

:: deftheorem defines OrientedPaths GRAPH_5:def 5 :

for G being Graph

for v1, v2 being Element of G holds OrientedPaths (v1,v2) = { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } ;

for G being Graph

for v1, v2 being Element of G holds OrientedPaths (v1,v2) = { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } ;

theorem Th29: :: GRAPH_5:29

for G being Graph

for v1, v2 being Element of G

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

( v1 in vertices p & v2 in vertices p )

for v1, v2 being Element of G

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

( v1 in vertices p & v2 in vertices p )

proof end;

theorem :: GRAPH_5:30

for x being set

for G being Graph

for v1, v2 being Element of G holds

( x in OrientedPaths (v1,v2) iff ex p being oriented Chain of G st

( p = x & p is_orientedpath_of v1,v2 ) ) ;

for G being Graph

for v1, v2 being Element of G holds

( x in OrientedPaths (v1,v2) iff ex p being oriented Chain of G st

( p = x & p is_orientedpath_of v1,v2 ) ) ;

theorem Th31: :: GRAPH_5:31

for V being set

for G being Graph

for v1, v2 being Element of G

for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds

v1 in V

for G being Graph

for v1, v2 being Element of G

for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds

v1 in V

proof end;

theorem Th32: :: GRAPH_5:32

for V, U being set

for G being Graph

for v1, v2 being Element of G

for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & V c= U holds

p is_orientedpath_of v1,v2,U

for G being Graph

for v1, v2 being Element of G

for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & V c= U holds

p is_orientedpath_of v1,v2,U

proof end;

theorem Th33: :: GRAPH_5:33

for G being Graph

for pe being FinSequence of the carrier' of G

for v1, v2, v3 being Element of G

for p being oriented Chain of G st len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 holds

ex q being oriented Chain of G st

( q = p ^ pe & q is_orientedpath_of v1,v3 )

for pe being FinSequence of the carrier' of G

for v1, v2, v3 being Element of G

for p being oriented Chain of G st len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 holds

ex q being oriented Chain of G st

( q = p ^ pe & q is_orientedpath_of v1,v3 )

proof end;

theorem Th34: :: GRAPH_5:34

for V being set

for G being Graph

for pe being FinSequence of the carrier' of G

for v1, v2, v3 being Element of G

for q, p being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds

q is_orientedpath_of v1,v3,V \/ {v2}

for G being Graph

for pe being FinSequence of the carrier' of G

for v1, v2, v3 being Element of G

for q, p being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds

q is_orientedpath_of v1,v3,V \/ {v2}

proof end;

begin

definition

let G be Graph;

let p be oriented Chain of G;

let v1, v2 be Element of G;

end;
let p be oriented Chain of G;

let v1, v2 be Element of G;

pred p is_acyclicpath_of v1,v2 means :Def6: :: GRAPH_5:def 6

( p is Simple & p is_orientedpath_of v1,v2 );

( p is Simple & p is_orientedpath_of v1,v2 );

:: deftheorem Def6 defines is_acyclicpath_of GRAPH_5:def 6 :

for G being Graph

for p being oriented Chain of G

for v1, v2 being Element of G holds

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

for G being Graph

for p being oriented Chain of G

for v1, v2 being Element of G holds

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

definition

let G be Graph;

let p be oriented Chain of G;

let v1, v2 be Element of G;

let V be set ;

end;
let p be oriented Chain of G;

let v1, v2 be Element of G;

let V be set ;

pred p is_acyclicpath_of v1,v2,V means :Def7: :: GRAPH_5:def 7

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

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

:: deftheorem Def7 defines is_acyclicpath_of GRAPH_5:def 7 :

for G being Graph

for p being oriented Chain of G

for v1, v2 being Element of G

for V being set holds

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

for G being Graph

for p being oriented Chain of G

for v1, v2 being Element of G

for V being set holds

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

definition

let G be Graph;

let v1, v2 be Element of G;

{ p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } is Subset of ( the carrier' of G *)

end;
let v1, v2 be Element of G;

func AcyclicPaths (v1,v2) -> Subset of ( the carrier' of G *) equals :: GRAPH_5:def 8

{ p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } ;

coherence { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } ;

{ p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } is Subset of ( the carrier' of G *)

proof end;

:: deftheorem defines AcyclicPaths GRAPH_5:def 8 :

for G being Graph

for v1, v2 being Element of G holds AcyclicPaths (v1,v2) = { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } ;

for G being Graph

for v1, v2 being Element of G holds AcyclicPaths (v1,v2) = { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } ;

definition

let G be Graph;

let v1, v2 be Element of G;

let V be set ;

{ p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } is Subset of ( the carrier' of G *)

end;
let v1, v2 be Element of G;

let V be set ;

func AcyclicPaths (v1,v2,V) -> Subset of ( the carrier' of G *) equals :: GRAPH_5:def 9

{ p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } ;

coherence { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } ;

{ p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } is Subset of ( the carrier' of G *)

proof end;

:: deftheorem defines AcyclicPaths GRAPH_5:def 9 :

for G being Graph

for v1, v2 being Element of G

for V being set holds AcyclicPaths (v1,v2,V) = { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } ;

for G being Graph

for v1, v2 being Element of G

for V being set holds AcyclicPaths (v1,v2,V) = { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } ;

definition

let G be Graph;

let p be oriented Chain of G;

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

end;
let p be oriented Chain of G;

func AcyclicPaths p -> Subset of ( the carrier' of G *) equals :: GRAPH_5:def 10

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

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

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

proof end;

:: deftheorem defines AcyclicPaths GRAPH_5:def 10 :

for G being Graph

for p being oriented Chain of G holds AcyclicPaths p = { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } ;

for G being Graph

for p being oriented Chain of G holds AcyclicPaths p = { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } ;

definition

let G be Graph;

{ q where q is oriented Simple Chain of G : verum } is Subset of ( the carrier' of G *)

end;
func AcyclicPaths G -> Subset of ( the carrier' of G *) equals :: GRAPH_5:def 11

{ q where q is oriented Simple Chain of G : verum } ;

coherence { q where q is oriented Simple Chain of G : verum } ;

{ q where q is oriented Simple Chain of G : verum } is Subset of ( the carrier' of G *)

proof end;

:: deftheorem defines AcyclicPaths GRAPH_5:def 11 :

for G being Graph holds AcyclicPaths G = { q where q is oriented Simple Chain of G : verum } ;

for G being Graph holds AcyclicPaths G = { q where q is oriented Simple Chain of G : verum } ;

theorem :: GRAPH_5:35

for G being Graph

for v1, v2 being Element of G

for p being oriented Chain of G st p = {} holds

not p is_acyclicpath_of v1,v2

for v1, v2 being Element of G

for p being oriented Chain of G st p = {} holds

not p is_acyclicpath_of v1,v2

proof end;

theorem :: GRAPH_5:36

for G being Graph

for v1, v2 being Element of G

for p being oriented Chain of G st p is_acyclicpath_of v1,v2 holds

p is_orientedpath_of v1,v2 by Def6;

for v1, v2 being Element of G

for p being oriented Chain of G st p is_acyclicpath_of v1,v2 holds

p is_orientedpath_of v1,v2 by Def6;

theorem Th40: :: GRAPH_5:40

for G being Graph

for v1, v2 being Element of G

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

AcyclicPaths p c= AcyclicPaths (v1,v2)

for v1, v2 being Element of G

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

AcyclicPaths p c= AcyclicPaths (v1,v2)

proof end;

theorem Th41: :: GRAPH_5:41

for V being set

for G being Graph

for v1, v2 being Element of G

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

AcyclicPaths p c= AcyclicPaths (v1,v2,V)

for G being Graph

for v1, v2 being Element of G

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

AcyclicPaths p c= AcyclicPaths (v1,v2,V)

proof end;

theorem Th43: :: GRAPH_5:43

for G being Graph

for v1, v2 being Element of G

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

( AcyclicPaths p <> {} & AcyclicPaths (v1,v2) <> {} )

for v1, v2 being Element of G

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

( AcyclicPaths p <> {} & AcyclicPaths (v1,v2) <> {} )

proof end;

theorem Th44: :: GRAPH_5:44

for V being set

for G being Graph

for v1, v2 being Element of G

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

( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} )

for G being Graph

for v1, v2 being Element of G

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

( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} )

proof end;

theorem Th45: :: GRAPH_5:45

for V being set

for G being Graph

for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) c= AcyclicPaths G

for G being Graph

for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) c= AcyclicPaths G

proof end;

begin

definition

for b_{1} being Subset of REAL holds

( b_{1} = Real>=0 iff b_{1} = { r where r is Real : r >= 0 } )
by REAL_1:1;

coherence

Real>=0 is Subset of REAL by ARYTM_0:1;

end;

:: original: Real>=0

redefine func Real>=0 -> Subset of REAL equals :: GRAPH_5:def 12

{ r where r is Real : r >= 0 } ;

compatibility redefine func Real>=0 -> Subset of REAL equals :: GRAPH_5:def 12

{ r where r is Real : r >= 0 } ;

for b

( b

coherence

Real>=0 is Subset of REAL by ARYTM_0:1;

:: deftheorem Def13 defines is_weight>=0of GRAPH_5:def 13 :

for G being Graph

for W being Function holds

( W is_weight>=0of G iff W is Function of the carrier' of G,Real>=0 );

for G being Graph

for W being Function holds

( W is_weight>=0of G iff W is Function of the carrier' of G,Real>=0 );

:: deftheorem Def14 defines is_weight_of GRAPH_5:def 14 :

for G being Graph

for W being Function holds

( W is_weight_of G iff W is Function of the carrier' of G,REAL );

for G being Graph

for W being Function holds

( W is_weight_of G iff W is Function of the carrier' of G,REAL );

definition

let G be Graph;

let p be FinSequence of the carrier' of G;

let W be Function;

assume A1: W is_weight_of G ;

ex b_{1} being FinSequence of REAL st

( dom p = dom b_{1} & ( for i being Element of NAT st i in dom p holds

b_{1} . i = W . (p . i) ) )

for b_{1}, b_{2} being FinSequence of REAL st dom p = dom b_{1} & ( for i being Element of NAT st i in dom p holds

b_{1} . i = W . (p . i) ) & dom p = dom b_{2} & ( for i being Element of NAT st i in dom p holds

b_{2} . i = W . (p . i) ) holds

b_{1} = b_{2}

end;
let p be FinSequence of the carrier' of G;

let W be Function;

assume A1: W is_weight_of G ;

func RealSequence (p,W) -> FinSequence of REAL means :Def15: :: GRAPH_5:def 15

( dom p = dom it & ( for i being Element of NAT st i in dom p holds

it . i = W . (p . i) ) );

existence ( dom p = dom it & ( for i being Element of NAT st i in dom p holds

it . i = W . (p . i) ) );

ex b

( dom p = dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def15 defines RealSequence GRAPH_5:def 15 :

for G being Graph

for p being FinSequence of the carrier' of G

for W being Function st W is_weight_of G holds

for b_{4} being FinSequence of REAL holds

( b_{4} = RealSequence (p,W) iff ( dom p = dom b_{4} & ( for i being Element of NAT st i in dom p holds

b_{4} . i = W . (p . i) ) ) );

for G being Graph

for p being FinSequence of the carrier' of G

for W being Function st W is_weight_of G holds

for b

( b

b

definition

let G be Graph;

let p be FinSequence of the carrier' of G;

let W be Function;

coherence

Sum (RealSequence (p,W)) is Real ;

end;
let p be FinSequence of the carrier' of G;

let W be Function;

coherence

Sum (RealSequence (p,W)) is Real ;

:: deftheorem defines cost GRAPH_5:def 16 :

for G being Graph

for p being FinSequence of the carrier' of G

for W being Function holds cost (p,W) = Sum (RealSequence (p,W));

for G being Graph

for p being FinSequence of the carrier' of G

for W being Function holds cost (p,W) = Sum (RealSequence (p,W));

theorem Th47: :: GRAPH_5:47

for W being Function

for G being Graph

for pe being FinSequence of the carrier' of G

for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence (pe,W) holds

for i being Element of NAT st i in dom f holds

f . i >= 0

for G being Graph

for pe being FinSequence of the carrier' of G

for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence (pe,W) holds

for i being Element of NAT st i in dom f holds

f . i >= 0

proof end;

theorem Th48: :: GRAPH_5:48

for i being Element of NAT

for W being Function

for G being Graph

for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & W is_weight_of G & i in dom qe holds

ex j being Element of NAT st

( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i )

for W being Function

for G being Graph

for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & W is_weight_of G & i in dom qe holds

ex j being Element of NAT st

( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i )

proof end;

Lm3: for f being FinSequence of REAL holds

( ( for y being Real st y in rng f holds

y >= 0 ) iff for i being Nat st i in dom f holds

f . i >= 0 )

proof end;

Lm4: for p, q, r being FinSequence of REAL st r = p ^ q & ( for x being Real st x in rng r holds

x >= 0 ) holds

( ( for i being Element of NAT st i in dom p holds

p . i >= 0 ) & ( for i being Element of NAT st i in dom q holds

q . i >= 0 ) )

proof end;

theorem :: GRAPH_5:49

for W being Function

for G being Graph

for qe, pe being FinSequence of the carrier' of G st len qe = 1 & rng qe c= rng pe & W is_weight>=0of G holds

cost (qe,W) <= cost (pe,W)

for G being Graph

for qe, pe being FinSequence of the carrier' of G st len qe = 1 & rng qe c= rng pe & W is_weight>=0of G holds

cost (qe,W) <= cost (pe,W)

proof end;

theorem Th50: :: GRAPH_5:50

for W being Function

for G being Graph

for pe being FinSequence of the carrier' of G st W is_weight>=0of G holds

cost (pe,W) >= 0

for G being Graph

for pe being FinSequence of the carrier' of G st W is_weight>=0of G holds

cost (pe,W) >= 0

proof end;

theorem Th51: :: GRAPH_5:51

for W being Function

for G being Graph

for pe being FinSequence of the carrier' of G st pe = {} & W is_weight_of G holds

cost (pe,W) = 0

for G being Graph

for pe being FinSequence of the carrier' of G st pe = {} & W is_weight_of G holds

cost (pe,W) = 0

proof end;

theorem Th52: :: GRAPH_5:52

for W being Function

for G being Graph

for v1, v2 being Element of G

for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2) holds

ex pe being FinSequence of the carrier' of G st

( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds

cost (pe,W) <= cost (qe,W) ) )

for G being Graph

for v1, v2 being Element of G

for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2) holds

ex pe being FinSequence of the carrier' of G st

( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds

cost (pe,W) <= cost (qe,W) ) )

proof end;

theorem Th53: :: GRAPH_5:53

for V being set

for W being Function

for G being Graph

for v1, v2 being Element of G

for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) holds

ex pe being FinSequence of the carrier' of G st

( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds

cost (pe,W) <= cost (qe,W) ) )

for W being Function

for G being Graph

for v1, v2 being Element of G

for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) holds

ex pe being FinSequence of the carrier' of G st

( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds

cost (pe,W) <= cost (qe,W) ) )

proof end;

theorem Th54: :: GRAPH_5:54

for W being Function

for G being Graph

for pe, qe being FinSequence of the carrier' of G st W is_weight_of G holds

cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W))

for G being Graph

for pe, qe being FinSequence of the carrier' of G st W is_weight_of G holds

cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W))

proof end;

theorem Th55: :: GRAPH_5:55

for W being Function

for G being Graph

for qe, pe being FinSequence of the carrier' of G st qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G holds

cost (qe,W) <= cost (pe,W)

for G being Graph

for qe, pe being FinSequence of the carrier' of G st qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G holds

cost (qe,W) <= cost (pe,W)

proof end;

theorem Th56: :: GRAPH_5:56

for W being Function

for G being Graph

for pe being FinSequence of the carrier' of G

for p being oriented Chain of G st pe in AcyclicPaths p & W is_weight>=0of G holds

cost (pe,W) <= cost (p,W)

for G being Graph

for pe being FinSequence of the carrier' of G

for p being oriented Chain of G st pe in AcyclicPaths p & W is_weight>=0of G holds

cost (pe,W) <= cost (p,W)

proof end;

begin

definition

let G be Graph;

let v1, v2 be Vertex of G;

let p be oriented Chain of G;

let W be Function;

end;
let v1, v2 be Vertex of G;

let p be oriented Chain of G;

let W be Function;

pred p is_shortestpath_of v1,v2,W means :Def17: :: GRAPH_5:def 17

( p is_orientedpath_of v1,v2 & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds

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

( p is_orientedpath_of v1,v2 & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds

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

:: deftheorem Def17 defines is_shortestpath_of GRAPH_5:def 17 :

for G being Graph

for v1, v2 being Vertex of G

for p being oriented Chain of G

for W being Function holds

( p is_shortestpath_of v1,v2,W iff ( p is_orientedpath_of v1,v2 & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds

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

for G being Graph

for v1, v2 being Vertex of G

for p being oriented Chain of G

for W being Function holds

( p is_shortestpath_of v1,v2,W iff ( p is_orientedpath_of v1,v2 & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds

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

definition

let G be Graph;

let v1, v2 be Vertex of G;

let p be oriented Chain of G;

let V be set ;

let W be Function;

end;
let v1, v2 be Vertex of G;

let p be oriented Chain of G;

let V be set ;

let W be Function;

pred p is_shortestpath_of v1,v2,V,W means :Def18: :: GRAPH_5:def 18

( p is_orientedpath_of v1,v2,V & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds

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

( p is_orientedpath_of v1,v2,V & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds

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

:: deftheorem Def18 defines is_shortestpath_of GRAPH_5:def 18 :

for G being Graph

for v1, v2 being Vertex of G

for p being oriented Chain of G

for V being set

for W being Function holds

( p is_shortestpath_of v1,v2,V,W iff ( p is_orientedpath_of v1,v2,V & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds

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

for G being Graph

for v1, v2 being Vertex of G

for p being oriented Chain of G

for V being set

for W being Function holds

( p is_shortestpath_of v1,v2,V,W iff ( p is_orientedpath_of v1,v2,V & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds

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

begin

Lm5: for G being finite Graph holds AcyclicPaths G is finite

proof end;

Lm6: for G being finite Graph

for P being oriented Chain of G holds AcyclicPaths P is finite

proof end;

Lm7: for G being finite Graph

for v1, v2 being Element of G holds AcyclicPaths (v1,v2) is finite

proof end;

Lm8: for V being set

for G being finite Graph

for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) is finite

proof end;

registration
end;

registration
end;

registration

let G be finite Graph;

let v1, v2 be Element of G;

let V be set ;

coherence

AcyclicPaths (v1,v2,V) is finite by Lm8;

end;
let v1, v2 be Element of G;

let V be set ;

coherence

AcyclicPaths (v1,v2,V) is finite by Lm8;

theorem :: GRAPH_5:59

for W being Function

for G being finite Graph

for v1, v2 being Element of G st AcyclicPaths (v1,v2) <> {} holds

ex pe being FinSequence of the carrier' of G st

( pe in AcyclicPaths (v1,v2) & ( for qe being FinSequence of the carrier' of G st qe in AcyclicPaths (v1,v2) holds

cost (pe,W) <= cost (qe,W) ) ) by Th52;

for G being finite Graph

for v1, v2 being Element of G st AcyclicPaths (v1,v2) <> {} holds

ex pe being FinSequence of the carrier' of G st

( pe in AcyclicPaths (v1,v2) & ( for qe being FinSequence of the carrier' of G st qe in AcyclicPaths (v1,v2) holds

cost (pe,W) <= cost (qe,W) ) ) by Th52;

theorem :: GRAPH_5:60

for V being set

for W being Function

for G being finite Graph

for v1, v2 being Element of G st AcyclicPaths (v1,v2,V) <> {} holds

ex pe being FinSequence of the carrier' of G st

( pe in AcyclicPaths (v1,v2,V) & ( for qe being FinSequence of the carrier' of G st qe in AcyclicPaths (v1,v2,V) holds

cost (pe,W) <= cost (qe,W) ) ) by Th53;

for W being Function

for G being finite Graph

for v1, v2 being Element of G st AcyclicPaths (v1,v2,V) <> {} holds

ex pe being FinSequence of the carrier' of G st

( pe in AcyclicPaths (v1,v2,V) & ( for qe being FinSequence of the carrier' of G st qe in AcyclicPaths (v1,v2,V) holds

cost (pe,W) <= cost (qe,W) ) ) by Th53;

theorem :: GRAPH_5:61

for W being Function

for G being finite Graph

for P being oriented Chain of G

for v1, v2 being Element of G st P is_orientedpath_of v1,v2 & W is_weight>=0of G holds

ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W

for G being finite Graph

for P being oriented Chain of G

for v1, v2 being Element of G st P is_orientedpath_of v1,v2 & W is_weight>=0of G holds

ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W

proof end;

theorem Th62: :: GRAPH_5:62

for V being set

for W being Function

for G being finite Graph

for P being oriented Chain of G

for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds

ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W

for W being Function

for G being finite Graph

for P being oriented Chain of G

for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds

ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W

proof end;

begin

theorem Th63: :: GRAPH_5:63

for V being set

for W being Function

for G being finite Graph

for P being oriented Chain of G

for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & ( for Q being oriented Chain of G

for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds

cost (P,W) <= cost (Q,W) ) holds

P is_shortestpath_of v1,v2,W

for W being Function

for G being finite Graph

for P being oriented Chain of G

for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & ( for Q being oriented Chain of G

for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds

cost (P,W) <= cost (Q,W) ) holds

P is_shortestpath_of v1,v2,W

proof end;

theorem :: GRAPH_5:64

for V, U being set

for W being Function

for G being finite Graph

for P being oriented Chain of G

for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & V c= U & ( for Q being oriented Chain of G

for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds

cost (P,W) <= cost (Q,W) ) holds

P is_shortestpath_of v1,v2,U,W

for W being Function

for G being finite Graph

for P being oriented Chain of G

for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & V c= U & ( for Q being oriented Chain of G

for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds

cost (P,W) <= cost (Q,W) ) holds

P is_shortestpath_of v1,v2,U,W

proof end;

definition

let G be Graph;

let pe be FinSequence of the carrier' of G;

let V be set ;

let v1 be Vertex of G;

let W be Function;

end;
let pe be FinSequence of the carrier' of G;

let V be set ;

let v1 be Vertex of G;

let W be Function;

pred pe islongestInShortestpath V,v1,W means :Def19: :: GRAPH_5:def 19

for v being Vertex of G st v in V & v <> v1 holds

ex q being oriented Chain of G st

( q is_shortestpath_of v1,v,V,W & cost (q,W) <= cost (pe,W) );

for v being Vertex of G st v in V & v <> v1 holds

ex q being oriented Chain of G st

( q is_shortestpath_of v1,v,V,W & cost (q,W) <= cost (pe,W) );

:: deftheorem Def19 defines islongestInShortestpath GRAPH_5:def 19 :

for G being Graph

for pe being FinSequence of the carrier' of G

for V being set

for v1 being Vertex of G

for W being Function holds

( pe islongestInShortestpath V,v1,W iff for v being Vertex of G st v in V & v <> v1 holds

ex q being oriented Chain of G st

( q is_shortestpath_of v1,v,V,W & cost (q,W) <= cost (pe,W) ) );

for G being Graph

for pe being FinSequence of the carrier' of G

for V being set

for v1 being Vertex of G

for W being Function holds

( pe islongestInShortestpath V,v1,W iff for v being Vertex of G st v in V & v <> v1 holds

ex q being oriented Chain of G st

( q is_shortestpath_of v1,v,V,W & cost (q,W) <= cost (pe,W) ) );

:: Dijkstra's shortest path algorithm

theorem :: GRAPH_5:65

for e, V being set

for W being Function

for G being oriented finite Graph

for P, Q, R being oriented Chain of G

for v1, v2, v3 being Element of G st e in the carrier' of G & W is_weight>=0of G & len P >= 1 & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & R = P ^ <*e*> & Q is_shortestpath_of v1,v3,V,W & e orientedly_joins v2,v3 & P islongestInShortestpath V,v1,W holds

( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) )

for W being Function

for G being oriented finite Graph

for P, Q, R being oriented Chain of G

for v1, v2, v3 being Element of G st e in the carrier' of G & W is_weight>=0of G & len P >= 1 & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & R = P ^ <*e*> & Q is_shortestpath_of v1,v3,V,W & e orientedly_joins v2,v3 & P islongestInShortestpath V,v1,W holds

( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) )

proof end;