:: GRAPH_5 semantic presentation

theorem Th1: :: GRAPH_5:1

for b₁ being finite Function holds card (rng b₁) <= card (dom b₁)

proof end;

theorem Th2: :: GRAPH_5:2

for b₁ being set
for b₂, b₃ being Function st rng b₂ c= rng b₃ & b₁ in dom b₂ holds
ex b₄ being set st
( b₄ in dom b₃ & b₂ . b₁ = b₃ . b₄ )

proof end;

scheme :: GRAPH_5:sch 1
s1{ F₁() -> set , F₂() -> set , F₃( Element of F₂()) -> set } :

ex b₁ being Function st
( dom b₁ = F₁() & ( for b₂ being Element of F₂() st b₂ in F₁() holds
b₁ . b₂ = F₃(b₂) ) )

proof end;

theorem Th3: :: GRAPH_5:3

for b₁ being finite set
for b₂ being Nat
for b₃ being set st b₃ = { b₄ where B is Element of b₁ * : ( 1 <= len b₄ & len b₄ <= b₂ ) } holds
b₃ is finite

proof end;

theorem Th4: :: GRAPH_5:4

for b₁ being finite set
for b₂ being Nat
for b₃ being set st b₃ = { b₄ where B is Element of b₁ * : len b₄ <= b₂ } holds
b₃ is finite

proof end;

theorem Th5: :: GRAPH_5:5

for b₁ being finite set holds
( card b₁ <> 0 iff b₁ <> {} )

proof end;

theorem Th6: :: GRAPH_5:6

for b₁ being finite set
for b₂ being Nat st card b₁ = b₂ + 1 holds
ex b₃ being Element of b₁ex b₄ being Subset of b₁ st
( b₁ = b₄ \/ {b₃} & card b₄ = b₂ )

proof end;

theorem Th7: :: GRAPH_5:7

for b₁ being finite set st card b₁ = 1 holds
ex b₂ being Element of b₁ st b₁ = {b₂}

proof end;

scheme :: GRAPH_5:sch 2
s2{ F₁() -> non empty finite set , F₂( Element of F₁()) -> Real } :

ex b₁ being Element of F₁() st
for b₂ being Element of F₁() holds F₂(b₁) <= F₂(b₂)

proof end;

definition

let c₁ be set ;
let c₂ be non empty Subset of (c₁ * );
redefine mode Element as Element of c₂ -> FinSequence of a₁;
coherence

proof end;

end;

theorem Th8: :: GRAPH_5:8

for b₁ being FinSequence holds
( b₁ <> {} iff len b₁ >= 1 )

proof end;

Lemma9: for b₁ being Nat
for b₂, b₃ being FinSequence st 1 <= b₁ & b₁ <= len b₂ holds
b₂ . b₁ = (b₂ ^ b₃) . b₁

proof end;

Lemma10: for b₁ being Nat
for b₂, b₃ being FinSequence st 1 <= b₁ & b₁ <= len b₂ holds
b₂ . b₁ = (b₃ ^ b₂) . ((len b₃) + b₁)

proof end;

theorem Th9: :: GRAPH_5:9

for b₁ being FinSequence holds
( ( for b₂, b₃ being Nat st 1 <= b₂ & b₂ < b₃ & b₃ <= len b₁ holds
b₁ . b₂ <> b₁ . b₃ ) iff b₁ is one-to-one )

proof end;

theorem Th10: :: GRAPH_5:10

for b₁ being FinSequence holds
( ( for b₂, b₃ being Nat st 1 <= b₂ & b₂ < b₃ & b₃ <= len b₁ holds
b₁ . b₂ <> b₁ . b₃ ) iff card (rng b₁) = len b₁ )

proof end;

theorem Th11: :: GRAPH_5:11

for b₁ being Nat
for b₂ being Graph
for b₃ being FinSequence of the Edges of b₂ st b₁ in dom b₃ holds
( the Source of b₂ . (b₃ . b₁) in the Vertices of b₂ & the Target of b₂ . (b₃ . b₁) in the Vertices of b₂ )

proof end;

theorem Th12: :: GRAPH_5:12

for b₁ being set
for b₂, b₃ being FinSequence st b₂ ^ <*b₁*> is one-to-one & rng (b₂ ^ <*b₁*>) c= rng b₃ holds
ex b₄, b₅ being FinSequence st
( b₃ = (b₄ ^ <*b₁*>) ^ b₅ & rng b₂ c= rng (b₄ ^ b₅) )

proof end;

theorem Th13: :: GRAPH_5:13

