defpred S1[ Nat] means for P being _finite Path-like _Graph st P .order() = $1 + 1 holds
ex P0 being vertex-distinct Path of P st
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength );
A1:
S1[ 0 ]
proof
let P be
_finite Path-like _Graph;
( P .order() = 0 + 1 implies ex P0 being vertex-distinct Path of P st
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength ) )
assume
P .order() = 0 + 1
;
ex P0 being vertex-distinct Path of P st
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )
then A2:
P is
_trivial
by GLIB_000:26;
then consider v being
Vertex of
P such that A3:
the_Vertices_of P = {v}
by GLIB_000:22;
take P0 =
P .walkOf v;
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )
thus
P0 .vertices() = the_Vertices_of P
by A3, GLIB_001:90;
( P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )
thus
P0 .edges() = the_Edges_of P
by A2;
( ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )
thus
( (
Endvertices P = {(P0 .first()),(P0 .last())} implies not
P is
_trivial ) & ( not
P is
_trivial implies
Endvertices P = {(P0 .first()),(P0 .last())} ) & (
P0 is
closed implies
P is
_trivial ) & (
P is
_trivial implies
P0 is
closed ) &
P0 is
minlength )
by A2;
verum
end;
A4:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A5:
S1[
n]
;
S1[n + 1]
let P be
_finite Path-like _Graph;
( P .order() = (n + 1) + 1 implies ex P0 being vertex-distinct Path of P st
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength ) )
assume A6:
P .order() = (n + 1) + 1
;
ex P0 being vertex-distinct Path of P st
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )
then
P .order() <> 1
;
then A7:
not
P is
_trivial
by GLIB_000:26;
then A8:
P .minDegree() = 1
by Th30;
set v = the
with_min_degree Vertex of
P;
the
with_min_degree Vertex of
P .degree() = 1
by A8, GLIB_013:def 15;
then A9:
the
with_min_degree Vertex of
P is
endvertex
by GLIB_000:174;
set H = the
removeVertex of
P, the
with_min_degree Vertex of
P;
reconsider H = the
removeVertex of
P, the
with_min_degree Vertex of
P as
_finite Path-like _Graph by A9, Th21;
(H .order()) + 1
= P .order()
by A7, GLIB_000:48;
then A10:
H .order() = n + 1
by A6;
then consider P9 being
vertex-distinct Path of
H such that A11:
(
P9 .vertices() = the_Vertices_of H &
P9 .edges() = the_Edges_of H )
and A12:
(
Endvertices H = {(P9 .first()),(P9 .last())} iff not
H is
_trivial )
and A13:
(
P9 is
closed iff
H is
_trivial )
and A14:
P9 is
minlength
by A5;
reconsider P8 =
P9 as
Walk of
P by GLIB_001:167;
reconsider P8 =
P8 as
vertex-distinct Path of
P by GLIB_001:176;
consider e being
object such that A15:
( the
with_min_degree Vertex of
P .edgesInOut() = {e} & not
e Joins the
with_min_degree Vertex of
P, the
with_min_degree Vertex of
P,
P )
by A9, GLIB_000:def 51;
set w = the
with_min_degree Vertex of
P .adj e;
e in {e}
by TARSKI:def 1;
then A16:
e Joins the
with_min_degree Vertex of
P, the
with_min_degree Vertex of
P .adj e,
P
by A15, GLIB_000:67;
then A17:
the
with_min_degree Vertex of
P <> the
with_min_degree Vertex of
P .adj e
by A15;
then A18:
not the
with_min_degree Vertex of
P .adj e in { the with_min_degree Vertex of P}
by TARSKI:def 1;
A19:
the_Vertices_of H = (the_Vertices_of P) \ { the with_min_degree Vertex of P}
by A7, GLIB_000:47;
then reconsider u = the
with_min_degree Vertex of
P .adj e as
Vertex of
H by A18, XBOOLE_0:def 5;
the
with_min_degree Vertex of
P in { the with_min_degree Vertex of P}
by TARSKI:def 1;
then A20:
not the
with_min_degree Vertex of
P in the_Vertices_of H
by A19, XBOOLE_0:def 5;
A21:
not
e in the_Edges_of H
A22:
(
P is
addAdjVertex of
H,
u,
e, the
with_min_degree Vertex of
P or
P is
addAdjVertex of
H, the
with_min_degree Vertex of
P,
e,
u )
by A7, A15, GLIB_008:38;
then A23:
(
the_Vertices_of P = (the_Vertices_of H) \/ { the with_min_degree Vertex of P} &
the_Edges_of P = (the_Edges_of H) \/ {e} )
by A20, A21, GLIB_006:def 12;
per cases
( H is _trivial or not H is _trivial )
;
suppose A24:
H is
_trivial
;
ex P0 being vertex-distinct Path of P st
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )then A25:
the_Vertices_of H = {u}
by ZFMISC_1:132;
set P0 =
P8 .addEdge e;
P8 .last() =
P9 .last()
.=
u
by A25, TARSKI:def 1
;
then A26:
e Joins P8 .last() , the
with_min_degree Vertex of
P,
P
by A16, GLIB_000:14;
not the
with_min_degree Vertex of
P in P9 .vertices()
by A20;
then
not the
with_min_degree Vertex of
P in P8 .vertices()
by GLIB_001:98;
then reconsider P0 =
P8 .addEdge e as
vertex-distinct Walk of
P by A26, GLIB_001:155;
reconsider P0 =
P0 as
vertex-distinct Path of
P ;
take
P0
;
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )thus P0 .vertices() =
(P8 .vertices()) \/ { the with_min_degree Vertex of P}
by A26, GLIB_001:95
.=
the_Vertices_of P
by A11, A23, GLIB_001:98
;
( P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )thus P0 .edges() =
(P8 .edges()) \/ {e}
by A26, GLIB_001:111
.=
the_Edges_of P
by A11, A23, GLIB_001:110
;
( ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )A27:
u =
P9 .first()
by A25, TARSKI:def 1
.=
P8 .first()
.=
P0 .first()
by A26, GLIB_001:63
;
A28:
the
with_min_degree Vertex of
P = P0 .last()
by A26, GLIB_001:63;
H .order() = 1
by A24, GLIB_000:26;
then A29:
Endvertices P =
{u} \/ { the with_min_degree Vertex of P}
by A6, A10, A23, A25, Lm6
.=
{(P0 .first()),(P0 .last())}
by A27, A28, ENUMSET1:1
;
(
P9 .first() = u &
P9 .last() = u )
by A25, TARSKI:def 1;
then
P9 is_Walk_from u,
u
by GLIB_001:def 23;
then
P0 is
minlength
by A14, A21, A22, GLIBPRE1:62, GLIBPRE1:63;
hence
( (
Endvertices P = {(P0 .first()),(P0 .last())} implies not
P is
_trivial ) & ( not
P is
_trivial implies
Endvertices P = {(P0 .first()),(P0 .last())} ) & (
P0 is
closed implies
P is
_trivial ) & (
P is
_trivial implies
P0 is
closed ) &
P0 is
minlength )
by A17, A27, A28, A29, GLIB_001:def 24;
verum end; suppose A30:
not
H is
_trivial
;
ex P0 being vertex-distinct Path of P st
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )then A31:
Endvertices H = {(P9 .first()),(P9 .last())}
by A12;
u is
endvertex
then
u in Endvertices H
by GLIB_006:def 8;
per cases then
( u = P9 .last() or u = P9 .first() )
by A31, TARSKI:def 2;
suppose A35:
u = P9 .last()
;
ex P0 being vertex-distinct Path of P st
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )then A36:
e Joins P8 .last() , the
with_min_degree Vertex of
P,
P
by A16, GLIB_000:14;
set P0 =
P8 .addEdge e;
not the
with_min_degree Vertex of
P in P9 .vertices()
by A20;
then
not the
with_min_degree Vertex of
P in P8 .vertices()
by GLIB_001:98;
then reconsider P0 =
P8 .addEdge e as
vertex-distinct Walk of
P by A36, GLIB_001:155;
reconsider P0 =
P0 as
vertex-distinct Path of
P ;
take
P0
;
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )thus A37:
P0 .vertices() =
(P8 .vertices()) \/ { the with_min_degree Vertex of P}
by A36, GLIB_001:95
.=
the_Vertices_of P
by A11, A23, GLIB_001:98
;
( P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )thus P0 .edges() =
(P8 .edges()) \/ {e}
by A36, GLIB_001:111
.=
the_Edges_of P
by A11, A23, GLIB_001:110
;
( ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )now for x being object holds
( ( not x in Endvertices P or x = P0 .first() or x = P0 .last() ) & ( ( x = P0 .first() or x = P0 .last() ) implies x in Endvertices P ) )let x be
object ;
( ( not x in Endvertices P or x = P0 .first() or x = P0 .last() ) & ( ( x = P0 .first() or x = P0 .last() ) implies b1 in Endvertices P ) )thus
( not
x in Endvertices P or
x = P0 .first() or
x = P0 .last() )
( ( x = P0 .first() or x = P0 .last() ) implies b1 in Endvertices P )assume
(
x = P0 .first() or
x = P0 .last() )
;
b1 in Endvertices Pper cases then
( x = P0 .first() or x = P0 .last() )
;
suppose
x = P0 .first()
;
b1 in Endvertices Pthen A39:
x =
P8 .first()
by A36, GLIB_001:63
.=
P9 .first()
;
then reconsider u9 =
x as
Vertex of
H ;
reconsider v9 =
u9 as
Vertex of
P by A23, XBOOLE_0:def 3;
A40:
u9 <> the
with_min_degree Vertex of
P
by A19, ZFMISC_1:56;
u9 <> the
with_min_degree Vertex of
P .adj e
by A13, A30, A35, A39, GLIB_001:def 24;
then A41:
u9 .degree() = v9 .degree()
by A40, A22, Th9;
u9 in Endvertices H
by A31, A39, TARSKI:def 2;
then
v9 .degree() = 1
by A41, GLIB_006:56, GLIB_000:174;
hence
x in Endvertices P
by GLIB_006:56, GLIB_000:174;
verum end; end; then A43:
Endvertices P = {(P0 .first()),(P0 .last())}
by TARSKI:def 2;
P0 .first() =
P8 .first()
by A36, GLIB_001:63
.=
P9 .first()
;
then
P0 .first() in the_Vertices_of H
;
then A44:
P0 .first() <> P0 .last()
by A20, A36, GLIB_001:63;
P9 is_Walk_from P9 .first() ,
u
by A35, GLIB_001:def 23;
then
P0 is
minlength
by A14, A21, A22, GLIBPRE1:62, GLIBPRE1:63;
hence
( (
Endvertices P = {(P0 .first()),(P0 .last())} implies not
P is
_trivial ) & ( not
P is
_trivial implies
Endvertices P = {(P0 .first()),(P0 .last())} ) & (
P0 is
closed implies
P is
_trivial ) & (
P is
_trivial implies
P0 is
closed ) &
P0 is
minlength )
by A43, A44, GLIB_001:def 24;
verum end; suppose A45:
u = P9 .first()
;
ex P0 being vertex-distinct Path of P st
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )then u =
P8 .first()
.=
(P8 .reverse()) .last()
by GLIB_001:22
;
then A47:
e Joins (P8 .reverse()) .last() , the
with_min_degree Vertex of
P,
P
by A16, GLIB_000:14;
set P0 =
(P8 .reverse()) .addEdge e;
not the
with_min_degree Vertex of
P in P9 .vertices()
by A20;
then
not the
with_min_degree Vertex of
P in P8 .vertices()
by GLIB_001:98;
then
not the
with_min_degree Vertex of
P in (P8 .reverse()) .vertices()
by GLIB_001:92;
then reconsider P0 =
(P8 .reverse()) .addEdge e as
vertex-distinct Walk of
P by A47, GLIB_001:155;
reconsider P0 =
P0 as
vertex-distinct Path of
P ;
take
P0
;
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )thus A48:
P0 .vertices() =
((P8 .reverse()) .vertices()) \/ { the with_min_degree Vertex of P}
by A47, GLIB_001:95
.=
(P8 .vertices()) \/ { the with_min_degree Vertex of P}
by GLIB_001:92
.=
the_Vertices_of P
by A11, A23, GLIB_001:98
;
( P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )thus P0 .edges() =
((P8 .reverse()) .edges()) \/ {e}
by A47, GLIB_001:111
.=
(P8 .edges()) \/ {e}
by GLIB_001:107
.=
the_Edges_of P
by A11, A23, GLIB_001:110
;
( ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )now for x being object holds
( ( not x in Endvertices P or x = P0 .first() or x = P0 .last() ) & ( ( x = P0 .first() or x = P0 .last() ) implies x in Endvertices P ) )let x be
object ;
( ( not x in Endvertices P or x = P0 .first() or x = P0 .last() ) & ( ( x = P0 .first() or x = P0 .last() ) implies b1 in Endvertices P ) )thus
( not
x in Endvertices P or
x = P0 .first() or
x = P0 .last() )
( ( x = P0 .first() or x = P0 .last() ) implies b1 in Endvertices P )assume
(
x = P0 .first() or
x = P0 .last() )
;
b1 in Endvertices Pper cases then
( x = P0 .first() or x = P0 .last() )
;
suppose
x = P0 .first()
;
b1 in Endvertices Pthen A50:
x =
(P8 .reverse()) .first()
by A47, GLIB_001:63
.=
P8 .last()
by GLIB_001:22
.=
P9 .last()
;
then reconsider u9 =
x as
Vertex of
H ;
reconsider v9 =
u9 as
Vertex of
P by A23, XBOOLE_0:def 3;
A51:
u9 <> the
with_min_degree Vertex of
P
by A19, ZFMISC_1:56;
u9 <> the
with_min_degree Vertex of
P .adj e
by A13, A30, A45, A50, GLIB_001:def 24;
then A52:
u9 .degree() = v9 .degree()
by A51, A22, Th9;
u9 in Endvertices H
by A31, A50, TARSKI:def 2;
then
v9 .degree() = 1
by A52, GLIB_006:56, GLIB_000:174;
hence
x in Endvertices P
by GLIB_006:56, GLIB_000:174;
verum end; end; then A54:
Endvertices P = {(P0 .first()),(P0 .last())}
by TARSKI:def 2;
P0 .first() =
(P8 .reverse()) .first()
by A47, GLIB_001:63
.=
P8 .last()
by GLIB_001:22
.=
P9 .last()
;
then
P0 .first() in the_Vertices_of H
;
then A55:
P0 .first() <> P0 .last()
by A20, A47, GLIB_001:63;
P9 .reverse() is_Walk_from P9 .last() ,
u
by A45, GLIB_001:def 23, GLIB_001:23;
then
P0 is
minlength
by A14, A21, A22, GLIBPRE1:62, GLIBPRE1:63;
hence
( (
Endvertices P = {(P0 .first()),(P0 .last())} implies not
P is
_trivial ) & ( not
P is
_trivial implies
Endvertices P = {(P0 .first()),(P0 .last())} ) & (
P0 is
closed implies
P is
_trivial ) & (
P is
_trivial implies
P0 is
closed ) &
P0 is
minlength )
by A54, A55, GLIB_001:def 24;
verum end; end;
end;
A58:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A4);
let P be _finite Path-like _Graph; ex P0 being vertex-distinct Path of P st
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is trivial implies P is _trivial ) & ( P is _trivial implies P0 is trivial ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )
consider n being Nat such that
A59:
P .order() = n + 1
by NAT_1:6;
consider P0 being vertex-distinct Path of P such that
A60:
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) )
and
A61:
( ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )
by A58, A59;
take
P0
; ( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is trivial implies P is _trivial ) & ( P is _trivial implies P0 is trivial ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )
hence
( P0 .vertices() = the_Vertices_of P & P0 .edges() = the_Edges_of P & ( Endvertices P = {(P0 .first()),(P0 .last())} implies not P is _trivial ) & ( not P is _trivial implies Endvertices P = {(P0 .first()),(P0 .last())} ) & ( P0 is trivial implies P is _trivial ) & ( P is _trivial implies P0 is trivial ) & ( P0 is closed implies P is _trivial ) & ( P is _trivial implies P0 is closed ) & P0 is minlength )
by A60, A61; verum