:: Oriented Simple Chains Included in Oriented Chains :: by Yatsuka Nakamura and Piotr Rudnicki :: :: Received August 19, 1998 :: Copyright (c) 1998-2012 Association of Mizar Users begin definition let G be Graph; let x, y be Element of G; let e be set ; prede 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_:_ 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 proofend; definition let G be Graph; let x, y be Element of the carrier of G; predx,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 Th2: :: 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 ) proofend; definition let G be Graph; let X be set ; funcG -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 ; funcG -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 {} = {} ) proofend; definition let G be Graph; let vs be FinSequence of the carrier of G; let c be FinSequence; predvs is_oriented_vertex_seq_of c means :Def5: :: GRAPH_4:def 5 ( len vs = (len c) + 1 & ( for n being Element of 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_:_ 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 Element of 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 proofend; 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 proofend; 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 proofend; 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)) proofend; begin theorem :: GRAPH_4:8 for G being Graph for v being Element of G holds <*v*> is_oriented_vertex_seq_of {} proofend; 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 proofend; 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 proofend; 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 Element of 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 proofend; theorem Th12: :: GRAPH_4:12 for q being FinSequence for m, n being Element of 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 proofend; theorem Th13: :: GRAPH_4:13 for m, n being Element of 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 proofend; 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 proofend; theorem Th15: :: GRAPH_4:15 for G being Graph for vs1, vs2, vs being FinSequence of the carrier 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 proofend; begin Lm1: for G being Graph for v being Element of G holds <*v*> is_oriented_vertex_seq_of {} proofend; definition let G be Graph; let IT be oriented Chain of G; attrIT 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 Element of 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 Element of 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 proofend; 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 ) proofend; end; theorem Th16: :: GRAPH_4:16 for n being Element of NAT for G being Graph for q being oriented Chain of G holds q | (Seg n) is oriented Chain of G proofend; theorem :: GRAPH_4:17 for n being Element of 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 proofend; 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 proofend; Lm2: for p being FinSequence for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds ((m,n) -cut p) . (i + 1) = p . (m + i) ) ) proofend; 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 ) proofend; 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) ) proofend; theorem :: GRAPH_4:22 for p being FinSequence for n being Element of NAT for G being Graph st p is OrientedPath of G holds p | (Seg n) is OrientedPath of G proofend; theorem Th23: :: GRAPH_4:23 for G being Graph for sc being oriented simple Chain of G holds sc is OrientedPath of G proofend; 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;