:: GRAPH_4 semantic presentation
begin
definition
let G be Graph;
let x, y be Element of G;
let e be set ;
prede orientedly_joins x,y means :Def1: :: GRAPH_4:def 1
( the Source of G . e = x & the Target of G . e = y );
end;
:: deftheorem Def1 defines orientedly_joins GRAPH_4:def_1_:_
for G being Graph
for x, y being Element of G
for e being set holds
( e orientedly_joins x,y iff ( the Source of G . e = x & the Target of G . e = y ) );
theorem Th1: :: GRAPH_4:1
for e being set
for G being Graph
for v1, v2 being Element of G st e orientedly_joins v1,v2 holds
e joins v1,v2
proof
let e be set ; ::_thesis: for G being Graph
for v1, v2 being Element of G st e orientedly_joins v1,v2 holds
e joins v1,v2
let G be Graph; ::_thesis: for v1, v2 being Element of G st e orientedly_joins v1,v2 holds
e joins v1,v2
let v1, v2 be Element of G; ::_thesis: ( e orientedly_joins v1,v2 implies e joins v1,v2 )
assume A1: e orientedly_joins v1,v2 ; ::_thesis: e joins v1,v2
then A2: the Source of G . e = v1 by Def1;
the Target of G . e = v2 by A1, Def1;
hence e joins v1,v2 by A2, GRAPH_1:def_12; ::_thesis: verum
end;
definition
let G be Graph;
let x, y be Element of the carrier of G;
predx,y are_orientedly_incident means :: GRAPH_4:def 2
ex v being set st
( v in the carrier' of G & v orientedly_joins x,y );
end;
:: deftheorem defines are_orientedly_incident GRAPH_4:def_2_:_
for G being Graph
for x, y being Element of the carrier of G holds
( x,y are_orientedly_incident iff ex v being set st
( v in the carrier' of G & v orientedly_joins x,y ) );
theorem Th2: :: GRAPH_4:2
for e being set
for G being Graph
for v1, v2, v3, v4 being Element of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds
( v1 = v3 & v2 = v4 )
proof
let e be set ; ::_thesis: for G being Graph
for v1, v2, v3, v4 being Element of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds
( v1 = v3 & v2 = v4 )
let G be Graph; ::_thesis: for v1, v2, v3, v4 being Element of G st e orientedly_joins v1,v2 & e orientedly_joins v3,v4 holds
( v1 = v3 & v2 = v4 )
let v1, v2, v3, v4 be Element of G; ::_thesis: ( e orientedly_joins v1,v2 & e orientedly_joins v3,v4 implies ( v1 = v3 & v2 = v4 ) )
assume that
A1: e orientedly_joins v1,v2 and
A2: e orientedly_joins v3,v4 ; ::_thesis: ( v1 = v3 & v2 = v4 )
A3: the Source of G . e = v1 by A1, Def1;
the Target of G . e = v2 by A1, Def1;
hence ( v1 = v3 & v2 = v4 ) by A2, A3, Def1; ::_thesis: verum
end;
definition
let G be Graph;
let X be set ;
funcG -SVSet X -> set equals :: GRAPH_4:def 3
{ v where v is Element of G : ex e being Element of the carrier' of G st
( e in X & v = the Source of G . e ) } ;
correctness
coherence
{ v where v is Element of G : ex e being Element of the carrier' of G st
( e in X & v = the Source of G . e ) } is set ;
;
end;
:: deftheorem defines -SVSet GRAPH_4:def_3_:_
for G being Graph
for X being set holds G -SVSet X = { v where v is Element of G : ex e being Element of the carrier' of G st
( e in X & v = the Source of G . e ) } ;
definition
let G be Graph;
let X be set ;
funcG -TVSet X -> set equals :: GRAPH_4:def 4
{ v where v is Element of G : ex e being Element of the carrier' of G st
( e in X & v = the Target of G . e ) } ;
correctness
coherence
{ v where v is Element of G : ex e being Element of the carrier' of G st
( e in X & v = the Target of G . e ) } is set ;
;
end;
:: deftheorem defines -TVSet GRAPH_4:def_4_:_
for G being Graph
for X being set holds G -TVSet X = { v where v is Element of G : ex e being Element of the carrier' of G st
( e in X & v = the Target of G . e ) } ;
theorem :: GRAPH_4:3
for G being Graph holds
( G -SVSet {} = {} & G -TVSet {} = {} )
proof
let G be Graph; ::_thesis: ( G -SVSet {} = {} & G -TVSet {} = {} )
set X = {} ;
A1: now__::_thesis:_not_G_-SVSet_{}_<>_{}
assume A2: G -SVSet {} <> {} ; ::_thesis: contradiction
set x = the Element of G -SVSet {};
the Element of G -SVSet {} in G -SVSet {} by A2;
then ex v being Element of G st
( v = the Element of G -SVSet {} & ex e being Element of the carrier' of G st
( e in {} & v = the Source of G . e ) ) ;
hence contradiction ; ::_thesis: verum
end;
now__::_thesis:_not_G_-TVSet_{}_<>_{}
assume A3: G -TVSet {} <> {} ; ::_thesis: contradiction
set x = the Element of G -TVSet {};
the Element of G -TVSet {} in G -TVSet {} by A3;
then ex v being Element of G st
( v = the Element of G -TVSet {} & ex e being Element of the carrier' of G st
( e in {} & v = the Target of G . e ) ) ;
hence contradiction ; ::_thesis: verum
end;
hence ( G -SVSet {} = {} & G -TVSet {} = {} ) by A1; ::_thesis: verum
end;
definition
let G be Graph;
let vs be FinSequence of the carrier of G;
let c be FinSequence;
predvs is_oriented_vertex_seq_of c means :Def5: :: GRAPH_4:def 5
( len vs = (len c) + 1 & ( for n being Element of NAT st 1 <= n & n <= len c holds
c . n orientedly_joins vs /. n,vs /. (n + 1) ) );
end;
:: deftheorem Def5 defines is_oriented_vertex_seq_of GRAPH_4:def_5_:_
for G being Graph
for vs being FinSequence of the carrier of G
for c being FinSequence holds
( vs is_oriented_vertex_seq_of c iff ( len vs = (len c) + 1 & ( for n being Element of NAT st 1 <= n & n <= len c holds
c . n orientedly_joins vs /. n,vs /. (n + 1) ) ) );
theorem Th4: :: GRAPH_4:4
for G being Graph
for vs being FinSequence of the carrier of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
vs is_vertex_seq_of c
proof
let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
vs is_vertex_seq_of c
let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
vs is_vertex_seq_of c
let c be oriented Chain of G; ::_thesis: ( vs is_oriented_vertex_seq_of c implies vs is_vertex_seq_of c )
assume A1: vs is_oriented_vertex_seq_of c ; ::_thesis: vs is_vertex_seq_of c
then A2: len vs = (len c) + 1 by Def5;
for n being Element of NAT st 1 <= n & n <= len c holds
c . n joins vs /. n,vs /. (n + 1)
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len c implies c . n joins vs /. n,vs /. (n + 1) )
assume that
A3: 1 <= n and
A4: n <= len c ; ::_thesis: c . n joins vs /. n,vs /. (n + 1)
c . n orientedly_joins vs /. n,vs /. (n + 1) by A1, A3, A4, Def5;
hence c . n joins vs /. n,vs /. (n + 1) by Th1; ::_thesis: verum
end;
hence vs is_vertex_seq_of c by A2, GRAPH_2:def_6; ::_thesis: verum
end;
theorem :: GRAPH_4:5
for G being Graph
for vs being FinSequence of the carrier of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
G -SVSet (rng c) c= rng vs
proof
let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
G -SVSet (rng c) c= rng vs
let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
G -SVSet (rng c) c= rng vs
let c be oriented Chain of G; ::_thesis: ( vs is_oriented_vertex_seq_of c implies G -SVSet (rng c) c= rng vs )
assume A1: vs is_oriented_vertex_seq_of c ; ::_thesis: G -SVSet (rng c) c= rng vs
then A2: len vs = (len c) + 1 by Def5;
G -SVSet (rng c) c= rng vs
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in G -SVSet (rng c) or y in rng vs )
assume y in G -SVSet (rng c) ; ::_thesis: y in rng vs
then consider v being Element of G such that
A3: v = y and
A4: ex e being Element of the carrier' of G st
( e in rng c & v = the Source of G . e ) ;
consider e being Element of the carrier' of G such that
A5: e in rng c and
A6: v = the Source of G . e by A4;
consider x being set such that
A7: x in dom c and
A8: e = c . x by A5, FUNCT_1:def_3;
reconsider x = x as Element of NAT by A7;
A9: 1 <= x by A7, FINSEQ_3:25;
A10: x <= len c by A7, FINSEQ_3:25;
then A11: x <= len vs by A2, NAT_1:12;
set v1 = vs /. x;
set v2 = vs /. (x + 1);
A12: vs /. x = vs . x by A9, A11, FINSEQ_4:15;
c . x orientedly_joins vs /. x,vs /. (x + 1) by A1, A9, A10, Def5;
then A13: v = vs /. x by A6, A8, Def1;
x in dom vs by A9, A11, FINSEQ_3:25;
hence y in rng vs by A3, A12, A13, FUNCT_1:def_3; ::_thesis: verum
end;
hence G -SVSet (rng c) c= rng vs ; ::_thesis: verum
end;
theorem :: GRAPH_4:6
for G being Graph
for vs being FinSequence of the carrier of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
G -TVSet (rng c) c= rng vs
proof
let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
G -TVSet (rng c) c= rng vs
let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
G -TVSet (rng c) c= rng vs
let c be oriented Chain of G; ::_thesis: ( vs is_oriented_vertex_seq_of c implies G -TVSet (rng c) c= rng vs )
assume A1: vs is_oriented_vertex_seq_of c ; ::_thesis: G -TVSet (rng c) c= rng vs
then A2: len vs = (len c) + 1 by Def5;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in G -TVSet (rng c) or y in rng vs )
assume y in G -TVSet (rng c) ; ::_thesis: y in rng vs
then consider v being Element of G such that
A3: v = y and
A4: ex e being Element of the carrier' of G st
( e in rng c & v = the Target of G . e ) ;
consider e being Element of the carrier' of G such that
A5: e in rng c and
A6: v = the Target of G . e by A4;
consider x being set such that
A7: x in dom c and
A8: e = c . x by A5, FUNCT_1:def_3;
reconsider x = x as Element of NAT by A7;
A9: 1 <= x by A7, FINSEQ_3:25;
A10: x <= len c by A7, FINSEQ_3:25;
A11: 1 <= x + 1 by NAT_1:12;
A12: x + 1 <= len vs by A2, A10, XREAL_1:7;
set v1 = vs /. x;
set v2 = vs /. (x + 1);
A13: vs /. (x + 1) = vs . (x + 1) by A2, A10, A11, FINSEQ_4:15, XREAL_1:7;
c . x orientedly_joins vs /. x,vs /. (x + 1) by A1, A9, A10, Def5;
then A14: v = vs /. (x + 1) by A6, A8, Def1;
x + 1 in dom vs by A11, A12, FINSEQ_3:25;
hence y in rng vs by A3, A13, A14, FUNCT_1:def_3; ::_thesis: verum
end;
theorem :: GRAPH_4:7
for G being Graph
for vs being FinSequence of the carrier of G
for c being oriented Chain of G st c <> {} & vs is_oriented_vertex_seq_of c holds
rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c))
proof
let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G
for c being oriented Chain of G st c <> {} & vs is_oriented_vertex_seq_of c holds
rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c))
let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st c <> {} & vs is_oriented_vertex_seq_of c holds
rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c))
let c be oriented Chain of G; ::_thesis: ( c <> {} & vs is_oriented_vertex_seq_of c implies rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c)) )
assume that
A1: c <> {} and
A2: vs is_oriented_vertex_seq_of c ; ::_thesis: rng vs c= (G -SVSet (rng c)) \/ (G -TVSet (rng c))
A3: len vs = (len c) + 1 by A2, Def5;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng vs or y in (G -SVSet (rng c)) \/ (G -TVSet (rng c)) )
assume y in rng vs ; ::_thesis: y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))
then consider x being set such that
A4: x in dom vs and
A5: y = vs . x by FUNCT_1:def_3;
reconsider x = x as Element of NAT by A4;
A6: 1 <= x by A4, FINSEQ_3:25;
A7: x <= len vs by A4, FINSEQ_3:25;
percases ( x <= len c or x = (len c) + 1 ) by A3, A7, NAT_1:8;
supposeA8: x <= len c ; ::_thesis: y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))
then x in dom c by A6, FINSEQ_3:25;
then A9: c . x in rng c by FUNCT_1:def_3;
rng c c= the carrier' of G by FINSEQ_1:def_4;
then reconsider e = c . x as Element of the carrier' of G by A9;
set v1 = vs /. x;
set v2 = vs /. (x + 1);
A10: vs /. x = vs . x by A6, A7, FINSEQ_4:15;
c . x orientedly_joins vs /. x,vs /. (x + 1) by A2, A6, A8, Def5;
then A11: vs /. x = the Source of G . e by Def1;
x in dom c by A6, A8, FINSEQ_3:25;
then e in rng c by FUNCT_1:def_3;
then y in G -SVSet (rng c) by A5, A10, A11;
hence y in (G -SVSet (rng c)) \/ (G -TVSet (rng c)) by XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA12: x = (len c) + 1 ; ::_thesis: y in (G -SVSet (rng c)) \/ (G -TVSet (rng c))
set l = len c;
0 + 1 = 1 ;
then A13: 1 <= len c by A1, NAT_1:13;
then len c in dom c by FINSEQ_3:25;
then A14: c . (len c) in rng c by FUNCT_1:def_3;
rng c c= the carrier' of G by FINSEQ_1:def_4;
then reconsider e = c . (len c) as Element of the carrier' of G by A14;
set v1 = vs /. (len c);
set v2 = vs /. ((len c) + 1);
A15: vs /. ((len c) + 1) = vs . ((len c) + 1) by A3, A6, A12, FINSEQ_4:15;
c . (len c) orientedly_joins vs /. (len c),vs /. ((len c) + 1) by A2, A13, Def5;
then A16: vs /. ((len c) + 1) = the Target of G . e by Def1;
len c in dom c by A13, FINSEQ_3:25;
then e in rng c by FUNCT_1:def_3;
then y in G -TVSet (rng c) by A5, A12, A15, A16;
hence y in (G -SVSet (rng c)) \/ (G -TVSet (rng c)) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
begin
theorem :: GRAPH_4:8
for G being Graph
for v being Element of G holds <*v*> is_oriented_vertex_seq_of {}
proof
let G be Graph; ::_thesis: for v being Element of G holds <*v*> is_oriented_vertex_seq_of {}
let v be Element of G; ::_thesis: <*v*> is_oriented_vertex_seq_of {}
set c = {} ;
thus len <*v*> = (len {}) + 1 by FINSEQ_1:40; :: according to GRAPH_4:def_5 ::_thesis: for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1)
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len {} implies {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) )
assume that
A1: 1 <= n and
A2: n <= len {} ; ::_thesis: {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1)
thus {} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) by A1, A2; ::_thesis: verum
end;
theorem Th9: :: GRAPH_4:9
for G being Graph
for c being oriented Chain of G ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c
proof
let G be Graph; ::_thesis: for c being oriented Chain of G ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c
let c be oriented Chain of G; ::_thesis: ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c
now__::_thesis:_(_(_c_<>_{}_&_ex_vs_being_FinSequence_of_the_carrier_of_G_st_vs_is_oriented_vertex_seq_of_c_)_or_(_c_=_{}_&_ex_vs_being_FinSequence_of_the_carrier_of_G_st_vs_is_oriented_vertex_seq_of_c_)_)
percases ( c <> {} or c = {} ) ;
caseA1: c <> {} ; ::_thesis: ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c
defpred S1[ Nat, set ] means ( ( $1 = (len c) + 1 implies $2 = the Target of G . (c . (len c)) ) & ( $1 <> (len c) + 1 implies $2 = the Source of G . (c . $1) ) );
A2: for k being Nat st k in Seg ((len c) + 1) holds
ex x being set st S1[k,x]
proof
let k be Nat; ::_thesis: ( k in Seg ((len c) + 1) implies ex x being set st S1[k,x] )
assume k in Seg ((len c) + 1) ; ::_thesis: ex x being set st S1[k,x]
now__::_thesis:_(_(_k_=_(len_c)_+_1_&_ex_x_being_set_st_S1[k,x]_)_or_(_k_<>_(len_c)_+_1_&_ex_x_being_set_st_S1[k,x]_)_)
percases ( k = (len c) + 1 or k <> (len c) + 1 ) ;
case k = (len c) + 1 ; ::_thesis: ex x being set st S1[k,x]
hence ex x being set st S1[k,x] ; ::_thesis: verum
end;
case k <> (len c) + 1 ; ::_thesis: ex x being set st S1[k,x]
hence ex x being set st S1[k,x] ; ::_thesis: verum
end;
end;
end;
hence ex x being set st S1[k,x] ; ::_thesis: verum
end;
ex p being FinSequence st
( dom p = Seg ((len c) + 1) & ( for k being Nat st k in Seg ((len c) + 1) holds
S1[k,p . k] ) ) from FINSEQ_1:sch_1(A2);
then consider p being FinSequence such that
A3: dom p = Seg ((len c) + 1) and
A4: for k being Nat st k in Seg ((len c) + 1) holds
( ( k = (len c) + 1 implies p . k = the Target of G . (c . (len c)) ) & ( k <> (len c) + 1 implies p . k = the Source of G . (c . k) ) ) ;
A5: len p = (len c) + 1 by A3, FINSEQ_1:def_3;
rng p c= the carrier of G
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng p or y in the carrier of G )
assume y in rng p ; ::_thesis: y in the carrier of G
then consider x being set such that
A6: x in dom p and
A7: y = p . x by FUNCT_1:def_3;
reconsider k = x as Element of NAT by A6;
A8: 1 <= k by A3, A6, FINSEQ_1:1;
A9: k <= (len c) + 1 by A3, A6, FINSEQ_1:1;
now__::_thesis:_(_(_k_=_(len_c)_+_1_&_y_in_the_carrier_of_G_)_or_(_k_<>_(len_c)_+_1_&_y_in_the_carrier_of_G_)_)
percases ( k = (len c) + 1 or k <> (len c) + 1 ) ;
case k = (len c) + 1 ; ::_thesis: y in the carrier of G
then A10: y = the Target of G . (c . (len c)) by A3, A4, A6, A7;
len c >= 0 + 1 by A1, NAT_1:13;
then len c in Seg (len c) by FINSEQ_1:1;
then len c in dom c by FINSEQ_1:def_3;
then A11: c . (len c) in rng c by FUNCT_1:def_3;
rng c c= the carrier' of G by FINSEQ_1:def_4;
hence y in the carrier of G by A10, A11, FUNCT_2:5; ::_thesis: verum
end;
caseA12: k <> (len c) + 1 ; ::_thesis: y in the carrier of G
then A13: y = the Source of G . (c . k) by A3, A4, A6, A7;
k < (len c) + 1 by A9, A12, XXREAL_0:1;
then k <= len c by NAT_1:13;
then k in Seg (len c) by A8, FINSEQ_1:1;
then k in dom c by FINSEQ_1:def_3;
then A14: c . k in rng c by FUNCT_1:def_3;
rng c c= the carrier' of G by FINSEQ_1:def_4;
hence y in the carrier of G by A13, A14, FUNCT_2:5; ::_thesis: verum
end;
end;
end;
hence y in the carrier of G ; ::_thesis: verum
end;
then reconsider vs = p as FinSequence of the carrier of G by FINSEQ_1:def_4;
for n being Element of NAT st 1 <= n & n <= len c holds
c . n orientedly_joins vs /. n,vs /. (n + 1)
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len c implies c . n orientedly_joins vs /. n,vs /. (n + 1) )
assume that
A15: 1 <= n and
A16: n <= len c ; ::_thesis: c . n orientedly_joins vs /. n,vs /. (n + 1)
percases ( n = len c or n <> len c ) ;
supposeA17: n = len c ; ::_thesis: c . n orientedly_joins vs /. n,vs /. (n + 1)
then A18: n < (len c) + 1 by NAT_1:13;
then n in Seg ((len c) + 1) by A15, FINSEQ_1:1;
then A19: p . n = the Source of G . (c . n) by A4, A18;
1 < n + 1 by A15, NAT_1:13;
then n + 1 in Seg ((len c) + 1) by A17, FINSEQ_1:1;
then A20: p . (n + 1) = the Target of G . (c . (len c)) by A4, A17;
A21: the Source of G . (c . n) = vs /. n by A5, A15, A18, A19, FINSEQ_4:15;
1 < n + 1 by A15, NAT_1:13;
then the Target of G . (c . n) = vs /. (n + 1) by A5, A17, A20, FINSEQ_4:15;
hence c . n orientedly_joins vs /. n,vs /. (n + 1) by A21, Def1; ::_thesis: verum
end;
suppose n <> len c ; ::_thesis: c . n orientedly_joins vs /. n,vs /. (n + 1)
then A22: n < len c by A16, XXREAL_0:1;
then n + 1 <= len c by NAT_1:13;
then A23: n + 1 < (len c) + 1 by NAT_1:13;
A24: n < (len c) + 1 by A16, NAT_1:13;
then n in Seg ((len c) + 1) by A15, FINSEQ_1:1;
then A25: p . n = the Source of G . (c . n) by A4, A24;
1 < n + 1 by A15, NAT_1:13;
then n + 1 in Seg ((len c) + 1) by A23, FINSEQ_1:1;
then A26: p . (n + 1) = the Source of G . (c . (n + 1)) by A4, A23;
A27: the Source of G . (c . n) = vs /. n by A5, A15, A24, A25, FINSEQ_4:15;
1 < n + 1 by A15, NAT_1:13;
then vs /. (n + 1) = p . (n + 1) by A5, A23, FINSEQ_4:15;
then the Target of G . (c . n) = vs /. (n + 1) by A15, A22, A26, GRAPH_1:def_15;
hence c . n orientedly_joins vs /. n,vs /. (n + 1) by A27, Def1; ::_thesis: verum
end;
end;
end;
then vs is_oriented_vertex_seq_of c by A5, Def5;
hence ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c ; ::_thesis: verum
end;
caseA28: c = {} ; ::_thesis: ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c
set x = the Element of G;
set vs = <* the Element of G*>;
len c = 0 by A28;
then A29: len <* the Element of G*> = (len c) + 1 by FINSEQ_1:40;
for n being Element of NAT st 1 <= n & n <= len c holds
c . n orientedly_joins <* the Element of G*> /. n,<* the Element of G*> /. (n + 1) by A28;
then <* the Element of G*> is_oriented_vertex_seq_of c by A29, Def5;
hence ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c ; ::_thesis: verum
end;
end;
end;
hence ex vs being FinSequence of the carrier of G st vs is_oriented_vertex_seq_of c ; ::_thesis: verum
end;
theorem Th10: :: GRAPH_4:10
for G being Graph
for vs1, vs2 being FinSequence of the carrier of G
for c being oriented Chain of G st c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c holds
vs1 = vs2
proof
let G be Graph; ::_thesis: for vs1, vs2 being FinSequence of the carrier of G
for c being oriented Chain of G st c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c holds
vs1 = vs2
let vs1, vs2 be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c holds
vs1 = vs2
let c be oriented Chain of G; ::_thesis: ( c <> {} & vs1 is_oriented_vertex_seq_of c & vs2 is_oriented_vertex_seq_of c implies vs1 = vs2 )
assume that
A1: c <> {} and
A2: vs1 is_oriented_vertex_seq_of c and
A3: vs2 is_oriented_vertex_seq_of c ; ::_thesis: vs1 = vs2
A4: len vs1 = (len c) + 1 by A2, Def5;
A5: len vs2 = (len c) + 1 by A3, Def5;
for n being Nat st 1 <= n & n <= len vs1 holds
vs1 . n = vs2 . n
proof
let n be Nat; ::_thesis: ( 1 <= n & n <= len vs1 implies vs1 . n = vs2 . n )
assume that
A6: 1 <= n and
A7: n <= len vs1 ; ::_thesis: vs1 . n = vs2 . n
A8: n <= (len c) + 1 by A2, A7, Def5;
A9: n in NAT by ORDINAL1:def_12;
percases ( n < (len c) + 1 or n >= (len c) + 1 ) ;
suppose n < (len c) + 1 ; ::_thesis: vs1 . n = vs2 . n
then A10: n <= len c by NAT_1:13;
then c . n orientedly_joins vs1 /. n,vs1 /. (n + 1) by A2, A6, A9, Def5;
then A11: the Source of G . (c . n) = vs1 /. n by Def1;
c . n orientedly_joins vs2 /. n,vs2 /. (n + 1) by A3, A6, A9, A10, Def5;
then A12: the Source of G . (c . n) = vs2 /. n by Def1;
vs1 . n = vs1 /. n by A6, A7, FINSEQ_4:15;
hence vs1 . n = vs2 . n by A4, A5, A6, A7, A11, A12, FINSEQ_4:15; ::_thesis: verum
end;
suppose n >= (len c) + 1 ; ::_thesis: vs1 . n = vs2 . n
then A13: n = (len c) + 1 by A8, XXREAL_0:1;
then A14: n - 1 = len c ;
A15: 0 + 1 <= len c by A1, NAT_1:13;
then A16: n - 1 = n -' 1 by A13, NAT_D:39;
A17: n -' 1 = len c by A14, A15, NAT_D:39;
then c . (n -' 1) orientedly_joins vs1 /. (n -' 1),vs1 /. ((n -' 1) + 1) by A2, A15, Def5;
then A18: the Target of G . (c . (n -' 1)) = vs1 /. ((n -' 1) + 1) by Def1;
c . (n -' 1) orientedly_joins vs2 /. (n -' 1),vs2 /. ((n -' 1) + 1) by A3, A15, A17, Def5;
then A19: the Target of G . (c . (n -' 1)) = vs2 /. ((n -' 1) + 1) by Def1;
vs1 . n = vs1 /. n by A6, A7, FINSEQ_4:15;
hence vs1 . n = vs2 . n by A4, A5, A6, A7, A16, A18, A19, FINSEQ_4:15; ::_thesis: verum
end;
end;
end;
hence vs1 = vs2 by A4, A5, FINSEQ_1:14; ::_thesis: verum
end;
definition
let G be Graph;
let c be oriented Chain of G;
assume A1: c <> {} ;
func oriented-vertex-seq c -> FinSequence of the carrier of G means :: GRAPH_4:def 6
it is_oriented_vertex_seq_of c;
existence
ex b1 being FinSequence of the carrier of G st b1 is_oriented_vertex_seq_of c by Th9;
uniqueness
for b1, b2 being FinSequence of the carrier of G st b1 is_oriented_vertex_seq_of c & b2 is_oriented_vertex_seq_of c holds
b1 = b2 by A1, Th10;
end;
:: deftheorem defines oriented-vertex-seq GRAPH_4:def_6_:_
for G being Graph
for c being oriented Chain of G st c <> {} holds
for b3 being FinSequence of the carrier of G holds
( b3 = oriented-vertex-seq c iff b3 is_oriented_vertex_seq_of c );
theorem :: GRAPH_4:11
for n being Element of NAT
for G being Graph
for vs, vs1 being FinSequence of the carrier of G
for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds
vs1 is_oriented_vertex_seq_of c1
proof
let n be Element of NAT ; ::_thesis: for G being Graph
for vs, vs1 being FinSequence of the carrier of G
for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds
vs1 is_oriented_vertex_seq_of c1
let G be Graph; ::_thesis: for vs, vs1 being FinSequence of the carrier of G
for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds
vs1 is_oriented_vertex_seq_of c1
let vs, vs1 be FinSequence of the carrier of G; ::_thesis: for c, c1 being oriented Chain of G st vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds
vs1 is_oriented_vertex_seq_of c1
let c, c1 be oriented Chain of G; ::_thesis: ( vs is_oriented_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) implies vs1 is_oriented_vertex_seq_of c1 )
assume A1: vs is_oriented_vertex_seq_of c ; ::_thesis: ( not c1 = c | (Seg n) or not vs1 = vs | (Seg (n + 1)) or vs1 is_oriented_vertex_seq_of c1 )
then A2: len vs = (len c) + 1 by Def5;
assume that
A3: c1 = c | (Seg n) and
A4: vs1 = vs | (Seg (n + 1)) ; ::_thesis: vs1 is_oriented_vertex_seq_of c1
now__::_thesis:_(_len_vs1_=_(len_c1)_+_1_&_(_for_k_being_Element_of_NAT_st_1_<=_k_&_k_<=_len_c1_holds_
c1_._k_orientedly_joins_vs1_/._k,vs1_/._(k_+_1)_)_)
percases ( n <= len c or len c <= n ) ;
supposeA5: n <= len c ; ::_thesis: ( len vs1 = (len c1) + 1 & ( for k being Element of NAT st 1 <= k & k <= len c1 holds
c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) )
then A6: n + 1 <= len vs by A2, XREAL_1:6;
A7: len c1 = n by A3, A5, FINSEQ_1:17;
A8: len vs1 = n + 1 by A4, A6, FINSEQ_1:17;
thus len vs1 = (len c1) + 1 by A4, A6, A7, FINSEQ_1:17; ::_thesis: for k being Element of NAT st 1 <= k & k <= len c1 holds
c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1)
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len c1 implies c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) )
assume that
A9: 1 <= k and
A10: k <= len c1 ; ::_thesis: c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1)
A11: k <= len c by A5, A7, A10, XXREAL_0:2;
k in Seg n by A7, A9, A10, FINSEQ_1:1;
then A12: c1 . k = c . k by A3, FUNCT_1:49;
A13: k <= len vs by A2, A11, NAT_1:12;
A14: k <= n + 1 by A7, A10, NAT_1:12;
then A15: k in Seg (n + 1) by A9, FINSEQ_1:1;
A16: 1 <= k + 1 by NAT_1:12;
k + 1 <= (len c1) + 1 by A10, XREAL_1:7;
then A17: k + 1 in Seg (n + 1) by A7, A16, FINSEQ_1:1;
A18: vs1 . k = vs . k by A4, A15, FUNCT_1:49;
A19: vs1 . (k + 1) = vs . (k + 1) by A4, A17, FUNCT_1:49;
A20: vs /. k = vs . k by A9, A13, FINSEQ_4:15;
A21: vs /. (k + 1) = vs . (k + 1) by A2, A11, A16, FINSEQ_4:15, XREAL_1:7;
A22: vs1 /. k = vs1 . k by A8, A9, A14, FINSEQ_4:15;
vs1 /. (k + 1) = vs1 . (k + 1) by A7, A8, A10, A16, FINSEQ_4:15, XREAL_1:7;
hence c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) by A1, A9, A11, A12, A18, A19, A20, A21, A22, Def5; ::_thesis: verum
end;
supposeA23: len c <= n ; ::_thesis: ( len vs1 = (len c1) + 1 & ( for k being Element of NAT st 1 <= k & k <= len c1 holds
c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) )
then A24: len vs <= n + 1 by A2, XREAL_1:6;
A25: c1 = c by A3, A23, FINSEQ_2:20;
vs1 = vs by A4, A24, FINSEQ_2:20;
hence ( len vs1 = (len c1) + 1 & ( for k being Element of NAT st 1 <= k & k <= len c1 holds
c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) ) ) by A1, A25, Def5; ::_thesis: verum
end;
end;
end;
hence vs1 is_oriented_vertex_seq_of c1 by Def5; ::_thesis: verum
end;
theorem Th12: :: GRAPH_4:12
for q being FinSequence
for m, n being Element of NAT
for G being Graph
for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is oriented Chain of G
proof
let q be FinSequence; ::_thesis: for m, n being Element of NAT
for G being Graph
for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is oriented Chain of G
let m, n be Element of NAT ; ::_thesis: for G being Graph
for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is oriented Chain of G
let G be Graph; ::_thesis: for c being oriented Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds
q is oriented Chain of G
let c be oriented Chain of G; ::_thesis: ( 1 <= m & m <= n & n <= len c & q = (m,n) -cut c implies q is oriented Chain of G )
assume that
A1: 1 <= m and
A2: m <= n and
A3: n <= len c and
A4: q = (m,n) -cut c ; ::_thesis: q is oriented Chain of G
consider vs being FinSequence of the carrier of G such that
A5: vs is_oriented_vertex_seq_of c by Th9;
A6: ((len q) + m) - m = (n + 1) - m by A1, A2, A3, A4, GRAPH_2:def_1;
reconsider qq = q as Chain of G by A1, A2, A3, A4, GRAPH_2:41;
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)
proof
let k be Element of NAT ; ::_thesis: ( 1 <= k & k < len q implies the Source of G . (q . (k + 1)) = the Target of G . (q . k) )
assume that
A7: 1 <= k and
A8: k < len q ; ::_thesis: the Source of G . (q . (k + 1)) = the Target of G . (q . k)
1 - 1 <= m - 1 by A1, XREAL_1:9;
then m - 1 = m -' 1 by XREAL_0:def_2;
then reconsider m1 = m - 1 as Element of NAT ;
reconsider i = m1 + k as Element of NAT ;
set v1 = vs /. i;
set v2 = vs /. (i + 1);
0 + 1 <= k by A7;
then consider j being Element of NAT such that
0 <= j and
A9: j < len q and
A10: k = j + 1 by A8, GRAPH_2:1;
A11: i = m + j by A10;
i + 1 = m + (j + 1) by A10;
then A12: c . (i + 1) = q . (k + 1) by A1, A2, A3, A4, A8, GRAPH_2:def_1;
A13: c . i = q . k by A1, A2, A3, A4, A9, A10, A11, GRAPH_2:def_1;
1 - 1 <= m - 1 by A1, XREAL_1:9;
then A14: 0 + 1 <= (m - 1) + k by A7, XREAL_1:7;
i <= (m - 1) + (n - (m - 1)) by A6, A8, XREAL_1:6;
then i <= len c by A3, XXREAL_0:2;
then c . i orientedly_joins vs /. i,vs /. (i + 1) by A5, A14, Def5;
then A15: the Target of G . (c . i) = vs /. (i + 1) by Def1;
A16: 1 < i + 1 by A14, NAT_1:13;
k + m < n + 1 by A6, A8, XREAL_1:6;
then k + m <= n by NAT_1:13;
then m + k <= len c by A3, XXREAL_0:2;
then c . (i + 1) orientedly_joins vs /. (i + 1),vs /. ((i + 1) + 1) by A5, A16, Def5;
hence the Source of G . (q . (k + 1)) = the Target of G . (q . k) by A12, A13, A15, Def1; ::_thesis: verum
end;
then qq is oriented by GRAPH_1:def_15;
hence q is oriented Chain of G ; ::_thesis: verum
end;
theorem Th13: :: GRAPH_4:13
for m, n being Element of NAT
for G being Graph
for vs, vs1 being FinSequence of the carrier of G
for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds
vs1 is_oriented_vertex_seq_of c1
proof
let m, n be Element of NAT ; ::_thesis: for G being Graph
for vs, vs1 being FinSequence of the carrier of G
for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds
vs1 is_oriented_vertex_seq_of c1
let G be Graph; ::_thesis: for vs, vs1 being FinSequence of the carrier of G
for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds
vs1 is_oriented_vertex_seq_of c1
let vs, vs1 be FinSequence of the carrier of G; ::_thesis: for c, c1 being oriented Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds
vs1 is_oriented_vertex_seq_of c1
let c, c1 be oriented Chain of G; ::_thesis: ( 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_oriented_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs implies vs1 is_oriented_vertex_seq_of c1 )
assume that
A1: 1 <= m and
A2: m <= n and
A3: n <= len c ; ::_thesis: ( not c1 = (m,n) -cut c or not vs is_oriented_vertex_seq_of c or not vs1 = (m,(n + 1)) -cut vs or vs1 is_oriented_vertex_seq_of c1 )
assume A4: c1 = (m,n) -cut c ; ::_thesis: ( not vs is_oriented_vertex_seq_of c or not vs1 = (m,(n + 1)) -cut vs or vs1 is_oriented_vertex_seq_of c1 )
assume that
A5: vs is_oriented_vertex_seq_of c and
A6: vs1 = (m,(n + 1)) -cut vs ; ::_thesis: vs1 is_oriented_vertex_seq_of c1
A7: len vs = (len c) + 1 by A5, Def5;
A8: m <= n + 1 by A2, NAT_1:12;
A9: n + 1 <= len vs by A3, A7, XREAL_1:6;
A10: (len c1) + m = n + 1 by A1, A2, A3, A4, GRAPH_2:def_1;
(len vs1) + m = (n + 1) + 1 by A1, A6, A8, A9, GRAPH_2:def_1;
hence A11: len vs1 = (len c1) + 1 by A10; :: according to GRAPH_4:def_5 ::_thesis: for n being Element of NAT st 1 <= n & n <= len c1 holds
c1 . n orientedly_joins vs1 /. n,vs1 /. (n + 1)
let k be Element of NAT ; ::_thesis: ( 1 <= k & k <= len c1 implies c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) )
assume that
A12: 1 <= k and
A13: k <= len c1 ; ::_thesis: c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1)
0 + 1 <= k by A12;
then consider j being Element of NAT such that
0 <= j and
A14: j < len c1 and
A15: k = j + 1 by A13, GRAPH_2:1;
set i = m + j;
set v1 = vs /. (m + j);
set v2 = vs /. ((m + j) + 1);
m + k <= (len c1) + m by A13, XREAL_1:7;
then A16: ((m + j) + 1) - 1 <= ((len c1) + m) - 1 by A15, XREAL_1:9;
A17: 1 <= m + j by A1, NAT_1:12;
A18: m + j <= len c by A3, A10, A16, XXREAL_0:2;
then A19: c . (m + j) orientedly_joins vs /. (m + j),vs /. ((m + j) + 1) by A5, A17, Def5;
j < len vs1 by A11, A14, NAT_1:13;
then A20: vs1 . k = vs . (m + j) by A1, A6, A8, A9, A15, GRAPH_2:def_1;
A21: j + 1 < len vs1 by A11, A14, XREAL_1:6;
(m + j) + 1 = m + (j + 1) ;
then A22: vs1 . (k + 1) = vs . ((m + j) + 1) by A1, A6, A8, A9, A15, A21, GRAPH_2:def_1;
A23: m + j <= len vs by A7, A18, NAT_1:12;
A24: 1 <= (m + j) + 1 by NAT_1:12;
A25: vs /. (m + j) = vs . (m + j) by A1, A23, FINSEQ_4:15, NAT_1:12;
A26: vs /. ((m + j) + 1) = vs . ((m + j) + 1) by A7, A18, A24, FINSEQ_4:15, XREAL_1:7;
0 + 1 = 1 ;
then A27: 1 <= k by A15, NAT_1:13;
A28: k <= len c1 by A14, A15, NAT_1:13;
then A29: k <= len vs1 by A11, NAT_1:12;
A30: 1 <= k + 1 by NAT_1:12;
A31: vs1 /. k = vs1 . k by A27, A29, FINSEQ_4:15;
vs1 /. (k + 1) = vs1 . (k + 1) by A11, A28, A30, FINSEQ_4:15, XREAL_1:7;
hence c1 . k orientedly_joins vs1 /. k,vs1 /. (k + 1) by A1, A2, A3, A4, A14, A15, A19, A20, A22, A25, A26, A31, GRAPH_2:def_1; ::_thesis: verum
end;
theorem Th14: :: GRAPH_4:14
for G being Graph
for vs1, vs2 being FinSequence of the carrier of G
for c1, c2 being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds
c1 ^ c2 is oriented Chain of G
proof
let G be Graph; ::_thesis: for vs1, vs2 being FinSequence of the carrier of G
for c1, c2 being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds
c1 ^ c2 is oriented Chain of G
let vs1, vs2 be FinSequence of the carrier of G; ::_thesis: for c1, c2 being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds
c1 ^ c2 is oriented Chain of G
let c1, c2 be oriented Chain of G; ::_thesis: ( vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 implies c1 ^ c2 is oriented Chain of G )
assume that
A1: vs1 is_oriented_vertex_seq_of c1 and
A2: vs2 is_oriented_vertex_seq_of c2 and
A3: vs1 . (len vs1) = vs2 . 1 ; ::_thesis: c1 ^ c2 is oriented Chain of G
A4: vs1 is_vertex_seq_of c1 by A1, Th4;
A5: vs2 is_vertex_seq_of c2 by A2, Th4;
A6: len vs1 = (len c1) + 1 by A1, Def5;
A7: len vs2 = (len c2) + 1 by A2, Def5;
set q = c1 ^ c2;
set p = vs1 ^' vs2;
thus c1 ^ c2 is oriented Chain of G ::_thesis: verum
proof
reconsider cc = c1 ^ c2 as Chain of G by A3, A4, A5, GRAPH_2:43;
for n being Element of NAT st 1 <= n & n < len (c1 ^ c2) holds
the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n)
proof
let n be Element of NAT ; ::_thesis: ( 1 <= n & n < len (c1 ^ c2) implies the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n) )
assume that
A8: 1 <= n and
A9: n < len (c1 ^ c2) ; ::_thesis: the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n)
A10: n in dom (c1 ^ c2) by A8, A9, FINSEQ_3:25;
A11: n + 1 <= len (c1 ^ c2) by A9, NAT_1:13;
A12: 1 < n + 1 by A8, NAT_1:13;
now__::_thesis:_(_(_n_in_dom_c1_&_ex_v1,_v2_being_Element_of_G_st_
(_v1_=_(vs1_^'_vs2)_._n_&_v2_=_(vs1_^'_vs2)_._(n_+_1)_&_(c1_^_c2)_._n_orientedly_joins_v1,v2_)_)_or_(_ex_k_being_Nat_st_
(_k_in_dom_c2_&_n_=_(len_c1)_+_k_)_&_ex_v1,_v2_being_Element_of_G_st_
(_v1_=_(vs1_^'_vs2)_._n_&_v2_=_(vs1_^'_vs2)_._(n_+_1)_&_(c1_^_c2)_._n_orientedly_joins_v1,v2_)_)_)
percases ( n in dom c1 or ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ) by A10, FINSEQ_1:25;
caseA13: n in dom c1 ; ::_thesis: ex v1, v2 being Element of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 )
then A14: (c1 ^ c2) . n = c1 . n by FINSEQ_1:def_7;
set v1 = vs1 /. n;
set v2 = vs1 /. (n + 1);
A15: 1 <= n by A13, FINSEQ_3:25;
A16: n <= len c1 by A13, FINSEQ_3:25;
then A17: c1 . n orientedly_joins vs1 /. n,vs1 /. (n + 1) by A1, A15, Def5;
A18: n <= len vs1 by A6, A16, NAT_1:12;
n + 1 <= (len c1) + 1 by A16, XREAL_1:6;
then A19: n + 1 <= len vs1 by A1, Def5;
A20: vs1 /. n = vs1 . n by A15, A18, FINSEQ_4:15;
A21: vs1 /. (n + 1) = vs1 . (n + 1) by A19, FINSEQ_4:15, NAT_1:12;
A22: (vs1 ^' vs2) . n = vs1 . n by A15, A18, GRAPH_2:14;
(vs1 ^' vs2) . (n + 1) = vs1 . (n + 1) by A19, GRAPH_2:14, NAT_1:12;
hence ex v1, v2 being Element of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 ) by A14, A17, A20, A21, A22; ::_thesis: verum
end;
case ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ; ::_thesis: ex v1, v2 being Element of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 )
then consider k being Nat such that
A23: k in dom c2 and
A24: n = (len c1) + k ;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A25: (c1 ^ c2) . n = c2 . k by A23, A24, FINSEQ_1:def_7;
A26: 1 <= k by A23, FINSEQ_3:25;
A27: k <= len c2 by A23, FINSEQ_3:25;
A28: 1 <= k + 1 by NAT_1:12;
A29: k <= len vs2 by A7, A27, NAT_1:12;
set v1 = vs2 /. k;
set v2 = vs2 /. (k + 1);
A30: vs2 /. k = vs2 . k by A26, A29, FINSEQ_4:15;
A31: vs2 /. (k + 1) = vs2 . (k + 1) by A7, A27, A28, FINSEQ_4:15, XREAL_1:7;
A32: c2 . k orientedly_joins vs2 /. k,vs2 /. (k + 1) by A2, A26, A27, Def5;
A33: k <= len vs2 by A7, A27, NAT_1:12;
0 + 1 <= k by A23, FINSEQ_3:25;
then consider j being Element of NAT such that
0 <= j and
A34: j < len vs2 and
A35: k = j + 1 by A33, GRAPH_2:1;
A36: (vs1 ^' vs2) . n = vs2 . k
proof
percases ( 1 = k or 1 < k ) by A26, XXREAL_0:1;
supposeA37: 1 = k ; ::_thesis: (vs1 ^' vs2) . n = vs2 . k
A38: 0 + 1 <= len vs1 by A6, NAT_1:13;
thus (vs1 ^' vs2) . n = (vs1 ^' vs2) . (len vs1) by A1, A24, A37, Def5
.= vs2 . k by A3, A37, A38, GRAPH_2:14 ; ::_thesis: verum
end;
suppose 1 < k ; ::_thesis: (vs1 ^' vs2) . n = vs2 . k
then A39: 1 <= j by A35, NAT_1:13;
thus (vs1 ^' vs2) . n = (vs1 ^' vs2) . (((len c1) + 1) + j) by A24, A35
.= (vs1 ^' vs2) . ((len vs1) + j) by A1, Def5
.= vs2 . k by A34, A35, A39, GRAPH_2:15 ; ::_thesis: verum
end;
end;
end;
A40: k < len vs2 by A7, A27, NAT_1:13;
(vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (((len c1) + 1) + k) by A24
.= (vs1 ^' vs2) . ((len vs1) + k) by A1, Def5
.= vs2 . (k + 1) by A26, A40, GRAPH_2:15 ;
hence ex v1, v2 being Element of G st
( v1 = (vs1 ^' vs2) . n & v2 = (vs1 ^' vs2) . (n + 1) & (c1 ^ c2) . n orientedly_joins v1,v2 ) by A25, A30, A31, A32, A36; ::_thesis: verum
end;
end;
end;
then consider v1, v2 being Element of G such that
v1 = (vs1 ^' vs2) . n and
A41: v2 = (vs1 ^' vs2) . (n + 1) and
A42: (c1 ^ c2) . n orientedly_joins v1,v2 ;
A43: n + 1 in dom (c1 ^ c2) by A11, A12, FINSEQ_3:25;
A44: now__::_thesis:_(_(_n_+_1_in_dom_c1_&_ex_v299,_v39_being_Element_of_G_st_
(_v299_=_(vs1_^'_vs2)_._(n_+_1)_&_v39_=_(vs1_^'_vs2)_._((n_+_1)_+_1)_&_(c1_^_c2)_._(n_+_1)_orientedly_joins_v299,v39_)_)_or_(_ex_k_being_Nat_st_
(_k_in_dom_c2_&_n_+_1_=_(len_c1)_+_k_)_&_ex_v299,_v39_being_Element_of_G_st_
(_v299_=_(vs1_^'_vs2)_._(n_+_1)_&_v39_=_(vs1_^'_vs2)_._((n_+_1)_+_1)_&_(c1_^_c2)_._(n_+_1)_orientedly_joins_v299,v39_)_)_)
percases ( n + 1 in dom c1 or ex k being Nat st
( k in dom c2 & n + 1 = (len c1) + k ) ) by A43, FINSEQ_1:25;
caseA45: n + 1 in dom c1 ; ::_thesis: ex v299, v39 being Element of G st
( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 )
then A46: (c1 ^ c2) . (n + 1) = c1 . (n + 1) by FINSEQ_1:def_7;
set v29 = vs1 /. (n + 1);
set v3 = vs1 /. ((n + 1) + 1);
A47: 1 <= n + 1 by A45, FINSEQ_3:25;
A48: n + 1 <= len c1 by A45, FINSEQ_3:25;
then A49: c1 . (n + 1) orientedly_joins vs1 /. (n + 1),vs1 /. ((n + 1) + 1) by A1, A47, Def5;
A50: n + 1 <= len vs1 by A6, A48, NAT_1:12;
(n + 1) + 1 <= (len c1) + 1 by A48, XREAL_1:6;
then A51: (n + 1) + 1 <= len vs1 by A1, Def5;
A52: vs1 /. (n + 1) = vs1 . (n + 1) by A47, A50, FINSEQ_4:15;
A53: vs1 /. ((n + 1) + 1) = vs1 . ((n + 1) + 1) by A51, FINSEQ_4:15, NAT_1:12;
A54: (vs1 ^' vs2) . (n + 1) = vs1 . (n + 1) by A47, A50, GRAPH_2:14;
(vs1 ^' vs2) . ((n + 1) + 1) = vs1 . ((n + 1) + 1) by A51, GRAPH_2:14, NAT_1:12;
hence ex v299, v39 being Element of G st
( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 ) by A46, A49, A52, A53, A54; ::_thesis: verum
end;
case ex k being Nat st
( k in dom c2 & n + 1 = (len c1) + k ) ; ::_thesis: ex v299, v39 being Element of G st
( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 )
then consider k being Nat such that
A55: k in dom c2 and
A56: n + 1 = (len c1) + k ;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A57: (c1 ^ c2) . (n + 1) = c2 . k by A55, A56, FINSEQ_1:def_7;
A58: 1 <= k by A55, FINSEQ_3:25;
A59: k <= len c2 by A55, FINSEQ_3:25;
A60: 1 <= k + 1 by NAT_1:12;
A61: k <= len vs2 by A7, A59, NAT_1:12;
set v29 = vs2 /. k;
set v3 = vs2 /. (k + 1);
A62: vs2 /. k = vs2 . k by A58, A61, FINSEQ_4:15;
A63: vs2 /. (k + 1) = vs2 . (k + 1) by A7, A59, A60, FINSEQ_4:15, XREAL_1:7;
A64: c2 . k orientedly_joins vs2 /. k,vs2 /. (k + 1) by A2, A58, A59, Def5;
A65: k <= len vs2 by A7, A59, NAT_1:12;
0 + 1 <= k by A55, FINSEQ_3:25;
then consider j being Element of NAT such that
0 <= j and
A66: j < len vs2 and
A67: k = j + 1 by A65, GRAPH_2:1;
A68: (vs1 ^' vs2) . (n + 1) = vs2 . k
proof
percases ( 1 = k or 1 < k ) by A58, XXREAL_0:1;
supposeA69: 1 = k ; ::_thesis: (vs1 ^' vs2) . (n + 1) = vs2 . k
A70: 0 + 1 <= len vs1 by A6, NAT_1:13;
thus (vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (len vs1) by A1, A56, A69, Def5
.= vs2 . k by A3, A69, A70, GRAPH_2:14 ; ::_thesis: verum
end;
suppose 1 < k ; ::_thesis: (vs1 ^' vs2) . (n + 1) = vs2 . k
then A71: 1 <= j by A67, NAT_1:13;
thus (vs1 ^' vs2) . (n + 1) = (vs1 ^' vs2) . (((len c1) + 1) + j) by A56, A67
.= (vs1 ^' vs2) . ((len vs1) + j) by A1, Def5
.= vs2 . k by A66, A67, A71, GRAPH_2:15 ; ::_thesis: verum
end;
end;
end;
A72: k < len vs2 by A7, A59, NAT_1:13;
(vs1 ^' vs2) . ((n + 1) + 1) = (vs1 ^' vs2) . (((len c1) + 1) + k) by A56
.= (vs1 ^' vs2) . ((len vs1) + k) by A1, Def5
.= vs2 . (k + 1) by A58, A72, GRAPH_2:15 ;
hence ex v299, v39 being Element of G st
( v299 = (vs1 ^' vs2) . (n + 1) & v39 = (vs1 ^' vs2) . ((n + 1) + 1) & (c1 ^ c2) . (n + 1) orientedly_joins v299,v39 ) by A57, A62, A63, A64, A68; ::_thesis: verum
end;
end;
end;
the Target of G . ((c1 ^ c2) . n) = v2 by A42, Def1;
hence the Source of G . ((c1 ^ c2) . (n + 1)) = the Target of G . ((c1 ^ c2) . n) by A41, A44, Def1; ::_thesis: verum
end;
then cc is oriented by GRAPH_1:def_15;
hence c1 ^ c2 is oriented Chain of G ; ::_thesis: verum
end;
end;
theorem Th15: :: GRAPH_4:15
for G being Graph
for vs1, vs2, vs being FinSequence of the carrier of G
for c1, c2, c being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds
vs is_oriented_vertex_seq_of c
proof
let G be Graph; ::_thesis: for vs1, vs2, vs being FinSequence of the carrier of G
for c1, c2, c being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds
vs is_oriented_vertex_seq_of c
let vs1, vs2, vs be FinSequence of the carrier of G; ::_thesis: for c1, c2, c being oriented Chain of G st vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds
vs is_oriented_vertex_seq_of c
let c1, c2, c be oriented Chain of G; ::_thesis: ( vs1 is_oriented_vertex_seq_of c1 & vs2 is_oriented_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 implies vs is_oriented_vertex_seq_of c )
assume that
A1: vs1 is_oriented_vertex_seq_of c1 and
A2: vs2 is_oriented_vertex_seq_of c2 and
A3: vs1 . (len vs1) = vs2 . 1 ; ::_thesis: ( not c = c1 ^ c2 or not vs = vs1 ^' vs2 or vs is_oriented_vertex_seq_of c )
assume that
A4: c = c1 ^ c2 and
A5: vs = vs1 ^' vs2 ; ::_thesis: vs is_oriented_vertex_seq_of c
A6: len vs1 = (len c1) + 1 by A1, Def5;
A7: len vs2 = (len c2) + 1 by A2, Def5;
then A8: vs2 <> {} ;
set q = c1 ^ c2;
set p = vs1 ^' vs2;
(len (vs1 ^' vs2)) + 1 = (len vs1) + (len vs2) by A8, GRAPH_2:13;
then A9: len (vs1 ^' vs2) = ((len c1) + (len c2)) + 1 by A6, A7
.= (len (c1 ^ c2)) + 1 by FINSEQ_1:22 ;
reconsider p = vs1 ^' vs2 as FinSequence of the carrier of G ;
now__::_thesis:_for_n_being_Element_of_NAT_st_1_<=_n_&_n_<=_len_(c1_^_c2)_holds_
(c1_^_c2)_._n_orientedly_joins_p_/._n,p_/._(n_+_1)
let n be Element of NAT ; ::_thesis: ( 1 <= n & n <= len (c1 ^ c2) implies (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1) )
assume that
A10: 1 <= n and
A11: n <= len (c1 ^ c2) ; ::_thesis: (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1)
A12: n <= len p by A9, A11, NAT_1:12;
A13: 1 <= n + 1 by NAT_1:12;
A14: p /. n = p . n by A10, A12, FINSEQ_4:15;
A15: p /. (n + 1) = p . (n + 1) by A9, A11, A13, FINSEQ_4:15, XREAL_1:7;
A16: n in dom (c1 ^ c2) by A10, A11, FINSEQ_3:25;
percases ( n in dom c1 or ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ) by A16, FINSEQ_1:25;
supposeA17: n in dom c1 ; ::_thesis: (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1)
set v1 = vs1 /. n;
set v2 = vs1 /. (n + 1);
A18: 1 <= n by A17, FINSEQ_3:25;
A19: n <= len c1 by A17, FINSEQ_3:25;
then A20: c1 . n orientedly_joins vs1 /. n,vs1 /. (n + 1) by A1, A18, Def5;
A21: n <= len vs1 by A6, A19, NAT_1:12;
n + 1 <= (len c1) + 1 by A19, XREAL_1:6;
then A22: n + 1 <= len vs1 by A1, Def5;
A23: vs1 /. n = vs1 . n by A18, A21, FINSEQ_4:15;
A24: vs1 /. (n + 1) = vs1 . (n + 1) by A22, FINSEQ_4:15, NAT_1:12;
A25: p . n = vs1 . n by A18, A21, GRAPH_2:14;
p . (n + 1) = vs1 . (n + 1) by A22, GRAPH_2:14, NAT_1:12;
hence (c1 ^ c2) . n orientedly_joins p /. n,p /. (n + 1) by A14, A15, A17, A20, A23, A24, A25, FINSEQ_1:def_7; ::_thesis: verum
end;
suppose ex k being Nat st
( k in dom c2 & n = (len c1) + k ) ; ::_thesis: (c1 ^ c2) . b1 orientedly_joins p /. b1,p /. (b1 + 1)
then consider k being Nat such that
A26: k in dom c2 and
A27: n = (len c1) + k ;
reconsider k = k as Element of NAT by ORDINAL1:def_12;
A28: (c1 ^ c2) . n = c2 . k by A26, A27, FINSEQ_1:def_7;
A29: 1 <= k by A26, FINSEQ_3:25;
A30: k <= len c2 by A26, FINSEQ_3:25;
A31: 1 <= k + 1 by NAT_1:12;
k <= len vs2 by A7, A30, NAT_1:12;
then A32: vs2 /. k = vs2 . k by A29, FINSEQ_4:15;
A33: vs2 /. (k + 1) = vs2 . (k + 1) by A7, A30, A31, FINSEQ_4:15, XREAL_1:7;
A34: k <= len vs2 by A7, A30, NAT_1:12;
0 + 1 <= k by A26, FINSEQ_3:25;
then consider j being Element of NAT such that
0 <= j and
A35: j < len vs2 and
A36: k = j + 1 by A34, GRAPH_2:1;
A37: p . n = vs2 . k
proof
percases ( 1 = k or 1 < k ) by A29, XXREAL_0:1;
supposeA38: 1 = k ; ::_thesis: p . n = vs2 . k
A39: 0 + 1 <= len vs1 by A6, NAT_1:13;
thus p . n = p . (len vs1) by A1, A27, A38, Def5
.= vs2 . k by A3, A38, A39, GRAPH_2:14 ; ::_thesis: verum
end;
suppose 1 < k ; ::_thesis: p . n = vs2 . k
then A40: 1 <= j by A36, NAT_1:13;
thus p . n = p . (((len c1) + 1) + j) by A27, A36
.= p . ((len vs1) + j) by A1, Def5
.= vs2 . k by A35, A36, A40, GRAPH_2:15 ; ::_thesis: verum
end;
end;
end;
A41: k < len vs2 by A7, A30, NAT_1:13;
p . (n + 1) = p . (((len c1) + 1) + k) by A27
.= p . ((len vs1) + k) by A1, Def5
.= vs2 . (k + 1) by A29, A41, GRAPH_2:15 ;
hence (c1 ^ c2) . n orientedly_joins p /. n,p /. (n + 1) by A2, A14, A15, A28, A29, A30, A32, A33, A37, Def5; ::_thesis: verum
end;
end;
end;
hence vs is_oriented_vertex_seq_of c by A4, A5, A9, Def5; ::_thesis: verum
end;
begin
Lm1: for G being Graph
for v being Element of G holds <*v*> is_oriented_vertex_seq_of {}
proof
let G be Graph; ::_thesis: for v being Element of G holds <*v*> is_oriented_vertex_seq_of {}
let v be Element of G; ::_thesis: <*v*> is_oriented_vertex_seq_of {}
set p = <*v*>;
set ec = {} ;
A1: len <*v*> = 0 + 1 by FINSEQ_1:39
.= (len {}) + 1 ;
for n being Element of NAT st 1 <= n & n <= len {} holds
{} . n orientedly_joins <*v*> /. n,<*v*> /. (n + 1) ;
hence <*v*> is_oriented_vertex_seq_of {} by A1, Def5; ::_thesis: verum
end;
definition
let G be Graph;
let IT be oriented Chain of G;
attrIT is Simple means :Def7: :: GRAPH_4:def 7
ex vs being FinSequence of the carrier of G st
( vs is_oriented_vertex_seq_of IT & ( for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) ) );
end;
:: deftheorem Def7 defines Simple GRAPH_4:def_7_:_
for G being Graph
for IT being oriented Chain of G holds
( IT is Simple iff ex vs being FinSequence of the carrier of G st
( vs is_oriented_vertex_seq_of IT & ( for n, m being Element of NAT st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds
( n = 1 & m = len vs ) ) ) );
registration
let G be Graph;
cluster Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented Simple for Chain of G;
existence
ex b1 being oriented Chain of G st b1 is Simple
proof
set q = the empty oriented Chain of G;
set x = the Element of G;
reconsider p = <* the Element of G*> as FinSequence of the carrier of G ;
A1: p is_oriented_vertex_seq_of the empty oriented Chain of G by Lm1;
for n, m being Element of NAT st 1 <= n & n < m & m <= len p & p . n = p . m holds
( n = 1 & m = len p )
proof
let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len p & p . n = p . m implies ( n = 1 & m = len p ) )
assume that
A2: 1 <= n and
A3: n < m and
A4: m <= len p and
p . n = p . m ; ::_thesis: ( n = 1 & m = len p )
1 < m by A2, A3, XXREAL_0:2;
hence ( n = 1 & m = len p ) by A4, FINSEQ_1:39; ::_thesis: verum
end;
then the empty oriented Chain of G is Simple by A1, Def7;
hence ex b1 being oriented Chain of G st b1 is Simple ; ::_thesis: verum
end;
end;
registration
let G be Graph;
cluster Relation-like NAT -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like oriented simple for Chain of G;
existence
ex b1 being Chain of G st
( b1 is oriented & b1 is simple )
proof
set q = the empty oriented Chain of G;
set x = the Element of G;
reconsider p = <* the Element of G*> as FinSequence of the carrier of G ;
A1: p is_vertex_seq_of the empty oriented Chain of G by Lm1, Th4;
reconsider q9 = the empty oriented Chain of G as Chain of G ;
for n, m being Element of NAT st 1 <= n & n < m & m <= len p & p . n = p . m holds
( n = 1 & m = len p )
proof
let n, m be Element of NAT ; ::_thesis: ( 1 <= n & n < m & m <= len p & p . n = p . m implies ( n = 1 & m = len p ) )
assume that
A2: 1 <= n and
A3: n < m and
A4: m <= len p and
p . n = p . m ; ::_thesis: ( n = 1 & m = len p )
1 < m by A2, A3, XXREAL_0:2;
hence ( n = 1 & m = len p ) by A4, FINSEQ_1:39; ::_thesis: verum
end;
then q9 is simple by A1, GRAPH_2:def_9;
hence ex b1 being Chain of G st
( b1 is oriented & b1 is simple ) ; ::_thesis: verum
end;
end;
theorem Th16: :: GRAPH_4:16
for n being Element of NAT
for G being Graph
for q being oriented Chain of G holds q | (Seg n) is oriented Chain of G
proof
let n be Element of NAT ; ::_thesis: for G being Graph
for q being oriented Chain of G holds q | (Seg n) is oriented Chain of G
let G be Graph; ::_thesis: for q being oriented Chain of G holds q | (Seg n) is oriented Chain of G
let q be oriented Chain of G; ::_thesis: q | (Seg n) is oriented Chain of G
reconsider q9 = q | (Seg n) as FinSequence by FINSEQ_1:15;
for i being Element of NAT st 1 <= i & i < len q9 holds
the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i)
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len q9 implies the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) )
assume that
A1: 1 <= i and
A2: i < len q9 ; ::_thesis: the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i)
percases ( n >= len q or n < len q ) ;
suppose n >= len q ; ::_thesis: the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i)
then q | (Seg n) = q by FINSEQ_3:49;
hence the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) by A1, A2, GRAPH_1:def_15; ::_thesis: verum
end;
supposeA3: n < len q ; ::_thesis: the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i)
then A4: len q9 = n by FINSEQ_1:17;
then A5: i < len q by A2, A3, XXREAL_0:2;
i in Seg n by A1, A2, A4, FINSEQ_1:1;
then A6: (q | (Seg n)) . i = q . i by FUNCT_1:49;
A7: i + 1 <= n by A2, A4, NAT_1:13;
1 < i + 1 by A1, NAT_1:13;
then i + 1 in Seg n by A7, FINSEQ_1:1;
then (q | (Seg n)) . (i + 1) = q . (i + 1) by FUNCT_1:49;
hence the Source of G . ((q | (Seg n)) . (i + 1)) = the Target of G . ((q | (Seg n)) . i) by A1, A5, A6, GRAPH_1:def_15; ::_thesis: verum
end;
end;
end;
hence q | (Seg n) is oriented Chain of G by GRAPH_1:4, GRAPH_1:def_15; ::_thesis: verum
end;
theorem :: GRAPH_4:17
for n being Element of NAT
for G being Graph
for sc being oriented simple Chain of G holds sc | (Seg n) is oriented simple Chain of G by Th16, GRAPH_2:45;
theorem Th18: :: GRAPH_4:18
for G being Graph
for sc being oriented simple Chain of G
for sc9 being oriented Chain of G st sc9 = sc holds
sc9 is Simple
proof
let G be Graph; ::_thesis: for sc being oriented simple Chain of G
for sc9 being oriented Chain of G st sc9 = sc holds
sc9 is Simple
let sc be oriented simple Chain of G; ::_thesis: for sc9 being oriented Chain of G st sc9 = sc holds
sc9 is Simple
let sc9 be oriented Chain of G; ::_thesis: ( sc9 = sc implies sc9 is Simple )
assume A1: sc9 = sc ; ::_thesis: sc9 is Simple
consider vs being FinSequence of the carrier of G such that
A2: vs is_oriented_vertex_seq_of sc9 by Th9;
vs is_vertex_seq_of sc by A1, A2, Th4;
then 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_2:47;
hence sc9 is Simple by A2, Def7; ::_thesis: verum
end;
theorem Th19: :: GRAPH_4:19
for G being Graph
for sc9 being oriented Simple Chain of G holds sc9 is oriented simple Chain of G
proof
let G be Graph; ::_thesis: for sc9 being oriented Simple Chain of G holds sc9 is oriented simple Chain of G
let sc9 be oriented Simple Chain of G; ::_thesis: sc9 is oriented simple Chain of G
consider vs being FinSequence of the carrier of G such that
A1: vs is_oriented_vertex_seq_of sc9 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 Def7;
vs is_vertex_seq_of sc9 by A1, Th4;
hence sc9 is oriented simple Chain of G by A2, GRAPH_2:def_9; ::_thesis: verum
end;
Lm2: for p being FinSequence
for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds
( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )
proof
let p be FinSequence; ::_thesis: for m, n being Element of NAT st 1 <= m & m <= n + 1 & n <= len p holds
( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )
let m, n be Element of NAT ; ::_thesis: ( 1 <= m & m <= n + 1 & n <= len p implies ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) ) )
assume that
A1: 1 <= m and
A2: m <= n + 1 and
A3: n <= len p ; ::_thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )
A4: ( m = n + 1 or m < n + 1 ) by A2, XXREAL_0:1;
percases ( m = n + 1 or m <= n ) by A4, NAT_1:13;
supposeA5: m = n + 1 ; ::_thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )
then A6: n < m by XREAL_1:29;
A7: ( not 1 <= m or not m <= n or not n <= len p ) by A5, XREAL_1:29;
(m,n) -cut p = {} by A6, GRAPH_2:def_1;
hence (len ((m,n) -cut p)) + m = n + 1 by A5, CARD_1:27; ::_thesis: for i being Element of NAT st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i)
thus for i being Element of NAT st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) by A7, CARD_1:27, GRAPH_2:def_1; ::_thesis: verum
end;
suppose m <= n ; ::_thesis: ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) )
hence ( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Element of NAT st i < len ((m,n) -cut p) holds
((m,n) -cut p) . (i + 1) = p . (m + i) ) ) by A1, A3, GRAPH_2:def_1; ::_thesis: verum
end;
end;
end;
theorem Th20: :: GRAPH_4:20
for G being Graph
for vs being FinSequence of the carrier of G
for c being oriented Chain of G st not c is Simple & vs is_oriented_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
proof
let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G
for c being oriented Chain of G st not c is Simple & vs is_oriented_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st not c is Simple & vs is_oriented_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
let c be oriented Chain of G; ::_thesis: ( not c is Simple & vs is_oriented_vertex_seq_of c implies ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 ) )
assume that
A1: not c is Simple and
A2: vs is_oriented_vertex_seq_of c ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
consider n, m being Element of NAT such that
A3: 1 <= n and
A4: n < m and
A5: m <= len vs and
A6: vs . n = vs . m and
A7: ( n <> 1 or m <> len vs ) by A1, A2, Def7;
A8: len vs = (len c) + 1 by A2, Def5;
A9: m - n > n - n by A4, XREAL_1:9;
reconsider n1 = n -' 1 as Element of NAT ;
A10: 1 - 1 <= n - 1 by A3, XREAL_1:9;
then A11: n - 1 = n -' 1 by XREAL_0:def_2;
A12: n1 + 1 = (n - 1) + 1 by A10, XREAL_0:def_2
.= n ;
percases ( ( n <> 1 & m <> len vs ) or ( n = 1 & m <> len vs ) or ( n <> 1 & m = len vs ) ) by A7;
supposeA13: ( n <> 1 & m <> len vs ) ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
then 1 < n by A3, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then A14: (1 + 1) - 1 <= n - 1 by XREAL_1:9;
n < len vs by A4, A5, XXREAL_0:2;
then A15: n - 1 < ((len c) + 1) - 1 by A8, XREAL_1:9;
A16: 1 <= n1 + 1 by NAT_1:12;
A17: m < len vs by A5, A13, XXREAL_0:1;
then A18: m <= len c by A8, NAT_1:13;
A19: 1 <= m by A3, A4, XXREAL_0:2;
A20: m <= len c by A8, A17, NAT_1:13;
reconsider c1 = (1,n1) -cut c as oriented Chain of G by A11, A14, A15, Th12;
reconsider c2 = (m,(len c)) -cut c as oriented Chain of G by A19, A20, Th12;
set pp = (1,n) -cut vs;
set p2 = (m,((len c) + 1)) -cut vs;
set p29 = ((m + 1),((len c) + 1)) -cut vs;
reconsider pp = (1,n) -cut vs as FinSequence of the carrier of G ;
reconsider p2 = (m,((len c) + 1)) -cut vs as FinSequence of the carrier of G ;
A21: n <= len vs by A4, A5, XXREAL_0:2;
A22: 1 <= m by A3, A4, XXREAL_0:2;
A23: m <= (len c) + 1 by A2, A5, Def5;
A24: (len c) + 1 <= len vs by A2, Def5;
A25: pp is_oriented_vertex_seq_of c1 by A2, A12, A14, A15, Th13;
A26: p2 is_oriented_vertex_seq_of c2 by A2, A19, A20, Th13;
A27: len pp = (len c1) + 1 by A25, Def5;
A28: len p2 = (len c2) + 1 by A26, Def5;
1 - 1 <= m - 1 by A19, XREAL_1:9;
then m -' 1 = m - 1 by XREAL_0:def_2;
then reconsider m1 = m - 1 as Element of NAT ;
A29: m = m1 + 1 ;
A30: (len c2) + m = (len c) + 1 by A19, A20, GRAPH_2:def_1;
A31: m - m <= (len c) - m by A18, XREAL_1:9;
then (len c2) -' 1 = (len c2) - 1 by A30, XREAL_0:def_2;
then reconsider lc21 = (len c2) - 1 as Element of NAT ;
A32: m + lc21 = m1 + (len c2) ;
0 + 1 = 1 ;
then A33: 1 <= len p2 by A28, NAT_1:13;
A34: p2 = ((0 + 1),(len p2)) -cut p2 by GRAPH_2:7
.= (((0 + 1),1) -cut p2) ^ (((1 + 1),(len p2)) -cut p2) by A33, GRAPH_2:8 ;
m1 <= m by A29, NAT_1:12;
then A35: p2 = (((m1 + 1),m) -cut vs) ^ (((m + 1),((len c) + 1)) -cut vs) by A5, A8, GRAPH_2:8;
(1,1) -cut p2 = <*(p2 . (0 + 1))*> by A33, GRAPH_2:6
.= <*(vs . (m + 0))*> by A22, A23, A24, A28, GRAPH_2:def_1
.= (m,m) -cut vs by A5, A19, GRAPH_2:6 ;
then A36: ((m + 1),((len c) + 1)) -cut vs = (2,(len p2)) -cut p2 by A34, A35, FINSEQ_1:33;
set domfc = { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ;
deffunc H1( set ) -> set = c . $1;
consider fc being Function such that
A37: dom fc = { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } and
A38: for x being set st x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } holds
fc . x = H1(x) from FUNCT_1:sch_3();
{ k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } c= Seg (len c)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } or x in Seg (len c) )
assume x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; ::_thesis: x in Seg (len c)
then consider kk being Element of NAT such that
A39: x = kk and
A40: ( ( 1 <= kk & kk <= n1 ) or ( m <= kk & kk <= len c ) ) ;
A41: 1 <= kk by A19, A40, XXREAL_0:2;
kk <= len c by A11, A15, A40, XXREAL_0:2;
hence x in Seg (len c) by A39, A41, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider fc = fc as FinSubsequence by A37, FINSEQ_1:def_12;
fc c= c
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fc or p in c )
assume A42: p in fc ; ::_thesis: p in c
then consider x, y being set such that
A43: [x,y] = p by RELAT_1:def_1;
A44: x in dom fc by A42, A43, FUNCT_1:1;
A45: y = fc . x by A42, A43, FUNCT_1:1;
consider kk being Element of NAT such that
A46: x = kk and
A47: ( ( 1 <= kk & kk <= n1 ) or ( m <= kk & kk <= len c ) ) by A37, A44;
A48: 1 <= kk by A19, A47, XXREAL_0:2;
kk <= len c by A11, A15, A47, XXREAL_0:2;
then A49: x in dom c by A46, A48, FINSEQ_3:25;
y = c . kk by A37, A38, A44, A45, A46;
hence p in c by A43, A46, A49, FUNCT_1:1; ::_thesis: verum
end;
then reconsider fc = fc as Subset of c ;
take fc ; ::_thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
set domfvs = { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ;
deffunc H2( set ) -> set = vs . $1;
consider fvs being Function such that
A50: dom fvs = { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } and
A51: for x being set st x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } holds
fvs . x = H2(x) from FUNCT_1:sch_3();
{ k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } c= Seg (len vs)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } or x in Seg (len vs) )
assume x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; ::_thesis: x in Seg (len vs)
then consider kk being Element of NAT such that
A52: x = kk and
A53: ( ( 1 <= kk & kk <= n ) or ( m + 1 <= kk & kk <= len vs ) ) ;
1 <= m + 1 by NAT_1:12;
then A54: 1 <= kk by A53, XXREAL_0:2;
kk <= len vs by A21, A53, XXREAL_0:2;
hence x in Seg (len vs) by A52, A54, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider fvs = fvs as FinSubsequence by A50, FINSEQ_1:def_12;
fvs c= vs
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fvs or p in vs )
assume A55: p in fvs ; ::_thesis: p in vs
then consider x, y being set such that
A56: [x,y] = p by RELAT_1:def_1;
A57: x in dom fvs by A55, A56, FUNCT_1:1;
A58: y = fvs . x by A55, A56, FUNCT_1:1;
consider kk being Element of NAT such that
A59: x = kk and
A60: ( ( 1 <= kk & kk <= n ) or ( m + 1 <= kk & kk <= len vs ) ) by A50, A57;
1 <= m + 1 by NAT_1:12;
then A61: 1 <= kk by A60, XXREAL_0:2;
kk <= len vs by A21, A60, XXREAL_0:2;
then A62: x in dom vs by A59, A61, FINSEQ_3:25;
y = vs . kk by A50, A51, A57, A58, A59;
hence p in vs by A56, A59, A62, FUNCT_1:1; ::_thesis: verum
end;
then reconsider fvs = fvs as Subset of vs ;
take fvs ; ::_thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
A63: p2 . 1 = vs . m by A22, A23, A24, GRAPH_2:12;
A64: pp . (len pp) = vs . n by A3, A21, GRAPH_2:12;
then reconsider c9 = c1 ^ c2 as oriented Chain of G by A6, A25, A26, A63, Th14;
take c9 ; ::_thesis: ex vs1 being FinSequence of the carrier of G st
( len c9 < len c & vs1 is_oriented_vertex_seq_of c9 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c9 & Seq fvs = vs1 )
take p1 = pp ^' p2; ::_thesis: ( len c9 < len c & p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
A65: p1 = pp ^ (((m + 1),((len c) + 1)) -cut vs) by A36, GRAPH_2:def_2;
A66: (len c1) + 1 = n1 + 1 by A11, A15, A16, Lm2;
- (- (m - n)) = m - n ;
then A67: - (m - n) < 0 by A9;
len c9 = (n - 1) + (((len c) - m) + 1) by A11, A30, A66, FINSEQ_1:22
.= (len c) + (n + (- m)) ;
hence A68: len c9 < len c by A67, XREAL_1:30; ::_thesis: ( p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
thus p1 is_oriented_vertex_seq_of c9 by A6, A25, A26, A63, A64, Th15; ::_thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
then len p1 = (len c9) + 1 by Def5;
hence len p1 < len vs by A8, A68, XREAL_1:6; ::_thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
1 <= 1 + (len c1) by NAT_1:12;
then 1 <= len pp by A25, Def5;
then p1 . 1 = pp . 1 by GRAPH_2:14;
hence vs . 1 = p1 . 1 by A3, A21, GRAPH_2:12; ::_thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
A69: p2 . (len p2) = vs . ((len c) + 1) by A22, A23, A24, GRAPH_2:12;
m - m <= (len c) - m by A20, XREAL_1:9;
then 0 + 1 <= ((len c) - m) + 1 by XREAL_1:6;
then 1 < len p2 by A28, A30, NAT_1:13;
hence vs . (len vs) = p1 . (len p1) by A8, A69, GRAPH_2:16; ::_thesis: ( Seq fc = c9 & Seq fvs = p1 )
set DL = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } ;
set DR = { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in__{__k_where_k_is_Element_of_NAT_:_(_(_1_<=_k_&_k_<=_n1_)_or_(_m_<=_k_&_k_<=_len_c_)_)__}__implies_x_in__{__kk_where_kk_is_Element_of_NAT_:_(_1_<=_kk_&_kk_<=_n1_)__}__\/__{__kk_where_kk_is_Element_of_NAT_:_(_m_<=_kk_&_kk_<=_len_c_)__}__)_&_(_x_in__{__kk_where_kk_is_Element_of_NAT_:_(_1_<=_kk_&_kk_<=_n1_)__}__\/__{__kk_where_kk_is_Element_of_NAT_:_(_m_<=_kk_&_kk_<=_len_c_)__}__implies_x_in__{__k_where_k_is_Element_of_NAT_:_(_(_1_<=_k_&_k_<=_n1_)_or_(_m_<=_k_&_k_<=_len_c_)_)__}__)_)
let x be set ; ::_thesis: ( ( x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } implies x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ) & ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } implies b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) } ) )
hereby ::_thesis: ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } implies b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) } )
assume x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; ::_thesis: x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) }
then ex k being Element of NAT st
( x = k & ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) ) ;
then ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } or x in { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ) ;
hence x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } by XBOOLE_0:def_3; ::_thesis: verum
end;
assume A70: x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) }
percases ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } or x in { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ) by A70, XBOOLE_0:def_3;
suppose x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) }
then ex k being Element of NAT st
( x = k & 1 <= k & k <= n1 ) ;
hence x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; ::_thesis: verum
end;
suppose x in { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n1 ) or ( m <= b2 & b2 <= len c ) ) }
then ex k being Element of NAT st
( x = k & m <= k & k <= len c ) ;
hence x in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } ; ::_thesis: verum
end;
end;
end;
then A71: { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } \/ { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } by TARSKI:1;
A72: ( { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } c= Seg (len c) & { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } c= Seg (len c) )
proof
hereby :: according to TARSKI:def_3 ::_thesis: { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } c= Seg (len c)
let x be set ; ::_thesis: ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } implies x in Seg (len c) )
assume x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } ; ::_thesis: x in Seg (len c)
then consider k being Element of NAT such that
A73: x = k and
A74: 1 <= k and
A75: k <= n1 ;
k <= len c by A11, A15, A75, XXREAL_0:2;
hence x in Seg (len c) by A73, A74, FINSEQ_1:1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } or x in Seg (len c) )
assume x in { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } ; ::_thesis: x in Seg (len c)
then consider k being Element of NAT such that
A76: x = k and
A77: m <= k and
A78: k <= len c ;
1 <= k by A22, A77, XXREAL_0:2;
hence x in Seg (len c) by A76, A78, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider DL = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } as finite set by FINSET_1:1;
reconsider DR = { kk where kk is Element of NAT : ( m <= kk & kk <= len c ) } as finite set by A72, FINSET_1:1;
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_DL_&_j_in_DR_holds_
i_<_j
let i, j be Element of NAT ; ::_thesis: ( i in DL & j in DR implies i < j )
assume i in DL ; ::_thesis: ( j in DR implies i < j )
then consider k being Element of NAT such that
A79: k = i and
1 <= k and
A80: k <= n1 ;
assume j in DR ; ::_thesis: i < j
then A81: ex l being Element of NAT st
( l = j & m <= l & l <= len c ) ;
n1 < m by A4, A12, NAT_1:13;
then k < m by A80, XXREAL_0:2;
hence i < j by A79, A81, XXREAL_0:2; ::_thesis: verum
end;
then A82: Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR) by A72, FINSEQ_3:42;
m + lc21 = len c by A30;
then A83: card DR = ((len c2) + (- 1)) + 1 by GRAPH_2:4
.= len c2 ;
A84: len (Sgm DR) = card DR by A72, FINSEQ_3:39;
DL = Seg n1 by FINSEQ_1:def_1;
then A85: Sgm DL = idseq n1 by FINSEQ_3:48;
then A86: dom (Sgm DL) = Seg n1 by RELAT_1:45;
rng (Sgm DL) = DL by A72, FINSEQ_1:def_13;
then A87: rng (Sgm DL) c= dom fc by A37, A71, XBOOLE_1:7;
rng (Sgm DR) = DR by A72, FINSEQ_1:def_13;
then A88: rng (Sgm DR) c= dom fc by A37, A71, XBOOLE_1:7;
set SL = Sgm DL;
set SR = Sgm DR;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in_c1_implies_p_in_fc_*_(Sgm_DL)_)_&_(_p_in_fc_*_(Sgm_DL)_implies_p_in_c1_)_)
let p be set ; ::_thesis: ( ( p in c1 implies p in fc * (Sgm DL) ) & ( p in fc * (Sgm DL) implies p in c1 ) )
hereby ::_thesis: ( p in fc * (Sgm DL) implies p in c1 )
assume A89: p in c1 ; ::_thesis: p in fc * (Sgm DL)
then consider x, y being set such that
A90: p = [x,y] by RELAT_1:def_1;
A91: x in dom c1 by A89, A90, FUNCT_1:1;
A92: y = c1 . x by A89, A90, FUNCT_1:1;
reconsider k = x as Element of NAT by A91;
A93: 1 <= k by A91, FINSEQ_3:25;
A94: k <= len c1 by A91, FINSEQ_3:25;
then A95: x in dom (Sgm DL) by A66, A86, A93, FINSEQ_1:1;
then A96: k = (Sgm DL) . k by A85, A86, FUNCT_1:18;
A97: k in { k where k is Element of NAT : ( ( 1 <= k & k <= n1 ) or ( m <= k & k <= len c ) ) } by A66, A93, A94;
then A98: x in dom (fc * (Sgm DL)) by A37, A95, A96, FUNCT_1:11;
0 + 1 <= k by A91, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A99: i < n1 and
A100: k = i + 1 by A66, A94, GRAPH_2:1;
(fc * (Sgm DL)) . x = fc . k by A96, A98, FUNCT_1:12
.= c . (1 + i) by A37, A97, A100, GRFUNC_1:2
.= y by A11, A15, A16, A66, A92, A99, A100, Lm2 ;
hence p in fc * (Sgm DL) by A90, A98, FUNCT_1:1; ::_thesis: verum
end;
assume A101: p in fc * (Sgm DL) ; ::_thesis: p in c1
then consider x, y being set such that
A102: p = [x,y] by RELAT_1:def_1;
A103: x in dom (fc * (Sgm DL)) by A101, A102, FUNCT_1:1;
A104: y = (fc * (Sgm DL)) . x by A101, A102, FUNCT_1:1;
A105: (fc * (Sgm DL)) . x = fc . ((Sgm DL) . x) by A103, FUNCT_1:12;
A106: x in dom (Sgm DL) by A103, FUNCT_1:11;
then x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } by A86, FINSEQ_1:def_1;
then consider k being Element of NAT such that
A107: k = x and
A108: 1 <= k and
A109: k <= n1 ;
A110: k in dom fc by A37, A108, A109;
A111: k = (Sgm DL) . k by A85, A86, A106, A107, FUNCT_1:18;
A112: k in dom c1 by A66, A108, A109, FINSEQ_3:25;
0 + 1 <= k by A108;
then ex i being Element of NAT st
( 0 <= i & i < n1 & k = i + 1 ) by A109, GRAPH_2:1;
then c1 . k = c . k by A11, A15, A16, A66, Lm2
.= y by A104, A105, A107, A110, A111, GRFUNC_1:2 ;
hence p in c1 by A102, A107, A112, FUNCT_1:1; ::_thesis: verum
end;
then A113: c1 = fc * (Sgm DL) by TARSKI:1;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in_c2_implies_p_in_fc_*_(Sgm_DR)_)_&_(_p_in_fc_*_(Sgm_DR)_implies_p_in_c2_)_)
let p be set ; ::_thesis: ( ( p in c2 implies p in fc * (Sgm DR) ) & ( p in fc * (Sgm DR) implies p in c2 ) )
hereby ::_thesis: ( p in fc * (Sgm DR) implies p in c2 )
assume A114: p in c2 ; ::_thesis: p in fc * (Sgm DR)
then consider x, y being set such that
A115: p = [x,y] by RELAT_1:def_1;
A116: x in dom c2 by A114, A115, FUNCT_1:1;
A117: y = c2 . x by A114, A115, FUNCT_1:1;
reconsider k = x as Element of NAT by A116;
A118: 1 <= k by A116, FINSEQ_3:25;
A119: k <= len c2 by A116, FINSEQ_3:25;
A120: x in dom (Sgm DR) by A83, A84, A116, FINSEQ_3:29;
A121: m1 + k = (Sgm DR) . k by A29, A30, A32, A118, A119, GRAPH_2:5;
A122: (Sgm DR) . k in rng (Sgm DR) by A120, FUNCT_1:def_3;
then A123: x in dom (fc * (Sgm DR)) by A88, A120, FUNCT_1:11;
0 + 1 <= k by A116, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A124: i < len c2 and
A125: k = i + 1 by A119, GRAPH_2:1;
(fc * (Sgm DR)) . x = fc . (m1 + k) by A121, A123, FUNCT_1:12
.= c . (m + i) by A88, A121, A122, A125, GRFUNC_1:2
.= y by A19, A20, A117, A124, A125, GRAPH_2:def_1 ;
hence p in fc * (Sgm DR) by A115, A123, FUNCT_1:1; ::_thesis: verum
end;
assume A126: p in fc * (Sgm DR) ; ::_thesis: p in c2
then consider x, y being set such that
A127: p = [x,y] by RELAT_1:def_1;
A128: x in dom (fc * (Sgm DR)) by A126, A127, FUNCT_1:1;
A129: y = (fc * (Sgm DR)) . x by A126, A127, FUNCT_1:1;
A130: x in dom (Sgm DR) by A128, FUNCT_1:11;
A131: (Sgm DR) . x in dom fc by A128, FUNCT_1:11;
reconsider k = x as Element of NAT by A130;
A132: k in dom c2 by A83, A84, A130, FINSEQ_3:29;
A133: 1 <= k by A130, FINSEQ_3:25;
A134: k <= len c2 by A83, A84, A130, FINSEQ_3:25;
then A135: m1 + k = (Sgm DR) . k by A29, A30, A32, A133, GRAPH_2:5;
0 + 1 <= k by A130, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A136: i < len c2 and
A137: k = i + 1 by A134, GRAPH_2:1;
c2 . k = c . ((m1 + 1) + i) by A19, A20, A136, A137, GRAPH_2:def_1
.= fc . ((Sgm DR) . k) by A131, A135, A137, GRFUNC_1:2
.= y by A129, A130, FUNCT_1:13 ;
hence p in c2 by A127, A132, FUNCT_1:1; ::_thesis: verum
end;
then A138: c2 = fc * (Sgm DR) by TARSKI:1;
Seq fc = fc * ((Sgm DL) ^ (Sgm DR)) by A37, A71, A82, FINSEQ_1:def_14;
hence Seq fc = c9 by A87, A88, A113, A138, GRAPH_2:24; ::_thesis: Seq fvs = p1
set DL = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } ;
set DR = { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in__{__k_where_k_is_Element_of_NAT_:_(_(_1_<=_k_&_k_<=_n_)_or_(_m_+_1_<=_k_&_k_<=_len_vs_)_)__}__implies_x_in__{__kk_where_kk_is_Element_of_NAT_:_(_1_<=_kk_&_kk_<=_n_)__}__\/__{__kk_where_kk_is_Element_of_NAT_:_(_m_+_1_<=_kk_&_kk_<=_len_vs_)__}__)_&_(_x_in__{__kk_where_kk_is_Element_of_NAT_:_(_1_<=_kk_&_kk_<=_n_)__}__\/__{__kk_where_kk_is_Element_of_NAT_:_(_m_+_1_<=_kk_&_kk_<=_len_vs_)__}__implies_x_in__{__k_where_k_is_Element_of_NAT_:_(_(_1_<=_k_&_k_<=_n_)_or_(_m_+_1_<=_k_&_k_<=_len_vs_)_)__}__)_)
let x be set ; ::_thesis: ( ( x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } implies x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ) & ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } implies b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) } ) )
hereby ::_thesis: ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } implies b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) } )
assume x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; ::_thesis: x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) }
then ex k being Element of NAT st
( x = k & ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) ) ;
then ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } or x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ) ;
hence x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } by XBOOLE_0:def_3; ::_thesis: verum
end;
assume A139: x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) }
percases ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } or x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ) by A139, XBOOLE_0:def_3;
suppose x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) }
then ex k being Element of NAT st
( x = k & 1 <= k & k <= n ) ;
hence x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; ::_thesis: verum
end;
suppose x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ; ::_thesis: b1 in { b2 where k is Element of NAT : ( ( 1 <= b2 & b2 <= n ) or ( m + 1 <= b2 & b2 <= len vs ) ) }
then ex k being Element of NAT st
( x = k & m + 1 <= k & k <= len vs ) ;
hence x in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } ; ::_thesis: verum
end;
end;
end;
then A140: { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } \/ { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } by TARSKI:1;
A141: ( { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } c= Seg (len vs) & { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } c= Seg (len vs) )
proof
hereby :: according to TARSKI:def_3 ::_thesis: { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } c= Seg (len vs)
let x be set ; ::_thesis: ( x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } implies x in Seg (len vs) )
assume x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } ; ::_thesis: x in Seg (len vs)
then consider k being Element of NAT such that
A142: x = k and
A143: 1 <= k and
A144: k <= n ;
k <= len vs by A21, A144, XXREAL_0:2;
hence x in Seg (len vs) by A142, A143, FINSEQ_1:1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } or x in Seg (len vs) )
assume x in { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } ; ::_thesis: x in Seg (len vs)
then consider k being Element of NAT such that
A145: x = k and
A146: m + 1 <= k and
A147: k <= len vs ;
1 <= m + 1 by NAT_1:12;
then 1 <= k by A146, XXREAL_0:2;
hence x in Seg (len vs) by A145, A147, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider DL = { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } as finite set by FINSET_1:1;
reconsider DR = { kk where kk is Element of NAT : ( m + 1 <= kk & kk <= len vs ) } as finite set by A141, FINSET_1:1;
now__::_thesis:_for_i,_j_being_Element_of_NAT_st_i_in_DL_&_j_in_DR_holds_
i_<_j
let i, j be Element of NAT ; ::_thesis: ( i in DL & j in DR implies i < j )
assume i in DL ; ::_thesis: ( j in DR implies i < j )
then consider k being Element of NAT such that
A148: k = i and
1 <= k and
A149: k <= n ;
assume j in DR ; ::_thesis: i < j
then consider l being Element of NAT such that
A150: l = j and
A151: m + 1 <= l and
l <= len vs ;
m <= m + 1 by NAT_1:12;
then A152: m <= l by A151, XXREAL_0:2;
k < m by A4, A149, XXREAL_0:2;
hence i < j by A148, A150, A152, XXREAL_0:2; ::_thesis: verum
end;
then A153: Sgm (DL \/ DR) = (Sgm DL) ^ (Sgm DR) by A141, FINSEQ_3:42;
1 <= len p2 by A28, NAT_1:12;
then 1 - 1 <= (len p2) - 1 by XREAL_1:9;
then (len p2) -' 1 = (len p2) - 1 by XREAL_0:def_2;
then reconsider lp21 = (len p2) - 1 as Element of NAT ;
lp21 -' 1 = lp21 - 1 by A28, A30, A31, XREAL_0:def_2;
then reconsider lp22 = lp21 - 1 as Element of NAT ;
A154: (m + 1) + lp22 = m + ((lp21 - 1) + 1)
.= m + (((((len c) - m) + 1) + 1) - 1) by A26, A30, Def5
.= (len c) + 1 ;
then A155: card DR = lp22 + 1 by A8, GRAPH_2:4
.= lp21 ;
A156: 1 <= m + 1 by NAT_1:12;
A157: m + 1 <= ((len c) + 1) + 1 by A23, XREAL_1:6;
A158: (len p2) + m = ((len c) + 1) + 1 by A22, A23, A24, GRAPH_2:def_1
.= (len (((m + 1),((len c) + 1)) -cut vs)) + (m + 1) by A24, A156, A157, Lm2
.= ((len (((m + 1),((len c) + 1)) -cut vs)) + 1) + m ;
A159: len (Sgm DR) = card DR by A141, FINSEQ_3:39;
DL = Seg n by FINSEQ_1:def_1;
then A160: Sgm DL = idseq n by FINSEQ_3:48;
then A161: dom (Sgm DL) = Seg n by RELAT_1:45;
rng (Sgm DL) = DL by A141, FINSEQ_1:def_13;
then A162: rng (Sgm DL) c= dom fvs by A50, A140, XBOOLE_1:7;
rng (Sgm DR) = DR by A141, FINSEQ_1:def_13;
then A163: rng (Sgm DR) c= dom fvs by A50, A140, XBOOLE_1:7;
set SL = Sgm DL;
set SR = Sgm DR;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in_pp_implies_p_in_fvs_*_(Sgm_DL)_)_&_(_p_in_fvs_*_(Sgm_DL)_implies_p_in_pp_)_)
let p be set ; ::_thesis: ( ( p in pp implies p in fvs * (Sgm DL) ) & ( p in fvs * (Sgm DL) implies p in pp ) )
hereby ::_thesis: ( p in fvs * (Sgm DL) implies p in pp )
assume A164: p in pp ; ::_thesis: p in fvs * (Sgm DL)
then consider x, y being set such that
A165: p = [x,y] by RELAT_1:def_1;
A166: x in dom pp by A164, A165, FUNCT_1:1;
A167: y = pp . x by A164, A165, FUNCT_1:1;
reconsider k = x as Element of NAT by A166;
A168: 1 <= k by A166, FINSEQ_3:25;
A169: k <= len pp by A166, FINSEQ_3:25;
then A170: x in dom (Sgm DL) by A11, A27, A66, A161, A168, FINSEQ_1:1;
then A171: k = (Sgm DL) . k by A160, A161, FUNCT_1:18;
A172: k in { k where k is Element of NAT : ( ( 1 <= k & k <= n ) or ( m + 1 <= k & k <= len vs ) ) } by A11, A27, A66, A168, A169;
then A173: x in dom (fvs * (Sgm DL)) by A50, A170, A171, FUNCT_1:11;
0 + 1 <= k by A166, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A174: i < n and
A175: k = i + 1 by A11, A27, A66, A169, GRAPH_2:1;
(fvs * (Sgm DL)) . x = fvs . k by A171, A173, FUNCT_1:12
.= vs . (1 + i) by A50, A172, A175, GRFUNC_1:2
.= y by A3, A11, A21, A27, A66, A167, A174, A175, GRAPH_2:def_1 ;
hence p in fvs * (Sgm DL) by A165, A173, FUNCT_1:1; ::_thesis: verum
end;
assume A176: p in fvs * (Sgm DL) ; ::_thesis: p in pp
then consider x, y being set such that
A177: p = [x,y] by RELAT_1:def_1;
A178: x in dom (fvs * (Sgm DL)) by A176, A177, FUNCT_1:1;
A179: y = (fvs * (Sgm DL)) . x by A176, A177, FUNCT_1:1;
A180: (fvs * (Sgm DL)) . x = fvs . ((Sgm DL) . x) by A178, FUNCT_1:12;
A181: x in dom (Sgm DL) by A178, FUNCT_1:11;
then x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } by A161, FINSEQ_1:def_1;
then consider k being Element of NAT such that
A182: k = x and
A183: 1 <= k and
A184: k <= n ;
A185: k in dom fvs by A50, A183, A184;
A186: k = (Sgm DL) . k by A160, A161, A181, A182, FUNCT_1:18;
A187: k in dom pp by A11, A27, A66, A183, A184, FINSEQ_3:25;
0 + 1 <= k by A183;
then ex i being Element of NAT st
( 0 <= i & i < n & k = i + 1 ) by A184, GRAPH_2:1;
then pp . k = vs . k by A3, A11, A21, A27, A66, GRAPH_2:def_1
.= y by A179, A180, A182, A185, A186, GRFUNC_1:2 ;
hence p in pp by A177, A182, A187, FUNCT_1:1; ::_thesis: verum
end;
then A188: pp = fvs * (Sgm DL) by TARSKI:1;
A189: (m + 1) + lp22 = m + lp21 ;
A190: 1 <= m + 1 by NAT_1:12;
A191: m + 1 <= ((len c) + 1) + 1 by A5, A8, XREAL_1:7;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in_((m_+_1),((len_c)_+_1))_-cut_vs_implies_p_in_fvs_*_(Sgm_DR)_)_&_(_p_in_fvs_*_(Sgm_DR)_implies_p_in_((m_+_1),((len_c)_+_1))_-cut_vs_)_)
let p be set ; ::_thesis: ( ( p in ((m + 1),((len c) + 1)) -cut vs implies p in fvs * (Sgm DR) ) & ( p in fvs * (Sgm DR) implies p in ((m + 1),((len c) + 1)) -cut vs ) )
hereby ::_thesis: ( p in fvs * (Sgm DR) implies p in ((m + 1),((len c) + 1)) -cut vs )
assume A192: p in ((m + 1),((len c) + 1)) -cut vs ; ::_thesis: p in fvs * (Sgm DR)
then consider x, y being set such that
A193: p = [x,y] by RELAT_1:def_1;
A194: x in dom (((m + 1),((len c) + 1)) -cut vs) by A192, A193, FUNCT_1:1;
A195: y = (((m + 1),((len c) + 1)) -cut vs) . x by A192, A193, FUNCT_1:1;
reconsider k = x as Element of NAT by A194;
A196: 1 <= k by A194, FINSEQ_3:25;
A197: k <= len (((m + 1),((len c) + 1)) -cut vs) by A194, FINSEQ_3:25;
A198: x in dom (Sgm DR) by A155, A158, A159, A194, FINSEQ_3:29;
A199: m + k = (Sgm DR) . k by A8, A154, A158, A189, A196, A197, GRAPH_2:5;
A200: (Sgm DR) . k in rng (Sgm DR) by A198, FUNCT_1:def_3;
then A201: x in dom (fvs * (Sgm DR)) by A163, A198, FUNCT_1:11;
0 + 1 <= k by A194, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A202: i < len (((m + 1),((len c) + 1)) -cut vs) and
A203: k = i + 1 by A197, GRAPH_2:1;
(fvs * (Sgm DR)) . x = fvs . (m + k) by A199, A201, FUNCT_1:12
.= vs . ((m + 1) + i) by A163, A199, A200, A203, GRFUNC_1:2
.= y by A8, A190, A191, A195, A202, A203, Lm2 ;
hence p in fvs * (Sgm DR) by A193, A201, FUNCT_1:1; ::_thesis: verum
end;
assume A204: p in fvs * (Sgm DR) ; ::_thesis: p in ((m + 1),((len c) + 1)) -cut vs
then consider x, y being set such that
A205: p = [x,y] by RELAT_1:def_1;
A206: x in dom (fvs * (Sgm DR)) by A204, A205, FUNCT_1:1;
A207: y = (fvs * (Sgm DR)) . x by A204, A205, FUNCT_1:1;
A208: x in dom (Sgm DR) by A206, FUNCT_1:11;
A209: (Sgm DR) . x in dom fvs by A206, FUNCT_1:11;
reconsider k = x as Element of NAT by A208;
A210: k in dom (((m + 1),((len c) + 1)) -cut vs) by A155, A158, A159, A208, FINSEQ_3:29;
A211: 1 <= k by A208, FINSEQ_3:25;
A212: k <= len (((m + 1),((len c) + 1)) -cut vs) by A155, A158, A159, A208, FINSEQ_3:25;
then A213: m + k = (Sgm DR) . k by A8, A154, A158, A189, A211, GRAPH_2:5;
0 + 1 <= k by A208, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A214: i < len (((m + 1),((len c) + 1)) -cut vs) and
A215: k = i + 1 by A212, GRAPH_2:1;
(((m + 1),((len c) + 1)) -cut vs) . k = vs . ((m + 1) + i) by A8, A190, A191, A214, A215, Lm2
.= fvs . ((Sgm DR) . k) by A209, A213, A215, GRFUNC_1:2
.= y by A207, A208, FUNCT_1:13 ;
hence p in ((m + 1),((len c) + 1)) -cut vs by A205, A210, FUNCT_1:1; ::_thesis: verum
end;
then A216: ((m + 1),((len c) + 1)) -cut vs = fvs * (Sgm DR) by TARSKI:1;
Seq fvs = fvs * ((Sgm DL) ^ (Sgm DR)) by A50, A140, A153, FINSEQ_1:def_14;
hence Seq fvs = p1 by A65, A162, A163, A188, A216, GRAPH_2:24; ::_thesis: verum
end;
supposeA217: ( n = 1 & m <> len vs ) ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
then A218: m < len vs by A5, XXREAL_0:1;
then A219: m <= len c by A8, NAT_1:13;
A220: 1 < m by A3, A4, XXREAL_0:2;
A221: 1 <= m by A3, A4, XXREAL_0:2;
A222: m <= len c by A8, A218, NAT_1:13;
reconsider c2 = (m,(len c)) -cut c as oriented Chain of G by A219, A220, Th12;
set p2 = (m,((len c) + 1)) -cut vs;
A223: (m,((len c) + 1)) -cut vs is_oriented_vertex_seq_of c2 by A2, A219, A220, Th13;
set domfc = { k where k is Element of NAT : ( m <= k & k <= len c ) } ;
deffunc H1( set ) -> set = c . $1;
consider fc being Function such that
A224: dom fc = { k where k is Element of NAT : ( m <= k & k <= len c ) } and
A225: for x being set st x in { k where k is Element of NAT : ( m <= k & k <= len c ) } holds
fc . x = H1(x) from FUNCT_1:sch_3();
{ k where k is Element of NAT : ( m <= k & k <= len c ) } c= Seg (len c)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m <= k & k <= len c ) } or x in Seg (len c) )
assume x in { k where k is Element of NAT : ( m <= k & k <= len c ) } ; ::_thesis: x in Seg (len c)
then consider kk being Element of NAT such that
A226: x = kk and
A227: m <= kk and
A228: kk <= len c ;
1 <= kk by A220, A227, XXREAL_0:2;
hence x in Seg (len c) by A226, A228, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider fc = fc as FinSubsequence by A224, FINSEQ_1:def_12;
fc c= c
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fc or p in c )
assume A229: p in fc ; ::_thesis: p in c
then consider x, y being set such that
A230: [x,y] = p by RELAT_1:def_1;
A231: x in dom fc by A229, A230, FUNCT_1:1;
A232: y = fc . x by A229, A230, FUNCT_1:1;
consider kk being Element of NAT such that
A233: x = kk and
A234: m <= kk and
A235: kk <= len c by A224, A231;
1 <= kk by A220, A234, XXREAL_0:2;
then A236: x in dom c by A233, A235, FINSEQ_3:25;
y = c . kk by A224, A225, A231, A232, A233;
hence p in c by A230, A233, A236, FUNCT_1:1; ::_thesis: verum
end;
then reconsider fc = fc as Subset of c ;
take fc ; ::_thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
set domfvs = { k where k is Element of NAT : ( m <= k & k <= len vs ) } ;
deffunc H2( set ) -> set = vs . $1;
consider fvs being Function such that
A237: dom fvs = { k where k is Element of NAT : ( m <= k & k <= len vs ) } and
A238: for x being set st x in { k where k is Element of NAT : ( m <= k & k <= len vs ) } holds
fvs . x = H2(x) from FUNCT_1:sch_3();
{ k where k is Element of NAT : ( m <= k & k <= len vs ) } c= Seg (len vs)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m <= k & k <= len vs ) } or x in Seg (len vs) )
assume x in { k where k is Element of NAT : ( m <= k & k <= len vs ) } ; ::_thesis: x in Seg (len vs)
then consider kk being Element of NAT such that
A239: x = kk and
A240: m <= kk and
A241: kk <= len vs ;
1 <= kk by A220, A240, XXREAL_0:2;
hence x in Seg (len vs) by A239, A241, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider fvs = fvs as FinSubsequence by A237, FINSEQ_1:def_12;
fvs c= vs
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fvs or p in vs )
assume A242: p in fvs ; ::_thesis: p in vs
then consider x, y being set such that
A243: [x,y] = p by RELAT_1:def_1;
A244: x in dom fvs by A242, A243, FUNCT_1:1;
A245: y = fvs . x by A242, A243, FUNCT_1:1;
consider kk being Element of NAT such that
A246: x = kk and
A247: m <= kk and
A248: kk <= len vs by A237, A244;
1 <= kk by A220, A247, XXREAL_0:2;
then A249: x in dom vs by A246, A248, FINSEQ_3:25;
y = vs . kk by A237, A238, A244, A245, A246;
hence p in vs by A243, A246, A249, FUNCT_1:1; ::_thesis: verum
end;
then reconsider fvs = fvs as Subset of vs ;
take fvs ; ::_thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
take c1 = c2; ::_thesis: ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
take p1 = (m,((len c) + 1)) -cut vs; ::_thesis: ( len c1 < len c & p1 is_oriented_vertex_seq_of c1 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )
A250: (len c2) + m = (len c) + 1 by A4, A5, A8, A217, Lm2;
A251: m - m <= (len c) - m by A219, XREAL_1:9;
1 - 1 <= m - 1 by A220, XREAL_1:9;
then m -' 1 = m - 1 by XREAL_0:def_2;
then reconsider m1 = m - 1 as Element of NAT ;
A252: m = m1 + 1 ;
(len c2) -' 1 = (len c2) - 1 by A250, A251, XREAL_0:def_2;
then reconsider lc21 = (len c2) - 1 as Element of NAT ;
A253: m + lc21 = m1 + (len c2) ;
A254: m <= ((len c) + 1) + 1 by A5, A8, NAT_1:12;
A255: (len c) + 1 <= len vs by A2, Def5;
then A256: (len ((m,((len c) + 1)) -cut vs)) + m = ((len c) + 1) + 1 by A4, A217, A254, Lm2;
then len ((m,((len c) + 1)) -cut vs) = (((len c) - m) + 1) + 1 ;
then A257: 1 <= len ((m,((len c) + 1)) -cut vs) by A250, NAT_1:12;
A258: len c2 = (len c) + ((- m) + 1) by A250;
1 - 1 < m - 1 by A220, XREAL_1:9;
then 0 < - (- (m - 1)) ;
then - (m - 1) < 0 ;
hence A259: len c1 < len c by A258, XREAL_1:30; ::_thesis: ( p1 is_oriented_vertex_seq_of c1 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )
thus p1 is_oriented_vertex_seq_of c1 by A2, A221, A222, Th13; ::_thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )
len p1 = (len c1) + 1 by A223, Def5;
hence len p1 < len vs by A8, A259, XREAL_1:6; ::_thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )
thus vs . 1 = p1 . 1 by A4, A5, A6, A8, A217, GRAPH_2:12; ::_thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c1 & Seq fvs = p1 )
thus vs . (len vs) = p1 . (len p1) by A4, A5, A8, A217, GRAPH_2:12; ::_thesis: ( Seq fc = c1 & Seq fvs = p1 )
A260: { k where k is Element of NAT : ( m <= k & k <= len c ) } c= Seg (len c)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m <= k & k <= len c ) } or x in Seg (len c) )
assume x in { k where k is Element of NAT : ( m <= k & k <= len c ) } ; ::_thesis: x in Seg (len c)
then consider k being Element of NAT such that
A261: x = k and
A262: m <= k and
A263: k <= len c ;
1 <= k by A220, A262, XXREAL_0:2;
hence x in Seg (len c) by A261, A263, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider domfc = { k where k is Element of NAT : ( m <= k & k <= len c ) } as finite set by FINSET_1:1;
(len c2) -' 1 = (len c2) - 1 by A250, A251, XREAL_0:def_2;
then reconsider lc21 = (len c2) - 1 as Element of NAT ;
m + lc21 = len c by A250;
then A264: card domfc = ((len c2) + (- 1)) + 1 by GRAPH_2:4
.= len c2 ;
A265: len (Sgm domfc) = card domfc by A260, FINSEQ_3:39;
A266: rng (Sgm domfc) c= dom fc by A224, A260, FINSEQ_1:def_13;
set SR = Sgm domfc;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in_c2_implies_p_in_fc_*_(Sgm_domfc)_)_&_(_p_in_fc_*_(Sgm_domfc)_implies_p_in_c2_)_)
let p be set ; ::_thesis: ( ( p in c2 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c2 ) )
hereby ::_thesis: ( p in fc * (Sgm domfc) implies p in c2 )
assume A267: p in c2 ; ::_thesis: p in fc * (Sgm domfc)
then consider x, y being set such that
A268: p = [x,y] by RELAT_1:def_1;
A269: x in dom c2 by A267, A268, FUNCT_1:1;
A270: y = c2 . x by A267, A268, FUNCT_1:1;
reconsider k = x as Element of NAT by A269;
A271: 1 <= k by A269, FINSEQ_3:25;
A272: k <= len c2 by A269, FINSEQ_3:25;
A273: x in dom (Sgm domfc) by A264, A265, A269, FINSEQ_3:29;
A274: m1 + k = (Sgm domfc) . k by A250, A252, A253, A271, A272, GRAPH_2:5;
A275: (Sgm domfc) . k in rng (Sgm domfc) by A273, FUNCT_1:def_3;
then A276: x in dom (fc * (Sgm domfc)) by A266, A273, FUNCT_1:11;
0 + 1 <= k by A269, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A277: i < len c2 and
A278: k = i + 1 by A272, GRAPH_2:1;
(fc * (Sgm domfc)) . x = fc . (m1 + k) by A274, A276, FUNCT_1:12
.= c . (m + i) by A266, A274, A275, A278, GRFUNC_1:2
.= y by A4, A5, A8, A217, A270, A277, A278, Lm2 ;
hence p in fc * (Sgm domfc) by A268, A276, FUNCT_1:1; ::_thesis: verum
end;
assume A279: p in fc * (Sgm domfc) ; ::_thesis: p in c2
then consider x, y being set such that
A280: p = [x,y] by RELAT_1:def_1;
A281: x in dom (fc * (Sgm domfc)) by A279, A280, FUNCT_1:1;
A282: y = (fc * (Sgm domfc)) . x by A279, A280, FUNCT_1:1;
A283: x in dom (Sgm domfc) by A281, FUNCT_1:11;
A284: (Sgm domfc) . x in dom fc by A281, FUNCT_1:11;
reconsider k = x as Element of NAT by A283;
A285: k in dom c2 by A264, A265, A283, FINSEQ_3:29;
A286: 1 <= k by A283, FINSEQ_3:25;
A287: k <= len c2 by A264, A265, A283, FINSEQ_3:25;
then A288: m1 + k = (Sgm domfc) . k by A250, A252, A253, A286, GRAPH_2:5;
0 + 1 <= k by A283, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A289: i < len c2 and
A290: k = i + 1 by A287, GRAPH_2:1;
c2 . k = c . ((m1 + 1) + i) by A4, A5, A8, A217, A289, A290, Lm2
.= fc . ((Sgm domfc) . k) by A284, A288, A290, GRFUNC_1:2
.= y by A282, A283, FUNCT_1:13 ;
hence p in c2 by A280, A285, FUNCT_1:1; ::_thesis: verum
end;
then c2 = fc * (Sgm domfc) by TARSKI:1;
hence Seq fc = c1 by A224, FINSEQ_1:def_14; ::_thesis: Seq fvs = p1
A291: { k where k is Element of NAT : ( m <= k & k <= len vs ) } c= Seg (len vs)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( m <= k & k <= len vs ) } or x in Seg (len vs) )
assume x in { k where k is Element of NAT : ( m <= k & k <= len vs ) } ; ::_thesis: x in Seg (len vs)
then consider k being Element of NAT such that
A292: x = k and
A293: m <= k and
A294: k <= len vs ;
1 <= k by A220, A293, XXREAL_0:2;
hence x in Seg (len vs) by A292, A294, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider domfvs = { k where k is Element of NAT : ( m <= k & k <= len vs ) } as finite set by FINSET_1:1;
1 - 1 <= (len ((m,((len c) + 1)) -cut vs)) - 1 by A257, XREAL_1:9;
then (len ((m,((len c) + 1)) -cut vs)) -' 1 = (len ((m,((len c) + 1)) -cut vs)) - 1 by XREAL_0:def_2;
then reconsider lp21 = (len ((m,((len c) + 1)) -cut vs)) - 1 as Element of NAT ;
A295: m + lp21 = (len c) + 1 by A256;
A296: m + lp21 = m1 + (len ((m,((len c) + 1)) -cut vs)) ;
A297: card domfvs = ((len ((m,((len c) + 1)) -cut vs)) + (- 1)) + 1 by A8, A295, GRAPH_2:4
.= len ((m,((len c) + 1)) -cut vs) ;
A298: len (Sgm domfvs) = card domfvs by A291, FINSEQ_3:39;
A299: rng (Sgm domfvs) c= dom fvs by A237, A291, FINSEQ_1:def_13;
set SR = Sgm domfvs;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in_(m,((len_c)_+_1))_-cut_vs_implies_p_in_fvs_*_(Sgm_domfvs)_)_&_(_p_in_fvs_*_(Sgm_domfvs)_implies_p_in_(m,((len_c)_+_1))_-cut_vs_)_)
let p be set ; ::_thesis: ( ( p in (m,((len c) + 1)) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in (m,((len c) + 1)) -cut vs ) )
hereby ::_thesis: ( p in fvs * (Sgm domfvs) implies p in (m,((len c) + 1)) -cut vs )
assume A300: p in (m,((len c) + 1)) -cut vs ; ::_thesis: p in fvs * (Sgm domfvs)
then consider x, y being set such that
A301: p = [x,y] by RELAT_1:def_1;
A302: x in dom ((m,((len c) + 1)) -cut vs) by A300, A301, FUNCT_1:1;
A303: y = ((m,((len c) + 1)) -cut vs) . x by A300, A301, FUNCT_1:1;
reconsider k = x as Element of NAT by A302;
A304: 1 <= k by A302, FINSEQ_3:25;
A305: k <= len ((m,((len c) + 1)) -cut vs) by A302, FINSEQ_3:25;
A306: x in dom (Sgm domfvs) by A297, A298, A302, FINSEQ_3:29;
A307: m1 + k = (Sgm domfvs) . k by A8, A252, A256, A296, A304, A305, GRAPH_2:5;
A308: (Sgm domfvs) . k in rng (Sgm domfvs) by A306, FUNCT_1:def_3;
then A309: x in dom (fvs * (Sgm domfvs)) by A299, A306, FUNCT_1:11;
0 + 1 <= k by A302, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A310: i < len ((m,((len c) + 1)) -cut vs) and
A311: k = i + 1 by A305, GRAPH_2:1;
(fvs * (Sgm domfvs)) . x = fvs . (m1 + k) by A307, A309, FUNCT_1:12
.= vs . (m + i) by A299, A307, A308, A311, GRFUNC_1:2
.= y by A4, A217, A254, A255, A303, A310, A311, Lm2 ;
hence p in fvs * (Sgm domfvs) by A301, A309, FUNCT_1:1; ::_thesis: verum
end;
assume A312: p in fvs * (Sgm domfvs) ; ::_thesis: p in (m,((len c) + 1)) -cut vs
then consider x, y being set such that
A313: p = [x,y] by RELAT_1:def_1;
A314: x in dom (fvs * (Sgm domfvs)) by A312, A313, FUNCT_1:1;
A315: y = (fvs * (Sgm domfvs)) . x by A312, A313, FUNCT_1:1;
A316: x in dom (Sgm domfvs) by A314, FUNCT_1:11;
A317: (Sgm domfvs) . x in dom fvs by A314, FUNCT_1:11;
reconsider k = x as Element of NAT by A316;
A318: k in dom ((m,((len c) + 1)) -cut vs) by A297, A298, A316, FINSEQ_3:29;
A319: 1 <= k by A316, FINSEQ_3:25;
A320: k <= len ((m,((len c) + 1)) -cut vs) by A297, A298, A316, FINSEQ_3:25;
then A321: m1 + k = (Sgm domfvs) . k by A8, A252, A256, A296, A319, GRAPH_2:5;
0 + 1 <= k by A316, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A322: i < len ((m,((len c) + 1)) -cut vs) and
A323: k = i + 1 by A320, GRAPH_2:1;
((m,((len c) + 1)) -cut vs) . k = vs . ((m1 + 1) + i) by A4, A217, A254, A255, A322, A323, Lm2
.= fvs . ((Sgm domfvs) . k) by A317, A321, A323, GRFUNC_1:2
.= y by A315, A316, FUNCT_1:13 ;
hence p in (m,((len c) + 1)) -cut vs by A313, A318, FUNCT_1:1; ::_thesis: verum
end;
then (m,((len c) + 1)) -cut vs = fvs * (Sgm domfvs) by TARSKI:1;
hence Seq fvs = p1 by A237, FINSEQ_1:def_14; ::_thesis: verum
end;
supposeA324: ( n <> 1 & m = len vs ) ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
then 1 < n by A3, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then A325: (1 + 1) - 1 <= n - 1 by XREAL_1:9;
n < len vs by A4, A5, XXREAL_0:2;
then A326: n - 1 < ((len c) + 1) - 1 by A8, XREAL_1:9;
A327: 1 <= n1 + 1 by NAT_1:12;
reconsider c1 = (1,n1) -cut c as oriented Chain of G by A11, A325, A326, Th12;
set pp = (1,n) -cut vs;
A328: n <= len vs by A4, A5, XXREAL_0:2;
A329: (1,n) -cut vs is_oriented_vertex_seq_of c1 by A2, A12, A325, A326, Th13;
then A330: len ((1,n) -cut vs) = (len c1) + 1 by Def5;
set domfc = { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } ;
deffunc H1( set ) -> set = c . $1;
consider fc being Function such that
A331: dom fc = { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } and
A332: for x being set st x in { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } holds
fc . x = H1(x) from FUNCT_1:sch_3();
{ k where k is Element of NAT : ( 1 <= k & k <= n1 ) } c= Seg (len c)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } or x in Seg (len c) )
assume x in { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } ; ::_thesis: x in Seg (len c)
then consider kk being Element of NAT such that
A333: x = kk and
A334: 1 <= kk and
A335: kk <= n1 ;
kk <= len c by A11, A326, A335, XXREAL_0:2;
hence x in Seg (len c) by A333, A334, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider fc = fc as FinSubsequence by A331, FINSEQ_1:def_12;
fc c= c
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fc or p in c )
assume A336: p in fc ; ::_thesis: p in c
then consider x, y being set such that
A337: [x,y] = p by RELAT_1:def_1;
A338: x in dom fc by A336, A337, FUNCT_1:1;
A339: y = fc . x by A336, A337, FUNCT_1:1;
consider kk being Element of NAT such that
A340: x = kk and
A341: 1 <= kk and
A342: kk <= n1 by A331, A338;
kk <= len c by A11, A326, A342, XXREAL_0:2;
then A343: x in dom c by A340, A341, FINSEQ_3:25;
y = c . kk by A331, A332, A338, A339, A340;
hence p in c by A337, A340, A343, FUNCT_1:1; ::_thesis: verum
end;
then reconsider fc = fc as Subset of c ;
take fc ; ::_thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
set domfvs = { k where k is Element of NAT : ( 1 <= k & k <= n ) } ;
deffunc H2( set ) -> set = vs . $1;
consider fvs being Function such that
A344: dom fvs = { k where k is Element of NAT : ( 1 <= k & k <= n ) } and
A345: for x being set st x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } holds
fvs . x = H2(x) from FUNCT_1:sch_3();
{ k where k is Element of NAT : ( 1 <= k & k <= n ) } c= Seg (len vs)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } or x in Seg (len vs) )
assume x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } ; ::_thesis: x in Seg (len vs)
then consider kk being Element of NAT such that
A346: x = kk and
A347: 1 <= kk and
A348: kk <= n ;
kk <= len vs by A328, A348, XXREAL_0:2;
hence x in Seg (len vs) by A346, A347, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider fvs = fvs as FinSubsequence by A344, FINSEQ_1:def_12;
fvs c= vs
proof
let p be set ; :: according to TARSKI:def_3 ::_thesis: ( not p in fvs or p in vs )
assume A349: p in fvs ; ::_thesis: p in vs
then consider x, y being set such that
A350: [x,y] = p by RELAT_1:def_1;
A351: x in dom fvs by A349, A350, FUNCT_1:1;
A352: y = fvs . x by A349, A350, FUNCT_1:1;
consider kk being Element of NAT such that
A353: x = kk and
A354: 1 <= kk and
A355: kk <= n by A344, A351;
kk <= len vs by A328, A355, XXREAL_0:2;
then A356: x in dom vs by A353, A354, FINSEQ_3:25;
y = vs . kk by A344, A345, A351, A352, A353;
hence p in vs by A350, A353, A356, FUNCT_1:1; ::_thesis: verum
end;
then reconsider fvs = fvs as Subset of vs ;
take fvs ; ::_thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( len c1 < len c & vs1 is_oriented_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )
take c9 = c1; ::_thesis: ex vs1 being FinSequence of the carrier of G st
( len c9 < len c & vs1 is_oriented_vertex_seq_of c9 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c9 & Seq fvs = vs1 )
take p1 = (1,n) -cut vs; ::_thesis: ( len c9 < len c & p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
A357: (len c1) + 1 = n1 + 1 by A11, A326, A327, Lm2;
then A358: len c1 = n - 1 by A10, XREAL_0:def_2;
thus len c9 < len c by A10, A326, A357, XREAL_0:def_2; ::_thesis: ( p1 is_oriented_vertex_seq_of c9 & len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
thus p1 is_oriented_vertex_seq_of c9 by A2, A12, A325, A326, Th13; ::_thesis: ( len p1 < len vs & vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
len p1 = (len c1) + 1 by A329, Def5;
hence len p1 < len vs by A4, A5, A358, XXREAL_0:2; ::_thesis: ( vs . 1 = p1 . 1 & vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
thus vs . 1 = p1 . 1 by A3, A328, GRAPH_2:12; ::_thesis: ( vs . (len vs) = p1 . (len p1) & Seq fc = c9 & Seq fvs = p1 )
thus vs . (len vs) = p1 . (len p1) by A3, A4, A6, A324, GRAPH_2:12; ::_thesis: ( Seq fc = c9 & Seq fvs = p1 )
{ k where k is Element of NAT : ( 1 <= k & k <= n1 ) } c= Seg (len c)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } or x in Seg (len c) )
assume x in { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } ; ::_thesis: x in Seg (len c)
then consider k being Element of NAT such that
A359: x = k and
A360: 1 <= k and
A361: k <= n1 ;
k <= len c by A11, A326, A361, XXREAL_0:2;
hence x in Seg (len c) by A359, A360, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider domfc = { k where k is Element of NAT : ( 1 <= k & k <= n1 ) } as finite set by FINSET_1:1;
domfc = Seg n1 by FINSEQ_1:def_1;
then A362: Sgm domfc = idseq n1 by FINSEQ_3:48;
then A363: dom (Sgm domfc) = Seg n1 by RELAT_1:45;
set SL = Sgm domfc;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in_c1_implies_p_in_fc_*_(Sgm_domfc)_)_&_(_p_in_fc_*_(Sgm_domfc)_implies_p_in_c1_)_)
let p be set ; ::_thesis: ( ( p in c1 implies p in fc * (Sgm domfc) ) & ( p in fc * (Sgm domfc) implies p in c1 ) )
hereby ::_thesis: ( p in fc * (Sgm domfc) implies p in c1 )
assume A364: p in c1 ; ::_thesis: p in fc * (Sgm domfc)
then consider x, y being set such that
A365: p = [x,y] by RELAT_1:def_1;
A366: x in dom c1 by A364, A365, FUNCT_1:1;
A367: y = c1 . x by A364, A365, FUNCT_1:1;
reconsider k = x as Element of NAT by A366;
A368: 1 <= k by A366, FINSEQ_3:25;
A369: k <= len c1 by A366, FINSEQ_3:25;
then A370: x in dom (Sgm domfc) by A357, A363, A368, FINSEQ_1:1;
then A371: k = (Sgm domfc) . k by A362, A363, FUNCT_1:18;
A372: k in domfc by A357, A368, A369;
then A373: x in dom (fc * (Sgm domfc)) by A331, A370, A371, FUNCT_1:11;
0 + 1 <= k by A366, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A374: i < n1 and
A375: k = i + 1 by A357, A369, GRAPH_2:1;
(fc * (Sgm domfc)) . x = fc . k by A371, A373, FUNCT_1:12
.= c . (1 + i) by A331, A372, A375, GRFUNC_1:2
.= y by A11, A326, A327, A357, A367, A374, A375, Lm2 ;
hence p in fc * (Sgm domfc) by A365, A373, FUNCT_1:1; ::_thesis: verum
end;
assume A376: p in fc * (Sgm domfc) ; ::_thesis: p in c1
then consider x, y being set such that
A377: p = [x,y] by RELAT_1:def_1;
A378: x in dom (fc * (Sgm domfc)) by A376, A377, FUNCT_1:1;
A379: y = (fc * (Sgm domfc)) . x by A376, A377, FUNCT_1:1;
A380: (fc * (Sgm domfc)) . x = fc . ((Sgm domfc) . x) by A378, FUNCT_1:12;
A381: x in dom (Sgm domfc) by A378, FUNCT_1:11;
then x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n1 ) } by A363, FINSEQ_1:def_1;
then consider k being Element of NAT such that
A382: k = x and
A383: 1 <= k and
A384: k <= n1 ;
A385: k in dom fc by A331, A383, A384;
A386: k = (Sgm domfc) . k by A362, A363, A381, A382, FUNCT_1:18;
A387: k in dom c1 by A357, A383, A384, FINSEQ_3:25;
0 + 1 <= k by A383;
then ex i being Element of NAT st
( 0 <= i & i < n1 & k = i + 1 ) by A384, GRAPH_2:1;
then c1 . k = c . k by A11, A326, A327, A357, Lm2
.= y by A379, A380, A382, A385, A386, GRFUNC_1:2 ;
hence p in c1 by A377, A382, A387, FUNCT_1:1; ::_thesis: verum
end;
then c1 = fc * (Sgm domfc) by TARSKI:1;
hence Seq fc = c9 by A331, FINSEQ_1:def_14; ::_thesis: Seq fvs = p1
{ k where k is Element of NAT : ( 1 <= k & k <= n ) } c= Seg (len vs)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } or x in Seg (len vs) )
assume x in { k where k is Element of NAT : ( 1 <= k & k <= n ) } ; ::_thesis: x in Seg (len vs)
then consider k being Element of NAT such that
A388: x = k and
A389: 1 <= k and
A390: k <= n ;
k <= len vs by A328, A390, XXREAL_0:2;
hence x in Seg (len vs) by A388, A389, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider domfvs = { k where k is Element of NAT : ( 1 <= k & k <= n ) } as finite set by FINSET_1:1;
domfvs = Seg n by FINSEQ_1:def_1;
then A391: Sgm domfvs = idseq n by FINSEQ_3:48;
then A392: dom (Sgm domfvs) = Seg n by RELAT_1:45;
set SL = Sgm domfvs;
now__::_thesis:_for_p_being_set_holds_
(_(_p_in_(1,n)_-cut_vs_implies_p_in_fvs_*_(Sgm_domfvs)_)_&_(_p_in_fvs_*_(Sgm_domfvs)_implies_p_in_(1,n)_-cut_vs_)_)
let p be set ; ::_thesis: ( ( p in (1,n) -cut vs implies p in fvs * (Sgm domfvs) ) & ( p in fvs * (Sgm domfvs) implies p in (1,n) -cut vs ) )
hereby ::_thesis: ( p in fvs * (Sgm domfvs) implies p in (1,n) -cut vs )
assume A393: p in (1,n) -cut vs ; ::_thesis: p in fvs * (Sgm domfvs)
then consider x, y being set such that
A394: p = [x,y] by RELAT_1:def_1;
A395: x in dom ((1,n) -cut vs) by A393, A394, FUNCT_1:1;
A396: y = ((1,n) -cut vs) . x by A393, A394, FUNCT_1:1;
reconsider k = x as Element of NAT by A395;
A397: 1 <= k by A395, FINSEQ_3:25;
A398: k <= len ((1,n) -cut vs) by A395, FINSEQ_3:25;
then A399: x in dom (Sgm domfvs) by A330, A358, A392, A397, FINSEQ_1:1;
then A400: k = (Sgm domfvs) . k by A391, A392, FUNCT_1:18;
A401: k in domfvs by A330, A358, A397, A398;
then A402: x in dom (fvs * (Sgm domfvs)) by A344, A399, A400, FUNCT_1:11;
0 + 1 <= k by A395, FINSEQ_3:25;
then consider i being Element of NAT such that
0 <= i and
A403: i < n and
A404: k = i + 1 by A330, A358, A398, GRAPH_2:1;
(fvs * (Sgm domfvs)) . x = fvs . k by A400, A402, FUNCT_1:12
.= vs . (1 + i) by A344, A401, A404, GRFUNC_1:2
.= y by A3, A328, A330, A358, A396, A403, A404, GRAPH_2:def_1 ;
hence p in fvs * (Sgm domfvs) by A394, A402, FUNCT_1:1; ::_thesis: verum
end;
assume A405: p in fvs * (Sgm domfvs) ; ::_thesis: p in (1,n) -cut vs
then consider x, y being set such that
A406: p = [x,y] by RELAT_1:def_1;
A407: x in dom (fvs * (Sgm domfvs)) by A405, A406, FUNCT_1:1;
A408: y = (fvs * (Sgm domfvs)) . x by A405, A406, FUNCT_1:1;
A409: (fvs * (Sgm domfvs)) . x = fvs . ((Sgm domfvs) . x) by A407, FUNCT_1:12;
A410: x in dom (Sgm domfvs) by A407, FUNCT_1:11;
then x in { kk where kk is Element of NAT : ( 1 <= kk & kk <= n ) } by A392, FINSEQ_1:def_1;
then consider k being Element of NAT such that
A411: k = x and
A412: 1 <= k and
A413: k <= n ;
A414: k in dom fvs by A344, A412, A413;
A415: k = (Sgm domfvs) . k by A391, A392, A410, A411, FUNCT_1:18;
A416: k in dom ((1,n) -cut vs) by A330, A358, A412, A413, FINSEQ_3:25;
0 + 1 <= k by A412;
then ex i being Element of NAT st
( 0 <= i & i < n & k = i + 1 ) by A413, GRAPH_2:1;
then ((1,n) -cut vs) . k = vs . k by A3, A328, A330, A358, GRAPH_2:def_1
.= y by A408, A409, A411, A414, A415, GRFUNC_1:2 ;
hence p in (1,n) -cut vs by A406, A411, A416, FUNCT_1:1; ::_thesis: verum
end;
then (1,n) -cut vs = fvs * (Sgm domfvs) by TARSKI:1;
hence Seq fvs = p1 by A344, FINSEQ_1:def_14; ::_thesis: verum
end;
end;
end;
theorem :: GRAPH_4:21
for G being Graph
for vs being FinSequence of the carrier of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
proof
let G be Graph; ::_thesis: for vs being FinSequence of the carrier of G
for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
let vs be FinSequence of the carrier of G; ::_thesis: for c being oriented Chain of G st vs is_oriented_vertex_seq_of c holds
ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
let c be oriented Chain of G; ::_thesis: ( vs is_oriented_vertex_seq_of c implies ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) )
assume A1: vs is_oriented_vertex_seq_of c ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
percases ( c is Simple or not c is Simple ) ;
supposeA2: c is Simple ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
reconsider fc = c as Subset of c by GRAPH_2:26;
reconsider fvs = vs as Subset of vs by GRAPH_2:26;
reconsider sc = c as oriented simple Chain of G by A2, Th19;
take fc ; ::_thesis: ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
take fvs ; ::_thesis: ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
take sc ; ::_thesis: ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
take vs ; ::_thesis: ( Seq fc = sc & Seq fvs = vs & vs is_oriented_vertex_seq_of sc & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) )
thus ( Seq fc = sc & Seq fvs = vs ) by FINSEQ_3:116; ::_thesis: ( vs is_oriented_vertex_seq_of sc & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) )
thus vs is_oriented_vertex_seq_of sc by A1; ::_thesis: ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) )
thus ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) ; ::_thesis: verum
end;
supposeA3: not c is Simple ; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
defpred S1[ Nat] means ex fc being Subset of c ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = c1 & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = $1 & not c1 is Simple );
S1[ len c]
proof
reconsider fc = c as Subset of c by GRAPH_2:26;
reconsider fvs = vs as Subset of vs by GRAPH_2:26;
take fc ; ::_thesis: ex fvs being Subset of vs ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = c1 & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = len c & not c1 is Simple )
take fvs ; ::_thesis: ex c1 being oriented Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = c1 & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c1 & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c1 = len c & not c1 is Simple )
take c ; ::_thesis: ex vs1 being FinSequence of the carrier of G st
( Seq fc = c & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of c & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & len c = len c & not c is Simple )
take vs ; ::_thesis: ( Seq fc = c & Seq fvs = vs & vs is_oriented_vertex_seq_of c & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & not c is Simple )
thus ( Seq fc = c & Seq fvs = vs ) by FINSEQ_3:116; ::_thesis: ( vs is_oriented_vertex_seq_of c & vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & not c is Simple )
thus vs is_oriented_vertex_seq_of c by A1; ::_thesis: ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) & len c = len c & not c is Simple )
thus ( vs . 1 = vs . 1 & vs . (len vs) = vs . (len vs) ) ; ::_thesis: ( len c = len c & not c is Simple )
thus ( len c = len c & not c is Simple ) by A3; ::_thesis: verum
end;
then A4: ex k being Nat st S1[k] ;
consider k being Nat such that
A5: ( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch_5(A4);
consider fc being Subset of c, fvs being Subset of vs, c1 being oriented Chain of G, vs1 being FinSequence of the carrier of G such that
A6: Seq fc = c1 and
A7: Seq fvs = vs1 and
A8: vs1 is_oriented_vertex_seq_of c1 and
A9: vs . 1 = vs1 . 1 and
A10: vs . (len vs) = vs1 . (len vs1) and
A11: len c1 = k and
A12: not c1 is Simple by A5;
consider fc1 being Subset of c1, fvs1 being Subset of vs1, c2 being oriented Chain of G, vs2 being FinSequence of the carrier of G such that
A13: len c2 < len c1 and
A14: vs2 is_oriented_vertex_seq_of c2 and
len vs2 < len vs1 and
A15: vs1 . 1 = vs2 . 1 and
A16: vs1 . (len vs1) = vs2 . (len vs2) and
A17: Seq fc1 = c2 and
A18: Seq fvs1 = vs2 by A8, A12, Th20;
reconsider fc9 = fc | (rng ((Sgm (dom fc)) | (dom fc1))) as Subset of c by GRAPH_2:27;
A19: Seq fc9 = c2 by A6, A17, GRAPH_2:28;
reconsider fvs9 = fvs | (rng ((Sgm (dom fvs)) | (dom fvs1))) as Subset of vs by GRAPH_2:27;
A20: Seq fvs9 = vs2 by A7, A18, GRAPH_2:28;
now__::_thesis:_(_c2_is_oriented_Simple_Chain_of_G_implies_ex_fc9_being_Subset_of_c_ex_sc_being_oriented_simple_Chain_of_G_ex_fc_being_Subset_of_c_ex_fvs_being_Subset_of_vs_ex_sc_being_oriented_simple_Chain_of_G_ex_vs1_being_FinSequence_of_the_carrier_of_G_st_
(_Seq_fc_=_sc_&_Seq_fvs_=_vs1_&_vs1_is_oriented_vertex_seq_of_sc_&_vs_._1_=_vs1_._1_&_vs_._(len_vs)_=_vs1_._(len_vs1)_)_)
assume c2 is oriented Simple Chain of G ; ::_thesis: ex fc9 being Subset of c ex sc being oriented simple Chain of G ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
then reconsider sc = c2 as oriented simple Chain of G by Th19;
take fc9 = fc9; ::_thesis: ex sc being oriented simple Chain of G ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
take sc = sc; ::_thesis: ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )
Seq fc9 = sc by A6, A17, GRAPH_2:28;
hence ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) by A9, A10, A14, A15, A16, A20; ::_thesis: verum
end;
hence ex fc being Subset of c ex fvs being Subset of vs ex sc being oriented simple Chain of G ex vs1 being FinSequence of the carrier of G st
( Seq fc = sc & Seq fvs = vs1 & vs1 is_oriented_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) ) by A5, A9, A10, A11, A13, A14, A15, A16, A19, A20; ::_thesis: verum
end;
end;
end;
theorem :: GRAPH_4:22
for p being FinSequence
for n being Element of NAT
for G being Graph st p is OrientedPath of G holds
p | (Seg n) is OrientedPath of G
proof
let p be FinSequence; ::_thesis: for n being Element of NAT
for G being Graph st p is OrientedPath of G holds
p | (Seg n) is OrientedPath of G
let n be Element of NAT ; ::_thesis: for G being Graph st p is OrientedPath of G holds
p | (Seg n) is OrientedPath of G
let G be Graph; ::_thesis: ( p is OrientedPath of G implies p | (Seg n) is OrientedPath of G )
assume A1: p is OrientedPath of G ; ::_thesis: p | (Seg n) is OrientedPath of G
then reconsider p9 = p | (Seg n) as oriented Chain of G by Th16;
reconsider q = p | (Seg n) as FinSequence by FINSEQ_1:15;
now__::_thesis:_for_n1,_m1_being_Element_of_NAT_st_1_<=_n1_&_n1_<_m1_&_m1_<=_len_q_holds_
q_._n1_<>_q_._m1
let n1, m1 be Element of NAT ; ::_thesis: ( 1 <= n1 & n1 < m1 & m1 <= len q implies q . n1 <> q . m1 )
assume that
A2: 1 <= n1 and
A3: n1 < m1 and
A4: m1 <= len q ; ::_thesis: q . n1 <> q . m1
1 < m1 by A2, A3, XXREAL_0:2;
then m1 in dom q by A4, FINSEQ_3:25;
then A5: q . m1 = p . m1 by FUNCT_1:47;
n1 < len q by A3, A4, XXREAL_0:2;
then n1 in dom q by A2, FINSEQ_3:25;
then A6: q . n1 = p . n1 by FUNCT_1:47;
dom q c= dom p by RELAT_1:60;
then dom q c= Seg (len p) by FINSEQ_1:def_3;
then Seg (len q) c= Seg (len p) by FINSEQ_1:def_3;
then len q <= len p by FINSEQ_1:5;
then m1 <= len p by A4, XXREAL_0:2;
hence q . n1 <> q . m1 by A1, A2, A3, A5, A6, GRAPH_1:def_16; ::_thesis: verum
end;
then p9 is Path of G by GRAPH_1:def_16;
hence p | (Seg n) is OrientedPath of G ; ::_thesis: verum
end;
theorem Th23: :: GRAPH_4:23
for G being Graph
for sc being oriented simple Chain of G holds sc is OrientedPath of G
proof
let G be Graph; ::_thesis: for sc being oriented simple Chain of G holds sc is OrientedPath of G
let sc be oriented simple Chain of G; ::_thesis: sc is OrientedPath of G
assume sc is not OrientedPath of G ; ::_thesis: contradiction
then consider m, n being Element of NAT such that
A1: 1 <= m and
A2: m < n and
A3: n <= len sc and
A4: sc . m = sc . n by GRAPH_1:def_16;
sc is Simple by Th18;
then consider vs being FinSequence of the carrier of G such that
A5: vs is_oriented_vertex_seq_of sc 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 Def7;
A7: len vs = (len sc) + 1 by A5, Def5;
A8: m <= len sc by A2, A3, XXREAL_0:2;
A9: 1 <= n by A1, A2, XXREAL_0:2;
A10: n <= len vs by A3, A7, NAT_1:12;
A11: m + 1 < n + 1 by A2, XREAL_1:6;
A12: n + 1 <= len vs by A3, A7, XREAL_1:6;
A13: m < n + 1 by A11, NAT_1:12;
set v1 = vs /. m;
set v2 = vs /. (m + 1);
A14: sc . m orientedly_joins vs /. m,vs /. (m + 1) by A1, A5, A8, Def5;
set v19 = vs /. n;
set v29 = vs /. (n + 1);
A15: sc . n orientedly_joins vs /. n,vs /. (n + 1) by A3, A5, A9, Def5;
then A16: vs /. m = vs /. n by A4, A14, Th2;
A17: vs /. (m + 1) = vs /. (n + 1) by A4, A14, A15, Th2;
A18: m <= len vs by A12, A13, XXREAL_0:2;
A19: m + 1 <= len vs by A11, A12, XXREAL_0:2;
A20: vs /. m = vs . m by A1, A18, FINSEQ_4:15;
A21: vs /. (m + 1) = vs . (m + 1) by A19, FINSEQ_4:15, NAT_1:12;
A22: vs /. n = vs . n by A9, A10, FINSEQ_4:15;
A23: vs /. (n + 1) = vs . (n + 1) by A12, FINSEQ_4:15, NAT_1:12;
m = 1 by A1, A2, A6, A10, A16, A20, A22;
hence contradiction by A6, A11, A12, A17, A21, A23; ::_thesis: verum
end;
theorem :: GRAPH_4:24
for G being Graph
for c1 being FinSequence holds
( ( c1 is oriented Simple Chain of G implies c1 is oriented simple Chain of G ) & ( c1 is oriented simple Chain of G implies c1 is oriented Simple Chain of G ) & ( c1 is oriented simple Chain of G implies c1 is OrientedPath of G ) ) by Th18, Th19, Th23;