:: GLIB_001 semantic presentation

theorem Th1: :: GLIB_001:1

for b₁, b₂ being odd Nat holds
( b₁ < b₂ iff b₁ + 2 <= b₂ )

proof end;

Lemma2: for b₁, b₂, b₃ being real number st 0 < b₃ & b₁ * b₃ <= b₂ * b₃ holds
b₁ <= b₂
by XREAL_1:70;

Lemma3: for b₁ being finite Function holds card (dom b₁) = card b₁
by PRE_CIRC:21;

theorem Th2: :: GLIB_001:2

for b₁ being set
for b₂ being Nat st b₁ c= Seg b₂ holds
for b₃, b₄ being Nat st b₃ in dom (Sgm b₁) & b₄ = (Sgm b₁) . b₃ holds
b₃ <= b₄

proof end;

theorem Th3: :: GLIB_001:3

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being FinSubsequence of b₂ holds len (Seq b₃) <= len b₂

proof end;

theorem Th4: :: GLIB_001:4

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being FinSubsequence of b₂
for b₄ being Nat st b₄ in dom (Seq b₃) holds
ex b₅ being Nat st
( b₅ in dom b₂ & b₄ <= b₅ & (Seq b₃) . b₄ = b₂ . b₅ )

proof end;

theorem Th5: :: GLIB_001:5

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being FinSubsequence of b₂ holds len (Seq b₃) = card b₃

proof end;

theorem Th6: :: GLIB_001:6

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being FinSubsequence of b₂ holds dom (Seq b₃) = dom (Sgm (dom b₃))

proof end;

definition

let c₁ be _Graph;
mode VertexSeq of c₁ -> FinSequence of the_Vertices_of a₁ means :Def1: :: GLIB_001:def 1
for b₁ being Nat st 1 <= b₁ & b₁ < len a₂ holds
ex b₂ being set st b₂ Joins a₂ . b₁,a₂ . (b₁ + 1),a₁;
existence

proof end;

end;

:: deftheorem Def1 defines VertexSeq GLIB_001:def 1 :

definition

let c₁ be _Graph;
mode EdgeSeq of c₁ -> FinSequence of the_Edges_of a₁ means :Def2: :: GLIB_001:def 2
ex b₁ being FinSequence of the_Vertices_of a₁ st
( len b₁ = (len a₂) + 1 & ( for b₂ being Nat st 1 <= b₂ & b₂ <= len a₂ holds
a₂ . b₂ Joins b₁ . b₂,b₁ . (b₂ + 1),a₁ ) );
existence

proof end;

end;

:: deftheorem Def2 defines EdgeSeq GLIB_001:def 2 :

definition

let c₁ be _Graph;
mode Walk of c₁ -> FinSequence of (the_Vertices_of a₁) \/ (the_Edges_of a₁) means :Def3: :: GLIB_001:def 3
( not len a₂ is even & a₂ . 1 in the_Vertices_of a₁ & ( for b₁ being odd Nat st b₁ < len a₂ holds
a₂ . (b₁ + 1) Joins a₂ . b₁,a₂ . (b₁ + 2),a₁ ) );
existence

proof end;

end;

:: deftheorem Def3 defines Walk GLIB_001:def 3 :

registration

let c₁ be _Graph;
let c₂ be Walk of c₁;
cluster len a₂ -> non empty odd ;
correctness

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be Vertex of c₁;
func c₁ .walkOf c₂ -> Walk of a₁ equals :: GLIB_001:def 4
<*a₂*>;
coherence

proof end;

end;

:: deftheorem Def4 defines .walkOf GLIB_001:def 4 :

definition

let c₁ be _Graph;
let c₂, c₃, c₄ be set ;
func c₁ .walkOf c₂,c₄,c₃ -> Walk of a₁ equals :Def5: :: GLIB_001:def 5
<*a₂,a₄,a₃*> if a₄ Joins a₂,a₃,a₁
otherwise a₁ .walkOf (choose (the_Vertices_of a₁));
coherence

proof end;

consistency ;

end;

:: deftheorem Def5 defines .walkOf GLIB_001:def 5 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
func c₂ .first() -> Vertex of a₁ equals :: GLIB_001:def 6
a₂ . 1;
coherence by Def3;
func c₂ .last() -> Vertex of a₁ equals :: GLIB_001:def 7
a₂ . (len a₂);
coherence

proof end;

end;

:: deftheorem Def6 defines .first() GLIB_001:def 6 :

:: deftheorem Def7 defines .last() GLIB_001:def 7 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
let c₃ be Nat;
func c₂ .vertexAt c₃ -> Vertex of a₁ equals :Def8: :: GLIB_001:def 8
a₂ . a₃ if ( not a₃ is even & a₃ <= len a₂ )
otherwise a₂ .first() ;
correctness

proof end;

end;

:: deftheorem Def8 defines .vertexAt GLIB_001:def 8 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
func c₂ .reverse() -> Walk of a₁ equals :: GLIB_001:def 9
Rev a₂;
coherence

proof end;

end;

:: deftheorem Def9 defines .reverse() GLIB_001:def 9 :

definition

let c₁ be _Graph;
let c₂, c₃ be Walk of c₁;
func c₂ .append c₃ -> Walk of a₁ equals :Def10: :: GLIB_001:def 10
a₂ ^' a₃ if a₂ .last() = a₃ .first()
otherwise a₂;
correctness

proof end;

end;

:: deftheorem Def10 defines .append GLIB_001:def 10 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
let c₃, c₄ be Nat;
func c₂ .cut c₃,c₄ -> Walk of a₁ equals :Def11: :: GLIB_001:def 11
a₃,a₄ -cut a₂ if ( not a₃ is even & not a₄ is even & a₃ <= a₄ & a₄ <= len a₂ )
otherwise a₂;
correctness

proof end;

end;

:: deftheorem Def11 defines .cut GLIB_001:def 11 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
let c₃, c₄ be Nat;
func c₂ .remove c₃,c₄ -> Walk of a₁ equals :Def12: :: GLIB_001:def 12
(a₂ .cut 1,a₃) .append (a₂ .cut a₄,(len a₂)) if ( not a₃ is even & not a₄ is even & a₃ <= a₄ & a₄ <= len a₂ & a₂ . a₃ = a₂ . a₄ )
otherwise a₂;
correctness ;

end;

:: deftheorem Def12 defines .remove GLIB_001:def 12 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
let c₃ be set ;
func c₂ .addEdge c₃ -> Walk of a₁ equals :: GLIB_001:def 13
a₂ .append (a₁ .walkOf (a₂ .last() ),a₃,((a₂ .last() ) .adj a₃));
coherence ;

end;

