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

theorem Th1: :: GLIB_001:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being odd Nat holds
( x < y iff x + 2 <= y )
proof end;

Lm1: for x, y, z being real number st 0 < z & x * z <= y * z holds
x <= y
by XREAL_1:70;

Lm2: for F being finite Function holds card (dom F) = card F
by PRE_CIRC:21;

theorem Th2: :: GLIB_001:2  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 k being Nat st X c= Seg k holds
for m, n being Nat st m in dom (Sgm X) & n = (Sgm X) . m holds
m <= n
proof end;

theorem Th3: :: GLIB_001:3  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 len (Seq fss) <= len fs
proof end;

theorem Th4: :: GLIB_001:4  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
for m being Nat st m in dom (Seq fss) holds
ex n being Nat st
( n in dom fs & m <= n & (Seq fss) . m = fs . n )
proof end;

theorem Th5: :: GLIB_001:5  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 len (Seq fss) = card fss
proof end;

theorem Th6: :: GLIB_001:6  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 (Seq fss) = dom (Sgm (dom fss))
proof end;

definition
let G be _Graph;
mode VertexSeq of G -> FinSequence of the_Vertices_of G means :Def1: :: GLIB_001:def 1
for n being Nat st 1 <= n & n < len it holds
ex e being set st e Joins it . n,it . (n + 1),G;
existence
ex b1 being FinSequence of the_Vertices_of G st
for n being Nat st 1 <= n & n < len b1 holds
ex e being set st e Joins b1 . n,b1 . (n + 1),G
proof end;
end;

:: deftheorem Def1 defines VertexSeq GLIB_001:def 1 :
for G being _Graph
for b2 being FinSequence of the_Vertices_of G holds
( b2 is VertexSeq of G iff for n being Nat st 1 <= n & n < len b2 holds
ex e being set st e Joins b2 . n,b2 . (n + 1),G );

definition
let G be _Graph;
mode EdgeSeq of G -> FinSequence of the_Edges_of G means :Def2: :: GLIB_001:def 2
ex vs being FinSequence of the_Vertices_of G st
( len vs = (len it) + 1 & ( for n being Nat st 1 <= n & n <= len it holds
it . n Joins vs . n,vs . (n + 1),G ) );
existence
ex b1 being FinSequence of the_Edges_of G ex vs being FinSequence of the_Vertices_of G st
( len vs = (len b1) + 1 & ( for n being Nat st 1 <= n & n <= len b1 holds
b1 . n Joins vs . n,vs . (n + 1),G ) )
proof end;
end;

:: deftheorem Def2 defines EdgeSeq GLIB_001:def 2 :
for G being _Graph
for b2 being FinSequence of the_Edges_of G holds
( b2 is EdgeSeq of G iff ex vs being FinSequence of the_Vertices_of G st
( len vs = (len b2) + 1 & ( for n being Nat st 1 <= n & n <= len b2 holds
b2 . n Joins vs . n,vs . (n + 1),G ) ) );

definition
let G be _Graph;
mode Walk of G -> FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) means :Def3: :: GLIB_001:def 3
( not len it is even & it . 1 in the_Vertices_of G & ( for n being odd Nat st n < len it holds
it . (n + 1) Joins it . n,it . (n + 2),G ) );
existence
ex b1 being FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) st
( not len b1 is even & b1 . 1 in the_Vertices_of G & ( for n being odd Nat st n < len b1 holds
b1 . (n + 1) Joins b1 . n,b1 . (n + 2),G ) )
proof end;
end;

:: deftheorem Def3 defines Walk GLIB_001:def 3 :
for G being _Graph
for b2 being FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) holds
( b2 is Walk of G iff ( not len b2 is even & b2 . 1 in the_Vertices_of G & ( for n being odd Nat st n < len b2 holds
b2 . (n + 1) Joins b2 . n,b2 . (n + 2),G ) ) );

registration
let G be _Graph;
let W be Walk of G;
cluster len W -> non empty odd ;
correctness
coherence
( not len W is even & not len W is empty )
;
proof end;
end;

definition
let G be _Graph;
let v be Vertex of G;
func G .walkOf v -> Walk of G equals :: GLIB_001:def 4
<*v*>;
coherence
<*v*> is Walk of G
proof end;
end;

:: deftheorem defines .walkOf GLIB_001:def 4 :
for G being _Graph
for v being Vertex of G holds G .walkOf v = <*v*>;

definition
let G be _Graph;
let x, y, e be set ;
func G .walkOf x,e,y -> Walk of G equals :Def5: :: GLIB_001:def 5
<*x,e,y*> if e Joins x,y,G
otherwise G .walkOf (choose (the_Vertices_of G));
coherence
( ( e Joins x,y,G implies <*x,e,y*> is Walk of G ) & ( not e Joins x,y,G implies G .walkOf (choose (the_Vertices_of G)) is Walk of G ) )
proof end;
consistency
for b1 being Walk of G holds verum
;
end;

:: deftheorem Def5 defines .walkOf GLIB_001:def 5 :
for G being _Graph
for x, y, e being set holds
( ( e Joins x,y,G implies G .walkOf x,e,y = <*x,e,y*> ) & ( not e Joins x,y,G implies G .walkOf x,e,y = G .walkOf (choose (the_Vertices_of G)) ) );

definition
let G be _Graph;
let W be Walk of G;
func W .first() -> Vertex of G equals :: GLIB_001:def 6
W . 1;
coherence
W . 1 is Vertex of G
by Def3;
func W .last() -> Vertex of G equals :: GLIB_001:def 7
W . (len W);
coherence
W . (len W) is Vertex of G
proof end;
end;

:: deftheorem defines .first() GLIB_001:def 6 :
for G being _Graph
for W being Walk of G holds W .first() = W . 1;

:: deftheorem defines .last() GLIB_001:def 7 :
for G being _Graph
for W being Walk of G holds W .last() = W . (len W);

definition
let G be _Graph;
let W be Walk of G;
let n be Nat;
func W .vertexAt n -> Vertex of G equals :Def8: :: GLIB_001:def 8
W . n if ( not n is even & n <= len W )
otherwise W .first() ;
correctness
coherence
( ( not n is even & n <= len W implies W . n is Vertex of G ) & ( ( n is even or not n <= len W ) implies W .first() is Vertex of G ) )
;
consistency
for b1 being Vertex of G holds verum
;
proof end;
end;

:: deftheorem Def8 defines .vertexAt GLIB_001:def 8 :
for G being _Graph
for W being Walk of G
for n being Nat holds
( ( not n is even & n <= len W implies W .vertexAt n = W . n ) & ( ( n is even or not n <= len W ) implies W .vertexAt n = W .first() ) );

definition
let G be _Graph;
let W be Walk of G;
func W .reverse() -> Walk of G equals :: GLIB_001:def 9
Rev W;
coherence
Rev W is Walk of G
proof end;
end;

:: deftheorem defines .reverse() GLIB_001:def 9 :
for G being _Graph
for W being Walk of G holds W .reverse() = Rev W;

