:: About Path and Cycle Graphs
:: by Sebastian Koch
::
:: Received December 9, 2024
:: Copyright (c) 2024-2025 Association of Mizar Users

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial non-Dmulti loopfull non 0 -vertex for set ;

existence
ex b₁ being _Graph st
( b₁ is _trivial & b₁ is non-Dmulti & b₁ is loopfull )

proof end;

let G be non acyclic _Graph;

cluster Relation-like omega -defined Function-like finite [Graph-like] non acyclic non 0 -vertex for Subgraph of G;

existence
not for b₁ being Subgraph of G holds b₁ is acyclic

proof end;

end;

:: variant of GLIB_000:81 for possibly infinite graphs
:: into GLIB_000 ?

theorem Th1: :: GLPACY00:1

for G1 being _Graph
for G2 being Subgraph of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( v2 .inDegree() c= v1 .inDegree() & v2 .outDegree() c= v1 .outDegree() & v2 .degree() c= v1 .degree() )

proof end;

::: into GLIB_001 ?

theorem Th4: :: GLPACY00:2

for G being _Graph
for T being Trail of G holds T .length() = card (T .edges())

proof end;

Th5: for G being _Graph
for C being Walk of G
for u, v, w being object st C is Cycle-like & u in C .vertices() & v in C .vertices() & u <> w & v <> w holds
ex W being Path of G st
( W is_Walk_from u,v & not w in W .vertices() )
by GLIBPRE1:130;

::: into GLIB_002

registration

let G be non acyclic _Graph;

cluster non empty Relation-like omega -defined (the_Vertices_of G) \/ (the_Edges_of G) -valued Function-like finite FinSequence-like FinSubsequence-like Cycle-like for Walk of G;

existence
ex b₁ being Walk of G st b₁ is Cycle-like by GLIB_002:def 2;

end;

Lm1: for T being non _trivial Tree-like _Graph
for v being Vertex of T
for F being removeVertex of T,v
for C being Component of F
for w1, w2 being Vertex of F st w1 <> w2 & w1 in the_Vertices_of C & w2 in the_Vertices_of C & w1 in v .allNeighbors() holds
not w2 in v .allNeighbors()

proof end;

::: into CHORD

theorem Th6: :: GLPACY00:3

for T being non _trivial Tree-like _Graph
for v being Vertex of T
for F being removeVertex of T,v holds F .numComponents() = v .degree()

proof end;

::: into GLIBPRE0

theorem Th7: :: GLPACY00:4

for T being _finite non _trivial Tree-like _Graph
for v being Vertex of T
for F being removeVertex of T,v
for C being Component of F ex w being Vertex of T st
( w is endvertex & w in the_Vertices_of C )

proof end;

::: into GLIBPRE0

theorem Th9: :: GLPACY00:5

for G2 being _Graph
for v, e, w being object
for v2 being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st v1 <> v & v1 <> w & v1 = v2 holds
( v1 .edgesIn() = v2 .edgesIn() & v1 .inDegree() = v2 .inDegree() & v1 .edgesOut() = v2 .edgesOut() & v1 .outDegree() = v2 .outDegree() & v1 .edgesInOut() = v2 .edgesInOut() & v1 .degree() = v2 .degree() )

proof end;

::: into GLIBPRE0

theorem Th10: :: GLPACY00:6

for G2 being _Graph
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for v1 being Vertex of G1 st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v1 = v holds
( v1 .edgesIn() = v .edgesIn() & v1 .inDegree() = v .inDegree() & v1 .edgesOut() = (v .edgesOut()) \/ {e} & v1 .outDegree() = (v .outDegree()) +` 1 & v1 .edgesInOut() = (v .edgesInOut()) \/ {e} & v1 .degree() = (v .degree()) +` 1 )

proof end;

::: into GLIBPRE0

theorem Th11: :: GLPACY00:7

for G2 being _Graph
for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w
for w1 being Vertex of G1 st not e in the_Edges_of G2 & not v in the_Vertices_of G2 & w1 = w holds
( w1 .edgesIn() = (w .edgesIn()) \/ {e} & w1 .inDegree() = (w .inDegree()) +` 1 & w1 .edgesOut() = w .edgesOut() & w1 .outDegree() = w .outDegree() & w1 .edgesInOut() = (w .edgesInOut()) \/ {e} & w1 .degree() = (w .degree()) +` 1 )

proof end;

::: into GLIBPRE0

theorem Th12: :: GLPACY00:8

for G being _Graph
for C being Component of G holds Endvertices C c= Endvertices G

proof end;

::: into GLIB_006

registration

let G be edgeless _Graph;

cluster Endvertices G -> empty ;

coherence
Endvertices G is empty

proof end;

end;

Th8: for G being complete _Graph st 3 c= G .order() holds
not G is acyclic
by GLIB_013:100;

Th13: for G being _Graph
for n being Nat st ( for v being Vertex of G holds v .degree() c= n ) holds
G is with_max_degree
by GLIB_013:101;