:: deftheorem Def13 defines .addEdge GLIB_001:def 13 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
func c₂ .vertexSeq() -> VertexSeq of a₁ means :Def14: :: GLIB_001:def 14
( (len a₂) + 1 = 2 * (len a₃) & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₃ holds
a₃ . b₁ = a₂ . ((2 * b₁) - 1) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines .vertexSeq() GLIB_001:def 14 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
func c₂ .edgeSeq() -> EdgeSeq of a₁ means :Def15: :: GLIB_001:def 15
( len a₂ = (2 * (len a₃)) + 1 & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₃ holds
a₃ . b₁ = a₂ . (2 * b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines .edgeSeq() GLIB_001:def 15 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
func c₂ .vertices() -> finite Subset of (the_Vertices_of a₁) equals :: GLIB_001:def 16
rng (a₂ .vertexSeq() );
coherence ;

end;

:: deftheorem Def16 defines .vertices() GLIB_001:def 16 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
func c₂ .edges() -> finite Subset of (the_Edges_of a₁) equals :: GLIB_001:def 17
rng (a₂ .edgeSeq() );
coherence ;

end;

:: deftheorem Def17 defines .edges() GLIB_001:def 17 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
func c₂ .length() -> Nat equals :: GLIB_001:def 18
len (a₂ .edgeSeq() );
coherence ;

end;

:: deftheorem Def18 defines .length() GLIB_001:def 18 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
let c₃ be set ;
func c₂ .find c₃ -> odd Nat means :Def19: :: GLIB_001:def 19
( a₄ <= len a₂ & a₂ . a₄ = a₃ & ( for b₁ being odd Nat st b₁ <= len a₂ & a₂ . b₁ = a₃ holds
a₄ <= b₁ ) ) if a₃ in a₂ .vertices()
otherwise a₄ = len a₂;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def19 defines .find GLIB_001:def 19 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
let c₃ be Nat;
func c₂ .find c₃ -> odd Nat means :Def20: :: GLIB_001:def 20
( a₄ <= len a₂ & a₂ . a₄ = a₂ . a₃ & ( for b₁ being odd Nat st b₁ <= len a₂ & a₂ . b₁ = a₂ . a₃ holds
a₄ <= b₁ ) ) if ( not a₃ is even & a₃ <= len a₂ )
otherwise a₄ = len a₂;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def20 defines .find GLIB_001:def 20 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
let c₃ be set ;
func c₂ .rfind c₃ -> odd Nat means :Def21: :: GLIB_001:def 21
( a₄ <= len a₂ & a₂ . a₄ = a₃ & ( for b₁ being odd Nat st b₁ <= len a₂ & a₂ . b₁ = a₃ holds
b₁ <= a₄ ) ) if a₃ in a₂ .vertices()
otherwise a₄ = len a₂;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def21 defines .rfind GLIB_001:def 21 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
let c₃ be Nat;
func c₂ .rfind c₃ -> odd Nat means :Def22: :: GLIB_001:def 22
( a₄ <= len a₂ & a₂ . a₄ = a₂ . a₃ & ( for b₁ being odd Nat st b₁ <= len a₂ & a₂ . b₁ = a₂ . a₃ holds
b₁ <= a₄ ) ) if ( not a₃ is even & a₃ <= len a₂ )
otherwise a₄ = len a₂;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

:: deftheorem Def22 defines .rfind GLIB_001:def 22 :

definition

let c₁ be _Graph;
let c₂, c₃ be set ;
let c₄ be Walk of c₁;
pred c₄ is_Walk_from c₂,c₃ means :Def23: :: GLIB_001:def 23
( a₄ .first() = a₂ & a₄ .last() = a₃ );

end;

:: deftheorem Def23 defines is_Walk_from GLIB_001:def 23 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
attr a₂ is closed means :Def24: :: GLIB_001:def 24
a₂ .first() = a₂ .last() ;
attr a₂ is directed means :Def25: :: GLIB_001:def 25
for b₁ being odd Nat st b₁ < len a₂ holds
(the_Source_of a₁) . (a₂ . (b₁ + 1)) = a₂ . b₁;
attr a₂ is trivial means :Def26: :: GLIB_001:def 26
a₂ .length() = 0;
attr a₂ is Trail-like means :Def27: :: GLIB_001:def 27
a₂ .edgeSeq() is one-to-one;

end;

:: deftheorem Def24 defines closed GLIB_001:def 24 :

:: deftheorem Def25 defines directed GLIB_001:def 25 :

:: deftheorem Def26 defines trivial GLIB_001:def 26 :

:: deftheorem Def27 defines Trail-like GLIB_001:def 27 :

notation

let c₁ be _Graph;
let c₂ be Walk of c₁;
antonym open c₂ for closed c₂;

end;

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
attr a₂ is Path-like means :Def28: :: GLIB_001:def 28
( a₂ is Trail-like & ( for b₁, b₂ being odd Nat st b₁ < b₂ & b₂ <= len a₂ & a₂ . b₁ = a₂ . b₂ holds
( b₁ = 1 & b₂ = len a₂ ) ) );

end;

:: deftheorem Def28 defines Path-like GLIB_001:def 28 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
attr a₂ is vertex-distinct means :Def29: :: GLIB_001:def 29
for b₁, b₂ being odd Nat st b₁ <= len a₂ & b₂ <= len a₂ & a₂ . b₁ = a₂ . b₂ holds
b₁ = b₂;

end;

:: deftheorem Def29 defines vertex-distinct GLIB_001:def 29 :

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
attr a₂ is Circuit-like means :Def30: :: GLIB_001:def 30
( a₂ is closed & a₂ is Trail-like & not a₂ is trivial );
attr a₂ is Cycle-like means :Def31: :: GLIB_001:def 31
( a₂ is closed & a₂ is Path-like & not a₂ is trivial );

end;

:: deftheorem Def30 defines Circuit-like GLIB_001:def 30 :

:: deftheorem Def31 defines Cycle-like GLIB_001:def 31 :

Lemma32: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
b₂ . b₃ in the_Vertices_of b₁

proof end;

Lemma33: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being even Nat st b₃ in dom b₂ holds
ex b₄ being odd Nat st
( b₄ = b₃ - 1 & b₃ - 1 in dom b₂ & b₃ + 1 in dom b₂ & b₂ . b₃ Joins b₂ . b₄,b₂ . (b₃ + 1),b₁ )

proof end;

Lemma34: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ < len b₂ holds
( b₃ in dom b₂ & b₃ + 1 in dom b₂ & b₃ + 2 in dom b₂ )

proof end;

Lemma35: for b₁ being _Graph
for b₂ being Vertex of b₁ holds
( b₁ .walkOf b₂ is closed & b₁ .walkOf b₂ is directed & b₁ .walkOf b₂ is trivial & b₁ .walkOf b₂ is Trail-like & b₁ .walkOf b₂ is Path-like )

proof end;

Lemma36: for b₁ being _Graph
for b₂, b₃, b₄ being set st b₃ Joins b₂,b₄,b₁ holds
len (b₁ .walkOf b₂,b₃,b₄) = 3

proof end;

Lemma37: for b₁ being _Graph
for b₂, b₃, b₄ being set st b₃ Joins b₂,b₄,b₁ holds
( (b₁ .walkOf b₂,b₃,b₄) .first() = b₂ & (b₁ .walkOf b₂,b₃,b₄) .last() = b₄ & b₁ .walkOf b₂,b₃,b₄ is_Walk_from b₂,b₄ )

proof end;

Lemma38: for b₁ being _Graph
for b₂ being Walk of b₁ holds
( len b₂ = len (b₂ .reverse() ) & dom b₂ = dom (b₂ .reverse() ) & rng b₂ = rng (b₂ .reverse() ) )
by FINSEQ_5:def 3, FINSEQ_5:60;

Lemma39: for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ .first() = (b₂ .reverse() ) .last() & b₂ .last() = (b₂ .reverse() ) .first() )

proof end;

Lemma40: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat st b₃ in dom (b₂ .reverse() ) holds
( (b₂ .reverse() ) . b₃ = b₂ . (((len b₂) - b₃) + 1) & ((len b₂) - b₃) + 1 in dom b₂ )

proof end;

Lemma41: for b₁ being _Graph
for b₂ being Walk of b₁ holds (b₂ .reverse() ) .reverse() = b₂
by FINSEQ_6:29;

Lemma42: for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
(len (b₂ .append b₃)) + 1 = (len b₂) + (len b₃)

proof end;

Lemma43: for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
( len b₂ <= len (b₂ .append b₃) & len b₃ <= len (b₂ .append b₃) )

proof end;

Lemma44: for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
( (b₂ .append b₃) .first() = b₂ .first() & (b₂ .append b₃) .last() = b₃ .last() & b₂ .append b₃ is_Walk_from b₂ .first() ,b₃ .last() )

proof end;

Lemma45: for b₁ being _Graph
for b₂, b₃ being Walk of b₁
for b₄ being Nat st b₄ in dom b₂ holds
( (b₂ .append b₃) . b₄ = b₂ . b₄ & b₄ in dom (b₂ .append b₃) )

proof end;

Lemma46: for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
for b₄ being Nat st b₄ < len b₃ holds
( (b₂ .append b₃) . ((len b₂) + b₄) = b₃ . (b₄ + 1) & (len b₂) + b₄ in dom (b₂ .append b₃) )

proof end;

Lemma47: for b₁ being _Graph
for b₂, b₃ being Walk of b₁
for b₄ being Nat holds
( not b₄ in dom (b₂ .append b₃) or b₄ in dom b₂ or ex b₅ being Nat st
( b₅ < len b₃ & b₄ = (len b₂) + b₅ ) )

proof end;

Lemma48: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ holds
( (len (b₂ .cut b₃,b₄)) + b₃ = b₄ + 1 & ( for b₅ being Nat st b₅ < len (b₂ .cut b₃,b₄) holds
( (b₂ .cut b₃,b₄) . (b₅ + 1) = b₂ . (b₃ + b₅) & b₃ + b₅ in dom b₂ ) ) )

proof end;

Lemma49: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ holds
( (b₂ .cut b₃,b₄) .first() = b₂ . b₃ & (b₂ .cut b₃,b₄) .last() = b₂ . b₄ & b₂ .cut b₃,b₄ is_Walk_from b₂ . b₃,b₂ . b₄ )

proof end;

Lemma50: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄, b₅ being odd Nat st b₃ <= b₄ & b₄ <= b₅ & b₅ <= len b₂ holds
(b₂ .cut b₃,b₄) .append (b₂ .cut b₄,b₅) = b₂ .cut b₃,b₅

proof end;

Lemma51: for b₁ being _Graph
for b₂ being Walk of b₁ holds b₂ .cut 1,(len b₂) = b₂

proof end;

Lemma52: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
b₂ .cut b₃,b₃ = <*(b₂ .vertexAt b₃)*>

proof end;

Lemma53: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being Nat st not b₃ is even & b₃ <= b₄ holds
(b₂ .cut 1,b₄) .cut 1,b₃ = b₂ .cut 1,b₃

proof end;

Lemma54: for b₁ being _Graph
for b₂, b₃ being Walk of b₁
for b₄, b₅ being odd Nat st b₄ <= b₅ & b₅ <= len b₂ & b₂ .last() = b₃ .first() holds
(b₂ .append b₃) .cut b₄,b₅ = b₂ .cut b₄,b₅

proof end;

Lemma55: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
len (b₂ .cut 1,b₃) = b₃

proof end;

Lemma56: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat
for b₄ being Nat st b₄ in dom (b₂ .cut 1,b₃) & b₃ <= len b₂ holds
(b₂ .cut 1,b₃) . b₄ = b₂ . b₄

proof end;

Lemma57: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ holds
(len (b₂ .remove b₃,b₄)) + b₄ = (len b₂) + b₃

proof end;

Lemma58: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being Nat
for b₅, b₆ being set st b₂ is_Walk_from b₅,b₆ holds
b₂ .remove b₃,b₄ is_Walk_from b₅,b₆

proof end;

Lemma59: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being Nat holds len (b₂ .remove b₃,b₄) <= len b₂

proof end;

Lemma60: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat holds b₂ .remove b₃,b₃ = b₂

proof end;

Lemma61: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ holds
(b₂ .cut 1,b₃) .last() = (b₂ .cut b₄,(len b₂)) .first()

proof end;

Lemma62: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set
for b₅, b₆ being odd Nat st b₅ <= b₆ & b₆ <= len b₂ & b₂ . b₅ = b₂ . b₆ holds
for b₇ being Nat st b₇ in Seg b₅ holds
(b₂ .remove b₅,b₆) . b₇ = b₂ . b₇

proof end;

Lemma63: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ holds
for b₅ being Nat st b₃ <= b₅ & b₅ <= len (b₂ .remove b₃,b₄) holds
( (b₂ .remove b₃,b₄) . b₅ = b₂ . ((b₅ - b₃) + b₄) & (b₅ - b₃) + b₄ is Nat & (b₅ - b₃) + b₄ <= len b₂ )

proof end;

Lemma64: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ holds
len (b₂ .remove b₃,b₄) = ((len b₂) + b₃) - b₄

proof end;

Lemma65: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat st b₂ .first() = b₂ . b₃ holds
b₂ .remove 1,b₃ = b₂ .cut b₃,(len b₂)

proof end;

Lemma66: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being Nat holds
( (b₂ .remove b₃,b₄) .first() = b₂ .first() & (b₂ .remove b₃,b₄) .last() = b₂ .last() )

proof end;

Lemma67: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat
for b₅ being Nat st b₃ <= b₄ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ & b₅ in dom (b₂ .remove b₃,b₄) & not b₅ in Seg b₃ holds
( b₃ <= b₅ & b₅ <= len (b₂ .remove b₃,b₄) )

proof end;

Lemma68: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
b₂ .addEdge b₃ = b₂ ^ <*b₃,b₄*>

proof end;

Lemma69: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
( (b₂ .addEdge b₃) .first() = b₂ .first() & (b₂ .addEdge b₃) .last() = b₄ & b₂ .addEdge b₃ is_Walk_from b₂ .first() ,b₄ )

proof end;

Lemma70: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
len (b₂ .addEdge b₃) = (len b₂) + 2

proof end;

Lemma71: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
( (b₂ .addEdge b₃) . ((len b₂) + 1) = b₃ & (b₂ .addEdge b₃) . ((len b₂) + 2) = b₄ & ( for b₅ being Nat st b₅ in dom b₂ holds
(b₂ .addEdge b₃) . b₅ = b₂ . b₅ ) )

proof end;

Lemma72: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄, b₅, b₆ being set st b₂ is_Walk_from b₄,b₅ & b₃ Joins b₅,b₆,b₁ holds
b₂ .addEdge b₃ is_Walk_from b₄,b₆

proof end;

Lemma73: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being even Nat st 1 <= b₃ & b₃ <= len b₂ holds
( b₃ div 2 in dom (b₂ .edgeSeq() ) & b₂ . b₃ = (b₂ .edgeSeq() ) . (b₃ div 2) )

proof end;

Lemma74: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat holds
( b₃ in dom (b₂ .edgeSeq() ) iff 2 * b₃ in dom b₂ )

proof end;

Lemma75: for b₁ being _Graph
for b₂ being Walk of b₁ ex b₃ being even Nat st
( b₃ = (len b₂) - 1 & len (b₂ .edgeSeq() ) = b₃ div 2 )

proof end;

Lemma76: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat holds (b₂ .cut 1,b₃) .edgeSeq() c= b₂ .edgeSeq()

proof end;

Lemma77: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
(b₂ .addEdge b₃) .edgeSeq() = (b₂ .edgeSeq() ) ^ <*b₃*>

proof end;

Lemma78: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being set holds
( b₃ in b₂ .vertices() iff ex b₄ being odd Nat st
( b₄ <= len b₂ & b₂ . b₄ = b₃ ) )

proof end;

Lemma79: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being set holds
( b₃ in b₂ .edges() iff ex b₄ being even Nat st
( 1 <= b₄ & b₄ <= len b₂ & b₂ . b₄ = b₃ ) )

proof end;

Lemma80: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being set st b₃ in b₂ .edges() holds
ex b₄, b₅ being Vertex of b₁ex b₆ being odd Nat st
( b₆ + 2 <= len b₂ & b₄ = b₂ . b₆ & b₃ = b₂ . (b₆ + 1) & b₅ = b₂ . (b₆ + 2) & b₃ Joins b₄,b₅,b₁ )

proof end;

Lemma81: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄, b₅ being set st b₃ in b₂ .edges() & b₃ Joins b₄,b₅,b₁ holds
( b₄ in b₂ .vertices() & b₅ in b₂ .vertices() )

proof end;

Lemma82: for b₁ being _Graph
for b₂ being Walk of b₁ holds len b₂ = (2 * (b₂ .length() )) + 1
by Def15;

Lemma83: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
b₂ .find b₃ <= b₃

proof end;

Lemma84: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
b₂ .rfind b₃ >= b₃

proof end;

Lemma85: for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is directed iff for b₃ being odd Nat st b₃ < len b₂ holds
b₂ . (b₃ + 1) DJoins b₂ . b₃,b₂ . (b₃ + 2),b₁ )

proof end;

Lemma86: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄, b₅, b₆ being set st b₂ is directed & b₂ is_Walk_from b₃,b₅ & b₄ DJoins b₅,b₆,b₁ holds
( b₂ .addEdge b₄ is directed & b₂ .addEdge b₄ is_Walk_from b₃,b₆ )

proof end;

Lemma87: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being Nat st b₂ is directed holds
b₂ .cut b₃,b₄ is directed

proof end;

Lemma88: for b₁ being _Graph
for b₂ being Walk of b₁ holds
( not b₂ is trivial iff 3 <= len b₂ )

proof end;

Lemma89: for b₁ being _Graph
for b₂ being Walk of b₁ holds
( not b₂ is trivial iff len b₂ <> 1 )

proof end;

Lemma90: for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is trivial iff ex b₃ being Vertex of b₁ st b₂ = b₁ .walkOf b₃ )

