:: by Yatsuka Nakamura and Piotr Rudnicki

::

:: Received May 13, 1995

:: Copyright (c) 1995-2017 Association of Mizar Users

theorem Th1: :: GRAPH_2:1

for m, k, n being Nat holds

( ( m + 1 <= k & k <= n ) iff ex i being Nat st

( m <= i & i < n & k = i + 1 ) )

( ( m + 1 <= k & k <= n ) iff ex i being Nat st

( m <= i & i < n & k = i + 1 ) )

proof end;

theorem Th2: :: GRAPH_2:2

for p, q being FinSequence

for n being Nat st q = p | (Seg n) holds

( len q <= len p & ( for i being Nat st 1 <= i & i <= len q holds

p . i = q . i ) )

for n being Nat st q = p | (Seg n) holds

( len q <= len p & ( for i being Nat st 1 <= i & i <= len q holds

p . i = q . i ) )

proof end;

theorem Th3: :: GRAPH_2:3

for X, Y being set

for k being Nat st X c= Seg k & Y c= dom (Sgm X) holds

(Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))

for k being Nat st X c= Seg k & Y c= dom (Sgm X) holds

(Sgm X) * (Sgm Y) = Sgm (rng ((Sgm X) | Y))

proof end;

Lm1: for m, n being Nat

for F being finite set st F = { k where k is Nat : ( m <= k & k <= m + n ) } holds

card F = n + 1

proof end;

theorem Th5: :: GRAPH_2:5

for m, n, l being Nat st 1 <= l & l <= n holds

(Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . l = m + l

(Sgm { kk where kk is Nat : ( m + 1 <= kk & kk <= m + n ) } ) . l = m + l

proof end;

definition

let p be FinSequence;

let m, n be Nat;

for b_{1} being FinSequence holds verum
;

existence

( ( 1 <= m & m <= n & n <= len p implies ex b_{1} being FinSequence st

( (len b_{1}) + m = n + 1 & ( for i being Nat st i < len b_{1} holds

b_{1} . (i + 1) = p . (m + i) ) ) ) & ( ( not 1 <= m or not m <= n or not n <= len p ) implies ex b_{1} being FinSequence st b_{1} = {} ) )

for b_{1}, b_{2} being FinSequence holds

( ( 1 <= m & m <= n & n <= len p & (len b_{1}) + m = n + 1 & ( for i being Nat st i < len b_{1} holds

b_{1} . (i + 1) = p . (m + i) ) & (len b_{2}) + m = n + 1 & ( for i being Nat st i < len b_{2} holds

b_{2} . (i + 1) = p . (m + i) ) implies b_{1} = b_{2} ) & ( ( not 1 <= m or not m <= n or not n <= len p ) & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) )

end;
let m, n be Nat;

func (m,n) -cut p -> FinSequence means :Def1: :: GRAPH_2:def 1

( (len it) + m = n + 1 & ( for i being Nat st i < len it holds

it . (i + 1) = p . (m + i) ) ) if ( 1 <= m & m <= n & n <= len p )

otherwise it = {} ;

consistency ( (len it) + m = n + 1 & ( for i being Nat st i < len it holds

it . (i + 1) = p . (m + i) ) ) if ( 1 <= m & m <= n & n <= len p )

otherwise it = {} ;

for b

existence

( ( 1 <= m & m <= n & n <= len p implies ex b

( (len b

b

proof end;

uniqueness for b

( ( 1 <= m & m <= n & n <= len p & (len b

b

b

proof end;

:: deftheorem Def1 defines -cut GRAPH_2:def 1 :

for p being FinSequence

for m, n being Nat

for b_{4} being FinSequence holds

( ( 1 <= m & m <= n & n <= len p implies ( b_{4} = (m,n) -cut p iff ( (len b_{4}) + m = n + 1 & ( for i being Nat st i < len b_{4} holds

b_{4} . (i + 1) = p . (m + i) ) ) ) ) & ( ( not 1 <= m or not m <= n or not n <= len p ) implies ( b_{4} = (m,n) -cut p iff b_{4} = {} ) ) );

for p being FinSequence

for m, n being Nat

for b

( ( 1 <= m & m <= n & n <= len p implies ( b

b

Lm2: for p being FinSequence

for m, n being Nat st 1 <= m & m <= n + 1 & n <= len p holds

( (len ((m,n) -cut p)) + m = n + 1 & ( for i being Nat st i < len ((m,n) -cut p) holds

((m,n) -cut p) . (i + 1) = p . (m + i) ) )

proof end;

theorem Th8: :: GRAPH_2:8

for p being FinSequence

for m, n, r being Nat st m <= n & n <= r & r <= len p holds

(((m + 1),n) -cut p) ^ (((n + 1),r) -cut p) = ((m + 1),r) -cut p

for m, n, r being Nat st m <= n & n <= r & r <= len p holds

(((m + 1),n) -cut p) ^ (((n + 1),r) -cut p) = ((m + 1),r) -cut p

proof end;

theorem :: GRAPH_2:9

for p being FinSequence

for m being Nat st m <= len p holds

((1,m) -cut p) ^ (((m + 1),(len p)) -cut p) = p

for m being Nat st m <= len p holds

((1,m) -cut p) ^ (((m + 1),(len p)) -cut p) = p

proof end;

theorem :: GRAPH_2:10

for p being FinSequence

for m, n being Nat st m <= n & n <= len p holds

(((1,m) -cut p) ^ (((m + 1),n) -cut p)) ^ (((n + 1),(len p)) -cut p) = p

for m, n being Nat st m <= n & n <= len p holds

(((1,m) -cut p) ^ (((m + 1),n) -cut p)) ^ (((n + 1),(len p)) -cut p) = p

proof end;

definition

let D be set ;

let p be FinSequence of D;

let m, n be Nat;

:: original: -cut

redefine func (m,n) -cut p -> FinSequence of D;

coherence

(m,n) -cut p is FinSequence of D

end;
let p be FinSequence of D;

let m, n be Nat;

:: original: -cut

redefine func (m,n) -cut p -> FinSequence of D;

coherence

(m,n) -cut p is FinSequence of D

proof end;

theorem Th12: :: GRAPH_2:12

for p being FinSequence

for m, n being Nat st 1 <= m & m <= n & n <= len p holds

( ((m,n) -cut p) . 1 = p . m & ((m,n) -cut p) . (len ((m,n) -cut p)) = p . n )

for m, n being Nat st 1 <= m & m <= n & n <= len p holds

( ((m,n) -cut p) . 1 = p . m & ((m,n) -cut p) . (len ((m,n) -cut p)) = p . n )

proof end;

definition
end;

:: deftheorem defines ^' GRAPH_2:def 2 :

for p, q being FinSequence holds p ^' q = p ^ ((2,(len q)) -cut q);

for p, q being FinSequence holds p ^' q = p ^ ((2,(len q)) -cut q);

theorem Th15: :: GRAPH_2:15

for p, q being FinSequence

for k being Nat st 1 <= k & k < len q holds

(p ^' q) . ((len p) + k) = q . (k + 1)

for k being Nat st 1 <= k & k < len q holds

(p ^' q) . ((len p) + k) = q . (k + 1)

proof end;

definition

let D be set ;

let p, q be FinSequence of D;

:: original: ^'

redefine func p ^' q -> FinSequence of D;

coherence

p ^' q is FinSequence of D

end;
let p, q be FinSequence of D;

:: original: ^'

redefine func p ^' q -> FinSequence of D;

coherence

p ^' q is FinSequence of D

proof end;

theorem :: GRAPH_2:18

for p, q being FinSequence st p <> {} & q <> {} & p . (len p) = q . 1 holds

rng (p ^' q) = (rng p) \/ (rng q)

rng (p ^' q) = (rng p) \/ (rng q)

proof end;

definition
end;

:: deftheorem Def3 defines TwoValued GRAPH_2:def 3 :

for f being FinSequence holds

( f is TwoValued iff card (rng f) = 2 );

for f being FinSequence holds

( f is TwoValued iff card (rng f) = 2 );

Lm3: now :: thesis: ( len <*1,2*> > 1 & 1 <> 2 & rng <*1,2*> = {1,2} )

set p = <*1,2*>;

2 > 1 ;

hence len <*1,2*> > 1 by FINSEQ_1:44; :: thesis: ( 1 <> 2 & rng <*1,2*> = {1,2} )

thus 1 <> 2 ; :: thesis: rng <*1,2*> = {1,2}

thus rng <*1,2*> = (rng <*1*>) \/ (rng <*2*>) by FINSEQ_1:31

.= {1} \/ (rng <*2*>) by FINSEQ_1:38

.= {1} \/ {2} by FINSEQ_1:38

.= {1,2} by ENUMSET1:1 ; :: thesis: verum

end;
2 > 1 ;

hence len <*1,2*> > 1 by FINSEQ_1:44; :: thesis: ( 1 <> 2 & rng <*1,2*> = {1,2} )

thus 1 <> 2 ; :: thesis: rng <*1,2*> = {1,2}

thus rng <*1,2*> = (rng <*1*>) \/ (rng <*2*>) by FINSEQ_1:31

.= {1} \/ (rng <*2*>) by FINSEQ_1:38

.= {1} \/ {2} by FINSEQ_1:38

.= {1,2} by ENUMSET1:1 ; :: thesis: verum

theorem Th19: :: GRAPH_2:19

for p being FinSequence holds

( p is TwoValued iff ( len p > 1 & ex x, y being object st

( x <> y & rng p = {x,y} ) ) )

( p is TwoValued iff ( len p > 1 & ex x, y being object st

( x <> y & rng p = {x,y} ) ) )

proof end;

then Lm4: <*1,2*> is TwoValued

by Lm3;

Lm5: now :: thesis: for i being Nat st 1 <= i & i + 1 <= len <*1,2*> holds

<*1,2*> . i <> <*1,2*> . (i + 1)

<*1,2*> . i <> <*1,2*> . (i + 1)

let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len <*1,2*> implies <*1,2*> . i <> <*1,2*> . (i + 1) )

set p = <*1,2*>;

assume that

A1: 1 <= i and

A2: i + 1 <= len <*1,2*> ; :: thesis: <*1,2*> . i <> <*1,2*> . (i + 1)

i + 1 <= 1 + 1 by A2, FINSEQ_1:44;

then i <= 1 by XREAL_1:6;

then A3: i = 1 by A1, XXREAL_0:1;

then <*1,2*> . i = 1 by FINSEQ_1:44;

hence <*1,2*> . i <> <*1,2*> . (i + 1) by A3, FINSEQ_1:44; :: thesis: verum

end;
set p = <*1,2*>;

assume that

A1: 1 <= i and

A2: i + 1 <= len <*1,2*> ; :: thesis: <*1,2*> . i <> <*1,2*> . (i + 1)

i + 1 <= 1 + 1 by A2, FINSEQ_1:44;

then i <= 1 by XREAL_1:6;

then A3: i = 1 by A1, XXREAL_0:1;

then <*1,2*> . i = 1 by FINSEQ_1:44;

hence <*1,2*> . i <> <*1,2*> . (i + 1) by A3, FINSEQ_1:44; :: thesis: verum

:: deftheorem Def4 defines Alternating GRAPH_2:def 4 :

for f being FinSequence holds

( f is Alternating iff for i being Nat st 1 <= i & i + 1 <= len f holds

f . i <> f . (i + 1) );

for f being FinSequence holds

( f is Alternating iff for i being Nat st 1 <= i & i + 1 <= len f holds

f . i <> f . (i + 1) );

Lm6: <*1,2*> is Alternating

by Lm5;

registration

ex b_{1} being FinSequence st

( b_{1} is TwoValued & b_{1} is Alternating )
by Lm4, Lm6;

end;

cluster Relation-like omega -defined Function-like finite FinSequence-like FinSubsequence-like TwoValued Alternating for set ;

existence ex b

( b

theorem Th20: :: GRAPH_2:20

for a1, a2 being TwoValued Alternating FinSequence st len a1 = len a2 & rng a1 = rng a2 & a1 . 1 = a2 . 1 holds

a1 = a2

a1 = a2

proof end;

theorem Th21: :: GRAPH_2:21

for a1, a2 being TwoValued Alternating FinSequence st a1 <> a2 & len a1 = len a2 & rng a1 = rng a2 holds

for i being Nat st 1 <= i & i <= len a1 holds

a1 . i <> a2 . i

for i being Nat st 1 <= i & i <= len a1 holds

a1 . i <> a2 . i

proof end;

theorem Th22: :: GRAPH_2:22

for a1, a2 being TwoValued Alternating FinSequence st a1 <> a2 & len a1 = len a2 & rng a1 = rng a2 holds

for a being TwoValued Alternating FinSequence st len a = len a1 & rng a = rng a1 & not a = a1 holds

a = a2

for a being TwoValued Alternating FinSequence st len a = len a1 & rng a = rng a1 & not a = a1 holds

a = a2

proof end;

theorem Th23: :: GRAPH_2:23

for X, Y being set

for n being Nat st X <> Y & n > 1 holds

ex a1 being TwoValued Alternating FinSequence st

( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X )

for n being Nat st X <> Y & n > 1 holds

ex a1 being TwoValued Alternating FinSequence st

( rng a1 = {X,Y} & len a1 = n & a1 . 1 = X )

proof end;

registration

let X be set ;

let fs be FinSequence of X;

coherence

for b_{1} being Subset of fs holds b_{1} is FinSubsequence-like

end;
let fs be FinSequence of X;

coherence

for b

proof end;

theorem Th24: :: GRAPH_2:24

for f being FinSubsequence

for g, h, fg, fh, fgh being FinSequence st rng g c= dom f & rng h c= dom f & fg = f * g & fh = f * h & fgh = f * (g ^ h) holds

fgh = fg ^ fh

for g, h, fg, fh, fgh being FinSequence st rng g c= dom f & rng h c= dom f & fg = f * g & fh = f * h & fgh = f * (g ^ h) holds

fgh = fg ^ fh

proof end;

theorem :: GRAPH_2:25

for X being set

for fs being FinSequence of X

for fss being Subset of fs holds

( dom fss c= dom fs & rng fss c= rng fs ) by RELAT_1:11;

for fs being FinSequence of X

for fss being Subset of fs holds

( dom fss c= dom fs & rng fss c= rng fs ) by RELAT_1:11;

theorem Th27: :: GRAPH_2:27

for X, Y being set

for fs being FinSequence of X

for fss being Subset of fs holds fss | Y is Subset of fs

for fs being FinSequence of X

for fss being Subset of fs holds fss | Y is Subset of fs

proof end;

theorem Th28: :: GRAPH_2:28

for X being set

for fs, fs1, fs2 being FinSequence of X

for fss, fss2 being Subset of fs

for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) holds

Seq fss2 = fs2

for fs, fs1, fs2 being FinSequence of X

for fss, fss2 being Subset of fs

for fss1 being Subset of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) holds

Seq fss2 = fs2

proof end;

theorem :: GRAPH_2:29

theorem :: GRAPH_2:30

definition

let G be Graph;

let X be set ;

coherence

{ v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & ( v = the Source of G . e or v = the Target of G . e ) ) } is set ;

;

end;
let X be set ;

func G -VSet X -> set equals :: GRAPH_2:def 5

{ v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & ( v = the Source of G . e or v = the Target of G . e ) ) } ;

correctness { v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & ( v = the Source of G . e or v = the Target of G . e ) ) } ;

coherence

{ v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & ( v = the Source of G . e or v = the Target of G . e ) ) } is set ;

;

:: deftheorem defines -VSet GRAPH_2:def 5 :

for G being Graph

for X being set holds G -VSet X = { v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & ( v = the Source of G . e or v = the Target of G . e ) ) } ;

for G being Graph

for X being set holds G -VSet X = { v where v is Element of G : ex e being Element of the carrier' of G st

( e in X & ( v = the Source of G . e or v = the Target of G . e ) ) } ;

:: deftheorem defines is_vertex_seq_of GRAPH_2:def 6 :

for G being Graph

for vs being FinSequence of the carrier of G

for c being FinSequence holds

( vs is_vertex_seq_of c iff ( len vs = (len c) + 1 & ( for n being Nat st 1 <= n & n <= len c holds

c . n joins vs /. n,vs /. (n + 1) ) ) );

for G being Graph

for vs being FinSequence of the carrier of G

for c being FinSequence holds

( vs is_vertex_seq_of c iff ( len vs = (len c) + 1 & ( for n being Nat st 1 <= n & n <= len c holds

c . n joins vs /. n,vs /. (n + 1) ) ) );

theorem Th31: :: GRAPH_2:31

for G being Graph

for vs being FinSequence of the carrier of G

for c being Chain of G st c <> {} & vs is_vertex_seq_of c holds

G -VSet (rng c) = rng vs

for vs being FinSequence of the carrier of G

for c being Chain of G st c <> {} & vs is_vertex_seq_of c holds

G -VSet (rng c) = rng vs

proof end;

theorem Th33: :: GRAPH_2:33

for G being Graph

for c being Chain of G ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c

for c being Chain of G ex vs being FinSequence of the carrier of G st vs is_vertex_seq_of c

proof end;

theorem Th34: :: GRAPH_2:34

for G being Graph

for vs1, vs2 being FinSequence of the carrier of G

for c being Chain of G st c <> {} & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & vs1 <> vs2 holds

( vs1 . 1 <> vs2 . 1 & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )

for vs1, vs2 being FinSequence of the carrier of G

for c being Chain of G st c <> {} & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & vs1 <> vs2 holds

( vs1 . 1 <> vs2 . 1 & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )

proof end;

:: deftheorem defines alternates_vertices_in GRAPH_2:def 7 :

for G being Graph

for c being FinSequence holds

( c alternates_vertices_in G iff ( len c >= 1 & card (G -VSet (rng c)) = 2 & ( for n being Nat st n in dom c holds

the Source of G . (c . n) <> the Target of G . (c . n) ) ) );

for G being Graph

for c being FinSequence holds

( c alternates_vertices_in G iff ( len c >= 1 & card (G -VSet (rng c)) = 2 & ( for n being Nat st n in dom c holds

the Source of G . (c . n) <> the Target of G . (c . n) ) ) );

theorem Th35: :: GRAPH_2:35

for G being Graph

for vs being FinSequence of the carrier of G

for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds

for k being Nat st k in dom c holds

vs . k <> vs . (k + 1)

for vs being FinSequence of the carrier of G

for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds

for k being Nat st k in dom c holds

vs . k <> vs . (k + 1)

proof end;

theorem Th36: :: GRAPH_2:36

for G being Graph

for vs being FinSequence of the carrier of G

for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds

rng vs = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}

for vs being FinSequence of the carrier of G

for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds

rng vs = {( the Source of G . (c . 1)),( the Target of G . (c . 1))}

proof end;

theorem Th37: :: GRAPH_2:37

for G being Graph

for vs being FinSequence of the carrier of G

for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds

vs is TwoValued Alternating FinSequence

for vs being FinSequence of the carrier of G

for c being Chain of G st c alternates_vertices_in G & vs is_vertex_seq_of c holds

vs is TwoValued Alternating FinSequence

proof end;

theorem Th38: :: GRAPH_2:38

for G being Graph

for c being Chain of G st c alternates_vertices_in G holds

ex vs1, vs2 being FinSequence of the carrier of G st

( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )

for c being Chain of G st c alternates_vertices_in G holds

ex vs1, vs2 being FinSequence of the carrier of G st

( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the carrier of G holds

( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )

proof end;

Lm7: for D being non empty set st ( for x, y being set st x in D & y in D holds

x = y ) holds

card D = 1

proof end;

theorem Th39: :: GRAPH_2:39

for G being Graph

for vs being FinSequence of the carrier of G

for c being Chain of G st vs is_vertex_seq_of c holds

( ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) iff for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds

vs1 = vs )

for vs being FinSequence of the carrier of G

for c being Chain of G st vs is_vertex_seq_of c holds

( ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) iff for vs1 being FinSequence of the carrier of G st vs1 is_vertex_seq_of c holds

vs1 = vs )

proof end;

definition

let G be Graph;

let c be Chain of G;

assume A1: ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) ;

existence

ex b_{1} being FinSequence of the carrier of G st b_{1} is_vertex_seq_of c
by Th33;

uniqueness

for b_{1}, b_{2} being FinSequence of the carrier of G st b_{1} is_vertex_seq_of c & b_{2} is_vertex_seq_of c holds

b_{1} = b_{2}
by A1, Th39;

end;
let c be Chain of G;

assume A1: ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) ;

existence

ex b

uniqueness

for b

b

:: deftheorem defines vertex-seq GRAPH_2:def 8 :

for G being Graph

for c being Chain of G st ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) holds

for b_{3} being FinSequence of the carrier of G holds

( b_{3} = vertex-seq c iff b_{3} is_vertex_seq_of c );

for G being Graph

for c being Chain of G st ( card the carrier of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) holds

for b

( b

theorem Th40: :: GRAPH_2:40

for n being Nat

for G being Graph

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being Chain of G st vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds

vs1 is_vertex_seq_of c1

for G being Graph

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being Chain of G st vs is_vertex_seq_of c & c1 = c | (Seg n) & vs1 = vs | (Seg (n + 1)) holds

vs1 is_vertex_seq_of c1

proof end;

theorem Th41: :: GRAPH_2:41

for q being FinSequence

for m, n being Nat

for G being Graph

for c being Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds

q is Chain of G

for m, n being Nat

for G being Graph

for c being Chain of G st 1 <= m & m <= n & n <= len c & q = (m,n) -cut c holds

q is Chain of G

proof end;

theorem Th42: :: GRAPH_2:42

for m, n being Nat

for G being Graph

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds

vs1 is_vertex_seq_of c1

for G being Graph

for vs, vs1 being FinSequence of the carrier of G

for c, c1 being Chain of G st 1 <= m & m <= n & n <= len c & c1 = (m,n) -cut c & vs is_vertex_seq_of c & vs1 = (m,(n + 1)) -cut vs holds

vs1 is_vertex_seq_of c1

proof end;

theorem Th43: :: GRAPH_2:43

for G being Graph

for vs1, vs2 being FinSequence of the carrier of G

for c1, c2 being Chain of G st vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds

c1 ^ c2 is Chain of G

for vs1, vs2 being FinSequence of the carrier of G

for c1, c2 being Chain of G st vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 holds

c1 ^ c2 is Chain of G

proof end;

theorem Th44: :: GRAPH_2:44

for G being Graph

for vs, vs1, vs2 being FinSequence of the carrier of G

for c, c1, c2 being Chain of G st vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds

vs is_vertex_seq_of c

for vs, vs1, vs2 being FinSequence of the carrier of G

for c, c1, c2 being Chain of G st vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds

vs is_vertex_seq_of c

proof end;

Lm8: for G being Graph

for v being Element of G holds <*v*> is_vertex_seq_of {}

by FINSEQ_1:39;

:: deftheorem Def9 defines simple GRAPH_2:def 9 :

for G being Graph

for IT being Chain of G holds

( IT is simple iff ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of IT & ( for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs ) ) ) );

for G being Graph

for IT being Chain of G holds

( IT is simple iff ex vs being FinSequence of the carrier of G st

( vs is_vertex_seq_of IT & ( for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs ) ) ) );

registration

let G be Graph;

ex b_{1} being Chain of G st b_{1} is simple

end;
cluster Relation-like omega -defined the carrier' of G -valued Function-like finite FinSequence-like FinSubsequence-like simple for Chain of G;

existence ex b

proof end;

theorem :: GRAPH_2:45

for n being Nat

for G being Graph

for sc being simple Chain of G holds sc | (Seg n) is simple Chain of G

for G being Graph

for sc being simple Chain of G holds sc | (Seg n) is simple Chain of G

proof end;

theorem Th46: :: GRAPH_2:46

for G being Graph

for vs1, vs2 being FinSequence of the carrier of G

for sc being simple Chain of G st 2 < len sc & vs1 is_vertex_seq_of sc & vs2 is_vertex_seq_of sc holds

vs1 = vs2

for vs1, vs2 being FinSequence of the carrier of G

for sc being simple Chain of G st 2 < len sc & vs1 is_vertex_seq_of sc & vs2 is_vertex_seq_of sc holds

vs1 = vs2

proof end;

theorem :: GRAPH_2:47

for G being Graph

for vs being FinSequence of the carrier of G

for sc being simple Chain of G st vs is_vertex_seq_of sc holds

for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

for vs being FinSequence of the carrier of G

for sc being simple Chain of G st vs is_vertex_seq_of sc holds

for n, m being Nat st 1 <= n & n < m & m <= len vs & vs . n = vs . m holds

( n = 1 & m = len vs )

proof end;

theorem Th48: :: GRAPH_2:48

for G being Graph

for vs being FinSequence of the carrier of G

for c being Chain of G st c is not simple Chain of G & vs is_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

for vs being FinSequence of the carrier of G

for c being Chain of G st c is not simple Chain of G & vs is_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex c1 being Chain of G ex vs1 being FinSequence of the carrier of G st

( len c1 < len c & vs1 is_vertex_seq_of c1 & len vs1 < len vs & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) & Seq fc = c1 & Seq fvs = vs1 )

