:: by Gilbert Lee

::

:: Received February 22, 2005

:: Copyright (c) 2005-2012 Association of Mizar Users

begin

theorem Th3: :: GLIB_001:3

for X being set

for fs being FinSequence of X

for fss being Subset of fs holds len (Seq fss) <= len fs

for fs being FinSequence of X

for fss being Subset of fs holds len (Seq fss) <= len fs

proof end;

theorem Th4: :: GLIB_001:4

for X being set

for fs being FinSequence of X

for fss being Subset of fs

for m being Element of NAT st m in dom (Seq fss) holds

ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n )

for fs being FinSequence of X

for fss being Subset of fs

for m being Element of NAT st m in dom (Seq fss) holds

ex n being Element of NAT st

( n in dom fs & m <= n & (Seq fss) . m = fs . n )

proof end;

theorem Th5: :: GLIB_001:5

for X being set

for fs being FinSequence of X

for fss being Subset of fs holds len (Seq fss) = card fss

for fs being FinSequence of X

for fss being Subset of fs holds len (Seq fss) = card fss

proof end;

theorem Th6: :: GLIB_001:6

for X being set

for fs being FinSequence of X

for fss being Subset of fs holds dom (Seq fss) = dom (Sgm (dom fss))

for fs being FinSequence of X

for fss being Subset of fs holds dom (Seq fss) = dom (Sgm (dom fss))

proof end;

begin

definition

let G be _Graph;

ex b_{1} being FinSequence of the_Vertices_of G st

for n being Element of NAT st 1 <= n & n < len b_{1} holds

ex e being set st e Joins b_{1} . n,b_{1} . (n + 1),G

end;
mode VertexSeq of G -> FinSequence of the_Vertices_of G means :Def1: :: GLIB_001:def 1

for n being Element of NAT st 1 <= n & n < len it holds

ex e being set st e Joins it . n,it . (n + 1),G;

existence for n being Element of NAT st 1 <= n & n < len it holds

ex e being set st e Joins it . n,it . (n + 1),G;

ex b

for n being Element of NAT st 1 <= n & n < len b

ex e being set st e Joins b

proof end;

:: deftheorem Def1 defines VertexSeq GLIB_001:def 1 :

for G being _Graph

for b_{2} being FinSequence of the_Vertices_of G holds

( b_{2} is VertexSeq of G iff for n being Element of NAT st 1 <= n & n < len b_{2} holds

ex e being set st e Joins b_{2} . n,b_{2} . (n + 1),G );

for G being _Graph

for b

( b

ex e being set st e Joins b

definition

let G be _Graph;

ex b_{1} being FinSequence of the_Edges_of G ex vs being FinSequence of the_Vertices_of G st

( len vs = (len b_{1}) + 1 & ( for n being Element of NAT st 1 <= n & n <= len b_{1} holds

b_{1} . n Joins vs . n,vs . (n + 1),G ) )

end;
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 Element of NAT st 1 <= n & n <= len it holds

it . n Joins vs . n,vs . (n + 1),G ) );

existence ex vs being FinSequence of the_Vertices_of G st

( len vs = (len it) + 1 & ( for n being Element of NAT st 1 <= n & n <= len it holds

it . n Joins vs . n,vs . (n + 1),G ) );

ex b

( len vs = (len b

b

proof end;

:: deftheorem Def2 defines EdgeSeq GLIB_001:def 2 :

for G being _Graph

for b_{2} being FinSequence of the_Edges_of G holds

( b_{2} is EdgeSeq of G iff ex vs being FinSequence of the_Vertices_of G st

( len vs = (len b_{2}) + 1 & ( for n being Element of NAT st 1 <= n & n <= len b_{2} holds

b_{2} . n Joins vs . n,vs . (n + 1),G ) ) );

for G being _Graph

for b

( b

( len vs = (len b

b

definition

let G be _Graph;

ex b_{1} being FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) st

( len b_{1} is odd & b_{1} . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len b_{1} holds

b_{1} . (n + 1) Joins b_{1} . n,b_{1} . (n + 2),G ) )

end;
mode Walk of G -> FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) means :Def3: :: GLIB_001:def 3

( len it is odd & it . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len it holds

it . (n + 1) Joins it . n,it . (n + 2),G ) );

existence ( len it is odd & it . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len it holds

it . (n + 1) Joins it . n,it . (n + 2),G ) );

ex b

( len b

b

proof end;

:: deftheorem Def3 defines Walk GLIB_001:def 3 :

for G being _Graph

for b_{2} being FinSequence of (the_Vertices_of G) \/ (the_Edges_of G) holds

( b_{2} is Walk of G iff ( len b_{2} is odd & b_{2} . 1 in the_Vertices_of G & ( for n being odd Element of NAT st n < len b_{2} holds

b_{2} . (n + 1) Joins b_{2} . n,b_{2} . (n + 2),G ) ) );

for G being _Graph

for b

( b

b

registration

let G be _Graph;

let W be Walk of G;

correctness

coherence

( not len W is even & not len W is empty );

end;
let W be Walk of G;

correctness

coherence

( not len W is even & not len W is empty );

proof end;

:: deftheorem defines .walkOf GLIB_001:def 4 :

for G being _Graph

for v being Vertex of G holds G .walkOf v = <*v*>;

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 ;

( ( 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 ) )

for b_{1} being Walk of G holds verum
;

end;
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 <*x,e,y*> if e Joins x,y,G

otherwise G .walkOf (choose (the_Vertices_of G));

( ( 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 b

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

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;

coherence

W . 1 is Vertex of G by Def3;

coherence

W . (len W) is Vertex of G

end;
let W be Walk of G;

coherence

W . 1 is Vertex of G by Def3;

coherence

W . (len W) is Vertex of G

proof end;

:: deftheorem defines .first() GLIB_001:def 6 :

for G being _Graph

for W being Walk of G holds W .first() = W . 1;

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

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;

coherence

( ( n is odd & n <= len W implies W . n is Vertex of G ) & ( ( not n is odd or not n <= len W ) implies W .first() is Vertex of G ) );

consistency

for b_{1} being Vertex of G holds verum;

end;
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 ( n is odd & n <= len W )

otherwise W .first() ;

correctness W . n if ( n is odd & n <= len W )

otherwise W .first() ;

coherence

( ( n is odd & n <= len W implies W . n is Vertex of G ) & ( ( not n is odd or not n <= len W ) implies W .first() is Vertex of G ) );

consistency

for b

proof end;

:: deftheorem Def8 defines .vertexAt GLIB_001:def 8 :

for G being _Graph

for W being Walk of G

for n being Nat holds

( ( n is odd & n <= len W implies W .vertexAt n = W . n ) & ( ( not n is odd or not n <= len W ) implies W .vertexAt n = W .first() ) );

for G being _Graph

for W being Walk of G

for n being Nat holds

( ( n is odd & n <= len W implies W .vertexAt n = W . n ) & ( ( not n is odd or not n <= len W ) implies W .vertexAt n = W .first() ) );

definition

let G be _Graph;

let W be Walk of G;

coherence

Rev W is Walk of G

for b_{1}, b_{2} being Walk of G st b_{1} = Rev b_{2} holds

b_{2} = Rev b_{1}
;

end;
let W be Walk of G;

coherence

Rev W is Walk of G

proof end;

involutiveness for b

b

:: deftheorem defines .reverse() GLIB_001:def 9 :

for G being _Graph

for W being Walk of G holds W .reverse() = Rev W;

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;

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 b_{1} being Walk of G holds verum;

end;
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 W1 ^' W2 if W1 .last() = W2 .first()

otherwise W1;

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 b

proof 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 ) );

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;

coherence

( ( m is odd & n is odd & m <= n & n <= len W implies (m,n) -cut W is Walk of G ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W ) implies W is Walk of G ) );

consistency

for b_{1} being Walk of G holds verum;

end;
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 ( m is odd & n is odd & m <= n & n <= len W )

otherwise W;

correctness (m,n) -cut W if ( m is odd & n is odd & m <= n & n <= len W )

otherwise W;

coherence

( ( m is odd & n is odd & m <= n & n <= len W implies (m,n) -cut W is Walk of G ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W ) implies W is Walk of G ) );