Th16: for G being _Graph
for C being Component of G holds
( G .minDegree() c= C .minDegree() & G .minInDegree() c= C .minInDegree() & G .minOutDegree() c= C .minOutDegree() )
by GLIB_013:104;

:: this definition includes the ray and the double ray

definition

let G be _Graph;

attr G is Path-like means :Def1: :: GLPACY00:def 1
( G is Tree-like & ( for v being Vertex of G holds v .degree() c= 2 ) );

end;

:: deftheorem Def1 defines Path-like GLPACY00:def 1 :
for G being _Graph holds
( G is Path-like iff ( G is Tree-like & ( for v being Vertex of G holds v .degree() c= 2 ) ) );

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] Path-like -> Tree-like locally-finite with_max_degree for set ;

coherence
for b₁ being _Graph st b₁ is Path-like holds
( b₁ is Tree-like & b₁ is locally-finite & b₁ is with_max_degree )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial edgeless -> Path-like for set ;

coherence
for b₁ being _Graph st b₁ is _trivial & b₁ is edgeless holds
b₁ is Path-like ;

cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial Path-like -> edgeless for set ;

coherence
for b₁ being _Graph st b₁ is _trivial & b₁ is Path-like holds
b₁ is edgeless ;

cluster Relation-like omega -defined Function-like finite [Graph-like] _finite non 0 -vertex Path-like for set ;

existence
ex b₁ being _Graph st
( b₁ is _finite & b₁ is Path-like )

proof end;

end;

theorem Th17: :: GLPACY00:9

for G being locally-finite _Graph holds
( G is Path-like iff ( G is Tree-like & ( for v being Vertex of G holds v .degree() <= 2 ) ) )

proof end;

definition

let F be Graph-yielding Function;

attr F is Path-like means :Def2: :: GLPACY00:def 2
for x being object st x in dom F holds
ex G being _Graph st
( F . x = G & G is Path-like );

end;

:: deftheorem Def2 defines Path-like GLPACY00:def 2 :
for F being Graph-yielding Function holds
( F is Path-like iff for x being object st x in dom F holds
ex G being _Graph st
( F . x = G & G is Path-like ) );

registration

let P be Path-like _Graph;

cluster <*P*> -> Path-like ;

coherence
<*P*> is Path-like

proof end;

cluster NAT --> P -> Path-like ;

coherence
NAT --> P is Path-like by FUNCOP_1:7;

end;

definition

let F be non empty Graph-yielding Function;

redefine attr F is Path-like means :Def3: :: GLPACY00:def 3
for x being Element of dom F holds F . x is Path-like ;

compatibility
( F is Path-like iff for x being Element of dom F holds F . x is Path-like )

proof end;

end;

:: deftheorem Def3 defines Path-like GLPACY00:def 3 :
for F being non empty Graph-yielding Function holds
( F is Path-like iff for x being Element of dom F holds F . x is Path-like );

Lm2: for F being ManySortedSet of NAT
for n being object holds
( n is Nat iff n in dom F )

proof end;

definition

let S be GraphSeq;

redefine attr S is Path-like means :Def4: :: GLPACY00:def 4
for n being Nat holds S . n is Path-like ;

compatibility
( S is Path-like iff for n being Nat holds S . n is Path-like )

proof end;

end;

:: deftheorem Def4 defines Path-like GLPACY00:def 4 :
for S being GraphSeq holds
( S is Path-like iff for n being Nat holds S . n is Path-like );

registration

cluster empty Relation-like Function-like Graph-yielding -> Graph-yielding Path-like for set ;

coherence
for b₁ being Graph-yielding Function st b₁ is empty holds
b₁ is Path-like ;

cluster Relation-like Function-like Graph-yielding _trivial edgeless -> Graph-yielding Path-like for set ;

coherence
for b₁ being Graph-yielding Function st b₁ is _trivial & b₁ is edgeless holds
b₁ is Path-like

proof end;

cluster Relation-like Function-like Graph-yielding Path-like -> Graph-yielding Tree-like for set ;

coherence
for b₁ being Graph-yielding Function st b₁ is Path-like holds
b₁ is Tree-like

proof end;

cluster non empty Relation-like omega -defined Function-like total Graph-yielding Path-like for set ;

existence
ex b₁ being GraphSeq st
( not b₁ is empty & b₁ is Path-like )

proof end;

end;

registration

let F be non empty Graph-yielding Path-like Function;
let x be Element of dom F;

cluster F . x -> Path-like ;

coherence
F . x is Path-like by Def3;

end;

registration

let S be Path-like GraphSeq;
let n be Nat;

cluster S . n -> Path-like ;

coherence
S . n is Path-like by Def4;

end;

registration

let p be Graph-yielding Path-like FinSequence;
let n be Nat;

cluster p | n -> Path-like ;

coherence
p | n is Path-like

proof end;

cluster p /^ n -> Path-like ;

coherence
p /^ n is Path-like

proof end;

let m be Nat;

cluster smid (p,m,n) -> Path-like ;

