:: GRAPH_5 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: GRAPH_5:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f being finite Function holds card (rng f) <= card (dom f)
proof end;

theorem Th2: :: GRAPH_5:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

scheme :: GRAPH_5:sch 1
LambdaAB{ F1() -> set , F2() -> set , F3( Element of F2()) -> set } :
ex f being Function st
( dom f = F1() & ( for x being Element of F2() st x in F1() holds
f . x = F3(x) ) )
proof end;

theorem Th3: :: GRAPH_5:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being finite set
for n being 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 Th4: :: GRAPH_5:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being finite set
for n being Nat
for X being set st X = { x where x is Element of D * : len x <= n } holds
X is finite
proof end;

theorem Th5: :: GRAPH_5:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being finite set holds
( card D <> 0 iff D <> {} )
proof end;

theorem Th6: :: GRAPH_5:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being finite set
for k being 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;

theorem Th7: :: GRAPH_5:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for D being finite set st card D = 1 holds
ex x being Element of D st D = {x}
proof end;

scheme :: GRAPH_5:sch 2
MinValue{ F1() -> non empty finite set , F2( Element of F1()) -> Real } :
ex x being Element of F1() st
for y being Element of F1() holds F2(x) <= F2(y)
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 b1 being Element of X holds b1 is FinSequence of D
proof end;
end;

theorem Th8: :: GRAPH_5:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence holds
( p <> {} iff len p >= 1 )
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 q, p being FinSequence st 1 <= n & n <= len q holds
q . n = (p ^ q) . ((len p) + n)
proof end;

theorem Th9: :: GRAPH_5:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence holds
( ( for n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n <> p . m ) iff p is one-to-one )
proof end;

theorem Th10: :: GRAPH_5:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence holds
( ( for n, m being Nat st 1 <= n & n < m & m <= len p holds
p . n <> p . m ) iff card (rng p) = len p )
proof end;

theorem Th11: :: GRAPH_5:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for G being Graph
for pe being FinSequence of the Edges of G st i in dom pe holds
( the Source of G . (pe . i) in the Vertices of G & the Target of G . (pe . i) in the Vertices of G )
proof end;

theorem Th12: :: GRAPH_5:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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) )
proof end;

theorem Th13: :: GRAPH_5:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th14: :: GRAPH_5:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th15: :: GRAPH_5:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th16: :: GRAPH_5:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph holds {} is oriented Simple Chain of G
proof end;

theorem Th17: :: GRAPH_5:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th18: :: GRAPH_5:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for pe being FinSequence of the Edges of G st len pe = 1 holds
pe is oriented Simple Chain of G
proof end;

theorem Th19: :: GRAPH_5:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for p being oriented Simple Chain of G
for q being FinSequence of the Edges 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 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;

theorem Th20: :: GRAPH_5:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for p being oriented Simple Chain of G holds p is one-to-one
proof end;

definition
let G be Graph;
let e be Element of the Edges of G;
func vertices e -> set equals :: GRAPH_5:def 1
{(the Source of G . e),(the Target of G . e)};
coherence
{(the Source of G . e),(the Target of G . e)} is set
;
end;

:: deftheorem defines vertices GRAPH_5:def 1 :
for G being Graph
for e being Element of the Edges 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 Edges of G;
func vertices pe -> Subset of the Vertices of G equals :: GRAPH_5:def 2
{ v where v is Vertex of G : ex i being Nat st
( i in dom pe & v in vertices (pe /. i) )
}
;
coherence
{ v where v is Vertex of G : ex i being Nat st
( i in dom pe & v in vertices (pe /. i) )
}
is Subset of the Vertices of G
proof end;
end;

:: deftheorem defines vertices GRAPH_5:def 2 :
for G being Graph
for pe being FinSequence of the Edges of G holds vertices pe = { v where v is Vertex of G : ex i being Nat st
( i in dom pe & v in vertices (pe /. i) )
}
;

theorem Th21: :: GRAPH_5:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for pe, qe being FinSequence of the Edges 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 Th22: :: GRAPH_5:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for G being Graph
for pe being FinSequence of the Edges 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 Th23: :: GRAPH_5:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for G being Graph
for pe being FinSequence of the Edges of G st not vertices pe c= V holds
ex i being Nat ex q, r being FinSequence of the Edges 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 Th24: :: GRAPH_5:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for qe, pe being FinSequence of the Edges of G st rng qe c= rng pe holds
vertices qe c= vertices pe
proof end;