definition
let G be _Graph;
let W1, W2 be Walk of G;
func W1 .append W2 -> Walk of G equals :Def10: :: GLIB_001:def 10
W1 ^' W2 if W1 .last() = W2 .first()
otherwise W1;
correctness
coherence
( ( W1 .last() = W2 .first() implies W1 ^' W2 is Walk of G ) & ( not W1 .last() = W2 .first() implies W1 is Walk of G ) )
;
consistency
for b1 being Walk of G holds verum
;
proof end;
end;

:: deftheorem Def10 defines .append GLIB_001:def 10 :
for G being _Graph
for W1, W2 being Walk of G holds
( ( W1 .last() = W2 .first() implies W1 .append W2 = W1 ^' W2 ) & ( not W1 .last() = W2 .first() implies W1 .append W2 = W1 ) );

definition
let G be _Graph;
let W be Walk of G;
let m, n be Nat;
func W .cut m,n -> Walk of G equals :Def11: :: GLIB_001:def 11
m,n -cut W if ( not m is even & not n is even & m <= n & n <= len W )
otherwise W;
correctness
coherence
( ( not m is even & not n is even & m <= n & n <= len W implies m,n -cut W is Walk of G ) & ( ( m is even or n is even or not m <= n or not n <= len W ) implies W is Walk of G ) )
;
consistency
for b1 being Walk of G holds verum
;
proof end;
end;

:: deftheorem Def11 defines .cut GLIB_001:def 11 :
for G being _Graph
for W being Walk of G
for m, n being Nat holds
( ( not m is even & not n is even & m <= n & n <= len W implies W .cut m,n = m,n -cut W ) & ( ( m is even or n is even or not m <= n or not n <= len W ) implies W .cut m,n = W ) );

definition
let G be _Graph;
let W be Walk of G;
let m, n be Nat;
func W .remove m,n -> Walk of G equals :Def12: :: GLIB_001:def 12
(W .cut 1,m) .append (W .cut n,(len W)) if ( not m is even & not n is even & m <= n & n <= len W & W . m = W . n )
otherwise W;
correctness
coherence
( ( not m is even & not n is even & m <= n & n <= len W & W . m = W . n implies (W .cut 1,m) .append (W .cut n,(len W)) is Walk of G ) & ( ( m is even or n is even or not m <= n or not n <= len W or not W . m = W . n ) implies W is Walk of G ) )
;
consistency
for b1 being Walk of G holds verum
;
;
end;

:: deftheorem Def12 defines .remove GLIB_001:def 12 :
for G being _Graph
for W being Walk of G
for m, n being Nat holds
( ( not m is even & not n is even & m <= n & n <= len W & W . m = W . n implies W .remove m,n = (W .cut 1,m) .append (W .cut n,(len W)) ) & ( ( m is even or n is even or not m <= n or not n <= len W or not W . m = W . n ) implies W .remove m,n = W ) );

definition
let G be _Graph;
let W be Walk of G;
let e be set ;
func W .addEdge e -> Walk of G equals :: GLIB_001:def 13
W .append (G .walkOf (W .last() ),e,((W .last() ) .adj e));
coherence
W .append (G .walkOf (W .last() ),e,((W .last() ) .adj e)) is Walk of G
;
end;

:: deftheorem defines .addEdge GLIB_001:def 13 :
for G being _Graph
for W being Walk of G
for e being set holds W .addEdge e = W .append (G .walkOf (W .last() ),e,((W .last() ) .adj e));

definition
let G be _Graph;
let W be Walk of G;
func W .vertexSeq() -> VertexSeq of G means :Def14: :: GLIB_001:def 14
( (len W) + 1 = 2 * (len it) & ( for n being Nat st 1 <= n & n <= len it holds
it . n = W . ((2 * n) - 1) ) );
existence
ex b1 being VertexSeq of G st
( (len W) + 1 = 2 * (len b1) & ( for n being Nat st 1 <= n & n <= len b1 holds
b1 . n = W . ((2 * n) - 1) ) )
proof end;
uniqueness
for b1, b2 being VertexSeq of G st (len W) + 1 = 2 * (len b1) & ( for n being Nat st 1 <= n & n <= len b1 holds
b1 . n = W . ((2 * n) - 1) ) & (len W) + 1 = 2 * (len b2) & ( for n being Nat st 1 <= n & n <= len b2 holds
b2 . n = W . ((2 * n) - 1) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def14 defines .vertexSeq() GLIB_001:def 14 :
for G being _Graph
for W being Walk of G
for b3 being VertexSeq of G holds
( b3 = W .vertexSeq() iff ( (len W) + 1 = 2 * (len b3) & ( for n being Nat st 1 <= n & n <= len b3 holds
b3 . n = W . ((2 * n) - 1) ) ) );

definition
let G be _Graph;
let W be Walk of G;
func W .edgeSeq() -> EdgeSeq of G means :Def15: :: GLIB_001:def 15
( len W = (2 * (len it)) + 1 & ( for n being Nat st 1 <= n & n <= len it holds
it . n = W . (2 * n) ) );
existence
ex b1 being EdgeSeq of G st
( len W = (2 * (len b1)) + 1 & ( for n being Nat st 1 <= n & n <= len b1 holds
b1 . n = W . (2 * n) ) )
proof end;
uniqueness
for b1, b2 being EdgeSeq of G st len W = (2 * (len b1)) + 1 & ( for n being Nat st 1 <= n & n <= len b1 holds
b1 . n = W . (2 * n) ) & len W = (2 * (len b2)) + 1 & ( for n being Nat st 1 <= n & n <= len b2 holds
b2 . n = W . (2 * n) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines .edgeSeq() GLIB_001:def 15 :
for G being _Graph
for W being Walk of G
for b3 being EdgeSeq of G holds
( b3 = W .edgeSeq() iff ( len W = (2 * (len b3)) + 1 & ( for n being Nat st 1 <= n & n <= len b3 holds
b3 . n = W . (2 * n) ) ) );

definition
let G be _Graph;
let W be Walk of G;
func W .vertices() -> finite Subset of (the_Vertices_of G) equals :: GLIB_001:def 16
rng (W .vertexSeq() );
coherence
rng (W .vertexSeq() ) is finite Subset of (the_Vertices_of G)
;
end;

:: deftheorem defines .vertices() GLIB_001:def 16 :
for G being _Graph
for W being Walk of G holds W .vertices() = rng (W .vertexSeq() );

definition
let G be _Graph;
let W be Walk of G;
func W .edges() -> finite Subset of (the_Edges_of G) equals :: GLIB_001:def 17
rng (W .edgeSeq() );
coherence
rng (W .edgeSeq() ) is finite Subset of (the_Edges_of G)
;
end;

:: deftheorem defines .edges() GLIB_001:def 17 :
for G being _Graph
for W being Walk of G holds W .edges() = rng (W .edgeSeq() );

definition
let G be _Graph;
let W be Walk of G;
func W .length() -> Nat equals :: GLIB_001:def 18
len (W .edgeSeq() );
coherence
len (W .edgeSeq() ) is Nat
;
end;

:: deftheorem defines .length() GLIB_001:def 18 :
for G being _Graph
for W being Walk of G holds W .length() = len (W .edgeSeq() );

definition
let G be _Graph;
let W be Walk of G;
let v be set ;
func W .find v -> odd Nat means :Def19: :: GLIB_001:def 19
( it <= len W & W . it = v & ( for n being odd Nat st n <= len W & W . n = v holds
it <= n ) ) if v in W .vertices()
otherwise it = len W;
existence
( ( v in W .vertices() implies ex b1 being odd Nat st
( b1 <= len W & W . b1 = v & ( for n being odd Nat st n <= len W & W . n = v holds
b1 <= n ) ) ) & ( not v in W .vertices() implies ex b1 being odd Nat st b1 = len W ) )
proof end;
uniqueness
for b1, b2 being odd Nat holds
( ( v in W .vertices() & b1 <= len W & W . b1 = v & ( for n being odd Nat st n <= len W & W . n = v holds
b1 <= n ) & b2 <= len W & W . b2 = v & ( for n being odd Nat st n <= len W & W . n = v holds
b2 <= n ) implies b1 = b2 ) & ( not v in W .vertices() & b1 = len W & b2 = len W implies b1 = b2 ) )
proof end;
consistency
for b1 being odd Nat holds verum
;
end;

:: deftheorem Def19 defines .find GLIB_001:def 19 :
for G being _Graph
for W being Walk of G
for v being set
for b4 being odd Nat holds
( ( v in W .vertices() implies ( b4 = W .find v iff ( b4 <= len W & W . b4 = v & ( for n being odd Nat st n <= len W & W . n = v holds
b4 <= n ) ) ) ) & ( not v in W .vertices() implies ( b4 = W .find v iff b4 = len W ) ) );

definition
let G be _Graph;
let W be Walk of G;
let n be Nat;
func W .find n -> odd Nat means :Def20: :: GLIB_001:def 20
( it <= len W & W . it = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
it <= k ) ) if ( not n is even & n <= len W )
otherwise it = len W;
existence
( ( not n is even & n <= len W implies ex b1 being odd Nat st
( b1 <= len W & W . b1 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
b1 <= k ) ) ) & ( ( n is even or not n <= len W ) implies ex b1 being odd Nat st b1 = len W ) )
proof end;
uniqueness
for b1, b2 being odd Nat holds
( ( not n is even & n <= len W & b1 <= len W & W . b1 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
b1 <= k ) & b2 <= len W & W . b2 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
b2 <= k ) implies b1 = b2 ) & ( ( n is even or not n <= len W ) & b1 = len W & b2 = len W implies b1 = b2 ) )
proof end;
consistency
for b1 being odd Nat holds verum
;
end;

:: deftheorem Def20 defines .find GLIB_001:def 20 :
for G being _Graph
for W being Walk of G
for n being Nat
for b4 being odd Nat holds
( ( not n is even & n <= len W implies ( b4 = W .find n iff ( b4 <= len W & W . b4 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
b4 <= k ) ) ) ) & ( ( n is even or not n <= len W ) implies ( b4 = W .find n iff b4 = len W ) ) );

definition
let G be _Graph;
let W be Walk of G;
let v be set ;
func W .rfind v -> odd Nat means :Def21: :: GLIB_001:def 21
( it <= len W & W . it = v & ( for n being odd Nat st n <= len W & W . n = v holds
n <= it ) ) if v in W .vertices()
otherwise it = len W;
existence
( ( v in W .vertices() implies ex b1 being odd Nat st
( b1 <= len W & W . b1 = v & ( for n being odd Nat st n <= len W & W . n = v holds
n <= b1 ) ) ) & ( not v in W .vertices() implies ex b1 being odd Nat st b1 = len W ) )
proof end;
uniqueness
for b1, b2 being odd Nat holds
( ( v in W .vertices() & b1 <= len W & W . b1 = v & ( for n being odd Nat st n <= len W & W . n = v holds
n <= b1 ) & b2 <= len W & W . b2 = v & ( for n being odd Nat st n <= len W & W . n = v holds
n <= b2 ) implies b1 = b2 ) & ( not v in W .vertices() & b1 = len W & b2 = len W implies b1 = b2 ) )
proof end;
consistency
for b1 being odd Nat holds verum
;
end;

:: deftheorem Def21 defines .rfind GLIB_001:def 21 :
for G being _Graph
for W being Walk of G
for v being set
for b4 being odd Nat holds
( ( v in W .vertices() implies ( b4 = W .rfind v iff ( b4 <= len W & W . b4 = v & ( for n being odd Nat st n <= len W & W . n = v holds
n <= b4 ) ) ) ) & ( not v in W .vertices() implies ( b4 = W .rfind v iff b4 = len W ) ) );

definition
let G be _Graph;
let W be Walk of G;
let n be Nat;
func W .rfind n -> odd Nat means :Def22: :: GLIB_001:def 22
( it <= len W & W . it = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
k <= it ) ) if ( not n is even & n <= len W )
otherwise it = len W;
existence
( ( not n is even & n <= len W implies ex b1 being odd Nat st
( b1 <= len W & W . b1 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
k <= b1 ) ) ) & ( ( n is even or not n <= len W ) implies ex b1 being odd Nat st b1 = len W ) )
proof end;
uniqueness
for b1, b2 being odd Nat holds
( ( not n is even & n <= len W & b1 <= len W & W . b1 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
k <= b1 ) & b2 <= len W & W . b2 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
k <= b2 ) implies b1 = b2 ) & ( ( n is even or not n <= len W ) & b1 = len W & b2 = len W implies b1 = b2 ) )
proof end;
consistency
for b1 being odd Nat holds verum
;
end;

:: deftheorem Def22 defines .rfind GLIB_001:def 22 :
for G being _Graph
for W being Walk of G
for n being Nat
for b4 being odd Nat holds
( ( not n is even & n <= len W implies ( b4 = W .rfind n iff ( b4 <= len W & W . b4 = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds
k <= b4 ) ) ) ) & ( ( n is even or not n <= len W ) implies ( b4 = W .rfind n iff b4 = len W ) ) );

definition
let G be _Graph;
let u, v be set ;
let W be Walk of G;
pred W is_Walk_from u,v means :Def23: :: GLIB_001:def 23
( W .first() = u & W .last() = v );
end;

