:: GRAPH_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

scheme :: GRAPH_2:sch 1
FinSegRng{ F1() -> Nat, F2() -> Nat, F3( set ) -> set , P1[ Nat] } :
{ F3(i) where i is Nat : ( F1() <= i & i <= F2() & P1[i] ) } is finite
proof end;

theorem Th1: :: GRAPH_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th2: :: GRAPH_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p 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 ) )
proof end;

theorem Th3: :: GRAPH_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))
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 Th4: :: GRAPH_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat holds Card { k where k is Nat : ( m <= k & k <= m + n ) } = n + 1
proof end;

theorem Th5: :: GRAPH_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n, m, l being Nat st 1 <= l & l <= n holds
(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;
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 + 1 & n <= len p )
otherwise it = {} ;
consistency
for b1 being FinSequence holds verum
;
existence
( ( 1 <= m & m <= n + 1 & n <= len p implies ex b1 being FinSequence st
( (len b1) + m = n + 1 & ( for i being Nat st i < len b1 holds
b1 . (i + 1) = p . (m + i) ) ) ) & ( ( not 1 <= m or not m <= n + 1 or not n <= len p ) implies ex b1 being FinSequence st b1 = {} ) )
proof end;
uniqueness
for b1, b2 being FinSequence holds
( ( 1 <= m & m <= n + 1 & n <= len p & (len b1) + m = n + 1 & ( for i being Nat st i < len b1 holds
b1 . (i + 1) = p . (m + i) ) & (len b2) + m = n + 1 & ( for i being Nat st i < len b2 holds
b2 . (i + 1) = p . (m + i) ) implies b1 = b2 ) & ( ( not 1 <= m or not m <= n + 1 or not n <= len p ) & b1 = {} & b2 = {} implies b1 = b2 ) )
proof end;
end;

:: deftheorem Def1 defines -cut GRAPH_2:def 1 :
for p being FinSequence
for m, n being Nat
for b4 being FinSequence holds
( ( 1 <= m & m <= n + 1 & n <= len p implies ( b4 = m,n -cut p iff ( (len b4) + m = n + 1 & ( for i being Nat st i < len b4 holds
b4 . (i + 1) = p . (m + i) ) ) ) ) & ( ( not 1 <= m or not m <= n + 1 or not n <= len p ) implies ( b4 = m,n -cut p iff b4 = {} ) ) );

theorem Th6: :: GRAPH_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for m being Nat st 1 <= m & m <= len p holds
m,m -cut p = <*(p . m)*>
proof end;

theorem Th7: :: GRAPH_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence holds 1,(len p) -cut p = p
proof end;

theorem Th8: :: GRAPH_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: GRAPH_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th11: :: GRAPH_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence
for m, n being Nat holds rng (m,n -cut p) c= rng 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
proof end;
end;

theorem Th12: :: GRAPH_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let p, q be FinSequence;
func p ^' q -> FinSequence equals :: GRAPH_2:def 2
p ^ (2,(len q) -cut q);
correctness
coherence
p ^ (2,(len q) -cut q) is FinSequence
;
;
end;

:: deftheorem defines ^' GRAPH_2:def 2 :
for p, q being FinSequence holds p ^' q = p ^ (2,(len q) -cut q);

