:: by Yatsuka Nakamura and Piotr Rudnicki

::

:: Received August 19, 1998

:: Copyright (c) 1998-2019 Association of Mizar Users

definition

let G be Graph;

let x, y be Element of G;

let e be set ;

end;
let x, y be Element of G;

let e be set ;

pred e orientedly_joins x,y means :: GRAPH_4:def 1

( the Source of G . e = x & the Target of G . e = y );

( the Source of G . e = x & the Target of G . e = y );

:: deftheorem defines orientedly_joins GRAPH_4:def 1 :

for G being Graph

for x, y being Element of G

for e being set holds

( e orientedly_joins x,y iff ( the Source of G . e = x & the Target of G . e = y ) );

for G being Graph

for x, y being Element of G

for e being set holds

( e orientedly_joins x,y iff ( the Source of G . e = x & the Target of G . e = y ) );

theorem Th1: :: GRAPH_4:1

for e being set

for G being Graph

for v1, v2 being Element of G st e orientedly_joins v1,v2 holds

e joins v1,v2 by GRAPH_1:def 12;

for G being Graph

for v1, v2 being Element of G st e orientedly_joins v1,v2 holds

e joins v1,v2 by GRAPH_1:def 12;

definition

let G be Graph;

let x, y be Element of the carrier of G;

end;
let x, y be Element of the carrier of G;

pred x,y are_orientedly_incident means :: GRAPH_4:def 2

ex v being set st

( v in the carrier' of G & v orientedly_joins x,y );

ex v being set st

( v in the carrier' of G & v orientedly_joins x,y );

:: deftheorem defines are_orientedly_incident GRAPH_4:def 2 :

for G being Graph

for x, y being Element of the carrier of G holds

( x,y are_orientedly_incident iff ex v being set st

( v in the carrier' of G & v orientedly_joins x,y ) );

for G being Graph

for x, y being Element of the carrier of G holds

( x,y are_orientedly_incident iff ex v being set st

( v in the carrier' of G & v orientedly_joins x,y ) );

theorem :: GRAPH_4:2

for e being set

for G being Graph

for v1, v2, v3, v4 being Element of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds

( v1 = v3 & v2 = v4 ) ;

for G being Graph

for v1, v2, v3, v4 being Element of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds

( v1 = v3 & v2 = v4 ) ;

definition

let G be Graph;

let X be set ;

coherence

{ v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Source of G . e ) } is set ;

;

end;
let X be set ;

func G -SVSet X -> set equals :: GRAPH_4:def 3

{ v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Source of G . e ) } ;

correctness { v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Source of G . e ) } ;

coherence

{ v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Source of G . e ) } is set ;

;

:: deftheorem defines -SVSet GRAPH_4:def 3 :

for G being Graph

for X being set holds G -SVSet X = { v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Source of G . e ) } ;

for G being Graph

for X being set holds G -SVSet X = { v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Source of G . e ) } ;

definition

let G be Graph;

let X be set ;

coherence

{ v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Target of G . e ) } is set ;

;

end;
let X be set ;

func G -TVSet X -> set equals :: GRAPH_4:def 4

{ v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Target of G . e ) } ;

correctness { v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Target of G . e ) } ;

coherence

{ v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Target of G . e ) } is set ;

;

:: deftheorem defines -TVSet GRAPH_4:def 4 :

for G being Graph

for X being set holds G -TVSet X = { v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Target of G . e ) } ;

for G being Graph

for X being set holds G -TVSet X = { v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & v = the Target of G . e ) } ;

:: deftheorem defines is_oriented_vertex_seq_of GRAPH_4:def 5 :

for G being Graph

for vs being FinSequence of the carrier of G

for c being FinSequence holds

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

c . n orientedly_joins vs /. n,vs /. (n + 1) ) ) );

for G being Graph

for vs being FinSequence of the carrier of G

for c being FinSequence holds

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

c . n orientedly_joins vs /. n,vs /. (n + 1) ) ) );

theorem Th4: :: GRAPH_4:4

for G being Graph

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds

vs is_vertex_seq_of c

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds

vs is_vertex_seq_of c

proof end;

theorem :: GRAPH_4:5

for G being Graph

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds

G -SVSet (rng c) c= rng vs

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds

G -SVSet (rng c) c= rng vs

proof end;

theorem :: GRAPH_4:6

for G being Graph

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds

G -TVSet (rng c) c= rng vs

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds

G -TVSet (rng c) c= rng vs

proof end;

theorem :: GRAPH_4:7

for G being Graph

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st c <> {} & vs is_oriented_vertex_seq_of c holds

rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c))

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st c <> {} & vs is_oriented_vertex_seq_of c holds

rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c))

proof end;

theorem :: GRAPH_4:8

theorem Th9: :: GRAPH_4:9

for G being Graph

for c being oriented Chain of G ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c

for c being oriented Chain of G ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c

proof end;

theorem Th10: :: GRAPH_4:10

for G being Graph

for vs1, vs2 being FinSequence of the carrier of G

for c being oriented Chain of G st c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c holds

vs1 = vs2

for vs1, vs2 being FinSequence of the carrier of G

for c being oriented Chain of G st c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c holds

vs1 = vs2

proof end;

definition

let G be Graph;

let c be oriented Chain of G;

assume A1: c <> {} ;

ex b_{1} being FinSequence of the carrier of G st b_{1} is_oriented_vertex_seq_of c
by Th9;

uniqueness