:: deftheorem Def23 defines is_Walk_from GLIB_001:def 23 :
for G being _Graph
for u, v being set
for W being Walk of G holds
( W is_Walk_from u,v iff ( W .first() = u & W .last() = v ) );

definition
let G be _Graph;
let W be Walk of G;
attr W is closed means :Def24: :: GLIB_001:def 24
W .first() = W .last() ;
attr W is directed means :Def25: :: GLIB_001:def 25
for n being odd Nat st n < len W holds
(the_Source_of G) . (W . (n + 1)) = W . n;
attr W is trivial means :Def26: :: GLIB_001:def 26
W .length() = 0;
attr W is Trail-like means :Def27: :: GLIB_001:def 27
W .edgeSeq() is one-to-one;
end;

:: deftheorem Def24 defines closed GLIB_001:def 24 :
for G being _Graph
for W being Walk of G holds
( W is closed iff W .first() = W .last() );

:: deftheorem Def25 defines directed GLIB_001:def 25 :
for G being _Graph
for W being Walk of G holds
( W is directed iff for n being odd Nat st n < len W holds
(the_Source_of G) . (W . (n + 1)) = W . n );

:: deftheorem Def26 defines trivial GLIB_001:def 26 :
for G being _Graph
for W being Walk of G holds
( W is trivial iff W .length() = 0 );

:: deftheorem Def27 defines Trail-like GLIB_001:def 27 :
for G being _Graph
for W being Walk of G holds
( W is Trail-like iff W .edgeSeq() is one-to-one );

notation
let G be _Graph;
let W be Walk of G;
antonym open W for closed W;
end;

definition
let G be _Graph;
let W be Walk of G;
attr W is Path-like means :Def28: :: GLIB_001:def 28
( W is Trail-like & ( for m, n being odd Nat st m < n & n <= len W & W . m = W . n holds
( m = 1 & n = len W ) ) );
end;

:: deftheorem Def28 defines Path-like GLIB_001:def 28 :
for G being _Graph
for W being Walk of G holds
( W is Path-like iff ( W is Trail-like & ( for m, n being odd Nat st m < n & n <= len W & W . m = W . n holds
( m = 1 & n = len W ) ) ) );

definition
let G be _Graph;
let W be Walk of G;
attr W is vertex-distinct means :Def29: :: GLIB_001:def 29
for m, n being odd Nat st m <= len W & n <= len W & W . m = W . n holds
m = n;
end;

:: deftheorem Def29 defines vertex-distinct GLIB_001:def 29 :
for G being _Graph
for W being Walk of G holds
( W is vertex-distinct iff for m, n being odd Nat st m <= len W & n <= len W & W . m = W . n holds
m = n );

definition
let G be _Graph;
let W be Walk of G;
attr W is Circuit-like means :Def30: :: GLIB_001:def 30
( W is closed & W is Trail-like & not W is trivial );
attr W is Cycle-like means :Def31: :: GLIB_001:def 31
( W is closed & W is Path-like & not W is trivial );
end;

:: deftheorem Def30 defines Circuit-like GLIB_001:def 30 :
for G being _Graph
for W being Walk of G holds
( W is Circuit-like iff ( W is closed & W is Trail-like & not W is trivial ) );

:: deftheorem Def31 defines Cycle-like GLIB_001:def 31 :
for G being _Graph
for W being Walk of G holds
( W is Cycle-like iff ( W is closed & W is Path-like & not W is trivial ) );

Lm3: for G being _Graph
for W being Walk of G
for n being odd Nat st n <= len W holds
W . n in the_Vertices_of G
proof end;

Lm4: for G being _Graph
for W being Walk of G
for n being even Nat st n in dom W holds
ex naa1 being odd Nat st
( naa1 = n - 1 & n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G )
proof end;

Lm5: for G being _Graph
for W being Walk of G
for n being odd Nat st n < len W holds
( n in dom W & n + 1 in dom W & n + 2 in dom W )
proof end;

Lm6: for G being _Graph
for v being Vertex of G holds
( G .walkOf v is closed & G .walkOf v is directed & G .walkOf v is trivial & G .walkOf v is Trail-like & G .walkOf v is Path-like )
proof end;

Lm7: for G being _Graph
for x, e, y being set st e Joins x,y,G holds
len (G .walkOf x,e,y) = 3
proof end;

Lm8: for G being _Graph
for x, e, y being set st e Joins x,y,G holds
( (G .walkOf x,e,y) .first() = x & (G .walkOf x,e,y) .last() = y & G .walkOf x,e,y is_Walk_from x,y )
proof end;

Lm9: for G being _Graph
for W being Walk of G holds
( len W = len (W .reverse() ) & dom W = dom (W .reverse() ) & rng W = rng (W .reverse() ) )
by FINSEQ_5:def 3, FINSEQ_5:60;

Lm10: for G being _Graph
for W being Walk of G holds
( W .first() = (W .reverse() ) .last() & W .last() = (W .reverse() ) .first() )
proof end;

Lm11: for G being _Graph
for W being Walk of G
for n being Nat st n in dom (W .reverse() ) holds
( (W .reverse() ) . n = W . (((len W) - n) + 1) & ((len W) - n) + 1 in dom W )
proof end;

Lm12: for G being _Graph
for W being Walk of G holds (W .reverse() ) .reverse() = W
by FINSEQ_6:29;

Lm13: for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(len (W1 .append W2)) + 1 = (len W1) + (len W2)
proof end;

Lm14: for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
( len W1 <= len (W1 .append W2) & len W2 <= len (W1 .append W2) )
proof end;

Lm15: for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
( (W1 .append W2) .first() = W1 .first() & (W1 .append W2) .last() = W2 .last() & W1 .append W2 is_Walk_from W1 .first() ,W2 .last() )
proof end;

Lm16: for G being _Graph
for W1, W2 being Walk of G
for n being Nat st n in dom W1 holds
( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )
proof end;

Lm17: for G being _Graph
for W1, W2 being Walk of G st W1 .last() = W2 .first() holds
for n being Nat st n < len W2 holds
( (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) & (len W1) + n in dom (W1 .append W2) )
proof end;

Lm18: for G being _Graph
for W1, W2 being Walk of G
for n being Nat holds
( not n in dom (W1 .append W2) or n in dom W1 or ex k being Nat st
( k < len W2 & n = (len W1) + k ) )
proof end;

Lm19: for G being _Graph
for W being Walk of G
for m, n being odd Nat st m <= n & n <= len W holds
( (len (W .cut m,n)) + m = n + 1 & ( for i being Nat st i < len (W .cut m,n) holds
( (W .cut m,n) . (i + 1) = W . (m + i) & m + i in dom W ) ) )
proof end;

Lm20: for G being _Graph
for W being Walk of G
for m, n being odd Nat st m <= n & n <= len W holds
( (W .cut m,n) .first() = W . m & (W .cut m,n) .last() = W . n & W .cut m,n is_Walk_from W . m,W . n )
proof end;

Lm21: for G being _Graph
for W being Walk of G
for m, n, o being odd Nat st m <= n & n <= o & o <= len W holds
(W .cut m,n) .append (W .cut n,o) = W .cut m,o
proof end;

Lm22: for G being _Graph
for W being Walk of G holds W .cut 1,(len W) = W
proof end;

Lm23: for G being _Graph
for W being Walk of G
for n being odd Nat st n <= len W holds
W .cut n,n = <*(W .vertexAt n)*>
proof end;

Lm24: for G being _Graph
for W being Walk of G
for m, n being Nat st not m is even & m <= n holds
(W .cut 1,n) .cut 1,m = W .cut 1,m
proof end;

Lm25: for G being _Graph
for W1, W2 being Walk of G
for m, n being odd Nat st m <= n & n <= len W1 & W1 .last() = W2 .first() holds
(W1 .append W2) .cut m,n = W1 .cut m,n
proof end;

Lm26: for G being _Graph
for W being Walk of G
for m being odd Nat st m <= len W holds
len (W .cut 1,m) = m
proof end;

Lm27: for G being _Graph
for W being Walk of G
for m being odd Nat
for x being Nat st x in dom (W .cut 1,m) & m <= len W holds
(W .cut 1,m) . x = W . x
proof end;

Lm28: for G being _Graph
for W being Walk of G
for m, n being odd Nat st m <= n & n <= len W & W . m = W . n holds
(len (W .remove m,n)) + n = (len W) + m
proof end;

Lm29: for G being _Graph
for W being Walk of G
for m, n being Nat
for x, y being set st W is_Walk_from x,y holds
W .remove m,n is_Walk_from x,y
proof end;

Lm30: for G being _Graph
for W being Walk of G
for m, n being Nat holds len (W .remove m,n) <= len W
proof end;

Lm31: for G being _Graph
for W being Walk of G
for m being Nat holds W .remove m,m = W
proof end;

Lm32: for G being _Graph
for W being Walk of G
for m, n being odd Nat st m <= n & n <= len W & W . m = W . n holds
(W .cut 1,m) .last() = (W .cut n,(len W)) .first()
proof end;

Lm33: for G being _Graph
for W being Walk of G
for x, y being set
for m, n being odd Nat st m <= n & n <= len W & W . m = W . n holds
for x being Nat st x in Seg m holds
(W .remove m,n) . x = W . x
proof end;

Lm34: for G being _Graph
for W being Walk of G
for m, n being odd Nat st m <= n & n <= len W & W . m = W . n holds
for x being Nat st m <= x & x <= len (W .remove m,n) holds
( (W .remove m,n) . x = W . ((x - m) + n) & (x - m) + n is Nat & (x - m) + n <= len W )
proof end;

Lm35: for G being _Graph
for W being Walk of G
for m, n being odd Nat st m <= n & n <= len W & W . m = W . n holds
len (W .remove m,n) = ((len W) + m) - n
proof end;

Lm36: for G being _Graph
for W being Walk of G
for m being Nat st W .first() = W . m holds
W .remove 1,m = W .cut m,(len W)
proof end;

Lm37: for G being _Graph
for W being Walk of G
for m, n being Nat holds
( (W .remove m,n) .first() = W .first() & (W .remove m,n) .last() = W .last() )
proof end;

