:: Oriented Simple Chains Included in Oriented Chains
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received August 19, 1998
:: Copyright (c) 1998-2021 Association of Mizar Users

definition

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

end;

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

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;

definition

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

end;

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

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

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 G : ex e being Element of the carrier' of G st
( e in X & v = the Source of G . e ) } ;

correctness
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;

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

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 G : ex e being Element of the carrier' of G st
( e in X & v = the Target of G . e ) } ;

correctness
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;

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

theorem :: GRAPH_4:3

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

proof end;

definition

let G be Graph;
let vs be FinSequence of the carrier of G;
let c be FinSequence;

pred vs is_oriented_vertex_seq_of c means :: 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 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) ) ) );

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

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

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

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

proof end;

theorem :: GRAPH_4:8

for G being Graph
for v being Element of G holds <*v*> is_oriented_vertex_seq_of {} by FINSEQ_1:40;

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

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

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 carrier of G means :: GRAPH_4:def 6
it is_oriented_vertex_seq_of c;

existence
ex b₁ being FinSequence of the carrier of G st b₁ is_oriented_vertex_seq_of c by Th9;
uniqueness
for b₁, b₂ being FinSequence of the carrier of G st b₁ is_oriented_vertex_seq_of c & b₂ is_oriented_vertex_seq_of c holds
b₁ = b₂ by A1, Th10;

end;

:: 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₃ being FinSequence of the carrier of G holds
( b₃ = oriented-vertex-seq c iff b₃ is_oriented_vertex_seq_of c );

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

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

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

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

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

proof end;

Lm1: for G being Graph
for v being Element of G holds <*v*> is_oriented_vertex_seq_of {}
by FINSEQ_1:39;

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

end;

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

registration

let G be Graph;

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₁ being oriented Chain of G st b₁ is Simple

proof end;

end;

registration

let G be Graph;

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₁ being Chain of G st
( b₁ is oriented & b₁ is simple )

proof end;

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

proof end;

theorem :: GRAPH_4:17

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 Th16, GRAPH_2:45;

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

proof end;

theorem Th19: :: GRAPH_4:19

for G being Graph
for sc9 being oriented Simple Chain of G holds sc9 is oriented simple Chain of G

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 )

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

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

proof end;

theorem Th23: :: GRAPH_4:23

for G being Graph
for sc being oriented simple Chain of G holds sc 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;