:: Vertex sequences induced by chains
:: by Yatsuka Nakamura and Piotr Rudnicki
::
:: 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 b1 being FinSequence of the carrier of G st b1 is_vertex_seq_of c
by Th33;
uniqueness
for b1, b2 being FinSequence of the carrier of G st b1 is_vertex_seq_of c & b2 is_vertex_seq_of c holds
b1 = b2
by ;
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 b3 being FinSequence of the carrier of G holds
( b3 = vertex-seq c iff b3 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;
existence
ex b1 being Chain of G st b1 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 b1 being Chain of G st b1 is empty holds
b1 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;
existence
ex b1 being Path of G st b1 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 b1 being Chain of G st b1 is empty holds
b1 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 b1 being FinSequence of the carrier of G st
( b1 is_vertex_seq_of oc & b1 . 1 = the Source of G . (oc . 1) )
proof end;
uniqueness
for b1, b2 being FinSequence of the carrier of G st b1 is_vertex_seq_of oc & b1 . 1 = the Source of G . (oc . 1) & b2 is_vertex_seq_of oc & b2 . 1 = the Source of G . (oc . 1) holds
b1 = b2
by ;
end;

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