Lm38: for G being _Graph
for W being Walk of G
for m, n being odd Nat
for x being Nat st m <= n & n <= len W & W . m = W . n & x in dom (W .remove m,n) & not x in Seg m holds
( m <= x & x <= len (W .remove m,n) )
proof end;

Lm39: for G being _Graph
for W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
W .addEdge e = W ^ <*e,x*>
proof end;

Lm40: for G being _Graph
for W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = x & W .addEdge e is_Walk_from W .first() ,x )
proof end;

Lm41: for G being _Graph
for W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
len (W .addEdge e) = (len W) + 2
proof end;

Lm42: for G being _Graph
for W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
( (W .addEdge e) . ((len W) + 1) = e & (W .addEdge e) . ((len W) + 2) = x & ( for n being Nat st n in dom W holds
(W .addEdge e) . n = W . n ) )
proof end;

Lm43: for G being _Graph
for W being Walk of G
for e, x, y, z being set st W is_Walk_from x,y & e Joins y,z,G holds
W .addEdge e is_Walk_from x,z
proof end;

Lm44: for G being _Graph
for W being Walk of G
for n being even Nat st 1 <= n & n <= len W holds
( n div 2 in dom (W .edgeSeq() ) & W . n = (W .edgeSeq() ) . (n div 2) )
proof end;

Lm45: for G being _Graph
for W being Walk of G
for n being Nat holds
( n in dom (W .edgeSeq() ) iff 2 * n in dom W )
proof end;

Lm46: for G being _Graph
for W being Walk of G ex lenWaa1 being even Nat st
( lenWaa1 = (len W) - 1 & len (W .edgeSeq() ) = lenWaa1 div 2 )
proof end;

Lm47: for G being _Graph
for W being Walk of G
for n being Nat holds (W .cut 1,n) .edgeSeq() c= W .edgeSeq()
proof end;

Lm48: for G being _Graph
for W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
(W .addEdge e) .edgeSeq() = (W .edgeSeq() ) ^ <*e*>
proof end;

Lm49: for G being _Graph
for W being Walk of G
for x being set holds
( x in W .vertices() iff ex n being odd Nat st
( n <= len W & W . n = x ) )
proof end;

Lm50: for G being _Graph
for W being Walk of G
for e being set holds
( e in W .edges() iff ex n being even Nat st
( 1 <= n & n <= len W & W . n = e ) )
proof end;

Lm51: for G being _Graph
for W being Walk of G
for e being set st e in W .edges() holds
ex v1, v2 being Vertex of G ex n being odd Nat st
( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )
proof end;

Lm52: for G being _Graph
for W being Walk of G
for e, x, y being set st e in W .edges() & e Joins x,y,G holds
( x in W .vertices() & y in W .vertices() )
proof end;

Lm53: for G being _Graph
for W being Walk of G holds len W = (2 * (W .length() )) + 1
by Def15;

Lm54: for G being _Graph
for W being Walk of G
for n being odd Nat st n <= len W holds
W .find n <= n
proof end;

Lm55: for G being _Graph
for W being Walk of G
for n being odd Nat st n <= len W holds
W .rfind n >= n
proof end;

Lm56: for G being _Graph
for W being Walk of G holds
( W is directed iff for n being odd Nat st n < len W holds
W . (n + 1) DJoins W . n,W . (n + 2),G )
proof end;

Lm57: for G being _Graph
for W being Walk of G
for x, e, y, z being set st W is directed & W is_Walk_from x,y & e DJoins y,z,G holds
( W .addEdge e is directed & W .addEdge e is_Walk_from x,z )
proof end;

Lm58: for G being _Graph
for W being Walk of G
for m, n being Nat st W is directed holds
W .cut m,n is directed
proof end;

Lm59: for G being _Graph
for W being Walk of G holds
( not W is trivial iff 3 <= len W )
proof end;

Lm60: for G being _Graph
for W being Walk of G holds
( not W is trivial iff len W <> 1 )
proof end;

Lm61: for G being _Graph
for W being Walk of G holds
( W is trivial iff ex v being Vertex of G st W = G .walkOf v )
proof end;

Lm62: for G being _Graph
for W being Walk of G holds
( W is Trail-like iff for m, n being even Nat st 1 <= m & m < n & n <= len W holds
W . m <> W . n )
proof end;

Lm63: for G being _Graph
for W being Walk of G holds
( W is Trail-like iff W .reverse() is Trail-like )
proof end;

Lm64: for G being _Graph
for W being Walk of G
for m, n being Nat st W is Trail-like holds
W .cut m,n is Trail-like
proof end;

Lm65: for G being _Graph
for W being Walk of G
for e being set st W is Trail-like & e in (W .last() ) .edgesInOut() & not e in W .edges() holds
W .addEdge e is Trail-like
proof end;

Lm66: for G being _Graph
for W being Walk of G st len W <= 3 holds
W is Trail-like
proof end;

Lm67: for G being _Graph
for x, e, y being set st e Joins x,y,G holds
G .walkOf x,e,y is Path-like
proof end;

Lm68: for G being _Graph
for W being Walk of G holds
( W is Path-like iff W .reverse() is Path-like )
proof end;

Lm69: for G being _Graph
for W being Walk of G
for m, n being Nat st W is Path-like holds
W .cut m,n is Path-like
proof end;

Lm70: for G being _Graph
for W being Walk of G
for e, v being set st W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or not W is closed ) & ( for n being odd Nat st 1 < n & n <= len W holds
W . n <> v ) holds
W .addEdge e is Path-like
proof end;

Lm71: for G being _Graph
for W being Walk of G st ( for m, n being odd Nat st m <= len W & n <= len W & W . m = W . n holds
m = n ) holds
W is Path-like
proof end;

Lm72: for G being _Graph
for W being Walk of G st ( for n being odd Nat st n <= len W holds
W .rfind n = n ) holds
W is Path-like
proof end;

Lm73: for G being _Graph
for W being Walk of G
for e, v being set st e Joins W .last() ,v,G & W is Path-like & not v in W .vertices() & ( W is trivial or not W is closed ) holds
W .addEdge e is Path-like
proof end;

Lm74: for G being _Graph
for W being Walk of G st len W <= 3 holds
W is Path-like
proof end;

registration
let G be _Graph;
cluster Path-like -> Trail-like Walk of G;
correctness
coherence
for b1 being Walk of G st b1 is Path-like holds
b1 is Trail-like
;
by Def28;
cluster trivial -> Path-like Walk of G;
correctness
coherence
for b1 being Walk of G st b1 is trivial holds
b1 is Path-like
;
proof end;
cluster trivial -> vertex-distinct Walk of G;
coherence
for b1 being Walk of G st b1 is trivial holds
b1 is vertex-distinct
proof end;
cluster vertex-distinct -> Path-like Walk of G;
coherence
for b1 being Walk of G st b1 is vertex-distinct holds
b1 is Path-like
proof end;
cluster Circuit-like -> closed non trivial Trail-like Walk of G;
correctness
coherence
for b1 being Walk of G st b1 is Circuit-like holds
( b1 is closed & b1 is Trail-like & not b1 is trivial )
;
by Def30;
cluster Cycle-like -> closed non trivial Path-like Walk of G;
correctness
coherence
for b1 being Walk of G st b1 is Cycle-like holds
( b1 is closed & b1 is Path-like & not b1 is trivial )
;
by Def31;
end;

registration
let G be _Graph;
cluster closed directed trivial Trail-like Path-like vertex-distinct Walk of G;
existence
ex b1 being Walk of G st
( b1 is closed & b1 is directed & b1 is trivial )
proof end;
end;

registration
let G be _Graph;
cluster Trail-like Path-like vertex-distinct Walk of G;
existence
ex b1 being Walk of G st b1 is vertex-distinct
proof end;
end;

definition
let G be _Graph;
mode Trail of G is Trail-like Walk of G;
mode Path of G is Path-like Walk of G;
end;

definition
let G be _Graph;
mode DWalk of G is directed Walk of G;
mode DTrail of G is directed Trail of G;
mode DPath of G is directed Path of G;
end;

registration
let G be _Graph;
let v be Vertex of G;
cluster G .walkOf v -> closed directed trivial Trail-like Path-like vertex-distinct ;
coherence
( G .walkOf v is closed & G .walkOf v is directed & G .walkOf v is trivial )
by Lm6;
end;

registration
let G be _Graph;
let x, e, y be set ;
cluster G .walkOf x,e,y -> Trail-like Path-like ;
coherence
G .walkOf x,e,y is Path-like
proof end;
end;

registration
let G be _Graph;
let x, e be set ;
cluster G .walkOf x,e,x -> closed Trail-like Path-like ;
coherence
G .walkOf x,e,x is closed
proof end;
end;

registration
let G be _Graph;
let W be closed Walk of G;
cluster W .reverse() -> closed ;
coherence
W .reverse() is closed
proof end;
end;

registration
let G be _Graph;
let W be trivial Walk of G;
cluster W .reverse() -> trivial Trail-like Path-like vertex-distinct ;
coherence
W .reverse() is trivial
proof end;
end;

registration
let G be _Graph;
let W be Trail of G;
cluster W .reverse() -> Trail-like ;
coherence
W .reverse() is Trail-like
by Lm63;
end;

registration
let G be _Graph;
let W be Path of G;
cluster W .reverse() -> Trail-like Path-like ;
coherence
W .reverse() is Path-like
by Lm68;
end;

registration
let G be _Graph;
let W1, W2 be closed Walk of G;
cluster W1 .append W2 -> closed ;
coherence
W1 .append W2 is closed
proof end;
end;

registration
let G be _Graph;
let W1, W2 be DWalk of G;
cluster W1 .append W2 -> directed ;
coherence
W1 .append W2 is directed
proof end;
end;

registration
let G be _Graph;
let W1, W2 be trivial Walk of G;
cluster W1 .append W2 -> trivial Trail-like Path-like vertex-distinct ;
coherence
W1 .append W2 is trivial
proof end;
end;

registration
let G be _Graph;
let W be DWalk of G;
let m, n be Nat;
cluster W .cut m,n -> directed ;
coherence
W .cut m,n is directed
by Lm58;
end;

