let G be _Graph; for W being Path of G
for e, v being object st 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 Path of G; for e, v being object st 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 ; ( 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:
e Joins W .last() ,v,G
and
A2:
not e in W .edges()
and
A3:
( not W is V5() or W is open )
and
A4:
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;
A5:
e in (W .last()) .edgesInOut()
by A1, 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) ) ) )thus
W .addEdge e is
Trail-like
by A2, A5, 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 A6:
m < n
and A7:
n <= len (W .addEdge e)
and A8:
(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 A3;
suppose A9:
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 A10:
n <= len W
;
( m = 1 & n = len (W .addEdge e) )A11:
1
<= m
by ABIAN:12;
m <= len W
by A6, A10, XXREAL_0:2;
then
m in dom W
by A11, FINSEQ_3:25;
then A12:
(W .addEdge e) . m = W . m
by A1, Lm38;
1
<= n
by ABIAN:12;
then
n in dom W
by A10, FINSEQ_3:25;
then A13:
W . m = W . n
by A1, A8, A12, Lm38;
then
m = 1
by A6, A10, Def28;
then
W .first() = W .last()
by A6, A10, A13, Def28;
hence
(
m = 1 &
n = len (W .addEdge e) )
by A9;
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 A14:
len (W .addEdge e) <= n
by A1, Lm37;
then A15:
n = len (W .addEdge e)
by A7, XXREAL_0:1;
then
(W .addEdge e) . n = (W .addEdge e) . ((len W) + 2)
by A1, Lm37;
then A16:
(W .addEdge e) . n = v
by A1, Lm38;
m < (len W) + (1 + 1)
by A1, A6, A15, 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 A1, A8, A16, Lm38;
hence
m = 1
;
n = len (W .addEdge e)thus
n = len (W .addEdge e)
by A7, A14, XXREAL_0:1;
verum end; hence
(
m = 1 &
n = len (W .addEdge e) )
;
verum 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 Th12;
then A20:
len (W .addEdge e) = 1
+ 2
by A1, Lm37;
A21:
m + 1
<= n
by A6, 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
m < 3
by A6, A7, A20, XXREAL_0:1;
then
(m + 1) - 1
<= 3
- 1
by 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 A7, A22, A23, XXREAL_0:1;
verum end; hence
(
m = 1 &
n = len (W .addEdge e) )
;
verum end;
hence
W .addEdge e is Path-like
; verum