theorem Th13: :: GRAPH_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being FinSequence st q <> {} holds
(len (p ^' q)) + 1 = (len p) + (len q)
proof end;

theorem Th14: :: GRAPH_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence
for k being Nat st 1 <= k & k <= len p holds
(p ^' q) . k = p . k
proof end;

theorem Th15: :: GRAPH_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being FinSequence
for k being Nat st 1 <= k & k < len q holds
(p ^' q) . ((len p) + k) = q . (k + 1)
proof end;

theorem Th16: :: GRAPH_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q, p being FinSequence st 1 < len q holds
(p ^' q) . (len (p ^' q)) = q . (len q)
proof end;

theorem Th17: :: GRAPH_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence holds rng (p ^' q) c= (rng p) \/ (rng q)
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
proof end;
end;

theorem :: GRAPH_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p, q being FinSequence st p <> {} & q <> {} & p . (len p) = q . 1 holds
rng (p ^' q) = (rng p) \/ (rng q)
proof end;

definition
let f be FinSequence;
attr f is TwoValued means :Def3: :: GRAPH_2:def 3
card (rng f) = 2;
end;

:: deftheorem Def3 defines TwoValued GRAPH_2:def 3 :
for f being FinSequence holds
( f is TwoValued iff card (rng f) = 2 );

Lm2: now
set p = <*1,2*>;
2 > 1 ;
hence len <*1,2*> > 1 by FINSEQ_1:61; :: thesis: ( 1 <> 2 & rng <*1,2*> = {1,2} )
thus 1 <> 2 ; :: thesis: rng <*1,2*> = {1,2}
thus rng <*1,2*> = rng (<*1*> ^ <*2*>) by FINSEQ_1:def 9
.= (rng <*1*>) \/ (rng <*2*>) by FINSEQ_1:44
.= {1} \/ (rng <*2*>) by FINSEQ_1:55
.= {1} \/ {2} by FINSEQ_1:55
.= {1,2} by ENUMSET1:41 ; :: thesis: verum
end;

theorem Th19: :: GRAPH_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSequence holds
( p is TwoValued iff ( len p > 1 & ex x, y being set st
( x <> y & rng p = {x,y} ) ) )
proof end;

then Lm3: <*1,2*> is TwoValued
by Lm2;

Lm4: now
set p = <*1,2*>;
let i be Nat; :: thesis: ( 1 <= i & i + 1 <= len <*1,2*> implies <*1,2*> . i <> <*1,2*> . (i + 1) )
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:61;
then i <= 1 by XREAL_1:8;
then i = 1 by A1, XREAL_1:1;
then ( <*1,2*> . i = 1 & <*1,2*> . (i + 1) = 2 ) by FINSEQ_1:61;
hence <*1,2*> . i <> <*1,2*> . (i + 1) ; :: thesis: verum
end;

definition
let f be FinSequence;
attr f is Alternating means :Def4: :: GRAPH_2:def 4
for i being Nat st 1 <= i & i + 1 <= len f holds
f . i <> f . (i + 1);
end;

:: deftheorem Def4 defines Alternating GRAPH_2:def 4 :
for f being FinSequence holds
( f is Alternating iff for i being Nat st 1 <= i & i + 1 <= len f holds
f . i <> f . (i + 1) );

Lm5: <*1,2*> is Alternating
by Def4, Lm4;

registration
cluster TwoValued Alternating set ;
existence
ex b1 being FinSequence st
( b1 is TwoValued & b1 is Alternating )
by Lm3, Lm5;
end;

theorem Th20: :: GRAPH_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a1, a2 being TwoValued Alternating FinSequence st len a1 = len a2 & rng a1 = rng a2 & a1 . 1 = a2 . 1 holds
a1 = a2
proof end;

theorem Th21: :: GRAPH_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th22: :: GRAPH_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th23: :: GRAPH_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

definition
let X be set ;
let fs be FinSequence of X;
mode FinSubsequence of fs -> FinSubsequence means :Def5: :: GRAPH_2:def 5
it c= fs;
existence
ex b1 being FinSubsequence st b1 c= fs
proof end;
end;

:: deftheorem Def5 defines FinSubsequence GRAPH_2:def 5 :
for X being set
for fs being FinSequence of X
for b3 being FinSubsequence holds
( b3 is FinSubsequence of fs iff b3 c= fs );

theorem Th24: :: GRAPH_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for ss being FinSubsequence st ss is FinSequence holds
Seq ss = ss
proof end;

theorem :: GRAPH_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th26: :: GRAPH_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th27: :: GRAPH_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for fs being FinSequence of X
for fss being FinSubsequence of fs holds
( dom fss c= dom fs & rng fss c= rng fs )
proof end;

theorem Th28: :: GRAPH_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for fs being FinSequence of X holds fs is FinSubsequence of fs
proof end;

theorem Th29: :: GRAPH_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for fs being FinSequence of X
for fss being FinSubsequence of fs holds fss | Y is FinSubsequence of fs
proof end;

theorem Th30: :: GRAPH_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being set
for fs, fs1, fs2 being FinSequence of X
for fss, fss2 being FinSubsequence of fs
for fss1 being FinSubsequence of fs1 st Seq fss = fs1 & Seq fss1 = fs2 & fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss1))) holds
Seq fss2 = fs2
proof end;

registration
let G be Graph;
cluster the Vertices of G -> non empty ;
coherence
not the Vertices of G is empty
by GRAPH_1:def 1;
end;

theorem Th31: :: GRAPH_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v1, v2 being Element of the Vertices of G
for e being set st e joins v1,v2 holds
e joins v2,v1
proof end;

theorem Th32: :: GRAPH_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v1, v2, v3, v4 being Element of the Vertices of G
for e being set st e joins v1,v2 & e joins v3,v4 & not ( v1 = v3 & v2 = v4 ) holds
( v1 = v4 & v2 = v3 )
proof end;

registration
let G be Graph;
cluster empty Chain of G;
existence
ex b1 being Chain of G st b1 is empty
proof end;
end;

definition
let G be Graph;
let X be set ;
func G -VSet X -> set equals :: GRAPH_2:def 6
{ v where v is Element of the Vertices of G : ex e being Element of the Edges of G st
( e in X & ( v = the Source of G . e or v = the Target of G . e ) )
}
;
correctness
coherence
{ v where v is Element of the Vertices of G : ex e being Element of the Edges of G st
( e in X & ( v = the Source of G . e or v = the Target of G . e ) )
}
is set
;
;
end;

:: deftheorem defines -VSet GRAPH_2:def 6 :
for G being Graph
for X being set holds G -VSet X = { v where v is Element of the Vertices of G : ex e being Element of the Edges of G st
( e in X & ( v = the Source of G . e or v = the Target of G . e ) )
}
;

definition
let G be Graph;
let vs be FinSequence of the Vertices of G;
let c be FinSequence;
pred vs is_vertex_seq_of c means :Def7: :: GRAPH_2:def 7
( len vs = (len c) + 1 & ( for n being Nat st 1 <= n & n <= len c holds
c . n joins vs /. n,vs /. (n + 1) ) );
end;

:: deftheorem Def7 defines is_vertex_seq_of GRAPH_2:def 7 :
for G being Graph
for vs being FinSequence of the Vertices 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 :: GRAPH_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th34: :: GRAPH_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs being FinSequence of the Vertices 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 Th35: :: GRAPH_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for v being Element of the Vertices of G holds <*v*> is_vertex_seq_of {}
proof end;

theorem Th36: :: GRAPH_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for c being Chain of G ex vs being FinSequence of the Vertices of G st vs is_vertex_seq_of c
proof end;

theorem Th37: :: GRAPH_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs1, vs2 being FinSequence of the Vertices 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 Vertices of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )
proof end;

definition
let G be Graph;
let c be FinSequence;
pred c alternates_vertices_in G means :Def8: :: GRAPH_2:def 8
( 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) ) );
end;