registration
let G be _Graph;
let W be trivial Walk of G;
let m, n be Nat;
cluster W .cut m,n -> trivial Trail-like Path-like vertex-distinct ;
coherence
W .cut m,n is trivial
proof end;
end;

registration
let G be _Graph;
let W be Trail of G;
let m, n be Nat;
cluster W .cut m,n -> Trail-like ;
coherence
W .cut m,n is Trail-like
by Lm64;
end;

registration
let G be _Graph;
let W be Path of G;
let m, n be Nat;
cluster W .cut m,n -> Trail-like Path-like ;
coherence
W .cut m,n is Path-like
by Lm69;
end;

registration
let G be _Graph;
let W be vertex-distinct Walk of G;
let m, n be Nat;
cluster W .cut m,n -> Trail-like Path-like vertex-distinct ;
coherence
W .cut m,n is vertex-distinct
proof end;
end;

registration
let G be _Graph;
let W be closed Walk of G;
let m, n be Nat;
cluster W .remove m,n -> closed ;
coherence
W .remove m,n is closed
proof end;
end;

registration
let G be _Graph;
let W be DWalk of G;
let m, n be Nat;
cluster W .remove m,n -> directed ;
coherence
W .remove m,n is directed
proof end;
end;

registration
let G be _Graph;
let W be trivial Walk of G;
let m, n be Nat;
cluster W .remove m,n -> trivial Trail-like Path-like vertex-distinct ;
coherence
W .remove m,n is trivial
proof end;
end;

registration
let G be _Graph;
let W be Trail of G;
let m, n be Nat;
cluster W .remove m,n -> Trail-like ;
coherence
W .remove m,n is Trail-like
proof end;
end;

registration
let G be _Graph;
let W be Path of G;
let m, n be Nat;
cluster W .remove m,n -> Trail-like Path-like ;
coherence
W .remove m,n is Path-like
proof end;
end;

definition
let G be _Graph;
let W be Walk of G;
mode Subwalk of W -> Walk of G means :Def32: :: GLIB_001:def 32
( it is_Walk_from W .first() ,W .last() & ex es being FinSubsequence of W .edgeSeq() st it .edgeSeq() = Seq es );
existence
ex b1 being Walk of G st
( b1 is_Walk_from W .first() ,W .last() & ex es being FinSubsequence of W .edgeSeq() st b1 .edgeSeq() = Seq es )
proof end;
end;

:: deftheorem Def32 defines Subwalk GLIB_001:def 32 :
for G being _Graph
for W, b3 being Walk of G holds
( b3 is Subwalk of W iff ( b3 is_Walk_from W .first() ,W .last() & ex es being FinSubsequence of W .edgeSeq() st b3 .edgeSeq() = Seq es ) );

Lm75: for G being _Graph
for W being Walk of G holds W is Subwalk of W
proof end;

Lm76: for G being _Graph
for W1 being Walk of G
for W2 being Subwalk of W1
for W3 being Subwalk of W2 holds W3 is Subwalk of W1
proof end;

Lm77: for G being _Graph
for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
len W1 <= len W2
proof end;

definition
let G be _Graph;
let W be Walk of G;
let m, n be Nat;
:: original: .remove
redefine func W .remove m,n -> Subwalk of W;
coherence
W .remove m,n is Subwalk of W
proof end;
end;

registration
let G be _Graph;
let W be Walk of G;
cluster Trail-like Path-like Subwalk of W;
existence
ex b1 being Subwalk of W st
( b1 is Trail-like & b1 is Path-like )
proof end;
end;

definition
let G be _Graph;
let W be Walk of G;
mode Trail of W is Trail-like Subwalk of W;
mode Path of W is Path-like Subwalk of W;
end;

registration
let G be _Graph;
let W be DWalk of G;
cluster directed Subwalk of W;
existence
ex b1 being Path of W st b1 is directed
proof end;
end;

definition
let G be _Graph;
let W be DWalk of G;
mode DWalk of W is directed Subwalk of W;
mode DTrail of W is directed Trail of W;
mode DPath of W is directed Path of W;
end;

definition
let G be _Graph;
func G .allWalks() -> non empty Subset of (((the_Vertices_of G) \/ (the_Edges_of G)) * ) equals :: GLIB_001:def 33
{ W where W is Walk of G : verum } ;
coherence
{ W where W is Walk of G : verum } is non empty Subset of (((the_Vertices_of G) \/ (the_Edges_of G)) * )
proof end;
end;

:: deftheorem defines .allWalks() GLIB_001:def 33 :
for G being _Graph holds G .allWalks() = { W where W is Walk of G : verum } ;

definition
let G be _Graph;
func G .allTrails() -> non empty Subset of (G .allWalks() ) equals :: GLIB_001:def 34
{ W where W is Trail of G : verum } ;
coherence
{ W where W is Trail of G : verum } is non empty Subset of (G .allWalks() )
proof end;
end;

:: deftheorem defines .allTrails() GLIB_001:def 34 :
for G being _Graph holds G .allTrails() = { W where W is Trail of G : verum } ;

definition
let G be _Graph;
func G .allPaths() -> non empty Subset of (G .allTrails() ) equals :: GLIB_001:def 35
{ W where W is Path of G : verum } ;
coherence
{ W where W is Path of G : verum } is non empty Subset of (G .allTrails() )
proof end;
end;

:: deftheorem defines .allPaths() GLIB_001:def 35 :
for G being _Graph holds G .allPaths() = { W where W is Path of G : verum } ;

definition
let G be _Graph;
func G .allDWalks() -> non empty Subset of (G .allWalks() ) equals :: GLIB_001:def 36
{ W where W is DWalk of G : verum } ;
coherence
{ W where W is DWalk of G : verum } is non empty Subset of (G .allWalks() )
proof end;
end;

:: deftheorem defines .allDWalks() GLIB_001:def 36 :
for G being _Graph holds G .allDWalks() = { W where W is DWalk of G : verum } ;

definition
let G be _Graph;
func G .allDTrails() -> non empty Subset of (G .allTrails() ) equals :: GLIB_001:def 37
{ W where W is DTrail of G : verum } ;
coherence
{ W where W is DTrail of G : verum } is non empty Subset of (G .allTrails() )
proof end;
end;

:: deftheorem defines .allDTrails() GLIB_001:def 37 :
for G being _Graph holds G .allDTrails() = { W where W is DTrail of G : verum } ;

definition
let G be _Graph;
func G .allDPaths() -> non empty Subset of (G .allDTrails() ) equals :: GLIB_001:def 38
{ W where W is directed Path of G : verum } ;
coherence
{ W where W is directed Path of G : verum } is non empty Subset of (G .allDTrails() )
proof end;
end;

:: deftheorem defines .allDPaths() GLIB_001:def 38 :
for G being _Graph holds G .allDPaths() = { W where W is directed Path of G : verum } ;

registration
let G be finite _Graph;
cluster G .allTrails() -> non empty finite ;
correctness
coherence
G .allTrails() is finite
;
proof end;
end;

definition
let G be _Graph;
let X be non empty Subset of (G .allWalks() );
:: original: Element
redefine mode Element of X -> Walk of G;
coherence
for b1 being Element of X holds b1 is Walk of G
proof end;
end;

definition
let G be _Graph;
let X be non empty Subset of (G .allTrails() );
:: original: Element
redefine mode Element of X -> Trail of G;
coherence
for b1 being Element of X holds b1 is Trail of G
proof end;
end;

definition
let G be _Graph;
let X be non empty Subset of (G .allPaths() );
:: original: Element
redefine mode Element of X -> Path of G;
coherence
for b1 being Element of X holds b1 is Path of G
proof end;
end;

definition
let G be _Graph;
let X be non empty Subset of (G .allDWalks() );
:: original: Element
redefine mode Element of X -> DWalk of G;
coherence
for b1 being Element of X holds b1 is DWalk of G
proof end;
end;

definition
let G be _Graph;
let X be non empty Subset of (G .allDTrails() );
:: original: Element
redefine mode Element of X -> DTrail of G;
coherence
for b1 being Element of X holds b1 is DTrail of G
proof end;
end;

definition
let G be _Graph;
let X be non empty Subset of (G .allDPaths() );
:: original: Element
redefine mode Element of X -> DPath of G;
coherence
for b1 being Element of X holds b1 is DPath of G
proof end;
end;

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

theorem :: GLIB_001:8  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 W being Walk of G
for n being odd Nat st n <= len W holds
W . n in the_Vertices_of G by Lm3;

theorem Th9: :: GLIB_001:9  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 W being Walk of G
for n being even Nat st n in dom W holds
W . n in the_Edges_of G
proof end;

theorem :: GLIB_001:10  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 W being Walk of G
for n being even Nat st n in dom W holds
ex naa1 being odd Nat st
( naa1 = n - 1 & n - 1 in dom W & n + 1 in dom W & W . n Joins W . naa1,W . (n + 1),G ) by Lm4;

theorem Th11: :: GLIB_001:11  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 W being Walk of G
for n being odd Nat st n < len W holds
W . (n + 1) in (W .vertexAt n) .edgesInOut()
proof end;

theorem Th12: :: GLIB_001:12  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 W being Walk of G
for n being odd Nat st 1 < n & n <= len W holds
W . (n - 1) in (W .vertexAt n) .edgesInOut()
proof end;

theorem :: GLIB_001:13  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 W being Walk of G
for n being odd Nat st n < len W holds
( n in dom W & n + 1 in dom W & n + 2 in dom W )
proof end;

theorem Th14: :: GLIB_001:14  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 Vertex of G holds
( len (G .walkOf v) = 1 & (G .walkOf v) . 1 = v & (G .walkOf v) .first() = v & (G .walkOf v) .last() = v & G .walkOf v is_Walk_from v,v )
proof end;

theorem Th15: :: GLIB_001:15  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 e, x, y being set st e Joins x,y,G holds
len (G .walkOf x,e,y) = 3
proof end;

theorem Th16: :: GLIB_001:16  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 e, x, y being set st e Joins x,y,G holds
( (G .walkOf x,e,y) .first() = x & (G .walkOf x,e,y) .last() = y & G .walkOf x,e,y is_Walk_from x,y )
proof end;

theorem :: GLIB_001:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( W1 .first() = W2 .first() & W1 .last() = W2 .last() ) ;

