begin
begin
::
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)) ) );
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
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 )
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 )
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 )
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
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 )
Lm7:
for G being _Graph
for W being Walk of G holds
( W .first() = (W .reverse()) .last() & W .last() = (W .reverse()) .first() )
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 )
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)
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) )
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() )
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) )
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) )
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 ) )
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 ) ) )
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 )
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)
Lm18:
for G being _Graph
for W being Walk of G holds W .cut (1,(len W)) = W
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)*>
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)
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)
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
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
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
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
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
Lm27:
for G being _Graph
for W being Walk of G
for m being Element of NAT holds W .remove (m,m) = W
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()
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
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 )
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
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))
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() )
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)) ) )
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*>
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 )
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
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 ) )
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
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) )
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 )
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 )
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()
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*>
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 ) )
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 ) )
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 )
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() )
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
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
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 )
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 )
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
Lm54:
for G being _Graph
for W being Walk of G holds
( not W is trivial iff 3 <= len W )
Lm55:
for G being _Graph
for W being Walk of G holds
( not W is trivial iff len W <> 1 )
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 )
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 )
Lm58:
for G being _Graph
for W being Walk of G holds
( W is Trail-like iff W .reverse() is Trail-like )
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
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
Lm61:
for G being _Graph
for W being Walk of G st len W <= 3 holds
W is Trail-like
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
Lm63:
for G being _Graph
for W being Walk of G holds
( W is Path-like iff W .reverse() is Path-like )
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
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
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
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
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
Lm69:
for G being _Graph
for W being Walk of G st len W <= 3 holds
W is Path-like
Lm70:
for G being _Graph
for W being Walk of G holds W is Subwalk of W
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
Lm72:
for G being _Graph
for W1, W2 being Walk of G st W1 is Subwalk of W2 holds
len W1 <= len W2
begin
theorem Th15:
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 )