:: deftheorem Def8 defines alternates_vertices_in GRAPH_2:def 8 :
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 Th38: :: GRAPH_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs being FinSequence of the Vertices 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 Th39: :: GRAPH_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs being FinSequence of the Vertices 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 Th40: :: GRAPH_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs being FinSequence of the Vertices 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 Th41: :: GRAPH_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for c being Chain of G st c alternates_vertices_in G holds
ex vs1, vs2 being FinSequence of the Vertices of G st
( vs1 <> vs2 & vs1 is_vertex_seq_of c & vs2 is_vertex_seq_of c & ( for vs being FinSequence of the Vertices of G holds
( not vs is_vertex_seq_of c or vs = vs1 or vs = vs2 ) ) )
proof end;

Lm6: 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 Th42: :: GRAPH_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs being FinSequence of the Vertices of G
for c being Chain of G st vs is_vertex_seq_of c holds
( ( Card the Vertices of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) iff for vs1 being FinSequence of the Vertices 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 Vertices of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) ;
func vertex-seq c -> FinSequence of the Vertices of G means :: GRAPH_2:def 9
it is_vertex_seq_of c;
existence
ex b1 being FinSequence of the Vertices of G st b1 is_vertex_seq_of c
by Th36;
uniqueness
for b1, b2 being FinSequence of the Vertices of G st b1 is_vertex_seq_of c & b2 is_vertex_seq_of c holds
b1 = b2
by A1, Th42;
end;