coherence
smid (p,m,n) is Path-like

proof end;

cluster (m,n) -cut p -> Path-like ;

coherence
(m,n) -cut p is Path-like

proof end;

end;

registration

let p, q be Graph-yielding Path-like FinSequence;

cluster p ^ q -> Path-like ;

coherence
p ^ q is Path-like

proof end;

cluster p ^' q -> Path-like ;

coherence
p ^' q is Path-like

proof end;

end;

registration

let P1, P2 be Path-like _Graph;

cluster <*P1,P2*> -> Path-like ;

coherence
<*P1,P2*> is Path-like

proof end;

let P3 be Path-like _Graph;

cluster <*P1,P2,P3*> -> Path-like ;

coherence
<*P1,P2,P3*> is Path-like

proof end;

end;

definition

let S be Graph-membered set ;

attr S is Path-like means :Def5: :: GLPACY00:def 5
for G being _Graph st G in S holds
G is Path-like ;

end;

:: deftheorem Def5 defines Path-like GLPACY00:def 5 :
for S being Graph-membered set holds
( S is Path-like iff for G being _Graph st G in S holds
G is Path-like );

registration

cluster empty Graph-membered -> Graph-membered Path-like for set ;

coherence
for b₁ being Graph-membered set st b₁ is empty holds
b₁ is Path-like ;

cluster Graph-membered Path-like -> Graph-membered Tree-like for set ;

coherence
for b₁ being Graph-membered set st b₁ is Path-like holds
b₁ is Tree-like

proof end;

end;

registration

let P1 be Path-like _Graph;

cluster {P1} -> Path-like ;

coherence
{P1} is Path-like by TARSKI:def 1;
let P2 be Path-like _Graph;

cluster {P1,P2} -> Path-like ;

coherence
{P1,P2} is Path-like

proof end;

end;

registration

let F be Graph-yielding Path-like Function;

cluster rng F -> Path-like ;

coherence
rng F is Path-like

proof end;

end;

registration

let X be Graph-membered Path-like set ;

cluster -> Path-like for Element of K32(X);

coherence
for b₁ being Subset of X holds b₁ is Path-like by Def5;

end;

registration

let X be Graph-membered Path-like set ;
let Y be set ;

cluster X /\ Y -> Path-like ;

coherence
X /\ Y is Path-like

proof end;

cluster X \ Y -> Path-like ;

coherence
X \ Y is Path-like ;

end;

registration

let X, Y be Graph-membered Path-like set ;

cluster X \/ Y -> Path-like ;

coherence
X \/ Y is Path-like

proof end;

cluster X \+\ Y -> Path-like ;

coherence
X \+\ Y is Path-like ;

end;

registration

cluster non empty Graph-membered Path-like for set ;

existence
ex b₁ being Graph-membered set st
( not b₁ is empty & b₁ is Path-like )

proof end;

end;

registration

let S be non empty Graph-membered Path-like set ;

cluster -> Path-like for Element of S;

coherence
for b₁ being Element of S holds b₁ is Path-like by Def5;

end;

Lm3: for G1, G2 being _Graph st G1 == G2 & G1 is Path-like holds
G2 is Path-like

proof end;

:: adding a vertex incident with an endvertex of a path results in a path

theorem Th18: :: GLPACY00:10

for P2 being Path-like _Graph
for v2 being Vertex of P2
for e, w2 being object
for P1 being addAdjVertex of P2,v2,e,w2 st ( v2 is endvertex or P2 is _trivial ) holds
P1 is Path-like

proof end;

theorem Th19: :: GLPACY00:11

for P2 being Path-like _Graph
for v2, e being object
for w2 being Vertex of P2
for P1 being addAdjVertex of P2,v2,e,w2 st ( w2 is endvertex or P2 is _trivial ) holds
P1 is Path-like

proof end;

registration

let n be Nat;

cluster Relation-like omega -defined Function-like finite [Graph-like] non 0 -vertex n + 1 -vertex n -edge Path-like for set ;

existence
ex b₁ being _Graph st
( b₁ is n + 1 -vertex & b₁ is n -edge & b₁ is Path-like )

proof end;

end;

registration

let n be non zero Nat;

cluster Relation-like omega -defined Function-like finite [Graph-like] n -vertex non 0 -vertex n -' 1 -edge Path-like for set ;