proof end;

theorem :: GRAPH_2:49

for G being Graph

for vs being FinSequence of the carrier of G

for c being Chain of G st vs is_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex sc being simple Chain of G ex vs1 being FinSequence of the carrier of G st

( Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )

for vs being FinSequence of the carrier of G

for c being Chain of G st vs is_vertex_seq_of c holds

ex fc being Subset of c ex fvs being Subset of vs ex sc being simple Chain of G ex vs1 being FinSequence of the carrier of G st

( Seq fc = sc & Seq fvs = vs1 & vs1 is_vertex_seq_of sc & vs . 1 = vs1 . 1 & vs . (len vs) = vs1 . (len vs1) )

proof end;

registration

let G be Graph;

correctness

coherence

for b_{1} being Chain of G st b_{1} is empty holds

b_{1} is V17();

;

end;
correctness

coherence

for b

b

;

theorem :: GRAPH_2:50

for p being FinSequence

for n being Nat

for G being Graph st p is Path of G holds

p | (Seg n) is Path of G

for n being Nat

for G being Graph st p is Path of G holds

p | (Seg n) is Path of G

proof end;

registration

let G be Graph;

ex b_{1} being Path of G st b_{1} is simple

end;
cluster Relation-like omega -defined the carrier' of G -valued Function-like one-to-one finite FinSequence-like FinSubsequence-like simple for Chain of G;