:: deftheorem defines vertex-seq GRAPH_2:def 9 :
for G being Graph
for c being Chain of G st ( Card the Vertices of G = 1 or ( c <> {} & not c alternates_vertices_in G ) ) holds
for b3 being FinSequence of the Vertices of G holds
( b3 = vertex-seq c iff b3 is_vertex_seq_of c );

theorem Th43: :: GRAPH_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for G being Graph
for vs, vs1 being FinSequence of the Vertices 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 Th44: :: GRAPH_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th45: :: GRAPH_2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for m, n being Nat
for G being Graph
for vs, vs1 being FinSequence of the Vertices 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 Th46: :: GRAPH_2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs1, vs2 being FinSequence of the Vertices 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 Th47: :: GRAPH_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs1, vs2, vs being FinSequence of the Vertices of G
for c1, c2, c being Chain of G st vs1 is_vertex_seq_of c1 & vs2 is_vertex_seq_of c2 & vs1 . (len vs1) = vs2 . 1 & c = c1 ^ c2 & vs = vs1 ^' vs2 holds
vs is_vertex_seq_of c
proof end;

Lm7: for G being Graph
for v being Element of the Vertices of G holds <*v*> is_vertex_seq_of {}
proof end;

definition
let G be Graph;
let IT be Chain of G;
attr IT is simple means :Def10: :: GRAPH_2:def 10
ex vs being FinSequence of the Vertices 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 ) ) );
end;

:: deftheorem Def10 defines simple GRAPH_2:def 10 :
for G being Graph
for IT being Chain of G holds
( IT is simple iff ex vs being FinSequence of the Vertices 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;
cluster simple Chain of G;
existence
ex b1 being Chain of G st b1 is simple
proof end;
end;

theorem :: GRAPH_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: GRAPH_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for n being Nat
for G being Graph
for sc being simple Chain of G holds sc | (Seg n) is simple Chain of G
proof end;

theorem Th50: :: GRAPH_2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs1, vs2 being FinSequence of the Vertices 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:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs being FinSequence of the Vertices 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 Th52: :: GRAPH_2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs being FinSequence of the Vertices 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 FinSubsequence of c ex fvs being FinSubsequence of vs ex c1 being Chain of G ex vs1 being FinSequence of the Vertices 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:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for vs being FinSequence of the Vertices of G
for c being Chain of G st vs is_vertex_seq_of c holds
ex fc being FinSubsequence of c ex fvs being FinSubsequence of vs ex sc being simple Chain of G ex vs1 being FinSequence of the Vertices 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;
cluster empty -> V5 Chain of G;
correctness
coherence
for b1 being Chain of G st b1 is empty holds
b1 is one-to-one
;
;
end;

theorem :: GRAPH_2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

registration
let G be Graph;
cluster simple Chain of G;
existence
ex b1 being Path of G st b1 is simple
proof end;
end;

theorem :: GRAPH_2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being Graph
for sc being simple Chain of G st 2 < len sc holds
sc is Path of G
proof end;

theorem :: GRAPH_2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

registration
let G be Graph;
cluster empty -> oriented Chain of G;
correctness
coherence
for b1 being Chain of G st b1 is empty holds
b1 is oriented
;
proof end;
end;

definition
let G be Graph;
let oc be oriented Chain of G;
assume A1: oc <> {} ;
func vertex-seq oc -> FinSequence of the Vertices of G means :: GRAPH_2:def 11
( it is_vertex_seq_of oc & it . 1 = the Source of G . (oc . 1) );
existence
ex b1 being FinSequence of the Vertices of G st
( b1 is_vertex_seq_of oc & b1 . 1 = the Source of G . (oc . 1) )
proof end;
uniqueness
for b1, b2 being FinSequence of the Vertices of G st b1 is_vertex_seq_of oc & b1 . 1 = the Source of G . (oc . 1) & b2 is_vertex_seq_of oc & b2 . 1 = the Source of G . (oc . 1) holds
b1 = b2
by A1, Th37;
end;

:: deftheorem defines vertex-seq GRAPH_2:def 11 :
for G being Graph
for oc being oriented Chain of G st oc <> {} holds
for b3 being FinSequence of the Vertices of G holds
( b3 = vertex-seq oc iff ( b3 is_vertex_seq_of oc & b3 . 1 = the Source of G . (oc . 1) ) );