theorem Th18: :: GLIB_001:18  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 W being Walk of G
for x, y being set holds
( W is_Walk_from x,y iff ( W . 1 = x & W . (len W) = y ) )
proof end;

theorem :: GLIB_001:19  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 W being Walk of G
for x, y being set st W is_Walk_from x,y holds
( x is Vertex of G & y is Vertex of G )
proof end;

theorem :: GLIB_001:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for x, y being set
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( W1 is_Walk_from x,y iff W2 is_Walk_from x,y )
proof end;

theorem :: GLIB_001:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
for n being Nat holds W1 .vertexAt n = W2 .vertexAt n
proof end;

theorem :: GLIB_001:22  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 W being Walk of G holds
( len W = len (W .reverse() ) & dom W = dom (W .reverse() ) & rng W = rng (W .reverse() ) ) by Lm9;

theorem Th23: :: GLIB_001:23  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 W being Walk of G holds
( W .first() = (W .reverse() ) .last() & W .last() = (W .reverse() ) .first() )
proof end;

theorem Th24: :: GLIB_001:24  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 W being Walk of G
for x, y being set holds
( W is_Walk_from x,y iff W .reverse() is_Walk_from y,x )
proof end;

theorem Th25: :: GLIB_001:25  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 W being Walk of G
for n being Nat st n in dom W holds
( W . n = (W .reverse() ) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse() ) )
proof end;

theorem :: GLIB_001:26  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 W being Walk of G
for n being Nat st n in dom (W .reverse() ) holds
( (W .reverse() ) . n = W . (((len W) - n) + 1) & ((len W) - n) + 1 in dom W ) by Lm11;

theorem :: GLIB_001:27  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 W being Walk of G holds (W .reverse() ) .reverse() = W by Lm12;

theorem :: GLIB_001:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .reverse() = W2 .reverse() ;

theorem :: GLIB_001:29  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 W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(len (W1 .append W2)) + 1 = (len W1) + (len W2) by Lm13;

theorem :: GLIB_001:30  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 W1, W2 being Walk of G st W1 .last() = W2 .first() holds
( len W1 <= len (W1 .append W2) & len W2 <= len (W1 .append W2) ) by Lm14;

theorem :: GLIB_001: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 W1, W2 being Walk of G st W1 .last() = W2 .first() holds
( (W1 .append W2) .first() = W1 .first() & (W1 .append W2) .last() = W2 .last() & W1 .append W2 is_Walk_from W1 .first() ,W2 .last() ) by Lm15;

theorem Th32: :: GLIB_001: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 W1, W2 being Walk of G
for x, y, z being set st W1 is_Walk_from x,y & W2 is_Walk_from y,z holds
W1 .append W2 is_Walk_from x,z
proof end;

theorem :: GLIB_001:33  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 W1, W2 being Walk of G
for n being Nat st n in dom W1 holds
( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) ) by Lm16;

theorem :: GLIB_001: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 W1, W2 being Walk of G st W1 .last() = W2 .first() holds
for n being Nat st n < len W2 holds
( (W1 .append W2) . ((len W1) + n) = W2 . (n + 1) & (len W1) + n in dom (W1 .append W2) ) by Lm17;

theorem :: GLIB_001: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 W1, W2 being Walk of G
for n being Nat holds
( not n in dom (W1 .append W2) or n in dom W1 or ex k being Nat st
( k < len W2 & n = (len W1) + k ) ) by Lm18;

theorem Th36: :: GLIB_001:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1A, W1B being Walk of G1
for W2A, W2B being Walk of G2 st W1A = W2A & W1B = W2B holds
W1A .append W1B = W2A .append W2B
proof end;

theorem :: GLIB_001: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 W being Walk of G
for m, n being odd Nat st m <= n & n <= len W holds
( (len (W .cut m,n)) + m = n + 1 & ( for i being Nat st i < len (W .cut m,n) holds
( (W .cut m,n) . (i + 1) = W . (m + i) & m + i in dom W ) ) ) by Lm19;

theorem :: GLIB_001: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 W being Walk of G
for m, n being odd Nat st m <= n & n <= len W holds
( (W .cut m,n) .first() = W . m & (W .cut m,n) .last() = W . n & W .cut m,n is_Walk_from W . m,W . n ) by Lm20;

theorem :: GLIB_001: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 W being Walk of G
for m, n, o being odd Nat st m <= n & n <= o & o <= len W holds
(W .cut m,n) .append (W .cut n,o) = W .cut m,o by Lm21;

theorem :: GLIB_001: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 W being Walk of G holds W .cut 1,(len W) = W by Lm22;

theorem Th41: :: GLIB_001: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 W being Walk of G
for n being odd Nat st n < len W holds
G .walkOf (W . n),(W . (n + 1)),(W . (n + 2)) = W .cut n,(n + 2)
proof end;

theorem Th42: :: GLIB_001: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 W being Walk of G
for m, n being odd Nat st m <= n & n < len W holds
(W .cut m,n) .addEdge (W . (n + 1)) = W .cut m,(n + 2)
proof end;

theorem :: GLIB_001:43  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 W being Walk of G
for n being odd Nat st n <= len W holds
W .cut n,n = <*(W .vertexAt n)*> by Lm23;

theorem :: GLIB_001:44  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 W being Walk of G
for m, n being Nat st not m is even & m <= n holds
(W .cut 1,n) .cut 1,m = W .cut 1,m by Lm24;

theorem :: GLIB_001:45  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 W1, W2 being Walk of G
for m, n being odd Nat st m <= n & n <= len W1 & W1 .last() = W2 .first() holds
(W1 .append W2) .cut m,n = W1 .cut m,n by Lm25;

theorem :: GLIB_001: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 W being Walk of G
for m being odd Nat st m <= len W holds
len (W .cut 1,m) = m by Lm26;

theorem :: GLIB_001: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 W being Walk of G
for m being odd Nat
for x being Nat st x in dom (W .cut 1,m) & m <= len W holds
(W .cut 1,m) . x = W . x by Lm27;

theorem :: GLIB_001:48  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 W being Walk of G
for m, n being odd Nat
for i being Nat st m <= n & n <= len W & i in dom (W .cut m,n) holds
( (W .cut m,n) . i = W . ((m + i) - 1) & (m + i) - 1 in dom W )
proof end;

theorem Th49: :: GLIB_001:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2
for m, n being Nat st W1 = W2 holds
W1 .cut m,n = W2 .cut m,n
proof end;

theorem :: GLIB_001: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 W being Walk of G
for m, n being odd Nat st m <= n & n <= len W & W . m = W . n holds
(len (W .remove m,n)) + n = (len W) + m by Lm28;

theorem :: GLIB_001: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 W being Walk of G
for x, y being set
for m, n being Nat st W is_Walk_from x,y holds
W .remove m,n is_Walk_from x,y by Lm29;

theorem :: GLIB_001: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 W being Walk of G
for m, n being Nat holds len (W .remove m,n) <= len W by Lm30;

theorem :: GLIB_001: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 W being Walk of G
for m being Nat holds W .remove m,m = W by Lm31;

theorem :: GLIB_001:54  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 W being Walk of G
for m, n being odd Nat st m <= n & n <= len W & W . m = W . n holds
(W .cut 1,m) .last() = (W .cut n,(len W)) .first() by Lm32;

theorem :: GLIB_001: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 W being Walk of G
for m, n being odd Nat st m <= n & n <= len W & W . m = W . n holds
for x being Nat st x in Seg m holds
(W .remove m,n) . x = W . x by Lm33;

theorem :: GLIB_001: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 W being Walk of G
for m, n being odd Nat st m <= n & n <= len W & W . m = W . n holds
for x being Nat st m <= x & x <= len (W .remove m,n) holds
( (W .remove m,n) . x = W . ((x - m) + n) & (x - m) + n is Nat & (x - m) + n <= len W ) by Lm34;

theorem :: GLIB_001:57  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 W being Walk of G
for m, n being odd Nat st m <= n & n <= len W & W . m = W . n holds
len (W .remove m,n) = ((len W) + m) - n by Lm35;

theorem Th58: :: GLIB_001:58  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 W being Walk of G
for m being Nat st W . m = W .last() holds
W .remove m,(len W) = W .cut 1,m
proof end;

theorem :: GLIB_001:59  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 W being Walk of G
for m being Nat st W .first() = W . m holds
W .remove 1,m = W .cut m,(len W) by Lm36;

theorem :: GLIB_001:60  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 W being Walk of G
for m, n being Nat holds
( (W .remove m,n) .first() = W .first() & (W .remove m,n) .last() = W .last() ) by Lm37;

theorem :: GLIB_001:61  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 W being Walk of G
for m, n being odd Nat
for x being Nat st m <= n & n <= len W & W . m = W . n & x in dom (W .remove m,n) & not x in Seg m holds
( m <= x & x <= len (W .remove m,n) ) by Lm38;

theorem :: GLIB_001:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2
for m, n being Nat st W1 = W2 holds
W1 .remove m,n = W2 .remove m,n
proof end;

theorem :: GLIB_001:63  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 W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
W .addEdge e = W ^ <*e,x*> by Lm39;

theorem :: GLIB_001:64  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 W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
( (W .addEdge e) .first() = W .first() & (W .addEdge e) .last() = x & W .addEdge e is_Walk_from W .first() ,x ) by Lm40;

theorem :: GLIB_001:65  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 W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
len (W .addEdge e) = (len W) + 2 by Lm41;

theorem :: GLIB_001:66  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 W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
( (W .addEdge e) . ((len W) + 1) = e & (W .addEdge e) . ((len W) + 2) = x & ( for n being Nat st n in dom W holds
(W .addEdge e) . n = W . n ) ) by Lm42;

theorem :: GLIB_001:67  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 W being Walk of G
for x, y, e, z being set st W is_Walk_from x,y & e Joins y,z,G holds
W .addEdge e is_Walk_from x,z by Lm43;

theorem Th68: :: GLIB_001:68  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 W being Walk of G holds 1 <= len (W .vertexSeq() )
proof end;

