:: GRAPH_5 semantic presentation begin theorem Th1: :: GRAPH_5:1 for x being set for f, g being Function st rng f c= rng g & x in dom f holds ex y being set st ( y in dom g & f . x = g . y ) proof let x be set ; ::_thesis: for f, g being Function st rng f c= rng g & x in dom f holds ex y being set st ( y in dom g & f . x = g . y ) let f, g be Function; ::_thesis: ( rng f c= rng g & x in dom f implies ex y being set st ( y in dom g & f . x = g . y ) ) assume that A1: rng f c= rng g and A2: x in dom f ; ::_thesis: ex y being set st ( y in dom g & f . x = g . y ) f . x in rng f by A2, FUNCT_1:3; hence ex y being set st ( y in dom g & f . x = g . y ) by A1, FUNCT_1:def_3; ::_thesis: verum end; scheme :: GRAPH_5:sch 1 LambdaAB{ F1() -> set , F2() -> set , F3( Element of F2()) -> set } : ex f being Function st ( dom f = F1() & ( for x being Element of F2() st x in F1() holds f . x = F3(x) ) ) proof defpred S1[ set , set ] means ( ( $1 is Element of F2() implies ex x being Element of F2() st ( x = $1 & $2 = F3(x) ) ) & ( $1 is not Element of F2() implies $2 = 0 ) ); A1: for x being set st x in F1() holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in F1() implies ex y being set st S1[x,y] ) assume x in F1() ; ::_thesis: ex y being set st S1[x,y] percases ( x is Element of F2() or not x is Element of F2() ) ; suppose x is Element of F2() ; ::_thesis: ex y being set st S1[x,y] then reconsider z = x as Element of F2() ; take F3(z) ; ::_thesis: S1[x,F3(z)] thus S1[x,F3(z)] ; ::_thesis: verum end; supposeA2: x is not Element of F2() ; ::_thesis: ex y being set st S1[x,y] take 0 ; ::_thesis: S1[x, 0 ] thus S1[x, 0 ] by A2; ::_thesis: verum end; end; end; ex f being Function st ( dom f = F1() & ( for x being set st x in F1() holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); then consider f being Function such that A3: dom f = F1() and A4: for x being set st x in F1() holds S1[x,f . x] ; take f ; ::_thesis: ( dom f = F1() & ( for x being Element of F2() st x in F1() holds f . x = F3(x) ) ) now__::_thesis:_for_x_being_Element_of_F2()_st_x_in_F1()_holds_ f_._x_=_F3(x) let x be Element of F2(); ::_thesis: ( x in F1() implies f . x = F3(x) ) assume x in F1() ; ::_thesis: f . x = F3(x) then S1[x,f . x] by A4; hence f . x = F3(x) ; ::_thesis: verum end; hence ( dom f = F1() & ( for x being Element of F2() st x in F1() holds f . x = F3(x) ) ) by A3; ::_thesis: verum end; theorem Th2: :: GRAPH_5:2 for D being finite set for n being Element of NAT for X being set st X = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } holds X is finite proof let D be finite set ; ::_thesis: for n being Element of NAT for X being set st X = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } holds X is finite let n be Element of NAT ; ::_thesis: for X being set st X = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } holds X is finite let X be set ; ::_thesis: ( X = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } implies X is finite ) deffunc H1( Element of NAT ) -> FinSequenceSet of D = $1 -tuples_on D; consider f being Function such that A1: ( dom f = Seg n & ( for x being Element of NAT st x in Seg n holds f . x = H1(x) ) ) from GRAPH_5:sch_1(); assume A2: X = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } ; ::_thesis: X is finite A3: X c= Union f proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in Union f ) assume x in X ; ::_thesis: x in Union f then consider y being Element of D * such that A4: x = y and A5: ( 1 <= len y & len y <= n ) by A2; consider m being Nat such that A6: dom y = Seg m by FINSEQ_1:def_2; m in NAT by ORDINAL1:def_12; then A7: len y = m by A6, FINSEQ_1:def_3; then A8: m in dom f by A1, A5, FINSEQ_1:1; y in { s where s is Element of D * : len s = m } by A7; then y in m -tuples_on D by FINSEQ_2:def_4; then y in f . m by A1, A8; hence x in Union f by A4, A8, CARD_5:2; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_is_finite let x be set ; ::_thesis: ( x in dom f implies f . x is finite ) assume A9: x in dom f ; ::_thesis: f . x is finite then reconsider z = x as Element of NAT by A1; f . z = H1(z) by A1, A9; hence f . x is finite ; ::_thesis: verum end; then Union f is finite by A1, CARD_2:88; hence X is finite by A3; ::_thesis: verum end; theorem Th3: :: GRAPH_5:3 for D being finite set for n being Element of NAT for X being set st X = { x where x is Element of D * : len x <= n } holds X is finite proof let D be finite set ; ::_thesis: for n being Element of NAT for X being set st X = { x where x is Element of D * : len x <= n } holds X is finite let n be Element of NAT ; ::_thesis: for X being set st X = { x where x is Element of D * : len x <= n } holds X is finite let X be set ; ::_thesis: ( X = { x where x is Element of D * : len x <= n } implies X is finite ) set B = { x where x is Element of D * : ( 1 <= len x & len x <= n ) } ; assume A1: X = { x where x is Element of D * : len x <= n } ; ::_thesis: X is finite A2: X c= {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) } proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in X or y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) } ) assume y in X ; ::_thesis: y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) } then consider x being Element of D * such that A3: y = x and A4: len x <= n by A1; percases ( len x < 0 + 1 or len x >= 0 + 1 ) ; suppose len x < 0 + 1 ; ::_thesis: y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) } then x = {} by NAT_1:13; then x in {{}} by TARSKI:def_1; hence y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) } by A3, XBOOLE_0:def_3; ::_thesis: verum end; suppose len x >= 0 + 1 ; ::_thesis: y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) } then x in { x where x is Element of D * : ( 1 <= len x & len x <= n ) } by A4; hence y in {{}} \/ { x where x is Element of D * : ( 1 <= len x & len x <= n ) } by A3, XBOOLE_0:def_3; ::_thesis: verum end; end; end; { x where x is Element of D * : ( 1 <= len x & len x <= n ) } is finite by Th2; hence X is finite by A2; ::_thesis: verum end; theorem Th4: :: GRAPH_5:4 for D being finite set for k being Element of NAT st card D = k + 1 holds ex x being Element of D ex C being Subset of D st ( D = C \/ {x} & card C = k ) proof let D be finite set ; ::_thesis: for k being Element of NAT st card D = k + 1 holds ex x being Element of D ex C being Subset of D st ( D = C \/ {x} & card C = k ) let k be Element of NAT ; ::_thesis: ( card D = k + 1 implies ex x being Element of D ex C being Subset of D st ( D = C \/ {x} & card C = k ) ) assume A1: card D = k + 1 ; ::_thesis: ex x being Element of D ex C being Subset of D st ( D = C \/ {x} & card C = k ) then D <> {} ; then consider x being set such that A2: x in D by XBOOLE_0:def_1; reconsider C = D \ {x} as Subset of D ; reconsider x = x as Element of D by A2; take x ; ::_thesis: ex C being Subset of D st ( D = C \/ {x} & card C = k ) take C ; ::_thesis: ( D = C \/ {x} & card C = k ) x in {x} by TARSKI:def_1; then A3: not x in C by XBOOLE_0:def_5; {x} c= D by A2, ZFMISC_1:31; hence D = C \/ {x} by XBOOLE_1:45; ::_thesis: card C = k then card D = (card C) + 1 by A3, CARD_2:41; hence card C = k by A1; ::_thesis: verum end; theorem Th5: :: GRAPH_5:5 for D being finite set st card D = 1 holds ex x being Element of D st D = {x} proof let D be finite set ; ::_thesis: ( card D = 1 implies ex x being Element of D st D = {x} ) assume card D = 1 ; ::_thesis: ex x being Element of D st D = {x} then card D = 0 + 1 ; then consider x being Element of D, C being Subset of D such that A1: D = C \/ {x} and A2: card C = 0 by Th4; take x ; ::_thesis: D = {x} C = {} by A2; hence D = {x} by A1; ::_thesis: verum end; scheme :: GRAPH_5:sch 2 MinValue{ F1() -> non empty finite set , F2( Element of F1()) -> real number } : ex x being Element of F1() st for y being Element of F1() holds F2(x) <= F2(y) proof defpred S1[ Element of NAT ] means for A being Subset of F1() st $1 + 1 = card A holds ex x being Element of F1() st ( x in A & ( for y being Element of F1() st y in A holds F2(x) <= F2(y) ) ); A1: ((card F1()) -' 1) + 1 = ((card F1()) - 1) + 1 by PRE_CIRC:20 .= card F1() ; A2: F1() c= F1() ; A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_A_being_Subset_of_F1()_st_(k_+_1)_+_1_=_card_A_holds_ ex_x_being_Element_of_F1()_st_ (_x_in_A_&_(_for_y_being_Element_of_F1()_st_y_in_A_holds_ F2(x)_<=_F2(y)_)_) let A be Subset of F1(); ::_thesis: ( (k + 1) + 1 = card A implies ex x being Element of F1() st ( b2 in x & ( for y being Element of F1() st b3 in x holds F2(y) <= F2(b3) ) ) ) assume A5: (k + 1) + 1 = card A ; ::_thesis: ex x being Element of F1() st ( b2 in x & ( for y being Element of F1() st b3 in x holds F2(y) <= F2(b3) ) ) then A6: A <> {} ; consider x being Element of A, C being Subset of A such that A7: A = C \/ {x} and A8: card C = k + 1 by A5, Th4; x in A by A6; then reconsider x = x as Element of F1() ; reconsider C = C as Subset of F1() by XBOOLE_1:1; consider z being Element of F1() such that A9: z in C and A10: for y being Element of F1() st y in C holds F2(z) <= F2(y) by A4, A8; percases ( F2(x) <= F2(z) or F2(x) > F2(z) ) ; supposeA11: F2(x) <= F2(z) ; ::_thesis: ex x being Element of F1() st ( b2 in x & ( for y being Element of F1() st b3 in x holds F2(y) <= F2(b3) ) ) take x = x; ::_thesis: ( x in A & ( for y being Element of F1() st y in A holds F2(x) <= F2(y) ) ) thus x in A by A6; ::_thesis: for y being Element of F1() st y in A holds F2(x) <= F2(y) hereby ::_thesis: verum let y be Element of F1(); ::_thesis: ( y in A implies F2(x) <= F2(b1) ) assume A12: y in A ; ::_thesis: F2(x) <= F2(b1) percases ( y in C or y in {x} ) by A7, A12, XBOOLE_0:def_3; suppose y in C ; ::_thesis: F2(x) <= F2(b1) then F2(z) <= F2(y) by A10; hence F2(x) <= F2(y) by A11, XXREAL_0:2; ::_thesis: verum end; suppose y in {x} ; ::_thesis: F2(x) <= F2(b1) hence F2(x) <= F2(y) by TARSKI:def_1; ::_thesis: verum end; end; end; end; supposeA13: F2(x) > F2(z) ; ::_thesis: ex z being Element of F1() st ( b2 in z & ( for y being Element of F1() st b3 in z holds F2(y) <= F2(b3) ) ) take z = z; ::_thesis: ( z in A & ( for y being Element of F1() st y in A holds F2(z) <= F2(y) ) ) thus z in A by A9; ::_thesis: for y being Element of F1() st y in A holds F2(z) <= F2(y) hereby ::_thesis: verum let y be Element of F1(); ::_thesis: ( y in A implies F2(z) <= F2(b1) ) assume A14: y in A ; ::_thesis: F2(z) <= F2(b1) percases ( y in C or y in {x} ) by A7, A14, XBOOLE_0:def_3; suppose y in C ; ::_thesis: F2(z) <= F2(b1) hence F2(z) <= F2(y) by A10; ::_thesis: verum end; suppose y in {x} ; ::_thesis: F2(z) <= F2(b1) hence F2(z) <= F2(y) by A13, TARSKI:def_1; ::_thesis: verum end; end; end; end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A15: S1[ 0 ] proof let A be Subset of F1(); ::_thesis: ( 0 + 1 = card A implies ex x being Element of F1() st ( x in A & ( for y being Element of F1() st y in A holds F2(x) <= F2(y) ) ) ) assume 0 + 1 = card A ; ::_thesis: ex x being Element of F1() st ( x in A & ( for y being Element of F1() st y in A holds F2(x) <= F2(y) ) ) then consider x being Element of A such that A16: A = {x} by Th5; reconsider x = x as Element of F1() by A16, ZFMISC_1:31; take x ; ::_thesis: ( x in A & ( for y being Element of F1() st y in A holds F2(x) <= F2(y) ) ) thus x in A by A16; ::_thesis: for y being Element of F1() st y in A holds F2(x) <= F2(y) thus for y being Element of F1() st y in A holds F2(x) <= F2(y) by A16, TARSKI:def_1; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A3); then consider x being Element of F1() such that x in F1() and A17: for y being Element of F1() st y in F1() holds F2(x) <= F2(y) by A1, A2; take x ; ::_thesis: for y being Element of F1() holds F2(x) <= F2(y) let y be Element of F1(); ::_thesis: F2(x) <= F2(y) thus F2(x) <= F2(y) by A17; ::_thesis: verum end; definition let D be set ; let X be non empty Subset of (D *); :: original: Element redefine mode Element of X -> FinSequence of D; coherence for b1 being Element of X holds b1 is FinSequence of D proof let x be Element of X; ::_thesis: x is FinSequence of D reconsider y = x as Element of D * ; y is FinSequence of D ; hence x is FinSequence of D ; ::_thesis: verum end; end; begin Lm1: for n being Element of NAT for p, q being FinSequence st 1 <= n & n <= len p holds p . n = (p ^ q) . n proof let n be Element of NAT ; ::_thesis: for p, q being FinSequence st 1 <= n & n <= len p holds p . n = (p ^ q) . n let p, q be FinSequence; ::_thesis: ( 1 <= n & n <= len p implies p . n = (p ^ q) . n ) assume ( 1 <= n & n <= len p ) ; ::_thesis: p . n = (p ^ q) . n then n in dom p by FINSEQ_3:25; hence p . n = (p ^ q) . n by FINSEQ_1:def_7; ::_thesis: verum end; Lm2: for n being Element of NAT for q, p being FinSequence st 1 <= n & n <= len q holds q . n = (p ^ q) . ((len p) + n) proof let n be Element of NAT ; ::_thesis: for q, p being FinSequence st 1 <= n & n <= len q holds q . n = (p ^ q) . ((len p) + n) let q, p be FinSequence; ::_thesis: ( 1 <= n & n <= len q implies q . n = (p ^ q) . ((len p) + n) ) assume ( 1 <= n & n <= len q ) ; ::_thesis: q . n = (p ^ q) . ((len p) + n) then n in dom q by FINSEQ_3:25; hence q . n = (p ^ q) . ((len p) + n) by FINSEQ_1:def_7; ::_thesis: verum end; theorem Th6: :: GRAPH_5:6 for p being FinSequence holds ( ( for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds p . n <> p . m ) iff p is one-to-one ) proof let p be FinSequence; ::_thesis: ( ( for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds p . n <> p . m ) iff p is one-to-one ) hereby ::_thesis: ( p is one-to-one implies for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds p . n <> p . m ) assume A1: for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds p . n <> p . m ; ::_thesis: p is one-to-one thus p is one-to-one ::_thesis: verum proof let x1, x2 be set ; :: according to FUNCT_1:def_4 ::_thesis: ( not x1 in dom p or not x2 in dom p or not p . x1 = p . x2 or x1 = x2 ) assume that A2: ( x1 in dom p & x2 in dom p ) and A3: p . x1 = p . x2 ; ::_thesis: x1 = x2 reconsider n = x1, m = x2 as Element of NAT by A2; A4: ( n <= len p & 1 <= m ) by A2, FINSEQ_3:25; A5: ( 1 <= n & m <= len p ) by A2, FINSEQ_3:25; assume A6: x1 <> x2 ; ::_thesis: contradiction percases ( m <= n or m > n ) ; suppose m <= n ; ::_thesis: contradiction then m < n by A6, XXREAL_0:1; hence contradiction by A1, A3, A4; ::_thesis: verum end; suppose m > n ; ::_thesis: contradiction hence contradiction by A1, A3, A5; ::_thesis: verum end; end; end; end; assume A7: p is one-to-one ; ::_thesis: for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds p . n <> p . m let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len p implies p . n <> p . m ) assume that A8: 1 <= n and A9: n < m and A10: m <= len p ; ::_thesis: p . n <> p . m n <= len p by A9, A10, XXREAL_0:2; then A11: n in dom p by A8, FINSEQ_3:25; 1 <= m by A8, A9, XXREAL_0:2; then A12: m in dom p by A10, FINSEQ_3:25; assume p . n = p . m ; ::_thesis: contradiction hence contradiction by A7, A9, A11, A12, FUNCT_1:def_4; ::_thesis: verum end; theorem Th7: :: GRAPH_5:7 for p being FinSequence holds ( ( for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds p . n <> p . m ) iff card (rng p) = len p ) proof let p be FinSequence; ::_thesis: ( ( for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds p . n <> p . m ) iff card (rng p) = len p ) ( p is one-to-one iff card (rng p) = len p ) by FINSEQ_4:62; hence ( ( for n, m being Element of NAT st 1 <= n & n < m & m <= len p holds p . n <> p . m ) iff card (rng p) = len p ) by Th6; ::_thesis: verum end; theorem :: GRAPH_5:8 for i being Element of NAT for G being Graph for pe being FinSequence of the carrier' of G st i in dom pe holds ( the Source of G . (pe . i) in the carrier of G & the Target of G . (pe . i) in the carrier of G ) by FINSEQ_2:11, FUNCT_2:5; theorem Th9: :: GRAPH_5:9 for x being set for q, p being FinSequence st q ^ <*x*> is one-to-one & rng (q ^ <*x*>) c= rng p holds ex p1, p2 being FinSequence st ( p = (p1 ^ <*x*>) ^ p2 & rng q c= rng (p1 ^ p2) ) proof let x be set ; ::_thesis: for q, p being FinSequence st q ^ <*x*> is one-to-one & rng (q ^ <*x*>) c= rng p holds ex p1, p2 being FinSequence st ( p = (p1 ^ <*x*>) ^ p2 & rng q c= rng (p1 ^ p2) ) let q, p be FinSequence; ::_thesis: ( q ^ <*x*> is one-to-one & rng (q ^ <*x*>) c= rng p implies ex p1, p2 being FinSequence st ( p = (p1 ^ <*x*>) ^ p2 & rng q c= rng (p1 ^ p2) ) ) set r = q ^ <*x*>; set i = (len q) + 1; assume that A1: q ^ <*x*> is one-to-one and A2: rng (q ^ <*x*>) c= rng p ; ::_thesis: ex p1, p2 being FinSequence st ( p = (p1 ^ <*x*>) ^ p2 & rng q c= rng (p1 ^ p2) ) A3: (q ^ <*x*>) . ((len q) + 1) = x by FINSEQ_1:42; rng q c= rng (q ^ <*x*>) by FINSEQ_1:29; then A4: rng q c= rng p by A2, XBOOLE_1:1; ( len (q ^ <*x*>) = (len q) + 1 & 1 <= (len q) + 1 ) by FINSEQ_2:16, NAT_1:11; then A5: (len q) + 1 in dom (q ^ <*x*>) by FINSEQ_3:25; then consider y being set such that A6: y in dom p and A7: (q ^ <*x*>) . ((len q) + 1) = p . y by A2, Th1; reconsider j = y as Element of NAT by A6; j <= len p by A6, FINSEQ_3:25; then consider k being Nat such that A8: len p = j + k by NAT_1:10; reconsider k = k as Element of NAT by ORDINAL1:def_12; consider s, p2 being FinSequence such that A9: len s = j and len p2 = k and A10: p = s ^ p2 by A8, FINSEQ_2:22; A11: 1 <= j by A6, FINSEQ_3:25; then ex m being Nat st j = 1 + m by NAT_1:10; then consider p1 being FinSequence, d being set such that A12: s = p1 ^ <*d*> by A9, FINSEQ_2:18; j in dom s by A9, A11, FINSEQ_3:25; then A13: s . j = x by A7, A10, A3, FINSEQ_1:def_7; take p1 ; ::_thesis: ex p2 being FinSequence st ( p = (p1 ^ <*x*>) ^ p2 & rng q c= rng (p1 ^ p2) ) take p2 ; ::_thesis: ( p = (p1 ^ <*x*>) ^ p2 & rng q c= rng (p1 ^ p2) ) A14: j = (len p1) + 1 by A9, A12, FINSEQ_2:16; hence p = (p1 ^ <*x*>) ^ p2 by A10, A12, A13, FINSEQ_1:42; ::_thesis: rng q c= rng (p1 ^ p2) let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng q or y in rng (p1 ^ p2) ) assume A15: y in rng q ; ::_thesis: y in rng (p1 ^ p2) now__::_thesis:_for_y_being_set_st_y_in_rng_q_holds_ not_y_=_x let y be set ; ::_thesis: ( y in rng q implies not y = x ) assume A16: y in rng q ; ::_thesis: not y = x assume y = x ; ::_thesis: contradiction then consider z being set such that A17: z in dom q and A18: x = q . z by A16, FUNCT_1:def_3; reconsider n = z as Element of NAT by A17; n <= len q by A17, FINSEQ_3:25; then A19: n <> (len q) + 1 by XREAL_1:29; ( n in dom (q ^ <*x*>) & (q ^ <*x*>) . n = (q ^ <*x*>) . ((len q) + 1) ) by A3, A17, A18, FINSEQ_1:def_7, FINSEQ_2:15; hence contradiction by A1, A5, A19, FUNCT_1:def_4; ::_thesis: verum end; then A20: y <> x by A15; s = p1 ^ <*x*> by A12, A14, A13, FINSEQ_1:42; then rng p = (rng (p1 ^ <*x*>)) \/ (rng p2) by A10, FINSEQ_1:31 .= ((rng p1) \/ (rng <*x*>)) \/ (rng p2) by FINSEQ_1:31 .= ((rng p1) \/ (rng p2)) \/ (rng <*x*>) by XBOOLE_1:4 .= (rng (p1 ^ p2)) \/ (rng <*x*>) by FINSEQ_1:31 .= (rng (p1 ^ p2)) \/ {x} by FINSEQ_1:38 ; then ( y in rng (p1 ^ p2) or y in {x} ) by A15, A4, XBOOLE_0:def_3; hence y in rng (p1 ^ p2) by A20, TARSKI:def_1; ::_thesis: verum end; begin theorem Th10: :: GRAPH_5:10 for p, q being FinSequence for G being Graph st p ^ q is Chain of G holds ( p is Chain of G & q is Chain of G ) proof let p, q be FinSequence; ::_thesis: for G being Graph st p ^ q is Chain of G holds ( p is Chain of G & q is Chain of G ) let G be Graph; ::_thesis: ( p ^ q is Chain of G implies ( p is Chain of G & q is Chain of G ) ) set r = p ^ q; set D = the carrier' of G; set V = the carrier of G; assume A1: p ^ q is Chain of G ; ::_thesis: ( p is Chain of G & q is Chain of G ) then consider f being FinSequence such that A2: len f = (len (p ^ q)) + 1 and A3: for n being Element of NAT st 1 <= n & n <= len f holds f . n in the carrier of G and A4: for n being Element of NAT st 1 <= n & n <= len (p ^ q) holds ex x, y being Element of the carrier of G st ( x = f . n & y = f . (n + 1) & (p ^ q) . n joins x,y ) by GRAPH_1:def_14; A5: len (p ^ q) = (len p) + (len q) by FINSEQ_1:22; then len f = (len p) + ((len q) + 1) by A2; then consider h1, h2 being FinSequence such that A6: len h1 = len p and A7: len h2 = (len q) + 1 and A8: f = h1 ^ h2 by FINSEQ_2:22; A9: now__::_thesis:_ex_h2_being_FinSequence_st_ (_len_h2_=_(len_q)_+_1_&_(_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_h2_holds_ h2_._n_in_the_carrier_of_G_)_&_(_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_q_holds_ ex_x,_y_being_Element_of_the_carrier_of_G_st_ (_x_=_h2_._n_&_h2_._(n_+_1)_=_y_&_q_._n_joins_x,y_)_)_) take h2 = h2; ::_thesis: ( len h2 = (len q) + 1 & ( for n being Element of NAT st 1 <= n & n <= len h2 holds h2 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len q holds ex x, y being Element of the carrier of G st ( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y ) ) ) thus len h2 = (len q) + 1 by A7; ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len h2 holds h2 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len q holds ex x, y being Element of the carrier of G st ( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y ) ) ) hereby ::_thesis: for n being Element of NAT st 1 <= n & n <= len q holds ex x, y being Element of the carrier of G st ( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y ) let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len h2 implies h2 . n in the carrier of G ) assume that A10: 1 <= n and A11: n <= len h2 ; ::_thesis: h2 . n in the carrier of G n <= (len h1) + n by NAT_1:11; then A12: 1 <= (len h1) + n by A10, XXREAL_0:2; (len h1) + n <= (len h1) + (len h2) by A11, XREAL_1:7; then A13: (len h1) + n <= len f by A8, FINSEQ_1:22; n in dom h2 by A10, A11, FINSEQ_3:25; then h2 . n = f . ((len h1) + n) by A8, FINSEQ_1:def_7; hence h2 . n in the carrier of G by A3, A13, A12; ::_thesis: verum end; hereby ::_thesis: verum let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len q implies ex x, y being Element of the carrier of G st ( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y ) ) assume that A14: 1 <= n and A15: n <= len q ; ::_thesis: ex x, y being Element of the carrier of G st ( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y ) set m = (len p) + n; n <= (len p) + n by NAT_1:11; then 1 <= (len p) + n by A14, XXREAL_0:2; then consider x, y being Element of the carrier of G such that A16: x = f . ((len p) + n) and A17: y = f . (((len p) + n) + 1) and A18: (p ^ q) . ((len p) + n) joins x,y by A4, A5, A15, XREAL_1:7; take x = x; ::_thesis: ex y being Element of the carrier of G st ( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y ) take y = y; ::_thesis: ( x = h2 . n & h2 . (n + 1) = y & q . n joins x,y ) len q <= len h2 by A7, NAT_1:11; then n <= len h2 by A15, XXREAL_0:2; hence x = h2 . n by A6, A8, A14, A16, Lm2; ::_thesis: ( h2 . (n + 1) = y & q . n joins x,y ) 1 <= n + 1 by NAT_1:11; hence h2 . (n + 1) = f . ((len h1) + (n + 1)) by A7, A8, A15, Lm2, XREAL_1:7 .= y by A6, A17 ; ::_thesis: q . n joins x,y thus q . n joins x,y by A14, A15, A18, Lm2; ::_thesis: verum end; end; A19: len f = ((len p) + 1) + (len q) by A2, A5; then consider f1, f2 being FinSequence such that A20: len f1 = (len p) + 1 and len f2 = len q and A21: f = f1 ^ f2 by FINSEQ_2:22; A22: now__::_thesis:_ex_f1_being_FinSequence_st_ (_len_f1_=_(len_p)_+_1_&_(_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_f1_holds_ f1_._n_in_the_carrier_of_G_)_&_(_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_p_holds_ ex_x,_y_being_Element_of_the_carrier_of_G_st_ (_x_=_f1_._n_&_y_=_f1_._(n_+_1)_&_p_._n_joins_x,y_)_)_) take f1 = f1; ::_thesis: ( len f1 = (len p) + 1 & ( for n being Element of NAT st 1 <= n & n <= len f1 holds f1 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len p holds ex x, y being Element of the carrier of G st ( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y ) ) ) thus len f1 = (len p) + 1 by A20; ::_thesis: ( ( for n being Element of NAT st 1 <= n & n <= len f1 holds f1 . n in the carrier of G ) & ( for n being Element of NAT st 1 <= n & n <= len p holds ex x, y being Element of the carrier of G st ( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y ) ) ) hereby ::_thesis: for n being Element of NAT st 1 <= n & n <= len p holds ex x, y being Element of the carrier of G st ( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y ) let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len f1 implies f1 . n in the carrier of G ) assume that A23: 1 <= n and A24: n <= len f1 ; ::_thesis: f1 . n in the carrier of G len f1 <= len f by A19, A20, NAT_1:11; then n <= len f by A24, XXREAL_0:2; then A25: f . n in the carrier of G by A3, A23; n in dom f1 by A23, A24, FINSEQ_3:25; hence f1 . n in the carrier of G by A21, A25, FINSEQ_1:def_7; ::_thesis: verum end; hereby ::_thesis: verum let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len p implies ex x, y being Element of the carrier of G st ( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y ) ) assume that A26: 1 <= n and A27: n <= len p ; ::_thesis: ex x, y being Element of the carrier of G st ( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y ) len p <= len (p ^ q) by A5, NAT_1:11; then n <= len (p ^ q) by A27, XXREAL_0:2; then consider x, y being Element of the carrier of G such that A28: x = f . n and A29: y = f . (n + 1) and A30: (p ^ q) . n joins x,y by A4, A26; take x = x; ::_thesis: ex y being Element of the carrier of G st ( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y ) take y = y; ::_thesis: ( x = f1 . n & y = f1 . (n + 1) & p . n joins x,y ) len p <= len f1 by A20, NAT_1:11; then n <= len f1 by A27, XXREAL_0:2; hence x = f1 . n by A21, A26, A28, Lm1; ::_thesis: ( y = f1 . (n + 1) & p . n joins x,y ) ( 1 <= n + 1 & n + 1 <= len f1 ) by A20, A27, NAT_1:11, XREAL_1:7; then n + 1 in dom f1 by FINSEQ_3:25; hence y = f1 . (n + 1) by A21, A29, FINSEQ_1:def_7; ::_thesis: p . n joins x,y thus p . n joins x,y by A26, A27, A30, Lm1; ::_thesis: verum end; end; A31: p is FinSequence of the carrier' of G by A1, FINSEQ_1:36; now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_p_holds_ p_._n_in_the_carrier'_of_G let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len p implies p . n in the carrier' of G ) assume ( 1 <= n & n <= len p ) ; ::_thesis: p . n in the carrier' of G then n in dom p by FINSEQ_3:25; hence p . n in the carrier' of G by A31, FINSEQ_2:11; ::_thesis: verum end; hence p is Chain of G by A22, GRAPH_1:def_14; ::_thesis: q is Chain of G A32: q is FinSequence of the carrier' of G by A1, FINSEQ_1:36; now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_q_holds_ q_._n_in_the_carrier'_of_G let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len q implies q . n in the carrier' of G ) assume ( 1 <= n & n <= len q ) ; ::_thesis: q . n in the carrier' of G then n in dom q by FINSEQ_3:25; hence q . n in the carrier' of G by A32, FINSEQ_2:11; ::_thesis: verum end; hence q is Chain of G by A9, GRAPH_1:def_14; ::_thesis: verum end; theorem Th11: :: GRAPH_5:11 for p, q being FinSequence for G being Graph st p ^ q is oriented Chain of G holds ( p is oriented Chain of G & q is oriented Chain of G ) proof let p, q be FinSequence; ::_thesis: for G being Graph st p ^ q is oriented Chain of G holds ( p is oriented Chain of G & q is oriented Chain of G ) let G be Graph; ::_thesis: ( p ^ q is oriented Chain of G implies ( p is oriented Chain of G & q is oriented Chain of G ) ) assume A1: p ^ q is oriented Chain of G ; ::_thesis: ( p is oriented Chain of G & q is oriented Chain of G ) set r = p ^ q; A2: len (p ^ q) = (len p) + (len q) by FINSEQ_1:22; A3: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<_len_q_holds_ the_Source_of_G_._(q_._(n_+_1))_=_the_Target_of_G_._(q_._n) let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len q implies the Source of G . (q . (n + 1)) = the Target of G . (q . n) ) assume that A4: 1 <= n and A5: n < len q ; ::_thesis: the Source of G . (q . (n + 1)) = the Target of G . (q . n) set m = (len p) + n; n <= (len p) + n by NAT_1:11; then A6: 1 <= (len p) + n by A4, XXREAL_0:2; n + 1 <= len q by A5, NAT_1:13; then A7: q . (n + 1) = (p ^ q) . ((len p) + (n + 1)) by Lm2, NAT_1:11 .= (p ^ q) . (((len p) + n) + 1) ; (len p) + n < len (p ^ q) by A2, A5, XREAL_1:8; then the Source of G . ((p ^ q) . (((len p) + n) + 1)) = the Target of G . ((p ^ q) . ((len p) + n)) by A1, A6, GRAPH_1:def_15; hence the Source of G . (q . (n + 1)) = the Target of G . (q . n) by A4, A5, A7, Lm2; ::_thesis: verum end; now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<_len_p_holds_ the_Source_of_G_._(p_._(n_+_1))_=_the_Target_of_G_._(p_._n) let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len p implies the Source of G . (p . (n + 1)) = the Target of G . (p . n) ) assume that A8: 1 <= n and A9: n < len p ; ::_thesis: the Source of G . (p . (n + 1)) = the Target of G . (p . n) n + 1 <= len p by A9, NAT_1:13; then A10: p . (n + 1) = (p ^ q) . (n + 1) by Lm1, NAT_1:11; len p <= len (p ^ q) by A2, NAT_1:11; then n < len (p ^ q) by A9, XXREAL_0:2; then the Source of G . ((p ^ q) . (n + 1)) = the Target of G . ((p ^ q) . n) by A1, A8, GRAPH_1:def_15; hence the Source of G . (p . (n + 1)) = the Target of G . (p . n) by A8, A9, A10, Lm1; ::_thesis: verum end; hence ( p is oriented Chain of G & q is oriented Chain of G ) by A1, A3, Th10, GRAPH_1:def_15; ::_thesis: verum end; theorem Th12: :: GRAPH_5:12 for G being Graph for p, q being oriented Chain of G st the Target of G . (p . (len p)) = the Source of G . (q . 1) holds p ^ q is oriented Chain of G proof let G be Graph; ::_thesis: for p, q being oriented Chain of G st the Target of G . (p . (len p)) = the Source of G . (q . 1) holds p ^ q is oriented Chain of G let p, q be oriented Chain of G; ::_thesis: ( the Target of G . (p . (len p)) = the Source of G . (q . 1) implies p ^ q is oriented Chain of G ) assume A1: the Target of G . (p . (len p)) = the Source of G . (q . 1) ; ::_thesis: p ^ q is oriented Chain of G percases ( p = {} or q = {} or ( not p = {} & not q = {} ) ) ; supposeA2: ( p = {} or q = {} ) ; ::_thesis: p ^ q is oriented Chain of G hereby ::_thesis: verum percases ( p = {} or q = {} ) by A2; suppose p = {} ; ::_thesis: p ^ q is oriented Chain of G hence p ^ q is oriented Chain of G by FINSEQ_1:34; ::_thesis: verum end; suppose q = {} ; ::_thesis: p ^ q is oriented Chain of G hence p ^ q is oriented Chain of G by FINSEQ_1:34; ::_thesis: verum end; end; end; end; supposeA3: ( not p = {} & not q = {} ) ; ::_thesis: p ^ q is oriented Chain of G consider vs2 being FinSequence of the carrier of G such that A4: vs2 is_oriented_vertex_seq_of q by GRAPH_4:9; len vs2 = (len q) + 1 by A4, GRAPH_4:def_5; then A5: len vs2 >= 1 by NAT_1:12; len q >= 1 by A3, FINSEQ_1:20; then q . 1 orientedly_joins vs2 /. 1,vs2 /. (1 + 1) by A4, GRAPH_4:def_5; then A6: the Source of G . (q . 1) = vs2 /. 1 by GRAPH_4:def_1 .= vs2 . 1 by A5, FINSEQ_4:15 ; consider vs1 being FinSequence of the carrier of G such that A7: vs1 is_oriented_vertex_seq_of p by GRAPH_4:9; A8: len vs1 = (len p) + 1 by A7, GRAPH_4:def_5; then A9: len vs1 >= 1 by NAT_1:12; len p >= 1 by A3, FINSEQ_1:20; then p . (len p) orientedly_joins vs1 /. (len p),vs1 /. ((len p) + 1) by A7, GRAPH_4:def_5; then the Target of G . (p . (len p)) = vs1 /. (len vs1) by A8, GRAPH_4:def_1 .= vs1 . (len vs1) by A9, FINSEQ_4:15 ; hence p ^ q is oriented Chain of G by A1, A7, A4, A6, GRAPH_4:14; ::_thesis: verum end; end; end; begin theorem Th13: :: GRAPH_5:13 for G being Graph holds {} is oriented Simple Chain of G proof let G be Graph; ::_thesis: {} is oriented Simple Chain of G set v = the Element of G; set vs = <* the Element of G*>; A1: now__::_thesis:_for_n,_m_being_Element_of_NAT_st_1_<=_n_&_n_<_m_&_m_<=_len_<*_the_Element_of_G*>_&_<*_the_Element_of_G*>_._n_=_<*_the_Element_of_G*>_._m_holds_ (_n_=_1_&_m_=_len_<*_the_Element_of_G*>_) let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len <* the Element of G*> & <* the Element of G*> . n = <* the Element of G*> . m implies ( n = 1 & m = len <* the Element of G*> ) ) assume that A2: ( 1 <= n & n < m & m <= len <* the Element of G*> ) and <* the Element of G*> . n = <* the Element of G*> . m ; ::_thesis: ( n = 1 & m = len <* the Element of G*> ) assume ( not n = 1 or not m = len <* the Element of G*> ) ; ::_thesis: contradiction len <* the Element of G*> = 1 by FINSEQ_1:39; hence contradiction by A2, XXREAL_0:2; ::_thesis: verum end; <* the Element of G*> is_oriented_vertex_seq_of {} by GRAPH_4:8; hence {} is oriented Simple Chain of G by A1, GRAPH_1:14, GRAPH_4:def_7; ::_thesis: verum end; theorem Th14: :: GRAPH_5:14 for p, q being FinSequence for G being Graph st p ^ q is oriented Simple Chain of G holds ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) proof let p, q be FinSequence; ::_thesis: for G being Graph st p ^ q is oriented Simple Chain of G holds ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) let G be Graph; ::_thesis: ( p ^ q is oriented Simple Chain of G implies ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) ) assume A1: p ^ q is oriented Simple Chain of G ; ::_thesis: ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) set r = p ^ q; percases ( p = {} or q = {} or ( not p = {} & not q = {} ) ) ; supposeA2: ( p = {} or q = {} ) ; ::_thesis: ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) hereby ::_thesis: verum percases ( p = {} or q = {} ) by A2; suppose p = {} ; ::_thesis: ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) hence ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) by A1, Th13, FINSEQ_1:34; ::_thesis: verum end; suppose q = {} ; ::_thesis: ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) hence ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) by A1, Th13, FINSEQ_1:34; ::_thesis: verum end; end; end; end; supposeA3: ( not p = {} & not q = {} ) ; ::_thesis: ( p is oriented Simple Chain of G & q is oriented Simple Chain of G ) consider vs being FinSequence of the carrier of G such that A4: vs is_oriented_vertex_seq_of p ^ q and A5: 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 ) by A1, GRAPH_4:def_7; A6: len vs = (len (p ^ q)) + 1 by A4, GRAPH_4:def_5; A7: len (p ^ q) = (len p) + (len q) by FINSEQ_1:22; then A8: len vs = ((len p) + 1) + (len q) by A6; then consider f1, f2 being FinSequence such that A9: len f1 = (len p) + 1 and len f2 = len q and A10: vs = f1 ^ f2 by FINSEQ_2:22; A11: len vs = (len p) + ((len q) + 1) by A6, A7; then consider h1, h2 being FinSequence such that A12: len h1 = len p and A13: len h2 = (len q) + 1 and A14: vs = h1 ^ h2 by FINSEQ_2:22; reconsider f1 = f1 as FinSequence of the carrier of G by A10, FINSEQ_1:36; A15: now__::_thesis:_for_n,_m_being_Element_of_NAT_st_1_<=_n_&_n_<_m_&_m_<=_len_f1_&_f1_._n_=_f1_._m_holds_ (_n_=_1_&_m_=_len_f1_) let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len f1 & f1 . n = f1 . m implies ( n = 1 & m = len f1 ) ) assume that A16: 1 <= n and A17: n < m and A18: m <= len f1 and A19: f1 . n = f1 . m ; ::_thesis: ( n = 1 & m = len f1 ) n <= len f1 by A17, A18, XXREAL_0:2; then A20: f1 . n = vs . n by A10, A16, Lm1; 1 <= m by A16, A17, XXREAL_0:2; then A21: f1 . m = vs . m by A10, A18, Lm1; assume ( not n = 1 or not m = len f1 ) ; ::_thesis: contradiction (len f1) + 0 < len vs by A3, A8, A9, XREAL_1:8; then m < len vs by A18, XXREAL_0:2; hence contradiction by A5, A16, A17, A19, A20, A21; ::_thesis: verum end; reconsider h2 = h2 as FinSequence of the carrier of G by A14, FINSEQ_1:36; now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_q_holds_ q_._n_orientedly_joins_h2_/._n,h2_/._(n_+_1) let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len q implies q . n orientedly_joins h2 /. n,h2 /. (n + 1) ) assume that A22: 1 <= n and A23: n <= len q ; ::_thesis: q . n orientedly_joins h2 /. n,h2 /. (n + 1) set m = (len p) + n; A24: (len p) + n <= len (p ^ q) by A7, A23, XREAL_1:7; then ( 1 <= ((len p) + n) + 1 & ((len p) + n) + 1 <= len vs ) by A6, NAT_1:11, XREAL_1:7; then A25: ((len p) + n) + 1 in dom vs by FINSEQ_3:25; A26: 1 <= n + 1 by NAT_1:11; n + 1 <= len h2 by A13, A23, XREAL_1:7; then n + 1 in dom h2 by A26, FINSEQ_3:25; then A27: h2 /. (n + 1) = h2 . (n + 1) by PARTFUN1:def_6 .= vs . ((len h1) + (n + 1)) by A13, A14, A23, A26, Lm2, XREAL_1:7 .= vs /. (((len p) + n) + 1) by A12, A25, PARTFUN1:def_6 ; n <= (len p) + n by NAT_1:11; then A28: 1 <= (len p) + n by A22, XXREAL_0:2; len (p ^ q) <= len vs by A6, NAT_1:11; then (len p) + n <= len vs by A24, XXREAL_0:2; then A29: (len p) + n in dom vs by A28, FINSEQ_3:25; A30: n + 0 <= len h2 by A13, A23, XREAL_1:7; then n in dom h2 by A22, FINSEQ_3:25; then A31: h2 /. n = h2 . n by PARTFUN1:def_6 .= vs . ((len p) + n) by A12, A14, A22, A30, Lm2 .= vs /. ((len p) + n) by A29, PARTFUN1:def_6 ; (p ^ q) . ((len p) + n) orientedly_joins vs /. ((len p) + n),vs /. (((len p) + n) + 1) by A4, A24, A28, GRAPH_4:def_5; hence q . n orientedly_joins h2 /. n,h2 /. (n + 1) by A22, A23, A31, A27, Lm2; ::_thesis: verum end; then A32: h2 is_oriented_vertex_seq_of q by A13, GRAPH_4:def_5; now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_p_holds_ p_._n_orientedly_joins_f1_/._n,f1_/._(n_+_1) let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len p implies p . n orientedly_joins f1 /. n,f1 /. (n + 1) ) assume that A33: 1 <= n and A34: n <= len p ; ::_thesis: p . n orientedly_joins f1 /. n,f1 /. (n + 1) A35: 1 <= n + 1 by NAT_1:11; len p <= len (p ^ q) by A7, NAT_1:11; then A36: n <= len (p ^ q) by A34, XXREAL_0:2; then n + 1 <= len vs by A6, XREAL_1:7; then A37: n + 1 in dom vs by A35, FINSEQ_3:25; len p <= len vs by A11, NAT_1:11; then n <= len vs by A34, XXREAL_0:2; then A38: n in dom vs by A33, FINSEQ_3:25; A39: n + 0 <= len f1 by A9, A34, XREAL_1:7; then n in dom f1 by A33, FINSEQ_3:25; then A40: f1 /. n = f1 . n by PARTFUN1:def_6 .= vs . n by A10, A33, A39, Lm1 .= vs /. n by A38, PARTFUN1:def_6 ; n + 1 <= len f1 by A9, A34, XREAL_1:7; then n + 1 in dom f1 by A35, FINSEQ_3:25; then A41: f1 /. (n + 1) = f1 . (n + 1) by PARTFUN1:def_6 .= vs . (n + 1) by A9, A10, A34, A35, Lm1, XREAL_1:7 .= vs /. (n + 1) by A37, PARTFUN1:def_6 ; (p ^ q) . n orientedly_joins vs /. n,vs /. (n + 1) by A4, A33, A36, GRAPH_4:def_5; hence p . n orientedly_joins f1 /. n,f1 /. (n + 1) by A33, A34, A40, A41, Lm1; ::_thesis: verum end; then f1 is_oriented_vertex_seq_of p by A9, GRAPH_4:def_5; hence p is oriented Simple Chain of G by A1, A15, Th11, GRAPH_4:def_7; ::_thesis: q is oriented Simple Chain of G now__::_thesis:_for_n,_m_being_Element_of_NAT_st_1_<=_n_&_n_<_m_&_m_<=_len_h2_&_h2_._n_=_h2_._m_holds_ (_n_=_1_&_m_=_len_h2_) let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len h2 & h2 . n = h2 . m implies ( n = 1 & m = len h2 ) ) assume that A42: 1 <= n and A43: n < m and A44: m <= len h2 and A45: h2 . n = h2 . m ; ::_thesis: ( n = 1 & m = len h2 ) n <= len h2 by A43, A44, XXREAL_0:2; then A46: h2 . n = vs . ((len h1) + n) by A14, A42, Lm2; assume ( not n = 1 or not m = len h2 ) ; ::_thesis: contradiction A47: (len h1) + m <= len vs by A11, A12, A13, A44, XREAL_1:7; 1 <= m by A42, A43, XXREAL_0:2; then A48: h2 . m = vs . ((len h1) + m) by A14, A44, Lm2; ( 0 + 1 < (len h1) + n & (len h1) + n < (len h1) + m ) by A3, A12, A42, A43, XREAL_1:8; hence contradiction by A5, A45, A46, A48, A47; ::_thesis: verum end; hence q is oriented Simple Chain of G by A1, A32, Th11, GRAPH_4:def_7; ::_thesis: verum end; end; end; theorem Th15: :: GRAPH_5:15 for G being Graph for pe being FinSequence of the carrier' of G st len pe = 1 holds pe is oriented Simple Chain of G proof let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G st len pe = 1 holds pe is oriented Simple Chain of G let pe be FinSequence of the carrier' of G; ::_thesis: ( len pe = 1 implies pe is oriented Simple Chain of G ) set p = pe; set v1 = the Source of G . (pe . 1); set v2 = the Target of G . (pe . 1); A1: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_pe_holds_ pe_._n_in_the_carrier'_of_G let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len pe implies pe . n in the carrier' of G ) assume ( 1 <= n & n <= len pe ) ; ::_thesis: pe . n in the carrier' of G then n in dom pe by FINSEQ_3:25; hence pe . n in the carrier' of G by FINSEQ_2:11; ::_thesis: verum end; assume A2: len pe = 1 ; ::_thesis: pe is oriented Simple Chain of G then 1 in dom pe by FINSEQ_3:25; then reconsider v1 = the Source of G . (pe . 1), v2 = the Target of G . (pe . 1) as Element of G by FINSEQ_2:11, FUNCT_2:5; set vs = <*v1,v2*>; A3: len <*v1,v2*> = (len pe) + 1 by A2, FINSEQ_1:44; A4: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_pe_holds_ ex_v1,_v2_being_Element_of_G_st_ (_v1_=_<*v1,v2*>_._n_&_v2_=_<*v1,v2*>_._(n_+_1)_&_pe_._n_joins_v1,v2_) let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len pe implies ex v1, v2 being Element of G st ( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 ) ) assume ( 1 <= n & n <= len pe ) ; ::_thesis: ex v1, v2 being Element of G st ( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 ) then A5: n = 1 by A2, XXREAL_0:1; take v1 = v1; ::_thesis: ex v2 being Element of G st ( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 ) take v2 = v2; ::_thesis: ( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) & pe . n joins v1,v2 ) thus ( v1 = <*v1,v2*> . n & v2 = <*v1,v2*> . (n + 1) ) by A5, FINSEQ_1:44; ::_thesis: pe . n joins v1,v2 thus pe . n joins v1,v2 by A5, GRAPH_1:def_12; ::_thesis: verum end; A6: len <*v1,v2*> = 2 by FINSEQ_1:44; A7: now__::_thesis:_for_n,_m_being_Element_of_NAT_st_1_<=_n_&_n_<_m_&_m_<=_len_<*v1,v2*>_&_<*v1,v2*>_._n_=_<*v1,v2*>_._m_holds_ (_n_=_1_&_m_=_len_<*v1,v2*>_) let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len <*v1,v2*> & <*v1,v2*> . n = <*v1,v2*> . m implies ( n = 1 & m = len <*v1,v2*> ) ) assume that A8: 1 <= n and A9: n < m and A10: m <= len <*v1,v2*> and <*v1,v2*> . n = <*v1,v2*> . m ; ::_thesis: ( n = 1 & m = len <*v1,v2*> ) n < 1 + 1 by A6, A9, A10, XXREAL_0:2; then n <= 1 by NAT_1:13; hence n = 1 by A8, XXREAL_0:1; ::_thesis: m = len <*v1,v2*> 1 < m by A8, A9, XXREAL_0:2; then 1 + 1 < m + 1 by XREAL_1:8; then 2 <= m by NAT_1:13; hence m = len <*v1,v2*> by A6, A10, XXREAL_0:1; ::_thesis: verum end; A11: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_<*v1,v2*>_holds_ <*v1,v2*>_._n_in_the_carrier_of_G let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len <*v1,v2*> implies <*v1,v2*> . b1 in the carrier of G ) assume that A12: 1 <= n and A13: n <= len <*v1,v2*> ; ::_thesis: <*v1,v2*> . b1 in the carrier of G percases ( n < 1 + 1 or n >= 2 ) ; suppose n < 1 + 1 ; ::_thesis: <*v1,v2*> . b1 in the carrier of G then n <= 1 by NAT_1:13; then n = 1 by A12, XXREAL_0:1; then <*v1,v2*> . n = v1 by FINSEQ_1:44; hence <*v1,v2*> . n in the carrier of G ; ::_thesis: verum end; suppose n >= 2 ; ::_thesis: <*v1,v2*> . b1 in the carrier of G then n = 2 by A6, A13, XXREAL_0:1; then <*v1,v2*> . n = v2 by FINSEQ_1:44; hence <*v1,v2*> . n in the carrier of G ; ::_thesis: verum end; end; end; A14: for n being Element of NAT st 1 <= n & n < len pe holds not the Source of G . (pe . (n + 1)) <> the Target of G . (pe . n) by A2; now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_pe_holds_ pe_._n_orientedly_joins_<*v1,v2*>_/._n,<*v1,v2*>_/._(n_+_1) let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len pe implies pe . n orientedly_joins <*v1,v2*> /. n,<*v1,v2*> /. (n + 1) ) assume ( 1 <= n & n <= len pe ) ; ::_thesis: pe . n orientedly_joins <*v1,v2*> /. n,<*v1,v2*> /. (n + 1) then A15: n = 1 by A2, XXREAL_0:1; ( <*v1,v2*> /. 1 = v1 & <*v1,v2*> /. (1 + 1) = v2 ) by FINSEQ_4:17; hence pe . n orientedly_joins <*v1,v2*> /. n,<*v1,v2*> /. (n + 1) by A15, GRAPH_4:def_1; ::_thesis: verum end; then <*v1,v2*> is_oriented_vertex_seq_of pe by A3, GRAPH_4:def_5; hence pe is oriented Simple Chain of G by A3, A7, A1, A11, A4, A14, GRAPH_1:def_14, GRAPH_1:def_15, GRAPH_4:def_7; ::_thesis: verum end; theorem Th16: :: GRAPH_5:16 for G being Graph for p being oriented Simple Chain of G for q being FinSequence of the carrier' of G st len p >= 1 & len q = 1 & the Source of G . (q . 1) = the Target of G . (p . (len p)) & the Source of G . (p . 1) <> the Target of G . (p . (len p)) & ( for k being Element of NAT holds ( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ) holds p ^ q is oriented Simple Chain of G proof let G be Graph; ::_thesis: for p being oriented Simple Chain of G for q being FinSequence of the carrier' of G st len p >= 1 & len q = 1 & the Source of G . (q . 1) = the Target of G . (p . (len p)) & the Source of G . (p . 1) <> the Target of G . (p . (len p)) & ( for k being Element of NAT holds ( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ) holds p ^ q is oriented Simple Chain of G let p be oriented Simple Chain of G; ::_thesis: for q being FinSequence of the carrier' of G st len p >= 1 & len q = 1 & the Source of G . (q . 1) = the Target of G . (p . (len p)) & the Source of G . (p . 1) <> the Target of G . (p . (len p)) & ( for k being Element of NAT holds ( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ) holds p ^ q is oriented Simple Chain of G let q be FinSequence of the carrier' of G; ::_thesis: ( len p >= 1 & len q = 1 & the Source of G . (q . 1) = the Target of G . (p . (len p)) & the Source of G . (p . 1) <> the Target of G . (p . (len p)) & ( for k being Element of NAT holds ( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ) implies p ^ q is oriented Simple Chain of G ) set FS = the Source of G; set FT = the Target of G; set v1 = the Source of G . (q . 1); set v2 = the Target of G . (q . 1); set vp = the Target of G . (p . (len p)); set E = the carrier' of G; set V = the carrier of G; assume that A1: len p >= 1 and A2: len q = 1 and A3: the Source of G . (q . 1) = the Target of G . (p . (len p)) and A4: the Source of G . (p . 1) <> the Target of G . (p . (len p)) and A5: for k being Element of NAT holds ( not 1 <= k or not k <= len p or not the Target of G . (p . k) = the Target of G . (q . 1) ) ; ::_thesis: p ^ q is oriented Simple Chain of G set lp = len p; 1 in dom q by A2, FINSEQ_3:25; then reconsider v1 = the Source of G . (q . 1), v2 = the Target of G . (q . 1) as Element of the carrier of G by FINSEQ_2:11, FUNCT_2:5; consider r being FinSequence of the carrier of G such that A6: r is_oriented_vertex_seq_of p and A7: for n, m being Element of NAT st 1 <= n & n < m & m <= len r & r . n = r . m holds ( n = 1 & m = len r ) by GRAPH_4:def_7; set pq = p ^ q; set rv = r ^ <*v2*>; A8: len r = (len p) + 1 by A6, GRAPH_4:def_5; A9: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_p_holds_ p_._n_joins_r_/._n,r_/._(n_+_1) let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len p implies p . n joins r /. n,r /. (n + 1) ) assume ( 1 <= n & n <= len p ) ; ::_thesis: p . n joins r /. n,r /. (n + 1) then p . n orientedly_joins r /. n,r /. (n + 1) by A6, GRAPH_4:def_5; hence p . n joins r /. n,r /. (n + 1) by GRAPH_4:1; ::_thesis: verum end; A10: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_(p_^_q)_holds_ ex_v1,_v2_being_Element_of_the_carrier_of_G_st_ (_v1_=_(r_^_<*v2*>)_._n_&_v2_=_(r_^_<*v2*>)_._(n_+_1)_&_(p_^_q)_._n_joins_v1,v2_) let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len (p ^ q) implies ex v1, v2 being Element of the carrier of G st ( v2 = (r ^ <*v2*>) . v1 & b3 = (r ^ <*v2*>) . (v1 + 1) & (p ^ q) . v1 joins v2,b3 ) ) assume that A11: 1 <= n and A12: n <= len (p ^ q) ; ::_thesis: ex v1, v2 being Element of the carrier of G st ( v2 = (r ^ <*v2*>) . v1 & b3 = (r ^ <*v2*>) . (v1 + 1) & (p ^ q) . v1 joins v2,b3 ) percases ( n = len (p ^ q) or n <> len (p ^ q) ) ; supposeA13: n = len (p ^ q) ; ::_thesis: ex v1, v2 being Element of the carrier of G st ( v2 = (r ^ <*v2*>) . v1 & b3 = (r ^ <*v2*>) . (v1 + 1) & (p ^ q) . v1 joins v2,b3 ) set m = len p; take v1 = v1; ::_thesis: ex v2 being Element of the carrier of G st ( v1 = (r ^ <*v2*>) . n & v2 = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins v1,v2 ) take v2 = v2; ::_thesis: ( v1 = (r ^ <*v2*>) . n & v2 = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins v1,v2 ) p . (len p) orientedly_joins r /. (len p),r /. ((len p) + 1) by A1, A6, GRAPH_4:def_5; then A14: the Target of G . (p . (len p)) = r /. ((len p) + 1) by GRAPH_4:def_1; A15: n = len r by A2, A8, A13, FINSEQ_1:22; then n in dom r by A11, FINSEQ_3:25; hence v1 = r . n by A3, A8, A15, A14, PARTFUN1:def_6 .= (r ^ <*v2*>) . n by A11, A15, Lm1 ; ::_thesis: ( v2 = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins v1,v2 ) thus v2 = (r ^ <*v2*>) . (n + 1) by A15, FINSEQ_1:42; ::_thesis: (p ^ q) . n joins v1,v2 q . 1 joins v1,v2 by GRAPH_1:def_12; hence (p ^ q) . n joins v1,v2 by A2, A8, A15, Lm2; ::_thesis: verum end; supposeA16: n <> len (p ^ q) ; ::_thesis: ex x, y being Element of the carrier of G st ( y = (r ^ <*v2*>) . x & b3 = (r ^ <*v2*>) . (x + 1) & (p ^ q) . x joins y,b3 ) take x = r /. n; ::_thesis: ex y being Element of the carrier of G st ( x = (r ^ <*v2*>) . n & y = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins x,y ) take y = r /. (n + 1); ::_thesis: ( x = (r ^ <*v2*>) . n & y = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins x,y ) n < len (p ^ q) by A12, A16, XXREAL_0:1; then A17: n < (len p) + 1 by A2, FINSEQ_1:22; then A18: n + 1 <= len r by A8, NAT_1:13; n in dom r by A8, A11, A17, FINSEQ_3:25; hence x = r . n by PARTFUN1:def_6 .= (r ^ <*v2*>) . n by A8, A11, A17, Lm1 ; ::_thesis: ( y = (r ^ <*v2*>) . (n + 1) & (p ^ q) . n joins x,y ) 1 <= n + 1 by NAT_1:12; then n + 1 in dom r by A18, FINSEQ_3:25; hence y = r . (n + 1) by PARTFUN1:def_6 .= (r ^ <*v2*>) . (n + 1) by A18, Lm1, NAT_1:12 ; ::_thesis: (p ^ q) . n joins x,y A19: n <= len p by A17, NAT_1:13; then p . n joins r /. n,r /. (n + 1) by A9, A11; hence (p ^ q) . n joins x,y by A11, A19, Lm1; ::_thesis: verum end; end; end; A20: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_(p_^_q)_holds_ (p_^_q)_._n_in_the_carrier'_of_G let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len (p ^ q) implies (p ^ q) . n in the carrier' of G ) assume ( 1 <= n & n <= len (p ^ q) ) ; ::_thesis: (p ^ q) . n in the carrier' of G then n in dom (p ^ q) by FINSEQ_3:25; then (p ^ q) . n in rng (p ^ q) by FUNCT_1:def_3; then A21: (p ^ q) . n in (rng p) \/ (rng q) by FINSEQ_1:31; ( rng p c= the carrier' of G & rng q c= the carrier' of G ) by FINSEQ_1:def_4; then (rng p) \/ (rng q) c= the carrier' of G by XBOOLE_1:8; hence (p ^ q) . n in the carrier' of G by A21; ::_thesis: verum end; A22: len (r ^ <*v2*>) = (len r) + 1 by FINSEQ_2:16; then A23: len (r ^ <*v2*>) = (len (p ^ q)) + 1 by A2, A8, FINSEQ_1:22; p . (len p) orientedly_joins r /. (len p),r /. ((len p) + 1) by A1, A6, GRAPH_4:def_5; then A24: the Target of G . (p . (len p)) = r /. ((len p) + 1) by GRAPH_4:def_1; A25: now__::_thesis:_for_n,_m_being_Element_of_NAT_st_1_<=_n_&_n_<_m_&_m_<=_len_(r_^_<*v2*>)_&_(r_^_<*v2*>)_._n_=_(r_^_<*v2*>)_._m_holds_ (_n_=_1_&_m_=_len_(r_^_<*v2*>)_) let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len (r ^ <*v2*>) & (r ^ <*v2*>) . n = (r ^ <*v2*>) . m implies ( n = 1 & m = len (r ^ <*v2*>) ) ) assume that A26: 1 <= n and A27: n < m and A28: m <= len (r ^ <*v2*>) and A29: (r ^ <*v2*>) . n = (r ^ <*v2*>) . m ; ::_thesis: ( n = 1 & m = len (r ^ <*v2*>) ) assume A30: ( not n = 1 or not m = len (r ^ <*v2*>) ) ; ::_thesis: contradiction percases ( m < len (r ^ <*v2*>) or m >= len (r ^ <*v2*>) ) ; suppose m < len (r ^ <*v2*>) ; ::_thesis: contradiction then A31: m <= len r by A22, NAT_1:13; A32: 1 <= m by A26, A27, XXREAL_0:2; then A33: m in dom r by A31, FINSEQ_3:25; n < len r by A27, A31, XXREAL_0:2; then A34: r . n = (r ^ <*v2*>) . n by A26, Lm1 .= r . m by A29, A31, A32, Lm1 ; then A35: m = len r by A7, A26, A27, A31; A36: n = 1 by A7, A26, A27, A31, A34; then A37: 1 in dom r by A27, A35, FINSEQ_3:25; p . 1 orientedly_joins r /. 1,r /. (1 + 1) by A1, A6, GRAPH_4:def_5; then the Source of G . (p . 1) = r /. 1 by GRAPH_4:def_1 .= r . m by A34, A36, A37, PARTFUN1:def_6 .= the Target of G . (p . (len p)) by A8, A24, A35, A33, PARTFUN1:def_6 ; hence contradiction by A4; ::_thesis: verum end; supposeA38: m >= len (r ^ <*v2*>) ; ::_thesis: contradiction then m = len (r ^ <*v2*>) by A28, XXREAL_0:1; then A39: v2 = (r ^ <*v2*>) . m by A22, FINSEQ_1:42; consider k being Nat such that A40: n = k + 1 by A26, NAT_1:6; reconsider k = k as Element of NAT by ORDINAL1:def_12; 1 < n by A26, A28, A30, A38, XXREAL_0:1; then A41: 1 <= k by A40, NAT_1:13; k + 1 < (len r) + 1 by A22, A27, A28, A40, XXREAL_0:2; then A42: k + 1 <= len r by NAT_1:13; then A43: k + 1 in dom r by A26, A40, FINSEQ_3:25; A44: k <= len p by A8, A42, XREAL_1:6; then p . k orientedly_joins r /. k,r /. (k + 1) by A6, A41, GRAPH_4:def_5; then the Target of G . (p . k) = r /. (k + 1) by GRAPH_4:def_1 .= r . (k + 1) by A43, PARTFUN1:def_6 .= v2 by A26, A29, A39, A40, A42, Lm1 ; hence contradiction by A5, A41, A44; ::_thesis: verum end; end; end; A45: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<_len_(p_^_q)_holds_ the_Source_of_G_._((p_^_q)_._(n_+_1))_=_the_Target_of_G_._((p_^_q)_._n) let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len (p ^ q) implies the Source of G . ((p ^ q) . (b1 + 1)) = the Target of G . ((p ^ q) . b1) ) assume that A46: 1 <= n and A47: n < len (p ^ q) ; ::_thesis: the Source of G . ((p ^ q) . (b1 + 1)) = the Target of G . ((p ^ q) . b1) percases ( n < len p or n >= len p ) ; supposeA48: n < len p ; ::_thesis: the Source of G . ((p ^ q) . (b1 + 1)) = the Target of G . ((p ^ q) . b1) then A49: n + 1 <= len p by NAT_1:13; ( the Source of G . (p . (n + 1)) = the Target of G . (p . n) & p . n = (p ^ q) . n ) by A46, A48, Lm1, GRAPH_1:def_15; hence the Source of G . ((p ^ q) . (n + 1)) = the Target of G . ((p ^ q) . n) by A49, Lm1, NAT_1:12; ::_thesis: verum end; supposeA50: n >= len p ; ::_thesis: the Source of G . ((p ^ q) . (b1 + 1)) = the Target of G . ((p ^ q) . b1) n < (len p) + 1 by A2, A47, FINSEQ_1:22; then n <= len p by NAT_1:13; then A51: n = len p by A50, XXREAL_0:1; then (p ^ q) . n = p . (len p) by A1, Lm1; hence the Source of G . ((p ^ q) . (n + 1)) = the Target of G . ((p ^ q) . n) by A2, A3, A51, Lm2; ::_thesis: verum end; end; end; A52: now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_(r_^_<*v2*>)_holds_ (r_^_<*v2*>)_._n_in_the_carrier_of_G let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len (r ^ <*v2*>) implies (r ^ <*v2*>) . b1 in the carrier of G ) assume that A53: 1 <= n and A54: n <= len (r ^ <*v2*>) ; ::_thesis: (r ^ <*v2*>) . b1 in the carrier of G percases ( n = len (r ^ <*v2*>) or n <> len (r ^ <*v2*>) ) ; suppose n = len (r ^ <*v2*>) ; ::_thesis: (r ^ <*v2*>) . b1 in the carrier of G then (r ^ <*v2*>) . n = v2 by A22, FINSEQ_1:42; hence (r ^ <*v2*>) . n in the carrier of G ; ::_thesis: verum end; suppose n <> len (r ^ <*v2*>) ; ::_thesis: (r ^ <*v2*>) . b1 in the carrier of G then n < len (r ^ <*v2*>) by A54, XXREAL_0:1; then A55: n <= len r by A22, NAT_1:13; then n in dom r by A53, FINSEQ_3:25; then r . n in the carrier of G by FINSEQ_2:11; hence (r ^ <*v2*>) . n in the carrier of G by A53, A55, Lm1; ::_thesis: verum end; end; end; now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_(p_^_q)_holds_ (p_^_q)_._n_orientedly_joins_(r_^_<*v2*>)_/._n,(r_^_<*v2*>)_/._(n_+_1) A56: dom r c= dom (r ^ <*v2*>) by FINSEQ_1:26; let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len (p ^ q) implies (p ^ q) . b1 orientedly_joins (r ^ <*v2*>) /. b1,(r ^ <*v2*>) /. (b1 + 1) ) assume that A57: 1 <= n and A58: n <= len (p ^ q) ; ::_thesis: (p ^ q) . b1 orientedly_joins (r ^ <*v2*>) /. b1,(r ^ <*v2*>) /. (b1 + 1) percases ( n <= len p or n > len p ) ; supposeA59: n <= len p ; ::_thesis: (p ^ q) . b1 orientedly_joins (r ^ <*v2*>) /. b1,(r ^ <*v2*>) /. (b1 + 1) then A60: n + 1 <= len r by A8, XREAL_1:7; 1 <= n + 1 by NAT_1:12; then A61: n + 1 in dom r by A60, FINSEQ_3:25; then A62: r /. (n + 1) = r . (n + 1) by PARTFUN1:def_6 .= (r ^ <*v2*>) . (n + 1) by A60, Lm1, NAT_1:12 .= (r ^ <*v2*>) /. (n + 1) by A56, A61, PARTFUN1:def_6 ; A63: p . n orientedly_joins r /. n,r /. (n + 1) by A6, A57, A59, GRAPH_4:def_5; A64: n <= len r by A8, A59, NAT_1:12; then A65: n in dom r by A57, FINSEQ_3:25; then r /. n = r . n by PARTFUN1:def_6 .= (r ^ <*v2*>) . n by A57, A64, Lm1 .= (r ^ <*v2*>) /. n by A56, A65, PARTFUN1:def_6 ; hence (p ^ q) . n orientedly_joins (r ^ <*v2*>) /. n,(r ^ <*v2*>) /. (n + 1) by A57, A59, A63, A62, Lm1; ::_thesis: verum end; supposeA66: n > len p ; ::_thesis: (p ^ q) . b1 orientedly_joins (r ^ <*v2*>) /. b1,(r ^ <*v2*>) /. (b1 + 1) A67: (len p) + 1 >= n by A2, A58, FINSEQ_1:22; (len p) + 1 <= n by A66, NAT_1:13; then A68: n = len r by A8, A67, XXREAL_0:1; 1 <= n + 1 by NAT_1:12; then A69: n + 1 in dom (r ^ <*v2*>) by A22, A68, FINSEQ_3:25; A70: v2 = (r ^ <*v2*>) . (n + 1) by A68, FINSEQ_1:42 .= (r ^ <*v2*>) /. (n + 1) by A69, PARTFUN1:def_6 ; A71: q . 1 orientedly_joins v1,v2 by GRAPH_4:def_1; A72: n in dom r by A8, A57, A67, FINSEQ_3:25; then v1 = r . n by A3, A8, A24, A68, PARTFUN1:def_6 .= (r ^ <*v2*>) . n by A8, A57, A67, Lm1 .= (r ^ <*v2*>) /. n by A56, A72, PARTFUN1:def_6 ; hence (p ^ q) . n orientedly_joins (r ^ <*v2*>) /. n,(r ^ <*v2*>) /. (n + 1) by A2, A8, A68, A70, A71, Lm2; ::_thesis: verum end; end; end; then r ^ <*v2*> is_oriented_vertex_seq_of p ^ q by A23, GRAPH_4:def_5; hence p ^ q is oriented Simple Chain of G by A20, A23, A52, A10, A45, A25, GRAPH_1:def_14, GRAPH_1:def_15, GRAPH_4:def_7; ::_thesis: verum end; theorem Th17: :: GRAPH_5:17 for G being Graph for p being oriented Simple Chain of G holds p is V14() proof let G be Graph; ::_thesis: for p being oriented Simple Chain of G holds p is V14() let p be oriented Simple Chain of G; ::_thesis: p is V14() set VV = the carrier of G; consider vs being FinSequence of the carrier of G such that A1: vs is_oriented_vertex_seq_of p and A2: 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 ) by GRAPH_4:def_7; A3: len vs = (len p) + 1 by A1, GRAPH_4:def_5; now__::_thesis:_for_n,_m_being_Element_of_NAT_st_1_<=_n_&_n_<_m_&_m_<=_len_p_holds_ not_p_._n_=_p_._m let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len p implies not p . n = p . m ) assume that A4: 1 <= n and A5: n < m and A6: m <= len p ; ::_thesis: not p . n = p . m A7: 1 <= m by A4, A5, XXREAL_0:2; then A8: p . m orientedly_joins vs /. m,vs /. (m + 1) by A1, A6, GRAPH_4:def_5; assume A9: p . n = p . m ; ::_thesis: contradiction A10: n <= len p by A5, A6, XXREAL_0:2; then p . n orientedly_joins vs /. n,vs /. (n + 1) by A1, A4, GRAPH_4:def_5; then A11: vs /. n = the Source of G . (p . m) by A9, GRAPH_4:def_1 .= vs /. m by A8, GRAPH_4:def_1 ; A12: len p < len vs by A3, XREAL_1:29; then n <= len vs by A10, XXREAL_0:2; then n in dom vs by A4, FINSEQ_3:25; then A13: vs . n = vs /. n by PARTFUN1:def_6; A14: m <= len vs by A6, A12, XXREAL_0:2; then m in dom vs by A7, FINSEQ_3:25; then vs . m = vs . n by A11, A13, PARTFUN1:def_6; then m = len vs by A2, A4, A5, A14; hence contradiction by A3, A6, XREAL_1:29; ::_thesis: verum end; hence p is V14() by Th6; ::_thesis: verum end; begin definition let G be Graph; let e be Element of the carrier' of G; func vertices e -> set equals :: GRAPH_5:def 1 {( the Source of G . e),( the Target of G . e)}; coherence {( the Source of G . e),( the Target of G . e)} is set ; end; :: deftheorem defines vertices GRAPH_5:def_1_:_ for G being Graph for e being Element of the carrier' of G holds vertices e = {( the Source of G . e),( the Target of G . e)}; definition let G be Graph; let pe be FinSequence of the carrier' of G; func vertices pe -> Subset of the carrier of G equals :: GRAPH_5:def 2 { v where v is Vertex of G : ex i being Element of NAT st ( i in dom pe & v in vertices (pe /. i) ) } ; coherence { v where v is Vertex of G : ex i being Element of NAT st ( i in dom pe & v in vertices (pe /. i) ) } is Subset of the carrier of G proof set VT = { v where v is Vertex of G : ex i being Element of NAT st ( i in dom pe & v in vertices (pe /. i) ) } ; { v where v is Vertex of G : ex i being Element of NAT st ( i in dom pe & v in vertices (pe /. i) ) } c= the carrier of G proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { v where v is Vertex of G : ex i being Element of NAT st ( i in dom pe & v in vertices (pe /. i) ) } or x in the carrier of G ) assume x in { v where v is Vertex of G : ex i being Element of NAT st ( i in dom pe & v in vertices (pe /. i) ) } ; ::_thesis: x in the carrier of G then ex v being Vertex of G st ( x = v & ex i being Element of NAT st ( i in dom pe & v in vertices (pe /. i) ) ) ; hence x in the carrier of G ; ::_thesis: verum end; hence { v where v is Vertex of G : ex i being Element of NAT st ( i in dom pe & v in vertices (pe /. i) ) } is Subset of the carrier of G ; ::_thesis: verum end; end; :: deftheorem defines vertices GRAPH_5:def_2_:_ for G being Graph for pe being FinSequence of the carrier' of G holds vertices pe = { v where v is Vertex of G : ex i being Element of NAT st ( i in dom pe & v in vertices (pe /. i) ) } ; theorem Th18: :: GRAPH_5:18 for G being Graph for pe, qe being FinSequence of the carrier' of G for p being oriented Simple Chain of G st p = pe ^ qe & len pe >= 1 & len qe >= 1 & the Source of G . (p . 1) <> the Target of G . (p . (len p)) holds ( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe ) proof let G be Graph; ::_thesis: for pe, qe being FinSequence of the carrier' of G for p being oriented Simple Chain of G st p = pe ^ qe & len pe >= 1 & len qe >= 1 & the Source of G . (p . 1) <> the Target of G . (p . (len p)) holds ( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe ) let pe, qe be FinSequence of the carrier' of G; ::_thesis: for p being oriented Simple Chain of G st p = pe ^ qe & len pe >= 1 & len qe >= 1 & the Source of G . (p . 1) <> the Target of G . (p . (len p)) holds ( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe ) let p be oriented Simple Chain of G; ::_thesis: ( p = pe ^ qe & len pe >= 1 & len qe >= 1 & the Source of G . (p . 1) <> the Target of G . (p . (len p)) implies ( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe ) ) set FT = the Target of G; set FS = the Source of G; assume that A1: p = pe ^ qe and A2: len pe >= 1 and A3: len qe >= 1 and A4: the Source of G . (p . 1) <> the Target of G . (p . (len p)) ; ::_thesis: ( not the Source of G . (p . 1) in vertices qe & not the Target of G . (p . (len p)) in vertices pe ) consider vs being FinSequence of the carrier of G such that A5: vs is_oriented_vertex_seq_of p and A6: 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 ) by GRAPH_4:def_7; A7: len vs = (len p) + 1 by A5, GRAPH_4:def_5; then A8: 1 <= len vs by NAT_1:12; A9: len p = (len pe) + (len qe) by A1, FINSEQ_1:22; then A10: len p >= 1 by A2, NAT_1:12; then p . 1 orientedly_joins vs /. 1,vs /. (1 + 1) by A5, GRAPH_4:def_5; then A11: the Source of G . (p . 1) = vs /. 1 by GRAPH_4:def_1 .= vs . 1 by A8, FINSEQ_4:15 ; p . (len p) orientedly_joins vs /. (len p),vs /. ((len p) + 1) by A5, A10, GRAPH_4:def_5; then A12: the Target of G . (p . (len p)) = vs /. ((len p) + 1) by GRAPH_4:def_1 .= vs . (len vs) by A7, A8, FINSEQ_4:15 ; hereby ::_thesis: not the Target of G . (p . (len p)) in vertices pe assume the Source of G . (p . 1) in vertices qe ; ::_thesis: contradiction then consider x being Vertex of G such that A13: the Source of G . (p . 1) = x and A14: ex i being Element of NAT st ( i in dom qe & x in vertices (qe /. i) ) ; consider i being Element of NAT such that A15: i in dom qe and A16: x in vertices (qe /. i) by A14; set k = (len pe) + i; A17: qe /. i = qe . i by A15, PARTFUN1:def_6 .= p . ((len pe) + i) by A1, A15, FINSEQ_1:def_7 ; 1 <= i by A15, FINSEQ_3:25; then A18: 1 < i + 1 by NAT_1:13; i <= len qe by A15, FINSEQ_3:25; then A19: (len pe) + i <= len p by A9, XREAL_1:7; then A20: (len pe) + i <= len vs by A7, NAT_1:13; 1 + i <= (len pe) + i by A2, XREAL_1:7; then A21: 1 < (len pe) + i by A18, XXREAL_0:2; then A22: p . ((len pe) + i) orientedly_joins vs /. ((len pe) + i),vs /. (((len pe) + i) + 1) by A5, A19, GRAPH_4:def_5; percases ( x = the Source of G . (p . ((len pe) + i)) or x = the Target of G . (p . ((len pe) + i)) ) by A16, A17, TARSKI:def_2; supposeA23: x = the Source of G . (p . ((len pe) + i)) ; ::_thesis: contradiction the Source of G . (p . ((len pe) + i)) = vs /. ((len pe) + i) by A22, GRAPH_4:def_1 .= vs . ((len pe) + i) by A21, A20, FINSEQ_4:15 ; hence contradiction by A4, A6, A11, A12, A13, A21, A20, A23; ::_thesis: verum end; supposeA24: x = the Target of G . (p . ((len pe) + i)) ; ::_thesis: contradiction A25: 1 < ((len pe) + i) + 1 by A21, NAT_1:13; A26: ((len pe) + i) + 1 <= len vs by A7, A19, XREAL_1:7; the Target of G . (p . ((len pe) + i)) = vs /. (((len pe) + i) + 1) by A22, GRAPH_4:def_1 .= vs . (((len pe) + i) + 1) by A26, FINSEQ_4:15, NAT_1:12 ; hence contradiction by A4, A6, A11, A12, A13, A24, A26, A25; ::_thesis: verum end; end; end; hereby ::_thesis: verum assume the Target of G . (p . (len p)) in vertices pe ; ::_thesis: contradiction then consider x being Vertex of G such that A27: the Target of G . (p . (len p)) = x and A28: ex i being Element of NAT st ( i in dom pe & x in vertices (pe /. i) ) ; consider i being Element of NAT such that A29: i in dom pe and A30: x in vertices (pe /. i) by A28; A31: pe /. i = pe . i by A29, PARTFUN1:def_6 .= p . i by A1, A29, FINSEQ_1:def_7 ; A32: i <= len pe by A29, FINSEQ_3:25; then A33: i <= len p by A9, NAT_1:12; then A34: i < len vs by A7, NAT_1:13; A35: 1 <= i by A29, FINSEQ_3:25; then A36: p . i orientedly_joins vs /. i,vs /. (i + 1) by A5, A33, GRAPH_4:def_5; percases ( x = the Source of G . (p . i) or x = the Target of G . (p . i) ) by A30, A31, TARSKI:def_2; supposeA37: x = the Source of G . (p . i) ; ::_thesis: contradiction the Source of G . (p . i) = vs /. i by A36, GRAPH_4:def_1 .= vs . i by A35, A34, FINSEQ_4:15 ; hence contradiction by A4, A6, A12, A27, A35, A34, A37; ::_thesis: verum end; supposeA38: x = the Target of G . (p . i) ; ::_thesis: contradiction A39: i + 1 <= len vs by A7, A33, XREAL_1:7; ( (len pe) + 1 <= (len pe) + (len qe) & i + 1 <= (len pe) + 1 ) by A3, A32, XREAL_1:7; then i + 1 <= len p by A9, XXREAL_0:2; then A40: ( 1 <= i + 1 & i + 1 < len vs ) by A7, NAT_1:12, NAT_1:13; the Target of G . (p . i) = vs /. (i + 1) by A36, GRAPH_4:def_1 .= vs . (i + 1) by A39, FINSEQ_4:15, NAT_1:12 ; hence contradiction by A4, A6, A11, A12, A27, A38, A40; ::_thesis: verum end; end; end; end; theorem Th19: :: GRAPH_5:19 for V being set for G being Graph for pe being FinSequence of the carrier' of G holds ( vertices pe c= V iff for i being Nat st i in dom pe holds vertices (pe /. i) c= V ) proof let V be set ; ::_thesis: for G being Graph for pe being FinSequence of the carrier' of G holds ( vertices pe c= V iff for i being Nat st i in dom pe holds vertices (pe /. i) c= V ) let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G holds ( vertices pe c= V iff for i being Nat st i in dom pe holds vertices (pe /. i) c= V ) let pe be FinSequence of the carrier' of G; ::_thesis: ( vertices pe c= V iff for i being Nat st i in dom pe holds vertices (pe /. i) c= V ) set FS = the Source of G; set FT = the Target of G; hereby ::_thesis: ( ( for i being Nat st i in dom pe holds vertices (pe /. i) c= V ) implies vertices pe c= V ) assume A1: vertices pe c= V ; ::_thesis: for i being Nat st i in dom pe holds vertices (pe /. i) c= V hereby ::_thesis: verum let i be Nat; ::_thesis: ( i in dom pe implies vertices (pe /. i) c= V ) assume A2: i in dom pe ; ::_thesis: vertices (pe /. i) c= V then A3: ( 1 <= i & i <= len pe ) by FINSEQ_3:25; thus vertices (pe /. i) c= V ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in vertices (pe /. i) or x in V ) assume A4: x in vertices (pe /. i) ; ::_thesis: x in V then ( x = the Source of G . (pe /. i) or x = the Target of G . (pe /. i) ) by TARSKI:def_2; then ( x = the Source of G . (pe . i) or x = the Target of G . (pe . i) ) by A3, FINSEQ_4:15; then reconsider y = x as Vertex of G by A2, FINSEQ_2:11, FUNCT_2:5; y in { v where v is Vertex of G : ex i being Element of NAT st ( i in dom pe & v in vertices (pe /. i) ) } by A2, A4; hence x in V by A1; ::_thesis: verum end; end; end; assume A5: for i being Nat st i in dom pe holds vertices (pe /. i) c= V ; ::_thesis: vertices pe c= V let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in vertices pe or x in V ) assume x in vertices pe ; ::_thesis: x in V then consider y being Vertex of G such that A6: y = x and A7: ex i being Element of NAT st ( i in dom pe & y in vertices (pe /. i) ) ; consider i being Element of NAT such that A8: i in dom pe and A9: y in vertices (pe /. i) by A7; vertices (pe /. i) c= V by A5, A8; hence x in V by A6, A9; ::_thesis: verum end; theorem Th20: :: GRAPH_5:20 for V being set for G being Graph for pe being FinSequence of the carrier' of G st not vertices pe c= V holds ex i being Element of NAT ex q, r being FinSequence of the carrier' of G st ( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V & len q = i & pe = q ^ r & vertices q c= V ) proof let V be set ; ::_thesis: for G being Graph for pe being FinSequence of the carrier' of G st not vertices pe c= V holds ex i being Element of NAT ex q, r being FinSequence of the carrier' of G st ( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V & len q = i & pe = q ^ r & vertices q c= V ) let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G st not vertices pe c= V holds ex i being Element of NAT ex q, r being FinSequence of the carrier' of G st ( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V & len q = i & pe = q ^ r & vertices q c= V ) let pe be FinSequence of the carrier' of G; ::_thesis: ( not vertices pe c= V implies ex i being Element of NAT ex q, r being FinSequence of the carrier' of G st ( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V & len q = i & pe = q ^ r & vertices q c= V ) ) defpred S1[ Nat] means ( $1 in dom pe & not vertices (pe /. $1) c= V ); assume not vertices pe c= V ; ::_thesis: ex i being Element of NAT ex q, r being FinSequence of the carrier' of G st ( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V & len q = i & pe = q ^ r & vertices q c= V ) then A1: ex i being Nat st S1[i] by Th19; consider k being Nat such that A2: ( S1[k] & ( for n being Nat st S1[n] holds k <= n ) ) from NAT_1:sch_5(A1); k <= len pe by A2, FINSEQ_3:25; then consider j being Nat such that A3: len pe = k + j by NAT_1:10; reconsider j = j as Element of NAT by ORDINAL1:def_12; 1 <= k by A2, FINSEQ_3:25; then consider i being Nat such that A4: k = 1 + i by NAT_1:10; reconsider i = i as Element of NAT by ORDINAL1:def_12; len pe = i + (1 + j) by A4, A3; then consider q, r being FinSequence such that A5: len q = i and len r = 1 + j and A6: pe = q ^ r by FINSEQ_2:22; reconsider q = q, r = r as FinSequence of the carrier' of G by A6, FINSEQ_1:36; take i ; ::_thesis: ex q, r being FinSequence of the carrier' of G st ( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V & len q = i & pe = q ^ r & vertices q c= V ) take q ; ::_thesis: ex r being FinSequence of the carrier' of G st ( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V & len q = i & pe = q ^ r & vertices q c= V ) take r ; ::_thesis: ( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V & len q = i & pe = q ^ r & vertices q c= V ) thus ( i + 1 <= len pe & not vertices (pe /. (i + 1)) c= V ) by A2, A4, FINSEQ_3:25; ::_thesis: ( len q = i & pe = q ^ r & vertices q c= V ) thus ( len q = i & pe = q ^ r ) by A5, A6; ::_thesis: vertices q c= V now__::_thesis:_for_m_being_Nat_st_m_in_dom_q_holds_ vertices_(q_/._m)_c=_V let m be Nat; ::_thesis: ( m in dom q implies vertices (q /. m) c= V ) assume A7: m in dom q ; ::_thesis: vertices (q /. m) c= V then A8: m <= len q by FINSEQ_3:25; A9: dom q c= dom pe by A6, FINSEQ_1:26; assume A10: not vertices (q /. m) c= V ; ::_thesis: contradiction q /. m = q . m by A7, PARTFUN1:def_6 .= pe . m by A6, A7, FINSEQ_1:def_7 .= pe /. m by A7, A9, PARTFUN1:def_6 ; then k <= m by A2, A7, A10, A9; hence contradiction by A4, A5, A8, NAT_1:13; ::_thesis: verum end; hence vertices q c= V by Th19; ::_thesis: verum end; theorem Th21: :: GRAPH_5:21 for G being Graph for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe holds vertices qe c= vertices pe proof let G be Graph; ::_thesis: for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe holds vertices qe c= vertices pe let qe, pe be FinSequence of the carrier' of G; ::_thesis: ( rng qe c= rng pe implies vertices qe c= vertices pe ) assume A1: rng qe c= rng pe ; ::_thesis: vertices qe c= vertices pe let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in vertices qe or x in vertices pe ) assume x in vertices qe ; ::_thesis: x in vertices pe then consider v being Vertex of G such that A2: x = v and A3: ex i being Element of NAT st ( i in dom qe & v in vertices (qe /. i) ) ; consider i being Element of NAT such that A4: i in dom qe and A5: v in vertices (qe /. i) by A3; qe . i in rng qe by A4, FUNCT_1:def_3; then consider j being set such that A6: j in dom pe and A7: qe . i = pe . j by A1, FUNCT_1:def_3; reconsider j = j as Element of NAT by A6; qe /. i = qe . i by A4, PARTFUN1:def_6; then pe /. j = qe /. i by A6, A7, PARTFUN1:def_6; hence x in vertices pe by A2, A5, A6; ::_thesis: verum end; theorem Th22: :: GRAPH_5:22 for X, V being set for G being Graph for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & (vertices pe) \ X c= V holds (vertices qe) \ X c= V proof let X, V be set ; ::_thesis: for G being Graph for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & (vertices pe) \ X c= V holds (vertices qe) \ X c= V let G be Graph; ::_thesis: for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & (vertices pe) \ X c= V holds (vertices qe) \ X c= V let qe, pe be FinSequence of the carrier' of G; ::_thesis: ( rng qe c= rng pe & (vertices pe) \ X c= V implies (vertices qe) \ X c= V ) assume that A1: rng qe c= rng pe and A2: (vertices pe) \ X c= V ; ::_thesis: (vertices qe) \ X c= V vertices qe c= vertices pe by A1, Th21; then (vertices qe) \ X c= (vertices pe) \ X by XBOOLE_1:35; hence (vertices qe) \ X c= V by A2, XBOOLE_1:1; ::_thesis: verum end; theorem Th23: :: GRAPH_5:23 for X, V being set for G being Graph for pe, qe being FinSequence of the carrier' of G st (vertices (pe ^ qe)) \ X c= V holds ( (vertices pe) \ X c= V & (vertices qe) \ X c= V ) proof let X, V be set ; ::_thesis: for G being Graph for pe, qe being FinSequence of the carrier' of G st (vertices (pe ^ qe)) \ X c= V holds ( (vertices pe) \ X c= V & (vertices qe) \ X c= V ) let G be Graph; ::_thesis: for pe, qe being FinSequence of the carrier' of G st (vertices (pe ^ qe)) \ X c= V holds ( (vertices pe) \ X c= V & (vertices qe) \ X c= V ) let pe, qe be FinSequence of the carrier' of G; ::_thesis: ( (vertices (pe ^ qe)) \ X c= V implies ( (vertices pe) \ X c= V & (vertices qe) \ X c= V ) ) A1: ( rng pe c= rng (pe ^ qe) & rng qe c= rng (pe ^ qe) ) by FINSEQ_1:29, FINSEQ_1:30; assume (vertices (pe ^ qe)) \ X c= V ; ::_thesis: ( (vertices pe) \ X c= V & (vertices qe) \ X c= V ) hence ( (vertices pe) \ X c= V & (vertices qe) \ X c= V ) by A1, Th22; ::_thesis: verum end; theorem Th24: :: GRAPH_5:24 for i being Element of NAT for G being Graph for pe being FinSequence of the carrier' of G for v being Element of G st i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) holds v in vertices pe proof let i be Element of NAT ; ::_thesis: for G being Graph for pe being FinSequence of the carrier' of G for v being Element of G st i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) holds v in vertices pe let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G for v being Element of G st i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) holds v in vertices pe let pe be FinSequence of the carrier' of G; ::_thesis: for v being Element of G st i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) holds v in vertices pe let v be Element of G; ::_thesis: ( i in dom pe & ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) implies v in vertices pe ) set FS = the Source of G; set FT = the Target of G; assume that A1: i in dom pe and A2: ( v = the Source of G . (pe . i) or v = the Target of G . (pe . i) ) ; ::_thesis: v in vertices pe ( v = the Source of G . (pe /. i) or v = the Target of G . (pe /. i) ) by A1, A2, PARTFUN1:def_6; then v in vertices (pe /. i) by TARSKI:def_2; hence v in vertices pe by A1; ::_thesis: verum end; theorem Th25: :: GRAPH_5:25 for G being Graph for pe being FinSequence of the carrier' of G st len pe = 1 holds vertices pe = vertices (pe /. 1) proof let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G st len pe = 1 holds vertices pe = vertices (pe /. 1) let pe be FinSequence of the carrier' of G; ::_thesis: ( len pe = 1 implies vertices pe = vertices (pe /. 1) ) set FS = the Source of G; set FT = the Target of G; assume A1: len pe = 1 ; ::_thesis: vertices pe = vertices (pe /. 1) then A2: 1 in dom pe by FINSEQ_3:25; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_vertices_pe_implies_x_in_vertices_(pe_/._1)_)_&_(_x_in_vertices_(pe_/._1)_implies_x_in_vertices_pe_)_) let x be set ; ::_thesis: ( ( x in vertices pe implies x in vertices (pe /. 1) ) & ( x in vertices (pe /. 1) implies x in vertices pe ) ) hereby ::_thesis: ( x in vertices (pe /. 1) implies x in vertices pe ) assume x in vertices pe ; ::_thesis: x in vertices (pe /. 1) then consider y being Vertex of G such that A3: y = x and A4: ex i being Element of NAT st ( i in dom pe & y in vertices (pe /. i) ) ; consider i being Element of NAT such that A5: i in dom pe and A6: y in vertices (pe /. i) by A4; ( 1 <= i & i <= len pe ) by A5, FINSEQ_3:25; hence x in vertices (pe /. 1) by A1, A3, A6, XXREAL_0:1; ::_thesis: verum end; assume A7: x in vertices (pe /. 1) ; ::_thesis: x in vertices pe then ( x = the Source of G . (pe /. 1) or x = the Target of G . (pe /. 1) ) by TARSKI:def_2; then ( x = the Source of G . (pe . 1) or x = the Target of G . (pe . 1) ) by A1, FINSEQ_4:15; then reconsider y = x as Vertex of G by A2, FINSEQ_2:11, FUNCT_2:5; y in { v where v is Vertex of G : ex i being Element of NAT st ( i in dom pe & v in vertices (pe /. i) ) } by A2, A7; hence x in vertices pe ; ::_thesis: verum end; hence vertices pe = vertices (pe /. 1) by TARSKI:1; ::_thesis: verum end; theorem Th26: :: GRAPH_5:26 for G being Graph for pe, qe being FinSequence of the carrier' of G holds ( vertices pe c= vertices (pe ^ qe) & vertices qe c= vertices (pe ^ qe) ) proof let G be Graph; ::_thesis: for pe, qe being FinSequence of the carrier' of G holds ( vertices pe c= vertices (pe ^ qe) & vertices qe c= vertices (pe ^ qe) ) let pe, qe be FinSequence of the carrier' of G; ::_thesis: ( vertices pe c= vertices (pe ^ qe) & vertices qe c= vertices (pe ^ qe) ) ( rng pe c= rng (pe ^ qe) & rng qe c= rng (pe ^ qe) ) by FINSEQ_1:29, FINSEQ_1:30; hence ( vertices pe c= vertices (pe ^ qe) & vertices qe c= vertices (pe ^ qe) ) by Th21; ::_thesis: verum end; theorem Th27: :: GRAPH_5:27 for G being Graph for pe being FinSequence of the carrier' of G for p, q being oriented Chain of G st p = q ^ pe & len q >= 1 & len pe = 1 holds vertices p = (vertices q) \/ {( the Target of G . (pe . 1))} proof let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G for p, q being oriented Chain of G st p = q ^ pe & len q >= 1 & len pe = 1 holds vertices p = (vertices q) \/ {( the Target of G . (pe . 1))} let pe be FinSequence of the carrier' of G; ::_thesis: for p, q being oriented Chain of G st p = q ^ pe & len q >= 1 & len pe = 1 holds vertices p = (vertices q) \/ {( the Target of G . (pe . 1))} let p, q be oriented Chain of G; ::_thesis: ( p = q ^ pe & len q >= 1 & len pe = 1 implies vertices p = (vertices q) \/ {( the Target of G . (pe . 1))} ) assume that A1: p = q ^ pe and A2: len q >= 1 and A3: len pe = 1 ; ::_thesis: vertices p = (vertices q) \/ {( the Target of G . (pe . 1))} set FS = the Source of G; set FT = the Target of G; set V3 = {( the Target of G . (pe . 1))}; A4: len p = (len q) + 1 by A1, A3, FINSEQ_1:22; now__::_thesis:_for_x_being_set_holds_ (_(_x_in_vertices_p_implies_x_in_(vertices_q)_\/_{(_the_Target_of_G_._(pe_._1))}_)_&_(_x_in_(vertices_q)_\/_{(_the_Target_of_G_._(pe_._1))}_implies_x_in_vertices_p_)_) let x be set ; ::_thesis: ( ( x in vertices p implies x in (vertices q) \/ {( the Target of G . (pe . 1))} ) & ( x in (vertices q) \/ {( the Target of G . (pe . 1))} implies b1 in vertices p ) ) hereby ::_thesis: ( x in (vertices q) \/ {( the Target of G . (pe . 1))} implies b1 in vertices p ) assume x in vertices p ; ::_thesis: x in (vertices q) \/ {( the Target of G . (pe . 1))} then consider y being Vertex of G such that A5: y = x and A6: ex i being Element of NAT st ( i in dom p & y in vertices (p /. i) ) ; consider i being Element of NAT such that A7: i in dom p and A8: y in vertices (p /. i) by A6; A9: 1 <= i by A7, FINSEQ_3:25; A10: i <= len p by A7, FINSEQ_3:25; percases ( i <= len q or i > len q ) ; supposeA11: i <= len q ; ::_thesis: x in (vertices q) \/ {( the Target of G . (pe . 1))} then A12: i in dom q by A9, FINSEQ_3:25; p /. i = p . i by A9, A10, FINSEQ_4:15 .= q . i by A1, A9, A11, Lm1 .= q /. i by A9, A11, FINSEQ_4:15 ; then y in { v where v is Vertex of G : ex j being Element of NAT st ( j in dom q & v in vertices (q /. j) ) } by A8, A12; hence x in (vertices q) \/ {( the Target of G . (pe . 1))} by A5, XBOOLE_0:def_3; ::_thesis: verum end; supposeA13: i > len q ; ::_thesis: x in (vertices q) \/ {( the Target of G . (pe . 1))} reconsider z = y as Vertex of G ; i >= (len q) + 1 by A13, NAT_1:13; then A14: i = (len q) + 1 by A4, A10, XXREAL_0:1; A15: ( y = the Source of G . (p /. i) or y = the Target of G . (p /. i) ) by A8, TARSKI:def_2; hereby ::_thesis: verum percases ( z = the Source of G . (p . i) or z = the Target of G . (p . i) ) by A9, A10, A15, FINSEQ_4:15; supposeA16: z = the Source of G . (p . i) ; ::_thesis: x in (vertices q) \/ {( the Target of G . (pe . 1))} len q < len p by A4, NAT_1:13; then z = the Target of G . (p . (len q)) by A2, A14, A16, GRAPH_1:def_15 .= the Target of G . (q . (len q)) by A1, A2, Lm1 .= the Target of G . (q /. (len q)) by A2, FINSEQ_4:15 ; then A17: z in vertices (q /. (len q)) by TARSKI:def_2; len q in dom q by A2, FINSEQ_3:25; then z in { v where v is Vertex of G : ex j being Element of NAT st ( j in dom q & v in vertices (q /. j) ) } by A17; hence x in (vertices q) \/ {( the Target of G . (pe . 1))} by A5, XBOOLE_0:def_3; ::_thesis: verum end; suppose z = the Target of G . (p . i) ; ::_thesis: x in (vertices q) \/ {( the Target of G . (pe . 1))} then z = the Target of G . (pe . 1) by A1, A3, A14, Lm2; then z in {( the Target of G . (pe . 1))} by TARSKI:def_1; hence x in (vertices q) \/ {( the Target of G . (pe . 1))} by A5, XBOOLE_0:def_3; ::_thesis: verum end; end; end; end; end; end; assume A18: x in (vertices q) \/ {( the Target of G . (pe . 1))} ; ::_thesis: b1 in vertices p percases ( x in vertices q or x in {( the Target of G . (pe . 1))} ) by A18, XBOOLE_0:def_3; supposeA19: x in vertices q ; ::_thesis: b1 in vertices p vertices q c= vertices p by A1, Th26; hence x in vertices p by A19; ::_thesis: verum end; supposeA20: x in {( the Target of G . (pe . 1))} ; ::_thesis: b1 in vertices p 1 in dom pe by A3, FINSEQ_3:25; then reconsider y = the Target of G . (pe . 1) as Vertex of G by FINSEQ_2:11, FUNCT_2:5; A21: 1 <= len p by A4, NAT_1:12; then A22: len p in dom p by FINSEQ_3:25; y = the Target of G . (p . (len p)) by A1, A3, A4, Lm2 .= the Target of G . (p /. (len p)) by A21, FINSEQ_4:15 ; then A23: y in vertices (p /. (len p)) by TARSKI:def_2; x = the Target of G . (pe . 1) by A20, TARSKI:def_1; hence x in vertices p by A23, A22; ::_thesis: verum end; end; end; hence vertices p = (vertices q) \/ {( the Target of G . (pe . 1))} by TARSKI:1; ::_thesis: verum end; theorem Th28: :: GRAPH_5:28 for G being Graph for v being Element of G for p being oriented Chain of G st v <> the Source of G . (p . 1) & v in vertices p holds ex i being Element of NAT st ( 1 <= i & i <= len p & v = the Target of G . (p . i) ) proof let G be Graph; ::_thesis: for v being Element of G for p being oriented Chain of G st v <> the Source of G . (p . 1) & v in vertices p holds ex i being Element of NAT st ( 1 <= i & i <= len p & v = the Target of G . (p . i) ) let v be Element of G; ::_thesis: for p being oriented Chain of G st v <> the Source of G . (p . 1) & v in vertices p holds ex i being Element of NAT st ( 1 <= i & i <= len p & v = the Target of G . (p . i) ) let p be oriented Chain of G; ::_thesis: ( v <> the Source of G . (p . 1) & v in vertices p implies ex i being Element of NAT st ( 1 <= i & i <= len p & v = the Target of G . (p . i) ) ) set FT = the Target of G; set FS = the Source of G; assume that A1: v <> the Source of G . (p . 1) and A2: v in vertices p ; ::_thesis: ex i being Element of NAT st ( 1 <= i & i <= len p & v = the Target of G . (p . i) ) consider u being Vertex of G such that A3: v = u and A4: ex i being Element of NAT st ( i in dom p & u in vertices (p /. i) ) by A2; consider i being Element of NAT such that A5: i in dom p and A6: u in vertices (p /. i) by A4; A7: ( u = the Source of G . (p /. i) or u = the Target of G . (p /. i) ) by A6, TARSKI:def_2; A8: 1 <= i by A5, FINSEQ_3:25; A9: i <= len p by A5, FINSEQ_3:25; percases ( v = the Target of G . (p . i) or v = the Source of G . (p . i) ) by A3, A7, A8, A9, FINSEQ_4:15; supposeA10: v = the Target of G . (p . i) ; ::_thesis: ex i being Element of NAT st ( 1 <= i & i <= len p & v = the Target of G . (p . i) ) take i ; ::_thesis: ( 1 <= i & i <= len p & v = the Target of G . (p . i) ) thus ( 1 <= i & i <= len p & v = the Target of G . (p . i) ) by A5, A10, FINSEQ_3:25; ::_thesis: verum end; supposeA11: v = the Source of G . (p . i) ; ::_thesis: ex i being Element of NAT st ( 1 <= i & i <= len p & v = the Target of G . (p . i) ) consider j being Nat such that A12: i = 1 + j by A8, NAT_1:10; reconsider j = j as Element of NAT by ORDINAL1:def_12; A13: j < len p by A9, A12, NAT_1:13; take j ; ::_thesis: ( 1 <= j & j <= len p & v = the Target of G . (p . j) ) i > 1 by A1, A8, A11, XXREAL_0:1; then j >= 1 by A12, NAT_1:13; hence ( 1 <= j & j <= len p & v = the Target of G . (p . j) ) by A11, A12, A13, GRAPH_1:def_15; ::_thesis: verum end; end; end; begin definition let G be Graph; let p be oriented Chain of G; let v1, v2 be Element of G; predp is_orientedpath_of v1,v2 means :Def3: :: GRAPH_5:def 3 ( p <> {} & the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 ); end; :: deftheorem Def3 defines is_orientedpath_of GRAPH_5:def_3_:_ for G being Graph for p being oriented Chain of G for v1, v2 being Element of G holds ( p is_orientedpath_of v1,v2 iff ( p <> {} & the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 ) ); definition let G be Graph; let v1, v2 be Element of G; let p be oriented Chain of G; let V be set ; predp is_orientedpath_of v1,v2,V means :Def4: :: GRAPH_5:def 4 ( p is_orientedpath_of v1,v2 & (vertices p) \ {v2} c= V ); end; :: deftheorem Def4 defines is_orientedpath_of GRAPH_5:def_4_:_ for G being Graph for v1, v2 being Element of G for p being oriented Chain of G for V being set holds ( p is_orientedpath_of v1,v2,V iff ( p is_orientedpath_of v1,v2 & (vertices p) \ {v2} c= V ) ); definition let G be Graph; let v1, v2 be Element of G; func OrientedPaths (v1,v2) -> Subset of ( the carrier' of G *) equals :: GRAPH_5:def 5 { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } ; coherence { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } is Subset of ( the carrier' of G *) proof set PT = { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } ; { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } c= the carrier' of G * proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } or e in the carrier' of G * ) assume e in { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } ; ::_thesis: e in the carrier' of G * then ex p being oriented Chain of G st ( e = p & p is_orientedpath_of v1,v2 ) ; hence e in the carrier' of G * by FINSEQ_1:def_11; ::_thesis: verum end; hence { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } is Subset of ( the carrier' of G *) ; ::_thesis: verum end; end; :: deftheorem defines OrientedPaths GRAPH_5:def_5_:_ for G being Graph for v1, v2 being Element of G holds OrientedPaths (v1,v2) = { p where p is oriented Chain of G : p is_orientedpath_of v1,v2 } ; theorem Th29: :: GRAPH_5:29 for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds ( v1 in vertices p & v2 in vertices p ) proof let G be Graph; ::_thesis: for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds ( v1 in vertices p & v2 in vertices p ) let v1, v2 be Element of G; ::_thesis: for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds ( v1 in vertices p & v2 in vertices p ) let p be oriented Chain of G; ::_thesis: ( p is_orientedpath_of v1,v2 implies ( v1 in vertices p & v2 in vertices p ) ) assume A1: p is_orientedpath_of v1,v2 ; ::_thesis: ( v1 in vertices p & v2 in vertices p ) then p <> {} by Def3; then 1 <= len p by FINSEQ_1:20; then A2: ( 1 in dom p & len p in dom p ) by FINSEQ_3:25; ( the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 ) by A1, Def3; hence ( v1 in vertices p & v2 in vertices p ) by A2, Th24; ::_thesis: verum end; theorem :: GRAPH_5:30 for x being set for G being Graph for v1, v2 being Element of G holds ( x in OrientedPaths (v1,v2) iff ex p being oriented Chain of G st ( p = x & p is_orientedpath_of v1,v2 ) ) ; theorem Th31: :: GRAPH_5:31 for V being set for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds v1 in V proof let V be set ; ::_thesis: for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds v1 in V let G be Graph; ::_thesis: for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds v1 in V let v1, v2 be Element of G; ::_thesis: for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & v1 <> v2 holds v1 in V let p be oriented Chain of G; ::_thesis: ( p is_orientedpath_of v1,v2,V & v1 <> v2 implies v1 in V ) assume that A1: p is_orientedpath_of v1,v2,V and A2: v1 <> v2 ; ::_thesis: v1 in V p is_orientedpath_of v1,v2 by A1, Def4; then A3: v1 in vertices p by Th29; not v1 in {v2} by A2, TARSKI:def_1; then A4: v1 in (vertices p) \ {v2} by A3, XBOOLE_0:def_5; (vertices p) \ {v2} c= V by A1, Def4; hence v1 in V by A4; ::_thesis: verum end; theorem Th32: :: GRAPH_5:32 for V, U being set for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & V c= U holds p is_orientedpath_of v1,v2,U proof let V, U be set ; ::_thesis: for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & V c= U holds p is_orientedpath_of v1,v2,U let G be Graph; ::_thesis: for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & V c= U holds p is_orientedpath_of v1,v2,U let v1, v2 be Element of G; ::_thesis: for p being oriented Chain of G st p is_orientedpath_of v1,v2,V & V c= U holds p is_orientedpath_of v1,v2,U let p be oriented Chain of G; ::_thesis: ( p is_orientedpath_of v1,v2,V & V c= U implies p is_orientedpath_of v1,v2,U ) assume that A1: p is_orientedpath_of v1,v2,V and A2: V c= U ; ::_thesis: p is_orientedpath_of v1,v2,U (vertices p) \ {v2} c= V by A1, Def4; then A3: (vertices p) \ {v2} c= U by A2, XBOOLE_1:1; p is_orientedpath_of v1,v2 by A1, Def4; hence p is_orientedpath_of v1,v2,U by A3, Def4; ::_thesis: verum end; theorem Th33: :: GRAPH_5:33 for G being Graph for pe being FinSequence of the carrier' of G for v1, v2, v3 being Element of G for p being oriented Chain of G st len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 holds ex q being oriented Chain of G st ( q = p ^ pe & q is_orientedpath_of v1,v3 ) proof let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G for v1, v2, v3 being Element of G for p being oriented Chain of G st len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 holds ex q being oriented Chain of G st ( q = p ^ pe & q is_orientedpath_of v1,v3 ) let pe be FinSequence of the carrier' of G; ::_thesis: for v1, v2, v3 being Element of G for p being oriented Chain of G st len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 holds ex q being oriented Chain of G st ( q = p ^ pe & q is_orientedpath_of v1,v3 ) let v1, v2, v3 be Element of G; ::_thesis: for p being oriented Chain of G st len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 holds ex q being oriented Chain of G st ( q = p ^ pe & q is_orientedpath_of v1,v3 ) let p be oriented Chain of G; ::_thesis: ( len p >= 1 & p is_orientedpath_of v1,v2 & pe . 1 orientedly_joins v2,v3 & len pe = 1 implies ex q being oriented Chain of G st ( q = p ^ pe & q is_orientedpath_of v1,v3 ) ) assume that A1: len p >= 1 and A2: p is_orientedpath_of v1,v2 and A3: pe . 1 orientedly_joins v2,v3 and A4: len pe = 1 ; ::_thesis: ex q being oriented Chain of G st ( q = p ^ pe & q is_orientedpath_of v1,v3 ) set FT = the Target of G; set FS = the Source of G; A5: pe is oriented Chain of G by A4, Th15; ( the Target of G . (p . (len p)) = v2 & the Source of G . (pe . 1) = v2 ) by A2, A3, Def3, GRAPH_4:def_1; then reconsider q = p ^ pe as oriented Chain of G by A5, Th12; A6: len q = (len p) + 1 by A4, FINSEQ_1:22; the Target of G . (pe . 1) = v3 by A3, GRAPH_4:def_1; then A7: the Target of G . (q . (len q)) = v3 by A4, A6, Lm2; the Source of G . (p . 1) = v1 by A2, Def3; then A8: the Source of G . (q . 1) = v1 by A1, Lm1; take q ; ::_thesis: ( q = p ^ pe & q is_orientedpath_of v1,v3 ) q <> {} by A6; hence ( q = p ^ pe & q is_orientedpath_of v1,v3 ) by A8, A7, Def3; ::_thesis: verum end; theorem Th34: :: GRAPH_5:34 for V being set for G being Graph for pe being FinSequence of the carrier' of G for v1, v2, v3 being Element of G for q, p being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds q is_orientedpath_of v1,v3,V \/ {v2} proof let V be set ; ::_thesis: for G being Graph for pe being FinSequence of the carrier' of G for v1, v2, v3 being Element of G for q, p being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds q is_orientedpath_of v1,v3,V \/ {v2} let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G for v1, v2, v3 being Element of G for q, p being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds q is_orientedpath_of v1,v3,V \/ {v2} let pe be FinSequence of the carrier' of G; ::_thesis: for v1, v2, v3 being Element of G for q, p being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds q is_orientedpath_of v1,v3,V \/ {v2} let v1, v2, v3 be Element of G; ::_thesis: for q, p being oriented Chain of G st q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 holds q is_orientedpath_of v1,v3,V \/ {v2} let q, p be oriented Chain of G; ::_thesis: ( q = p ^ pe & len p >= 1 & len pe = 1 & p is_orientedpath_of v1,v2,V & pe . 1 orientedly_joins v2,v3 implies q is_orientedpath_of v1,v3,V \/ {v2} ) assume that A1: q = p ^ pe and A2: ( len p >= 1 & len pe = 1 ) and A3: p is_orientedpath_of v1,v2,V and A4: pe . 1 orientedly_joins v2,v3 ; ::_thesis: q is_orientedpath_of v1,v3,V \/ {v2} p is_orientedpath_of v1,v2 by A3, Def4; then A5: ex r being oriented Chain of G st ( r = p ^ pe & r is_orientedpath_of v1,v3 ) by A2, A4, Th33; set FT = the Target of G; the Target of G . (pe . 1) = v3 by A4, GRAPH_4:def_1; then (vertices q) \ {v3} = ((vertices p) \/ {v3}) \ {v3} by A1, A2, Th27 .= (vertices p) \ {v3} by XBOOLE_1:40 ; then A6: (vertices q) \ {v3} c= vertices p by XBOOLE_1:36; (vertices p) \ {v2} c= V by A3, Def4; then vertices p c= V \/ {v2} by XBOOLE_1:44; then (vertices q) \ {v3} c= V \/ {v2} by A6, XBOOLE_1:1; hence q is_orientedpath_of v1,v3,V \/ {v2} by A1, A5, Def4; ::_thesis: verum end; begin definition let G be Graph; let p be oriented Chain of G; let v1, v2 be Element of G; predp is_acyclicpath_of v1,v2 means :Def6: :: GRAPH_5:def 6 ( p is Simple & p is_orientedpath_of v1,v2 ); end; :: deftheorem Def6 defines is_acyclicpath_of GRAPH_5:def_6_:_ for G being Graph for p being oriented Chain of G for v1, v2 being Element of G holds ( p is_acyclicpath_of v1,v2 iff ( p is Simple & p is_orientedpath_of v1,v2 ) ); definition let G be Graph; let p be oriented Chain of G; let v1, v2 be Element of G; let V be set ; predp is_acyclicpath_of v1,v2,V means :Def7: :: GRAPH_5:def 7 ( p is Simple & p is_orientedpath_of v1,v2,V ); end; :: deftheorem Def7 defines is_acyclicpath_of GRAPH_5:def_7_:_ for G being Graph for p being oriented Chain of G for v1, v2 being Element of G for V being set holds ( p is_acyclicpath_of v1,v2,V iff ( p is Simple & p is_orientedpath_of v1,v2,V ) ); definition let G be Graph; let v1, v2 be Element of G; func AcyclicPaths (v1,v2) -> Subset of ( the carrier' of G *) equals :: GRAPH_5:def 8 { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } ; coherence { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } is Subset of ( the carrier' of G *) proof set PT = { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } ; { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } c= the carrier' of G * proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } or e in the carrier' of G * ) assume e in { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } ; ::_thesis: e in the carrier' of G * then ex p being oriented Simple Chain of G st ( e = p & p is_acyclicpath_of v1,v2 ) ; hence e in the carrier' of G * by FINSEQ_1:def_11; ::_thesis: verum end; hence { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } is Subset of ( the carrier' of G *) ; ::_thesis: verum end; end; :: deftheorem defines AcyclicPaths GRAPH_5:def_8_:_ for G being Graph for v1, v2 being Element of G holds AcyclicPaths (v1,v2) = { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2 } ; definition let G be Graph; let v1, v2 be Element of G; let V be set ; func AcyclicPaths (v1,v2,V) -> Subset of ( the carrier' of G *) equals :: GRAPH_5:def 9 { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } ; coherence { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } is Subset of ( the carrier' of G *) proof set PT = { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } ; { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } c= the carrier' of G * proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } or e in the carrier' of G * ) assume e in { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } ; ::_thesis: e in the carrier' of G * then ex p being oriented Simple Chain of G st ( e = p & p is_acyclicpath_of v1,v2,V ) ; hence e in the carrier' of G * by FINSEQ_1:def_11; ::_thesis: verum end; hence { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } is Subset of ( the carrier' of G *) ; ::_thesis: verum end; end; :: deftheorem defines AcyclicPaths GRAPH_5:def_9_:_ for G being Graph for v1, v2 being Element of G for V being set holds AcyclicPaths (v1,v2,V) = { p where p is oriented Simple Chain of G : p is_acyclicpath_of v1,v2,V } ; definition let G be Graph; let p be oriented Chain of G; func AcyclicPaths p -> Subset of ( the carrier' of G *) equals :: GRAPH_5:def 10 { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } ; coherence { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } is Subset of ( the carrier' of G *) proof set PT = { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } ; { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } c= the carrier' of G * proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } or e in the carrier' of G * ) assume e in { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } ; ::_thesis: e in the carrier' of G * then ex q being oriented Simple Chain of G st ( e = q & q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) ; hence e in the carrier' of G * by FINSEQ_1:def_11; ::_thesis: verum end; hence { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } is Subset of ( the carrier' of G *) ; ::_thesis: verum end; end; :: deftheorem defines AcyclicPaths GRAPH_5:def_10_:_ for G being Graph for p being oriented Chain of G holds AcyclicPaths p = { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } ; definition let G be Graph; func AcyclicPaths G -> Subset of ( the carrier' of G *) equals :: GRAPH_5:def 11 { q where q is oriented Simple Chain of G : verum } ; coherence { q where q is oriented Simple Chain of G : verum } is Subset of ( the carrier' of G *) proof set PT = { q where q is oriented Simple Chain of G : verum } ; { q where q is oriented Simple Chain of G : verum } c= the carrier' of G * proof let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in { q where q is oriented Simple Chain of G : verum } or e in the carrier' of G * ) assume e in { q where q is oriented Simple Chain of G : verum } ; ::_thesis: e in the carrier' of G * then ex q being oriented Simple Chain of G st e = q ; hence e in the carrier' of G * by FINSEQ_1:def_11; ::_thesis: verum end; hence { q where q is oriented Simple Chain of G : verum } is Subset of ( the carrier' of G *) ; ::_thesis: verum end; end; :: deftheorem defines AcyclicPaths GRAPH_5:def_11_:_ for G being Graph holds AcyclicPaths G = { q where q is oriented Simple Chain of G : verum } ; theorem :: GRAPH_5:35 for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p = {} holds not p is_acyclicpath_of v1,v2 proof let G be Graph; ::_thesis: for v1, v2 being Element of G for p being oriented Chain of G st p = {} holds not p is_acyclicpath_of v1,v2 let v1, v2 be Element of G; ::_thesis: for p being oriented Chain of G st p = {} holds not p is_acyclicpath_of v1,v2 let p be oriented Chain of G; ::_thesis: ( p = {} implies not p is_acyclicpath_of v1,v2 ) assume p = {} ; ::_thesis: not p is_acyclicpath_of v1,v2 then not p is_orientedpath_of v1,v2 by Def3; hence not p is_acyclicpath_of v1,v2 by Def6; ::_thesis: verum end; theorem :: GRAPH_5:36 for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_acyclicpath_of v1,v2 holds p is_orientedpath_of v1,v2 by Def6; theorem :: GRAPH_5:37 for G being Graph for v1, v2 being Element of G holds AcyclicPaths (v1,v2) c= OrientedPaths (v1,v2) proof let G be Graph; ::_thesis: for v1, v2 being Element of G holds AcyclicPaths (v1,v2) c= OrientedPaths (v1,v2) let v1, v2 be Element of G; ::_thesis: AcyclicPaths (v1,v2) c= OrientedPaths (v1,v2) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in AcyclicPaths (v1,v2) or x in OrientedPaths (v1,v2) ) assume x in AcyclicPaths (v1,v2) ; ::_thesis: x in OrientedPaths (v1,v2) then consider p being oriented Simple Chain of G such that A1: x = p and A2: p is_acyclicpath_of v1,v2 ; p is_orientedpath_of v1,v2 by A2, Def6; hence x in OrientedPaths (v1,v2) by A1; ::_thesis: verum end; theorem Th38: :: GRAPH_5:38 for G being Graph for p being oriented Chain of G holds AcyclicPaths p c= AcyclicPaths G proof let G be Graph; ::_thesis: for p being oriented Chain of G holds AcyclicPaths p c= AcyclicPaths G let p be oriented Chain of G; ::_thesis: AcyclicPaths p c= AcyclicPaths G let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in AcyclicPaths p or e in AcyclicPaths G ) assume e in AcyclicPaths p ; ::_thesis: e in AcyclicPaths G then ex q being oriented Simple Chain of G st ( e = q & q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) ; hence e in AcyclicPaths G ; ::_thesis: verum end; theorem Th39: :: GRAPH_5:39 for G being Graph for v1, v2 being Element of G holds AcyclicPaths (v1,v2) c= AcyclicPaths G proof let G be Graph; ::_thesis: for v1, v2 being Element of G holds AcyclicPaths (v1,v2) c= AcyclicPaths G let v1, v2 be Element of G; ::_thesis: AcyclicPaths (v1,v2) c= AcyclicPaths G let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in AcyclicPaths (v1,v2) or e in AcyclicPaths G ) assume e in AcyclicPaths (v1,v2) ; ::_thesis: e in AcyclicPaths G then ex q being oriented Simple Chain of G st ( e = q & q is_acyclicpath_of v1,v2 ) ; hence e in AcyclicPaths G ; ::_thesis: verum end; theorem Th40: :: GRAPH_5:40 for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds AcyclicPaths p c= AcyclicPaths (v1,v2) proof let G be Graph; ::_thesis: for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds AcyclicPaths p c= AcyclicPaths (v1,v2) let v1, v2 be Element of G; ::_thesis: for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds AcyclicPaths p c= AcyclicPaths (v1,v2) let p be oriented Chain of G; ::_thesis: ( p is_orientedpath_of v1,v2 implies AcyclicPaths p c= AcyclicPaths (v1,v2) ) assume p is_orientedpath_of v1,v2 ; ::_thesis: AcyclicPaths p c= AcyclicPaths (v1,v2) then A1: ( the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 ) by Def3; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in AcyclicPaths p or x in AcyclicPaths (v1,v2) ) assume x in AcyclicPaths p ; ::_thesis: x in AcyclicPaths (v1,v2) then consider q being oriented Simple Chain of G such that A2: x = q and A3: ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) ) and rng q c= rng p ; q is_orientedpath_of v1,v2 by A1, A3, Def3; then q is_acyclicpath_of v1,v2 by Def6; hence x in AcyclicPaths (v1,v2) by A2; ::_thesis: verum end; theorem Th41: :: GRAPH_5:41 for V being set for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds AcyclicPaths p c= AcyclicPaths (v1,v2,V) proof let V be set ; ::_thesis: for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds AcyclicPaths p c= AcyclicPaths (v1,v2,V) let G be Graph; ::_thesis: for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds AcyclicPaths p c= AcyclicPaths (v1,v2,V) let v1, v2 be Element of G; ::_thesis: for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds AcyclicPaths p c= AcyclicPaths (v1,v2,V) let p be oriented Chain of G; ::_thesis: ( p is_orientedpath_of v1,v2,V implies AcyclicPaths p c= AcyclicPaths (v1,v2,V) ) assume A1: p is_orientedpath_of v1,v2,V ; ::_thesis: AcyclicPaths p c= AcyclicPaths (v1,v2,V) let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in AcyclicPaths p or x in AcyclicPaths (v1,v2,V) ) assume x in AcyclicPaths p ; ::_thesis: x in AcyclicPaths (v1,v2,V) then consider q being oriented Simple Chain of G such that A2: x = q and A3: ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) ) and A4: rng q c= rng p ; (vertices p) \ {v2} c= V by A1, Def4; then A5: (vertices q) \ {v2} c= V by A4, Th22; p is_orientedpath_of v1,v2 by A1, Def4; then ( the Source of G . (p . 1) = v1 & the Target of G . (p . (len p)) = v2 ) by Def3; then q is_orientedpath_of v1,v2 by A3, Def3; then q is_orientedpath_of v1,v2,V by A5, Def4; then q is_acyclicpath_of v1,v2,V by Def7; hence x in AcyclicPaths (v1,v2,V) by A2; ::_thesis: verum end; theorem :: GRAPH_5:42 for G being Graph for q, p being oriented Chain of G st q in AcyclicPaths p holds len q <= len p proof let G be Graph; ::_thesis: for q, p being oriented Chain of G st q in AcyclicPaths p holds len q <= len p let q, p be oriented Chain of G; ::_thesis: ( q in AcyclicPaths p implies len q <= len p ) A1: card (rng p) <= card (dom p) by CARD_2:47; A2: card (dom p) = card (Seg (len p)) by FINSEQ_1:def_3 .= len p by FINSEQ_1:57 ; assume q in AcyclicPaths p ; ::_thesis: len q <= len p then consider x being oriented Simple Chain of G such that A3: q = x and x <> {} and the Source of G . (x . 1) = the Source of G . (p . 1) and the Target of G . (x . (len x)) = the Target of G . (p . (len p)) and A4: rng x c= rng p ; x is V14() by Th17; then A5: card (rng x) = len x by FINSEQ_4:62; card (rng x) <= card (rng p) by A4, NAT_1:43; hence len q <= len p by A3, A5, A1, A2, XXREAL_0:2; ::_thesis: verum end; theorem Th43: :: GRAPH_5:43 for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2) <> {} ) proof let G be Graph; ::_thesis: for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2) <> {} ) let v1, v2 be Element of G; ::_thesis: for p being oriented Chain of G st p is_orientedpath_of v1,v2 holds ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2) <> {} ) let p be oriented Chain of G; ::_thesis: ( p is_orientedpath_of v1,v2 implies ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2) <> {} ) ) defpred S1[ Element of NAT ] means for p being oriented Chain of G for v1, v2 being Element of G st $1 + 1 = len p & p is_orientedpath_of v1,v2 holds AcyclicPaths p <> {} ; set FS = the Source of G; set FT = the Target of G; A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_p_being_oriented_Chain_of_G for_v1,_v2_being_Element_of_G_st_(k_+_1)_+_1_=_len_p_&_p_is_orientedpath_of_v1,v2_holds_ AcyclicPaths_p_<>_{} let p be oriented Chain of G; ::_thesis: for v1, v2 being Element of G st (k + 1) + 1 = len p & p is_orientedpath_of v1,v2 holds AcyclicPaths b3 <> {} let v1, v2 be Element of G; ::_thesis: ( (k + 1) + 1 = len p & p is_orientedpath_of v1,v2 implies AcyclicPaths b1 <> {} ) assume that A3: (k + 1) + 1 = len p and p is_orientedpath_of v1,v2 ; ::_thesis: AcyclicPaths b1 <> {} consider p1, p2 being FinSequence such that A4: len p1 = k + 1 and A5: len p2 = 1 and A6: p = p1 ^ p2 by A3, FINSEQ_2:22; reconsider p1 = p1 as oriented Chain of G by A6, Th11; A7: 1 <= len p1 by A4, NAT_1:11; then 1 in dom p1 by FINSEQ_3:25; then reconsider x = the Source of G . (p1 . 1) as Element of G by FINSEQ_2:11, FUNCT_2:5; A8: p1 . 1 = p . 1 by A6, A7, Lm1; len p1 in dom p1 by A7, FINSEQ_3:25; then reconsider y = the Target of G . (p1 . (len p1)) as Element of G by FINSEQ_2:11, FUNCT_2:5; p1 <> {} by A4; then p1 is_orientedpath_of x,y by Def3; then AcyclicPaths p1 <> {} by A2, A4; then consider r being set such that A9: r in AcyclicPaths p1 by XBOOLE_0:def_1; A10: rng p1 c= rng p by A6, FINSEQ_1:29; A11: rng p2 c= rng p by A6, FINSEQ_1:30; A12: 1 in dom p2 by A5, FINSEQ_3:25; then A13: p . ((len p1) + 1) = p2 . 1 by A6, FINSEQ_1:def_7; consider q being oriented Simple Chain of G such that r = q and A14: q <> {} and A15: the Source of G . (q . 1) = x and A16: the Target of G . (q . (len q)) = y and A17: rng q c= rng p1 by A9; len p1 < len p by A3, A4, NAT_1:13; then A18: the Source of G . (p . ((len p1) + 1)) = the Target of G . (p . (len p1)) by A7, GRAPH_1:def_15 .= the Target of G . (q . (len q)) by A6, A7, A16, Lm1 ; then A19: the Source of G . (p2 . 1) = the Target of G . (q . (len q)) by A6, A12, FINSEQ_1:def_7; percases ( ex k being Element of NAT st ( 1 <= k & k <= len q & the Target of G . (q . k) = the Target of G . (p2 . 1) ) or for k being Element of NAT holds ( not 1 <= k or not k <= len q or not the Target of G . (q . k) = the Target of G . (p2 . 1) ) ) ; suppose ex k being Element of NAT st ( 1 <= k & k <= len q & the Target of G . (q . k) = the Target of G . (p2 . 1) ) ; ::_thesis: AcyclicPaths b1 <> {} then consider k being Element of NAT such that A20: 1 <= k and A21: k <= len q and A22: the Target of G . (q . k) = the Target of G . (p2 . 1) ; consider i being Nat such that A23: len q = k + i by A21, NAT_1:10; consider q1, q2 being FinSequence such that A24: len q1 = k and len q2 = i and A25: q = q1 ^ q2 by A23, FINSEQ_2:22; reconsider q1 = q1 as oriented Simple Chain of G by A25, Th14; A26: ( q1 <> {} & the Source of G . (q1 . 1) = the Source of G . (p . 1) ) by A8, A15, A20, A24, A25, Lm1; rng q1 c= rng q by A25, FINSEQ_1:29; then rng q1 c= rng p1 by A17, XBOOLE_1:1; then A27: rng q1 c= rng p by A10, XBOOLE_1:1; the Target of G . (q1 . (len q1)) = the Target of G . (p . (len p)) by A3, A4, A13, A20, A22, A24, A25, Lm1; then q1 in { w where w is oriented Simple Chain of G : ( w <> {} & the Source of G . (w . 1) = the Source of G . (p . 1) & the Target of G . (w . (len w)) = the Target of G . (p . (len p)) & rng w c= rng p ) } by A27, A26; hence AcyclicPaths p <> {} ; ::_thesis: verum end; supposeA28: for k being Element of NAT holds ( not 1 <= k or not k <= len q or not the Target of G . (q . k) = the Target of G . (p2 . 1) ) ; ::_thesis: AcyclicPaths b1 <> {} reconsider p2 = p2 as oriented Chain of G by A6, Th11; hereby ::_thesis: verum percases ( the Source of G . (q . 1) <> the Target of G . (q . (len q)) or the Source of G . (q . 1) = the Target of G . (q . (len q)) ) ; supposeA29: the Source of G . (q . 1) <> the Target of G . (q . (len q)) ; ::_thesis: AcyclicPaths p <> {} set qp = q ^ p2; ( rng (q ^ p2) = (rng q) \/ (rng p2) & rng q c= rng p ) by A17, A10, FINSEQ_1:31, XBOOLE_1:1; then A30: rng (q ^ p2) c= (rng p) \/ (rng p) by A11, XBOOLE_1:13; A31: len q >= 1 by A14, FINSEQ_1:20; then A32: the Source of G . ((q ^ p2) . 1) = the Source of G . (p . 1) by A8, A15, Lm1; len (q ^ p2) = (len q) + 1 by A5, FINSEQ_1:22; then A33: ( q ^ p2 <> {} & the Target of G . ((q ^ p2) . (len (q ^ p2))) = the Target of G . (p . (len p)) ) by A3, A4, A5, A13, Lm2; q ^ p2 is oriented Simple Chain of G by A5, A13, A18, A28, A29, A31, Th16; then q ^ p2 in { w where w is oriented Simple Chain of G : ( w <> {} & the Source of G . (w . 1) = the Source of G . (p . 1) & the Target of G . (w . (len w)) = the Target of G . (p . (len p)) & rng w c= rng p ) } by A32, A33, A30; hence AcyclicPaths p <> {} ; ::_thesis: verum end; supposeA34: the Source of G . (q . 1) = the Target of G . (q . (len q)) ; ::_thesis: AcyclicPaths p <> {} reconsider p2 = p2 as oriented Simple Chain of G by A5, Th15; ( p2 <> {} & the Target of G . (p2 . (len p2)) = the Target of G . (p . (len p)) ) by A3, A4, A5, A6, Lm2; then p2 in { w where w is oriented Simple Chain of G : ( w <> {} & the Source of G . (w . 1) = the Source of G . (p . 1) & the Target of G . (w . (len w)) = the Target of G . (p . (len p)) & rng w c= rng p ) } by A8, A15, A11, A19, A34; hence AcyclicPaths p <> {} ; ::_thesis: verum end; end; end; end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A35: S1[ 0 ] proof let p be oriented Chain of G; ::_thesis: for v1, v2 being Element of G st 0 + 1 = len p & p is_orientedpath_of v1,v2 holds AcyclicPaths p <> {} let v1, v2 be Element of G; ::_thesis: ( 0 + 1 = len p & p is_orientedpath_of v1,v2 implies AcyclicPaths p <> {} ) assume that A36: 0 + 1 = len p and p is_orientedpath_of v1,v2 ; ::_thesis: AcyclicPaths p <> {} reconsider r = p as oriented Simple Chain of G by A36, Th15; r <> {} by A36; then r in { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } ; hence AcyclicPaths p <> {} ; ::_thesis: verum end; A37: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A35, A1); assume A38: p is_orientedpath_of v1,v2 ; ::_thesis: ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2) <> {} ) then p <> {} by Def3; then len p >= 1 by FINSEQ_1:20; then ((len p) -' 1) + 1 = len p by XREAL_1:235; hence AcyclicPaths p <> {} by A38, A37; ::_thesis: AcyclicPaths (v1,v2) <> {} then A39: ex x being set st x in AcyclicPaths p by XBOOLE_0:def_1; AcyclicPaths p c= AcyclicPaths (v1,v2) by A38, Th40; hence AcyclicPaths (v1,v2) <> {} by A39; ::_thesis: verum end; theorem Th44: :: GRAPH_5:44 for V being set for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} ) proof let V be set ; ::_thesis: for G being Graph for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} ) let G be Graph; ::_thesis: for v1, v2 being Element of G for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} ) let v1, v2 be Element of G; ::_thesis: for p being oriented Chain of G st p is_orientedpath_of v1,v2,V holds ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} ) let p be oriented Chain of G; ::_thesis: ( p is_orientedpath_of v1,v2,V implies ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} ) ) defpred S1[ Element of NAT ] means for p being oriented Chain of G for v1, v2 being Element of G st len p <= $1 + 1 & p is_orientedpath_of v1,v2,V holds AcyclicPaths p <> {} ; set FS = the Source of G; set FT = the Target of G; assume A1: p is_orientedpath_of v1,v2,V ; ::_thesis: ( AcyclicPaths p <> {} & AcyclicPaths (v1,v2,V) <> {} ) then p is_orientedpath_of v1,v2 by Def4; then p <> {} by Def3; then len p >= 1 by FINSEQ_1:20; then A2: ((len p) -' 1) + 1 = len p by XREAL_1:235; A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_p_being_oriented_Chain_of_G for_v1,_v2_being_Element_of_G_st_len_p_<=_(k_+_1)_+_1_&_p_is_orientedpath_of_v1,v2,V_holds_ AcyclicPaths_p_<>_{} let p be oriented Chain of G; ::_thesis: for v1, v2 being Element of G st len p <= (k + 1) + 1 & p is_orientedpath_of v1,v2,V holds AcyclicPaths b3 <> {} let v1, v2 be Element of G; ::_thesis: ( len p <= (k + 1) + 1 & p is_orientedpath_of v1,v2,V implies AcyclicPaths b1 <> {} ) assume that A5: len p <= (k + 1) + 1 and A6: p is_orientedpath_of v1,v2,V ; ::_thesis: AcyclicPaths b1 <> {} consider vs being FinSequence of the carrier of G such that A7: vs is_oriented_vertex_seq_of p by GRAPH_4:9; A8: (vertices p) \ {v2} c= V by A6, Def4; A9: len vs = (len p) + 1 by A7, GRAPH_4:def_5; then A10: len vs >= 1 by NAT_1:12; A11: p is_orientedpath_of v1,v2 by A6, Def4; then A12: p <> {} by Def3; then A13: len p >= 1 by FINSEQ_1:20; then p . (len p) orientedly_joins vs /. (len p),vs /. ((len p) + 1) by A7, GRAPH_4:def_5; then the Target of G . (p . (len p)) = vs /. ((len p) + 1) by GRAPH_4:def_1; then A14: the Target of G . (p . (len p)) = vs . (len vs) by A9, A10, FINSEQ_4:15; percases ( 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 ) or ex n, m being Element of NAT st ( 1 <= n & n < m & m <= len vs & vs . n = vs . m & not ( n = 1 & m = len vs ) ) ) ; suppose 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 ) ; ::_thesis: AcyclicPaths b1 <> {} then p is Simple by A7, GRAPH_4:def_7; then p in { w where w is oriented Simple Chain of G : ( w <> {} & the Source of G . (w . 1) = the Source of G . (p . 1) & the Target of G . (w . (len w)) = the Target of G . (p . (len p)) & rng w c= rng p ) } by A12; hence AcyclicPaths p <> {} ; ::_thesis: verum end; suppose ex n, m being Element of NAT st ( 1 <= n & n < m & m <= len vs & vs . n = vs . m & not ( n = 1 & m = len vs ) ) ; ::_thesis: AcyclicPaths b1 <> {} then consider n, m being Element of NAT such that A15: 1 <= n and A16: n < m and A17: m <= len vs and A18: vs . n = vs . m and A19: ( not n = 1 or not m = len vs ) ; consider i being Nat such that A20: m = 1 + i by A15, A16, NAT_1:10, XXREAL_0:2; reconsider i = i as Element of NAT by ORDINAL1:def_12; A21: m >= 1 by A15, A16, XXREAL_0:2; hereby ::_thesis: verum percases ( n = 1 or n <> 1 ) ; supposeA22: n = 1 ; ::_thesis: AcyclicPaths p <> {} then m < len vs by A17, A19, XXREAL_0:1; then A23: m <= len p by A9, NAT_1:13; then consider j being Nat such that A24: len p = m + j by NAT_1:10; A25: p . 1 orientedly_joins vs /. 1,vs /. (1 + 1) by A7, A13, GRAPH_4:def_5; A26: n <= len vs by A16, A17, XXREAL_0:2; p . m orientedly_joins vs /. m,vs /. (m + 1) by A7, A16, A22, A23, GRAPH_4:def_5; then A27: the Source of G . (p . m) = vs /. m by GRAPH_4:def_1 .= vs . m by A16, A17, A22, FINSEQ_4:15 .= vs /. n by A15, A18, A26, FINSEQ_4:15 .= the Source of G . (p . 1) by A22, A25, GRAPH_4:def_1 .= v1 by A11, Def3 ; reconsider j = j as Element of NAT by ORDINAL1:def_12; A28: len p = i + (1 + j) by A20, A24; then consider p1, p2 being FinSequence such that A29: len p1 = i and A30: len p2 = 1 + j and A31: p = p1 ^ p2 by FINSEQ_2:22; A32: 1 <= len p2 by A30, NAT_1:11; then A33: p2 . 1 = p . m by A20, A29, A31, Lm2; p2 . (len p2) = p . (len p) by A28, A29, A30, A31, A32, Lm2; then A34: the Target of G . (p2 . (len p2)) = v2 by A11, Def3; reconsider p1 = p1, p2 = p2 as oriented Chain of G by A31, Th11; (i + 1) + (- 1) > 1 + (- 1) by A16, A20, A22, XREAL_1:8; then len p2 < len p by A28, A30, XREAL_1:29; then len p2 < (k + 1) + 1 by A5, XXREAL_0:2; then A35: len p2 <= k + 1 by NAT_1:13; (vertices (p1 ^ p2)) \ {v2} c= V by A6, A31, Def4; then A36: (vertices p2) \ {v2} c= V by Th23; p2 <> {} by A30; then p2 is_orientedpath_of v1,v2 by A27, A33, A34, Def3; then p2 is_orientedpath_of v1,v2,V by A36, Def4; then AcyclicPaths p2 <> {} by A4, A35; then consider r being set such that A37: r in AcyclicPaths p2 by XBOOLE_0:def_1; consider q being oriented Simple Chain of G such that r = q and A38: q <> {} and A39: ( the Source of G . (q . 1) = v1 & the Target of G . (q . (len q)) = v2 ) and A40: rng q c= rng p2 by A27, A33, A34, A37; rng p2 c= rng p by A31, FINSEQ_1:30; then A41: rng q c= rng p by A40, XBOOLE_1:1; ( the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) ) by A11, A39, Def3; then q in { w where w is oriented Simple Chain of G : ( w <> {} & the Source of G . (w . 1) = the Source of G . (p . 1) & the Target of G . (w . (len w)) = the Target of G . (p . (len p)) & rng w c= rng p ) } by A38, A41; hence AcyclicPaths p <> {} ; ::_thesis: verum end; supposeA42: n <> 1 ; ::_thesis: AcyclicPaths p <> {} consider n1 being Nat such that A43: n = 1 + n1 by A15, NAT_1:10; reconsider n1 = n1 as Element of NAT by ORDINAL1:def_12; A44: n < len vs by A16, A17, XXREAL_0:2; then A45: n1 < len p by A9, A43, XREAL_1:7; then consider j being Nat such that A46: len p = n1 + j by NAT_1:10; reconsider j = j as Element of NAT by ORDINAL1:def_12; consider p1, p2 being FinSequence such that A47: len p1 = n1 and len p2 = j and A48: p = p1 ^ p2 by A46, FINSEQ_2:22; A49: n > 1 by A15, A42, XXREAL_0:1; then A50: n1 >= 1 by A43, NAT_1:13; then A51: p1 . (len p1) = p . n1 by A47, A48, Lm1; p1 . 1 = p . 1 by A47, A48, A50, Lm1; then A52: the Source of G . (p1 . 1) = v1 by A11, Def3; A53: rng p1 c= rng p by A48, FINSEQ_1:29; reconsider p1 = p1, p2 = p2 as oriented Chain of G by A48, Th11; p . n1 orientedly_joins vs /. n1,vs /. (n1 + 1) by A7, A45, A50, GRAPH_4:def_5; then A54: the Target of G . (p . n1) = vs /. n by A43, GRAPH_4:def_1 .= vs . n by A15, A44, FINSEQ_4:15 ; hereby ::_thesis: verum percases ( m = len vs or m <> len vs ) ; suppose m = len vs ; ::_thesis: AcyclicPaths p <> {} then A55: the Target of G . (p1 . (len p1)) = v2 by A11, A14, A18, A54, A51, Def3; (vertices (p1 ^ p2)) \ {v2} c= V by A6, A48, Def4; then A56: (vertices p1) \ {v2} c= V by Th23; n1 < (k + 1) + 1 by A5, A45, XXREAL_0:2; then A57: len p1 <= k + 1 by A47, NAT_1:13; p1 <> {} by A49, A43, A47, NAT_1:13; then p1 is_orientedpath_of v1,v2 by A52, A55, Def3; then p1 is_orientedpath_of v1,v2,V by A56, Def4; then AcyclicPaths p1 <> {} by A4, A57; then consider r being set such that A58: r in AcyclicPaths p1 by XBOOLE_0:def_1; consider q being oriented Simple Chain of G such that r = q and A59: q <> {} and A60: the Source of G . (q . 1) = v1 and A61: the Target of G . (q . (len q)) = v2 and A62: rng q c= rng p1 by A52, A55, A58; A63: the Target of G . (q . (len q)) = the Target of G . (p . (len p)) by A11, A61, Def3; ( rng q c= rng p & the Source of G . (q . 1) = the Source of G . (p . 1) ) by A11, A53, A60, A62, Def3, XBOOLE_1:1; then q in { w where w is oriented Simple Chain of G : ( w <> {} & the Source of G . (w . 1) = the Source of G . (p . 1) & the Target of G . (w . (len w)) = the Target of G . (p . (len p)) & rng w c= rng p ) } by A59, A63; hence AcyclicPaths p <> {} ; ::_thesis: verum end; suppose m <> len vs ; ::_thesis: AcyclicPaths p <> {} then m < len vs by A17, XXREAL_0:1; then A64: m <= len p by A9, NAT_1:13; then consider h being Nat such that A65: len p = m + h by NAT_1:10; p . m orientedly_joins vs /. m,vs /. (m + 1) by A7, A21, A64, GRAPH_4:def_5; then A66: the Source of G . (p . m) = vs /. m by GRAPH_4:def_1 .= the Target of G . (p1 . (len p1)) by A17, A18, A21, A54, A51, FINSEQ_4:15 ; reconsider h = h as Element of NAT by ORDINAL1:def_12; A67: len p = i + (1 + h) by A20, A65; then consider q1, q2 being FinSequence such that A68: len q1 = i and A69: len q2 = 1 + h and A70: p = q1 ^ q2 by FINSEQ_2:22; reconsider q2 = q2 as oriented Chain of G by A70, Th11; A71: 1 <= len q2 by A69, NAT_1:12; then q2 . 1 = p . m by A20, A68, A70, Lm2; then reconsider pq = p1 ^ q2 as oriented Chain of G by A66, Th12; pq . (len pq) = pq . ((len p1) + (len q2)) by FINSEQ_1:22 .= q2 . (len q2) by A71, Lm2 .= p . (len p) by A67, A68, A69, A70, A71, Lm2 ; then A72: the Target of G . (pq . (len pq)) = v2 by A11, Def3; A73: rng pq = (rng p1) \/ (rng q2) by FINSEQ_1:31; rng q2 c= rng p by A70, FINSEQ_1:30; then A74: rng pq c= rng p by A53, A73, XBOOLE_1:8; then A75: (vertices pq) \ {v2} c= V by A8, Th22; A76: len pq = n1 + (1 + h) by A47, A69, FINSEQ_1:22; m + h > n + h by A16, XREAL_1:8; then len pq < (k + 1) + 1 by A5, A43, A65, A76, XXREAL_0:2; then A77: len pq <= k + 1 by NAT_1:13; A78: the Source of G . (pq . 1) = v1 by A47, A50, A52, Lm1; pq <> {} by A76; then pq is_orientedpath_of v1,v2 by A78, A72, Def3; then pq is_orientedpath_of v1,v2,V by A75, Def4; then AcyclicPaths pq <> {} by A4, A77; then consider r being set such that A79: r in AcyclicPaths pq by XBOOLE_0:def_1; consider q being oriented Simple Chain of G such that r = q and A80: q <> {} and A81: ( the Source of G . (q . 1) = v1 & the Target of G . (q . (len q)) = v2 ) and A82: rng q c= rng pq by A78, A72, A79; A83: rng q c= rng p by A74, A82, XBOOLE_1:1; ( the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) ) by A11, A81, Def3; then q in { w where w is oriented Simple Chain of G : ( w <> {} & the Source of G . (w . 1) = the Source of G . (p . 1) & the Target of G . (w . (len w)) = the Target of G . (p . (len p)) & rng w c= rng p ) } by A80, A83; hence AcyclicPaths p <> {} ; ::_thesis: verum end; end; end; end; end; end; end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A84: S1[ 0 ] proof let p be oriented Chain of G; ::_thesis: for v1, v2 being Element of G st len p <= 0 + 1 & p is_orientedpath_of v1,v2,V holds AcyclicPaths p <> {} let v1, v2 be Element of G; ::_thesis: ( len p <= 0 + 1 & p is_orientedpath_of v1,v2,V implies AcyclicPaths p <> {} ) assume that A85: len p <= 0 + 1 and A86: p is_orientedpath_of v1,v2,V ; ::_thesis: AcyclicPaths p <> {} p is_orientedpath_of v1,v2 by A86, Def4; then A87: p <> {} by Def3; then len p >= 1 by FINSEQ_1:20; then reconsider r = p as oriented Simple Chain of G by A85, Th15, XXREAL_0:1; r in { q where q is oriented Simple Chain of G : ( q <> {} & the Source of G . (q . 1) = the Source of G . (p . 1) & the Target of G . (q . (len q)) = the Target of G . (p . (len p)) & rng q c= rng p ) } by A87; hence AcyclicPaths p <> {} ; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A84, A3); hence AcyclicPaths p <> {} by A1, A2; ::_thesis: AcyclicPaths (v1,v2,V) <> {} then A88: ex x being set st x in AcyclicPaths p by XBOOLE_0:def_1; AcyclicPaths p c= AcyclicPaths (v1,v2,V) by A1, Th41; hence AcyclicPaths (v1,v2,V) <> {} by A88; ::_thesis: verum end; theorem Th45: :: GRAPH_5:45 for V being set for G being Graph for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) c= AcyclicPaths G proof let V be set ; ::_thesis: for G being Graph for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) c= AcyclicPaths G let G be Graph; ::_thesis: for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) c= AcyclicPaths G let v1, v2 be Element of G; ::_thesis: AcyclicPaths (v1,v2,V) c= AcyclicPaths G let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in AcyclicPaths (v1,v2,V) or e in AcyclicPaths G ) assume e in AcyclicPaths (v1,v2,V) ; ::_thesis: e in AcyclicPaths G then ex q being oriented Simple Chain of G st ( e = q & q is_acyclicpath_of v1,v2,V ) ; hence e in AcyclicPaths G ; ::_thesis: verum end; begin notation synonym Real>=0 for REAL+ ; end; definition :: original: Real>=0 redefine func Real>=0 -> Subset of REAL equals :: GRAPH_5:def 12 { r where r is Real : r >= 0 } ; compatibility for b1 being Subset of REAL holds ( b1 = Real>=0 iff b1 = { r where r is Real : r >= 0 } ) by REAL_1:1; coherence Real>=0 is Subset of REAL by ARYTM_0:1; end; :: deftheorem defines Real>=0 GRAPH_5:def_12_:_ Real>=0 = { r where r is Real : r >= 0 } ; registration cluster Real>=0 -> non empty ; coherence not Real>=0 is empty ; end; definition let G be Graph; let W be Function; predW is_weight>=0of G means :Def13: :: GRAPH_5:def 13 W is Function of the carrier' of G,Real>=0; end; :: deftheorem Def13 defines is_weight>=0of GRAPH_5:def_13_:_ for G being Graph for W being Function holds ( W is_weight>=0of G iff W is Function of the carrier' of G,Real>=0 ); definition let G be Graph; let W be Function; predW is_weight_of G means :Def14: :: GRAPH_5:def 14 W is Function of the carrier' of G,REAL; end; :: deftheorem Def14 defines is_weight_of GRAPH_5:def_14_:_ for G being Graph for W being Function holds ( W is_weight_of G iff W is Function of the carrier' of G,REAL ); definition let G be Graph; let p be FinSequence of the carrier' of G; let W be Function; assume A1: W is_weight_of G ; func RealSequence (p,W) -> FinSequence of REAL means :Def15: :: GRAPH_5:def 15 ( dom p = dom it & ( for i being Element of NAT st i in dom p holds it . i = W . (p . i) ) ); existence ex b1 being FinSequence of REAL st ( dom p = dom b1 & ( for i being Element of NAT st i in dom p holds b1 . i = W . (p . i) ) ) proof deffunc H1( set ) -> set = W . (p . $1); consider f being Function such that A2: ( dom f = dom p & ( for x being set st x in dom p holds f . x = H1(x) ) ) from FUNCT_1:sch_3(); A3: now__::_thesis:_for_i_being_Nat_st_i_in_dom_f_holds_ f_._i_in_REAL let i be Nat; ::_thesis: ( i in dom f implies f . i in REAL ) A4: W is Function of the carrier' of G,REAL by A1, Def14; assume A5: i in dom f ; ::_thesis: f . i in REAL then f . i = W . (p . i) by A2; hence f . i in REAL by A2, A5, A4, FINSEQ_2:11, FUNCT_2:5; ::_thesis: verum end; dom f = Seg (len p) by A2, FINSEQ_1:def_3; then f is FinSequence by FINSEQ_1:def_2; then reconsider g = f as FinSequence of REAL by A3, FINSEQ_2:12; take g ; ::_thesis: ( dom p = dom g & ( for i being Element of NAT st i in dom p holds g . i = W . (p . i) ) ) thus dom p = dom g by A2; ::_thesis: for i being Element of NAT st i in dom p holds g . i = W . (p . i) let i be Element of NAT ; ::_thesis: ( i in dom p implies g . i = W . (p . i) ) assume i in dom p ; ::_thesis: g . i = W . (p . i) hence g . i = W . (p . i) by A2; ::_thesis: verum end; uniqueness for b1, b2 being FinSequence of REAL st dom p = dom b1 & ( for i being Element of NAT st i in dom p holds b1 . i = W . (p . i) ) & dom p = dom b2 & ( for i being Element of NAT st i in dom p holds b2 . i = W . (p . i) ) holds b1 = b2 proof let f1, f2 be FinSequence of REAL ; ::_thesis: ( dom p = dom f1 & ( for i being Element of NAT st i in dom p holds f1 . i = W . (p . i) ) & dom p = dom f2 & ( for i being Element of NAT st i in dom p holds f2 . i = W . (p . i) ) implies f1 = f2 ) assume that A6: dom p = dom f1 and A7: for i being Element of NAT st i in dom p holds f1 . i = W . (p . i) ; ::_thesis: ( not dom p = dom f2 or ex i being Element of NAT st ( i in dom p & not f2 . i = W . (p . i) ) or f1 = f2 ) assume that A8: dom p = dom f2 and A9: for i being Element of NAT st i in dom p holds f2 . i = W . (p . i) ; ::_thesis: f1 = f2 now__::_thesis:_for_i_being_Nat_st_i_in_dom_f1_holds_ f1_._i_=_f2_._i let i be Nat; ::_thesis: ( i in dom f1 implies f1 . i = f2 . i ) assume A10: i in dom f1 ; ::_thesis: f1 . i = f2 . i hence f1 . i = W . (p . i) by A6, A7 .= f2 . i by A6, A9, A10 ; ::_thesis: verum end; hence f1 = f2 by A6, A8, FINSEQ_1:13; ::_thesis: verum end; end; :: deftheorem Def15 defines RealSequence GRAPH_5:def_15_:_ for G being Graph for p being FinSequence of the carrier' of G for W being Function st W is_weight_of G holds for b4 being FinSequence of REAL holds ( b4 = RealSequence (p,W) iff ( dom p = dom b4 & ( for i being Element of NAT st i in dom p holds b4 . i = W . (p . i) ) ) ); definition let G be Graph; let p be FinSequence of the carrier' of G; let W be Function; func cost (p,W) -> Real equals :: GRAPH_5:def 16 Sum (RealSequence (p,W)); coherence Sum (RealSequence (p,W)) is Real ; end; :: deftheorem defines cost GRAPH_5:def_16_:_ for G being Graph for p being FinSequence of the carrier' of G for W being Function holds cost (p,W) = Sum (RealSequence (p,W)); theorem Th46: :: GRAPH_5:46 for W being Function for G being Graph st W is_weight>=0of G holds W is_weight_of G proof let W be Function; ::_thesis: for G being Graph st W is_weight>=0of G holds W is_weight_of G let G be Graph; ::_thesis: ( W is_weight>=0of G implies W is_weight_of G ) assume W is_weight>=0of G ; ::_thesis: W is_weight_of G then W is Function of the carrier' of G,Real>=0 by Def13; then W is Function of the carrier' of G,REAL by FUNCT_2:7; hence W is_weight_of G by Def14; ::_thesis: verum end; theorem Th47: :: GRAPH_5:47 for W being Function for G being Graph for pe being FinSequence of the carrier' of G for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence (pe,W) holds for i being Element of NAT st i in dom f holds f . i >= 0 proof let W be Function; ::_thesis: for G being Graph for pe being FinSequence of the carrier' of G for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence (pe,W) holds for i being Element of NAT st i in dom f holds f . i >= 0 let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence (pe,W) holds for i being Element of NAT st i in dom f holds f . i >= 0 let pe be FinSequence of the carrier' of G; ::_thesis: for f being FinSequence of REAL st W is_weight>=0of G & f = RealSequence (pe,W) holds for i being Element of NAT st i in dom f holds f . i >= 0 let f be FinSequence of REAL ; ::_thesis: ( W is_weight>=0of G & f = RealSequence (pe,W) implies for i being Element of NAT st i in dom f holds f . i >= 0 ) assume that A1: W is_weight>=0of G and A2: f = RealSequence (pe,W) ; ::_thesis: for i being Element of NAT st i in dom f holds f . i >= 0 A3: W is Function of the carrier' of G,Real>=0 by A1, Def13; let i be Element of NAT ; ::_thesis: ( i in dom f implies f . i >= 0 ) assume A4: i in dom f ; ::_thesis: f . i >= 0 A5: W is_weight_of G by A1, Th46; then A6: dom pe = dom f by A2, Def15; then f . i = W . (pe . i) by A2, A5, A4, Def15; then f . i in Real>=0 by A6, A3, A4, FINSEQ_2:11, FUNCT_2:5; then ex r being Real st ( f . i = r & r >= 0 ) ; hence f . i >= 0 ; ::_thesis: verum end; theorem Th48: :: GRAPH_5:48 for i being Element of NAT for W being Function for G being Graph for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & W is_weight_of G & i in dom qe holds ex j being Element of NAT st ( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i ) proof let i be Element of NAT ; ::_thesis: for W being Function for G being Graph for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & W is_weight_of G & i in dom qe holds ex j being Element of NAT st ( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i ) let W be Function; ::_thesis: for G being Graph for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & W is_weight_of G & i in dom qe holds ex j being Element of NAT st ( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i ) let G be Graph; ::_thesis: for qe, pe being FinSequence of the carrier' of G st rng qe c= rng pe & W is_weight_of G & i in dom qe holds ex j being Element of NAT st ( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i ) let qe, pe be FinSequence of the carrier' of G; ::_thesis: ( rng qe c= rng pe & W is_weight_of G & i in dom qe implies ex j being Element of NAT st ( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i ) ) assume that A1: rng qe c= rng pe and A2: W is_weight_of G and A3: i in dom qe ; ::_thesis: ex j being Element of NAT st ( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i ) set g = RealSequence (qe,W); consider y being set such that A4: y in dom pe and A5: qe . i = pe . y by A1, A3, Th1; reconsider j = y as Element of NAT by A4; take j ; ::_thesis: ( j in dom pe & (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i ) thus j in dom pe by A4; ::_thesis: (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i (RealSequence (qe,W)) . i = W . (qe . i) by A2, A3, Def15; hence (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . i by A2, A4, A5, Def15; ::_thesis: verum end; Lm3: for f being FinSequence of REAL holds ( ( for y being Real st y in rng f holds y >= 0 ) iff for i being Nat st i in dom f holds f . i >= 0 ) proof let f be FinSequence of REAL ; ::_thesis: ( ( for y being Real st y in rng f holds y >= 0 ) iff for i being Nat st i in dom f holds f . i >= 0 ) hereby ::_thesis: ( ( for i being Nat st i in dom f holds f . i >= 0 ) implies for y being Real st y in rng f holds y >= 0 ) assume A1: for y being Real st y in rng f holds y >= 0 ; ::_thesis: for i being Nat st i in dom f holds f . i >= 0 hereby ::_thesis: verum let i be Nat; ::_thesis: ( i in dom f implies f . i >= 0 ) assume i in dom f ; ::_thesis: f . i >= 0 then f . i in rng f by FUNCT_1:def_3; hence f . i >= 0 by A1; ::_thesis: verum end; end; assume A2: for i being Nat st i in dom f holds f . i >= 0 ; ::_thesis: for y being Real st y in rng f holds y >= 0 hereby ::_thesis: verum let x be Real; ::_thesis: ( x in rng f implies x >= 0 ) assume x in rng f ; ::_thesis: x >= 0 then consider y being set such that A3: y in dom f and A4: x = f . y by FUNCT_1:def_3; thus x >= 0 by A2, A3, A4; ::_thesis: verum end; end; Lm4: for p, q, r being FinSequence of REAL st r = p ^ q & ( for x being Real st x in rng r holds x >= 0 ) holds ( ( for i being Element of NAT st i in dom p holds p . i >= 0 ) & ( for i being Element of NAT st i in dom q holds q . i >= 0 ) ) proof let p, q, r be FinSequence of REAL ; ::_thesis: ( r = p ^ q & ( for x being Real st x in rng r holds x >= 0 ) implies ( ( for i being Element of NAT st i in dom p holds p . i >= 0 ) & ( for i being Element of NAT st i in dom q holds q . i >= 0 ) ) ) assume that A1: r = p ^ q and A2: for x being Real st x in rng r holds x >= 0 ; ::_thesis: ( ( for i being Element of NAT st i in dom p holds p . i >= 0 ) & ( for i being Element of NAT st i in dom q holds q . i >= 0 ) ) rng p c= rng r by A1, FINSEQ_1:29; then for y being Real st y in rng p holds y >= 0 by A2; hence for i being Element of NAT st i in dom p holds p . i >= 0 by Lm3; ::_thesis: for i being Element of NAT st i in dom q holds q . i >= 0 rng q c= rng r by A1, FINSEQ_1:30; then for y being Real st y in rng q holds y >= 0 by A2; hence for i being Element of NAT st i in dom q holds q . i >= 0 by Lm3; ::_thesis: verum end; theorem :: GRAPH_5:49 for W being Function for G being Graph for qe, pe being FinSequence of the carrier' of G st len qe = 1 & rng qe c= rng pe & W is_weight>=0of G holds cost (qe,W) <= cost (pe,W) proof let W be Function; ::_thesis: for G being Graph for qe, pe being FinSequence of the carrier' of G st len qe = 1 & rng qe c= rng pe & W is_weight>=0of G holds cost (qe,W) <= cost (pe,W) let G be Graph; ::_thesis: for qe, pe being FinSequence of the carrier' of G st len qe = 1 & rng qe c= rng pe & W is_weight>=0of G holds cost (qe,W) <= cost (pe,W) let qe, pe be FinSequence of the carrier' of G; ::_thesis: ( len qe = 1 & rng qe c= rng pe & W is_weight>=0of G implies cost (qe,W) <= cost (pe,W) ) assume that A1: len qe = 1 and A2: rng qe c= rng pe and A3: W is_weight>=0of G ; ::_thesis: cost (qe,W) <= cost (pe,W) set f = RealSequence (pe,W); set g = RealSequence (qe,W); 1 in dom qe by A1, FINSEQ_3:25; then consider j being Element of NAT such that A4: j in dom pe and A5: (RealSequence (pe,W)) . j = (RealSequence (qe,W)) . 1 by A2, A3, Th46, Th48; A6: W is_weight_of G by A3, Th46; then dom pe = dom (RealSequence (pe,W)) by Def15; then A7: len pe = len (RealSequence (pe,W)) by FINSEQ_3:29; dom (RealSequence (qe,W)) = dom qe by A6, Def15; then len (RealSequence (qe,W)) = len qe by FINSEQ_3:29; then RealSequence (qe,W) = <*((RealSequence (qe,W)) . 1)*> by A1, FINSEQ_1:40; then A8: cost (qe,W) = (RealSequence (qe,W)) . 1 by FINSOP_1:11; j <= len pe by A4, FINSEQ_3:25; then consider m being Nat such that A9: len (RealSequence (pe,W)) = j + m by A7, NAT_1:10; reconsider m = m as Element of NAT by ORDINAL1:def_12; consider f1, f2 being FinSequence of REAL such that A10: len f1 = j and len f2 = m and A11: RealSequence (pe,W) = f1 ^ f2 by A9, FINSEQ_2:23; A12: 1 <= j by A4, FINSEQ_3:25; then consider h being FinSequence of REAL , d being Real such that A13: f1 = h ^ <*d*> by A10, FINSEQ_2:19; j in dom f1 by A12, A10, FINSEQ_3:25; then A14: f1 . j = (RealSequence (qe,W)) . 1 by A5, A11, FINSEQ_1:def_7; j = (len h) + 1 by A10, A13, FINSEQ_2:16; then A15: d = (RealSequence (qe,W)) . 1 by A13, A14, FINSEQ_1:42; for i being Nat st i in dom (RealSequence (pe,W)) holds (RealSequence (pe,W)) . i >= 0 by A3, Th47; then A16: for y being Real st y in rng (RealSequence (pe,W)) holds y >= 0 by Lm3; then for i being Nat st i in dom f2 holds f2 . i >= 0 by A11, Lm4; then A17: Sum f2 >= 0 by RVSUM_1:84; for i being Nat st i in dom f1 holds f1 . i >= 0 by A11, A16, Lm4; then for y being Real st y in rng f1 holds y >= 0 by Lm3; then for i being Nat st i in dom h holds h . i >= 0 by A13, Lm4; then A18: Sum h >= 0 by RVSUM_1:84; Sum f1 = (Sum h) + (Sum <*d*>) by A13, RVSUM_1:75 .= (Sum h) + ((RealSequence (qe,W)) . 1) by A15, FINSOP_1:11 ; then A19: Sum f1 >= 0 + ((RealSequence (qe,W)) . 1) by A18, XREAL_1:7; Sum (RealSequence (pe,W)) = (Sum f1) + (Sum f2) by A11, RVSUM_1:75; hence cost (qe,W) <= cost (pe,W) by A8, A17, A19, XREAL_1:7; ::_thesis: verum end; theorem Th50: :: GRAPH_5:50 for W being Function for G being Graph for pe being FinSequence of the carrier' of G st W is_weight>=0of G holds cost (pe,W) >= 0 proof let W be Function; ::_thesis: for G being Graph for pe being FinSequence of the carrier' of G st W is_weight>=0of G holds cost (pe,W) >= 0 let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G st W is_weight>=0of G holds cost (pe,W) >= 0 let pe be FinSequence of the carrier' of G; ::_thesis: ( W is_weight>=0of G implies cost (pe,W) >= 0 ) set f = RealSequence (pe,W); assume W is_weight>=0of G ; ::_thesis: cost (pe,W) >= 0 then for i being Nat st i in dom (RealSequence (pe,W)) holds (RealSequence (pe,W)) . i >= 0 by Th47; hence cost (pe,W) >= 0 by RVSUM_1:84; ::_thesis: verum end; theorem Th51: :: GRAPH_5:51 for W being Function for G being Graph for pe being FinSequence of the carrier' of G st pe = {} & W is_weight_of G holds cost (pe,W) = 0 proof let W be Function; ::_thesis: for G being Graph for pe being FinSequence of the carrier' of G st pe = {} & W is_weight_of G holds cost (pe,W) = 0 let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G st pe = {} & W is_weight_of G holds cost (pe,W) = 0 let pe be FinSequence of the carrier' of G; ::_thesis: ( pe = {} & W is_weight_of G implies cost (pe,W) = 0 ) assume that A1: pe = {} and A2: W is_weight_of G ; ::_thesis: cost (pe,W) = 0 set f = RealSequence (pe,W); dom (RealSequence (pe,W)) = dom pe by A2, Def15; then len (RealSequence (pe,W)) = len pe by FINSEQ_3:29 .= 0 by A1 ; then RealSequence (pe,W) = <*> REAL ; hence cost (pe,W) = 0 by RVSUM_1:72; ::_thesis: verum end; theorem Th52: :: GRAPH_5:52 for W being Function for G being Graph for v1, v2 being Element of G for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2) holds ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) proof let W be Function; ::_thesis: for G being Graph for v1, v2 being Element of G for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2) holds ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) let G be Graph; ::_thesis: for v1, v2 being Element of G for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2) holds ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) let v1, v2 be Element of G; ::_thesis: for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2) holds ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) let D be non empty finite Subset of ( the carrier' of G *); ::_thesis: ( D = AcyclicPaths (v1,v2) implies ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) ) deffunc H1( Element of D) -> Real = cost ($1,W); consider x being Element of D such that A1: for y being Element of D holds H1(x) <= H1(y) from GRAPH_5:sch_2(); assume D = AcyclicPaths (v1,v2) ; ::_thesis: ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) then x in AcyclicPaths (v1,v2) ; then consider p being oriented Simple Chain of G such that A2: x = p and p is_acyclicpath_of v1,v2 ; take p ; ::_thesis: ( p in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (p,W) <= cost (qe,W) ) ) thus p in D by A2; ::_thesis: for qe being FinSequence of the carrier' of G st qe in D holds cost (p,W) <= cost (qe,W) let pe be FinSequence of the carrier' of G; ::_thesis: ( pe in D implies cost (p,W) <= cost (pe,W) ) assume pe in D ; ::_thesis: cost (p,W) <= cost (pe,W) then reconsider y = pe as Element of D ; H1(x) <= H1(y) by A1; hence cost (p,W) <= cost (pe,W) by A2; ::_thesis: verum end; theorem Th53: :: GRAPH_5:53 for V being set for W being Function for G being Graph for v1, v2 being Element of G for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) holds ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) proof let V be set ; ::_thesis: for W being Function for G being Graph for v1, v2 being Element of G for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) holds ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) let W be Function; ::_thesis: for G being Graph for v1, v2 being Element of G for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) holds ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) let G be Graph; ::_thesis: for v1, v2 being Element of G for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) holds ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) let v1, v2 be Element of G; ::_thesis: for D being non empty finite Subset of ( the carrier' of G *) st D = AcyclicPaths (v1,v2,V) holds ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) let D be non empty finite Subset of ( the carrier' of G *); ::_thesis: ( D = AcyclicPaths (v1,v2,V) implies ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) ) deffunc H1( Element of D) -> Real = cost ($1,W); consider x being Element of D such that A1: for y being Element of D holds H1(x) <= H1(y) from GRAPH_5:sch_2(); assume D = AcyclicPaths (v1,v2,V) ; ::_thesis: ex pe being FinSequence of the carrier' of G st ( pe in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (pe,W) <= cost (qe,W) ) ) then x in AcyclicPaths (v1,v2,V) ; then consider p being oriented Simple Chain of G such that A2: x = p and p is_acyclicpath_of v1,v2,V ; take p ; ::_thesis: ( p in D & ( for qe being FinSequence of the carrier' of G st qe in D holds cost (p,W) <= cost (qe,W) ) ) thus p in D by A2; ::_thesis: for qe being FinSequence of the carrier' of G st qe in D holds cost (p,W) <= cost (qe,W) let pe be FinSequence of the carrier' of G; ::_thesis: ( pe in D implies cost (p,W) <= cost (pe,W) ) assume pe in D ; ::_thesis: cost (p,W) <= cost (pe,W) then reconsider y = pe as Element of D ; H1(x) <= H1(y) by A1; hence cost (p,W) <= cost (pe,W) by A2; ::_thesis: verum end; theorem Th54: :: GRAPH_5:54 for W being Function for G being Graph for pe, qe being FinSequence of the carrier' of G st W is_weight_of G holds cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W)) proof let W be Function; ::_thesis: for G being Graph for pe, qe being FinSequence of the carrier' of G st W is_weight_of G holds cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W)) let G be Graph; ::_thesis: for pe, qe being FinSequence of the carrier' of G st W is_weight_of G holds cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W)) let pe, qe be FinSequence of the carrier' of G; ::_thesis: ( W is_weight_of G implies cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W)) ) set r = pe ^ qe; set f = RealSequence ((pe ^ qe),W); set g = RealSequence (pe,W); set h = RealSequence (qe,W); assume A1: W is_weight_of G ; ::_thesis: cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W)) then A2: dom pe = dom (RealSequence (pe,W)) by Def15; then A3: len pe = len (RealSequence (pe,W)) by FINSEQ_3:29; A4: dom qe = dom (RealSequence (qe,W)) by A1, Def15; then A5: len qe = len (RealSequence (qe,W)) by FINSEQ_3:29; A6: dom (pe ^ qe) = dom (RealSequence ((pe ^ qe),W)) by A1, Def15; then len (RealSequence ((pe ^ qe),W)) = len (pe ^ qe) by FINSEQ_3:29; then A7: len (RealSequence ((pe ^ qe),W)) = (len (RealSequence (pe,W))) + (len (RealSequence (qe,W))) by A3, A5, FINSEQ_1:22; A8: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(RealSequence_(qe,W))_holds_ (RealSequence_((pe_^_qe),W))_._((len_(RealSequence_(pe,W)))_+_i)_=_(RealSequence_(qe,W))_._i let i be Element of NAT ; ::_thesis: ( i in dom (RealSequence (qe,W)) implies (RealSequence ((pe ^ qe),W)) . ((len (RealSequence (pe,W))) + i) = (RealSequence (qe,W)) . i ) assume A9: i in dom (RealSequence (qe,W)) ; ::_thesis: (RealSequence ((pe ^ qe),W)) . ((len (RealSequence (pe,W))) + i) = (RealSequence (qe,W)) . i then 1 <= i by FINSEQ_3:25; then A10: 1 <= (len (RealSequence (pe,W))) + i by NAT_1:12; i <= len (RealSequence (qe,W)) by A9, FINSEQ_3:25; then (len (RealSequence (pe,W))) + i <= len (RealSequence ((pe ^ qe),W)) by A7, XREAL_1:7; then A11: (len (RealSequence (pe,W))) + i in dom (RealSequence ((pe ^ qe),W)) by A10, FINSEQ_3:25; ( (RealSequence (qe,W)) . i = W . (qe . i) & (pe ^ qe) . ((len (RealSequence (pe,W))) + i) = qe . i ) by A1, A4, A3, A9, Def15, FINSEQ_1:def_7; hence (RealSequence ((pe ^ qe),W)) . ((len (RealSequence (pe,W))) + i) = (RealSequence (qe,W)) . i by A1, A6, A11, Def15; ::_thesis: verum end; now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(RealSequence_(pe,W))_holds_ (RealSequence_((pe_^_qe),W))_._i_=_(RealSequence_(pe,W))_._i let i be Element of NAT ; ::_thesis: ( i in dom (RealSequence (pe,W)) implies (RealSequence ((pe ^ qe),W)) . i = (RealSequence (pe,W)) . i ) assume A12: i in dom (RealSequence (pe,W)) ; ::_thesis: (RealSequence ((pe ^ qe),W)) . i = (RealSequence (pe,W)) . i then i <= len (RealSequence (pe,W)) by FINSEQ_3:25; then A13: i <= len (RealSequence ((pe ^ qe),W)) by A7, NAT_1:12; 1 <= i by A12, FINSEQ_3:25; then A14: i in dom (RealSequence ((pe ^ qe),W)) by A13, FINSEQ_3:25; ( (RealSequence (pe,W)) . i = W . (pe . i) & (pe ^ qe) . i = pe . i ) by A1, A2, A12, Def15, FINSEQ_1:def_7; hence (RealSequence ((pe ^ qe),W)) . i = (RealSequence (pe,W)) . i by A1, A6, A14, Def15; ::_thesis: verum end; then RealSequence ((pe ^ qe),W) = (RealSequence (pe,W)) ^ (RealSequence (qe,W)) by A7, A8, FINSEQ_3:38; hence cost ((pe ^ qe),W) = (cost (pe,W)) + (cost (qe,W)) by RVSUM_1:75; ::_thesis: verum end; theorem Th55: :: GRAPH_5:55 for W being Function for G being Graph for qe, pe being FinSequence of the carrier' of G st qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G holds cost (qe,W) <= cost (pe,W) proof let W be Function; ::_thesis: for G being Graph for qe, pe being FinSequence of the carrier' of G st qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G holds cost (qe,W) <= cost (pe,W) let G be Graph; ::_thesis: for qe, pe being FinSequence of the carrier' of G st qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G holds cost (qe,W) <= cost (pe,W) let qe, pe be FinSequence of the carrier' of G; ::_thesis: ( qe is one-to-one & rng qe c= rng pe & W is_weight>=0of G implies cost (qe,W) <= cost (pe,W) ) set D = the carrier' of G; assume that A1: ( qe is one-to-one & rng qe c= rng pe ) and A2: W is_weight>=0of G ; ::_thesis: cost (qe,W) <= cost (pe,W) defpred S1[ Nat] means for p, q being FinSequence of the carrier' of G st q is one-to-one & rng q c= rng p & len q = $1 holds cost (q,W) <= cost (p,W); A3: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_p,_q_being_FinSequence_of_the_carrier'_of_G_st_q_is_one-to-one_&_rng_q_c=_rng_p_&_len_q_=_k_+_1_holds_ cost_(q,W)_<=_cost_(p,W) let p, q be FinSequence of the carrier' of G; ::_thesis: ( q is one-to-one & rng q c= rng p & len q = k + 1 implies cost (q,W) <= cost (p,W) ) assume that A5: q is one-to-one and A6: rng q c= rng p and A7: len q = k + 1 ; ::_thesis: cost (q,W) <= cost (p,W) consider q1 being FinSequence, x being set such that A8: q = q1 ^ <*x*> by A7, FINSEQ_2:18; A9: k + 1 = (len q1) + 1 by A7, A8, FINSEQ_2:16; consider p1, p2 being FinSequence such that A10: p = (p1 ^ <*x*>) ^ p2 and A11: rng q1 c= rng (p1 ^ p2) by A5, A6, A8, Th9; reconsider q1 = q1 as FinSequence of the carrier' of G by A8, FINSEQ_1:36; A12: p1 ^ <*x*> is FinSequence of the carrier' of G by A10, FINSEQ_1:36; then reconsider y = <*x*> as FinSequence of the carrier' of G by FINSEQ_1:36; reconsider p2 = p2 as FinSequence of the carrier' of G by A10, FINSEQ_1:36; reconsider p1 = p1 as FinSequence of the carrier' of G by A12, FINSEQ_1:36; q1 is one-to-one by A5, A8, FINSEQ_3:91; then A13: cost (q1,W) <= cost ((p1 ^ p2),W) by A4, A11, A9; A14: cost (q,W) = (cost (q1,W)) + (cost (y,W)) by A2, A8, Th46, Th54; cost (p,W) = (cost ((p1 ^ y),W)) + (cost (p2,W)) by A2, A10, Th46, Th54 .= ((cost (p1,W)) + (cost (y,W))) + (cost (p2,W)) by A2, Th46, Th54 .= ((cost (p1,W)) + (cost (p2,W))) + (cost (y,W)) .= (cost ((p1 ^ p2),W)) + (cost (y,W)) by A2, Th46, Th54 ; hence cost (q,W) <= cost (p,W) by A14, A13, XREAL_1:7; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A15: S1[ 0 ] proof let p, q be FinSequence of the carrier' of G; ::_thesis: ( q is one-to-one & rng q c= rng p & len q = 0 implies cost (q,W) <= cost (p,W) ) assume that q is one-to-one and rng q c= rng p and A16: len q = 0 ; ::_thesis: cost (q,W) <= cost (p,W) q = {} by A16; then cost (q,W) = 0 by A2, Th46, Th51; hence cost (q,W) <= cost (p,W) by A2, Th50; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A15, A3); then S1[ len qe] ; hence cost (qe,W) <= cost (pe,W) by A1; ::_thesis: verum end; theorem Th56: :: GRAPH_5:56 for W being Function for G being Graph for pe being FinSequence of the carrier' of G for p being oriented Chain of G st pe in AcyclicPaths p & W is_weight>=0of G holds cost (pe,W) <= cost (p,W) proof let W be Function; ::_thesis: for G being Graph for pe being FinSequence of the carrier' of G for p being oriented Chain of G st pe in AcyclicPaths p & W is_weight>=0of G holds cost (pe,W) <= cost (p,W) let G be Graph; ::_thesis: for pe being FinSequence of the carrier' of G for p being oriented Chain of G st pe in AcyclicPaths p & W is_weight>=0of G holds cost (pe,W) <= cost (p,W) let pe be FinSequence of the carrier' of G; ::_thesis: for p being oriented Chain of G st pe in AcyclicPaths p & W is_weight>=0of G holds cost (pe,W) <= cost (p,W) let p be oriented Chain of G; ::_thesis: ( pe in AcyclicPaths p & W is_weight>=0of G implies cost (pe,W) <= cost (p,W) ) assume that A1: pe in AcyclicPaths p and A2: W is_weight>=0of G ; ::_thesis: cost (pe,W) <= cost (p,W) A3: ex r being oriented Simple Chain of G st ( r = pe & r <> {} & the Source of G . (r . 1) = the Source of G . (p . 1) & the Target of G . (r . (len r)) = the Target of G . (p . (len p)) & rng r c= rng p ) by A1; then pe is one-to-one by Th17; hence cost (pe,W) <= cost (p,W) by A2, A3, Th55; ::_thesis: verum end; begin definition let G be Graph; let v1, v2 be Vertex of G; let p be oriented Chain of G; let W be Function; predp is_shortestpath_of v1,v2,W means :Def17: :: GRAPH_5:def 17 ( p is_orientedpath_of v1,v2 & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds cost (p,W) <= cost (q,W) ) ); end; :: deftheorem Def17 defines is_shortestpath_of GRAPH_5:def_17_:_ for G being Graph for v1, v2 being Vertex of G for p being oriented Chain of G for W being Function holds ( p is_shortestpath_of v1,v2,W iff ( p is_orientedpath_of v1,v2 & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds cost (p,W) <= cost (q,W) ) ) ); definition let G be Graph; let v1, v2 be Vertex of G; let p be oriented Chain of G; let V be set ; let W be Function; predp is_shortestpath_of v1,v2,V,W means :Def18: :: GRAPH_5:def 18 ( p is_orientedpath_of v1,v2,V & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds cost (p,W) <= cost (q,W) ) ); end; :: deftheorem Def18 defines is_shortestpath_of GRAPH_5:def_18_:_ for G being Graph for v1, v2 being Vertex of G for p being oriented Chain of G for V being set for W being Function holds ( p is_shortestpath_of v1,v2,V,W iff ( p is_orientedpath_of v1,v2,V & ( for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds cost (p,W) <= cost (q,W) ) ) ); begin theorem :: GRAPH_5:57 for G being finite Graph for ps being oriented Simple Chain of G holds len ps <= VerticesCount G proof let G be finite Graph; ::_thesis: for ps being oriented Simple Chain of G holds len ps <= VerticesCount G let ps be oriented Simple Chain of G; ::_thesis: len ps <= VerticesCount G set VV = the carrier of G; consider vs being FinSequence of the carrier of G such that A1: vs is_oriented_vertex_seq_of ps and A2: 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 ) by GRAPH_4:def_7; reconsider V = the carrier of G as finite set ; A3: len vs = (len ps) + 1 by A1, GRAPH_4:def_5; then vs <> {} ; then consider q being FinSequence, x being set such that A4: vs = q ^ <*x*> by FINSEQ_1:46; A5: (len ps) + 1 = (len q) + (len <*x*>) by A3, A4, FINSEQ_1:22 .= (len q) + 1 by FINSEQ_1:39 ; now__::_thesis:_for_n,_m_being_Element_of_NAT_st_1_<=_n_&_n_<_m_&_m_<=_len_q_holds_ not_q_._n_=_q_._m let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len q implies not q . n = q . m ) assume that A6: 1 <= n and A7: n < m and A8: m <= len q ; ::_thesis: not q . n = q . m 1 <= m by A6, A7, XXREAL_0:2; then A9: m in dom q by A8, FINSEQ_3:25; n <= len q by A7, A8, XXREAL_0:2; then n in dom q by A6, FINSEQ_3:25; then A10: vs . n = q . n by A4, FINSEQ_1:def_7; len q < len vs by A3, A5, XREAL_1:29; then A11: m < len vs by A8, XXREAL_0:2; assume q . n = q . m ; ::_thesis: contradiction then vs . m = vs . n by A4, A10, A9, FINSEQ_1:def_7; hence contradiction by A2, A6, A7, A11; ::_thesis: verum end; then A12: card (rng q) = len q by Th7; ( rng vs c= the carrier of G & rng q c= rng vs ) by A4, FINSEQ_1:29, FINSEQ_1:def_4; then card (rng q) <= card V by NAT_1:43, XBOOLE_1:1; hence len ps <= VerticesCount G by A5, A12, GRAPH_1:def_19; ::_thesis: verum end; theorem Th58: :: GRAPH_5:58 for G being finite Graph for ps being oriented Simple Chain of G holds len ps <= EdgesCount G proof let G be finite Graph; ::_thesis: for ps being oriented Simple Chain of G holds len ps <= EdgesCount G let ps be oriented Simple Chain of G; ::_thesis: len ps <= EdgesCount G reconsider V = the carrier' of G as finite set ; rng ps c= the carrier' of G by FINSEQ_1:def_4; then A1: card (rng ps) <= card V by NAT_1:43; ps is V14() by Th17; then card (rng ps) = len ps by FINSEQ_4:62; hence len ps <= EdgesCount G by A1, GRAPH_1:def_20; ::_thesis: verum end; Lm5: for G being finite Graph holds AcyclicPaths G is finite proof let G be finite Graph; ::_thesis: AcyclicPaths G is finite set n = EdgesCount G; set D = the carrier' of G; set A = { x where x is Element of the carrier' of G * : len x <= EdgesCount G } ; A1: AcyclicPaths G c= { x where x is Element of the carrier' of G * : len x <= EdgesCount G } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in AcyclicPaths G or x in { x where x is Element of the carrier' of G * : len x <= EdgesCount G } ) assume x in AcyclicPaths G ; ::_thesis: x in { x where x is Element of the carrier' of G * : len x <= EdgesCount G } then consider p being oriented Simple Chain of G such that A2: x = p ; ( p is Element of the carrier' of G * & len p <= EdgesCount G ) by Th58, FINSEQ_1:def_11; hence x in { x where x is Element of the carrier' of G * : len x <= EdgesCount G } by A2; ::_thesis: verum end; { x where x is Element of the carrier' of G * : len x <= EdgesCount G } is finite by Th3; hence AcyclicPaths G is finite by A1; ::_thesis: verum end; registration let G be finite Graph; cluster AcyclicPaths G -> finite ; coherence AcyclicPaths G is finite by Lm5; end; Lm6: for G being finite Graph for P being oriented Chain of G holds AcyclicPaths P is finite proof let G be finite Graph; ::_thesis: for P being oriented Chain of G holds AcyclicPaths P is finite let P be oriented Chain of G; ::_thesis: AcyclicPaths P is finite AcyclicPaths P c= AcyclicPaths G by Th38; hence AcyclicPaths P is finite ; ::_thesis: verum end; Lm7: for G being finite Graph for v1, v2 being Element of G holds AcyclicPaths (v1,v2) is finite proof let G be finite Graph; ::_thesis: for v1, v2 being Element of G holds AcyclicPaths (v1,v2) is finite let v1, v2 be Element of G; ::_thesis: AcyclicPaths (v1,v2) is finite AcyclicPaths (v1,v2) c= AcyclicPaths G by Th39; hence AcyclicPaths (v1,v2) is finite ; ::_thesis: verum end; Lm8: for V being set for G being finite Graph for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) is finite proof let V be set ; ::_thesis: for G being finite Graph for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) is finite let G be finite Graph; ::_thesis: for v1, v2 being Element of G holds AcyclicPaths (v1,v2,V) is finite let v1, v2 be Element of G; ::_thesis: AcyclicPaths (v1,v2,V) is finite AcyclicPaths (v1,v2,V) c= AcyclicPaths G by Th45; hence AcyclicPaths (v1,v2,V) is finite ; ::_thesis: verum end; registration let G be finite Graph; let P be oriented Chain of G; cluster AcyclicPaths P -> finite ; coherence AcyclicPaths P is finite by Lm6; end; registration let G be finite Graph; let v1, v2 be Element of G; cluster AcyclicPaths (v1,v2) -> finite ; coherence AcyclicPaths (v1,v2) is finite by Lm7; end; registration let G be finite Graph; let v1, v2 be Element of G; let V be set ; cluster AcyclicPaths (v1,v2,V) -> finite ; coherence AcyclicPaths (v1,v2,V) is finite by Lm8; end; theorem :: GRAPH_5:59 for W being Function for G being finite Graph for v1, v2 being Element of G st AcyclicPaths (v1,v2) <> {} holds ex pe being FinSequence of the carrier' of G st ( pe in AcyclicPaths (v1,v2) & ( for qe being FinSequence of the carrier' of G st qe in AcyclicPaths (v1,v2) holds cost (pe,W) <= cost (qe,W) ) ) by Th52; theorem :: GRAPH_5:60 for V being set for W being Function for G being finite Graph for v1, v2 being Element of G st AcyclicPaths (v1,v2,V) <> {} holds ex pe being FinSequence of the carrier' of G st ( pe in AcyclicPaths (v1,v2,V) & ( for qe being FinSequence of the carrier' of G st qe in AcyclicPaths (v1,v2,V) holds cost (pe,W) <= cost (qe,W) ) ) by Th53; theorem :: GRAPH_5:61 for W being Function for G being finite Graph for P being oriented Chain of G for v1, v2 being Element of G st P is_orientedpath_of v1,v2 & W is_weight>=0of G holds ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W proof let W be Function; ::_thesis: for G being finite Graph for P being oriented Chain of G for v1, v2 being Element of G st P is_orientedpath_of v1,v2 & W is_weight>=0of G holds ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W let G be finite Graph; ::_thesis: for P being oriented Chain of G for v1, v2 being Element of G st P is_orientedpath_of v1,v2 & W is_weight>=0of G holds ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W let P be oriented Chain of G; ::_thesis: for v1, v2 being Element of G st P is_orientedpath_of v1,v2 & W is_weight>=0of G holds ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W let v1, v2 be Element of G; ::_thesis: ( P is_orientedpath_of v1,v2 & W is_weight>=0of G implies ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W ) assume that A1: P is_orientedpath_of v1,v2 and A2: W is_weight>=0of G ; ::_thesis: ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,W AcyclicPaths (v1,v2) <> {} by A1, Th43; then consider r being FinSequence of the carrier' of G such that A3: r in AcyclicPaths (v1,v2) and A4: for s being FinSequence of the carrier' of G st s in AcyclicPaths (v1,v2) holds cost (r,W) <= cost (s,W) by Th52; consider t being oriented Simple Chain of G such that A5: r = t and A6: t is_acyclicpath_of v1,v2 by A3; take t ; ::_thesis: t is_shortestpath_of v1,v2,W thus t is_orientedpath_of v1,v2 by A6, Def6; :: according to GRAPH_5:def_17 ::_thesis: for q being oriented Chain of G st q is_orientedpath_of v1,v2 holds cost (t,W) <= cost (q,W) hereby ::_thesis: verum let s be oriented Chain of G; ::_thesis: ( s is_orientedpath_of v1,v2 implies cost (t,W) <= cost (s,W) ) assume A7: s is_orientedpath_of v1,v2 ; ::_thesis: cost (t,W) <= cost (s,W) then consider x being Element of the carrier' of G * such that A8: x in AcyclicPaths s by Th43, SUBSET_1:4; AcyclicPaths s c= AcyclicPaths (v1,v2) by A7, Th40; then A9: cost (r,W) <= cost (x,W) by A4, A8; cost (x,W) <= cost (s,W) by A2, A8, Th56; hence cost (t,W) <= cost (s,W) by A5, A9, XXREAL_0:2; ::_thesis: verum end; end; theorem Th62: :: GRAPH_5:62 for V being set for W being Function for G being finite Graph for P being oriented Chain of G for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W proof let V be set ; ::_thesis: for W being Function for G being finite Graph for P being oriented Chain of G for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W let W be Function; ::_thesis: for G being finite Graph for P being oriented Chain of G for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W let G be finite Graph; ::_thesis: for P being oriented Chain of G for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W let P be oriented Chain of G; ::_thesis: for v1, v2 being Element of G st P is_orientedpath_of v1,v2,V & W is_weight>=0of G holds ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W let v1, v2 be Element of G; ::_thesis: ( P is_orientedpath_of v1,v2,V & W is_weight>=0of G implies ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W ) assume that A1: P is_orientedpath_of v1,v2,V and A2: W is_weight>=0of G ; ::_thesis: ex q being oriented Simple Chain of G st q is_shortestpath_of v1,v2,V,W AcyclicPaths (v1,v2,V) <> {} by A1, Th44; then consider r being FinSequence of the carrier' of G such that A3: r in AcyclicPaths (v1,v2,V) and A4: for s being FinSequence of the carrier' of G st s in AcyclicPaths (v1,v2,V) holds cost (r,W) <= cost (s,W) by Th53; consider t being oriented Simple Chain of G such that A5: r = t and A6: t is_acyclicpath_of v1,v2,V by A3; take t ; ::_thesis: t is_shortestpath_of v1,v2,V,W thus t is_orientedpath_of v1,v2,V by A6, Def7; :: according to GRAPH_5:def_18 ::_thesis: for q being oriented Chain of G st q is_orientedpath_of v1,v2,V holds cost (t,W) <= cost (q,W) hereby ::_thesis: verum let s be oriented Chain of G; ::_thesis: ( s is_orientedpath_of v1,v2,V implies cost (t,W) <= cost (s,W) ) assume A7: s is_orientedpath_of v1,v2,V ; ::_thesis: cost (t,W) <= cost (s,W) then consider x being Element of the carrier' of G * such that A8: x in AcyclicPaths s by Th44, SUBSET_1:4; AcyclicPaths s c= AcyclicPaths (v1,v2,V) by A7, Th41; then A9: cost (r,W) <= cost (x,W) by A4, A8; cost (x,W) <= cost (s,W) by A2, A8, Th56; hence cost (t,W) <= cost (s,W) by A5, A9, XXREAL_0:2; ::_thesis: verum end; end; begin theorem Th63: :: GRAPH_5:63 for V being set for W being Function for G being finite Graph for P being oriented Chain of G for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) holds P is_shortestpath_of v1,v2,W proof let V be set ; ::_thesis: for W being Function for G being finite Graph for P being oriented Chain of G for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) holds P is_shortestpath_of v1,v2,W let W be Function; ::_thesis: for G being finite Graph for P being oriented Chain of G for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) holds P is_shortestpath_of v1,v2,W let G be finite Graph; ::_thesis: for P being oriented Chain of G for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) holds P is_shortestpath_of v1,v2,W let P be oriented Chain of G; ::_thesis: for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) holds P is_shortestpath_of v1,v2,W let v1, v2 be Element of G; ::_thesis: ( W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) implies P is_shortestpath_of v1,v2,W ) assume that A1: W is_weight>=0of G and A2: P is_shortestpath_of v1,v2,V,W and A3: v1 <> v2 and A4: for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ; ::_thesis: P is_shortestpath_of v1,v2,W A5: P is_orientedpath_of v1,v2,V by A2, Def18; then A6: v1 in V by A3, Th31; A7: now__::_thesis:_for_r_being_oriented_Chain_of_G_st_r_is_orientedpath_of_v1,v2_holds_ cost_(P,W)_<=_cost_(r,W) let r be oriented Chain of G; ::_thesis: ( r is_orientedpath_of v1,v2 implies cost (P,W) <= cost (b1,W) ) assume A8: r is_orientedpath_of v1,v2 ; ::_thesis: cost (P,W) <= cost (b1,W) percases ( not vertices r c= V or vertices r c= V ) ; supposeA9: not vertices r c= V ; ::_thesis: cost (P,W) <= cost (b1,W) set FT = the Target of G; set FS = the Source of G; consider i being Element of NAT , s, t being FinSequence of the carrier' of G such that A10: i + 1 <= len r and A11: not vertices (r /. (i + 1)) c= V and A12: len s = i and A13: r = s ^ t and A14: vertices s c= V by A9, Th20; i + 1 <= (len s) + (len t) by A10, A13, FINSEQ_1:22; then A15: 1 <= len t by A12, XREAL_1:6; then consider j being Nat such that A16: len t = 1 + j by NAT_1:10; reconsider s = s, t = t as oriented Chain of G by A13, Th11; reconsider j = j as Element of NAT by ORDINAL1:def_12; consider t1, t2 being FinSequence such that A17: len t1 = 1 and len t2 = j and A18: t = t1 ^ t2 by A16, FINSEQ_2:22; reconsider t1 = t1, t2 = t2 as oriented Chain of G by A18, Th11; A19: r . (i + 1) = t . 1 by A12, A13, A15, Lm2 .= t1 . 1 by A17, A18, Lm1 ; A20: cost (t2,W) >= 0 by A1, Th50; A21: r = (s ^ t1) ^ t2 by A13, A18, FINSEQ_1:32; then cost (r,W) = (cost ((s ^ t1),W)) + (cost (t2,W)) by A1, Th46, Th54; then A22: cost (r,W) >= (cost ((s ^ t1),W)) + 0 by A20, XREAL_1:7; set e = r /. (i + 1); A23: r /. (i + 1) = r . (i + 1) by A10, FINSEQ_4:15, NAT_1:11; consider x being set such that A24: x in vertices (r /. (i + 1)) and A25: not x in V by A11, TARSKI:def_3; A26: ( x = the Source of G . (r /. (i + 1)) or x = the Target of G . (r /. (i + 1)) ) by A24, TARSKI:def_2; 1 in dom t1 by A17, FINSEQ_3:25; then reconsider v3 = x as Vertex of G by A23, A19, A26, FINSEQ_2:11, FUNCT_2:5; A27: v1 = the Source of G . (r . 1) by A8, Def3; hereby ::_thesis: verum percases ( i = 0 or i <> 0 ) ; supposeA28: i = 0 ; ::_thesis: cost (P,W) <= cost (r,W) then A29: the Source of G . (t1 . 1) = v1 by A8, A19, Def3; A30: (vertices t1) \ {v3} c= V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (vertices t1) \ {v3} or x in V ) assume A31: x in (vertices t1) \ {v3} ; ::_thesis: x in V then A32: not x in {v3} by XBOOLE_0:def_5; x in vertices t1 by A31, XBOOLE_0:def_5; then x in vertices (t1 /. 1) by A17, Th25; then A33: ( x = the Source of G . (t1 /. 1) or x = the Target of G . (t1 /. 1) ) by TARSKI:def_2; the Target of G . (t1 /. 1) = v3 by A3, A5, A17, A23, A19, A25, A26, A27, A28, Th31, FINSEQ_4:15; hence x in V by A6, A17, A29, A32, A33, FINSEQ_4:15, TARSKI:def_1; ::_thesis: verum end; A34: t1 <> {} by A17; v1 = the Source of G . (r /. (i + 1)) by A8, A23, A28, Def3; then t1 is_orientedpath_of v1,v3 by A3, A5, A17, A23, A19, A25, A26, A34, Def3, Th31; then A35: t1 is_orientedpath_of v1,v3,V by A30, Def4; then consider q being oriented Simple Chain of G such that A36: q is_shortestpath_of v1,v3,V,W by A1, Th62; s = {} by A12, A28; then A37: s ^ t1 = t1 by FINSEQ_1:34; A38: cost (q,W) <= cost (t1,W) by A35, A36, Def18; cost (P,W) <= cost (q,W) by A4, A25, A36; then cost (P,W) <= cost (t1,W) by A38, XXREAL_0:2; hence cost (P,W) <= cost (r,W) by A22, A37, XXREAL_0:2; ::_thesis: verum end; supposeA39: i <> 0 ; ::_thesis: cost (P,W) <= cost (r,W) reconsider u = s ^ t1 as oriented Chain of G by A21, Th11; A40: i < len r by A10, NAT_1:13; i + 1 > 0 + 1 by A39, XREAL_1:8; then A41: i >= 1 by NAT_1:13; then A42: i in dom s by A12, FINSEQ_3:25; A43: now__::_thesis:_not_the_Source_of_G_._(r_._(i_+_1))_=_v3 assume the Source of G . (r . (i + 1)) = v3 ; ::_thesis: contradiction then A44: v3 = the Target of G . (r . i) by A41, A40, GRAPH_1:def_15; r . i = s . i by A12, A13, A41, Lm1; then v3 in vertices s by A42, A44, Th24; hence contradiction by A14, A25; ::_thesis: verum end; A45: (vertices u) \ {v3} c= V proof set V3 = {( the Target of G . (t1 . 1))}; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (vertices u) \ {v3} or x in V ) assume A46: x in (vertices u) \ {v3} ; ::_thesis: x in V then A47: x in vertices u by XBOOLE_0:def_5; vertices u = (vertices s) \/ {( the Target of G . (t1 . 1))} by A12, A17, A41, Th27; then A48: ( x in vertices s or x in {( the Target of G . (t1 . 1))} ) by A47, XBOOLE_0:def_3; not x in {v3} by A46, XBOOLE_0:def_5; hence x in V by A10, A14, A19, A26, A43, A48, FINSEQ_4:15, NAT_1:11; ::_thesis: verum end; len u = (len s) + (len t1) by FINSEQ_1:22; then A49: ( u <> {} & u . (len u) = t1 . 1 ) by A17, Lm2; u . 1 = s . 1 by A12, A41, Lm1 .= r . 1 by A12, A13, A41, Lm1 ; then the Source of G . (u . 1) = v1 by A8, Def3; then u is_orientedpath_of v1,v3 by A23, A19, A26, A43, A49, Def3; then A50: u is_orientedpath_of v1,v3,V by A45, Def4; then consider q being oriented Simple Chain of G such that A51: q is_shortestpath_of v1,v3,V,W by A1, Th62; A52: cost (q,W) <= cost (u,W) by A50, A51, Def18; cost (P,W) <= cost (q,W) by A4, A25, A51; then cost (P,W) <= cost (u,W) by A52, XXREAL_0:2; hence cost (P,W) <= cost (r,W) by A22, XXREAL_0:2; ::_thesis: verum end; end; end; end; suppose vertices r c= V ; ::_thesis: cost (P,W) <= cost (b1,W) then (vertices r) \ {v2} c= V \ {v2} by XBOOLE_1:33; then (vertices r) \ {v2} c= V by XBOOLE_1:1; then r is_orientedpath_of v1,v2,V by A8, Def4; hence cost (P,W) <= cost (r,W) by A2, Def18; ::_thesis: verum end; end; end; P is_orientedpath_of v1,v2 by A5, Def4; hence P is_shortestpath_of v1,v2,W by A7, Def17; ::_thesis: verum end; theorem :: GRAPH_5:64 for V, U being set for W being Function for G being finite Graph for P being oriented Chain of G for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & V c= U & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) holds P is_shortestpath_of v1,v2,U,W proof let V, U be set ; ::_thesis: for W being Function for G being finite Graph for P being oriented Chain of G for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & V c= U & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) holds P is_shortestpath_of v1,v2,U,W let W be Function; ::_thesis: for G being finite Graph for P being oriented Chain of G for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & V c= U & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) holds P is_shortestpath_of v1,v2,U,W let G be finite Graph; ::_thesis: for P being oriented Chain of G for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & V c= U & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) holds P is_shortestpath_of v1,v2,U,W let P be oriented Chain of G; ::_thesis: for v1, v2 being Element of G st W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & V c= U & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) holds P is_shortestpath_of v1,v2,U,W let v1, v2 be Element of G; ::_thesis: ( W is_weight>=0of G & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & V c= U & ( for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ) implies P is_shortestpath_of v1,v2,U,W ) assume that A1: W is_weight>=0of G and A2: P is_shortestpath_of v1,v2,V,W and A3: v1 <> v2 and A4: V c= U and A5: for Q being oriented Chain of G for v3 being Element of G st not v3 in V & Q is_shortestpath_of v1,v3,V,W holds cost (P,W) <= cost (Q,W) ; ::_thesis: P is_shortestpath_of v1,v2,U,W A6: P is_shortestpath_of v1,v2,W by A1, A2, A3, A5, Th63; A7: now__::_thesis:_for_q_being_oriented_Chain_of_G_st_q_is_orientedpath_of_v1,v2,U_holds_ cost_(P,W)_<=_cost_(q,W) let q be oriented Chain of G; ::_thesis: ( q is_orientedpath_of v1,v2,U implies cost (P,W) <= cost (q,W) ) assume q is_orientedpath_of v1,v2,U ; ::_thesis: cost (P,W) <= cost (q,W) then q is_orientedpath_of v1,v2 by Def4; hence cost (P,W) <= cost (q,W) by A6, Def17; ::_thesis: verum end; P is_orientedpath_of v1,v2,V by A2, Def18; then P is_orientedpath_of v1,v2,U by A4, Th32; hence P is_shortestpath_of v1,v2,U,W by A7, Def18; ::_thesis: verum end; definition let G be Graph; let pe be FinSequence of the carrier' of G; let V be set ; let v1 be Vertex of G; let W be Function; predpe islongestInShortestpath V,v1,W means :Def19: :: GRAPH_5:def 19 for v being Vertex of G st v in V & v <> v1 holds ex q being oriented Chain of G st ( q is_shortestpath_of v1,v,V,W & cost (q,W) <= cost (pe,W) ); end; :: deftheorem Def19 defines islongestInShortestpath GRAPH_5:def_19_:_ for G being Graph for pe being FinSequence of the carrier' of G for V being set for v1 being Vertex of G for W being Function holds ( pe islongestInShortestpath V,v1,W iff for v being Vertex of G st v in V & v <> v1 holds ex q being oriented Chain of G st ( q is_shortestpath_of v1,v,V,W & cost (q,W) <= cost (pe,W) ) ); theorem :: GRAPH_5:65 for e, V being set for W being Function for G being oriented finite Graph for P, Q, R being oriented Chain of G for v1, v2, v3 being Element of G st e in the carrier' of G & W is_weight>=0of G & len P >= 1 & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & R = P ^ <*e*> & Q is_shortestpath_of v1,v3,V,W & e orientedly_joins v2,v3 & P islongestInShortestpath V,v1,W holds ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) proof let e, V be set ; ::_thesis: for W being Function for G being oriented finite Graph for P, Q, R being oriented Chain of G for v1, v2, v3 being Element of G st e in the carrier' of G & W is_weight>=0of G & len P >= 1 & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & R = P ^ <*e*> & Q is_shortestpath_of v1,v3,V,W & e orientedly_joins v2,v3 & P islongestInShortestpath V,v1,W holds ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) let W be Function; ::_thesis: for G being oriented finite Graph for P, Q, R being oriented Chain of G for v1, v2, v3 being Element of G st e in the carrier' of G & W is_weight>=0of G & len P >= 1 & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & R = P ^ <*e*> & Q is_shortestpath_of v1,v3,V,W & e orientedly_joins v2,v3 & P islongestInShortestpath V,v1,W holds ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) let G be oriented finite Graph; ::_thesis: for P, Q, R being oriented Chain of G for v1, v2, v3 being Element of G st e in the carrier' of G & W is_weight>=0of G & len P >= 1 & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & R = P ^ <*e*> & Q is_shortestpath_of v1,v3,V,W & e orientedly_joins v2,v3 & P islongestInShortestpath V,v1,W holds ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) let P, Q, R be oriented Chain of G; ::_thesis: for v1, v2, v3 being Element of G st e in the carrier' of G & W is_weight>=0of G & len P >= 1 & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & R = P ^ <*e*> & Q is_shortestpath_of v1,v3,V,W & e orientedly_joins v2,v3 & P islongestInShortestpath V,v1,W holds ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) let v1, v2, v3 be Element of G; ::_thesis: ( e in the carrier' of G & W is_weight>=0of G & len P >= 1 & P is_shortestpath_of v1,v2,V,W & v1 <> v2 & v1 <> v3 & R = P ^ <*e*> & Q is_shortestpath_of v1,v3,V,W & e orientedly_joins v2,v3 & P islongestInShortestpath V,v1,W implies ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) ) assume that A1: e in the carrier' of G and A2: W is_weight>=0of G and A3: len P >= 1 and A4: P is_shortestpath_of v1,v2,V,W and A5: v1 <> v2 and A6: v1 <> v3 and A7: R = P ^ <*e*> and A8: Q is_shortestpath_of v1,v3,V,W and A9: e orientedly_joins v2,v3 and A10: P islongestInShortestpath V,v1,W ; ::_thesis: ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) A11: P is_orientedpath_of v1,v2,V by A4, Def18; then A12: v1 in V by A5, Th31; set Eg = the carrier' of G; reconsider pe = <*e*> as FinSequence of the carrier' of G by A1, FINSEQ_1:74; set V9 = V \/ {v2}; Q is_orientedpath_of v1,v3,V by A8, Def18; then A13: Q is_orientedpath_of v1,v3,V \/ {v2} by Th32, XBOOLE_1:7; A14: ( len pe = 1 & pe . 1 = e ) by FINSEQ_1:40; then consider s being oriented Simple Chain of G such that A15: s is_shortestpath_of v1,v3,V \/ {v2},W by A2, A3, A7, A9, A11, Th34, Th62; A16: R is_orientedpath_of v1,v3,V \/ {v2} by A3, A7, A9, A11, A14, Th34; A17: now__::_thesis:_(_cost_(Q,W)_<=_cost_(s,W)_implies_(_(_cost_(Q,W)_<=_cost_(R,W)_implies_Q_is_shortestpath_of_v1,v3,V_\/_{v2},W_)_&_(_cost_(Q,W)_>=_cost_(R,W)_implies_R_is_shortestpath_of_v1,v3,V_\/_{v2},W_)_)_) assume A18: cost (Q,W) <= cost (s,W) ; ::_thesis: ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) hereby ::_thesis: ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) assume cost (Q,W) <= cost (R,W) ; ::_thesis: Q is_shortestpath_of v1,v3,V \/ {v2},W now__::_thesis:_for_u_being_oriented_Chain_of_G_st_u_is_orientedpath_of_v1,v3,V_\/_{v2}_holds_ cost_(Q,W)_<=_cost_(u,W) let u be oriented Chain of G; ::_thesis: ( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (Q,W) <= cost (u,W) ) assume u is_orientedpath_of v1,v3,V \/ {v2} ; ::_thesis: cost (Q,W) <= cost (u,W) then cost (s,W) <= cost (u,W) by A15, Def18; hence cost (Q,W) <= cost (u,W) by A18, XXREAL_0:2; ::_thesis: verum end; hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A13, Def18; ::_thesis: verum end; hereby ::_thesis: verum assume A19: cost (Q,W) >= cost (R,W) ; ::_thesis: R is_shortestpath_of v1,v3,V \/ {v2},W now__::_thesis:_for_u_being_oriented_Chain_of_G_st_u_is_orientedpath_of_v1,v3,V_\/_{v2}_holds_ cost_(R,W)_<=_cost_(u,W) let u be oriented Chain of G; ::_thesis: ( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (R,W) <= cost (u,W) ) assume u is_orientedpath_of v1,v3,V \/ {v2} ; ::_thesis: cost (R,W) <= cost (u,W) then cost (s,W) <= cost (u,W) by A15, Def18; then cost (Q,W) <= cost (u,W) by A18, XXREAL_0:2; hence cost (R,W) <= cost (u,W) by A19, XXREAL_0:2; ::_thesis: verum end; hence R is_shortestpath_of v1,v3,V \/ {v2},W by A16, Def18; ::_thesis: verum end; end; set FT = the Target of G; set FS = the Source of G; A20: ( the Source of G . e = v2 & the Target of G . e = v3 ) by A9, GRAPH_4:def_1; A21: s is_orientedpath_of v1,v3,V \/ {v2} by A15, Def18; then A22: s is_orientedpath_of v1,v3 by Def4; then A23: the Target of G . (s . (len s)) = v3 by Def3; s <> {} by A22, Def3; then A24: len s >= 1 by FINSEQ_1:20; percases ( len s >= 2 or len s < 1 + 1 ) ; suppose len s >= 2 ; ::_thesis: ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) then consider k being Nat such that A25: len s = (1 + 1) + k by NAT_1:10; A26: (V \/ {v2}) \ {v2} = V \ {v2} by XBOOLE_1:40; reconsider k = k as Element of NAT by ORDINAL1:def_12; A27: len s = 1 + (1 + k) by A25; then consider s1, s2 being FinSequence such that A28: len s1 = 1 + k and A29: len s2 = 1 and A30: s = s1 ^ s2 by FINSEQ_2:22; reconsider s1 = s1, s2 = s2 as oriented Simple Chain of G by A30, Th14; A31: len s1 >= 1 by A28, NAT_1:12; A32: the Source of G . (s . 1) = v1 by A22, Def3; then A33: the Source of G . (s1 . 1) = v1 by A30, A31, Lm1; len s2 = 1 by A29; then A34: not v3 in vertices s1 by A6, A23, A30, A31, A32, Th18; A35: s2 . 1 = s . (len s) by A27, A28, A29, A30, Lm2; then A36: (vertices s) \ {v3} = ((vertices s1) \/ {v3}) \ {v3} by A23, A28, A29, A30, Th27, NAT_1:12 .= (vertices s1) \ {v3} by XBOOLE_1:40 .= vertices s1 by A34, ZFMISC_1:57 ; then vertices s1 c= V \/ {v2} by A21, Def4; then (vertices s1) \ {v2} c= (V \/ {v2}) \ {v2} by XBOOLE_1:33; then A37: (vertices s1) \ {v2} c= V by A26, XBOOLE_1:1; A38: len s1 < len s by A27, A28, NAT_1:13; then A39: the Source of G . (s . ((len s1) + 1)) = the Target of G . (s . (len s1)) by A31, GRAPH_1:def_15; A40: s1 . (len s1) = s . (len s1) by A30, A31, Lm1; then A41: the Source of G . (s2 . 1) = the Target of G . (s1 . (len s1)) by A27, A28, A35, A31, A38, GRAPH_1:def_15; A42: cost (s,W) = (cost (s1,W)) + (cost (s2,W)) by A2, A30, Th46, Th54; A43: not v1 in vertices s2 by A6, A23, A29, A30, A31, A32, Th18; hereby ::_thesis: verum percases ( v2 in vertices s1 or not v2 in vertices s1 ) ; suppose v2 in vertices s1 ; ::_thesis: ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) then consider i being Element of NAT such that A44: 1 <= i and A45: i <= len s1 and A46: v2 = the Target of G . (s1 . i) by A5, A33, Th28; s2 /. 1 in the carrier' of G by A1; then A47: s2 . 1 in the carrier' of G by A29, FINSEQ_4:15; hereby ::_thesis: verum percases ( the Source of G . (s2 . 1) = v2 or the Source of G . (s2 . 1) <> v2 ) ; supposeA48: the Source of G . (s2 . 1) = v2 ; ::_thesis: ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) s1 <> {} by A28; then s1 is_orientedpath_of v1,v2 by A33, A41, A48, Def3; then s1 is_orientedpath_of v1,v2,V by A37, Def4; then A49: cost (P,W) <= cost (s1,W) by A4, Def18; s2 . 1 = e by A1, A23, A20, A35, A47, A48, GRAPH_1:def_7; then s2 = pe by A29, FINSEQ_1:40; then cost (R,W) = (cost (P,W)) + (cost (s2,W)) by A2, A7, Th46, Th54; then A50: cost (R,W) <= cost (s,W) by A42, A49, XREAL_1:7; hereby ::_thesis: ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) assume cost (Q,W) <= cost (R,W) ; ::_thesis: Q is_shortestpath_of v1,v3,V \/ {v2},W then A51: cost (Q,W) <= cost (s,W) by A50, XXREAL_0:2; now__::_thesis:_for_u_being_oriented_Chain_of_G_st_u_is_orientedpath_of_v1,v3,V_\/_{v2}_holds_ cost_(Q,W)_<=_cost_(u,W) let u be oriented Chain of G; ::_thesis: ( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (Q,W) <= cost (u,W) ) assume u is_orientedpath_of v1,v3,V \/ {v2} ; ::_thesis: cost (Q,W) <= cost (u,W) then cost (s,W) <= cost (u,W) by A15, Def18; hence cost (Q,W) <= cost (u,W) by A51, XXREAL_0:2; ::_thesis: verum end; hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A13, Def18; ::_thesis: verum end; hereby ::_thesis: verum assume cost (Q,W) >= cost (R,W) ; ::_thesis: R is_shortestpath_of v1,v3,V \/ {v2},W now__::_thesis:_for_u_being_oriented_Chain_of_G_st_u_is_orientedpath_of_v1,v3,V_\/_{v2}_holds_ cost_(R,W)_<=_cost_(u,W) let u be oriented Chain of G; ::_thesis: ( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (R,W) <= cost (u,W) ) assume u is_orientedpath_of v1,v3,V \/ {v2} ; ::_thesis: cost (R,W) <= cost (u,W) then cost (s,W) <= cost (u,W) by A15, Def18; hence cost (R,W) <= cost (u,W) by A50, XXREAL_0:2; ::_thesis: verum end; hence R is_shortestpath_of v1,v3,V \/ {v2},W by A16, Def18; ::_thesis: verum end; end; supposeA52: the Source of G . (s2 . 1) <> v2 ; ::_thesis: ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) len s1 in dom s1 by A31, FINSEQ_3:25; then reconsider vx = the Target of G . (s1 . (len s1)) as Vertex of G by FINSEQ_2:11, FUNCT_2:5; A53: not vx in {v2} by A41, A52, TARSKI:def_1; len s1 in dom s1 by A31, FINSEQ_3:25; then A54: vx in vertices s1 by Th24; vertices s1 c= V \/ {v2} by A21, A36, Def4; then A55: vx in V by A54, A53, XBOOLE_0:def_3; {vx} c= V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {vx} or x in V ) assume x in {vx} ; ::_thesis: x in V hence x in V by A55, TARSKI:def_1; ::_thesis: verum end; then A56: V \/ {vx} c= V by XBOOLE_1:8; 1 in dom s2 by A29, FINSEQ_3:25; then vx <> v1 by A25, A28, A35, A40, A43, A39, Th24; then consider q9 being oriented Chain of G such that A57: q9 is_shortestpath_of v1,vx,V,W and A58: cost (q9,W) <= cost (P,W) by A10, A55, Def19; consider j being Nat such that A59: len s1 = i + j by A45, NAT_1:10; A60: q9 is_orientedpath_of v1,vx,V by A57, Def18; then A61: q9 is_orientedpath_of v1,vx by Def4; then q9 <> {} by Def3; then A62: len q9 >= 1 by FINSEQ_1:20; the Target of G . (q9 . (len q9)) = vx by A61, Def3; then reconsider qx = q9 ^ s2 as oriented Chain of G by A25, A28, A35, A40, A39, Th12; len qx = (len q9) + 1 by A29, FINSEQ_1:22; then A63: ( qx <> {} & the Target of G . (qx . (len qx)) = v3 ) by A23, A29, A35, Lm2; the Source of G . (q9 . 1) = v1 by A61, Def3; then the Source of G . (qx . 1) = v1 by A62, Lm1; then A64: qx is_orientedpath_of v1,v3 by A63, Def3; (vertices q9) \ {vx} c= V by A60, Def4; then vertices q9 c= V \/ {vx} by XBOOLE_1:44; then vertices q9 c= V by A56, XBOOLE_1:1; then A65: (vertices q9) \ {v3} c= V \ {v3} by XBOOLE_1:33; vertices qx = (vertices q9) \/ {v3} by A23, A29, A35, A62, Th27; then (vertices qx) \ {v3} = (vertices q9) \ {v3} by XBOOLE_1:40; then (vertices qx) \ {v3} c= V by A65, XBOOLE_1:1; then qx is_orientedpath_of v1,v3,V by A64, Def4; then A66: cost (Q,W) <= cost (qx,W) by A8, Def18; reconsider j = j as Element of NAT by ORDINAL1:def_12; consider t1, t2 being FinSequence such that A67: len t1 = i and len t2 = j and A68: s1 = t1 ^ t2 by A59, FINSEQ_2:22; reconsider t1 = t1, t2 = t2 as oriented Simple Chain of G by A68, Th14; A69: the Target of G . (t1 . (len t1)) = v2 by A44, A46, A67, A68, Lm1; vertices t1 c= vertices (t1 ^ t2) by Th26; then (vertices t1) \ {v2} c= (vertices s1) \ {v2} by A68, XBOOLE_1:33; then A70: (vertices t1) \ {v2} c= V by A37, XBOOLE_1:1; ( t1 <> {} & the Source of G . (t1 . 1) = v1 ) by A33, A44, A67, A68, Lm1; then t1 is_orientedpath_of v1,v2 by A69, Def3; then t1 is_orientedpath_of v1,v2,V by A70, Def4; then A71: cost (P,W) <= cost (t1,W) by A4, Def18; A72: cost (t2,W) >= 0 by A2, Th50; cost (s1,W) = (cost (t1,W)) + (cost (t2,W)) by A2, A68, Th46, Th54; then (cost (t1,W)) + 0 <= cost (s1,W) by A72, XREAL_1:7; then cost (P,W) <= cost (s1,W) by A71, XXREAL_0:2; then A73: cost (q9,W) <= cost (s1,W) by A58, XXREAL_0:2; cost (qx,W) = (cost (q9,W)) + (cost (s2,W)) by A2, Th46, Th54; then cost (qx,W) <= cost (s,W) by A42, A73, XREAL_1:7; then A74: cost (Q,W) <= cost (s,W) by A66, XXREAL_0:2; hereby ::_thesis: ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) assume cost (Q,W) <= cost (R,W) ; ::_thesis: Q is_shortestpath_of v1,v3,V \/ {v2},W now__::_thesis:_for_u_being_oriented_Chain_of_G_st_u_is_orientedpath_of_v1,v3,V_\/_{v2}_holds_ cost_(Q,W)_<=_cost_(u,W) let u be oriented Chain of G; ::_thesis: ( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (Q,W) <= cost (u,W) ) assume u is_orientedpath_of v1,v3,V \/ {v2} ; ::_thesis: cost (Q,W) <= cost (u,W) then cost (s,W) <= cost (u,W) by A15, Def18; hence cost (Q,W) <= cost (u,W) by A74, XXREAL_0:2; ::_thesis: verum end; hence Q is_shortestpath_of v1,v3,V \/ {v2},W by A13, Def18; ::_thesis: verum end; hereby ::_thesis: verum assume cost (Q,W) >= cost (R,W) ; ::_thesis: R is_shortestpath_of v1,v3,V \/ {v2},W then A75: cost (R,W) <= cost (s,W) by A74, XXREAL_0:2; now__::_thesis:_for_u_being_oriented_Chain_of_G_st_u_is_orientedpath_of_v1,v3,V_\/_{v2}_holds_ cost_(R,W)_<=_cost_(u,W) let u be oriented Chain of G; ::_thesis: ( u is_orientedpath_of v1,v3,V \/ {v2} implies cost (R,W) <= cost (u,W) ) assume u is_orientedpath_of v1,v3,V \/ {v2} ; ::_thesis: cost (R,W) <= cost (u,W) then cost (s,W) <= cost (u,W) by A15, Def18; hence cost (R,W) <= cost (u,W) by A75, XXREAL_0:2; ::_thesis: verum end; hence R is_shortestpath_of v1,v3,V \/ {v2},W by A16, Def18; ::_thesis: verum end; end; end; end; end; suppose not v2 in vertices s1 ; ::_thesis: ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) then A76: (vertices s1) \ {v2} = vertices s1 by ZFMISC_1:57; then (vertices s1) \ {v2} c= V \/ {v2} by A21, A36, Def4; then (vertices s) \ {v3} c= V by A36, A76, XBOOLE_1:43; then s is_orientedpath_of v1,v3,V by A22, Def4; hence ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) by A8, A17, Def18; ::_thesis: verum end; end; end; end; suppose len s < 1 + 1 ; ::_thesis: ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) then A77: len s <= 1 by NAT_1:13; then A78: len s = 1 by A24, XXREAL_0:1; A79: vertices s = vertices (s /. 1) by A24, A77, Th25, XXREAL_0:1; (vertices s) \ {v3} c= V proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (vertices s) \ {v3} or x in V ) assume A80: x in (vertices s) \ {v3} ; ::_thesis: x in V then A81: not x in {v3} by XBOOLE_0:def_5; x in vertices (s /. 1) by A79, A80, XBOOLE_0:def_5; then A82: ( x = the Source of G . (s /. 1) or x = the Target of G . (s /. 1) ) by TARSKI:def_2; A83: s /. 1 = s . 1 by A24, FINSEQ_4:15; v3 = the Target of G . (s . (len s)) by A22, Def3 .= the Target of G . (s /. 1) by A78, FINSEQ_4:15 ; hence x in V by A22, A12, A81, A82, A83, Def3, TARSKI:def_1; ::_thesis: verum end; then s is_orientedpath_of v1,v3,V by A22, Def4; hence ( ( cost (Q,W) <= cost (R,W) implies Q is_shortestpath_of v1,v3,V \/ {v2},W ) & ( cost (Q,W) >= cost (R,W) implies R is_shortestpath_of v1,v3,V \/ {v2},W ) ) by A8, A17, Def18; ::_thesis: verum end; end; end;