existence ex b

proof end;

theorem :: GRAPH_2:52

for G being Graph

for sc being simple Chain of G holds

( sc is Path of G iff ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) )

for sc being simple Chain of G holds

( sc is Path of G iff ( len sc = 0 or len sc = 1 or sc . 1 <> sc . 2 ) )

proof end;

registration

let G be Graph;

correctness

coherence

for b_{1} being Chain of G st b_{1} is empty holds

b_{1} is oriented ;

;

end;
correctness

coherence

for b

b

;

definition

let G be Graph;

let oc be oriented Chain of G;

assume A1: oc <> {} ;

ex b_{1} being FinSequence of the carrier of G st

( b_{1} is_vertex_seq_of oc & b_{1} . 1 = the Source of G . (oc . 1) )

for b_{1}, b_{2} being FinSequence of the carrier of G st b_{1} is_vertex_seq_of oc & b_{1} . 1 = the Source of G . (oc . 1) & b_{2} is_vertex_seq_of oc & b_{2} . 1 = the Source of G . (oc . 1) holds

b_{1} = b_{2}
by A1, Th34;

end;
let oc be oriented Chain of G;

assume A1: oc <> {} ;

func vertex-seq oc -> FinSequence of the carrier of G means :: GRAPH_2:def 10

( it is_vertex_seq_of oc & it . 1 = the Source of G . (oc . 1) );