theorem Th69: :: GLIB_001:69  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 W being Walk of G
for n being odd Nat st n <= len W holds
( (2 * ((n + 1) div 2)) - 1 = n & 1 <= (n + 1) div 2 & (n + 1) div 2 <= len (W .vertexSeq() ) )
proof end;

theorem :: GLIB_001:70  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 Vertex of G holds (G .walkOf v) .vertexSeq() = <*v*>
proof end;

theorem Th71: :: GLIB_001:71  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 e, x, y being set st e Joins x,y,G holds
(G .walkOf x,e,y) .vertexSeq() = <*x,y*>
proof end;

theorem :: GLIB_001:72  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 W being Walk of G holds
( W .first() = (W .vertexSeq() ) . 1 & W .last() = (W .vertexSeq() ) . (len (W .vertexSeq() )) )
proof end;

theorem :: GLIB_001:73  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 W being Walk of G
for n being odd Nat st n <= len W holds
W .vertexAt n = (W .vertexSeq() ) . ((n + 1) div 2)
proof end;

theorem Th74: :: GLIB_001:74  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 W being Walk of G
for n being Nat holds
( n in dom (W .vertexSeq() ) iff (2 * n) - 1 in dom W )
proof end;

theorem :: GLIB_001:75  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 W being Walk of G
for n being Nat holds (W .cut 1,n) .vertexSeq() c= W .vertexSeq()
proof end;

theorem Th76: :: GLIB_001:76  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 W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
(W .addEdge e) .vertexSeq() = (W .vertexSeq() ) ^ <*x*>
proof end;

theorem Th77: :: GLIB_001:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .vertexSeq() = W2 .vertexSeq()
proof end;

theorem :: GLIB_001:78  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 W being Walk of G
for n being even Nat st 1 <= n & n <= len W holds
( n div 2 in dom (W .edgeSeq() ) & W . n = (W .edgeSeq() ) . (n div 2) ) by Lm44;

theorem :: GLIB_001:79  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 W being Walk of G
for n being Nat holds
( n in dom (W .edgeSeq() ) iff 2 * n in dom W ) by Lm45;

theorem :: GLIB_001:80  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 W being Walk of G
for n being Nat st n in dom (W .edgeSeq() ) holds
(W .edgeSeq() ) . n in the_Edges_of G
proof end;

theorem :: GLIB_001:81  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 W being Walk of G ex lenWaa1 being even Nat st
( lenWaa1 = (len W) - 1 & len (W .edgeSeq() ) = lenWaa1 div 2 ) by Lm46;

theorem :: GLIB_001:82  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 W being Walk of G
for n being Nat holds (W .cut 1,n) .edgeSeq() c= W .edgeSeq() by Lm47;

theorem :: GLIB_001:83  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 W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
(W .addEdge e) .edgeSeq() = (W .edgeSeq() ) ^ <*e*> by Lm48;

theorem Th84: :: GLIB_001:84  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 e, x, y being set holds
( e Joins x,y,G iff (G .walkOf x,e,y) .edgeSeq() = <*e*> )
proof end;

theorem :: GLIB_001:85  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 W being Walk of G holds (W .reverse() ) .edgeSeq() = Rev (W .edgeSeq() )
proof end;

theorem :: GLIB_001:86  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 W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .edgeSeq() = (W1 .edgeSeq() ) ^ (W2 .edgeSeq() )
proof end;

theorem Th87: :: GLIB_001:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .edgeSeq() = W2 .edgeSeq()
proof end;

theorem :: GLIB_001:88  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 W being Walk of G
for x being set holds
( x in W .vertices() iff ex n being odd Nat st
( n <= len W & W . n = x ) ) by Lm49;

theorem Th89: :: GLIB_001:89  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 W being Walk of G holds
( W .first() in W .vertices() & W .last() in W .vertices() )
proof end;

theorem Th90: :: GLIB_001:90  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 W being Walk of G
for n being odd Nat st n <= len W holds
W .vertexAt n in W .vertices()
proof end;

theorem :: GLIB_001:91  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 Vertex of G holds (G .walkOf v) .vertices() = {v}
proof end;

theorem Th92: :: GLIB_001:92  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 e, x, y being set st e Joins x,y,G holds
(G .walkOf x,e,y) .vertices() = {x,y}
proof end;

theorem :: GLIB_001:93  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 W being Walk of G holds W .vertices() = (W .reverse() ) .vertices()
proof end;

theorem Th94: :: GLIB_001:94  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 W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .vertices() = (W1 .vertices() ) \/ (W2 .vertices() )
proof end;

theorem :: GLIB_001:95  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 W being Walk of G
for m, n being odd Nat st m <= n & n <= len W holds
(W .cut m,n) .vertices() c= W .vertices()
proof end;

theorem Th96: :: GLIB_001:96  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 W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
(W .addEdge e) .vertices() = (W .vertices() ) \/ {x}
proof end;

theorem :: GLIB_001:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite _Graph
for W being Walk of G
for e, x being set st e Joins W .last() ,x,G & not x in W .vertices() holds
card ((W .addEdge e) .vertices() ) = (card (W .vertices() )) + 1
proof end;

theorem :: GLIB_001:98  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 W being Walk of G
for x, y being set st x in W .vertices() & y in W .vertices() holds
ex W' being Walk of G st W' is_Walk_from x,y
proof end;

theorem Th99: :: GLIB_001:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .vertices() = W2 .vertices() by Th77;

theorem :: GLIB_001:100  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 W being Walk of G
for e being set holds
( e in W .edges() iff ex n being even Nat st
( 1 <= n & n <= len W & W . n = e ) ) by Lm50;

theorem Th101: :: GLIB_001:101  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 W being Walk of G
for e being set holds
( e in W .edges() iff ex n being odd Nat st
( n < len W & W . (n + 1) = e ) )
proof end;

theorem Th102: :: GLIB_001:102  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 W being Walk of G holds rng W = (W .vertices() ) \/ (W .edges() )
proof end;

theorem Th103: :: GLIB_001:103  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 W1, W2 being Walk of G st W1 .last() = W2 .first() holds
(W1 .append W2) .edges() = (W1 .edges() ) \/ (W2 .edges() )
proof end;

theorem :: GLIB_001:104  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 W being Walk of G
for e being set st e in W .edges() holds
ex v1, v2 being Vertex of G ex n being odd Nat st
( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G ) by Lm51;

theorem Th105: :: GLIB_001:105  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 W being Walk of G
for e being set holds
( e in W .edges() iff ex n being Nat st
( n in dom (W .edgeSeq() ) & (W .edgeSeq() ) . n = e ) )
proof end;

theorem :: GLIB_001:106  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 W being Walk of G
for e, x, y being set st e in W .edges() & e Joins x,y,G holds
( x in W .vertices() & y in W .vertices() ) by Lm52;

theorem :: GLIB_001:107  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 W being Walk of G
for m, n being Nat holds (W .cut m,n) .edges() c= W .edges()
proof end;

theorem Th108: :: GLIB_001:108  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 W being Walk of G holds W .edges() = (W .reverse() ) .edges()
proof end;

theorem Th109: :: GLIB_001:109  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 e, x, y being set holds
( e Joins x,y,G iff (G .walkOf x,e,y) .edges() = {e} )
proof end;

theorem :: GLIB_001:110  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 W being Walk of G holds W .edges() c= G .edgesBetween (W .vertices() )
proof end;

theorem :: GLIB_001:111  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .edges() = W2 .edges() by Th87;

theorem :: GLIB_001:112  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 W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
(W .addEdge e) .edges() = (W .edges() ) \/ {e}
proof end;

theorem :: GLIB_001:113  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 W being Walk of G holds len W = (2 * (W .length() )) + 1 by Lm53;

theorem :: GLIB_001:114  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 W1, W2 being Walk of G holds
( len W1 = len W2 iff W1 .length() = W2 .length() )
proof end;

theorem :: GLIB_001:115  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
W1 .length() = W2 .length() by Th87;

theorem Th116: :: GLIB_001:116  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 W being Walk of G
for n being odd Nat st n <= len W holds
( W .find (W . n) <= n & W .rfind (W . n) >= n )
proof end;

theorem :: GLIB_001:117  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2
for v being set st W1 = W2 holds
( W1 .find v = W2 .find v & W1 .rfind v = W2 .rfind v )
proof end;

theorem :: GLIB_001:118  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 W being Walk of G
for n being odd Nat st n <= len W holds
( W .find n <= n & W .rfind n >= n ) by Lm54, Lm55;

theorem Th119: :: GLIB_001:119  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 W being Walk of G holds
( W is closed iff W . 1 = W . (len W) )
proof end;

theorem :: GLIB_001:120  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 W being Walk of G holds
( W is closed iff ex x being set st W is_Walk_from x,x )
proof end;

theorem :: GLIB_001:121  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 W being Walk of G holds
( W is closed iff W .reverse() is closed )
proof end;

theorem :: GLIB_001:122  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is closed holds
W2 is closed
proof end;

theorem :: GLIB_001:123  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 W being Walk of G holds
( W is directed iff for n being odd Nat st n < len W holds
W . (n + 1) DJoins W . n,W . (n + 2),G ) by Lm56;

theorem :: GLIB_001:124  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 W being Walk of G
for x, y, e, z being set st W is directed & W is_Walk_from x,y & e DJoins y,z,G holds
( W .addEdge e is directed & W .addEdge e is_Walk_from x,z ) by Lm57;

theorem :: GLIB_001:125  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 W being DWalk of G
for m, n being Nat holds W .cut m,n is directed ;

theorem :: GLIB_001:126  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 W being Walk of G holds
( not W is trivial iff 3 <= len W ) by Lm59;

theorem :: GLIB_001:127  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 W being Walk of G holds
( not W is trivial iff len W <> 1 ) by Lm60;

theorem Th128: :: GLIB_001:128  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 W being Walk of G st W .first() <> W .last() holds
not W is trivial by Lm60;

theorem :: GLIB_001:129  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 W being Walk of G holds
( W is trivial iff ex v being Vertex of G st W = G .walkOf v ) by Lm61;

theorem :: GLIB_001:130  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 W being Walk of G holds
( W is trivial iff W .reverse() is trivial )
proof end;