proof end;

Lemma91: for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is Trail-like iff for b₃, b₄ being even Nat st 1 <= b₃ & b₃ < b₄ & b₄ <= len b₂ holds
b₂ . b₃ <> b₂ . b₄ )

proof end;

Lemma92: for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is Trail-like iff b₂ .reverse() is Trail-like )

proof end;

Lemma93: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being Nat st b₂ is Trail-like holds
b₂ .cut b₃,b₄ is Trail-like

proof end;

Lemma94: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being set st b₂ is Trail-like & b₃ in (b₂ .last() ) .edgesInOut() & not b₃ in b₂ .edges() holds
b₂ .addEdge b₃ is Trail-like

proof end;

Lemma95: for b₁ being _Graph
for b₂ being Walk of b₁ st len b₂ <= 3 holds
b₂ is Trail-like

proof end;

Lemma96: for b₁ being _Graph
for b₂, b₃, b₄ being set st b₃ Joins b₂,b₄,b₁ holds
b₁ .walkOf b₂,b₃,b₄ is Path-like

proof end;

Lemma97: for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is Path-like iff b₂ .reverse() is Path-like )

proof end;

Lemma98: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being Nat st b₂ is Path-like holds
b₂ .cut b₃,b₄ is Path-like

proof end;

Lemma99: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₂ is Path-like & b₃ Joins b₂ .last() ,b₄,b₁ & not b₃ in b₂ .edges() & ( b₂ is trivial or not b₂ is closed ) & ( for b₅ being odd Nat st 1 < b₅ & b₅ <= len b₂ holds
b₂ . b₅ <> b₄ ) holds
b₂ .addEdge b₃ is Path-like

proof end;

Lemma100: for b₁ being _Graph
for b₂ being Walk of b₁ st ( for b₃, b₄ being odd Nat st b₃ <= len b₂ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ holds
b₃ = b₄ ) holds
b₂ is Path-like

proof end;

Lemma101: for b₁ being _Graph
for b₂ being Walk of b₁ st ( for b₃ being odd Nat st b₃ <= len b₂ holds
b₂ .rfind b₃ = b₃ ) holds
b₂ is Path-like

proof end;

Lemma102: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ & b₂ is Path-like & not b₄ in b₂ .vertices() & ( b₂ is trivial or not b₂ is closed ) holds
b₂ .addEdge b₃ is Path-like

proof end;

Lemma103: for b₁ being _Graph
for b₂ being Walk of b₁ st len b₂ <= 3 holds
b₂ is Path-like

proof end;

registration

let c₁ be _Graph;
cluster Path-like -> Trail-like Walk of a₁;
correctness by Def28;
cluster trivial -> Path-like Walk of a₁;
correctness

proof end;

cluster trivial -> vertex-distinct Walk of a₁;
coherence

proof end;

cluster vertex-distinct -> Path-like Walk of a₁;
coherence

proof end;

cluster Circuit-like -> closed non trivial Trail-like Walk of a₁;
correctness by Def30;
cluster Cycle-like -> closed non trivial Path-like Walk of a₁;
correctness by Def31;

end;

registration

let c₁ be _Graph;
cluster closed directed trivial Trail-like Path-like vertex-distinct Walk of a₁;
existence

proof end;

end;

registration

let c₁ be _Graph;
cluster Trail-like Path-like vertex-distinct Walk of a₁;
existence

proof end;

end;

definition

let c₁ be _Graph;
mode Trail of a₁ is Trail-like Walk of a₁;
mode Path of a₁ is Path-like Walk of a₁;

end;

definition

let c₁ be _Graph;
mode DWalk of a₁ is directed Walk of a₁;
mode DTrail of a₁ is directed Trail of a₁;
mode DPath of a₁ is directed Path of a₁;

end;

registration

let c₁ be _Graph;
let c₂ be Vertex of c₁;
cluster a₁ .walkOf a₂ -> closed directed trivial Trail-like Path-like vertex-distinct ;
coherence by Lemma35;

end;

registration

