let G be _Graph; :: thesis: for W being Path of G
for e, v being set st e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or not W is closed ) & ( for n being odd 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; :: thesis: for e, v being set st e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or not W is closed ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> v ) holds
W .addEdge e is Path-like
let e, v be set ; :: thesis: ( e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or not W is closed ) & ( 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 A1:
( e Joins W .last() ,v,G & not e in W .edges() & ( W is trivial or not W is closed ) & ( for n being odd Element of NAT st 1 < n & n <= len W holds
W . n <> v ) )
; :: thesis: W .addEdge e is Path-like
then A2:
e in (W .last() ) .edgesInOut()
by GLIB_000:65;
set W2 = W .addEdge e;
reconsider lenW = len W as odd Element of NAT ;
now thus
W .addEdge e is
Trail-like
by A1, A2, Lm60;
:: thesis: 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 ;
:: thesis: ( m < n & n <= len (W .addEdge e) & (W .addEdge e) . m = (W .addEdge e) . n implies ( m = 1 & n = len (W .addEdge e) ) )assume A3:
(
m < n &
n <= len (W .addEdge e) &
(W .addEdge e) . m = (W .addEdge e) . n )
;
:: thesis: ( m = 1 & n = len (W .addEdge e) )now per cases
( not W is closed or W is trivial )
by A1;
suppose A4:
not
W is
closed
;
:: thesis: ( m = 1 & n = len (W .addEdge e) )now per cases
( n <= len W or n > len W )
;
suppose A5:
n <= len W
;
:: thesis: ( m = 1 & n = len (W .addEdge e) )then A6:
m <= len W
by A3, XXREAL_0:2;
1
<= m
by HEYTING3:1;
then
m in dom W
by A6, FINSEQ_3:27;
then A7:
(W .addEdge e) . m = W . m
by A1, Lm38;
1
<= n
by HEYTING3:1;
then A8:
n in dom W
by A5, FINSEQ_3:27;
then
W . m = W . n
by A1, A3, A7, Lm38;
then
(
m = 1 &
n = len W )
by A3, A5, Def28;
then
W .first() = W .last()
by A1, A3, A7, A8, Lm38;
hence
(
m = 1 &
n = len (W .addEdge e) )
by A4, Def24;
:: thesis: verum end; suppose
n > len W
;
:: thesis: ( 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 A9:
len (W .addEdge e) <= n
by A1, Lm37;
then A10:
n = len (W .addEdge e)
by A3, XXREAL_0:1;
then
(W .addEdge e) . n = (W .addEdge e) . ((len W) + 2)
by A1, Lm37;
then A11:
(W .addEdge e) . n = v
by A1, Lm38;
m < (len W) + (1 + 1)
by A1, A3, A10, Lm37;
then
m < ((len W) + 1) + 1
;
then
m <= lenW + 1
by NAT_1:13;
then
m < lenW + 1
by XXREAL_0:1;
then A12:
m <= len W
by NAT_1:13;
1
<= m
by HEYTING3:1;
then
m in dom W
by A12, FINSEQ_3:27;
then A13:
W . m = v
by A1, A3, A11, Lm38;
hence
m = 1
;
:: thesis: n = len (W .addEdge e)thus
n = len (W .addEdge e)
by A3, A9, XXREAL_0:1;
:: thesis: verum end; hence
(
m = 1 &
n = len (W .addEdge e) )
;
:: thesis: verum suppose
W is
trivial
;
:: thesis: ( m = 1 & n = len (W .addEdge e) )then consider v being
Vertex of
G such that A15:
W = G .walkOf v
by Lm56;
len W = 1
by A15, Th14;
then A16:
len (W .addEdge e) = 1
+ 2
by A1, Lm37;
A17:
1
<= m
by HEYTING3:1;
then A18:
1
+ 1
<= m + 1
by XREAL_1:9;
m + 1
<= n
by A3, NAT_1:13;
then
2
* 1
<= n
by A18, XXREAL_0:2;
then
2
* 1
< n
by XXREAL_0:1;
then A19:
len (W .addEdge e) <= n
by A16, NAT_1:13;
then
m < 3
by A3, A16, XXREAL_0:1;
then
(m + 1) - 1
<= 3
- 1
by A16, 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:15;
hence
(
m = 1 &
n = len (W .addEdge e) )
by A3, A17, A19, XXREAL_0:1;
:: thesis: verum end; hence
(
m = 1 &
n = len (W .addEdge e) )
;
:: thesis: verum end;
hence
W .addEdge e is Path-like
by Def28; :: thesis: verum