for b₁, b₂ being FinSequence
for b₃ being Graph st b₁ ^ b₂ is Chain of b₃ holds
( b₁ is Chain of b₃ & b₂ is Chain of b₃ )

proof end;

theorem Th14: :: GRAPH_5:14

for b₁, b₂ being FinSequence
for b₃ being Graph st b₁ ^ b₂ is oriented Chain of b₃ holds
( b₁ is oriented Chain of b₃ & b₂ is oriented Chain of b₃ )

proof end;

theorem Th15: :: GRAPH_5:15

for b₁ being Graph
for b₂, b₃ being oriented Chain of b₁ st the Target of b₁ . (b₂ . (len b₂)) = the Source of b₁ . (b₃ . 1) holds
b₂ ^ b₃ is oriented Chain of b₁

proof end;

theorem Th16: :: GRAPH_5:16

for b₁ being Graph holds {} is oriented Simple Chain of b₁

proof end;

theorem Th17: :: GRAPH_5:17

for b₁, b₂ being FinSequence
for b₃ being Graph st b₁ ^ b₂ is oriented Simple Chain of b₃ holds
( b₁ is oriented Simple Chain of b₃ & b₂ is oriented Simple Chain of b₃ )

proof end;

theorem Th18: :: GRAPH_5:18

for b₁ being Graph
for b₂ being FinSequence of the Edges of b₁ st len b₂ = 1 holds
b₂ is oriented Simple Chain of b₁

proof end;

theorem Th19: :: GRAPH_5:19

for b₁ being Graph
for b₂ being oriented Simple Chain of b₁
for b₃ being FinSequence of the Edges of b₁ st len b₂ >= 1 & len b₃ = 1 & the Source of b₁ . (b₃ . 1) = the Target of b₁ . (b₂ . (len b₂)) & the Source of b₁ . (b₂ . 1) <> the Target of b₁ . (b₂ . (len b₂)) & ( for b₄ being Nat holds
( not 1 <= b₄ or not b₄ <= len b₂ or not the Target of b₁ . (b₂ . b₄) = the Target of b₁ . (b₃ . 1) ) ) holds
b₂ ^ b₃ is oriented Simple Chain of b₁

proof end;

theorem Th20: :: GRAPH_5:20

for b₁ being Graph
for b₂ being oriented Simple Chain of b₁ holds b₂ is one-to-one

proof end;

definition

let c₁ be Graph;
let c₂ be Element of the Edges of c₁;
func vertices c₂ -> set equals :: GRAPH_5:def 1
{(the Source of a₁ . a₂),(the Target of a₁ . a₂)};
coherence ;

end;

:: deftheorem Def1 defines vertices GRAPH_5:def 1 :

definition

let c₁ be Graph;
let c₂ be FinSequence of the Edges of c₁;
func vertices c₂ -> Subset of the Vertices of a₁ equals :: GRAPH_5:def 2
{ b₁ where B is Vertex of a₁ : ex b₁ being Nat st
( b₂ in dom a₂ & b₁ in vertices (a₂ /. b₂) ) } ;
coherence

proof end;

end;

:: deftheorem Def2 defines vertices GRAPH_5:def 2 :

theorem Th21: :: GRAPH_5:21

for b₁ being Graph
for b₂, b₃ being FinSequence of the Edges of b₁
for b₄ being oriented Simple Chain of b₁ st b₄ = b₂ ^ b₃ & len b₂ >= 1 & len b₃ >= 1 & the Source of b₁ . (b₄ . 1) <> the Target of b₁ . (b₄ . (len b₄)) holds
( not the Source of b₁ . (b₄ . 1) in vertices b₃ & not the Target of b₁ . (b₄ . (len b₄)) in vertices b₂ )

proof end;

theorem Th22: :: GRAPH_5:22

for b₁ being set
for b₂ being Graph
for b₃ being FinSequence of the Edges of b₂ holds
( vertices b₃ c= b₁ iff for b₄ being Nat st b₄ in dom b₃ holds
vertices (b₃ /. b₄) c= b₁ )

proof end;

theorem Th23: :: GRAPH_5:23

for b₁ being set
for b₂ being Graph
for b₃ being FinSequence of the Edges of b₂ st not vertices b₃ c= b₁ holds
ex b₄ being Natex b₅, b₆ being FinSequence of the Edges of b₂ st
( b₄ + 1 <= len b₃ & not vertices (b₃ /. (b₄ + 1)) c= b₁ & len b₅ = b₄ & b₃ = b₅ ^ b₆ & vertices b₅ c= b₁ )

proof end;

theorem Th24: :: GRAPH_5:24

for b₁ being Graph
for b₂, b₃ being FinSequence of the Edges of b₁ st rng b₂ c= rng b₃ holds
vertices b₂ c= vertices b₃

