:: GRAPH_4 semantic presentation

definition

let G be Graph;
let x, y be Element of the Vertices of G;
let e be set ;
pred e orientedly_joins x,y means :Def1: :: GRAPH_4:def 1
( the Source of G . e = x & the Target of G . e = y );

end;

:: deftheorem Def1 defines orientedly_joins GRAPH_4:def 1 :

theorem Th1: :: GRAPH_4:1

for e being set
for G being Graph
for v1, v2 being Element of the Vertices of G st e orientedly_joins v1,v2 holds
e joins v1,v2

proof end;

definition

let G be Graph;
let x, y be Element of the Vertices of G;
pred x,y are_orientedly_incident means :: GRAPH_4:def 2
ex v being set st
( v in the Edges of G & v orientedly_joins x,y );

end;

:: deftheorem defines are_orientedly_incident GRAPH_4:def 2 :

theorem Th2: :: GRAPH_4:2

for e being set
for G being Graph
for v1, v2, v3, v4 being Element of the Vertices of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds
( v1 = v3 & v2 = v4 )

proof end;

registration

let G be Graph;
cluster empty oriented Chain of G;
existence

proof end;

end;

definition

let G be Graph;
let X be set ;
func G -SVSet X -> set equals :: GRAPH_4:def 3
{ v where v is Element of the Vertices of G : ex e being Element of the Edges of G st
( e in X & v = the Source of G . e ) } ;
correctness ;

end;

:: deftheorem defines -SVSet GRAPH_4:def 3 :

definition

let G be Graph;
let X be set ;
func G -TVSet X -> set equals :: GRAPH_4:def 4
{ v where v is Element of the Vertices of G : ex e being Element of the Edges of G st
( e in X & v = the Target of G . e ) } ;
correctness ;

end;

:: deftheorem defines -TVSet GRAPH_4:def 4 :

theorem :: GRAPH_4:3

canceled;

theorem :: GRAPH_4:4

for G being Graph holds
( G -SVSet {} = {} & G -TVSet {} = {} )

proof end;

definition

let G be Graph;
let vs be FinSequence of the Vertices of G;
let c be FinSequence;
pred vs is_oriented_vertex_seq_of c means :Def5: :: GRAPH_4:def 5
( 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) ) );

end;

:: deftheorem Def5 defines is_oriented_vertex_seq_of GRAPH_4:def 5 :

theorem Th5: :: GRAPH_4:5

for G being Graph
for vs being FinSequence of the Vertices 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:6

for G being Graph
for vs being FinSequence of the Vertices 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:7

for G being Graph
for vs being FinSequence of the Vertices 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:8

for G being Graph
for vs being FinSequence of the Vertices 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:9

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

proof end;

theorem Th10: :: GRAPH_4:10

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

proof end;

theorem Th11: :: GRAPH_4:11

for G being Graph
for vs1, vs2 being FinSequence of the Vertices 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 <> {} ;
func oriented-vertex-seq c -> FinSequence of the Vertices of G means :: GRAPH_4:def 6
it is_oriented_vertex_seq_of c;
existence by Th10;
uniqueness by A1, Th11;

end;

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

theorem :: GRAPH_4:12

for n being Nat
for G being Graph
for vs, vs1 being FinSequence of the Vertices 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 Th13: :: GRAPH_4:13

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

proof end;

theorem Th14: :: GRAPH_4:14

for m, n being Nat
for G being Graph
for vs, vs1 being FinSequence of the Vertices 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 Th15: :: GRAPH_4:15

for G being Graph
for vs1, vs2 being FinSequence of the Vertices 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 Th16: :: GRAPH_4:16

for G being Graph
for vs1, vs2, vs being FinSequence of the Vertices of G
for c1, c2, c 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 the Vertices of G holds <*v*> is_oriented_vertex_seq_of {}

proof end;

definition

let G be Graph;
let IT be oriented Chain of G;
attr IT is Simple means :Def7: :: GRAPH_4:def 7
ex vs being FinSequence of the Vertices 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 ) ) );

end;

:: deftheorem Def7 defines Simple GRAPH_4:def 7 :

registration

let G be Graph;
cluster oriented Simple Chain of G;
existence

proof end;

end;

registration

let G be Graph;
cluster oriented simple Chain of G;
existence

proof end;

end;

theorem :: GRAPH_4:17

canceled;

theorem Th18: :: GRAPH_4:18

for n being Nat
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:19

for n being Nat
for G being Graph
for sc being oriented simple Chain of G holds sc | (Seg n) is oriented simple Chain of G by Th18, GRAPH_2:49;

theorem Th20: :: GRAPH_4:20

for G being Graph
for sc being oriented simple Chain of G
for sc' being oriented Chain of G st sc' = sc holds
sc' is Simple

proof end;

theorem Th21: :: GRAPH_4:21

for G being Graph
for sc' being oriented Simple Chain of G holds sc' is oriented simple Chain of G

proof end;

theorem Th22: :: GRAPH_4:22

for G being Graph
for vs being FinSequence of the Vertices 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 FinSubsequence of c ex fvs being FinSubsequence of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the Vertices 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:23

for G being Graph
for vs being FinSequence of the Vertices of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
ex fc being FinSubsequence of c ex fvs being FinSubsequence of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the Vertices 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;

registration

let G be Graph;
cluster empty oriented -> V6 oriented Chain of G;
correctness ;

end;

theorem :: GRAPH_4:24

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

proof end;

theorem Th25: :: GRAPH_4:25

for G being Graph
for sc being oriented simple Chain of G holds sc is OrientedPath of G

proof end;

theorem :: GRAPH_4:26

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 Th20, Th21, Th25;