existence
ex b₁ being _Graph st
( b₁ is n -vertex & b₁ is n -' 1 -edge & b₁ is Path-like )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] non _trivial non 0 -vertex n + 1 -vertex n -edge Path-like for set ;

existence
ex b₁ being _Graph st
( b₁ is n + 1 -vertex & b₁ is n -edge & b₁ is Path-like & not b₁ is _trivial )

proof end;

end;

registration

let P be Path-like _Graph;

cluster connected -> Path-like for Subgraph of P;

coherence
for b₁ being Subgraph of P st b₁ is connected holds
b₁ is Path-like

proof end;

end;

theorem :: GLPACY00:12

for G2 being _Graph
for v1, e, v2 being object
for G1 being addAdjVertex of G2,v1,e,v2 st G1 is Path-like holds
G2 is Path-like

proof end;

:: removing an endvertex from a path results in a path

theorem Th21: :: GLPACY00:13

for P1 being Path-like _Graph
for v being Vertex of P1
for P2 being removeVertex of P1,v st ( v is endvertex or P1 is _trivial ) holds
P2 is Path-like

proof end;

Lm4: for p being non empty FinSequence
for x being object
for n being Nat holds
( not n <= (len (p ^ <*x*>)) - 1 or n = (len (p ^ <*x*>)) - 1 or n <= (len p) - 1 )

proof end;

:: mostly copied from GLIB_008

theorem Th22: :: GLPACY00:14

for G being _finite Path-like _Graph
for H being connected Subgraph of G ex p being non empty Graph-yielding _finite Path-like FinSequence st
( p . 1 == H & p . (len p) = G & len p = ((G .order()) - (H .order())) + 1 & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & not v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v1 in Endvertices (p . n) ) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) & ( not p . n is _trivial implies v2 in Endvertices (p . n) ) ) ) ) ) )

proof end;

:: finite paths can be finitely constructed by adding
:: a vertex incident with an endvertex at a time

theorem Th23: :: GLPACY00:15

for G being _finite Path-like _Graph ex p being non empty Graph-yielding _finite Path-like FinSequence st
( p . 1 is _trivial & p . 1 is edgeless & p . (len p) = G & len p = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in the_Vertices_of (p . n) & ( n >= 2 implies v1 in Endvertices (p . n) ) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in the_Vertices_of (p . n) & ( n >= 2 implies v2 in Endvertices (p . n) ) ) ) ) ) )

proof end;

theorem :: GLPACY00:16

for p being non empty Graph-yielding FinSequence st p . 1 is Path-like & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, e, v2 being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & ( p . n is _trivial or v1 in Endvertices (p . n) or v2 in Endvertices (p . n) ) ) ) holds
p . (len p) is Path-like

proof end;

:: version with K_1 skipped

theorem Th25: :: GLPACY00:17

for G being _finite non _trivial Path-like _Graph ex p being non empty Graph-yielding _finite Path-like FinSequence st
( p . 1 is 2 -vertex & p . 1 is Path-like & p . (len p) = G & (len p) + 1 = G .order() & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, v2 being Vertex of G ex e being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & e in (the_Edges_of G) \ (the_Edges_of (p . n)) & ( ( v1 in Endvertices (p . n) & not v2 in the_Vertices_of (p . n) ) or ( not v1 in the_Vertices_of (p . n) & v2 in Endvertices (p . n) ) ) ) ) )

proof end;

theorem :: GLPACY00:18

for p being non empty Graph-yielding FinSequence st not p . 1 is _trivial & p . 1 is Path-like & ( for n being Element of dom p st n <= (len p) - 1 holds
ex v1, e, v2 being object st
( p . (n + 1) is addAdjVertex of p . n,v1,e,v2 & ( v1 in Endvertices (p . n) or v2 in Endvertices (p . n) ) ) ) holds
p . (len p) is Path-like

proof end;

Lm5: for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism & G2 is Path-like holds
G1 is Path-like

proof end;

theorem Th27: :: GLPACY00:19

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is Path-like iff G2 is Path-like )

proof end;

theorem :: GLPACY00:20

for G1, G2 being _Graph st G1 == G2 & G1 is Path-like holds
G2 is Path-like by Lm3;

theorem :: GLPACY00:21

for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 is Path-like iff G2 is Path-like )

proof end;

registration

let P2 be 2 -vertex Path-like _Graph;

cluster -> endvertex for Element of the_Vertices_of P2;

coherence
for b₁ being Vertex of P2 holds b₁ is endvertex ;

end;

theorem Th30: :: GLPACY00:22

for P being _finite non _trivial Path-like _Graph holds P .minDegree() = 1

proof end;

Lm6: for P being Path-like _Graph st P .order() = 2 holds
Endvertices P = the_Vertices_of P

proof end;

theorem Th31: :: GLPACY00:23

for P being _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 )

proof end;

theorem Th32: :: GLPACY00:24

for n being non zero Nat
for P1, P2 being b₁ -vertex Path-like _Graph holds P2 is P1 -isomorphic

proof end;

theorem :: GLPACY00:25

for n being Nat
for P1, P2 being b₁ -edge Path-like _Graph holds P2 is P1 -isomorphic

proof end;

Lm7: for P being non _trivial Path-like _Graph holds
( ( P .order() = 2 implies P .maxDegree() = 1 ) & ( P .order() <> 2 implies P .maxDegree() = 2 ) )

proof end;

theorem :: GLPACY00:26

for P being non _trivial Path-like _Graph holds
( ( P .order() = 2 implies P .maxDegree() = 1 ) & ( P .maxDegree() = 1 implies P .order() = 2 ) & ( P .order() <> 2 implies P .maxDegree() = 2 ) & ( P .maxDegree() = 2 implies P .order() <> 2 ) ) by Lm7;