consistency

for b

proof 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

( ( m is odd & n is odd & m <= n & n <= len W implies W .cut (m,n) = (m,n) -cut W ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W ) implies W .cut (m,n) = W ) );

for G being _Graph

for W being Walk of G

for m, n being Nat holds

( ( m is odd & n is odd & m <= n & n <= len W implies W .cut (m,n) = (m,n) -cut W ) & ( ( not m is odd or not n is odd 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 Element of NAT ;

coherence

( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n implies (W .cut (1,m)) .append (W .cut (n,(len W))) is Walk of G ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) implies W is Walk of G ) );

consistency

for b_{1} being Walk of G holds verum;

;

end;
let W be Walk of G;

let m, n be Element of 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 ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n )

otherwise W;

correctness (W .cut (1,m)) .append (W .cut (n,(len W))) if ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n )

otherwise W;

coherence

( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n implies (W .cut (1,m)) .append (W .cut (n,(len W))) is Walk of G ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) implies W is Walk of G ) );

consistency

for b

;

:: deftheorem Def12 defines .remove GLIB_001:def 12 :

for G being _Graph

for W being Walk of G

for m, n being Element of NAT holds

( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n implies W .remove (m,n) = (W .cut (1,m)) .append (W .cut (n,(len W))) ) & ( ( not m is odd or not n is odd or not m <= n or not n <= len W or not W . m = W . n ) implies W .remove (m,n) = W ) );

for G being _Graph

for W being Walk of G

for m, n being Element of NAT holds

( ( m is odd & n is odd & m <= n & n <= len W & W . m = W . n implies W .remove (m,n) = (W .cut (1,m)) .append (W .cut (n,(len W))) ) & ( ( not m is odd or not n is odd 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 ;

W .append (G .walkOf ((W .last()),e,((W .last()) .adj e))) is Walk of G ;

end;
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)));

W .append (G .walkOf ((W .last()),e,((W .last()) .adj e))) is Walk of G ;

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

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;

ex b_{1} being VertexSeq of G st

( (len W) + 1 = 2 * (len b_{1}) & ( for n being Nat st 1 <= n & n <= len b_{1} holds

b_{1} . n = W . ((2 * n) - 1) ) )

for b_{1}, b_{2} being VertexSeq of G st (len W) + 1 = 2 * (len b_{1}) & ( for n being Nat st 1 <= n & n <= len b_{1} holds

b_{1} . n = W . ((2 * n) - 1) ) & (len W) + 1 = 2 * (len b_{2}) & ( for n being Nat st 1 <= n & n <= len b_{2} holds

b_{2} . n = W . ((2 * n) - 1) ) holds

b_{1} = b_{2}

end;
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 ( (len W) + 1 = 2 * (len it) & ( for n being Nat st 1 <= n & n <= len it holds

it . n = W . ((2 * n) - 1) ) );

ex b