let c₁ be _Graph;
let c₂, c₃, c₄ be set ;
cluster a₁ .walkOf a₂,a₃,a₄ -> Trail-like Path-like ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂, c₃ be set ;
cluster a₁ .walkOf a₂,a₃,a₂ -> closed Trail-like Path-like ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be closed Walk of c₁;
cluster a₂ .reverse() -> closed ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be trivial Walk of c₁;
cluster a₂ .reverse() -> trivial Trail-like Path-like vertex-distinct ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be Trail of c₁;
cluster a₂ .reverse() -> Trail-like ;
coherence by Lemma92;

end;

registration

let c₁ be _Graph;
let c₂ be Path of c₁;
cluster a₂ .reverse() -> Trail-like Path-like ;
coherence by Lemma97;

end;

registration

let c₁ be _Graph;
let c₂, c₃ be closed Walk of c₁;
cluster a₂ .append a₃ -> closed ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂, c₃ be DWalk of c₁;
cluster a₂ .append a₃ -> directed ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂, c₃ be trivial Walk of c₁;
cluster a₂ .append a₃ -> trivial Trail-like Path-like vertex-distinct ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be DWalk of c₁;
let c₃, c₄ be Nat;
cluster a₂ .cut a₃,a₄ -> directed ;
coherence by Lemma87;

end;

registration

let c₁ be _Graph;
let c₂ be trivial Walk of c₁;
let c₃, c₄ be Nat;
cluster a₂ .cut a₃,a₄ -> trivial Trail-like Path-like vertex-distinct ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be Trail of c₁;
let c₃, c₄ be Nat;
cluster a₂ .cut a₃,a₄ -> Trail-like ;
coherence by Lemma93;

end;

registration

let c₁ be _Graph;
let c₂ be Path of c₁;
let c₃, c₄ be Nat;
cluster a₂ .cut a₃,a₄ -> Trail-like Path-like ;
coherence by Lemma98;

end;

registration

let c₁ be _Graph;
let c₂ be vertex-distinct Walk of c₁;
let c₃, c₄ be Nat;
cluster a₂ .cut a₃,a₄ -> Trail-like Path-like vertex-distinct ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be closed Walk of c₁;
let c₃, c₄ be Nat;
cluster a₂ .remove a₃,a₄ -> closed ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be DWalk of c₁;
let c₃, c₄ be Nat;
cluster a₂ .remove a₃,a₄ -> directed ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be trivial Walk of c₁;
let c₃, c₄ be Nat;
cluster a₂ .remove a₃,a₄ -> trivial Trail-like Path-like vertex-distinct ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be Trail of c₁;
let c₃, c₄ be Nat;
cluster a₂ .remove a₃,a₄ -> Trail-like ;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be Path of c₁;
let c₃, c₄ be Nat;
cluster a₂ .remove a₃,a₄ -> Trail-like Path-like ;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
mode Subwalk of c₂ -> Walk of a₁ means :Def32: :: GLIB_001:def 32
( a₃ is_Walk_from a₂ .first() ,a₂ .last() & ex b₁ being FinSubsequence of a₂ .edgeSeq() st a₃ .edgeSeq() = Seq b₁ );
existence

proof end;

end;

:: deftheorem Def32 defines Subwalk GLIB_001:def 32 :

Lemma105: for b₁ being _Graph
for b₂ being Walk of b₁ holds b₂ is Subwalk of b₂

proof end;

Lemma106: for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Subwalk of b₂
for b₄ being Subwalk of b₃ holds b₄ is Subwalk of b₂

proof end;

Lemma107: for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ is Subwalk of b₃ holds
len b₂ <= len b₃

proof end;

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
let c₃, c₄ be Nat;
redefine func .remove as c₂ .remove c₃,c₄ -> Subwalk of a₂;
coherence

proof end;

end;

registration

let c₁ be _Graph;
let c₂ be Walk of c₁;
cluster Trail-like Path-like Subwalk of a₂;
existence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be Walk of c₁;
mode Trail of a₂ is Trail-like Subwalk of a₂;
mode Path of a₂ is Path-like Subwalk of a₂;

end;

registration

let c₁ be _Graph;
let c₂ be DWalk of c₁;
cluster directed Subwalk of a₂;
existence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be DWalk of c₁;
mode DWalk of a₂ is directed Subwalk of a₂;
mode DTrail of a₂ is directed Trail of a₂;
mode DPath of a₂ is directed Path of a₂;

end;

definition

let c₁ be _Graph;
func c₁ .allWalks() -> non empty Subset of (((the_Vertices_of a₁) \/ (the_Edges_of a₁)) * ) equals :: GLIB_001:def 33
{ b₁ where B is Walk of a₁ : verum } ;
coherence

proof end;

end;

:: deftheorem Def33 defines .allWalks() GLIB_001:def 33 :

definition

let c₁ be _Graph;
func c₁ .allTrails() -> non empty Subset of (a₁ .allWalks() ) equals :: GLIB_001:def 34
{ b₁ where B is Trail of a₁ : verum } ;
coherence

proof end;

end;

:: deftheorem Def34 defines .allTrails() GLIB_001:def 34 :

definition

let c₁ be _Graph;
func c₁ .allPaths() -> non empty Subset of (a₁ .allTrails() ) equals :: GLIB_001:def 35
{ b₁ where B is Path of a₁ : verum } ;
coherence

proof end;

end;

:: deftheorem Def35 defines .allPaths() GLIB_001:def 35 :

definition

let c₁ be _Graph;
func c₁ .allDWalks() -> non empty Subset of (a₁ .allWalks() ) equals :: GLIB_001:def 36
{ b₁ where B is DWalk of a₁ : verum } ;
coherence

proof end;

end;

:: deftheorem Def36 defines .allDWalks() GLIB_001:def 36 :

definition

let c₁ be _Graph;
func c₁ .allDTrails() -> non empty Subset of (a₁ .allTrails() ) equals :: GLIB_001:def 37
{ b₁ where B is DTrail of a₁ : verum } ;
coherence

proof end;

end;

:: deftheorem Def37 defines .allDTrails() GLIB_001:def 37 :

definition

let c₁ be _Graph;
func c₁ .allDPaths() -> non empty Subset of (a₁ .allDTrails() ) equals :: GLIB_001:def 38
{ b₁ where B is directed Path of a₁ : verum } ;
coherence

proof end;

end;

:: deftheorem Def38 defines .allDPaths() GLIB_001:def 38 :

registration

let c₁ be finite _Graph;
cluster a₁ .allTrails() -> non empty finite ;
correctness

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be non empty Subset of (c₁ .allWalks() );
redefine mode Element as Element of c₂ -> Walk of a₁;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be non empty Subset of (c₁ .allTrails() );
redefine mode Element as Element of c₂ -> Trail of a₁;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be non empty Subset of (c₁ .allPaths() );
redefine mode Element as Element of c₂ -> Path of a₁;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be non empty Subset of (c₁ .allDWalks() );
redefine mode Element as Element of c₂ -> DWalk of a₁;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be non empty Subset of (c₁ .allDTrails() );
redefine mode Element as Element of c₂ -> DTrail of a₁;
coherence

proof end;

end;

definition

let c₁ be _Graph;
let c₂ be non empty Subset of (c₁ .allDPaths() );
redefine mode Element as Element of c₂ -> DPath of a₁;
coherence

proof end;

end;

theorem Th7: :: GLIB_001:7

canceled;

theorem Th8: :: GLIB_001:8

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
b₂ . b₃ in the_Vertices_of b₁ by Lemma32;

theorem Th9: :: GLIB_001:9

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being even Nat st b₃ in dom b₂ holds
b₂ . b₃ in the_Edges_of b₁

proof end;

theorem Th10: :: GLIB_001:10

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being even Nat st b₃ in dom b₂ holds
ex b₄ being odd Nat st
( b₄ = b₃ - 1 & b₃ - 1 in dom b₂ & b₃ + 1 in dom b₂ & b₂ . b₃ Joins b₂ . b₄,b₂ . (b₃ + 1),b₁ ) by Lemma33;

theorem Th11: :: GLIB_001:11

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ < len b₂ holds
b₂ . (b₃ + 1) in (b₂ .vertexAt b₃) .edgesInOut()

proof end;

theorem Th12: :: GLIB_001:12

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st 1 < b₃ & b₃ <= len b₂ holds
b₂ . (b₃ - 1) in (b₂ .vertexAt b₃) .edgesInOut()

proof end;

theorem Th13: :: GLIB_001:13

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ < len b₂ holds
( b₃ in dom b₂ & b₃ + 1 in dom b₂ & b₃ + 2 in dom b₂ )

proof end;

theorem Th14: :: GLIB_001:14

for b₁ being _Graph
for b₂ being Vertex of b₁ holds
( len (b₁ .walkOf b₂) = 1 & (b₁ .walkOf b₂) . 1 = b₂ & (b₁ .walkOf b₂) .first() = b₂ & (b₁ .walkOf b₂) .last() = b₂ & b₁ .walkOf b₂ is_Walk_from b₂,b₂ )

proof end;

theorem Th15: :: GLIB_001:15

for b₁ being _Graph
for b₂, b₃, b₄ being set st b₂ Joins b₃,b₄,b₁ holds
len (b₁ .walkOf b₃,b₂,b₄) = 3

proof end;

theorem Th16: :: GLIB_001:16

for b₁ being _Graph
for b₂, b₃, b₄ being set st b₂ Joins b₃,b₄,b₁ holds
( (b₁ .walkOf b₃,b₂,b₄) .first() = b₃ & (b₁ .walkOf b₃,b₂,b₄) .last() = b₄ & b₁ .walkOf b₃,b₂,b₄ is_Walk_from b₃,b₄ )