proof end;

theorem Th25: :: GRAPH_5:25

for b₁, b₂ being set
for b₃ being Graph
for b₄, b₅ being FinSequence of the Edges of b₃ st rng b₄ c= rng b₅ & (vertices b₅) \ b₁ c= b₂ holds
(vertices b₄) \ b₁ c= b₂

proof end;

theorem Th26: :: GRAPH_5:26

for b₁, b₂ being set
for b₃ being Graph
for b₄, b₅ being FinSequence of the Edges of b₃ st (vertices (b₄ ^ b₅)) \ b₁ c= b₂ holds
( (vertices b₄) \ b₁ c= b₂ & (vertices b₅) \ b₁ c= b₂ )

proof end;

theorem Th27: :: GRAPH_5:27

for b₁ being Graph
for b₂ being Element of the Vertices of b₁
for b₃ being Element of the Edges of b₁ st ( b₂ = the Source of b₁ . b₃ or b₂ = the Target of b₁ . b₃ ) holds
b₂ in vertices b₃ by TARSKI:def 2;

theorem Th28: :: GRAPH_5:28

for b₁ being Nat
for b₂ being Graph
for b₃ being FinSequence of the Edges of b₂
for b₄ being Element of the Vertices of b₂ st b₁ in dom b₃ & ( b₄ = the Source of b₂ . (b₃ . b₁) or b₄ = the Target of b₂ . (b₃ . b₁) ) holds
b₄ in vertices b₃

proof end;

theorem Th29: :: GRAPH_5:29

for b₁ being Graph
for b₂ being FinSequence of the Edges of b₁ st len b₂ = 1 holds
vertices b₂ = vertices (b₂ /. 1)

proof end;

theorem Th30: :: GRAPH_5:30

for b₁ being Graph
for b₂, b₃ being FinSequence of the Edges of b₁ holds
( vertices b₂ c= vertices (b₂ ^ b₃) & vertices b₃ c= vertices (b₂ ^ b₃) )

proof end;

theorem Th31: :: GRAPH_5:31

for b₁ being Graph
for b₂ being FinSequence of the Edges of b₁
for b₃, b₄ being oriented Chain of b₁ st b₃ = b₄ ^ b₂ & len b₄ >= 1 & len b₂ = 1 holds
vertices b₃ = (vertices b₄) \/ {(the Target of b₁ . (b₂ . 1))}

proof end;

theorem Th32: :: GRAPH_5:32

for b₁ being Graph
for b₂ being Element of the Vertices of b₁
for b₃ being oriented Chain of b₁ st b₂ <> the Source of b₁ . (b₃ . 1) & b₂ in vertices b₃ holds
ex b₄ being Nat st
( 1 <= b₄ & b₄ <= len b₃ & b₂ = the Target of b₁ . (b₃ . b₄) )

proof end;

definition

let c₁ be Graph;
let c₂ be oriented Chain of c₁;
let c₃, c₄ be Element of the Vertices of c₁;
pred c₂ is_orientedpath_of c₃,c₄ means :Def3: :: GRAPH_5:def 3
( a₂ <> {} & the Source of a₁ . (a₂ . 1) = a₃ & the Target of a₁ . (a₂ . (len a₂)) = a₄ );

end;

:: deftheorem Def3 defines is_orientedpath_of GRAPH_5:def 3 :

definition

let c₁ be Graph;
let c₂, c₃ be Element of the Vertices of c₁;
let c₄ be oriented Chain of c₁;
let c₅ be set ;
pred c₄ is_orientedpath_of c₂,c₃,c₅ means :Def4: :: GRAPH_5:def 4
( a₄ is_orientedpath_of a₂,a₃ & (vertices a₄) \ {a₃} c= a₅ );

end;

:: deftheorem Def4 defines is_orientedpath_of GRAPH_5:def 4 :

definition

let c₁ be Graph;
let c₂, c₃ be Element of the Vertices of c₁;
func OrientedPaths c₂,c₃ -> Subset of (the Edges of a₁ * ) equals :: GRAPH_5:def 5
{ b₁ where B is oriented Chain of a₁ : b₁ is_orientedpath_of a₂,a₃ } ;
coherence

proof end;

end;

:: deftheorem Def5 defines OrientedPaths GRAPH_5:def 5 :

theorem Th33: :: GRAPH_5:33

for b₁ being Graph
for b₂, b₃ being Element of the Vertices of b₁
for b₄ being oriented Chain of b₁ st b₄ is_orientedpath_of b₂,b₃ holds
( b₂ in vertices b₄ & b₃ in vertices b₄ )

