:: Vertex sequences induced by chains
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: Received May 13, 1995
:: Copyright (c) 1995-2021 Association of Mizar Users

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 :: GRAPH_2:1

canceled;

theorem :: GRAPH_2:2

canceled;

theorem :: GRAPH_2:3

canceled;

theorem :: GRAPH_2:4

canceled;

theorem :: GRAPH_2:5

canceled;

theorem :: GRAPH_2:6

canceled;

theorem :: GRAPH_2:7

canceled;

theorem :: GRAPH_2:8

canceled;

theorem :: GRAPH_2:9

canceled;

theorem :: GRAPH_2:10

canceled;

theorem :: GRAPH_2:11

canceled;

theorem :: GRAPH_2:12

canceled;

theorem :: GRAPH_2:13

canceled;

theorem :: GRAPH_2:14

canceled;

theorem :: GRAPH_2:15

canceled;

theorem :: GRAPH_2:16

canceled;

theorem :: GRAPH_2:17

canceled;

theorem :: GRAPH_2:18

canceled;

theorem :: GRAPH_2:19

canceled;

theorem :: GRAPH_2:20

canceled;

theorem :: GRAPH_2:21

canceled;

theorem :: GRAPH_2:22

canceled;

theorem :: GRAPH_2:23

canceled;

theorem :: GRAPH_2:24

canceled;

theorem :: GRAPH_2:25

canceled;

theorem :: GRAPH_2:26

canceled;

theorem :: GRAPH_2:27

canceled;

theorem :: GRAPH_2:28

canceled;

canceled;

canceled;

canceled;

canceled;

theorem :: GRAPH_2:29

for e being set
for G being Graph
for v1, v2 being Element of G st e joins v1,v2 holds
e joins v2,v1 ;

theorem :: GRAPH_2:30

for e being set
for G being Graph
for v1, v2, v3, v4 being Element of G st e joins v1,v2 & e joins v3,v4 & not ( v1 = v3 & v2 = v4 ) holds
( v1 = v4 & v2 = v3 ) ;

definition

let G be Graph;
let X be set ;

func G -VSet X -> set equals :: GRAPH_2:def 1
{ 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 or 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 Source of G . e or v = the Target of G . e ) ) } is set ;
;

end;

:: deftheorem defines -VSet GRAPH_2:def 1 :
for G being Graph
for X being set holds G -VSet 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 or v = the Target of G . e ) ) } ;

definition

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

pred vs is_vertex_seq_of c means :: GRAPH_2:def 2
( len vs = (len c) + 1 & ( for n being Nat st 1 <= n & n <= len c holds
c . n joins vs /. n,vs /. (n + 1) ) );

end;

:: deftheorem defines is_vertex_seq_of GRAPH_2:def 2 :
for G being Graph
for vs being FinSequence of the carrier of G
for c being FinSequence holds
( vs is_vertex_seq_of c iff ( len vs = (len c) + 1 & ( for n being Nat st 1 <= n & n <= len c holds
c . n joins vs /. n,vs /. (n + 1) ) ) );

theorem Th31: :: GRAPH_2:31

for G being Graph
for vs being FinSequence of the carrier of G
for c being Chain of G st c <> {} & vs is_vertex_seq_of c holds
G -VSet (rng c) = rng vs

proof end;

theorem Th32: :: GRAPH_2:32

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

theorem Th33: :: GRAPH_2:33

for G being Graph
for c being Chain of G ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c

proof end;

theorem Th34: :: GRAPH_2:34

for G being Graph
for vs1, vs2 being FinSequence of the carrier of G
for c being Chain of G st c <> {} & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & vs1 <> vs2 holds
( vs1 . 1 <> vs2 . 1 & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )

proof end;

definition

let G be Graph;
let c be FinSequence;

pred c alternates_vertices_in G means :: GRAPH_2:def 3
( len c >= 1 & card (G -VSet (rng c)) = 2 & ( for n being Nat st n in dom c holds
the Source of G . (c . n) <> the Target of G . (c . n) ) );

end;

:: deftheorem defines alternates_vertices_in GRAPH_2:def 3 :
for G being Graph
for c being FinSequence holds
( c alternates_vertices_in G iff ( len c >= 1 & card (G -VSet (rng c)) = 2 & ( for n being Nat st n in dom c holds
the Source of G . (c . n) <> the Target of G . (c . n) ) ) );

theorem Th35: :: GRAPH_2:35

for G being Graph
for vs being FinSequence of the carrier of G
for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds
for k being Nat st k in dom c holds
vs . k <> vs . (k + 1)

proof end;

theorem Th36: :: GRAPH_2:36

for G being Graph
for vs being FinSequence of the carrier of G
for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds
rng vs = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}

proof end;

theorem Th37: :: GRAPH_2:37

for G being Graph
for vs being FinSequence of the carrier of G
for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds
vs is TwoValued Alternating FinSequence

proof end;

theorem Th38: :: GRAPH_2:38

for G being Graph
for c being Chain of G st c alternates_vertices_in G holds
ex vs1, vs2 being FinSequence of the carrier of G st
( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )

proof end;

Lm7: for D being non empty set st ( for x, y being set st x in D & y in D holds
x = y ) holds
card D = 1

proof end;

theorem Th39: :: GRAPH_2:39

for G being Graph
for vs being FinSequence of the carrier of G
for c being Chain of G st vs is_vertex_seq_of c holds
( ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) iff for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds
vs1 = vs )

proof end;

definition