theorem Th35: :: GLPACY00:27

for P being non _trivial Path-like _Graph
for v being Vertex of P st not v is endvertex holds
v .degree() = 2

proof end;

theorem Th36: :: GLPACY00:28

for P being _finite non _trivial Path-like _Graph ex v1, v2 being Vertex of P st
( v1 <> v2 & Endvertices P = {v1,v2} )

proof end;

theorem Th37: :: GLPACY00:29

for P being _finite non _trivial Path-like _Graph holds card (Endvertices P) = 2

proof end;

theorem :: GLPACY00:30

for G being _finite non _trivial _Graph st G is acyclic & G .minDegree() = 1 & card (Endvertices G) = 2 holds
G is Path-like

proof end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] simple connected 2 -vertex -> Path-like for set ;

coherence
for b₁ being _Graph st b₁ is 2 -vertex & b₁ is simple & b₁ is connected holds
b₁ is Path-like

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] 2 -vertex Path-like -> complete for set ;

coherence
for b₁ being _Graph st b₁ is 2 -vertex & b₁ is Path-like holds
b₁ is complete by GLIB_000:26;

end;

registration

let n be Nat;

cluster Relation-like omega -defined Function-like finite [Graph-like] n + 3 -vertex Path-like -> non complete for set ;

coherence
for b₁ being _Graph st b₁ is n + 3 -vertex & b₁ is Path-like holds
not b₁ is complete ;

end;

:: this definition includes the 1- and 2-cycle

definition

let G be _Graph;

attr G is Cycle-like means :: GLPACY00:def 6
( G is connected & not G is acyclic & G is 2 -regular );

end;

:: deftheorem defines Cycle-like GLPACY00:def 6 :
for G being _Graph holds
( G is Cycle-like iff ( G is connected & not G is acyclic & G is 2 -regular ) );

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] non _trivial non 0 -vertex Cycle-like for set ;

existence
ex b₁ being _Graph st
( not b₁ is _trivial & b₁ is Cycle-like )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] connected non acyclic 2 -regular -> Cycle-like for set ;

coherence
for b₁ being _Graph st b₁ is connected & not b₁ is acyclic & b₁ is 2 -regular holds
b₁ is Cycle-like ;

cluster Relation-like omega -defined Function-like finite [Graph-like] Cycle-like -> connected non acyclic 2 -regular for set ;

coherence
for b₁ being _Graph st b₁ is Cycle-like holds
( b₁ is connected & not b₁ is acyclic & b₁ is 2 -regular ) ;

end;

theorem Th39: :: GLPACY00:31

for G being Cycle-like _Graph
for C being Circuit-like Walk of G holds
( C .vertices() = the_Vertices_of G & C .edges() = the_Edges_of G )

proof end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] Cycle-like -> _finite non edgeless with_max_degree for set ;

coherence
for b₁ being _Graph st b₁ is Cycle-like holds
( not b₁ is edgeless & b₁ is _finite & b₁ is with_max_degree )

proof end;

end;

theorem Th40: :: GLPACY00:32

for G being Cycle-like _Graph holds G .order() = G .size()

proof end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial non-Dmulti loopfull -> Cycle-like for set ;

coherence
for b₁ being _Graph st b₁ is _trivial & b₁ is non-Dmulti & b₁ is loopfull holds
b₁ is Cycle-like

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial Cycle-like -> non-multi loopfull for set ;

coherence
for b₁ being _Graph st b₁ is _trivial & b₁ is Cycle-like holds
( b₁ is non-multi & b₁ is loopfull )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] non _trivial Cycle-like -> loopless for set ;

coherence
for b₁ being _Graph st not b₁ is _trivial & b₁ is Cycle-like holds
b₁ is loopless

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] _trivial non 0 -vertex Cycle-like for set ;

existence
ex b₁ being _Graph st
( b₁ is _trivial & b₁ is Cycle-like )

proof end;

end;

definition

let F be Graph-yielding Function;

attr F is Cycle-like means :Def7: :: GLPACY00:def 7
for x being object st x in dom F holds
ex G being _Graph st
( F . x = G & G is Cycle-like );

end;

:: deftheorem Def7 defines Cycle-like GLPACY00:def 7 :
for F being Graph-yielding Function holds
( F is Cycle-like iff for x being object st x in dom F holds
ex G being _Graph st
( F . x = G & G is Cycle-like ) );

registration

let C be Cycle-like _Graph;

cluster <*C*> -> Cycle-like ;

coherence
<*C*> is Cycle-like

proof end;

cluster NAT --> C -> Cycle-like ;

coherence
NAT --> C is Cycle-like by FUNCOP_1:7;

end;

definition

let F be non empty Graph-yielding Function;

redefine attr F is Cycle-like means :Def8: :: GLPACY00:def 8
for x being Element of dom F holds F . x is Cycle-like ;

compatibility
( F is Cycle-like iff for x being Element of dom F holds F . x is Cycle-like )