theorem Th25: :: GRAPH_5:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, V being set
for G being Graph
for qe, pe being FinSequence of the Edges of G st rng qe c= rng pe & (vertices pe) \ X c= V holds
(vertices qe) \ X c= V
proof end;

theorem Th26: :: GRAPH_5:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, V being set
for G being Graph
for pe, qe being FinSequence of the Edges of G st (vertices (pe ^ qe)) \ X c= V holds
( (vertices pe) \ X c= V & (vertices qe) \ X c= V )
proof end;

theorem Th27: :: GRAPH_5:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v being Element of the Vertices of G
for e being Element of the Edges of G st ( v = the Source of G . e or v = the Target of G . e ) holds
v in vertices e by TARSKI:def 2;

theorem Th28: :: GRAPH_5:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for G being Graph
for pe being FinSequence of the Edges of G
for v being Element of the Vertices 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 Th29: :: GRAPH_5:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for pe being FinSequence of the Edges of G st len pe = 1 holds
vertices pe = vertices (pe /. 1)
proof end;

theorem Th30: :: GRAPH_5:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for pe, qe being FinSequence of the Edges of G holds
( vertices pe c= vertices (pe ^ qe) & vertices qe c= vertices (pe ^ qe) )
proof end;

theorem Th31: :: GRAPH_5:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for pe being FinSequence of the Edges 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 Th32: :: GRAPH_5:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v being Element of the Vertices 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 Nat st
( 1 <= i & i <= len p & v = the Target of G . (p . i) )
proof end;

definition
let G be Graph;
let p be oriented Chain of G;
let v1, v2 be Element of the Vertices of G;
pred p is_orientedpath_of v1,v2 means :Def3: :: GRAPH_5:def 3
( p <> {} & the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 );
end;

:: 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 the Vertices 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 the Vertices 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 );
end;

:: deftheorem Def4 defines is_orientedpath_of GRAPH_5:def 4 :
for G being Graph
for v1, v2 being Element of the Vertices 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 the Vertices of G;
func OrientedPaths v1,v2 -> Subset of (the Edges 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 } is Subset of (the Edges of G * )
proof end;
end;

:: deftheorem defines OrientedPaths GRAPH_5:def 5 :
for G being Graph
for v1, v2 being Element of the Vertices of G holds OrientedPaths v1,v2 = { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } ;

theorem Th33: :: GRAPH_5:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v1, v2 being Element of the Vertices 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:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for G being Graph
for v1, v2 being Element of the Vertices 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 Th35: :: GRAPH_5:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for G being Graph
for v1, v2 being Element of the Vertices 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 Th36: :: GRAPH_5:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V, U being set
for G being Graph
for v1, v2 being Element of the Vertices 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 Th37: :: GRAPH_5:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for pe being FinSequence of the Edges of G
for v1, v2, v3 being Element of the Vertices 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 Th38: :: GRAPH_5:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for G being Graph
for pe being FinSequence of the Edges of G
for v1, v2, v3 being Element of the Vertices 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;

definition
let G be Graph;
let p be oriented Chain of G;
let v1, v2 be Element of the Vertices of G;
pred p is_acyclicpath_of v1,v2 means :Def6: :: GRAPH_5:def 6
( p is Simple & p is_orientedpath_of v1,v2 );
end;

:: 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 the Vertices 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 the Vertices 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 );
end;

:: 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 the Vertices 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 the Vertices of G;
func AcyclicPaths v1,v2 -> Subset of (the Edges 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 } is Subset of (the Edges of G * )
proof end;
end;

:: deftheorem defines AcyclicPaths GRAPH_5:def 8 :
for G being Graph
for v1, v2 being Element of the Vertices 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 the Vertices of G;
let V be set ;
func AcyclicPaths v1,v2,V -> Subset of (the Edges 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 } is Subset of (the Edges of G * )
proof end;
end;

:: deftheorem defines AcyclicPaths GRAPH_5:def 9 :
for G being Graph
for v1, v2 being Element of the Vertices 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;
func AcyclicPaths p -> Subset of (the Edges 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 ) } is Subset of (the Edges of G * )
proof end;
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 ) } ;

definition
let G be Graph;
func AcyclicPaths G -> Subset of (the Edges 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 } is Subset of (the Edges of G * )
proof end;
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 } ;

theorem :: GRAPH_5:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v1, v2 being Element of the Vertices of G
for p being oriented Chain of G st p = {} holds
not p is_acyclicpath_of v1,v2
proof end;

theorem :: GRAPH_5:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v1, v2 being Element of the Vertices 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 :: GRAPH_5:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v1, v2 being Element of the Vertices of G holds AcyclicPaths v1,v2 c= OrientedPaths v1,v2
proof end;

theorem Th42: :: GRAPH_5:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for p being oriented Chain of G holds AcyclicPaths p c= AcyclicPaths G
proof end;

theorem Th43: :: GRAPH_5:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v1, v2 being Element of the Vertices of G holds AcyclicPaths v1,v2 c= AcyclicPaths G
proof end;

theorem Th44: :: GRAPH_5:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v1, v2 being Element of the Vertices 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 Th45: :: GRAPH_5:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for G being Graph
for v1, v2 being Element of the Vertices 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 :: GRAPH_5:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for q, p being oriented Chain of G st q in AcyclicPaths p holds
len q <= len p
proof end;

theorem Th47: :: GRAPH_5:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v1, v2 being Element of the Vertices 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 Th48: :: GRAPH_5:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for G being Graph
for v1, v2 being Element of the Vertices 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 Th49: :: GRAPH_5:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for G being Graph
for v1, v2 being Element of the Vertices of G holds AcyclicPaths v1,v2,V c= AcyclicPaths G
proof end;

definition
func Real>=0 -> Subset of REAL equals :: GRAPH_5:def 12
{ r where r is Real : r >= 0 } ;
coherence
{ r where r is Real : r >= 0 } is Subset of REAL
proof end;
end;

:: deftheorem defines Real>=0 GRAPH_5:def 12 :
Real>=0 = { r where r is Real : r >= 0 } ;

registration
cluster Real>=0 -> non empty ;
coherence
not Real>=0 is empty
proof end;
end;

definition
let G be Graph;
let W be Function;
pred W is_weight>=0of G means :Def13: :: GRAPH_5:def 13
W is Function of the Edges of G, Real>=0 ;
end;

:: 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 Edges of G, Real>=0 );

definition
let G be Graph;
let W be Function;
pred W is_weight_of G means :Def14: :: GRAPH_5:def 14
W is Function of the Edges of G, REAL ;
end;

:: 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 Edges of G, REAL );

definition
let G be Graph;
let p be FinSequence of the Edges 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 Nat st i in dom p holds
it . i = W . (p . i) ) );
existence
ex b1 being FinSequence of REAL st
( dom p = dom b1 & ( for i being Nat st i in dom p holds
b1 . i = W . (p . i) ) )
proof end;
uniqueness
for b1, b2 being FinSequence of REAL st dom p = dom b1 & ( for i being Nat st i in dom p holds
b1 . i = W . (p . i) ) & dom p = dom b2 & ( for i being Nat st i in dom p holds
b2 . i = W . (p . i) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines RealSequence GRAPH_5:def 15 :
for G being Graph
for p being FinSequence of the Edges of G
for W being Function st W is_weight_of G holds
for b4 being FinSequence of REAL holds
( b4 = RealSequence p,W iff ( dom p = dom b4 & ( for i being Nat st i in dom p holds
b4 . i = W . (p . i) ) ) );

definition
let G be Graph;
let p be FinSequence of the Edges of G;
let W be Function;
func cost p,W -> Real equals :: GRAPH_5:def 16
Sum (RealSequence p,W);
coherence
Sum (RealSequence p,W) is Real
;
end;

:: deftheorem defines cost GRAPH_5:def 16 :
for G being Graph
for p being FinSequence of the Edges of G
for W being Function holds cost p,W = Sum (RealSequence p,W);

theorem Th50: :: GRAPH_5:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for G being Graph st W is_weight>=0of G holds
W is_weight_of G
proof end;

theorem Th51: :: GRAPH_5:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for G being Graph
for pe being FinSequence of the Edges of G
for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence pe,W holds
for i being Nat st i in dom f holds
f . i >= 0
proof end;

theorem Th52: :: GRAPH_5:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for W being Function
for G being Graph
for qe, pe being FinSequence of the Edges of G st rng qe c= rng pe & W is_weight_of G & i in dom qe holds
ex j being 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 Nat st i in dom p holds
p . i >= 0 ) & ( for i being Nat st i in dom q holds
q . i >= 0 ) )
proof end;