( (len W) + 1 = 2 * (len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def14 defines .vertexSeq() GLIB_001:def 14 :

for G being _Graph

for W being Walk of G

for b_{3} being VertexSeq of G holds

( b_{3} = W .vertexSeq() iff ( (len W) + 1 = 2 * (len b_{3}) & ( for n being Nat st 1 <= n & n <= len b_{3} holds

b_{3} . n = W . ((2 * n) - 1) ) ) );

for G being _Graph

for W being Walk of G

for b

( b

b

definition

let G be _Graph;

let W be Walk of G;

ex b_{1} being EdgeSeq of G st

( len W = (2 * (len b_{1})) + 1 & ( for n being Nat st 1 <= n & n <= len b_{1} holds

b_{1} . n = W . (2 * n) ) )

for b_{1}, b_{2} being EdgeSeq of G st len W = (2 * (len b_{1})) + 1 & ( for n being Nat st 1 <= n & n <= len b_{1} holds

b_{1} . n = W . (2 * n) ) & len W = (2 * (len b_{2})) + 1 & ( for n being Nat st 1 <= n & n <= len b_{2} holds

b_{2} . n = W . (2 * n) ) holds

b_{1} = b_{2}

end;
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 ( len W = (2 * (len it)) + 1 & ( for n being Nat st 1 <= n & n <= len it holds

it . n = W . (2 * n) ) );

ex b

( len W = (2 * (len b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def15 defines .edgeSeq() GLIB_001:def 15 :

for G being _Graph

for W being Walk of G

for b_{3} being EdgeSeq of G holds

( b_{3} = W .edgeSeq() iff ( len W = (2 * (len b_{3})) + 1 & ( for n being Nat st 1 <= n & n <= len b_{3} holds

b_{3} . n = W . (2 * n) ) ) );

for G being _Graph

for W being Walk of G

for b

( b

b

definition

let G be _Graph;

let W be Walk of G;

rng (W .vertexSeq()) is finite Subset of (the_Vertices_of G) ;

end;
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());

rng (W .vertexSeq()) is finite Subset of (the_Vertices_of G) ;

:: deftheorem defines .vertices() GLIB_001:def 16 :

for G being _Graph

for W being Walk of G holds W .vertices() = rng (W .vertexSeq());

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;

coherence

rng (W .edgeSeq()) is finite Subset of (the_Edges_of G) ;

end;
let W be Walk of G;

coherence

rng (W .edgeSeq()) is finite Subset of (the_Edges_of G) ;

:: deftheorem defines .edges() GLIB_001:def 17 :

for G being _Graph

for W being Walk of G holds W .edges() = rng (W .edgeSeq());

for G being _Graph

for W being Walk of G holds W .edges() = rng (W .edgeSeq());

definition
end;

:: deftheorem defines .length() GLIB_001:def 18 :

for G being _Graph

for W being Walk of G holds W .length() = len (W .edgeSeq());

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 ;

( ( v in W .vertices() implies ex b_{1} being odd Element of NAT st

( b_{1} <= len W & W . b_{1} = v & ( for n being odd Nat st n <= len W & W . n = v holds

b_{1} <= n ) ) ) & ( not v in W .vertices() implies ex b_{1} being odd Element of NAT st b_{1} = len W ) )

for b_{1}, b_{2} being odd Element of NAT holds

( ( v in W .vertices() & b_{1} <= len W & W . b_{1} = v & ( for n being odd Nat st n <= len W & W . n = v holds

b_{1} <= n ) & b_{2} <= len W & W . b_{2} = v & ( for n being odd Nat st n <= len W & W . n = v holds

b_{2} <= n ) implies b_{1} = b_{2} ) & ( not v in W .vertices() & b_{1} = len W & b_{2} = len W implies b_{1} = b_{2} ) )

for b_{1} being odd Element of NAT holds verum
;

end;
let W be Walk of G;

let v be set ;

func W .find v -> odd Element of 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 ( 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;

( ( v in W .vertices() implies ex b

( b

b

proof end;

uniqueness for b

( ( v in W .vertices() & b

b

b

proof end;

consistency for b

:: deftheorem Def19 defines .find GLIB_001:def 19 :

for G being _Graph

for W being Walk of G

for v being set

for b_{4} being odd Element of NAT holds

( ( v in W .vertices() implies ( b_{4} = W .find v iff ( b_{4} <= len W & W . b_{4} = v & ( for n being odd Nat st n <= len W & W . n = v holds

b_{4} <= n ) ) ) ) & ( not v in W .vertices() implies ( b_{4} = W .find v iff b_{4} = len W ) ) );

for G being _Graph

for W being Walk of G

for v being set

for b

( ( v in W .vertices() implies ( b

b

definition

let G be _Graph;

let W be Walk of G;

let n be Element of NAT ;

( ( n is odd & n <= len W implies ex b_{1} being odd Element of NAT st

( b_{1} <= len W & W . b_{1} = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

b_{1} <= k ) ) ) & ( ( not n is odd or not n <= len W ) implies ex b_{1} being odd Element of NAT st b_{1} = len W ) )

for b_{1}, b_{2} being odd Element of NAT holds

( ( n is odd & n <= len W & b_{1} <= len W & W . b_{1} = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

b_{1} <= k ) & b_{2} <= len W & W . b_{2} = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

b_{2} <= k ) implies b_{1} = b_{2} ) & ( ( not n is odd or not n <= len W ) & b_{1} = len W & b_{2} = len W implies b_{1} = b_{2} ) )

for b_{1} being odd Element of NAT holds verum
;

end;
let W be Walk of G;

let n be Element of NAT ;

func W .find n -> odd Element of 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 ( n is odd & n <= len W )

otherwise it = len W;

existence ( it <= len W & W . it = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

it <= k ) ) if ( n is odd & n <= len W )

otherwise it = len W;

( ( n is odd & n <= len W implies ex b

( b

b

proof end;

uniqueness for b

( ( n is odd & n <= len W & b

b

b

proof end;

consistency for b

:: deftheorem Def20 defines .find GLIB_001:def 20 :

for G being _Graph

for W being Walk of G

for n being Element of NAT

for b_{4} being odd Element of NAT holds

( ( n is odd & n <= len W implies ( b_{4} = W .find n iff ( b_{4} <= len W & W . b_{4} = W . n & ( for k being odd Nat st k <= len W & W . k = W . n holds

b_{4} <= k ) ) ) ) & ( ( not n is odd or not n <= len W ) implies ( b_{4} = W .find n iff b_{4} = len W ) ) );

for G being _Graph

for W being Walk of G

for n being Element of NAT

for b

( ( n is odd & n <= len W implies ( b

b

definition

let G be _Graph;

let W be Walk of G;

let v be set ;

( ( v in W .vertices() implies ex b_{1} being odd Element of NAT st

( b_{1} <= len W & W . b_{1} = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds

n <= b_{1} ) ) ) & ( not v in W .vertices() implies ex b_{1} being odd Element of NAT st b_{1} = len W ) )

for b_{1}, b_{2} being odd Element of NAT holds

( ( v in W .vertices() & b_{1} <= len W & W . b_{1} = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds

n <= b_{1} ) & b_{2} <= len W & W . b_{2} = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds

n <= b_{2} ) implies b_{1} = b_{2} ) & ( not v in W .vertices() & b_{1} = len W & b_{2} = len W implies b_{1} = b_{2} ) )

for b_{1} being odd Element of NAT holds verum
;

end;
let W be Walk of G;

let v be set ;

func W .rfind v -> odd Element of NAT means :Def21: :: GLIB_001:def 21

( it <= len W & W . it = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds

n <= it ) ) if v in W .vertices()

otherwise it = len W;

existence ( it <= len W & W . it = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds

n <= it ) ) if v in W .vertices()

otherwise it = len W;

( ( v in W .vertices() implies ex b

( b

n <= b

proof end;

uniqueness for b

( ( v in W .vertices() & b

n <= b

n <= b

proof end;

consistency for b

:: deftheorem Def21 defines .rfind GLIB_001:def 21 :

for G being _Graph

for W being Walk of G

for v being set

for b_{4} being odd Element of NAT holds

( ( v in W .vertices() implies ( b_{4} = W .rfind v iff ( b_{4} <= len W & W . b_{4} = v & ( for n being odd Element of NAT st n <= len W & W . n = v holds

n <= b_{4} ) ) ) ) & ( not v in W .vertices() implies ( b_{4} = W .rfind v iff b_{4} = len W ) ) );

for G being _Graph

for W being Walk of G

for v being set

for b

( ( v in W .vertices() implies ( b

n <= b

definition

let G be _Graph;

let W be Walk of G;

let n be Element of NAT ;

( ( n is odd & n <= len W implies ex b_{1} being odd Element of NAT st

( b_{1} <= len W & W . b_{1} = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= b_{1} ) ) ) & ( ( not n is odd or not n <= len W ) implies ex b_{1} being odd Element of NAT st b_{1} = len W ) )

for b_{1}, b_{2} being odd Element of NAT holds

( ( n is odd & n <= len W & b_{1} <= len W & W . b_{1} = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= b_{1} ) & b_{2} <= len W & W . b_{2} = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= b_{2} ) implies b_{1} = b_{2} ) & ( ( not n is odd or not n <= len W ) & b_{1} = len W & b_{2} = len W implies b_{1} = b_{2} ) )

for b_{1} being odd Element of NAT holds verum
;

end;
let W be Walk of G;

let n be Element of NAT ;

func W .rfind n -> odd Element of NAT means :Def22: :: GLIB_001:def 22

( it <= len W & W . it = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= it ) ) if ( n is odd & n <= len W )

otherwise it = len W;

existence ( it <= len W & W . it = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= it ) ) if ( n is odd & n <= len W )

otherwise it = len W;

( ( n is odd & n <= len W implies ex b

( b

k <= b

proof end;

uniqueness for b

( ( n is odd & n <= len W & b

k <= b

k <= b

proof end;

consistency for b

:: deftheorem Def22 defines .rfind GLIB_001:def 22 :

for G being _Graph

for W being Walk of G

for n being Element of NAT

for b_{4} being odd Element of NAT holds

( ( n is odd & n <= len W implies ( b_{4} = W .rfind n iff ( b_{4} <= len W & W . b_{4} = W . n & ( for k being odd Element of NAT st k <= len W & W . k = W . n holds

k <= b_{4} ) ) ) ) & ( ( not n is odd or not n <= len W ) implies ( b_{4} = W .rfind n iff b_{4} = len W ) ) );

for G being _Graph

for W being Walk of G

for n being Element of NAT

for b

( ( n is odd & n <= len W implies ( b

k <= b

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

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;

end;
let W be Walk of G;

attr W is directed means :Def25: :: GLIB_001:def 25

for n being odd Element of NAT st n < len W holds

(the_Source_of G) . (W . (n + 1)) = W . n;

for n being odd Element of NAT st n < len W holds

(the_Source_of G) . (W . (n + 1)) = W . n;

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

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 Element of NAT st n < len W holds

(the_Source_of G) . (W . (n + 1)) = W . n );

for G being _Graph

for W being Walk of G holds

( W is directed iff for n being odd Element of 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 );

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

for G being _Graph

for W being Walk of G holds

( W is Trail-like iff W .edgeSeq() is one-to-one );

:: 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 Element of NAT st m < n & n <= len W & W . m = W . n holds

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

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 Element of NAT st m < n & n <= len W & W . m = W . n holds

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

:: 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 Element of NAT st m <= len W & n <= len W & W . m = W . n holds

m = n );

for G being _Graph

for W being Walk of G holds

( W is vertex-distinct iff for m, n being odd Element of 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;

end;
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 );

( 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 );

( W is closed & W is Path-like & not W is trivial );

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

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

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

Lm1: for G being _Graph

for W being Walk of G

for n being odd Element of NAT st n <= len W holds

W . n in the_Vertices_of G

proof end;

Lm2: for G being _Graph

for W being Walk of G

for n being even Element of NAT st n in dom W holds

ex naa1 being odd Element of 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;

Lm3: for G being _Graph

for W being Walk of G

for n being odd Element of NAT st n < len W holds

( n in dom W & n + 1 in dom W & n + 2 in dom W )

proof end;

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

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

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

Lm7: for G being _Graph

for W being Walk of G holds

( W .first() = (W .reverse()) .last() & W .last() = (W .reverse()) .first() )

proof end;

Lm8: for G being _Graph

for W being Walk of G

for n being Element of 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;

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

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

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

Lm12: for G being _Graph

for W1, W2 being Walk of G

for n being Element of NAT st n in dom W1 holds

( (W1 .append W2) . n = W1 . n & n in dom (W1 .append W2) )

proof end;

Lm13: for G being _Graph

for W1, W2 being Walk of G st W1 .last() = W2 .first() holds

for n being Element of 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;

Lm14: for G being _Graph

for W1, W2 being Walk of G

for n being Element of NAT holds

( not n in dom (W1 .append W2) or n in dom W1 or ex k being Element of NAT st

( k < len W2 & n = (len W1) + k ) )

proof end;

Lm15: for G being _Graph

for W being Walk of G

for m, n being odd Element of NAT st m <= n & n <= len W holds

( (len (W .cut (m,n))) + m = n + 1 & ( for i being Element of 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;

Lm16: for G being _Graph

for W being Walk of G

for m, n being odd Element of 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;

Lm17: for G being _Graph

for W being Walk of G

for m, n, o being odd Element of 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;

Lm18: for G being _Graph

for W being Walk of G holds W .cut (1,(len W)) = W

proof end;

Lm19: for G being _Graph

for W being Walk of G

for n being odd Element of NAT st n <= len W holds

W .cut (n,n) = <*(W .vertexAt n)*>

proof end;

Lm20: for G being _Graph

for W being Walk of G

for m, n being Element of NAT st m is odd & m <= n holds

(W .cut (1,n)) .cut (1,m) = W .cut (1,m)

proof end;

Lm21: for G being _Graph

for W1, W2 being Walk of G

for m, n being odd Element of NAT st m <= n & n <= len W1 & W1 .last() = W2 .first() holds

(W1 .append W2) .cut (m,n) = W1 .cut (m,n)

proof end;

Lm22: for G being _Graph

for W being Walk of G

for m being odd Element of NAT st m <= len W holds

len (W .cut (1,m)) = m

proof end;

Lm23: for G being _Graph

for W being Walk of G

for m being odd Element of NAT

for x being Element of NAT st x in dom (W .cut (1,m)) & m <= len W holds

(W .cut (1,m)) . x = W . x

proof end;

Lm24: for G being _Graph

for W being Walk of G

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

(len (W .remove (m,n))) + n = (len W) + m

proof end;

Lm25: for G being _Graph

for W being Walk of G

for m, n being Element of 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;

Lm26: for G being _Graph

for W being Walk of G

for m, n being Element of NAT holds len (W .remove (m,n)) <= len W

proof end;

Lm27: for G being _Graph

for W being Walk of G

for m being Element of NAT holds W .remove (m,m) = W

proof end;

Lm28: for G being _Graph

for W being Walk of G

for m, n being odd Element of 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;

Lm29: for G being _Graph

for W being Walk of G

for x, y being set

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st x in Seg m holds

(W .remove (m,n)) . x = W . x

proof end;

Lm30: for G being _Graph

for W being Walk of G

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds

( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W )

proof end;

Lm31: for G being _Graph

for W being Walk of G

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

len (W .remove (m,n)) = ((len W) + m) - n

proof end;

Lm32: for G being _Graph

for W being Walk of G

for m being Element of NAT st W .first() = W . m holds

W .remove (1,m) = W .cut (m,(len W))

proof end;

Lm33: for G being _Graph

for W being Walk of G

for m, n being Element of NAT holds

( (W .remove (m,n)) .first() = W .first() & (W .remove (m,n)) .last() = W .last() )

proof end;

Lm34: for G being _Graph

for W being Walk of G

for m, n being odd Element of NAT

for x being Element of NAT holds

( not x in dom (W .remove (m,n)) or x in Seg m or ( m <= x & x <= len (W .remove (m,n)) ) )

proof end;

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

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

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

Lm38: 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 Element of NAT st n in dom W holds

(W .addEdge e) . n = W . n ) )

proof end;

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

Lm40: for G being _Graph

for W being Walk of G

for n being even Element of NAT st 1 <= n & n <= len W holds

( n div 2 in dom (W .edgeSeq()) & W . n = (W .edgeSeq()) . (n div 2) )

proof end;

Lm41: for G being _Graph

for W being Walk of G

for n being Element of NAT holds

( n in dom (W .edgeSeq()) iff 2 * n in dom W )

proof end;

Lm42: for G being _Graph

for W being Walk of G ex lenWaa1 being even Element of NAT st

( lenWaa1 = (len W) - 1 & len (W .edgeSeq()) = lenWaa1 div 2 )

proof end;

Lm43: for G being _Graph

for W being Walk of G

for n being Element of NAT holds (W .cut (1,n)) .edgeSeq() c= W .edgeSeq()

proof end;

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

Lm45: for G being _Graph

for W being Walk of G

for x being set holds

( x in W .vertices() iff ex n being odd Element of NAT st

( n <= len W & W . n = x ) )

proof end;

Lm46: for G being _Graph

for W being Walk of G

for e being set holds

( e in W .edges() iff ex n being even Element of NAT st

( 1 <= n & n <= len W & W . n = e ) )

proof end;

Lm47: 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 Element of NAT st

( n + 2 <= len W & v1 = W . n & e = W . (n + 1) & v2 = W . (n + 2) & e Joins v1,v2,G )

proof end;

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

Lm49: for G being _Graph

for W being Walk of G

for n being odd Element of NAT st n <= len W holds

W .find n <= n

proof end;

Lm50: for G being _Graph

for W being Walk of G

for n being odd Element of NAT st n <= len W holds

W .rfind n >= n

proof end;

Lm51: for G being _Graph

for W being Walk of G holds

( W is directed iff for n being odd Element of NAT st n < len W holds

W . (n + 1) DJoins W . n,W . (n + 2),G )

proof end;

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

Lm53: for G being _Graph

for W being Walk of G

for m, n being Element of NAT st W is directed holds

W .cut (m,n) is directed

proof end;

Lm54: for G being _Graph

for W being Walk of G holds

( not W is trivial iff 3 <= len W )

proof end;

Lm55: for G being _Graph

for W being Walk of G holds

( not W is trivial iff len W <> 1 )

proof end;

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

Lm57: for G being _Graph

for W being Walk of G holds

( W is Trail-like iff for m, n being even Element of NAT st 1 <= m & m < n & n <= len W holds

W . m <> W . n )

proof end;

Lm58: for G being _Graph

for W being Walk of G holds

( W is Trail-like iff W .reverse() is Trail-like )

proof end;

Lm59: for G being _Graph

for W being Walk of G

for m, n being Element of NAT st W is Trail-like holds

W .cut (m,n) is Trail-like

proof end;

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

Lm61: for G being _Graph

for W being Walk of G st len W <= 3 holds

W is Trail-like

proof end;

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

Lm63: for G being _Graph

for W being Walk of G holds

( W is Path-like iff W .reverse() is Path-like )

proof end;

Lm64: for G being _Graph

for W being Walk of G

for m, n being Element of NAT st W is Path-like holds

W .cut (m,n) is Path-like

proof end;

Lm65: 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 W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds

W . n <> v ) holds

W .addEdge e is Path-like

proof end;

Lm66: for G being _Graph

for W being Walk of G st ( for m, n being odd Element of NAT st m <= len W & n <= len W & W . m = W . n holds

m = n ) holds

W is Path-like

proof end;

Lm67: for G being _Graph

for W being Walk of G st ( for n being odd Element of NAT st n <= len W holds

W .rfind n = n ) holds

W is Path-like

proof end;

Lm68: 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 W is open ) holds

W .addEdge e is Path-like

proof end;

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

correctness

coherence

for b_{1} being Walk of G st b_{1} is Path-like holds

b_{1} is Trail-like ;

by Def28;

correctness

coherence

for b_{1} being Walk of G st b_{1} is trivial holds

b_{1} is Path-like ;

for b_{1} being Walk of G st b_{1} is trivial holds

b_{1} is vertex-distinct

for b_{1} being Walk of G st b_{1} is vertex-distinct holds

b_{1} is Path-like

coherence

for b_{1} being Walk of G st b_{1} is Circuit-like holds

( b_{1} is closed & b_{1} is Trail-like & not b_{1} is trivial );

by Def30;

correctness

coherence

for b_{1} being Walk of G st b_{1} is Cycle-like holds

( b_{1} is closed & b_{1} is Path-like & not b_{1} is trivial );

by Def31;

end;
correctness

coherence

for b

b

by Def28;

correctness

coherence

for b

b

proof end;

coherence for b

b

proof end;

coherence for b

b

proof end;

correctness coherence

for b

( b

by Def30;

correctness

coherence

for b

( b

by Def31;

registration

let G be _Graph;

ex b_{1} being Walk of G st

( b_{1} is closed & b_{1} is directed & b_{1} is trivial )

end;
cluster Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like closed directed trivial for Walk of G;

existence ex b

( b

proof end;

registration

let G be _Graph;

ex b_{1} being Walk of G st b_{1} is vertex-distinct

end;
cluster Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like vertex-distinct for Walk of G;

existence ex b

proof end;

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

registration

let G be _Graph;

let v be Vertex of G;

coherence

( G .walkOf v is closed & G .walkOf v is directed & G .walkOf v is trivial ) by Lm4;

end;
let v be Vertex of G;

coherence

( G .walkOf v is closed & G .walkOf v is directed & G .walkOf v is trivial ) by Lm4;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration
end;

registration

let G be _Graph;

let W be DWalk of G;

let m, n be Element of NAT ;

coherence

W .cut (m,n) is directed by Lm53;

end;
let W be DWalk of G;

let m, n be Element of NAT ;

coherence

W .cut (m,n) is directed by Lm53;

registration

let G be _Graph;

let W be trivial Walk of G;

let m, n be Element of NAT ;

coherence

W .cut (m,n) is trivial

end;
let W be trivial Walk of G;

let m, n be Element of NAT ;

coherence

W .cut (m,n) is trivial

proof end;

registration

let G be _Graph;

let W be Trail of G;

let m, n be Element of NAT ;

coherence

W .cut (m,n) is Trail-like by Lm59;

end;
let W be Trail of G;

let m, n be Element of NAT ;

coherence

W .cut (m,n) is Trail-like by Lm59;

registration

let G be _Graph;

let W be Path of G;

let m, n be Element of NAT ;

coherence

W .cut (m,n) is Path-like by Lm64;

end;
let W be Path of G;

let m, n be Element of NAT ;

coherence

W .cut (m,n) is Path-like by Lm64;

registration

let G be _Graph;

let W be vertex-distinct Walk of G;

let m, n be Element of NAT ;

coherence

W .cut (m,n) is vertex-distinct

end;
let W be vertex-distinct Walk of G;

let m, n be Element of NAT ;

coherence

W .cut (m,n) is vertex-distinct

proof end;

registration

let G be _Graph;

let W be closed Walk of G;

let m, n be Element of NAT ;

coherence

W .remove (m,n) is closed

end;
let W be closed Walk of G;

let m, n be Element of NAT ;

coherence

W .remove (m,n) is closed

proof end;

registration

let G be _Graph;

let W be DWalk of G;

let m, n be Element of NAT ;

coherence

W .remove (m,n) is directed

end;
let W be DWalk of G;

let m, n be Element of NAT ;

coherence

W .remove (m,n) is directed

proof end;

registration

let G be _Graph;

let W be trivial Walk of G;

let m, n be Element of NAT ;

coherence

W .remove (m,n) is trivial

end;
let W be trivial Walk of G;

let m, n be Element of NAT ;

coherence

W .remove (m,n) is trivial

proof end;

registration

let G be _Graph;

let W be Trail of G;

let m, n be Element of NAT ;

coherence

W .remove (m,n) is Trail-like

end;
let W be Trail of G;

let m, n be Element of NAT ;

coherence

W .remove (m,n) is Trail-like

proof end;

registration

let G be _Graph;

let W be Path of G;

let m, n be Element of NAT ;

coherence

W .remove (m,n) is Path-like

end;
let W be Path of G;

let m, n be Element of NAT ;

coherence

W .remove (m,n) is Path-like

proof end;

definition

let G be _Graph;

let W be Walk of G;

ex b_{1} being Walk of G st

( b_{1} is_Walk_from W .first() ,W .last() & ex es being Subset of (W .edgeSeq()) st b_{1} .edgeSeq() = Seq es )

end;
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 Subset of (W .edgeSeq()) st it .edgeSeq() = Seq es );

existence ( it is_Walk_from W .first() ,W .last() & ex es being Subset of (W .edgeSeq()) st it .edgeSeq() = Seq es );

ex b

( b

proof end;

:: deftheorem Def32 defines Subwalk GLIB_001:def 32 :

for G being _Graph

for W, b_{3} being Walk of G holds

( b_{3} is Subwalk of W iff ( b_{3} is_Walk_from W .first() ,W .last() & ex es being Subset of (W .edgeSeq()) st b_{3} .edgeSeq() = Seq es ) );

for G being _Graph

for W, b

( b

Lm70: for G being _Graph

for W being Walk of G holds W is Subwalk of W

proof end;

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

Lm72: 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 Element of NAT ;

:: original: .remove

redefine func W .remove (m,n) -> Subwalk of W;

coherence

W .remove (m,n) is Subwalk of W

end;
let W be Walk of G;

let m, n be Element of NAT ;

:: original: .remove

redefine func W .remove (m,n) -> Subwalk of W;

coherence

W .remove (m,n) is Subwalk of W

proof end;

registration

let G be _Graph;

let W be Walk of G;

ex b_{1} being Subwalk of W st

( b_{1} is Trail-like & b_{1} is Path-like )

end;
let W be Walk of G;

cluster Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Trail-like Path-like for Subwalk of W;

existence ex b

( b

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

registration

let G be _Graph;

let W be DWalk of G;

ex b_{1} being Path of W st b_{1} is directed

end;
let W be DWalk of G;

cluster Relation-like NAT -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like directed Trail-like Path-like for Subwalk of W;

existence ex b

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

definition

let G be _Graph;

{ W where W is Walk of G : verum } is non empty Subset of (((the_Vertices_of G) \/ (the_Edges_of G)) *)

end;
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 } ;

{ W where W is Walk of G : verum } is non empty Subset of (((the_Vertices_of G) \/ (the_Edges_of G)) *)

proof end;

:: deftheorem defines .allWalks() GLIB_001:def 33 :

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

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

definition

let G be _Graph;

{ W where W is Trail of G : verum } is non empty Subset of (G .allWalks())

end;
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 } ;

{ W where W is Trail of G : verum } is non empty Subset of (G .allWalks())

proof end;

:: deftheorem defines .allTrails() GLIB_001:def 34 :

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

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

definition

let G be _Graph;

{ W where W is Path of G : verum } is non empty Subset of (G .allTrails())

end;
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 } ;

{ W where W is Path of G : verum } is non empty Subset of (G .allTrails())

proof end;

:: deftheorem defines .allPaths() GLIB_001:def 35 :

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

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

definition

let G be _Graph;

{ W where W is DWalk of G : verum } is non empty Subset of (G .allWalks())

end;
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 } ;

{ W where W is DWalk of G : verum } is non empty Subset of (G .allWalks())

proof end;

:: deftheorem defines .allDWalks() GLIB_001:def 36 :

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

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

definition

let G be _Graph;

{ W where W is DTrail of G : verum } is non empty Subset of (G .allTrails())

end;
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 } ;

{ W where W is DTrail of G : verum } is non empty Subset of (G .allTrails())

proof end;

:: deftheorem defines .allDTrails() GLIB_001:def 37 :

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

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

definition

let G be _Graph;

{ W where W is directed Path of G : verum } is non empty Subset of (G .allDTrails())

end;
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 } ;

{ W where W is directed Path of G : verum } is non empty Subset of (G .allDTrails())

proof end;

:: deftheorem defines .allDPaths() GLIB_001:def 38 :

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

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

registration
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 b_{1} being Element of X holds b_{1} is Walk of G

end;
let X be non empty Subset of (G .allWalks());

:: original: Element

redefine mode Element of X -> Walk of G;

coherence

for b

proof 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 b_{1} being Element of X holds b_{1} is Trail of G

end;
let X be non empty Subset of (G .allTrails());

:: original: Element

redefine mode Element of X -> Trail of G;

coherence

for b

proof 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 b_{1} being Element of X holds b_{1} is Path of G

end;
let X be non empty Subset of (G .allPaths());

:: original: Element

redefine mode Element of X -> Path of G;

coherence

for b

proof 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 b_{1} being Element of X holds b_{1} is DWalk of G

end;
let X be non empty Subset of (G .allDWalks());

:: original: Element

redefine mode Element of X -> DWalk of G;

coherence

for b

proof 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 b_{1} being Element of X holds b_{1} is DTrail of G

end;
let X be non empty Subset of (G .allDTrails());

:: original: Element

redefine mode Element of X -> DTrail of G;

coherence

for b

proof 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 b_{1} being Element of X holds b_{1} is DPath of G

end;
let X be non empty Subset of (G .allDPaths());

:: original: Element

redefine mode Element of X -> DPath of G;

coherence

for b

proof end;

begin

theorem :: GLIB_001:7

theorem Th8: :: GLIB_001:8

for G being _Graph

for W being Walk of G

for n being even Element of NAT st n in dom W holds

W . n in the_Edges_of G

for W being Walk of G

for n being even Element of NAT st n in dom W holds

W . n in the_Edges_of G

proof end;

theorem :: GLIB_001:9

theorem Th10: :: GLIB_001:10

for G being _Graph

for W being Walk of G

for n being odd Element of NAT st n < len W holds

W . (n + 1) in (W .vertexAt n) .edgesInOut()

for W being Walk of G

for n being odd Element of NAT st n < len W holds

W . (n + 1) in (W .vertexAt n) .edgesInOut()

proof end;

theorem Th11: :: GLIB_001:11

for G being _Graph

for W being Walk of G

for n being odd Element of NAT st 1 < n & n <= len W holds

W . (n - 1) in (W .vertexAt n) .edgesInOut()

for W being Walk of G

for n being odd Element of NAT st 1 < n & n <= len W holds

W . (n - 1) in (W .vertexAt n) .edgesInOut()

proof end;

theorem :: GLIB_001:12

for G being _Graph

for W being Walk of G

for n being odd Element of NAT st n < len W holds

( n in dom W & n + 1 in dom W & n + 2 in dom W )

for W being Walk of G

for n being odd Element of NAT st n < len W holds

( n in dom W & n + 1 in dom W & n + 2 in dom W )

proof end;

theorem Th13: :: GLIB_001:13

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 )

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

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 )

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

theorem Th17: :: GLIB_001:17

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 ) )

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

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 )

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

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 )

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

for G1, G2 being _Graph

for W1 being Walk of G1

for W2 being Walk of G2 st W1 = W2 holds

for n being Element of NAT holds W1 .vertexAt n = W2 .vertexAt n

for W1 being Walk of G1

for W2 being Walk of G2 st W1 = W2 holds

for n being Element of NAT holds W1 .vertexAt n = W2 .vertexAt n

proof end;

theorem :: GLIB_001:21

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:57, FINSEQ_5:def 3;

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:57, FINSEQ_5:def 3;

theorem Th22: :: GLIB_001:22

for G being _Graph

for W being Walk of G holds

( W .first() = (W .reverse()) .last() & W .last() = (W .reverse()) .first() )

for W being Walk of G holds

( W .first() = (W .reverse()) .last() & W .last() = (W .reverse()) .first() )

proof end;

theorem Th23: :: GLIB_001:23

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 )

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 Th24: :: GLIB_001:24

for G being _Graph

for W being Walk of G

for n being Element of NAT st n in dom W holds

( W . n = (W .reverse()) . (((len W) - n) + 1) & ((len W) - n) + 1 in dom (W .reverse()) )

for W being Walk of G

for n being Element of 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:25

theorem :: GLIB_001:27

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() ;

for W1 being Walk of G1

for W2 being Walk of G2 st W1 = W2 holds

W1 .reverse() = W2 .reverse() ;

theorem :: GLIB_001:28

theorem :: GLIB_001:29

theorem :: GLIB_001:30

theorem Th31: :: GLIB_001:31

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

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

theorem :: GLIB_001:33

theorem :: GLIB_001:34

theorem Th35: :: GLIB_001:35

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

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

theorem :: GLIB_001:37

theorem :: GLIB_001:38

theorem :: GLIB_001:39

theorem Th40: :: GLIB_001:40

for G being _Graph

for W being Walk of G

for n being odd Element of NAT st n < len W holds

G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) = W .cut (n,(n + 2))

for W being Walk of G

for n being odd Element of NAT st n < len W holds

G .walkOf ((W . n),(W . (n + 1)),(W . (n + 2))) = W .cut (n,(n + 2))

proof end;

theorem Th41: :: GLIB_001:41

for G being _Graph

for W being Walk of G

for m, n being odd Element of NAT st m <= n & n < len W holds

(W .cut (m,n)) .addEdge (W . (n + 1)) = W .cut (m,(n + 2))

for W being Walk of G

for m, n being odd Element of 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:42

theorem :: GLIB_001:43

theorem :: GLIB_001:44

theorem :: GLIB_001:45

theorem :: GLIB_001:46

theorem :: GLIB_001:47

for G being _Graph

for W being Walk of G

for m, n being odd Element of NAT

for i being Element of 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 )

for W being Walk of G

for m, n being odd Element of NAT

for i being Element of 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 Th48: :: GLIB_001:48

for G1, G2 being _Graph

for W1 being Walk of G1

for W2 being Walk of G2

for m, n being Element of NAT st W1 = W2 holds

W1 .cut (m,n) = W2 .cut (m,n)

for W1 being Walk of G1

for W2 being Walk of G2

for m, n being Element of NAT st W1 = W2 holds

W1 .cut (m,n) = W2 .cut (m,n)

proof end;

theorem :: GLIB_001:49

theorem :: GLIB_001:50

for G being _Graph

for W being Walk of G

for x, y being set

for m, n being Element of NAT st W is_Walk_from x,y holds

W .remove (m,n) is_Walk_from x,y by Lm25;

for W being Walk of G

for x, y being set

for m, n being Element of NAT st W is_Walk_from x,y holds

W .remove (m,n) is_Walk_from x,y by Lm25;

theorem :: GLIB_001:51

theorem :: GLIB_001:52

theorem :: GLIB_001:53

theorem :: GLIB_001:54

theorem :: GLIB_001:55

for G being _Graph

for W being Walk of G

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds

( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W ) by Lm30;

for W being Walk of G

for m, n being odd Element of NAT st m <= n & n <= len W & W . m = W . n holds

for x being Element of NAT st m <= x & x <= len (W .remove (m,n)) holds

( (W .remove (m,n)) . x = W . ((x - m) + n) & (x - m) + n is Element of NAT & (x - m) + n <= len W ) by Lm30;

theorem :: GLIB_001:56

theorem Th57: :: GLIB_001:57

for G being _Graph

for W being Walk of G

for m being Element of NAT st W . m = W .last() holds

W .remove (m,(len W)) = W .cut (1,m)

for W being Walk of G

for m being Element of NAT st W . m = W .last() holds

W .remove (m,(len W)) = W .cut (1,m)

proof end;

theorem :: GLIB_001:58

theorem :: GLIB_001:59

theorem :: GLIB_001:60

theorem :: GLIB_001:61

for G1, G2 being _Graph

for W1 being Walk of G1

for W2 being Walk of G2

for m, n being Element of NAT st W1 = W2 holds

W1 .remove (m,n) = W2 .remove (m,n)

for W1 being Walk of G1

for W2 being Walk of G2

for m, n being Element of NAT st W1 = W2 holds

W1 .remove (m,n) = W2 .remove (m,n)

proof end;

theorem :: GLIB_001:62

theorem :: GLIB_001:63

theorem :: GLIB_001:64

theorem :: GLIB_001:65

theorem :: GLIB_001:66

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

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

theorem Th68: :: GLIB_001:68

for G being _Graph

for W being Walk of G

for n being odd Element of 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()) )

for W being Walk of G

for n being odd Element of 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 Th70: :: GLIB_001:70

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*>

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

for G being _Graph

for W being Walk of G holds

( W .first() = (W .vertexSeq()) . 1 & W .last() = (W .vertexSeq()) . (len (W .vertexSeq())) )

for W being Walk of G holds

( W .first() = (W .vertexSeq()) . 1 & W .last() = (W .vertexSeq()) . (len (W .vertexSeq())) )

proof end;

theorem :: GLIB_001:72

for G being _Graph

for W being Walk of G

for n being odd Element of NAT st n <= len W holds

W .vertexAt n = (W .vertexSeq()) . ((n + 1) div 2)

for W being Walk of G

for n being odd Element of NAT st n <= len W holds

W .vertexAt n = (W .vertexSeq()) . ((n + 1) div 2)

proof end;

theorem Th73: :: GLIB_001:73

for G being _Graph

for W being Walk of G

for n being Element of NAT holds

( n in dom (W .vertexSeq()) iff (2 * n) - 1 in dom W )

for W being Walk of G

for n being Element of NAT holds

( n in dom (W .vertexSeq()) iff (2 * n) - 1 in dom W )

proof end;

theorem :: GLIB_001:74

for G being _Graph

for W being Walk of G

for n being Element of NAT holds (W .cut (1,n)) .vertexSeq() c= W .vertexSeq()

for W being Walk of G

for n being Element of NAT holds (W .cut (1,n)) .vertexSeq() c= W .vertexSeq()

proof end;

theorem Th75: :: GLIB_001:75

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*>

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 Th76: :: GLIB_001:76

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()

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

theorem :: GLIB_001:78

theorem :: GLIB_001:79

for G being _Graph

for W being Walk of G

for n being Element of NAT st n in dom (W .edgeSeq()) holds

(W .edgeSeq()) . n in the_Edges_of G

for W being Walk of G

for n being Element of NAT st n in dom (W .edgeSeq()) holds

(W .edgeSeq()) . n in the_Edges_of G

proof end;

theorem :: GLIB_001:80

theorem :: GLIB_001:81

for G being _Graph

for W being Walk of G

for n being Element of NAT holds (W .cut (1,n)) .edgeSeq() c= W .edgeSeq() by Lm43;

for W being Walk of G

for n being Element of NAT holds (W .cut (1,n)) .edgeSeq() c= W .edgeSeq() by Lm43;

theorem :: GLIB_001:82

theorem Th83: :: GLIB_001:83

for G being _Graph

for e, x, y being set holds

( e Joins x,y,G iff (G .walkOf (x,e,y)) .edgeSeq() = <*e*> )

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

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())

for W1, W2 being Walk of G st W1 .last() = W2 .first() holds

(W1 .append W2) .edgeSeq() = (W1 .edgeSeq()) ^ (W2 .edgeSeq())

proof end;

theorem Th86: :: GLIB_001:86

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()

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

theorem Th88: :: GLIB_001:88

for G being _Graph

for W being Walk of G holds

( W .first() in W .vertices() & W .last() in W .vertices() )

for W being Walk of G holds

( W .first() in W .vertices() & W .last() in W .vertices() )

proof end;

theorem Th89: :: GLIB_001:89

for G being _Graph

for W being Walk of G

for n being odd Element of NAT st n <= len W holds

W .vertexAt n in W .vertices()

for W being Walk of G

for n being odd Element of NAT st n <= len W holds

W .vertexAt n in W .vertices()

proof end;

theorem Th91: :: GLIB_001:91

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}

for e, x, y being set st e Joins x,y,G holds

(G .walkOf (x,e,y)) .vertices() = {x,y}

proof end;

theorem Th93: :: GLIB_001:93

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())

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

for G being _Graph

for W being Walk of G

for m, n being odd Element of NAT st m <= n & n <= len W holds

(W .cut (m,n)) .vertices() c= W .vertices()

for W being Walk of G

for m, n being odd Element of NAT st m <= n & n <= len W holds

(W .cut (m,n)) .vertices() c= W .vertices()

proof end;

theorem Th95: :: GLIB_001:95

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}

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

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

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

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 W9 being Walk of G st W9 is_Walk_from x,y

for W being Walk of G

for x, y being set st x in W .vertices() & y in W .vertices() holds

ex W9 being Walk of G st W9 is_Walk_from x,y

proof end;

theorem :: GLIB_001:98

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

for W1 being Walk of G1

for W2 being Walk of G2 st W1 = W2 holds

W1 .vertices() = W2 .vertices() by Th76;

theorem :: GLIB_001:99

theorem Th100: :: GLIB_001:100

for G being _Graph

for W being Walk of G

for e being set holds

( e in W .edges() iff ex n being odd Element of NAT st

( n < len W & W . (n + 1) = e ) )

for W being Walk of G

for e being set holds

( e in W .edges() iff ex n being odd Element of NAT st

( n < len W & W . (n + 1) = e ) )

proof end;

theorem Th102: :: GLIB_001:102

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())

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

theorem Th104: :: GLIB_001:104

for G being _Graph

for W being Walk of G

for e being set holds

( e in W .edges() iff ex n being Element of NAT st

( n in dom (W .edgeSeq()) & (W .edgeSeq()) . n = e ) )

for W being Walk of G

for e being set holds

( e in W .edges() iff ex n being Element of NAT st

( n in dom (W .edgeSeq()) & (W .edgeSeq()) . n = e ) )

proof end;

theorem :: GLIB_001:105

theorem :: GLIB_001:106

for G being _Graph

for W being Walk of G

for m, n being Element of NAT holds (W .cut (m,n)) .edges() c= W .edges()

for W being Walk of G

for m, n being Element of NAT holds (W .cut (m,n)) .edges() c= W .edges()

proof end;

theorem Th108: :: GLIB_001:108

for G being _Graph

for e, x, y being set holds

( e Joins x,y,G iff (G .walkOf (x,e,y)) .edges() = {e} )

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

theorem :: GLIB_001:111

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}

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

theorem :: GLIB_001:113

for G being _Graph

for W1, W2 being Walk of G holds

( len W1 = len W2 iff W1 .length() = W2 .length() )

for W1, W2 being Walk of G holds

( len W1 = len W2 iff W1 .length() = W2 .length() )

proof end;

theorem :: GLIB_001:114

theorem Th115: :: GLIB_001:115

for G being _Graph

for W being Walk of G

for n being odd Element of NAT st n <= len W holds

( W .find (W . n) <= n & W .rfind (W . n) >= n )

for W being Walk of G

for n being odd Element of NAT st n <= len W holds

( W .find (W . n) <= n & W .rfind (W . n) >= n )

proof end;

theorem :: GLIB_001:116

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 )

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

theorem :: GLIB_001:119

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 )

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

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

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

theorem :: GLIB_001:123

theorem :: GLIB_001:124

theorem :: GLIB_001:125

theorem :: GLIB_001:126

theorem :: GLIB_001:127

theorem :: GLIB_001:128

theorem :: GLIB_001:131

for G being _Graph

for W being Walk of G

for m, n being odd Element of NAT st m <= n & n <= len W holds

( W .cut (m,n) is trivial iff m = n )

for W being Walk of G

for m, n being odd Element of NAT st m <= n & n <= len W holds

( W .cut (m,n) is trivial iff m = n )

proof end;

theorem Th132: :: GLIB_001:132

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

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 Th133: :: GLIB_001:133

for G being _Graph

for W being Walk of G st not W is trivial holds

ex lenW2 being odd Element of NAT st

( lenW2 = (len W) - 2 & (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W )

for W being Walk of G st not W is trivial holds

ex lenW2 being odd Element of NAT st

( lenW2 = (len W) - 2 & (W .cut (1,lenW2)) .addEdge (W . (lenW2 + 1)) = W )

proof end;

theorem Th134: :: GLIB_001:134

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()

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

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

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

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

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

theorem :: GLIB_001:139

theorem :: GLIB_001:140

for G being _Graph

for W being Walk of G holds

( W is Trail-like iff W .reverse() is Trail-like ) by Lm58;

for W being Walk of G holds

( W is Trail-like iff W .reverse() is Trail-like ) by Lm58;

theorem :: GLIB_001:141

theorem :: GLIB_001:142

theorem :: GLIB_001:143

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()

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

theorem :: GLIB_001:146

theorem :: GLIB_001:147

for G being _Graph

for W being Path of G st W is open holds

for m, n being odd Element of NAT st m < n & n <= len W holds

W . m <> W . n

for W being Path of G st W is open holds

for m, n being odd Element of NAT st m < n & n <= len W holds

W . m <> W . n

proof end;

theorem :: GLIB_001:148

theorem :: GLIB_001:149

theorem Th150: :: GLIB_001:150

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 W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds

W . n <> v ) holds

W .addEdge e is Path-like

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 W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds

W . n <> v ) holds