proof end;

theorem Th34: :: GRAPH_5:34

for b₁ being set
for b₂ being Graph
for b₃, b₄ being Element of the Vertices of b₂ holds
( b₁ in OrientedPaths b₃,b₄ iff ex b₅ being oriented Chain of b₂ st
( b₅ = b₁ & b₅ is_orientedpath_of b₃,b₄ ) ) ;

theorem Th35: :: GRAPH_5:35

for b₁ being set
for b₂ being Graph
for b₃, b₄ being Element of the Vertices of b₂
for b₅ being oriented Chain of b₂ st b₅ is_orientedpath_of b₃,b₄,b₁ & b₃ <> b₄ holds
b₃ in b₁

proof end;

theorem Th36: :: GRAPH_5:36

for b₁, b₂ being set
for b₃ being Graph
for b₄, b₅ being Element of the Vertices of b₃
for b₆ being oriented Chain of b₃ st b₆ is_orientedpath_of b₄,b₅,b₁ & b₁ c= b₂ holds
b₆ is_orientedpath_of b₄,b₅,b₂

proof end;

theorem Th37: :: GRAPH_5:37

for b₁ being Graph
for b₂ being FinSequence of the Edges of b₁
for b₃, b₄, b₅ being Element of the Vertices of b₁
for b₆ being oriented Chain of b₁ st len b₆ >= 1 & b₆ is_orientedpath_of b₃,b₄ & b₂ . 1 orientedly_joins b₄,b₅ & len b₂ = 1 holds
ex b₇ being oriented Chain of b₁ st
( b₇ = b₆ ^ b₂ & b₇ is_orientedpath_of b₃,b₅ )

proof end;

theorem Th38: :: GRAPH_5:38

for b₁ being set
for b₂ being Graph
for b₃ being FinSequence of the Edges of b₂
for b₄, b₅, b₆ being Element of the Vertices of b₂
for b₇, b₈ being oriented Chain of b₂ st b₇ = b₈ ^ b₃ & len b₈ >= 1 & len b₃ = 1 & b₈ is_orientedpath_of b₄,b₅,b₁ & b₃ . 1 orientedly_joins b₅,b₆ holds
b₇ is_orientedpath_of b₄,b₆,b₁ \/ {b₅}

proof end;

definition

let c₁ be Graph;
let c₂ be oriented Chain of c₁;
let c₃, c₄ be Element of the Vertices of c₁;
pred c₂ is_acyclicpath_of c₃,c₄ means :Def6: :: GRAPH_5:def 6
( a₂ is Simple & a₂ is_orientedpath_of a₃,a₄ );

end;

:: deftheorem Def6 defines is_acyclicpath_of GRAPH_5:def 6 :

definition

let c₁ be Graph;
let c₂ be oriented Chain of c₁;
let c₃, c₄ be Element of the Vertices of c₁;
let c₅ be set ;
pred c₂ is_acyclicpath_of c₃,c₄,c₅ means :Def7: :: GRAPH_5:def 7
( a₂ is Simple & a₂ is_orientedpath_of a₃,a₄,a₅ );

end;

:: deftheorem Def7 defines is_acyclicpath_of GRAPH_5:def 7 :

definition

let c₁ be Graph;
let c₂, c₃ be Element of the Vertices of c₁;
func AcyclicPaths c₂,c₃ -> Subset of (the Edges of a₁ * ) equals :: GRAPH_5:def 8
{ b₁ where B is oriented Simple Chain of a₁ : b₁ is_acyclicpath_of a₂,a₃ } ;
coherence

proof end;

end;

:: deftheorem Def8 defines AcyclicPaths GRAPH_5:def 8 :

definition

let c₁ be Graph;
let c₂, c₃ be Element of the Vertices of c₁;
let c₄ be set ;
func AcyclicPaths c₂,c₃,c₄ -> Subset of (the Edges of a₁ * ) equals :: GRAPH_5:def 9
{ b₁ where B is oriented Simple Chain of a₁ : b₁ is_acyclicpath_of a₂,a₃,a₄ } ;
coherence

proof end;

end;

:: deftheorem Def9 defines AcyclicPaths GRAPH_5:def 9 :

definition

