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

environ

vocabularies HIDDEN, NUMBERS, FINSEQ_1, SUBSET_1, GRAPH_1, FUNCT_1, STRUCT_0, TREES_2, XBOOLE_0, ARYTM_3, XXREAL_0, PARTFUN1, GRAPH_2, RELAT_1, TARSKI, CARD_1, NAT_1, ARYTM_1, ORDINAL4, GLIB_000, FINSET_1, FINSEQ_2, GRAPH_4;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, CARD_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, NAT_D, STRUCT_0, GRAPH_1, GRAPH_2, XXREAL_0;
definitions TARSKI;
theorems TARSKI, NAT_1, FINSEQ_1, FINSEQ_2, GRAPH_1, RELAT_1, FUNCT_1, GRFUNC_1, FUNCT_2, FINSET_1, FINSEQ_3, FINSEQ_4, GRAPH_2, XBOOLE_0, XBOOLE_1, XREAL_1, CARD_1, XXREAL_0, ORDINAL1, NAT_D, XREAL_0;
schemes NAT_1, FINSEQ_1, FUNCT_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_1, GRAPH_2, ORDINAL1, CARD_1, STRUCT_0, GRAPH_1;
constructors HIDDEN, RECDEF_1, GRAPH_2, NAT_D, FINSEQ_2, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities FINSEQ_2;
expansions ;


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 b1 being FinSequence of the carrier of G st b1 is_oriented_vertex_seq_of c by Th9;
uniqueness
for b1, b2 being FinSequence of the carrier of G st b1 is_oriented_vertex_seq_of c & b2 is_oriented_vertex_seq_of c holds
b1 = b2 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 b3 being FinSequence of the carrier of G holds
( b3 = oriented-vertex-seq c iff b3 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 b1 being oriented Chain of G st b1 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 b1 being Chain of G st
( b1 is oriented & b1 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;