for b_{1}, b_{2} being FinSequence of the carrier of G st b_{1} is_oriented_vertex_seq_of c & b_{2} is_oriented_vertex_seq_of c holds

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

end;
let c be oriented Chain of G;

assume A1: c <> {} ;

func oriented-vertex-seq c -> FinSequence of the carrier of G means :: GRAPH_4:def 6

it is_oriented_vertex_seq_of c;

existence it is_oriented_vertex_seq_of c;

ex b

uniqueness

for b

b

:: deftheorem defines oriented-vertex-seq GRAPH_4:def 6 :

for G being Graph

for c being oriented Chain of G st c <> {} holds

for b_{3} being FinSequence of the carrier of G holds

( b_{3} = oriented-vertex-seq c iff b_{3} is_oriented_vertex_seq_of c );

for G being Graph

for c being oriented Chain of G st c <> {} holds

for b

( b

theorem :: GRAPH_4:11

for n being Nat

for G being Graph

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds

vs1 is_oriented_vertex_seq_of c1

for G being Graph

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds

vs1 is_oriented_vertex_seq_of c1

proof end;

theorem Th12: :: GRAPH_4:12

for q being FinSequence

for m, n being Nat

for G being Graph

for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds

q is oriented Chain of G

for m, n being Nat

for G being Graph

for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds

q is oriented Chain of G

proof end;

theorem Th13: :: GRAPH_4:13

for m, n being Nat

for G being Graph

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds

vs1 is_oriented_vertex_seq_of c1

for G being Graph

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds

vs1 is_oriented_vertex_seq_of c1

proof end;

theorem Th14: :: GRAPH_4:14

for G being Graph

for vs1, vs2 being FinSequence of the carrier of G

for c1, c2 being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds

c1 ^ c2 is oriented Chain of G

for vs1, vs2 being FinSequence of the carrier of G

for c1, c2 being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds

c1 ^ c2 is oriented Chain of G

proof end;

theorem Th15: :: GRAPH_4:15

for G being Graph

for vs, vs1, vs2 being FinSequence of the carrier of G

for c, c1, c2 being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds

vs is_oriented_vertex_seq_of c

for vs, vs1, vs2 being FinSequence of the carrier of G

for c, c1, c2 being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds

vs is_oriented_vertex_seq_of c

proof end;

Lm1: for G being Graph

for v being Element of G holds <*v*> is_oriented_vertex_seq_of {}

by FINSEQ_1:39;

:: deftheorem Def7 defines Simple GRAPH_4:def 7 :

for G being Graph

for IT being oriented Chain of G holds

( IT is Simple iff ex vs being FinSequence of the carrier of G st

( vs is_oriented_vertex_seq_of IT & ( for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs ) ) ) );

for G being Graph

for IT being oriented Chain of G holds

( IT is Simple iff ex vs being FinSequence of the carrier of G st

( vs is_oriented_vertex_seq_of IT & ( for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs ) ) ) );

registration

let G be Graph;

ex b_{1} being oriented Chain of G st b_{1} is Simple

end;
cluster Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple for Chain of G;

existence ex b

proof end;

registration

let G be Graph;

ex b_{1} being Chain of G st

( b_{1} is oriented & b_{1} is simple )

end;
cluster Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented simple for Chain of G;

existence ex b

( b

proof end;

theorem Th16: :: GRAPH_4:16

for n being Nat

for G being Graph

for q being oriented Chain of G holds q | (Seg n) is oriented Chain of G

for G being Graph

for q being oriented Chain of G holds q | (Seg n) is oriented Chain of G

proof end;

theorem :: GRAPH_4:17

theorem Th18: :: GRAPH_4:18

for G being Graph

for sc being oriented simple Chain of G

for sc9 being oriented Chain of G st sc9 = sc holds

sc9 is Simple

for sc being oriented simple Chain of G

for sc9 being oriented Chain of G st sc9 = sc holds

sc9 is Simple

proof end;

Lm2: for p being FinSequence

for m, n being Nat st 1 <= m & m <= n + 1 & n <= len p holds

( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds

((m,n) -cut p) . (i + 1) = p . (m + i) ) )

proof end;

theorem Th20: :: GRAPH_4:20

for G being Graph

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st not c is Simple & vs is_oriented_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st not c is Simple & vs is_oriented_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

proof end;

theorem :: GRAPH_4:21

for G being Graph

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st

( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )

for vs being FinSequence of the carrier of G

for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st

( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )

proof end;

theorem :: GRAPH_4:22

for p being FinSequence

for n being Nat

for G being Graph st p is OrientedPath of G holds

p | (Seg n) is OrientedPath of G

for n being Nat

for G being Graph st p is OrientedPath of G holds

p | (Seg n) is OrientedPath of G

proof end;

theorem :: GRAPH_4:24

for G being Graph

for c1 being FinSequence holds

( ( c1 is oriented Simple Chain of G implies c1 is oriented simple Chain of G ) & ( c1 is oriented simple Chain of G implies c1 is oriented Simple Chain of G ) & ( c1 is oriented simple Chain of G implies c1 is OrientedPath of G ) ) by Th18, Th19, Th23;

for c1 being FinSequence holds

( ( c1 is oriented Simple Chain of G implies c1 is oriented simple Chain of G ) & ( c1 is oriented simple Chain of G implies c1 is oriented Simple Chain of G ) & ( c1 is oriented simple Chain of G implies c1 is OrientedPath of G ) ) by Th18, Th19, Th23;