let c₁ be Graph;
let c₂ be oriented Chain of c₁;
func AcyclicPaths c₂ -> Subset of (the Edges of a₁ * ) equals :: GRAPH_5:def 10
{ b₁ where B is oriented Simple Chain of a₁ : ( b₁ <> {} & the Source of a₁ . (b₁ . 1) = the Source of a₁ . (a₂ . 1) & the Target of a₁ . (b₁ . (len b₁)) = the Target of a₁ . (a₂ . (len a₂)) & rng b₁ c= rng a₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def10 defines AcyclicPaths GRAPH_5:def 10 :

definition

let c₁ be Graph;
func AcyclicPaths c₁ -> Subset of (the Edges of a₁ * ) equals :: GRAPH_5:def 11
{ b₁ where B is oriented Simple Chain of a₁ : verum } ;
coherence

proof end;

end;

:: deftheorem Def11 defines AcyclicPaths GRAPH_5:def 11 :

theorem Th39: :: GRAPH_5:39

for b₁ being Graph
for b₂, b₃ being Element of the Vertices of b₁
for b₄ being oriented Chain of b₁ st b₄ = {} holds
not b₄ is_acyclicpath_of b₂,b₃

proof end;

theorem Th40: :: GRAPH_5:40

for b₁ being Graph
for b₂, b₃ being Element of the Vertices of b₁
for b₄ being oriented Chain of b₁ st b₄ is_acyclicpath_of b₂,b₃ holds
b₄ is_orientedpath_of b₂,b₃ by Def6;

theorem Th41: :: GRAPH_5:41

for b₁ being Graph
for b₂, b₃ being Element of the Vertices of b₁ holds AcyclicPaths b₂,b₃ c= OrientedPaths b₂,b₃

proof end;

theorem Th42: :: GRAPH_5:42

for b₁ being Graph
for b₂ being oriented Chain of b₁ holds AcyclicPaths b₂ c= AcyclicPaths b₁

proof end;

theorem Th43: :: GRAPH_5:43

for b₁ being Graph
for b₂, b₃ being Element of the Vertices of b₁ holds AcyclicPaths b₂,b₃ c= AcyclicPaths b₁

proof end;

theorem Th44: :: GRAPH_5:44

for b₁ being Graph
for b₂, b₃ being Element of the Vertices of b₁
for b₄ being oriented Chain of b₁ st b₄ is_orientedpath_of b₂,b₃ holds
AcyclicPaths b₄ c= AcyclicPaths b₂,b₃

proof end;

theorem Th45: :: GRAPH_5:45

for b₁ being set
for b₂ being Graph
for b₃, b₄ being Element of the Vertices of b₂
for b₅ being oriented Chain of b₂ st b₅ is_orientedpath_of b₃,b₄,b₁ holds
AcyclicPaths b₅ c= AcyclicPaths b₃,b₄,b₁

proof end;

theorem Th46: :: GRAPH_5:46

for b₁ being Graph
for b₂, b₃ being oriented Chain of b₁ st b₂ in AcyclicPaths b₃ holds
len b₂ <= len b₃

proof end;

theorem Th47: :: GRAPH_5:47

for b₁ being Graph
for b₂, b₃ being Element of the Vertices of b₁
for b₄ being oriented Chain of b₁ st b₄ is_orientedpath_of b₂,b₃ holds
( AcyclicPaths b₄ <> {} & AcyclicPaths b₂,b₃ <> {} )

proof end;

theorem Th48: :: GRAPH_5:48

for b₁ being set
for b₂ being Graph
for b₃, b₄ being Element of the Vertices of b₂
for b₅ being oriented Chain of b₂ st b₅ is_orientedpath_of b₃,b₄,b₁ holds
( AcyclicPaths b₅ <> {} & AcyclicPaths b₃,b₄,b₁ <> {} )

proof end;

theorem Th49: :: GRAPH_5:49

for b₁ being set
for b₂ being Graph
for b₃, b₄ being Element of the Vertices of b₂ holds AcyclicPaths b₃,b₄,b₁ c= AcyclicPaths b₂

proof end;

definition

func Real>=0 -> Subset of REAL equals :: GRAPH_5:def 12
{ b₁ where B is Real : b₁ >= 0 } ;
coherence

proof end;

end;

:: deftheorem Def12 defines Real>=0 GRAPH_5:def 12 :

registration

cluster Real>=0 -> non empty ;
coherence

proof end;

end;

definition

let c₁ be Graph;
let c₂ be Function;
pred c₂ is_weight>=0of c₁ means :Def13: :: GRAPH_5:def 13
a₂ is Function of the Edges of a₁, Real>=0 ;

end;

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

definition

let c₁ be Graph;
let c₂ be Function;
pred c₂ is_weight_of c₁ means :Def14: :: GRAPH_5:def 14
a₂ is Function of the Edges of a₁, REAL ;

end;

:: deftheorem Def14 defines is_weight_of GRAPH_5:def 14 :

definition

let c₁ be Graph;
let c₂ be FinSequence of the Edges of c₁;
let c₃ be Function;
assume E53: c₃ is_weight_of c₁ ;
func RealSequence c₂,c₃ -> FinSequence of REAL means :Def15: :: GRAPH_5:def 15
( dom a₂ = dom a₄ & ( for b₁ being Nat st b₁ in dom a₂ holds
a₄ . b₁ = a₃ . (a₂ . b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines RealSequence GRAPH_5:def 15 :

definition

let c₁ be Graph;
let c₂ be FinSequence of the Edges of c₁;
let c₃ be Function;
func cost c₂,c₃ -> Real equals :: GRAPH_5:def 16
Sum (RealSequence a₂,a₃);
coherence ;

end;

:: deftheorem Def16 defines cost GRAPH_5:def 16 :

theorem Th50: :: GRAPH_5:50

for b₁ being Function
for b₂ being Graph st b₁ is_weight>=0of b₂ holds
b₁ is_weight_of b₂

proof end;

theorem Th51: :: GRAPH_5:51

for b₁ being Function
for b₂ being Graph
for b₃ being FinSequence of the Edges of b₂
for b₄ being FinSequence of REAL st b₁ is_weight>=0of b₂ & b₄ = RealSequence b₃,b₁ holds
for b₅ being Nat st b₅ in dom b₄ holds
b₄ . b₅ >= 0

proof end;

theorem Th52: :: GRAPH_5:52

for b₁ being Nat
for b₂ being Function
for b₃ being Graph
for b₄, b₅ being FinSequence of the Edges of b₃ st rng b₄ c= rng b₅ & b₂ is_weight_of b₃ & b₁ in dom b₄ holds
ex b₆ being Nat st
( b₆ in dom b₅ & (RealSequence b₅,b₂) . b₆ = (RealSequence b₄,b₂) . b₁ )

proof end;

Lemma57: for b₁ being FinSequence of REAL holds
( ( for b₂ being Real st b₂ in rng b₁ holds
b₂ >= 0 ) iff for b₂ being Nat st b₂ in dom b₁ holds
b₁ . b₂ >= 0 )

proof end;

Lemma58: for b₁, b₂, b₃ being FinSequence of REAL st b₃ = b₁ ^ b₂ & ( for b₄ being Real st b₄ in rng b₃ holds
b₄ >= 0 ) holds
( ( for b₄ being Nat st b₄ in dom b₁ holds
b₁ . b₄ >= 0 ) & ( for b₄ being Nat st b₄ in dom b₂ holds
b₂ . b₄ >= 0 ) )

proof end;

theorem Th53: :: GRAPH_5:53

for b₁ being Function
for b₂ being Graph
for b₃, b₄ being FinSequence of the Edges of b₂ st len b₃ = 1 & rng b₃ c= rng b₄ & b₁ is_weight>=0of b₂ holds
cost b₃,b₁ <= cost b₄,b₁

proof end;

theorem Th54: :: GRAPH_5:54

for b₁ being Function
for b₂ being Graph
for b₃ being FinSequence of the Edges of b₂ st b₁ is_weight>=0of b₂ holds
cost b₃,b₁ >= 0

proof end;

theorem Th55: :: GRAPH_5:55

for b₁ being Function
for b₂ being Graph
for b₃ being FinSequence of the Edges of b₂ st b₃ = {} & b₁ is_weight_of b₂ holds
cost b₃,b₁ = 0

proof end;

theorem Th56: :: GRAPH_5:56

for b₁ being Function
for b₂ being Graph
for b₃, b₄ being Element of the Vertices of b₂
for b₅ being non empty finite Subset of (the Edges of b₂ * ) st b₅ = AcyclicPaths b₃,b₄ holds
ex b₆ being FinSequence of the Edges of b₂ st
( b₆ in b₅ & ( for b₇ being FinSequence of the Edges of b₂ st b₇ in b₅ holds
cost b₆,b₁ <= cost b₇,b₁ ) )

proof end;

theorem Th57: :: GRAPH_5:57

for b₁ being set
for b₂ being Function
for b₃ being Graph
for b₄, b₅ being Element of the Vertices of b₃
for b₆ being non empty finite Subset of (the Edges of b₃ * ) st b₆ = AcyclicPaths b₄,b₅,b₁ holds
ex b₇ being FinSequence of the Edges of b₃ st
( b₇ in b₆ & ( for b₈ being FinSequence of the Edges of b₃ st b₈ in b₆ holds
cost b₇,b₂ <= cost b₈,b₂ ) )

proof end;

theorem Th58: :: GRAPH_5:58

for b₁ being Function
for b₂ being Graph
for b₃, b₄ being FinSequence of the Edges of b₂ st b₁ is_weight_of b₂ holds
cost (b₃ ^ b₄),b₁ = (cost b₃,b₁) + (cost b₄,b₁)

proof end;

theorem Th59: :: GRAPH_5:59

for b₁ being Function
for b₂ being Graph
for b₃, b₄ being FinSequence of the Edges of b₂ st b₃ is one-to-one & rng b₃ c= rng b₄ & b₁ is_weight>=0of b₂ holds
cost b₃,b₁ <= cost b₄,b₁

proof end;

theorem Th60: :: GRAPH_5:60

for b₁ being Function
for b₂ being Graph
for b₃ being FinSequence of the Edges of b₂
for b₄ being oriented Chain of b₂ st b₃ in AcyclicPaths b₄ & b₁ is_weight>=0of b₂ holds
cost b₃,b₁ <= cost b₄,b₁

proof end;

definition

let c₁ be Graph;
let c₂, c₃ be Vertex of c₁;
let c₄ be oriented Chain of c₁;
let c₅ be Function;
pred c₄ is_shortestpath_of c₂,c₃,c₅ means :Def17: :: GRAPH_5:def 17
( a₄ is_orientedpath_of a₂,a₃ & ( for b₁ being oriented Chain of a₁ st b₁ is_orientedpath_of a₂,a₃ holds
cost a₄,a₅ <= cost b₁,a₅ ) );

end;

:: deftheorem Def17 defines is_shortestpath_of GRAPH_5:def 17 :

definition

let c₁ be Graph;
let c₂, c₃ be Vertex of c₁;
let c₄ be oriented Chain of c₁;
let c₅ be set ;
let c₆ be Function;
pred c₄ is_shortestpath_of c₂,c₃,c₅,c₆ means :Def18: :: GRAPH_5:def 18
( a₄ is_orientedpath_of a₂,a₃,a₅ & ( for b₁ being oriented Chain of a₁ st b₁ is_orientedpath_of a₂,a₃,a₅ holds
cost a₄,a₆ <= cost b₁,a₆ ) );

end;

:: deftheorem Def18 defines is_shortestpath_of GRAPH_5:def 18 :

theorem Th61: :: GRAPH_5:61

for b₁ being finite Graph
for b₂ being oriented Simple Chain of b₁ holds len b₂ <= VerticesCount b₁

proof end;

theorem Th62: :: GRAPH_5:62

for b₁ being finite Graph
for b₂ being oriented Simple Chain of b₁ holds len b₂ <= EdgesCount b₁

proof end;

Lemma69: for b₁ being finite Graph holds AcyclicPaths b₁ is finite

proof end;

registration

let c₁ be finite Graph;
cluster AcyclicPaths a₁ -> finite ;
coherence by Lemma69;

end;

Lemma70: for b₁ being finite Graph
for b₂ being oriented Chain of b₁ holds AcyclicPaths b₂ is finite

proof end;

Lemma71: for b₁ being finite Graph
for b₂, b₃ being Element of the Vertices of b₁ holds AcyclicPaths b₂,b₃ is finite

proof end;

Lemma72: for b₁ being set
for b₂ being finite Graph
for b₃, b₄ being Element of the Vertices of b₂ holds AcyclicPaths b₃,b₄,b₁ is finite

proof end;

registration

let c₁ be finite Graph;
let c₂ be oriented Chain of c₁;
cluster AcyclicPaths a₂ -> finite ;
coherence by Lemma70;

end;

registration

let c₁ be finite Graph;
let c₂, c₃ be Element of the Vertices of c₁;
cluster AcyclicPaths a₂,a₃ -> finite ;
coherence by Lemma71;

end;

registration

let c₁ be finite Graph;
let c₂, c₃ be Element of the Vertices of c₁;
let c₄ be set ;
cluster AcyclicPaths a₂,a₃,a₄ -> finite ;
coherence by Lemma72;

end;

theorem Th63: :: GRAPH_5:63

for b₁ being Function
for b₂ being finite Graph
for b₃, b₄ being Element of the Vertices of b₂ st AcyclicPaths b₃,b₄ <> {} holds
ex b₅ being FinSequence of the Edges of b₂ st
( b₅ in AcyclicPaths b₃,b₄ & ( for b₆ being FinSequence of the Edges of b₂ st b₆ in AcyclicPaths b₃,b₄ holds
cost b₅,b₁ <= cost b₆,b₁ ) ) by Th56;

theorem Th64: :: GRAPH_5:64

for b₁ being set
for b₂ being Function
for b₃ being finite Graph
for b₄, b₅ being Element of the Vertices of b₃ st AcyclicPaths b₄,b₅,b₁ <> {} holds
ex b₆ being FinSequence of the Edges of b₃ st
( b₆ in AcyclicPaths b₄,b₅,b₁ & ( for b₇ being FinSequence of the Edges of b₃ st b₇ in AcyclicPaths b₄,b₅,b₁ holds
cost b₆,b₂ <= cost b₇,b₂ ) ) by Th57;

theorem Th65: :: GRAPH_5:65

for b₁ being Function
for b₂ being finite Graph
for b₃ being oriented Chain of b₂
for b₄, b₅ being Element of the Vertices of b₂ st b₃ is_orientedpath_of b₄,b₅ & b₁ is_weight>=0of b₂ holds
ex b₆ being oriented Simple Chain of b₂ st b₆ is_shortestpath_of b₄,b₅,b₁

proof end;

theorem Th66: :: GRAPH_5:66

for b₁ being set
for b₂ being Function
for b₃ being finite Graph
for b₄ being oriented Chain of b₃
for b₅, b₆ being Element of the Vertices of b₃ st b₄ is_orientedpath_of b₅,b₆,b₁ & b₂ is_weight>=0of b₃ holds
ex b₇ being oriented Simple Chain of b₃ st b₇ is_shortestpath_of b₅,b₆,b₁,b₂

proof end;

theorem Th67: :: GRAPH_5:67

for b₁ being set
for b₂ being Function
for b₃ being finite Graph
for b₄ being oriented Chain of b₃
for b₅, b₆ being Element of the Vertices of b₃ st b₂ is_weight>=0of b₃ & b₄ is_shortestpath_of b₅,b₆,b₁,b₂ & b₅ <> b₆ & ( for b₇ being oriented Chain of b₃
for b₈ being Element of the Vertices of b₃ st not b₈ in b₁ & b₇ is_shortestpath_of b₅,b₈,b₁,b₂ holds
cost b₄,b₂ <= cost b₇,b₂ ) holds
b₄ is_shortestpath_of b₅,b₆,b₂

proof end;

theorem Th68: :: GRAPH_5:68

for b₁, b₂ being set
for b₃ being Function
for b₄ being finite Graph
for b₅ being oriented Chain of b₄
for b₆, b₇ being Element of the Vertices of b₄ st b₃ is_weight>=0of b₄ & b₅ is_shortestpath_of b₆,b₇,b₁,b₃ & b₆ <> b₇ & b₁ c= b₂ & ( for b₈ being oriented Chain of b₄
for b₉ being Element of the Vertices of b₄ st not b₉ in b₁ & b₈ is_shortestpath_of b₆,b₉,b₁,b₃ holds
cost b₅,b₃ <= cost b₈,b₃ ) holds
b₅ is_shortestpath_of b₆,b₇,b₂,b₃

proof end;

definition

let c₁ be Graph;
let c₂ be FinSequence of the Edges of c₁;
let c₃ be set ;
let c₄ be Vertex of c₁;
let c₅ be Function;
pred c₂ islongestInShortestpath c₃,c₄,c₅ means :Def19: :: GRAPH_5:def 19
for b₁ being Vertex of a₁ st b₁ in a₃ & b₁ <> a₄ holds
ex b₂ being oriented Chain of a₁ st
( b₂ is_shortestpath_of a₄,b₁,a₃,a₅ & cost b₂,a₅ <= cost a₂,a₅ );

end;

:: deftheorem Def19 defines islongestInShortestpath GRAPH_5:def 19 :

theorem Th69: :: GRAPH_5:69

for b₁, b₂ being set
for b₃ being Function
for b₄ being oriented finite Graph
for b₅, b₆, b₇ being oriented Chain of b₄
for b₈, b₉, b₁₀ being Element of the Vertices of b₄ st b₁ in the Edges of b₄ & b₃ is_weight>=0of b₄ & len b₅ >= 1 & b₅ is_shortestpath_of b₈,b₉,b₂,b₃ & b₈ <> b₉ & b₈ <> b₁₀ & b₇ = b₅ ^ <*b₁*> & b₆ is_shortestpath_of b₈,b₁₀,b₂,b₃ & b₁ orientedly_joins b₉,b₁₀ & b₅ islongestInShortestpath b₂,b₈,b₃ holds
( ( cost b₆,b₃ <= cost b₇,b₃ implies b₆ is_shortestpath_of b₈,b₁₀,b₂ \/ {b₉},b₃ ) & ( cost b₆,b₃ >= cost b₇,b₃ implies b₇ is_shortestpath_of b₈,b₁₀,b₂ \/ {b₉},b₃ ) )

proof end;