W .addEdge e is Path-like

proof end;

theorem :: GLIB_001:151

theorem :: GLIB_001:152

for G being _Graph

for W being Walk of G st ( for n being odd Element of NAT st n <= len W holds

W .find (W . n) = W .rfind (W . n) ) holds

W is Path-like

for W being Walk of G st ( for n being odd Element of NAT st n <= len W holds

W .find (W . n) = W .rfind (W . n) ) holds

W is Path-like

proof end;

theorem :: GLIB_001:153

theorem :: GLIB_001:155

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

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

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() )

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

theorem :: GLIB_001:160

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 )

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 Th161: :: GLIB_001:161

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() )

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

theorem Th163: :: GLIB_001:163

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() )

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 Th164: :: GLIB_001:164

for G being _Graph

for W1, W2 being Walk of G st W1 is Subwalk of W2 holds

for m being odd Element of NAT st m <= len W1 holds

ex n being odd Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n )

for W1, W2 being Walk of G st W1 is Subwalk of W2 holds

for m being odd Element of NAT st m <= len W1 holds

ex n being odd Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n )

proof end;

theorem :: GLIB_001:165

for G being _Graph

for W1, W2 being Walk of G st W1 is Subwalk of W2 holds

for m being even Element of NAT st 1 <= m & m <= len W1 holds

ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n )

for W1, W2 being Walk of G st W1 is Subwalk of W2 holds

for m being even Element of NAT st 1 <= m & m <= len W1 holds

ex n being even Element of NAT st

( m <= n & n <= len W2 & W1 . m = W2 . n )

proof end;

theorem :: GLIB_001:166

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

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

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

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 Th169: :: GLIB_001:169

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

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 Th170: :: GLIB_001:170

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

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

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

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

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

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 Th173: :: GLIB_001:173

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)

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

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

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 Th175: :: GLIB_001:175

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 ) )

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 Th176: :: GLIB_001:176

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 ) )

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

for G1, G2 being _Graph

for x being set st G1 == G2 & x is VertexSeq of G1 holds

x is VertexSeq of G2

for x being set st G1 == G2 & x is VertexSeq of G1 holds

x is VertexSeq of G2

proof end;

theorem :: GLIB_001:180

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)

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

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 ) )

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;