:: Vertex sequences induced by chains :: by Yatsuka Nakamura and Piotr Rudnicki :: :: Received May 13, 1995 :: Copyright (c) 1995-2012 Association of Mizar Users begin theorem Th1: :: GRAPH_2:1 for m, k, n being Nat holds ( ( m + 1 <= k & k <= n ) iff ex i being Element of NAT st ( m <= i & i < n & k = i + 1 ) ) proofend; theorem Th2: :: GRAPH_2:2 for q, p being FinSequence for n being Element of NAT st q = p | (Seg n) holds ( len q <= len p & ( for i being Element of NAT st 1 <= i & i <= len q holds p . i = q . i ) ) proofend; theorem Th3: :: GRAPH_2:3 for X, Y being set for k being Element of NAT st X c= Seg k & Y c= dom (Sgm X) holds (Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y)) proofend; Lm1: for m, n being Element of NAT for F being finite set st F = { k where k is Element of NAT : ( m <= k & k <= m + n ) } holds card F = n + 1 proofend; theorem Th4: :: GRAPH_2:4 for m, n being Element of NAT holds card { k where k is Element of NAT : ( m <= k & k <= m + n ) } = n + 1 proofend; theorem Th5: :: GRAPH_2:5 for n, m, l being Element of NAT st 1 <= l & l <= n holds (Sgm { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= m + n ) } ) . l = m + l proofend; begin definition let p be FinSequence; let m, n be Nat; func(m,n) -cut p -> FinSequence means :Def1: :: GRAPH_2:def 1 ( (len it) + m = n + 1 & ( for i being Nat st i < len it holds it . (i + 1) = p . (m + i) ) ) if ( 1 <= m & m <= n & n <= len p ) otherwise it = {} ; consistency for b1 being FinSequence holds verum ; existence ( ( 1 <= m & m <= n & n <= len p implies ex b1 being FinSequence st ( (len b1) + m = n + 1 & ( for i being Nat st i < len b1 holds b1 . (i + 1) = p . (m + i) ) ) ) & ( ( not 1 <= m or not m <= n or not n <= len p ) implies ex b1 being FinSequence st b1 = {} ) ) proofend; uniqueness for b1, b2 being FinSequence holds ( ( 1 <= m & m <= n & n <= len p & (len b1) + m = n + 1 & ( for i being Nat st i < len b1 holds b1 . (i + 1) = p . (m + i) ) & (len b2) + m = n + 1 & ( for i being Nat st i < len b2 holds b2 . (i + 1) = p . (m + i) ) implies b1 = b2 ) & ( ( not 1 <= m or not m <= n or not n <= len p ) & b1 = {} & b2 = {} implies b1 = b2 ) ) proofend; end; :: deftheorem Def1 defines -cut GRAPH_2:def_1_:_ for p being FinSequence for m, n being Nat for b4 being FinSequence holds ( ( 1 <= m & m <= n & n <= len p implies ( b4 = (m,n) -cut p iff ( (len b4) + m = n + 1 & ( for i being Nat st i < len b4 holds b4 . (i + 1) = p . (m + i) ) ) ) ) & ( ( not 1 <= m or not m <= n or not n <= len p ) implies ( b4 = (m,n) -cut p iff b4 = {} ) ) ); 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 Th6: :: GRAPH_2:6 for p being FinSequence for m being Element of NAT st 1 <= m & m <= len p holds (m,m) -cut p = <*(p . m)*> proofend; theorem Th7: :: GRAPH_2:7 for p being FinSequence holds (1,(len p)) -cut p = p proofend; theorem Th8: :: GRAPH_2:8 for p being FinSequence for m, n, r being Element of NAT st m <= n & n <= r & r <= len p holds (((m + 1),n) -cut p) ^ (((n + 1),r) -cut p) = ((m + 1),r) -cut p proofend; theorem :: GRAPH_2:9 for p being FinSequence for m being Element of NAT st m <= len p holds ((1,m) -cut p) ^ (((m + 1),(len p)) -cut p) = p proofend; theorem :: GRAPH_2:10 for p being FinSequence for m, n being Element of NAT st m <= n & n <= len p holds (((1,m) -cut p) ^ (((m + 1),n) -cut p)) ^ (((n + 1),(len p)) -cut p) = p proofend; theorem Th11: :: GRAPH_2:11 for p being FinSequence for m, n being Element of NAT holds rng ((m,n) -cut p) c= rng p proofend; definition let D be set ; let p be FinSequence of D; let m, n be Nat; :: original:-cut redefine func(m,n) -cut p -> FinSequence of D; coherence (m,n) -cut p is FinSequence of D proofend; end; theorem Th12: :: GRAPH_2:12 for p being FinSequence for m, n being Element of NAT st 1 <= m & m <= n & n <= len p holds ( ((m,n) -cut p) . 1 = p . m & ((m,n) -cut p) . (len ((m,n) -cut p)) = p . n ) proofend; begin definition let p, q be FinSequence; funcp ^' q -> FinSequence equals :: GRAPH_2:def 2 p ^ ((2,(len q)) -cut q); correctness coherence p ^ ((2,(len q)) -cut q) is FinSequence; ; end; :: deftheorem defines ^' GRAPH_2:def_2_:_ for p, q being FinSequence holds p ^' q = p ^ ((2,(len q)) -cut q); theorem Th13: :: GRAPH_2:13 for q, p being FinSequence st q <> {} holds (len (p ^' q)) + 1 = (len p) + (len q) proofend; theorem Th14: :: GRAPH_2:14 for p, q being FinSequence for k being Element of NAT st 1 <= k & k <= len p holds (p ^' q) . k = p . k proofend; theorem Th15: :: GRAPH_2:15 for q, p being FinSequence for k being Element of NAT st 1 <= k & k < len q holds (p ^' q) . ((len p) + k) = q . (k + 1) proofend; theorem Th16: :: GRAPH_2:16 for q, p being FinSequence st 1 < len q holds (p ^' q) . (len (p ^' q)) = q . (len q) proofend; theorem Th17: :: GRAPH_2:17 for p, q being FinSequence holds rng (p ^' q) c= (rng p) \/ (rng q) proofend; definition let D be set ; let p, q be FinSequence of D; :: original:^' redefine funcp ^' q -> FinSequence of D; coherence p ^' q is FinSequence of D proofend; end; theorem :: GRAPH_2:18 for p, q being FinSequence st p <> {} & q <> {} & p . (len p) = q . 1 holds rng (p ^' q) = (rng p) \/ (rng q) proofend; begin definition let f be FinSequence; attrf is TwoValued means :Def3: :: GRAPH_2:def 3 card (rng f) = 2; end; :: deftheorem Def3 defines TwoValued GRAPH_2:def_3_:_ for f being FinSequence holds ( f is TwoValued iff card (rng f) = 2 ); Lm3: now__::_thesis:_(_len_<*1,2*>_>_1_&_1_<>_2_&_rng_<*1,2*>_=_{1,2}_) set p = <*1,2*>; 2 > 1 ; hence len <*1,2*> > 1 by FINSEQ_1:44; ::_thesis: ( 1 <> 2 & rng <*1,2*> = {1,2} ) thus 1 <> 2 ; ::_thesis: rng <*1,2*> = {1,2} thus rng <*1,2*> = (rng <*1*>) \/ (rng <*2*>) by FINSEQ_1:31 .= {1} \/ (rng <*2*>) by FINSEQ_1:38 .= {1} \/ {2} by FINSEQ_1:38 .= {1,2} by ENUMSET1:1 ; ::_thesis: verum end; theorem Th19: :: GRAPH_2:19 for p being FinSequence holds ( p is TwoValued iff ( len p > 1 & ex x, y being set st ( x <> y & rng p = {x,y} ) ) ) proofend; then Lm4: <*1,2*> is TwoValued by Lm3; Lm5: now__::_thesis:_for_i_being_Nat_st_1_<=_i_&_i_+_1_<=_len_<*1,2*>_holds_ <*1,2*>_._i_<>_<*1,2*>_._(i_+_1) let i be Nat; ::_thesis: ( 1 <= i & i + 1 <= len <*1,2*> implies <*1,2*> . i <> <*1,2*> . (i + 1) ) set p = <*1,2*>; assume that A1: 1 <= i and A2: i + 1 <= len <*1,2*> ; ::_thesis: <*1,2*> . i <> <*1,2*> . (i + 1) i + 1 <= 1 + 1 by A2, FINSEQ_1:44; then i <= 1 by XREAL_1:6; then A3: i = 1 by A1, XXREAL_0:1; then <*1,2*> . i = 1 by FINSEQ_1:44; hence <*1,2*> . i <> <*1,2*> . (i + 1) by A3, FINSEQ_1:44; ::_thesis: verum end; definition let f be FinSequence; attrf is Alternating means :Def4: :: GRAPH_2:def 4 for i being Nat st 1 <= i & i + 1 <= len f holds f . i <> f . (i + 1); end; :: deftheorem Def4 defines Alternating GRAPH_2:def_4_:_ for f being FinSequence holds ( f is Alternating iff for i being Nat st 1 <= i & i + 1 <= len f holds f . i <> f . (i + 1) ); Lm6: <*1,2*> is Alternating by Def4, Lm5; registration cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like TwoValued Alternating for set ; existence ex b1 being FinSequence st ( b1 is TwoValued & b1 is Alternating ) by Lm4, Lm6; end; theorem Th20: :: GRAPH_2:20 for a1, a2 being TwoValued Alternating FinSequence st len a1 = len a2 & rng a1 = rng a2 & a1 . 1 = a2 . 1 holds a1 = a2 proofend; theorem Th21: :: GRAPH_2:21 for a1, a2 being TwoValued Alternating FinSequence st a1 <> a2 & len a1 = len a2 & rng a1 = rng a2 holds for i being Element of NAT st 1 <= i & i <= len a1 holds a1 . i <> a2 . i proofend; theorem Th22: :: GRAPH_2:22 for a1, a2 being TwoValued Alternating FinSequence st a1 <> a2 & len a1 = len a2 & rng a1 = rng a2 holds for a being TwoValued Alternating FinSequence st len a = len a1 & rng a = rng a1 & not a = a1 holds a = a2 proofend; theorem Th23: :: GRAPH_2:23 for X, Y being set for n being Element of NAT st X <> Y & n > 1 holds ex a1 being TwoValued Alternating FinSequence st ( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X ) proofend; begin registration let X be set ; let fs be FinSequence of X; cluster -> FinSubsequence-like for Element of bool fs; coherence for b1 being Subset of fs holds b1 is FinSubsequence-like proofend; end; theorem Th24: :: GRAPH_2:24 for f being FinSubsequence for g, h, fg, fh, fgh being FinSequence st rng g c= dom f & rng h c= dom f & fg = f * g & fh = f * h & fgh = f * (g ^ h) holds fgh = fg ^ fh proofend; theorem :: GRAPH_2:25 for X being set for fs being FinSequence of X for fss being Subset of fs holds ( dom fss c= dom fs & rng fss c= rng fs ) by RELAT_1:11; theorem Th26: :: GRAPH_2:26 for X being set for fs being FinSequence of X holds fs is Subset of fs proofend; theorem Th27: :: GRAPH_2:27 for X, Y being set for fs being FinSequence of X for fss being Subset of fs holds fss | Y is Subset of fs proofend; theorem Th28: :: GRAPH_2:28 for X being set for fs, fs1, fs2 being FinSequence of X for fss, fss2 being Subset of fs for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) holds Seq fss2 = fs2 proofend; begin theorem Th29: :: GRAPH_2:29 for G being Graph for v1, v2 being Element of G for e being set st e joins v1,v2 holds e joins v2,v1 proofend; theorem Th30: :: GRAPH_2:30 for G being Graph for v1, v2, v3, v4 being Element of G for e being set st e joins v1,v2 & e joins v3,v4 & not ( v1 = v3 & v2 = v4 ) holds ( v1 = v4 & v2 = v3 ) proofend; definition let G be Graph; let X be set ; funcG -VSet X -> set equals :: GRAPH_2:def 5 { 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_5_:_ 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; predvs is_vertex_seq_of c means :Def6: :: GRAPH_2:def 6 ( len vs = (len c) + 1 & ( for n being Element of NAT st 1 <= n & n <= len c holds c . n joins vs /. n,vs /. (n + 1) ) ); end; :: deftheorem Def6 defines is_vertex_seq_of GRAPH_2:def_6_:_ 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 Element of 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 proofend; theorem Th32: :: GRAPH_2:32 for G being Graph for v being Element of G holds <*v*> is_vertex_seq_of {} proofend; 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 proofend; 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 ) ) ) proofend; definition let G be Graph; let c be FinSequence; predc alternates_vertices_in G means :Def7: :: GRAPH_2:def 7 ( len c >= 1 & card (G -VSet (rng c)) = 2 & ( for n being Element of NAT st n in dom c holds the Source of G . (c . n) <> the Target of G . (c . n) ) ); end; :: deftheorem Def7 defines alternates_vertices_in GRAPH_2:def_7_:_ 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 Element of 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 Element of NAT st k in dom c holds vs . k <> vs . (k + 1) proofend; 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))} proofend; 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 proofend; 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 ) ) ) proofend; 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 proofend; 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 ) proofend; 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 8 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 A1, Th39; end; :: deftheorem defines vertex-seq GRAPH_2:def_8_:_ 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 Element of 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 proofend; theorem Th41: :: GRAPH_2:41 for q being FinSequence for m, n being Element of 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 proofend; theorem Th42: :: GRAPH_2:42 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 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 proofend; 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 proofend; theorem Th44: :: GRAPH_2:44 for G being Graph for vs1, vs2, vs being FinSequence of the carrier of G for c1, c2, c 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 proofend; begin Lm8: for G being Graph for v being Element of G holds <*v*> is_vertex_seq_of {} proofend; definition let G be Graph; let IT be Chain of G; attrIT is simple means :Def9: :: GRAPH_2:def 9 ex vs being FinSequence of the carrier of G st ( vs is_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 Def9 defines simple GRAPH_2:def_9_:_ 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 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 simple for Chain of G; existence ex b1 being Chain of G st b1 is simple proofend; end; theorem :: GRAPH_2:45 for n being Element of NAT for G being Graph for sc being simple Chain of G holds sc | (Seg n) is simple Chain of G proofend; 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 proofend; 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 Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds ( n = 1 & m = len vs ) proofend; :: 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 ) proofend; 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) ) proofend; registration let G be Graph; cluster empty -> V14() for Chain of G; correctness coherence for b1 being Chain of G st b1 is empty holds b1 is V14(); ; end; theorem :: GRAPH_2:50 for p being FinSequence for n being Element of NAT for G being Graph st p is Path of G holds p | (Seg n) is Path of G proofend; 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 b1 being Path of G st b1 is simple proofend; 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 proofend; 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 ) ) proofend; 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 10 ( 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) ) proofend; 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 A1, Th34; end; :: deftheorem defines vertex-seq GRAPH_2:def_10_:_ 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) ) ); begin :: from AMISTD_1, 2006.01.12, A.T. theorem :: GRAPH_2:53 for D being non empty set for f1 being non empty FinSequence of D for f2 being FinSequence of D holds (f1 ^' f2) /. 1 = f1 /. 1 proofend; theorem :: GRAPH_2:54 for D being non empty set for f1 being FinSequence of D for f2 being non trivial FinSequence of D holds (f1 ^' f2) /. (len (f1 ^' f2)) = f2 /. (len f2) proofend; theorem Th55: :: GRAPH_2:55 for f being FinSequence holds f ^' {} = f proofend; theorem :: GRAPH_2:56 for x being set for f being FinSequence holds f ^' <*x*> = f proofend; theorem :: GRAPH_2:57 for D being non empty set for n being Element of NAT for f1, f2 being FinSequence of D st 1 <= n & n <= len f1 holds (f1 ^' f2) /. n = f1 /. n proofend; theorem :: GRAPH_2:58 for D being non empty set for n being Element of NAT for f1, f2 being FinSequence of D st 1 <= n & n < len f2 holds (f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1) proofend; :: from SFMATR3, 2007.07.26, A.T. definition let F be FinSequence of INT ; let m, n be Element of NAT ; assume that A1: 1 <= m and A2: m <= n and A3: n <= len F ; func min_at (F,m,n) -> Element of NAT means :Def11: :: GRAPH_2:def 11 ex X being non empty finite Subset of INT st ( X = rng ((m,n) -cut F) & it + 1 = ((min X) .. ((m,n) -cut F)) + m ); existence ex b1 being Element of NAT ex X being non empty finite Subset of INT st ( X = rng ((m,n) -cut F) & b1 + 1 = ((min X) .. ((m,n) -cut F)) + m ) proofend; uniqueness for b1, b2 being Element of NAT st ex X being non empty finite Subset of INT st ( X = rng ((m,n) -cut F) & b1 + 1 = ((min X) .. ((m,n) -cut F)) + m ) & ex X being non empty finite Subset of INT st ( X = rng ((m,n) -cut F) & b2 + 1 = ((min X) .. ((m,n) -cut F)) + m ) holds b1 = b2 ; end; :: deftheorem Def11 defines min_at GRAPH_2:def_11_:_ for F being FinSequence of INT for m, n being Element of NAT st 1 <= m & m <= n & n <= len F holds for b4 being Element of NAT holds ( b4 = min_at (F,m,n) iff ex X being non empty finite Subset of INT st ( X = rng ((m,n) -cut F) & b4 + 1 = ((min X) .. ((m,n) -cut F)) + m ) ); theorem Th59: :: GRAPH_2:59 for F being FinSequence of INT for m, n, ma being Element of NAT st 1 <= m & m <= n & n <= len F holds ( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Element of NAT st m <= i & i <= n holds F . ma <= F . i ) & ( for i being Element of NAT st m <= i & i < ma holds F . ma < F . i ) ) ) proofend; theorem :: GRAPH_2:60 for F being FinSequence of INT for m being Element of NAT st 1 <= m & m <= len F holds min_at (F,m,m) = m proofend; definition let F be FinSequence of INT ; let m, n be Element of NAT ; predF is_non_decreasing_on m,n means :Def12: :: GRAPH_2:def 12 for i, j being Element of NAT st m <= i & i <= j & j <= n holds F . i <= F . j; end; :: deftheorem Def12 defines is_non_decreasing_on GRAPH_2:def_12_:_ for F being FinSequence of INT for m, n being Element of NAT holds ( F is_non_decreasing_on m,n iff for i, j being Element of NAT st m <= i & i <= j & j <= n holds F . i <= F . j ); definition let F be FinSequence of INT ; let n be Element of NAT ; predF is_split_at n means :Def13: :: GRAPH_2:def 13 for i, j being Element of NAT st 1 <= i & i <= n & n < j & j <= len F holds F . i <= F . j; end; :: deftheorem Def13 defines is_split_at GRAPH_2:def_13_:_ for F being FinSequence of INT for n being Element of NAT holds ( F is_split_at n iff for i, j being Element of NAT st 1 <= i & i <= n & n < j & j <= len F holds F . i <= F . j ); theorem :: GRAPH_2:61 for F, F1 being FinSequence of INT for k, ma being Element of NAT st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F is_non_decreasing_on 1,k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds F1 is_non_decreasing_on 1,k + 1 proofend; theorem :: GRAPH_2:62 for F, F1 being FinSequence of INT for k, ma being Element of NAT st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds F1 is_split_at k + 1 proofend; :: from SCPISORT, 2011.02.13 theorem :: GRAPH_2:63 for f being FinSequence of INT for m, n being Element of NAT st m >= n holds f is_non_decreasing_on m,n proofend;