theorem :: GRAPH_5:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for G being Graph
for qe, pe being FinSequence of the Edges 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 Th54: :: GRAPH_5:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for G being Graph
for pe being FinSequence of the Edges of G st W is_weight>=0of G holds
cost pe,W >= 0
proof end;

theorem Th55: :: GRAPH_5:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for G being Graph
for pe being FinSequence of the Edges of G st pe = {} & W is_weight_of G holds
cost pe,W = 0
proof end;

theorem Th56: :: GRAPH_5:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for G being Graph
for v1, v2 being Element of the Vertices of G
for D being non empty finite Subset of (the Edges of G * ) st D = AcyclicPaths v1,v2 holds
ex pe being FinSequence of the Edges of G st
( pe in D & ( for qe being FinSequence of the Edges of G st qe in D holds
cost pe,W <= cost qe,W ) )
proof end;

theorem Th57: :: GRAPH_5:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for W being Function
for G being Graph
for v1, v2 being Element of the Vertices of G
for D being non empty finite Subset of (the Edges of G * ) st D = AcyclicPaths v1,v2,V holds
ex pe being FinSequence of the Edges of G st
( pe in D & ( for qe being FinSequence of the Edges of G st qe in D holds
cost pe,W <= cost qe,W ) )
proof end;

theorem Th58: :: GRAPH_5:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for G being Graph
for pe, qe being FinSequence of the Edges of G st W is_weight_of G holds
cost (pe ^ qe),W = (cost pe,W) + (cost qe,W)
proof end;

theorem Th59: :: GRAPH_5:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for G being Graph
for qe, pe being FinSequence of the Edges 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 Th60: :: GRAPH_5:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for G being Graph
for pe being FinSequence of the Edges 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;

definition
let G be Graph;
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 ) );
end;

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

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

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

theorem :: GRAPH_5:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite Graph
for ps being oriented Simple Chain of G holds len ps <= VerticesCount G
proof end;

theorem Th62: :: GRAPH_5:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite Graph
for ps being oriented Simple Chain of G holds len ps <= EdgesCount G
proof end;

Lm5: for G being finite Graph holds AcyclicPaths G is finite
proof end;

registration
let G be finite Graph;
cluster AcyclicPaths G -> finite ;
coherence
AcyclicPaths G is finite
by Lm5;
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 the Vertices 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 the Vertices of G holds AcyclicPaths v1,v2,V is finite
proof end;

registration
let G be finite Graph;
let P be oriented Chain of G;
cluster AcyclicPaths P -> finite ;
coherence
AcyclicPaths P is finite
by Lm6;
end;

registration
let G be finite Graph;
let v1, v2 be Element of the Vertices of G;
cluster AcyclicPaths v1,v2 -> finite ;
coherence
AcyclicPaths v1,v2 is finite
by Lm7;
end;

registration
let G be finite Graph;
let v1, v2 be Element of the Vertices of G;
let V be set ;
cluster AcyclicPaths v1,v2,V -> finite ;
coherence
AcyclicPaths v1,v2,V is finite
by Lm8;
end;

theorem :: GRAPH_5:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for G being finite Graph
for v1, v2 being Element of the Vertices of G st AcyclicPaths v1,v2 <> {} holds
ex pe being FinSequence of the Edges of G st
( pe in AcyclicPaths v1,v2 & ( for qe being FinSequence of the Edges of G st qe in AcyclicPaths v1,v2 holds
cost pe,W <= cost qe,W ) ) by Th56;

theorem :: GRAPH_5:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for V being set
for W being Function
for G being finite Graph
for v1, v2 being Element of the Vertices of G st AcyclicPaths v1,v2,V <> {} holds
ex pe being FinSequence of the Edges of G st
( pe in AcyclicPaths v1,v2,V & ( for qe being FinSequence of the Edges of G st qe in AcyclicPaths v1,v2,V holds
cost pe,W <= cost qe,W ) ) by Th57;

theorem :: GRAPH_5:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for W being Function
for G being finite Graph
for P being oriented Chain of G
for v1, v2 being Element of the Vertices 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 Th66: :: GRAPH_5:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 the Vertices 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;

theorem Th67: :: GRAPH_5:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 the Vertices 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 the Vertices 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:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 the Vertices 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 the Vertices 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 Edges 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 );
end;

:: deftheorem Def19 defines islongestInShortestpath GRAPH_5:def 19 :
for G being Graph
for pe being FinSequence of the Edges 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 ) );

theorem :: GRAPH_5:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 the Vertices of G st e in the Edges 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;