let G be Graph;
let c be Chain of G;
assume A1: ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) ;

func vertex-seq c -> FinSequence of the carrier of G means :: GRAPH_2:def 4
it is_vertex_seq_of c;

existence
ex b₁ being FinSequence of the carrier of G st b₁ is_vertex_seq_of c by Th33;
uniqueness
for b₁, b₂ being FinSequence of the carrier of G st b₁ is_vertex_seq_of c & b₂ is_vertex_seq_of c holds
b₁ = b₂ by A1, Th39;

end;

:: deftheorem defines vertex-seq GRAPH_2:def 4 :
for G being Graph
for c being Chain of G st ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) holds
for b₃ being FinSequence of the carrier of G holds
( b₃ = vertex-seq c iff b₃ is_vertex_seq_of c );

theorem Th40: :: GRAPH_2:40

for n being Nat
for G being Graph
for vs, vs1 being FinSequence of the carrier of G
for c, c1 being Chain of G st vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds
vs1 is_vertex_seq_of c1

proof end;

theorem Th41: :: GRAPH_2:41

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

proof end;

theorem Th42: :: GRAPH_2:42

for m, n being Nat
for G being Graph
for vs, vs1 being FinSequence of the carrier of G
for c, c1 being Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds
vs1 is_vertex_seq_of c1

proof end;

theorem Th43: :: GRAPH_2:43

for G being Graph
for vs1, vs2 being FinSequence of the carrier of G
for c1, c2 being Chain of G st vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds
c1 ^ c2 is Chain of G

proof end;

theorem Th44: :: GRAPH_2:44

for G being Graph
for vs, vs1, vs2 being FinSequence of the carrier of G
for c, c1, c2 being Chain of G st vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds
vs is_vertex_seq_of c

proof end;

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

definition

let G be Graph;
let IT be Chain of G;

attr IT is simple means :Def9: :: GRAPH_2:def 5
ex vs being FinSequence of the carrier of G st
( vs is_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 Def9 defines simple GRAPH_2:def 5 :
for G being Graph
for IT being Chain of G holds
( IT is simple iff ex vs being FinSequence of the carrier of G st
( vs is_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 simple for Chain of G;

existence
ex b₁ being Chain of G st b₁ is simple

proof end;

end;

theorem :: GRAPH_2:45

for n being Nat
for G being Graph
for sc being simple Chain of G holds sc | (Seg n) is simple Chain of G

proof end;

theorem Th46: :: GRAPH_2:46

for G being Graph
for vs1, vs2 being FinSequence of the carrier of G
for sc being simple Chain of G st 2 < len sc & vs1 is_vertex_seq_of sc & vs2 is_vertex_seq_of sc holds
vs1 = vs2

proof end;

theorem :: GRAPH_2:47

for G being Graph
for vs being FinSequence of the carrier of G
for sc being simple Chain of G st vs is_vertex_seq_of sc holds
for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs )

proof end;

:: A chain may have more than one simple chain spanning its endpoints.
:: The following chain:
:: .--->.
:: ^ |
:: | v
:: .--->.<---.--->.
:: | ^
:: v |
:: .--->.
:: is a case in point:

theorem Th48: :: GRAPH_2:48

for G being Graph
for vs being FinSequence of the carrier of G
for c being Chain of G st c is not simple Chain of G & vs is_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_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_2:49

for G being Graph
for vs being FinSequence of the carrier of G
for c being Chain of G st vs is_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex sc being simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )

proof end;

registration

let G be Graph;

cluster empty -> V17() for Chain of G;

correctness
coherence
for b₁ being Chain of G st b₁ is empty holds
b₁ is V17();
;

end;

theorem :: GRAPH_2:50

for p being FinSequence
for n being Nat
for G being Graph st p is Path of G holds
p | (Seg n) is Path of G

proof end;

registration

let G be Graph;

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

existence
ex b₁ being Path of G st b₁ is simple

proof end;

end;

theorem :: GRAPH_2:51

for G being Graph
for sc being simple Chain of G st 2 < len sc holds
sc is Path of G

proof end;

theorem :: GRAPH_2:52

for G being Graph
for sc being simple Chain of G holds
( sc is Path of G iff ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) )

proof end;

registration

let G be Graph;

cluster empty -> oriented for Chain of G;

correctness
coherence
for b₁ being Chain of G st b₁ is empty holds
b₁ is oriented ;
;

end;

definition

let G be Graph;
let oc be oriented Chain of G;
assume A1: oc <> {} ;

func vertex-seq oc -> FinSequence of the carrier of G means :: GRAPH_2:def 6
( it is_vertex_seq_of oc & it . 1 = the Source of G . (oc . 1) );

existence
ex b₁ being FinSequence of the carrier of G st
( b₁ is_vertex_seq_of oc & b₁ . 1 = the Source of G . (oc . 1) )

proof end;

uniqueness
for b₁, b₂ being FinSequence of the carrier of G st b₁ is_vertex_seq_of oc & b₁ . 1 = the Source of G . (oc . 1) & b₂ is_vertex_seq_of oc & b₂ . 1 = the Source of G . (oc . 1) holds
b₁ = b₂ by A1, Th34;

end;

:: deftheorem defines vertex-seq GRAPH_2:def 6 :
for G being Graph
for oc being oriented Chain of G st oc <> {} holds
for b₃ being FinSequence of the carrier of G holds
( b₃ = vertex-seq oc iff ( b₃ is_vertex_seq_of oc & b₃ . 1 = the Source of G . (oc . 1) ) );