existence ( it is_vertex_seq_of oc & it . 1 = the Source of G . (oc . 1) );

ex b

( b

proof end;

uniqueness for b

b

:: deftheorem defines vertex-seq GRAPH_2:def 10 :

for G being Graph

for oc being oriented Chain of G st oc <> {} holds

for b_{3} being FinSequence of the carrier of G holds

( b_{3} = vertex-seq oc iff ( b_{3} is_vertex_seq_of oc & b_{3} . 1 = the Source of G . (oc . 1) ) );

for G being Graph

for oc being oriented Chain of G st oc <> {} holds

for b

( b

:: from AMISTD_1, 2006.01.12, A.T.

theorem :: GRAPH_2:53

for D being non empty set

for f1 being non empty FinSequence of D

for f2 being FinSequence of D holds (f1 ^' f2) /. 1 = f1 /. 1

for f1 being non empty FinSequence of D

for f2 being FinSequence of D holds (f1 ^' f2) /. 1 = f1 /. 1

proof end;

theorem :: GRAPH_2:54

for D being non empty set

for f1 being FinSequence of D

for f2 being non trivial FinSequence of D holds (f1 ^' f2) /. (len (f1 ^' f2)) = f2 /. (len f2)

for f1 being FinSequence of D

for f2 being non trivial FinSequence of D holds (f1 ^' f2) /. (len (f1 ^' f2)) = f2 /. (len f2)

proof end;

theorem :: GRAPH_2:57

for D being non empty set

for n being Nat

for f1, f2 being FinSequence of D st 1 <= n & n <= len f1 holds

(f1 ^' f2) /. n = f1 /. n

for n being Nat

for f1, f2 being FinSequence of D st 1 <= n & n <= len f1 holds

(f1 ^' f2) /. n = f1 /. n

proof end;

theorem :: GRAPH_2:58

for D being non empty set

for n being Nat

for f1, f2 being FinSequence of D st 1 <= n & n < len f2 holds

(f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1)

for n being Nat

for f1, f2 being FinSequence of D st 1 <= n & n < len f2 holds

(f1 ^' f2) /. ((len f1) + n) = f2 /. (n + 1)

proof end;

:: from SFMATR3, 2007.07.26, A.T.

definition

let F be FinSequence of INT ;

let m, n be Nat;

assume that

A1: 1 <= m and

A2: m <= n and

A3: n <= len F ;

ex b_{1} being Nat ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & b_{1} + 1 = ((min X) .. ((m,n) -cut F)) + m )

for b_{1}, b_{2} being Nat st ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & b_{1} + 1 = ((min X) .. ((m,n) -cut F)) + m ) & ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & b_{2} + 1 = ((min X) .. ((m,n) -cut F)) + m ) holds

b_{1} = b_{2}
;

end;
let m, n be Nat;

assume that

A1: 1 <= m and

A2: m <= n and

A3: n <= len F ;

func min_at (F,m,n) -> Nat means :Def11: :: GRAPH_2:def 11

ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & it + 1 = ((min X) .. ((m,n) -cut F)) + m );

existence ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & it + 1 = ((min X) .. ((m,n) -cut F)) + m );