proof end;

theorem Th17: :: GLIB_001:17

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ holds
( b₃ .first() = b₄ .first() & b₃ .last() = b₄ .last() ) ;

theorem Th18: :: GLIB_001:18

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set holds
( b₂ is_Walk_from b₃,b₄ iff ( b₂ . 1 = b₃ & b₂ . (len b₂) = b₄ ) )

proof end;

theorem Th19: :: GLIB_001:19

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₂ is_Walk_from b₃,b₄ holds
( b₃ is Vertex of b₁ & b₄ is Vertex of b₁ )

proof end;

theorem Th20: :: GLIB_001:20

for b₁, b₂ being _Graph
for b₃, b₄ being set
for b₅ being Walk of b₁
for b₆ being Walk of b₂ st b₅ = b₆ holds
( b₅ is_Walk_from b₃,b₄ iff b₆ is_Walk_from b₃,b₄ )

proof end;

theorem Th21: :: GLIB_001:21

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ holds
for b₅ being Nat holds b₃ .vertexAt b₅ = b₄ .vertexAt b₅

proof end;

theorem Th22: :: GLIB_001:22

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( len b₂ = len (b₂ .reverse() ) & dom b₂ = dom (b₂ .reverse() ) & rng b₂ = rng (b₂ .reverse() ) ) by Lemma38;

theorem Th23: :: GLIB_001:23

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ .first() = (b₂ .reverse() ) .last() & b₂ .last() = (b₂ .reverse() ) .first() )

proof end;

theorem Th24: :: GLIB_001:24

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set holds
( b₂ is_Walk_from b₃,b₄ iff b₂ .reverse() is_Walk_from b₄,b₃ )

proof end;

theorem Th25: :: GLIB_001:25

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat st b₃ in dom b₂ holds
( b₂ . b₃ = (b₂ .reverse() ) . (((len b₂) - b₃) + 1) & ((len b₂) - b₃) + 1 in dom (b₂ .reverse() ) )

proof end;

theorem Th26: :: GLIB_001:26

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat st b₃ in dom (b₂ .reverse() ) holds
( (b₂ .reverse() ) . b₃ = b₂ . (((len b₂) - b₃) + 1) & ((len b₂) - b₃) + 1 in dom b₂ ) by Lemma40;

theorem Th27: :: GLIB_001:27

for b₁ being _Graph
for b₂ being Walk of b₁ holds (b₂ .reverse() ) .reverse() = b₂ by Lemma41;

theorem Th28: :: GLIB_001:28

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ holds
b₃ .reverse() = b₄ .reverse() ;

theorem Th29: :: GLIB_001:29

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
(len (b₂ .append b₃)) + 1 = (len b₂) + (len b₃) by Lemma42;

theorem Th30: :: GLIB_001:30

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
( len b₂ <= len (b₂ .append b₃) & len b₃ <= len (b₂ .append b₃) ) by Lemma43;

theorem Th31: :: GLIB_001:31

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
( (b₂ .append b₃) .first() = b₂ .first() & (b₂ .append b₃) .last() = b₃ .last() & b₂ .append b₃ is_Walk_from b₂ .first() ,b₃ .last() ) by Lemma44;

theorem Th32: :: GLIB_001:32

for b₁ being _Graph
for b₂, b₃ being Walk of b₁
for b₄, b₅, b₆ being set st b₂ is_Walk_from b₄,b₅ & b₃ is_Walk_from b₅,b₆ holds
b₂ .append b₃ is_Walk_from b₄,b₆

proof end;

theorem Th33: :: GLIB_001:33

for b₁ being _Graph
for b₂, b₃ being Walk of b₁
for b₄ being Nat st b₄ in dom b₂ holds
( (b₂ .append b₃) . b₄ = b₂ . b₄ & b₄ in dom (b₂ .append b₃) ) by Lemma45;

theorem Th34: :: GLIB_001:34

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
for b₄ being Nat st b₄ < len b₃ holds
( (b₂ .append b₃) . ((len b₂) + b₄) = b₃ . (b₄ + 1) & (len b₂) + b₄ in dom (b₂ .append b₃) ) by Lemma46;

theorem Th35: :: GLIB_001:35

for b₁ being _Graph
for b₂, b₃ being Walk of b₁
for b₄ being Nat holds
( not b₄ in dom (b₂ .append b₃) or b₄ in dom b₂ or ex b₅ being Nat st
( b₅ < len b₃ & b₄ = (len b₂) + b₅ ) ) by Lemma47;

theorem Th36: :: GLIB_001:36

for b₁, b₂ being _Graph
for b₃, b₄ being Walk of b₁
for b₅, b₆ being Walk of b₂ st b₃ = b₅ & b₄ = b₆ holds
b₃ .append b₄ = b₅ .append b₆

proof end;

theorem Th37: :: GLIB_001:37

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ holds
( (len (b₂ .cut b₃,b₄)) + b₃ = b₄ + 1 & ( for b₅ being Nat st b₅ < len (b₂ .cut b₃,b₄) holds
( (b₂ .cut b₃,b₄) . (b₅ + 1) = b₂ . (b₃ + b₅) & b₃ + b₅ in dom b₂ ) ) ) by Lemma48;

theorem Th38: :: GLIB_001:38

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ holds
( (b₂ .cut b₃,b₄) .first() = b₂ . b₃ & (b₂ .cut b₃,b₄) .last() = b₂ . b₄ & b₂ .cut b₃,b₄ is_Walk_from b₂ . b₃,b₂ . b₄ ) by Lemma49;

theorem Th39: :: GLIB_001:39

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄, b₅ being odd Nat st b₃ <= b₄ & b₄ <= b₅ & b₅ <= len b₂ holds
(b₂ .cut b₃,b₄) .append (b₂ .cut b₄,b₅) = b₂ .cut b₃,b₅ by Lemma50;

theorem Th40: :: GLIB_001:40

for b₁ being _Graph
for b₂ being Walk of b₁ holds b₂ .cut 1,(len b₂) = b₂ by Lemma51;

theorem Th41: :: GLIB_001:41

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ < len b₂ holds
b₁ .walkOf (b₂ . b₃),(b₂ . (b₃ + 1)),(b₂ . (b₃ + 2)) = b₂ .cut b₃,(b₃ + 2)

proof end;

theorem Th42: :: GLIB_001:42

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ < len b₂ holds
(b₂ .cut b₃,b₄) .addEdge (b₂ . (b₄ + 1)) = b₂ .cut b₃,(b₄ + 2)

proof end;

theorem Th43: :: GLIB_001:43

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
b₂ .cut b₃,b₃ = <*(b₂ .vertexAt b₃)*> by Lemma52;

theorem Th44: :: GLIB_001:44

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being Nat st not b₃ is even & b₃ <= b₄ holds
(b₂ .cut 1,b₄) .cut 1,b₃ = b₂ .cut 1,b₃ by Lemma53;

theorem Th45: :: GLIB_001:45

for b₁ being _Graph
for b₂, b₃ being Walk of b₁
for b₄, b₅ being odd Nat st b₄ <= b₅ & b₅ <= len b₂ & b₂ .last() = b₃ .first() holds
(b₂ .append b₃) .cut b₄,b₅ = b₂ .cut b₄,b₅ by Lemma54;

theorem Th46: :: GLIB_001:46

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
len (b₂ .cut 1,b₃) = b₃ by Lemma55;

theorem Th47: :: GLIB_001:47

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat
for b₄ being Nat st b₄ in dom (b₂ .cut 1,b₃) & b₃ <= len b₂ holds
(b₂ .cut 1,b₃) . b₄ = b₂ . b₄ by Lemma56;

theorem Th48: :: GLIB_001:48

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat
for b₅ being Nat st b₃ <= b₄ & b₄ <= len b₂ & b₅ in dom (b₂ .cut b₃,b₄) holds
( (b₂ .cut b₃,b₄) . b₅ = b₂ . ((b₃ + b₅) - 1) & (b₃ + b₅) - 1 in dom b₂ )

proof end;

theorem Th49: :: GLIB_001:49

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂
for b₅, b₆ being Nat st b₃ = b₄ holds
b₃ .cut b₅,b₆ = b₄ .cut b₅,b₆

proof end;

theorem Th50: :: GLIB_001:50

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ holds
(len (b₂ .remove b₃,b₄)) + b₄ = (len b₂) + b₃ by Lemma57;

theorem Th51: :: GLIB_001:51

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set
for b₅, b₆ being Nat st b₂ is_Walk_from b₃,b₄ holds
b₂ .remove b₅,b₆ is_Walk_from b₃,b₄ by Lemma58;

theorem Th52: :: GLIB_001:52

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being Nat holds len (b₂ .remove b₃,b₄) <= len b₂ by Lemma59;

theorem Th53: :: GLIB_001:53

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat holds b₂ .remove b₃,b₃ = b₂ by Lemma60;

theorem Th54: :: GLIB_001:54

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ holds
(b₂ .cut 1,b₃) .last() = (b₂ .cut b₄,(len b₂)) .first() by Lemma61;

theorem Th55: :: GLIB_001:55

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ holds
for b₅ being Nat st b₅ in Seg b₃ holds
(b₂ .remove b₃,b₄) . b₅ = b₂ . b₅ by Lemma62;

theorem Th56: :: GLIB_001:56

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ holds
for b₅ being Nat st b₃ <= b₅ & b₅ <= len (b₂ .remove b₃,b₄) holds
( (b₂ .remove b₃,b₄) . b₅ = b₂ . ((b₅ - b₃) + b₄) & (b₅ - b₃) + b₄ is Nat & (b₅ - b₃) + b₄ <= len b₂ ) by Lemma63;

theorem Th57: :: GLIB_001:57

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ holds
len (b₂ .remove b₃,b₄) = ((len b₂) + b₃) - b₄ by Lemma64;

theorem Th58: :: GLIB_001:58

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat st b₂ . b₃ = b₂ .last() holds
b₂ .remove b₃,(len b₂) = b₂ .cut 1,b₃

proof end;

theorem Th59: :: GLIB_001:59

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat st b₂ .first() = b₂ . b₃ holds
b₂ .remove 1,b₃ = b₂ .cut b₃,(len b₂) by Lemma65;

theorem Th60: :: GLIB_001:60

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being Nat holds
( (b₂ .remove b₃,b₄) .first() = b₂ .first() & (b₂ .remove b₃,b₄) .last() = b₂ .last() ) by Lemma66;

theorem Th61: :: GLIB_001:61

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat
for b₅ being Nat st b₃ <= b₄ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ & b₅ in dom (b₂ .remove b₃,b₄) & not b₅ in Seg b₃ holds
( b₃ <= b₅ & b₅ <= len (b₂ .remove b₃,b₄) ) by Lemma67;

theorem Th62: :: GLIB_001:62

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂
for b₅, b₆ being Nat st b₃ = b₄ holds
b₃ .remove b₅,b₆ = b₄ .remove b₅,b₆

proof end;

theorem Th63: :: GLIB_001:63

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
b₂ .addEdge b₃ = b₂ ^ <*b₃,b₄*> by Lemma68;

theorem Th64: :: GLIB_001:64

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
( (b₂ .addEdge b₃) .first() = b₂ .first() & (b₂ .addEdge b₃) .last() = b₄ & b₂ .addEdge b₃ is_Walk_from b₂ .first() ,b₄ ) by Lemma69;

theorem Th65: :: GLIB_001:65

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
len (b₂ .addEdge b₃) = (len b₂) + 2 by Lemma70;

theorem Th66: :: GLIB_001:66

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
( (b₂ .addEdge b₃) . ((len b₂) + 1) = b₃ & (b₂ .addEdge b₃) . ((len b₂) + 2) = b₄ & ( for b₅ being Nat st b₅ in dom b₂ holds
(b₂ .addEdge b₃) . b₅ = b₂ . b₅ ) ) by Lemma71;

theorem Th67: :: GLIB_001:67

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄, b₅, b₆ being set st b₂ is_Walk_from b₃,b₄ & b₅ Joins b₄,b₆,b₁ holds
b₂ .addEdge b₅ is_Walk_from b₃,b₆ by Lemma72;

theorem Th68: :: GLIB_001:68

for b₁ being _Graph
for b₂ being Walk of b₁ holds 1 <= len (b₂ .vertexSeq() )

proof end;

theorem Th69: :: GLIB_001:69

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
( (2 * ((b₃ + 1) div 2)) - 1 = b₃ & 1 <= (b₃ + 1) div 2 & (b₃ + 1) div 2 <= len (b₂ .vertexSeq() ) )

proof end;

theorem Th70: :: GLIB_001:70

for b₁ being _Graph
for b₂ being Vertex of b₁ holds (b₁ .walkOf b₂) .vertexSeq() = <*b₂*>

proof end;

theorem Th71: :: GLIB_001:71

for b₁ being _Graph
for b₂, b₃, b₄ being set st b₂ Joins b₃,b₄,b₁ holds
(b₁ .walkOf b₃,b₂,b₄) .vertexSeq() = <*b₃,b₄*>

proof end;

theorem Th72: :: GLIB_001:72

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ .first() = (b₂ .vertexSeq() ) . 1 & b₂ .last() = (b₂ .vertexSeq() ) . (len (b₂ .vertexSeq() )) )

proof end;

theorem Th73: :: GLIB_001:73

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
b₂ .vertexAt b₃ = (b₂ .vertexSeq() ) . ((b₃ + 1) div 2)

proof end;

theorem Th74: :: GLIB_001:74

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat holds
( b₃ in dom (b₂ .vertexSeq() ) iff (2 * b₃) - 1 in dom b₂ )

proof end;

theorem Th75: :: GLIB_001:75

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat holds (b₂ .cut 1,b₃) .vertexSeq() c= b₂ .vertexSeq()

proof end;

theorem Th76: :: GLIB_001:76

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
(b₂ .addEdge b₃) .vertexSeq() = (b₂ .vertexSeq() ) ^ <*b₄*>

proof end;

theorem Th77: :: GLIB_001:77

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ holds
b₃ .vertexSeq() = b₄ .vertexSeq()

proof end;

theorem Th78: :: GLIB_001:78

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being even Nat st 1 <= b₃ & b₃ <= len b₂ holds
( b₃ div 2 in dom (b₂ .edgeSeq() ) & b₂ . b₃ = (b₂ .edgeSeq() ) . (b₃ div 2) ) by Lemma73;

theorem Th79: :: GLIB_001:79

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat holds
( b₃ in dom (b₂ .edgeSeq() ) iff 2 * b₃ in dom b₂ ) by Lemma74;

theorem Th80: :: GLIB_001:80

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat st b₃ in dom (b₂ .edgeSeq() ) holds
(b₂ .edgeSeq() ) . b₃ in the_Edges_of b₁

proof end;

theorem Th81: :: GLIB_001:81

for b₁ being _Graph
for b₂ being Walk of b₁ ex b₃ being even Nat st
( b₃ = (len b₂) - 1 & len (b₂ .edgeSeq() ) = b₃ div 2 ) by Lemma75;

theorem Th82: :: GLIB_001:82

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Nat holds (b₂ .cut 1,b₃) .edgeSeq() c= b₂ .edgeSeq() by Lemma76;

theorem Th83: :: GLIB_001:83

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
(b₂ .addEdge b₃) .edgeSeq() = (b₂ .edgeSeq() ) ^ <*b₃*> by Lemma77;

theorem Th84: :: GLIB_001:84

for b₁ being _Graph
for b₂, b₃, b₄ being set holds
( b₂ Joins b₃,b₄,b₁ iff (b₁ .walkOf b₃,b₂,b₄) .edgeSeq() = <*b₂*> )

proof end;

theorem Th85: :: GLIB_001:85

for b₁ being _Graph
for b₂ being Walk of b₁ holds (b₂ .reverse() ) .edgeSeq() = Rev (b₂ .edgeSeq() )

proof end;

theorem Th86: :: GLIB_001:86

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
(b₂ .append b₃) .edgeSeq() = (b₂ .edgeSeq() ) ^ (b₃ .edgeSeq() )

proof end;

theorem Th87: :: GLIB_001:87

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ holds
b₃ .edgeSeq() = b₄ .edgeSeq()

proof end;

theorem Th88: :: GLIB_001:88

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being set holds
( b₃ in b₂ .vertices() iff ex b₄ being odd Nat st
( b₄ <= len b₂ & b₂ . b₄ = b₃ ) ) by Lemma78;

theorem Th89: :: GLIB_001:89

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ .first() in b₂ .vertices() & b₂ .last() in b₂ .vertices() )

proof end;

theorem Th90: :: GLIB_001:90

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
b₂ .vertexAt b₃ in b₂ .vertices()

proof end;

theorem Th91: :: GLIB_001:91

for b₁ being _Graph
for b₂ being Vertex of b₁ holds (b₁ .walkOf b₂) .vertices() = {b₂}

proof end;

theorem Th92: :: GLIB_001:92

for b₁ being _Graph
for b₂, b₃, b₄ being set st b₂ Joins b₃,b₄,b₁ holds
(b₁ .walkOf b₃,b₂,b₄) .vertices() = {b₃,b₄}

proof end;

theorem Th93: :: GLIB_001:93

for b₁ being _Graph
for b₂ being Walk of b₁ holds b₂ .vertices() = (b₂ .reverse() ) .vertices()

proof end;

theorem Th94: :: GLIB_001:94

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
(b₂ .append b₃) .vertices() = (b₂ .vertices() ) \/ (b₃ .vertices() )

proof end;

theorem Th95: :: GLIB_001:95

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ holds
(b₂ .cut b₃,b₄) .vertices() c= b₂ .vertices()

proof end;

theorem Th96: :: GLIB_001:96

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
(b₂ .addEdge b₃) .vertices() = (b₂ .vertices() ) \/ {b₄}

proof end;

theorem Th97: :: GLIB_001:97

for b₁ being finite _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ & not b₄ in b₂ .vertices() holds
card ((b₂ .addEdge b₃) .vertices() ) = (card (b₂ .vertices() )) + 1

proof end;

theorem Th98: :: GLIB_001:98

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ in b₂ .vertices() & b₄ in b₂ .vertices() holds
ex b₅ being Walk of b₁ st b₅ is_Walk_from b₃,b₄

proof end;

theorem Th99: :: GLIB_001:99

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ holds
b₃ .vertices() = b₄ .vertices() by Th77;

theorem Th100: :: GLIB_001:100

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being set holds
( b₃ in b₂ .edges() iff ex b₄ being even Nat st
( 1 <= b₄ & b₄ <= len b₂ & b₂ . b₄ = b₃ ) ) by Lemma79;

theorem Th101: :: GLIB_001:101

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being set holds
( b₃ in b₂ .edges() iff ex b₄ being odd Nat st
( b₄ < len b₂ & b₂ . (b₄ + 1) = b₃ ) )

proof end;

theorem Th102: :: GLIB_001:102

for b₁ being _Graph
for b₂ being Walk of b₁ holds rng b₂ = (b₂ .vertices() ) \/ (b₂ .edges() )

proof end;

theorem Th103: :: GLIB_001:103

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ .last() = b₃ .first() holds
(b₂ .append b₃) .edges() = (b₂ .edges() ) \/ (b₃ .edges() )

proof end;

theorem Th104: :: GLIB_001:104

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being set st b₃ in b₂ .edges() holds
ex b₄, b₅ being Vertex of b₁ex b₆ being odd Nat st
( b₆ + 2 <= len b₂ & b₄ = b₂ . b₆ & b₃ = b₂ . (b₆ + 1) & b₅ = b₂ . (b₆ + 2) & b₃ Joins b₄,b₅,b₁ ) by Lemma80;

theorem Th105: :: GLIB_001:105

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being set holds
( b₃ in b₂ .edges() iff ex b₄ being Nat st
( b₄ in dom (b₂ .edgeSeq() ) & (b₂ .edgeSeq() ) . b₄ = b₃ ) )

proof end;

theorem Th106: :: GLIB_001:106

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄, b₅ being set st b₃ in b₂ .edges() & b₃ Joins b₄,b₅,b₁ holds
( b₄ in b₂ .vertices() & b₅ in b₂ .vertices() ) by Lemma81;

theorem Th107: :: GLIB_001:107

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being Nat holds (b₂ .cut b₃,b₄) .edges() c= b₂ .edges()

proof end;

theorem Th108: :: GLIB_001:108

for b₁ being _Graph
for b₂ being Walk of b₁ holds b₂ .edges() = (b₂ .reverse() ) .edges()

proof end;

theorem Th109: :: GLIB_001:109

for b₁ being _Graph
for b₂, b₃, b₄ being set holds
( b₂ Joins b₃,b₄,b₁ iff (b₁ .walkOf b₃,b₂,b₄) .edges() = {b₂} )

proof end;

theorem Th110: :: GLIB_001:110

for b₁ being _Graph
for b₂ being Walk of b₁ holds b₂ .edges() c= b₁ .edgesBetween (b₂ .vertices() )

proof end;

theorem Th111: :: GLIB_001:111

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ holds
b₃ .edges() = b₄ .edges() by Th87;

theorem Th112: :: GLIB_001:112

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
(b₂ .addEdge b₃) .edges() = (b₂ .edges() ) \/ {b₃}

proof end;

theorem Th113: :: GLIB_001:113

for b₁ being _Graph
for b₂ being Walk of b₁ holds len b₂ = (2 * (b₂ .length() )) + 1 by Lemma82;

theorem Th114: :: GLIB_001:114

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ holds
( len b₂ = len b₃ iff b₂ .length() = b₃ .length() )

proof end;

theorem Th115: :: GLIB_001:115

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ holds
b₃ .length() = b₄ .length() by Th87;

theorem Th116: :: GLIB_001:116

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
( b₂ .find (b₂ . b₃) <= b₃ & b₂ .rfind (b₂ . b₃) >= b₃ )

proof end;

theorem Th117: :: GLIB_001:117

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂
for b₅ being set st b₃ = b₄ holds
( b₃ .find b₅ = b₄ .find b₅ & b₃ .rfind b₅ = b₄ .rfind b₅ )

proof end;

theorem Th118: :: GLIB_001:118

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being odd Nat st b₃ <= len b₂ holds
( b₂ .find b₃ <= b₃ & b₂ .rfind b₃ >= b₃ ) by Lemma83, Lemma84;

theorem Th119: :: GLIB_001:119

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is closed iff b₂ . 1 = b₂ . (len b₂) )

proof end;

theorem Th120: :: GLIB_001:120

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is closed iff ex b₃ being set st b₂ is_Walk_from b₃,b₃ )

proof end;

theorem Th121: :: GLIB_001:121

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is closed iff b₂ .reverse() is closed )

proof end;

theorem Th122: :: GLIB_001:122

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ & b₃ is closed holds
b₄ is closed

proof end;

theorem Th123: :: GLIB_001:123

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is directed iff for b₃ being odd Nat st b₃ < len b₂ holds
b₂ . (b₃ + 1) DJoins b₂ . b₃,b₂ . (b₃ + 2),b₁ ) by Lemma85;

theorem Th124: :: GLIB_001:124

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄, b₅, b₆ being set st b₂ is directed & b₂ is_Walk_from b₃,b₄ & b₅ DJoins b₄,b₆,b₁ holds
( b₂ .addEdge b₅ is directed & b₂ .addEdge b₅ is_Walk_from b₃,b₆ ) by Lemma86;

theorem Th125: :: GLIB_001:125

for b₁ being _Graph
for b₂ being DWalk of b₁
for b₃, b₄ being Nat holds b₂ .cut b₃,b₄ is directed ;

theorem Th126: :: GLIB_001:126

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( not b₂ is trivial iff 3 <= len b₂ ) by Lemma88;

theorem Th127: :: GLIB_001:127

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( not b₂ is trivial iff len b₂ <> 1 ) by Lemma89;

theorem Th128: :: GLIB_001:128

for b₁ being _Graph
for b₂ being Walk of b₁ st b₂ .first() <> b₂ .last() holds
not b₂ is trivial by Lemma89;

theorem Th129: :: GLIB_001:129

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is trivial iff ex b₃ being Vertex of b₁ st b₂ = b₁ .walkOf b₃ ) by Lemma90;

theorem Th130: :: GLIB_001:130

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is trivial iff b₂ .reverse() is trivial )

proof end;

theorem Th131: :: GLIB_001:131

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ is trivial holds
b₃ .append b₂ = b₃

proof end;

theorem Th132: :: GLIB_001:132

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being odd Nat st b₃ <= b₄ & b₄ <= len b₂ holds
( b₂ .cut b₃,b₄ is trivial iff b₃ = b₄ )

proof end;

theorem Th133: :: GLIB_001:133

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ holds
not b₂ .addEdge b₃ is trivial

proof end;

theorem Th134: :: GLIB_001:134

for b₁ being _Graph
for b₂ being Walk of b₁ st not b₂ is trivial holds
ex b₃ being odd Nat st
( b₃ = (len b₂) - 2 & (b₂ .cut 1,b₃) .addEdge (b₂ . (b₃ + 1)) = b₂ )

proof end;

theorem Th135: :: GLIB_001:135

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st not b₂ is trivial & b₂ .edges() c= b₃ .edges() holds
b₂ .vertices() c= b₃ .vertices()

proof end;

theorem Th136: :: GLIB_001:136

for b₁ being _Graph
for b₂ being Walk of b₁ st not b₂ is trivial holds
for b₃ being Vertex of b₁ st b₃ in b₂ .vertices() holds
not b₃ is isolated

proof end;

theorem Th137: :: GLIB_001:137

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is trivial iff b₂ .edges() = {} )

proof end;

theorem Th138: :: GLIB_001:138

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ & b₃ is trivial holds
b₄ is trivial

proof end;

theorem Th139: :: GLIB_001:139

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is Trail-like iff for b₃, b₄ being even Nat st 1 <= b₃ & b₃ < b₄ & b₄ <= len b₂ holds
b₂ . b₃ <> b₂ . b₄ ) by Lemma91;

theorem Th140: :: GLIB_001:140

for b₁ being _Graph
for b₂ being Walk of b₁ st len b₂ <= 3 holds
b₂ is Trail-like by Lemma95;

theorem Th141: :: GLIB_001:141

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is Trail-like iff b₂ .reverse() is Trail-like ) by Lemma92;

theorem Th142: :: GLIB_001:142

for b₁ being _Graph
for b₂ being Trail of b₁
for b₃, b₄ being Nat holds b₂ .cut b₃,b₄ is Trail-like ;

theorem Th143: :: GLIB_001:143

for b₁ being _Graph
for b₂ being Trail of b₁
for b₃ being set st b₃ in (b₂ .last() ) .edgesInOut() & not b₃ in b₂ .edges() holds
b₂ .addEdge b₃ is Trail-like by Lemma94;

theorem Th144: :: GLIB_001:144

for b₁ being _Graph
for b₂ being Trail of b₁
for b₃ being Vertex of b₁ st b₃ in b₂ .vertices() & b₃ is endvertex & not b₃ = b₂ .first() holds
b₃ = b₂ .last()

proof end;

theorem Th145: :: GLIB_001:145

for b₁ being finite _Graph
for b₂ being Trail of b₁ holds len (b₂ .edgeSeq() ) <= b₁ .size()

proof end;

theorem Th146: :: GLIB_001:146

for b₁ being _Graph
for b₂ being Walk of b₁ st len b₂ <= 3 holds
b₂ is Path-like by Lemma103;

theorem Th147: :: GLIB_001:147

for b₁ being _Graph
for b₂ being Walk of b₁ st ( for b₃, b₄ being odd Nat st b₃ <= len b₂ & b₄ <= len b₂ & b₂ . b₃ = b₂ . b₄ holds
b₃ = b₄ ) holds
b₂ is Path-like by Lemma100;

theorem Th148: :: GLIB_001:148

for b₁ being _Graph
for b₂ being Path of b₁ st not b₂ is closed holds
for b₃, b₄ being odd Nat st b₃ < b₄ & b₄ <= len b₂ holds
b₂ . b₃ <> b₂ . b₄

proof end;

theorem Th149: :: GLIB_001:149

for b₁ being _Graph
for b₂ being Walk of b₁ holds
( b₂ is Path-like iff b₂ .reverse() is Path-like ) by Lemma97;

theorem Th150: :: GLIB_001:150

for b₁ being _Graph
for b₂ being Path of b₁
for b₃, b₄ being Nat holds b₂ .cut b₃,b₄ is Path-like ;

theorem Th151: :: GLIB_001:151

for b₁ being _Graph
for b₂ being Path of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ & not b₃ in b₂ .edges() & ( b₂ is trivial or not b₂ is closed ) & ( for b₅ being odd Nat st 1 < b₅ & b₅ <= len b₂ holds
b₂ . b₅ <> b₄ ) holds
b₂ .addEdge b₃ is Path-like

proof end;

theorem Th152: :: GLIB_001:152

for b₁ being _Graph
for b₂ being Path of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ & not b₄ in b₂ .vertices() & ( b₂ is trivial or not b₂ is closed ) holds
b₂ .addEdge b₃ is Path-like by Lemma102;

theorem Th153: :: GLIB_001:153

for b₁ being _Graph
for b₂ being Walk of b₁ st ( for b₃ being odd Nat st b₃ <= len b₂ holds
b₂ .find (b₂ . b₃) = b₂ .rfind (b₂ . b₃) ) holds
b₂ is Path-like

proof end;

theorem Th154: :: GLIB_001:154

for b₁ being _Graph
for b₂ being Walk of b₁ st ( for b₃ being odd Nat st b₃ <= len b₂ holds
b₂ .rfind b₃ = b₃ ) holds
b₂ is Path-like by Lemma101;

theorem Th155: :: GLIB_001:155

for b₁ being finite _Graph
for b₂ being Path of b₁ holds len (b₂ .vertexSeq() ) <= (b₁ .order() ) + 1

proof end;

theorem Th156: :: GLIB_001:156

for b₁ being _Graph
for b₂ being vertex-distinct Walk of b₁
for b₃, b₄ being set st b₃ Joins b₂ .last() ,b₄,b₁ & not b₄ in b₂ .vertices() holds
b₂ .addEdge b₃ is vertex-distinct

proof end;

theorem Th157: :: GLIB_001:157

for b₁ being _Graph
for b₂, b₃ being set st b₂ Joins b₃,b₃,b₁ holds
b₁ .walkOf b₃,b₂,b₃ is Cycle-like

proof end;

theorem Th158: :: GLIB_001:158

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃, b₄, b₅ being set st b₃ Joins b₄,b₅,b₁ & b₃ in b₂ .edges() & b₂ is Cycle-like holds
ex b₆ being Walk of b₁ st
( b₆ is_Walk_from b₄,b₅ & not b₃ in b₆ .edges() )

proof end;

theorem Th159: :: GLIB_001:159

for b₁ being _Graph
for b₂ being Walk of b₁ holds b₂ is Subwalk of b₂ by Lemma105;

theorem Th160: :: GLIB_001:160

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being Subwalk of b₂
for b₄ being Subwalk of b₃ holds b₄ is Subwalk of b₂ by Lemma106;

theorem Th161: :: GLIB_001:161

for b₁ being _Graph
for b₂, b₃ being Walk of b₁
for b₄, b₅ being set st b₂ is Subwalk of b₃ holds
( b₂ is_Walk_from b₄,b₅ iff b₃ is_Walk_from b₄,b₅ )

proof end;

theorem Th162: :: GLIB_001:162

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ is Subwalk of b₃ holds
( b₂ .first() = b₃ .first() & b₂ .last() = b₃ .last() )

proof end;

theorem Th163: :: GLIB_001:163

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ is Subwalk of b₃ holds
len b₂ <= len b₃ by Lemma107;

theorem Th164: :: GLIB_001:164

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ is Subwalk of b₃ holds
( b₂ .edges() c= b₃ .edges() & b₂ .vertices() c= b₃ .vertices() )

proof end;

theorem Th165: :: GLIB_001:165

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ is Subwalk of b₃ holds
for b₄ being odd Nat st b₄ <= len b₂ holds
ex b₅ being odd Nat st
( b₄ <= b₅ & b₅ <= len b₃ & b₂ . b₄ = b₃ . b₅ )

proof end;

theorem Th166: :: GLIB_001:166

for b₁ being _Graph
for b₂, b₃ being Walk of b₁ st b₂ is Subwalk of b₃ holds
for b₄ being even Nat st 1 <= b₄ & b₄ <= len b₂ holds
ex b₅ being even Nat st
( b₄ <= b₅ & b₅ <= len b₃ & b₂ . b₄ = b₃ . b₅ )

proof end;

theorem Th167: :: GLIB_001:167

for b₁ being _Graph
for b₂ being Trail of b₁ st not b₂ is trivial holds
ex b₃ being Path of b₂ st not b₃ is trivial

proof end;

theorem Th168: :: GLIB_001:168

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Walk of b₂ holds b₃ is Walk of b₁

proof end;

theorem Th169: :: GLIB_001:169

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Walk of b₁ st b₃ is trivial & b₃ .first() in the_Vertices_of b₂ holds
b₃ is Walk of b₂

proof end;

theorem Th170: :: GLIB_001:170

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Walk of b₁ st not b₃ is trivial & b₃ .edges() c= the_Edges_of b₂ holds
b₃ is Walk of b₂

proof end;

theorem Th171: :: GLIB_001:171

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Walk of b₁ st b₃ .vertices() c= the_Vertices_of b₂ & b₃ .edges() c= the_Edges_of b₂ holds
b₃ is Walk of b₂

proof end;

theorem Th172: :: GLIB_001:172

for b₁ being non trivial _Graph
for b₂ being Walk of b₁
for b₃ being Vertex of b₁
for b₄ being removeVertex of b₁,b₃ st not b₃ in b₂ .vertices() holds
b₂ is Walk of b₄

proof end;

theorem Th173: :: GLIB_001:173

for b₁ being _Graph
for b₂ being Walk of b₁
for b₃ being set
for b₄ being removeEdge of b₁,b₃ st not b₃ in b₂ .edges() holds
b₂ is Walk of b₄

proof end;

theorem Th174: :: GLIB_001:174

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃, b₄, b₅ being set st b₅ Joins b₃,b₄,b₂ holds
b₁ .walkOf b₃,b₅,b₄ = b₂ .walkOf b₃,b₅,b₄

proof end;

theorem Th175: :: GLIB_001:175

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Walk of b₁
for b₄ being Walk of b₂
for b₅ being set st b₃ = b₄ & b₅ in (b₄ .last() ) .edgesInOut() holds
b₃ .addEdge b₅ = b₄ .addEdge b₅

proof end;

theorem Th176: :: GLIB_001:176

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Walk of b₂ holds
( ( b₃ is closed implies b₃ is closed Walk of b₁ ) & ( b₃ is directed implies b₃ is directed Walk of b₁ ) & ( b₃ is trivial implies b₃ is trivial Walk of b₁ ) & ( b₃ is Trail-like implies b₃ is Trail-like Walk of b₁ ) & ( b₃ is Path-like implies b₃ is Path-like Walk of b₁ ) & ( b₃ is vertex-distinct implies b₃ is vertex-distinct Walk of b₁ ) )

proof end;

theorem Th177: :: GLIB_001:177

for b₁ being _Graph
for b₂ being Subgraph of b₁
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₃ = b₄ holds
( ( b₃ is closed implies b₄ is closed ) & ( b₄ is closed implies b₃ is closed ) & ( b₃ is directed implies b₄ is directed ) & ( b₄ is directed implies b₃ is directed ) & ( b₃ is trivial implies b₄ is trivial ) & ( b₄ is trivial implies b₃ is trivial ) & ( b₃ is Trail-like implies b₄ is Trail-like ) & ( b₄ is Trail-like implies b₃ is Trail-like ) & ( b₃ is Path-like implies b₄ is Path-like ) & ( b₄ is Path-like implies b₃ is Path-like ) & ( b₃ is vertex-distinct implies b₄ is vertex-distinct ) & ( b₄ is vertex-distinct implies b₃ is vertex-distinct ) )

proof end;

theorem Th178: :: GLIB_001:178

for b₁, b₂ being _Graph
for b₃ being set st b₁ == b₂ & b₃ is VertexSeq of b₁ holds
b₃ is VertexSeq of b₂

proof end;

theorem Th179: :: GLIB_001:179

for b₁, b₂ being _Graph
for b₃ being set st b₁ == b₂ & b₃ is EdgeSeq of b₁ holds
b₃ is EdgeSeq of b₂

proof end;

theorem Th180: :: GLIB_001:180

for b₁, b₂ being _Graph
for b₃ being set st b₁ == b₂ & b₃ is Walk of b₁ holds
b₃ is Walk of b₂

proof end;

theorem Th181: :: GLIB_001:181

for b₁, b₂ being _Graph
for b₃, b₄, b₅ being set st b₁ == b₂ holds
b₁ .walkOf b₃,b₄,b₅ = b₂ .walkOf b₃,b₄,b₅

proof end;

theorem Th182: :: GLIB_001:182

for b₁, b₂ being _Graph
for b₃ being Walk of b₁
for b₄ being Walk of b₂ st b₁ == b₂ & b₃ = b₄ holds
( ( b₃ is closed implies b₄ is closed ) & ( b₄ is closed implies b₃ is closed ) & ( b₃ is directed implies b₄ is directed ) & ( b₄ is directed implies b₃ is directed ) & ( b₃ is trivial implies b₄ is trivial ) & ( b₄ is trivial implies b₃ is trivial ) & ( b₃ is Trail-like implies b₄ is Trail-like ) & ( b₄ is Trail-like implies b₃ is Trail-like ) & ( b₃ is Path-like implies b₄ is Path-like ) & ( b₄ is Path-like implies b₃ is Path-like ) & ( b₃ is vertex-distinct implies b₄ is vertex-distinct ) & ( b₄ is vertex-distinct implies b₃ is vertex-distinct ) )

proof end;