theorem :: GLIB_001:131  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 W2, W1 being Walk of G st W2 is trivial holds
W1 .append W2 = W1
proof end;

theorem :: GLIB_001:132  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 W being Walk of G
for m, n being odd Nat st m <= n & n <= len W holds
( W .cut m,n is trivial iff m = n )
proof end;

theorem Th133: :: GLIB_001:133  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 W being Walk of G
for e, x being set st e Joins W .last() ,x,G holds
not W .addEdge e is trivial
proof end;

theorem Th134: :: GLIB_001:134  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 W being Walk of G st not W is trivial holds
ex lenW2 being odd Nat st
( lenW2 = (len W) - 2 & (W .cut 1,lenW2) .addEdge (W . (lenW2 + 1)) = W )
proof end;

theorem Th135: :: GLIB_001:135  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 W2, W1 being Walk of G st not W2 is trivial & W2 .edges() c= W1 .edges() holds
W2 .vertices() c= W1 .vertices()
proof end;

theorem :: GLIB_001:136  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 W being Walk of G st not W is trivial holds
for v being Vertex of G st v in W .vertices() holds
not v is isolated
proof end;

theorem :: GLIB_001:137  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 W being Walk of G holds
( W is trivial iff W .edges() = {} )
proof end;

theorem :: GLIB_001:138  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 & W1 is trivial holds
W2 is trivial
proof end;

theorem :: GLIB_001:139  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 W being Walk of G holds
( W is Trail-like iff for m, n being even Nat st 1 <= m & m < n & n <= len W holds
W . m <> W . n ) by Lm62;

theorem :: GLIB_001:140  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 W being Walk of G st len W <= 3 holds
W is Trail-like by Lm66;

theorem :: GLIB_001:141  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 W being Walk of G holds
( W is Trail-like iff W .reverse() is Trail-like ) by Lm63;

theorem :: GLIB_001:142  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 W being Trail of G
for m, n being Nat holds W .cut m,n is Trail-like ;

theorem :: GLIB_001:143  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 W being Trail of G
for e being set st e in (W .last() ) .edgesInOut() & not e in W .edges() holds
W .addEdge e is Trail-like by Lm65;

theorem :: GLIB_001:144  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 W being Trail of G
for v being Vertex of G st v in W .vertices() & v is endvertex & not v = W .first() holds
v = W .last()
proof end;

theorem :: GLIB_001:145  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite _Graph
for W being Trail of G holds len (W .edgeSeq() ) <= G .size()
proof end;

theorem :: GLIB_001:146  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 W being Walk of G st len W <= 3 holds
W is Path-like by Lm74;

theorem :: GLIB_001:147  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 W being Walk of G st ( for m, n being odd Nat st m <= len W & n <= len W & W . m = W . n holds
m = n ) holds
W is Path-like by Lm71;

theorem :: GLIB_001:148  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 W being Path of G st not W is closed holds
for m, n being odd Nat st m < n & n <= len W holds
W . m <> W . n
proof end;

theorem :: GLIB_001:149  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 W being Walk of G holds
( W is Path-like iff W .reverse() is Path-like ) by Lm68;

theorem :: GLIB_001:150  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 W being Path of G
for m, n being Nat holds W .cut m,n is Path-like ;

theorem Th151: :: GLIB_001:151  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 W being Path of G
for e, v being set st e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or not W is closed ) & ( for n being odd Nat st 1 < n & n <= len W holds
W . n <> v ) holds
W .addEdge e is Path-like
proof end;

theorem :: GLIB_001:152  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 W being Path of G
for e, v being set st e Joins W .last() ,v,G & not v in W .vertices() & ( W is trivial or not W is closed ) holds
W .addEdge e is Path-like by Lm73;

theorem :: GLIB_001:153  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 W being Walk of G st ( for n being odd Nat st n <= len W holds
W .find (W . n) = W .rfind (W . n) ) holds
W is Path-like
proof end;

theorem :: GLIB_001:154  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 W being Walk of G st ( for n being odd Nat st n <= len W holds
W .rfind n = n ) holds
W is Path-like by Lm72;

theorem :: GLIB_001:155  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G being finite _Graph
for W being Path of G holds len (W .vertexSeq() ) <= (G .order() ) + 1
proof end;

theorem :: GLIB_001:156  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 W being vertex-distinct Walk of G
for e, v being set st e Joins W .last() ,v,G & not v in W .vertices() holds
W .addEdge e is vertex-distinct
proof end;

theorem :: GLIB_001:157  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 e, x being set st e Joins x,x,G holds
G .walkOf x,e,x is Cycle-like
proof end;

theorem :: GLIB_001:158  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 W1 being Walk of G
for e, x, y being set st e Joins x,y,G & e in W1 .edges() & W1 is Cycle-like holds
ex W2 being Walk of G st
( W2 is_Walk_from x,y & not e in W2 .edges() )
proof end;

theorem :: GLIB_001:159  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 W being Walk of G holds W is Subwalk of W by Lm75;

theorem :: GLIB_001:160  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 W1 being Walk of G
for W2 being Subwalk of W1
for W3 being Subwalk of W2 holds W3 is Subwalk of W1 by Lm76;

theorem :: GLIB_001:161  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 W1, W2 being Walk of G
for x, y being set st W1 is Subwalk of W2 holds
( W1 is_Walk_from x,y iff W2 is_Walk_from x,y )
proof end;

theorem Th162: :: GLIB_001:162  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 W1, W2 being Walk of G st W1 is Subwalk of W2 holds
( W1 .first() = W2 .first() & W1 .last() = W2 .last() )
proof end;

theorem :: GLIB_001:163  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 W1, W2 being Walk of G st W1 is Subwalk of W2 holds
len W1 <= len W2 by Lm77;

theorem Th164: :: GLIB_001:164  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 W1, W2 being Walk of G st W1 is Subwalk of W2 holds
( W1 .edges() c= W2 .edges() & W1 .vertices() c= W2 .vertices() )
proof end;

theorem Th165: :: GLIB_001:165  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 W1, W2 being Walk of G st W1 is Subwalk of W2 holds
for m being odd Nat st m <= len W1 holds
ex n being odd Nat st
( m <= n & n <= len W2 & W1 . m = W2 . n )
proof end;

theorem :: GLIB_001:166  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 W1, W2 being Walk of G st W1 is Subwalk of W2 holds
for m being even Nat st 1 <= m & m <= len W1 holds
ex n being even Nat st
( m <= n & n <= len W2 & W1 . m = W2 . n )
proof end;

theorem :: GLIB_001:167  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 W1 being Trail of G st not W1 is trivial holds
ex W2 being Path of W1 st not W2 is trivial
proof end;

theorem Th168: :: GLIB_001:168  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G2 holds W is Walk of G1
proof end;

theorem Th169: :: GLIB_001:169  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G1 st W is trivial & W .first() in the_Vertices_of G2 holds
W is Walk of G2
proof end;

theorem Th170: :: GLIB_001:170  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G1 st not W is trivial & W .edges() c= the_Edges_of G2 holds
W is Walk of G2
proof end;

theorem Th171: :: GLIB_001:171  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G1 st W .vertices() c= the_Vertices_of G2 & W .edges() c= the_Edges_of G2 holds
W is Walk of G2
proof end;

theorem :: GLIB_001:172  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being non trivial _Graph
for W being Walk of G1
for v being Vertex of G1
for G2 being removeVertex of G1,v st not v in W .vertices() holds
W is Walk of G2
proof end;

theorem :: GLIB_001:173  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for W being Walk of G1
for e being set
for G2 being removeEdge of G1,e st not e in W .edges() holds
W is Walk of G2
proof end;

theorem Th174: :: GLIB_001:174  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for G2 being Subgraph of G1
for x, y, e being set st e Joins x,y,G2 holds
G1 .walkOf x,e,y = G2 .walkOf x,e,y
proof end;

theorem :: GLIB_001:175  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for G2 being Subgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2
for e being set st W1 = W2 & e in (W2 .last() ) .edgesInOut() holds
W1 .addEdge e = W2 .addEdge e
proof end;

theorem Th176: :: GLIB_001:176  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for G2 being Subgraph of G1
for W being Walk of G2 holds
( ( W is closed implies W is closed Walk of G1 ) & ( W is directed implies W is directed Walk of G1 ) & ( W is trivial implies W is trivial Walk of G1 ) & ( W is Trail-like implies W is Trail-like Walk of G1 ) & ( W is Path-like implies W is Path-like Walk of G1 ) & ( W is vertex-distinct implies W is vertex-distinct Walk of G1 ) )
proof end;

theorem Th177: :: GLIB_001:177  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1 being _Graph
for G2 being Subgraph of G1
for W1 being Walk of G1
for W2 being Walk of G2 st W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
proof end;

theorem :: GLIB_001:178  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for x being set st G1 == G2 & x is VertexSeq of G1 holds
x is VertexSeq of G2
proof end;

theorem :: GLIB_001:179  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for x being set st G1 == G2 & x is EdgeSeq of G1 holds
x is EdgeSeq of G2
proof end;

theorem :: GLIB_001:180  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for x being set st G1 == G2 & x is Walk of G1 holds
x is Walk of G2
proof end;

theorem :: GLIB_001:181  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for x, e, y being set st G1 == G2 holds
G1 .walkOf x,e,y = G2 .walkOf x,e,y
proof end;

theorem :: GLIB_001:182  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for G1, G2 being _Graph
for W1 being Walk of G1
for W2 being Walk of G2 st G1 == G2 & W1 = W2 holds
( ( W1 is closed implies W2 is closed ) & ( W2 is closed implies W1 is closed ) & ( W1 is directed implies W2 is directed ) & ( W2 is directed implies W1 is directed ) & ( W1 is trivial implies W2 is trivial ) & ( W2 is trivial implies W1 is trivial ) & ( W1 is Trail-like implies W2 is Trail-like ) & ( W2 is Trail-like implies W1 is Trail-like ) & ( W1 is Path-like implies W2 is Path-like ) & ( W2 is Path-like implies W1 is Path-like ) & ( W1 is vertex-distinct implies W2 is vertex-distinct ) & ( W2 is vertex-distinct implies W1 is vertex-distinct ) )
proof end;