let G be _Graph; for W being Walk of G
for e, v being object st W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( not W is V5() 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
let W be Walk of G; for e, v being object st W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( not W is V5() 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
let e, v be object ; ( W is Path-like & e Joins W .last() ,v,G & not e in W .edges() & ( not W is V5() or W is open ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> v ) implies W .addEdge e is Path-like )
assume that
A1:
W is Path-like
and
A2:
e Joins W .last() ,v,G
and
A3:
not e in W .edges()
and
A4:
( not W is V5() or W is open )
and
A5:
for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> v
; W .addEdge e is Path-like
reconsider lenW = len W as odd Element of NAT ;
set W2 = W .addEdge e;
A6:
e in (W .last()) .edgesInOut()
by A2, GLIB_000:62;
now ( W .addEdge e is Trail-like & ( for m, n being odd Element of NAT st m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n holds
( m = 1 & n = len (W .addEdge e) ) ) )
W is
Trail-like
by A1;
hence
W .addEdge e is
Trail-like
by A3, A6, Lm60;
for m, n being odd Element of NAT st m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n holds
( m = 1 & n = len (W .addEdge e) )let m,
n be
odd Element of
NAT ;
( m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n implies ( m = 1 & n = len (W .addEdge e) ) )assume that A7:
m < n
and A8:
n <= len (W .addEdge e)
and A9:
(W .addEdge e) . m = (W .addEdge e) . n
;
( m = 1 & n = len (W .addEdge e) )now ( m = 1 & n = len (W .addEdge e) )per cases
( W is open or not W is V5() )
by A4;
suppose A10:
W is
open
;
( m = 1 & n = len (W .addEdge e) )now ( m = 1 & n = len (W .addEdge e) )per cases
( n <= len W or n > len W )
;
suppose A11:
n <= len W
;
( m = 1 & n = len (W .addEdge e) )A12:
1
<= m
by ABIAN:12;
m <= len W
by A7, A11, XXREAL_0:2;
then
m in dom W
by A12, FINSEQ_3:25;
then A13:
(W .addEdge e) . m = W . m
by A2, Lm38;
1
<= n
by ABIAN:12;
then
n in dom W
by A11, FINSEQ_3:25;
then A14:
W . m = W . n
by A2, A9, A13, Lm38;
then
m = 1
by A1, A7, A11;
then
W .first() = W .last()
by A1, A7, A11, A14;
hence
(
m = 1 &
n = len (W .addEdge e) )
by A10;
verum end; suppose
n > len W
;
( m = 1 & n = len (W .addEdge e) )then
lenW + 1
<= n
by NAT_1:13;
then
lenW + 1
< n
by XXREAL_0:1;
then
(lenW + 1) + 1
<= n
by NAT_1:13;
then
(len W) + (1 + 1) <= n
;
then A15:
len (W .addEdge e) <= n
by A2, Lm37;
then
n = len (W .addEdge e)
by A8, XXREAL_0:1;
then
(W .addEdge e) . n = (W .addEdge e) . ((len W) + 2)
by A2, Lm37;
then A16:
(W .addEdge e) . n = v
by A2, Lm38;
m < len (W .addEdge e)
by A7, A8, A15, XXREAL_0:1;
then
m < (len W) + (1 + 1)
by A2, Lm37;
then
m < ((len W) + 1) + 1
;
then
m <= lenW + 1
by NAT_1:13;
then
m < lenW + 1
by XXREAL_0:1;
then A17:
m <= len W
by NAT_1:13;
1
<= m
by ABIAN:12;
then
m in dom W
by A17, FINSEQ_3:25;
then A18:
W . m = v
by A2, A9, A16, Lm38;
hence
m = 1
;
n = len (W .addEdge e)thus
n = len (W .addEdge e)
by A8, A15, XXREAL_0:1;
verum end; end; end; hence
(
m = 1 &
n = len (W .addEdge e) )
;
verum end; suppose
W is
V5()
;
( m = 1 & n = len (W .addEdge e) )then
ex
v being
Vertex of
G st
W = G .walkOf v
by Lm56;
then
len W = 1
by FINSEQ_1:39;
then A20:
len (W .addEdge e) = 1
+ 2
by A2, Lm37;
A21:
m + 1
<= n
by A7, NAT_1:13;
A22:
1
<= m
by ABIAN:12;
then
1
+ 1
<= m + 1
by XREAL_1:7;
then
2
* 1
<= n
by A21, XXREAL_0:2;
then
2
* 1
< n
by XXREAL_0:1;
then A23:
len (W .addEdge e) <= n
by A20, NAT_1:13;
then
n = len (W .addEdge e)
by A8, XXREAL_0:1;
then
(m + 1) - 1
<= 3
- 1
by A7, A20, NAT_1:13;
then
m < 2
* 1
by XXREAL_0:1;
then
m + 1
<= 2
by NAT_1:13;
then
(m + 1) - 1
<= 2
- 1
by XREAL_1:13;
hence
(
m = 1 &
n = len (W .addEdge e) )
by A8, A22, A23, XXREAL_0:1;
verum end; end; end; hence
(
m = 1 &
n = len (W .addEdge e) )
;
verum end;
hence
W .addEdge e is Path-like
; verum