proof end;

end;

:: deftheorem Def8 defines Cycle-like GLPACY00:def 8 :
for F being non empty Graph-yielding Function holds
( F is Cycle-like iff for x being Element of dom F holds F . x is Cycle-like );

definition

let S be GraphSeq;

redefine attr S is Cycle-like means :Def9: :: GLPACY00:def 9
for n being Nat holds S . n is Cycle-like ;

compatibility
( S is Cycle-like iff for n being Nat holds S . n is Cycle-like )

proof end;

end;

:: deftheorem Def9 defines Cycle-like GLPACY00:def 9 :
for S being GraphSeq holds
( S is Cycle-like iff for n being Nat holds S . n is Cycle-like );

registration

cluster empty Relation-like Function-like Graph-yielding -> Graph-yielding Cycle-like for set ;

coherence
for b₁ being Graph-yielding Function st b₁ is empty holds
b₁ is Cycle-like ;

cluster Relation-like Function-like Graph-yielding _trivial non-Dmulti loopfull -> Graph-yielding Cycle-like for set ;

coherence
for b₁ being Graph-yielding Function st b₁ is _trivial & b₁ is non-Dmulti & b₁ is loopfull holds
b₁ is Cycle-like

proof end;

cluster Relation-like Function-like Graph-yielding Cycle-like -> Graph-yielding connected for set ;

coherence
for b₁ being Graph-yielding Function st b₁ is Cycle-like holds
b₁ is connected

proof end;

cluster non empty Relation-like omega -defined Function-like total Graph-yielding Cycle-like for set ;

existence
ex b₁ being GraphSeq st
( not b₁ is empty & b₁ is Cycle-like )

proof end;

end;

registration

let F be non empty Graph-yielding Cycle-like Function;
let x be Element of dom F;

cluster F . x -> Cycle-like ;

coherence
F . x is Cycle-like by Def8;

end;

registration

let S be Cycle-like GraphSeq;
let n be Nat;

cluster S . n -> Cycle-like ;

coherence
S . n is Cycle-like by Def9;

end;

registration

let p be Graph-yielding Cycle-like FinSequence;
let n be Nat;

cluster p | n -> Cycle-like ;

coherence
p | n is Cycle-like

proof end;

cluster p /^ n -> Cycle-like ;

coherence
p /^ n is Cycle-like

proof end;

let m be Nat;

cluster smid (p,m,n) -> Cycle-like ;

coherence
smid (p,m,n) is Cycle-like

proof end;

cluster (m,n) -cut p -> Cycle-like ;

coherence
(m,n) -cut p is Cycle-like

proof end;

end;

registration

let p, q be Graph-yielding Cycle-like FinSequence;

cluster p ^ q -> Cycle-like ;

coherence
p ^ q is Cycle-like

proof end;

cluster p ^' q -> Cycle-like ;

coherence
p ^' q is Cycle-like

proof end;

end;

registration

let C1, C2 be Cycle-like _Graph;

cluster <*C1,C2*> -> Cycle-like ;

coherence
<*C1,C2*> is Cycle-like

proof end;

let C3 be Cycle-like _Graph;

cluster <*C1,C2,C3*> -> Cycle-like ;

coherence
<*C1,C2,C3*> is Cycle-like

proof end;

end;

definition

let S be Graph-membered set ;

attr S is Cycle-like means :Def10: :: GLPACY00:def 10
for G being _Graph st G in S holds
G is Cycle-like ;

end;

:: deftheorem Def10 defines Cycle-like GLPACY00:def 10 :
for S being Graph-membered set holds
( S is Cycle-like iff for G being _Graph st G in S holds
G is Cycle-like );

registration

cluster empty Graph-membered -> Graph-membered Cycle-like for set ;

coherence
for b₁ being Graph-membered set st b₁ is empty holds
b₁ is Cycle-like ;

cluster Graph-membered Cycle-like -> Graph-membered connected for set ;

coherence
for b₁ being Graph-membered set st b₁ is Cycle-like holds
b₁ is connected

proof end;

end;

registration

let C1 be Cycle-like _Graph;

cluster {C1} -> Cycle-like ;

coherence
{C1} is Cycle-like by TARSKI:def 1;
let C2 be Cycle-like _Graph;

cluster {C1,C2} -> Cycle-like ;

coherence
{C1,C2} is Cycle-like

proof end;

end;

registration

let F be Graph-yielding Cycle-like Function;

cluster rng F -> Cycle-like ;

coherence
rng F is Cycle-like

proof end;

end;

registration

let X be Graph-membered Cycle-like set ;

cluster -> Cycle-like for Element of K32(X);

coherence
for b₁ being Subset of X holds b₁ is Cycle-like by Def10;

end;

registration

let X be Graph-membered Cycle-like set ;
let Y be set ;

cluster X /\ Y -> Cycle-like ;

coherence
X /\ Y is Cycle-like

proof end;

cluster X \ Y -> Cycle-like ;

