let G be _Graph; for P being Path of G st P is open holds
for a, e, b being set st not a in P .vertices() & b = P .first() & e Joins a,b,G holds
(G .walkOf (a,e,b)) .append P is Path-like
let P be Path of G; ( P is open implies for a, e, b being set st not a in P .vertices() & b = P .first() & e Joins a,b,G holds
(G .walkOf (a,e,b)) .append P is Path-like )
assume A1:
P is open
; for a, e, b being set st not a in P .vertices() & b = P .first() & e Joins a,b,G holds
(G .walkOf (a,e,b)) .append P is Path-like
let a, e, b be set ; ( not a in P .vertices() & b = P .first() & e Joins a,b,G implies (G .walkOf (a,e,b)) .append P is Path-like )
assume that
A2:
not a in P .vertices()
and
A3:
b = P .first()
and
A4:
e Joins a,b,G
; (G .walkOf (a,e,b)) .append P is Path-like
set T = G .walkOf (a,e,b);
A5:
(G .walkOf (a,e,b)) .last() = P .first()
by A3, A4, GLIB_001:15;
set J = (G .walkOf (a,e,b)) .append P;
3 in Seg 3
by FINSEQ_1:3;
then
3 in Seg (len (G .walkOf (a,e,b)))
by A4, GLIB_001:14;
then
3 in dom (G .walkOf (a,e,b))
by FINSEQ_1:def 3;
then
((G .walkOf (a,e,b)) .append P) . 3 = (G .walkOf (a,e,b)) . 3
by GLIB_001:32;
then A6:
((G .walkOf (a,e,b)) .append P) . 3 = (G .walkOf (a,e,b)) .last()
by A4, GLIB_001:14;
then A7:
((G .walkOf (a,e,b)) .append P) . 3 = b
by A4, GLIB_001:15;
A8:
now for m, n being odd Nat st m < n & n <= len ((G .walkOf (a,e,b)) .append P) holds
not ((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) . nlet m,
n be
odd Nat;
( m < n & n <= len ((G .walkOf (a,e,b)) .append P) implies not ((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) . n )assume that A9:
m < n
and A10:
n <= len ((G .walkOf (a,e,b)) .append P)
;
not ((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) . nassume A11:
((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) . n
;
contradictionA12:
1
<= m
by ABIAN:12;
then
(2 * 0) + 1
< n
by A9, XXREAL_0:2;
then A13:
1
+ 2
<= n
by Th4;
now not m = 1assume
m = 1
;
contradictionthen
((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) .first()
;
then
((G .walkOf (a,e,b)) .append P) . m = (G .walkOf (a,e,b)) .first()
by A5, GLIB_001:30;
then A14:
not
((G .walkOf (a,e,b)) .append P) . m in P .vertices()
by A2, A4, GLIB_001:15;
per cases
( n = 3 or n > 3 )
by A13, XXREAL_0:1;
suppose A15:
n > 3
;
contradictionthen
not
n in Seg 3
by FINSEQ_1:1;
then
not
n in Seg (len (G .walkOf (a,e,b)))
by A4, GLIB_001:14;
then A16:
not
n in dom (G .walkOf (a,e,b))
by FINSEQ_1:def 3;
1
<= n
by A15, XXREAL_0:2;
then
n in dom ((G .walkOf (a,e,b)) .append P)
by A10, FINSEQ_3:25;
then consider j being
Element of
NAT such that A17:
j < len P
and A18:
n = (len (G .walkOf (a,e,b))) + j
by A16, GLIB_001:34;
reconsider jj =
j as
even Nat by A18;
reconsider j1 =
jj + 1 as
odd Nat ;
j + 1
<= len P
by A17, NAT_1:13;
then
P . j1 in P .vertices()
by GLIB_001:87;
hence
contradiction
by A5, A11, A14, A17, A18, GLIB_001:33;
verum end; end; end; then
(2 * 0) + 1
< m
by A12, XXREAL_0:1;
then A19:
1
+ 2
<= m
by Th4;
then
3
<= n
by A9, XXREAL_0:2;
then
1
<= n
by XXREAL_0:2;
then
n in Seg (len ((G .walkOf (a,e,b)) .append P))
by A10, FINSEQ_1:1;
then A20:
n in dom ((G .walkOf (a,e,b)) .append P)
by FINSEQ_1:def 3;
3
< n
by A9, A19, XXREAL_0:2;
then
not
n in Seg 3
by FINSEQ_1:1;
then
not
n in Seg (len (G .walkOf (a,e,b)))
by A4, GLIB_001:14;
then
not
n in dom (G .walkOf (a,e,b))
by FINSEQ_1:def 3;
then consider j being
Element of
NAT such that A21:
j < len P
and A22:
n = (len (G .walkOf (a,e,b))) + j
by A20, GLIB_001:34;
reconsider jj =
j as
even Nat by A22;
reconsider j1 =
jj + 1 as
odd Nat ;
A23:
j1 <= len P
by A21, NAT_1:13;
m < len ((G .walkOf (a,e,b)) .append P)
by A9, A10, XXREAL_0:2;
then A24:
m in dom ((G .walkOf (a,e,b)) .append P)
by A12, FINSEQ_3:25;
A25:
((G .walkOf (a,e,b)) .append P) . n = P . (j + 1)
by A5, A21, A22, GLIB_001:33;
now not m = 3assume
m = 3
;
contradictionthen A26:
((G .walkOf (a,e,b)) .append P) . m = P . 1
by A3, A4, A6, GLIB_001:15;
0 <> j
by A4, A9, A19, A22, GLIB_001:14;
then
(2 * 0) + 1
< j1
by XREAL_1:8;
hence
contradiction
by A1, A11, A25, A23, A26, GLIB_001:147;
verum end; then
3
< m
by A19, XXREAL_0:1;
then
not
m in Seg 3
by FINSEQ_1:1;
then
not
m in Seg (len (G .walkOf (a,e,b)))
by A4, GLIB_001:14;
then
not
m in dom (G .walkOf (a,e,b))
by FINSEQ_1:def 3;
then consider k being
Element of
NAT such that A27:
k < len P
and A28:
m = (len (G .walkOf (a,e,b))) + k
by A24, GLIB_001:34;
reconsider kk =
k as
even Nat by A28;
reconsider k1 =
kk + 1 as
odd Nat ;
k < j
by A9, A22, A28, XREAL_1:7;
then A29:
k1 < j1
by XREAL_1:8;
((G .walkOf (a,e,b)) .append P) . m = P . (k + 1)
by A5, A27, A28, GLIB_001:33;
hence
contradiction
by A1, A11, A25, A23, A29, GLIB_001:147;
verum end;
now for m, n being odd Element of NAT st m <= len ((G .walkOf (a,e,b)) .append P) & n <= len ((G .walkOf (a,e,b)) .append P) & ((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) . n holds
n = mlet m,
n be
odd Element of
NAT ;
( m <= len ((G .walkOf (a,e,b)) .append P) & n <= len ((G .walkOf (a,e,b)) .append P) & ((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) . n implies n = m )assume that A30:
m <= len ((G .walkOf (a,e,b)) .append P)
and A31:
n <= len ((G .walkOf (a,e,b)) .append P)
;
( ((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) . n implies n = m )assume A32:
((G .walkOf (a,e,b)) .append P) . m = ((G .walkOf (a,e,b)) .append P) . n
;
n = mthen A33:
not
n < m
by A8, A30;
m >= n
by A8, A31, A32;
hence
n = m
by A33, XXREAL_0:1;
verum end;
hence
(G .walkOf (a,e,b)) .append P is Path-like
by GLIB_001:146; verum