:: 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;