coherence
X \ Y is Cycle-like ;

end;

registration

let X, Y be Graph-membered Cycle-like set ;

cluster X \/ Y -> Cycle-like ;

coherence
X \/ Y is Cycle-like

proof end;

cluster X \+\ Y -> Cycle-like ;

coherence
X \+\ Y is Cycle-like ;

end;

registration

cluster non empty Graph-membered Cycle-like for set ;

existence
ex b₁ being Graph-membered set st
( not b₁ is empty & b₁ is Cycle-like )

proof end;

end;

registration

let S be non empty Graph-membered Cycle-like set ;

cluster -> Cycle-like for Element of S;

coherence
for b₁ being Element of S holds b₁ is Cycle-like by Def10;

end;

:: this was essentially proven above with the registrations:
:: the 1-cycle is the trivial graph with a loop Part I

theorem Th41: :: GLPACY00:33

for G2 being _trivial edgeless _Graph
for v being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,v holds G1 is Cycle-like

proof end;

:: connecting endvertices of path graphs creates cycle graphs

theorem Th42: :: GLPACY00:34

for P being _finite non _trivial Path-like _Graph
for v1, v2 being Element of Endvertices P
for e being object
for C being addEdge of P,v1,e,v2 st v1 <> v2 & not e in the_Edges_of P holds
C is Cycle-like

proof end;

:: removing an edge from a cycle results in a path graph

theorem Th43: :: GLPACY00:35

for C being Cycle-like _Graph
for e being Edge of C
for P being removeEdge of C,e holds
( P is _finite & P is Path-like )

proof end;

registration

let C be Cycle-like _Graph;
let e be Edge of C;

cluster -> _finite Path-like for inducedSubgraph of C, the_Vertices_of C,(the_Edges_of C) \ {e};

coherence
for b₁ being removeEdge of C,e holds
( b₁ is _finite & b₁ is Path-like ) by Th43;

end;

:: the 1-cycle is the trivial graph with a loop Part II
:: actually already done with previous cluster
:: theorem
:: for G1 being _trivial Cycle-like _Graph, e being Edge of G1
:: for G2 being removeEdge of G1,e holds G2 is _trivial edgeless;
:: the 1-cycle is the trivial graph with a loop Part III

theorem :: GLPACY00:36

for G1 being _trivial Cycle-like _Graph
for v being Vertex of G1
for e being Edge of G1 ex G2 being _trivial edgeless _Graph st G1 is addEdge of G2,v,e,v

proof end;

:: all other cycles can be constructed from finite paths
:: by connecting the endvertices

theorem Th45: :: GLPACY00:37

for C being non _trivial Cycle-like _Graph
for v1, v2 being Vertex of C
for e being Edge of C st e DJoins v1,v2,C holds
ex P being _finite non _trivial Path-like _Graph st
( not e in the_Edges_of P & C is addEdge of P,v1,e,v2 & Endvertices P = {v1,v2} )

proof end;

theorem :: GLPACY00:38

for C being Cycle-like _Graph holds
( C .order() = 2 iff not C is non-multi )

proof end;

registration

let n be Nat;

cluster Relation-like omega -defined Function-like finite [Graph-like] n -vertex Cycle-like -> n -edge for set ;

coherence
for b₁ being _Graph st b₁ is n -vertex & b₁ is Cycle-like holds
b₁ is n -edge

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] n -edge Cycle-like -> n -vertex for set ;

coherence
for b₁ being _Graph st b₁ is n -edge & b₁ is Cycle-like holds
b₁ is n -vertex

proof end;

end;

registration

let n be Nat;

cluster Relation-like omega -defined Function-like finite [Graph-like] non 0 -vertex n + 1 -vertex n + 1 -edge Cycle-like for set ;

existence
ex b₁ being _Graph st
( b₁ is n + 1 -vertex & b₁ is n + 1 -edge & b₁ is Cycle-like )

proof end;

end;

registration

let n be Nat;

cluster Relation-like omega -defined Function-like finite [Graph-like] n + 2 -vertex Cycle-like -> loopless for set ;

coherence
for b₁ being _Graph st b₁ is n + 2 -vertex & b₁ is Cycle-like holds
b₁ is loopless

proof end;

end;

registration

let n be Nat;

cluster Relation-like omega -defined Function-like finite [Graph-like] n + 3 -vertex Cycle-like -> simple for set ;

coherence
for b₁ being _Graph st b₁ is n + 3 -vertex & b₁ is Cycle-like holds
b₁ is simple

proof end;

end;

registration

let n be Nat;

cluster Relation-like omega -defined Function-like finite [Graph-like] loopless non 0 -vertex n + 2 -vertex n + 2 -edge Cycle-like for set ;

existence
ex b₁ being _Graph st
( b₁ is n + 2 -vertex & b₁ is n + 2 -edge & b₁ is loopless & b₁ is Cycle-like )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] simple non 0 -vertex n + 3 -vertex n + 3 -edge Cycle-like for set ;

existence
ex b₁ being _Graph st
( b₁ is n + 3 -vertex & b₁ is n + 3 -edge & b₁ is simple & b₁ is Cycle-like )

proof end;

end;

registration

let n be non zero Nat;
reconsider m = n - 1 as Nat by CHORD:1;

cluster Relation-like omega -defined Function-like finite [Graph-like] n -vertex non 0 -vertex n -edge Cycle-like for set ;

existence
ex b₁ being _Graph st
( b₁ is n -vertex & b₁ is n -edge & b₁ is Cycle-like )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] n + 1 -vertex Cycle-like -> loopless for set ;

coherence
for b₁ being _Graph st b₁ is n + 1 -vertex & b₁ is Cycle-like holds
b₁ is loopless

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] n + 2 -vertex Cycle-like -> simple for set ;

coherence
for b₁ being _Graph st b₁ is n + 2 -vertex & b₁ is Cycle-like holds
b₁ is simple

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] loopless non 0 -vertex n + 1 -vertex n + 1 -edge Cycle-like for set ;

existence
ex b₁ being _Graph st
( b₁ is n + 1 -vertex & b₁ is n + 1 -edge & b₁ is Cycle-like & b₁ is loopless )

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] simple non 0 -vertex n + 2 -vertex n + 2 -edge Cycle-like for set ;

existence
ex b₁ being _Graph st
( b₁ is n + 2 -vertex & b₁ is n + 2 -edge & b₁ is Cycle-like & b₁ is simple )

proof end;

end;

theorem :: GLPACY00:39

for C1 being Cycle-like _Graph
for C2 being non acyclic Subgraph of C1 holds C1 == C2

proof end;

theorem Th48: :: GLPACY00:40

for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is Cycle-like iff G2 is Cycle-like ) by GLIB_010:140, GLIB_016:30;

theorem :: GLPACY00:41

for G1, G2 being _Graph st G1 == G2 & G1 is Cycle-like holds
G2 is Cycle-like

proof end;

theorem :: GLPACY00:42

for G1 being _Graph
for E being set
for G2 being reverseEdgeDirections of G1,E holds
( G1 is Cycle-like iff G2 is Cycle-like )

proof end;

Lm8: for G2 being _Graph
for v, e, w being object
for G1 being addEdge of G2,v,e,w holds the_Vertices_of G1 = the_Vertices_of G2

proof end;

theorem Th51: :: GLPACY00:43

for n being non zero Nat
for C1, C2 being b₁ -vertex Cycle-like _Graph holds C2 is C1 -isomorphic

proof end;

theorem :: GLPACY00:44

for n being non zero Nat
for C1, C2 being b₁ -edge Cycle-like _Graph holds C2 is C1 -isomorphic by Th51;

theorem :: GLPACY00:45

for P being _finite non _trivial Path-like _Graph
for v being object
for C being addAdjVertexAll of P,v, Endvertices P st not v in the_Vertices_of P holds
( C is simple & C is Cycle-like )

proof end;

theorem Th54: :: GLPACY00:46

for C being non _trivial Cycle-like _Graph
for v being Vertex of C
for P being removeVertex of C,v holds
( P is _finite & P is Path-like )

proof end;

theorem :: GLPACY00:47

for C being simple Cycle-like _Graph
for v being Vertex of C ex P being non _trivial Path-like _Graph st
( not v in the_Vertices_of P & C is addAdjVertexAll of P,v, Endvertices P )

proof end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] simple complete 3 -vertex -> Cycle-like for set ;

coherence
for b₁ being _Graph st b₁ is 3 -vertex & b₁ is simple & b₁ is complete holds
b₁ is Cycle-like

proof end;

cluster Relation-like omega -defined Function-like finite [Graph-like] 3 -vertex Cycle-like -> simple complete chordal for set ;

coherence
for b₁ being _Graph st b₁ is 3 -vertex & b₁ is Cycle-like holds
( b₁ is simple & b₁ is complete & b₁ is chordal )

proof end;

end;

registration

let n be Nat;

cluster Relation-like omega -defined Function-like finite [Graph-like] n + 4 -vertex Cycle-like -> non complete non chordal for set ;

coherence
for b₁ being _Graph st b₁ is n + 4 -vertex & b₁ is Cycle-like holds
( not b₁ is chordal & not b₁ is complete )

proof end;

end;

registration

let n be non zero Nat;
reconsider m = n - 1 as Nat by CHORD:1;

cluster Relation-like omega -defined Function-like finite [Graph-like] n + 3 -vertex Cycle-like -> non complete non chordal for set ;

coherence
for b₁ being _Graph st b₁ is n + 3 -vertex & b₁ is Cycle-like holds
( not b₁ is chordal & not b₁ is complete )

proof end;

end;

registration

cluster Relation-like omega -defined Function-like finite [Graph-like] non complete non chordal non 0 -vertex Cycle-like for set ;

existence
ex b₁ being _Graph st
( b₁ is Cycle-like & not b₁ is complete & not b₁ is chordal )

proof end;

end;