ex b

( X = rng ((m,n) -cut F) & b

proof end;

uniqueness for b

( X = rng ((m,n) -cut F) & b

( X = rng ((m,n) -cut F) & b

b

:: deftheorem Def11 defines min_at GRAPH_2:def 11 :

for F being FinSequence of INT

for m, n being Nat st 1 <= m & m <= n & n <= len F holds

for b_{4} being Nat holds

( b_{4} = min_at (F,m,n) iff ex X being non empty finite Subset of INT st

( X = rng ((m,n) -cut F) & b_{4} + 1 = ((min X) .. ((m,n) -cut F)) + m ) );

for F being FinSequence of INT

for m, n being Nat st 1 <= m & m <= n & n <= len F holds

for b

( b

( X = rng ((m,n) -cut F) & b

theorem Th59: :: GRAPH_2:59

for F being FinSequence of INT

for m, n, ma being Nat st 1 <= m & m <= n & n <= len F holds

( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) ) )

for m, n, ma being Nat st 1 <= m & m <= n & n <= len F holds

( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds

F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds

F . ma < F . i ) ) )

proof end;

definition

let F be FinSequence of INT ;

let m, n be Nat;

end;
let m, n be Nat;

pred F is_non_decreasing_on m,n means :: GRAPH_2:def 12

for i, j being Nat st m <= i & i <= j & j <= n holds

F . i <= F . j;

for i, j being Nat st m <= i & i <= j & j <= n holds

F . i <= F . j;

:: deftheorem defines is_non_decreasing_on GRAPH_2:def 12 :

for F being FinSequence of INT

for m, n being Nat holds

( F is_non_decreasing_on m,n iff for i, j being Nat st m <= i & i <= j & j <= n holds

F . i <= F . j );

for F being FinSequence of INT

for m, n being Nat holds

( F is_non_decreasing_on m,n iff for i, j being Nat st m <= i & i <= j & j <= n holds

F . i <= F . j );

:: deftheorem defines is_split_at GRAPH_2:def 13 :

for F being FinSequence of INT

for n being Nat holds

( F is_split_at n iff for i, j being Nat st 1 <= i & i <= n & n < j & j <= len F holds

F . i <= F . j );

for F being FinSequence of INT

for n being Nat holds

( F is_split_at n iff for i, j being Nat st 1 <= i & i <= n & n < j & j <= len F holds

F . i <= F . j );

theorem :: GRAPH_2:61

for F, F1 being FinSequence of INT

for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F is_non_decreasing_on 1,k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds

F1 is_non_decreasing_on 1,k + 1

for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F is_non_decreasing_on 1,k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds

F1 is_non_decreasing_on 1,k + 1

proof end;

theorem :: GRAPH_2:62

for F, F1 being FinSequence of INT

for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds

F1 is_split_at k + 1

for k, ma being Nat st k + 1 <= len F & ma = min_at (F,(k + 1),(len F)) & F is_split_at k & F1 = (F +* ((k + 1),(F . ma))) +* (ma,(F . (k + 1))) holds

F1 is_split_at k + 1

proof end;

:: from SCPISORT, 2011.02.13

:: The following chain:

:: .--->.

:: ^ |

:: | v

:: .--->.<---.--->.

:: | ^

:: v |

:: .--->.

:: is a case in point: