:: GRAPH_2 semantic presentation

scheme :: GRAPH_2:sch 1
s1{ F₁() -> Nat, F₂() -> Nat, F₃( set ) -> set , P₁[ Nat] } :

{ F₃(b₁) where B is Nat : ( F₁() <= b₁ & b₁ <= F₂() & P₁[b₁] ) } is finite

proof end;

theorem Th1: :: GRAPH_2:1

for b₁, b₂, b₃ being Nat holds
( ( b₁ + 1 <= b₂ & b₂ <= b₃ ) iff ex b₄ being Nat st
( b₁ <= b₄ & b₄ < b₃ & b₂ = b₄ + 1 ) )

proof end;

theorem Th2: :: GRAPH_2:2

for b₁, b₂ being FinSequence
for b₃ being Nat st b₁ = b₂ | (Seg b₃) holds
( len b₁ <= len b₂ & ( for b₄ being Nat st 1 <= b₄ & b₄ <= len b₁ holds
b₂ . b₄ = b₁ . b₄ ) )

proof end;

theorem Th3: :: GRAPH_2:3

for b₁, b₂ being set
for b₃ being Nat st b₁ c= Seg b₃ & b₂ c= dom (Sgm b₁) holds
(Sgm b₁) * (Sgm b₂) = Sgm (rng ((Sgm b₁) | b₂))

proof end;

Lemma4: for b₁, b₂ being Nat
for b₃ being finite set st b₃ = { b₄ where B is Nat : ( b₁ <= b₄ & b₄ <= b₁ + b₂ ) } holds
card b₃ = b₂ + 1

proof end;

theorem Th4: :: GRAPH_2:4

for b₁, b₂ being Nat holds Card { b₃ where B is Nat : ( b₁ <= b₃ & b₃ <= b₁ + b₂ ) } = b₂ + 1

proof end;

theorem Th5: :: GRAPH_2:5

for b₁, b₂, b₃ being Nat st 1 <= b₃ & b₃ <= b₁ holds
(Sgm { b₄ where B is Nat : ( b₂ + 1 <= b₄ & b₄ <= b₂ + b₁ ) } ) . b₃ = b₂ + b₃

proof end;

definition

let c₁ be FinSequence;
let c₂, c₃ be Nat;
func c₂,c₃ -cut c₁ -> FinSequence means :Def1: :: GRAPH_2:def 1
( (len a₄) + a₂ = a₃ + 1 & ( for b₁ being Nat st b₁ < len a₄ holds
a₄ . (b₁ + 1) = a₁ . (a₂ + b₁) ) ) if ( 1 <= a₂ & a₂ <= a₃ + 1 & a₃ <= len a₁ )
otherwise a₄ = {} ;
consistency ;
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines -cut GRAPH_2:def 1 :

theorem Th6: :: GRAPH_2:6

for b₁ being FinSequence
for b₂ being Nat st 1 <= b₂ & b₂ <= len b₁ holds
b₂,b₂ -cut b₁ = <*(b₁ . b₂)*>

proof end;

theorem Th7: :: GRAPH_2:7

for b₁ being FinSequence holds 1,(len b₁) -cut b₁ = b₁

proof end;

theorem Th8: :: GRAPH_2:8

for b₁ being FinSequence
for b₂, b₃, b₄ being Nat st b₂ <= b₃ & b₃ <= b₄ & b₄ <= len b₁ holds
((b₂ + 1),b₃ -cut b₁) ^ ((b₃ + 1),b₄ -cut b₁) = (b₂ + 1),b₄ -cut b₁

proof end;

theorem Th9: :: GRAPH_2:9

for b₁ being FinSequence
for b₂ being Nat st b₂ <= len b₁ holds
(1,b₂ -cut b₁) ^ ((b₂ + 1),(len b₁) -cut b₁) = b₁

proof end;

theorem Th10: :: GRAPH_2:10

for b₁ being FinSequence
for b₂, b₃ being Nat st b₂ <= b₃ & b₃ <= len b₁ holds
((1,b₂ -cut b₁) ^ ((b₂ + 1),b₃ -cut b₁)) ^ ((b₃ + 1),(len b₁) -cut b₁) = b₁

proof end;

theorem Th11: :: GRAPH_2:11

for b₁ being FinSequence
for b₂, b₃ being Nat holds rng (b₂,b₃ -cut b₁) c= rng b₁

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of c₁;
let c₃, c₄ be Nat;
redefine func -cut as c₃,c₄ -cut c₂ -> FinSequence of a₁;
coherence

proof end;

end;

theorem Th12: :: GRAPH_2:12

for b₁ being FinSequence
for b₂, b₃ being Nat st 1 <= b₂ & b₂ <= b₃ & b₃ <= len b₁ holds
( (b₂,b₃ -cut b₁) . 1 = b₁ . b₂ & (b₂,b₃ -cut b₁) . (len (b₂,b₃ -cut b₁)) = b₁ . b₃ )

proof end;

definition

let c₁, c₂ be FinSequence;
func c₁ ^' c₂ -> FinSequence equals :: GRAPH_2:def 2
a₁ ^ (2,(len a₂) -cut a₂);
correctness ;

end;

:: deftheorem Def2 defines ^' GRAPH_2:def 2 :

theorem Th13: :: GRAPH_2:13

for b₁, b₂ being FinSequence st b₁ <> {} holds
(len (b₂ ^' b₁)) + 1 = (len b₂) + (len b₁)

proof end;

theorem Th14: :: GRAPH_2:14

for b₁, b₂ being FinSequence
for b₃ being Nat st 1 <= b₃ & b₃ <= len b₁ holds
(b₁ ^' b₂) . b₃ = b₁ . b₃

proof end;

theorem Th15: :: GRAPH_2:15

for b₁, b₂ being FinSequence
for b₃ being Nat st 1 <= b₃ & b₃ < len b₁ holds
(b₂ ^' b₁) . ((len b₂) + b₃) = b₁ . (b₃ + 1)

proof end;

theorem Th16: :: GRAPH_2:16

for b₁, b₂ being FinSequence st 1 < len b₁ holds
(b₂ ^' b₁) . (len (b₂ ^' b₁)) = b₁ . (len b₁)

proof end;

theorem Th17: :: GRAPH_2:17

for b₁, b₂ being FinSequence holds rng (b₁ ^' b₂) c= (rng b₁) \/ (rng b₂)

proof end;

definition

let c₁ be set ;
let c₂, c₃ be FinSequence of c₁;
redefine func ^' as c₂ ^' c₃ -> FinSequence of a₁;
coherence

proof end;

end;

theorem Th18: :: GRAPH_2:18

for b₁, b₂ being FinSequence st b₁ <> {} & b₂ <> {} & b₁ . (len b₁) = b₂ . 1 holds
rng (b₁ ^' b₂) = (rng b₁) \/ (rng b₂)

proof end;

definition

let c₁ be FinSequence;
attr a₁ is TwoValued means :Def3: :: GRAPH_2:def 3
card (rng a₁) = 2;

end;

:: deftheorem Def3 defines TwoValued GRAPH_2:def 3 :

E19: now

set c₁ = <*1,2*>;
2 > 1 ;
hence len <*1,2*> > 1 by FINSEQ_1:61;
thus 1 <> 2 ;
thus rng <*1,2*> = rng (<*1*> ^ <*2*>) by FINSEQ_1:def 9
.= (rng <*1*>) \/ (rng <*2*>) by FINSEQ_1:44
.= {1} \/ (rng <*2*>) by FINSEQ_1:55
.= {1} \/ {2} by FINSEQ_1:55
.= {1,2} by ENUMSET1:41 ;

end;

theorem Th19: :: GRAPH_2:19

for b₁ being FinSequence holds
( b₁ is TwoValued iff ( len b₁ > 1 & ex b₂, b₃ being set st
( b₂ <> b₃ & rng b₁ = {b₂,b₃} ) ) )

proof end;

then Lemma21: <*1,2*> is TwoValued
by Lemma19;

E22: now

set c₁ = <*1,2*>;
let c₂ be Nat;
assume that
E23: 1 <= c₂ and
E24: c₂ + 1 <= len <*1,2*> ;
c₂ + 1 <= 1 + 1 by E24, FINSEQ_1:61;
then c₂ <= 1 by XREAL_1:8;
then c₂ = 1 by E23, XREAL_1:1;
then ( <*1,2*> . c₂ = 1 & <*1,2*> . (c₂ + 1) = 2 ) by FINSEQ_1:61;
hence <*1,2*> . c₂ <> <*1,2*> . (c₂ + 1) ;

end;

definition

let c₁ be FinSequence;
attr a₁ is Alternating means :Def4: :: GRAPH_2:def 4
for b₁ being Nat st 1 <= b₁ & b₁ + 1 <= len a₁ holds
a₁ . b₁ <> a₁ . (b₁ + 1);

end;

:: deftheorem Def4 defines Alternating GRAPH_2:def 4 :

Lemma24: <*1,2*> is Alternating
by Def4, Lemma22;

registration

cluster TwoValued Alternating set ;
existence by Lemma21, Lemma24;

end;

theorem Th20: :: GRAPH_2:20

for b₁, b₂ being TwoValued Alternating FinSequence st len b₁ = len b₂ & rng b₁ = rng b₂ & b₁ . 1 = b₂ . 1 holds
b₁ = b₂

proof end;

theorem Th21: :: GRAPH_2:21

for b₁, b₂ being TwoValued Alternating FinSequence st b₁ <> b₂ & len b₁ = len b₂ & rng b₁ = rng b₂ holds
for b₃ being Nat st 1 <= b₃ & b₃ <= len b₁ holds
b₁ . b₃ <> b₂ . b₃

proof end;

theorem Th22: :: GRAPH_2:22

for b₁, b₂ being TwoValued Alternating FinSequence st b₁ <> b₂ & len b₁ = len b₂ & rng b₁ = rng b₂ holds
for b₃ being TwoValued Alternating FinSequence st len b₃ = len b₁ & rng b₃ = rng b₁ & not b₃ = b₁ holds
b₃ = b₂

proof end;

theorem Th23: :: GRAPH_2:23

for b₁, b₂ being set
for b₃ being Nat st b₁ <> b₂ & b₃ > 1 holds
ex b₄ being TwoValued Alternating FinSequence st
( rng b₄ = {b₁,b₂} & len b₄ = b₃ & b₄ . 1 = b₁ )

proof end;

definition

let c₁ be set ;
let c₂ be FinSequence of c₁;
mode FinSubsequence of c₂ -> FinSubsequence means :Def5: :: GRAPH_2:def 5
a₃ c= a₂;
existence

proof end;

end;

:: deftheorem Def5 defines FinSubsequence GRAPH_2:def 5 :

theorem Th24: :: GRAPH_2:24

for b₁ being FinSubsequence st b₁ is FinSequence holds
Seq b₁ = b₁

proof end;

theorem Th25: :: GRAPH_2:25

canceled;

theorem Th26: :: GRAPH_2:26

for b₁ being FinSubsequence
for b₂, b₃, b₄, b₅, b₆ being FinSequence st rng b₂ c= dom b₁ & rng b₃ c= dom b₁ & b₄ = b₁ * b₂ & b₅ = b₁ * b₃ & b₆ = b₁ * (b₂ ^ b₃) holds
b₆ = b₄ ^ b₅

proof end;

theorem Th27: :: GRAPH_2:27

for b₁ being set
for b₂ being FinSequence of b₁
for b₃ being FinSubsequence of b₂ holds
( dom b₃ c= dom b₂ & rng b₃ c= rng b₂ )

proof end;

theorem Th28: :: GRAPH_2:28

for b₁ being set
for b₂ being FinSequence of b₁ holds b₂ is FinSubsequence of b₂

proof end;

theorem Th29: :: GRAPH_2:29

for b₁, b₂ being set
for b₃ being FinSequence of b₁
for b₄ being FinSubsequence of b₃ holds b₄ | b₂ is FinSubsequence of b₃

proof end;

theorem Th30: :: GRAPH_2:30

for b₁ being set
for b₂, b₃, b₄ being FinSequence of b₁
for b₅, b₆ being FinSubsequence of b₂
for b₇ being FinSubsequence of b₃ st Seq b₅ = b₃ & Seq b₇ = b₄ & b₆ = b₅ | (rng ((Sgm (dom b₅)) | (dom b₇))) holds
Seq b₆ = b₄

proof end;

registration

let c₁ be Graph;
cluster the Vertices of a₁ -> non empty ;
coherence by GRAPH_1:def 1;

end;

theorem Th31: :: GRAPH_2:31

for b₁ being Graph
for b₂, b₃ being Element of the Vertices of b₁
for b₄ being set st b₄ joins b₂,b₃ holds
b₄ joins b₃,b₂

proof end;

theorem Th32: :: GRAPH_2:32

for b₁ being Graph
for b₂, b₃, b₄, b₅ being Element of the Vertices of b₁
for b₆ being set st b₆ joins b₂,b₃ & b₆ joins b₄,b₅ & not ( b₂ = b₄ & b₃ = b₅ ) holds
( b₂ = b₅ & b₃ = b₄ )

proof end;

registration

let c₁ be Graph;
cluster empty Chain of a₁;
existence

proof end;

end;

definition

let c₁ be Graph;
let c₂ be set ;
func c₁ -VSet c₂ -> set equals :: GRAPH_2:def 6
{ b₁ where B is Element of the Vertices of a₁ : ex b₁ being Element of the Edges of a₁ st
( b₂ in a₂ & ( b₁ = the Source of a₁ . b₂ or b₁ = the Target of a₁ . b₂ ) ) } ;
correctness ;

end;

:: deftheorem Def6 defines -VSet GRAPH_2:def 6 :

definition

let c₁ be Graph;
let c₂ be FinSequence of the Vertices of c₁;
let c₃ be FinSequence;
pred c₂ is_vertex_seq_of c₃ means :Def7: :: GRAPH_2:def 7
( len a₂ = (len a₃) + 1 & ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₃ holds
a₃ . b₁ joins a₂ /. b₁,a₂ /. (b₁ + 1) ) );

end;

:: deftheorem Def7 defines is_vertex_seq_of GRAPH_2:def 7 :

theorem Th33: :: GRAPH_2:33

canceled;

theorem Th34: :: GRAPH_2:34

for b₁ being Graph
for b₂ being FinSequence of the Vertices of b₁
for b₃ being Chain of b₁ st b₃ <> {} & b₂ is_vertex_seq_of b₃ holds
b₁ -VSet (rng b₃) = rng b₂

proof end;

theorem Th35: :: GRAPH_2:35

for b₁ being Graph
for b₂ being Element of the Vertices of b₁ holds <*b₂*> is_vertex_seq_of {}

proof end;

theorem Th36: :: GRAPH_2:36

for b₁ being Graph
for b₂ being Chain of b₁ ex b₃ being FinSequence of the Vertices of b₁ st b₃ is_vertex_seq_of b₂

proof end;

theorem Th37: :: GRAPH_2:37

for b₁ being Graph
for b₂, b₃ being FinSequence of the Vertices of b₁
for b₄ being Chain of b₁ st b₄ <> {} & b₂ is_vertex_seq_of b₄ & b₃ is_vertex_seq_of b₄ & b₂ <> b₃ holds
( b₂ . 1 <> b₃ . 1 & ( for b₅ being FinSequence of the Vertices of b₁ holds
( not b₅ is_vertex_seq_of b₄ or b₅ = b₂ or b₅ = b₃ ) ) )

proof end;

definition

let c₁ be Graph;
let c₂ be FinSequence;
pred c₂ alternates_vertices_in c₁ means :Def8: :: GRAPH_2:def 8
( len a₂ >= 1 & Card (a₁ -VSet (rng a₂)) = 2 & ( for b₁ being Nat st b₁ in dom a₂ holds
the Source of a₁ . (a₂ . b₁) <> the Target of a₁ . (a₂ . b₁) ) );

end;

:: deftheorem Def8 defines alternates_vertices_in GRAPH_2:def 8 :

theorem Th38: :: GRAPH_2:38

for b₁ being Graph
for b₂ being FinSequence of the Vertices of b₁
for b₃ being Chain of b₁ st b₃ alternates_vertices_in b₁ & b₂ is_vertex_seq_of b₃ holds
for b₄ being Nat st b₄ in dom b₃ holds
b₂ . b₄ <> b₂ . (b₄ + 1)

proof end;

theorem Th39: :: GRAPH_2:39

for b₁ being Graph
for b₂ being FinSequence of the Vertices of b₁
for b₃ being Chain of b₁ st b₃ alternates_vertices_in b₁ & b₂ is_vertex_seq_of b₃ holds
rng b₂ = {(the Source of b₁ . (b₃ . 1)),(the Target of b₁ . (b₃ . 1))}

proof end;

theorem Th40: :: GRAPH_2:40

for b₁ being Graph
for b₂ being FinSequence of the Vertices of b₁
for b₃ being Chain of b₁ st b₃ alternates_vertices_in b₁ & b₂ is_vertex_seq_of b₃ holds
b₂ is TwoValued Alternating FinSequence

proof end;

theorem Th41: :: GRAPH_2:41

for b₁ being Graph
for b₂ being Chain of b₁ st b₂ alternates_vertices_in b₁ holds
ex b₃, b₄ being FinSequence of the Vertices of b₁ st
( b₃ <> b₄ & b₃ is_vertex_seq_of b₂ & b₄ is_vertex_seq_of b₂ & ( for b₅ being FinSequence of the Vertices of b₁ holds
( not b₅ is_vertex_seq_of b₂ or b₅ = b₃ or b₅ = b₄ ) ) )

proof end;

Lemma48: for b₁ being non empty set st ( for b₂, b₃ being set st b₂ in b₁ & b₃ in b₁ holds
b₂ = b₃ ) holds
Card b₁ = 1

proof end;

theorem Th42: :: GRAPH_2:42

for b₁ being Graph
for b₂ being FinSequence of the Vertices of b₁
for b₃ being Chain of b₁ st b₂ is_vertex_seq_of b₃ holds
( ( Card the Vertices of b₁ = 1 or ( b₃ <> {} & not b₃ alternates_vertices_in b₁ ) ) iff for b₄ being FinSequence of the Vertices of b₁ st b₄ is_vertex_seq_of b₃ holds
b₄ = b₂ )

proof end;

definition

let c₁ be Graph;
let c₂ be Chain of c₁;
assume E50: ( Card the Vertices of c₁ = 1 or ( c₂ <> {} & not c₂ alternates_vertices_in c₁ ) ) ;
func vertex-seq c₂ -> FinSequence of the Vertices of a₁ means :: GRAPH_2:def 9
a₃ is_vertex_seq_of a₂;
existence by Th36;
uniqueness by E50, Th42;

end;

:: deftheorem Def9 defines vertex-seq GRAPH_2:def 9 :

theorem Th43: :: GRAPH_2:43

for b₁ being Nat
for b₂ being Graph
for b₃, b₄ being FinSequence of the Vertices of b₂
for b₅, b₆ being Chain of b₂ st b₃ is_vertex_seq_of b₅ & b₆ = b₅ | (Seg b₁) & b₄ = b₃ | (Seg (b₁ + 1)) holds
b₄ is_vertex_seq_of b₆

proof end;

theorem Th44: :: GRAPH_2:44

for b₁ being FinSequence
for b₂, b₃ being Nat
for b₄ being Graph
for b₅ being Chain of b₄ st 1 <= b₂ & b₂ <= b₃ & b₃ <= len b₅ & b₁ = b₂,b₃ -cut b₅ holds
b₁ is Chain of b₄

proof end;

theorem Th45: :: GRAPH_2:45

for b₁, b₂ being Nat
for b₃ being Graph
for b₄, b₅ being FinSequence of the Vertices of b₃
for b₆, b₇ being Chain of b₃ st 1 <= b₁ & b₁ <= b₂ & b₂ <= len b₆ & b₇ = b₁,b₂ -cut b₆ & b₄ is_vertex_seq_of b₆ & b₅ = b₁,(b₂ + 1) -cut b₄ holds
b₅ is_vertex_seq_of b₇

proof end;

theorem Th46: :: GRAPH_2:46

for b₁ being Graph
for b₂, b₃ being FinSequence of the Vertices of b₁
for b₄, b₅ being Chain of b₁ st b₂ is_vertex_seq_of b₄ & b₃ is_vertex_seq_of b₅ & b₂ . (len b₂) = b₃ . 1 holds
b₄ ^ b₅ is Chain of b₁

proof end;

theorem Th47: :: GRAPH_2:47

for b₁ being Graph
for b₂, b₃, b₄ being FinSequence of the Vertices of b₁
for b₅, b₆, b₇ being Chain of b₁ st b₂ is_vertex_seq_of b₅ & b₃ is_vertex_seq_of b₆ & b₂ . (len b₂) = b₃ . 1 & b₇ = b₅ ^ b₆ & b₄ = b₂ ^' b₃ holds
b₄ is_vertex_seq_of b₇

proof end;

Lemma55: for b₁ being Graph
for b₂ being Element of the Vertices of b₁ holds <*b₂*> is_vertex_seq_of {}

proof end;

definition

let c₁ be Graph;
let c₂ be Chain of c₁;
attr a₂ is simple means :Def10: :: GRAPH_2:def 10
ex b₁ being FinSequence of the Vertices of a₁ st
( b₁ is_vertex_seq_of a₂ & ( for b₂, b₃ being Nat st 1 <= b₂ & b₂ < b₃ & b₃ <= len b₁ & b₁ . b₂ = b₁ . b₃ holds
( b₂ = 1 & b₃ = len b₁ ) ) );

end;

:: deftheorem Def10 defines simple GRAPH_2:def 10 :

registration

let c₁ be Graph;
cluster simple Chain of a₁;
existence

proof end;

end;

theorem Th48: :: GRAPH_2:48

canceled;

theorem Th49: :: GRAPH_2:49

for b₁ being Nat
for b₂ being Graph
for b₃ being simple Chain of b₂ holds b₃ | (Seg b₁) is simple Chain of b₂

proof end;

theorem Th50: :: GRAPH_2:50

for b₁ being Graph
for b₂, b₃ being FinSequence of the Vertices of b₁
for b₄ being simple Chain of b₁ st 2 < len b₄ & b₂ is_vertex_seq_of b₄ & b₃ is_vertex_seq_of b₄ holds
b₂ = b₃

proof end;

theorem Th51: :: GRAPH_2:51

for b₁ being Graph
for b₂ being FinSequence of the Vertices of b₁
for b₃ being simple Chain of b₁ st b₂ is_vertex_seq_of b₃ holds
for b₄, b₅ being Nat st 1 <= b₄ & b₄ < b₅ & b₅ <= len b₂ & b₂ . b₄ = b₂ . b₅ holds
( b₄ = 1 & b₅ = len b₂ )

proof end;

theorem Th52: :: GRAPH_2:52

for b₁ being Graph
for b₂ being FinSequence of the Vertices of b₁
for b₃ being Chain of b₁ st b₃ is not simple Chain of b₁ & b₂ is_vertex_seq_of b₃ holds
ex b₄ being FinSubsequence of b₃ex b₅ being FinSubsequence of b₂ex b₆ being Chain of b₁ex b₇ being FinSequence of the Vertices of b₁ st
( len b₆ < len b₃ & b₇ is_vertex_seq_of b₆ & len b₇ < len b₂ & b₂ . 1 = b₇ . 1 & b₂ . (len b₂) = b₇ . (len b₇) & Seq b₄ = b₆ & Seq b₅ = b₇ )

proof end;

theorem Th53: :: GRAPH_2:53

for b₁ being Graph
for b₂ being FinSequence of the Vertices of b₁
for b₃ being Chain of b₁ st b₂ is_vertex_seq_of b₃ holds
ex b₄ being FinSubsequence of b₃ex b₅ being FinSubsequence of b₂ex b₆ being simple Chain of b₁ex b₇ being FinSequence of the Vertices of b₁ st
( Seq b₄ = b₆ & Seq b₅ = b₇ & b₇ is_vertex_seq_of b₆ & b₂ . 1 = b₇ . 1 & b₂ . (len b₂) = b₇ . (len b₇) )

proof end;

registration

let c₁ be Graph;
cluster empty -> V5 Chain of a₁;
correctness ;

end;

theorem Th54: :: GRAPH_2:54

for b₁ being FinSequence
for b₂ being Nat
for b₃ being Graph st b₁ is Path of b₃ holds
b₁ | (Seg b₂) is Path of b₃

proof end;

registration

let c₁ be Graph;
cluster simple Chain of a₁;
existence

proof end;

end;

theorem Th55: :: GRAPH_2:55

for b₁ being Graph
for b₂ being simple Chain of b₁ st 2 < len b₂ holds
b₂ is Path of b₁

proof end;

theorem Th56: :: GRAPH_2:56

for b₁ being Graph
for b₂ being simple Chain of b₁ holds
( b₂ is Path of b₁ iff ( len b₂ = 0 or len b₂ = 1 or b₂ . 1 <> b₂ . 2 ) )

proof end;

registration

let c₁ be Graph;
cluster empty -> oriented Chain of a₁;
correctness

proof end;

end;

definition

let c₁ be Graph;
let c₂ be oriented Chain of c₁;
assume E59: c₂ <> {} ;
func vertex-seq c₂ -> FinSequence of the Vertices of a₁ means :: GRAPH_2:def 11
( a₃ is_vertex_seq_of a₂ & a₃ . 1 = the Source of a₁ . (a₂ . 1) );
existence

proof end;

uniqueness by E59, Th37;

end;

:: deftheorem Def11 defines vertex-seq GRAPH_2:def 11 :