:: GRAPH_4 semantic presentation

definition
let c1 be Graph;
let c2, c3 be Element of the Vertices of c1;
let c4 be set ;
pred c4 orientedly_joins c2,c3 means :Def1: :: GRAPH_4:def 1
( the Source of a1 . a4 = a2 & the Target of a1 . a4 = a3 );
end;

:: deftheorem Def1 defines orientedly_joins GRAPH_4:def 1 :
for b1 being Graph
for b2, b3 being Element of the Vertices of b1
for b4 being set holds
( b4 orientedly_joins b2,b3 iff ( the Source of b1 . b4 = b2 & the Target of b1 . b4 = b3 ) );

theorem Th1: :: GRAPH_4:1
for b1 being set
for b2 being Graph
for b3, b4 being Element of the Vertices of b2 st b1 orientedly_joins b3,b4 holds
b1 joins b3,b4
proof end;

definition
let c1 be Graph;
let c2, c3 be Element of the Vertices of c1;
pred c2,c3 are_orientedly_incident means :: GRAPH_4:def 2
ex b1 being set st
( b1 in the Edges of a1 & b1 orientedly_joins a2,a3 );
end;

:: deftheorem Def2 defines are_orientedly_incident GRAPH_4:def 2 :
for b1 being Graph
for b2, b3 being Element of the Vertices of b1 holds
( b2,b3 are_orientedly_incident iff ex b4 being set st
( b4 in the Edges of b1 & b4 orientedly_joins b2,b3 ) );

theorem Th2: :: GRAPH_4:2
for b1 being set
for b2 being Graph
for b3, b4, b5, b6 being Element of the Vertices of b2 st b1 orientedly_joins b3,b4 & b1 orientedly_joins b5,b6 holds
( b3 = b5 & b4 = b6 )
proof end;

registration
let c1 be Graph;
cluster empty oriented Chain of a1;
existence
ex b1 being Chain of c1 st
( b1 is empty & b1 is oriented )
proof end;
end;

definition
let c1 be Graph;
let c2 be set ;
func c1 -SVSet c2 -> set equals :: GRAPH_4:def 3
{ b1 where B is Element of the Vertices of a1 : ex b1 being Element of the Edges of a1 st
( b2 in a2 & b1 = the Source of a1 . b2 ) } ;
correctness
coherence
{ b1 where B is Element of the Vertices of c1 : ex b1 being Element of the Edges of c1 st
( b2 in c2 & b1 = the Source of c1 . b2 ) } is set ;
;
end;

:: deftheorem Def3 defines -SVSet GRAPH_4:def 3 :
for b1 being Graph
for b2 being set holds b1 -SVSet b2 = { b3 where B is Element of the Vertices of b1 : ex b1 being Element of the Edges of b1 st
( b4 in b2 & b3 = the Source of b1 . b4 ) } ;

definition
let c1 be Graph;
let c2 be set ;
func c1 -TVSet c2 -> set equals :: GRAPH_4:def 4
{ b1 where B is Element of the Vertices of a1 : ex b1 being Element of the Edges of a1 st
( b2 in a2 & b1 = the Target of a1 . b2 ) } ;
correctness
coherence
{ b1 where B is Element of the Vertices of c1 : ex b1 being Element of the Edges of c1 st
( b2 in c2 & b1 = the Target of c1 . b2 ) } is set ;
;
end;

:: deftheorem Def4 defines -TVSet GRAPH_4:def 4 :
for b1 being Graph
for b2 being set holds b1 -TVSet b2 = { b3 where B is Element of the Vertices of b1 : ex b1 being Element of the Edges of b1 st
( b4 in b2 & b3 = the Target of b1 . b4 ) } ;

theorem Th3: :: GRAPH_4:3
canceled;

theorem Th4: :: GRAPH_4:4
for b1 being Graph holds
( b1 -SVSet {} = {} & b1 -TVSet {} = {} )
proof end;

definition
let c1 be Graph;
let c2 be FinSequence of the Vertices of c1;
let c3 be FinSequence;
pred c2 is_oriented_vertex_seq_of c3 means :Def5: :: GRAPH_4:def 5
( len a2 = (len a3) + 1 & ( for b1 being Nat st 1 <= b1 & b1 <= len a3 holds
a3 . b1 orientedly_joins a2 /. b1,a2 /. (b1 + 1) ) );
end;

:: deftheorem Def5 defines is_oriented_vertex_seq_of GRAPH_4:def 5 :
for b1 being Graph
for b2 being FinSequence of the Vertices of b1
for b3 being FinSequence holds
( b2 is_oriented_vertex_seq_of b3 iff ( len b2 = (len b3) + 1 & ( for b4 being Nat st 1 <= b4 & b4 <= len b3 holds
b3 . b4 orientedly_joins b2 /. b4,b2 /. (b4 + 1) ) ) );

theorem Th5: :: GRAPH_4:5
for b1 being Graph
for b2 being FinSequence of the Vertices of b1
for b3 being oriented Chain of b1 st b2 is_oriented_vertex_seq_of b3 holds
b2 is_vertex_seq_of b3
proof end;

theorem Th6: :: GRAPH_4:6
for b1 being Graph
for b2 being FinSequence of the Vertices of b1
for b3 being oriented Chain of b1 st b2 is_oriented_vertex_seq_of b3 holds
b1 -SVSet (rng b3) c= rng b2
proof end;

theorem Th7: :: GRAPH_4:7
for b1 being Graph
for b2 being FinSequence of the Vertices of b1
for b3 being oriented Chain of b1 st b2 is_oriented_vertex_seq_of b3 holds
b1 -TVSet (rng b3) c= rng b2
proof end;

theorem Th8: :: GRAPH_4:8
for b1 being Graph
for b2 being FinSequence of the Vertices of b1
for b3 being oriented Chain of b1 st b3 <> {} & b2 is_oriented_vertex_seq_of b3 holds
rng b2 c= (b1 -SVSet (rng b3)) \/ (b1 -TVSet (rng b3))
proof end;

theorem Th9: :: GRAPH_4:9
for b1 being Graph
for b2 being Element of the Vertices of b1 holds <*b2*> is_oriented_vertex_seq_of {}
proof end;

theorem Th10: :: GRAPH_4:10
for b1 being Graph
for b2 being oriented Chain of b1 ex b3 being FinSequence of the Vertices of b1 st b3 is_oriented_vertex_seq_of b2
proof end;

theorem Th11: :: GRAPH_4:11
for b1 being Graph
for b2, b3 being FinSequence of the Vertices of b1
for b4 being oriented Chain of b1 st b4 <> {} & b2 is_oriented_vertex_seq_of b4 & b3 is_oriented_vertex_seq_of b4 holds
b2 = b3
proof end;

definition
let c1 be Graph;
let c2 be oriented Chain of c1;
assume E8: c2 <> {} ;
func oriented-vertex-seq c2 -> FinSequence of the Vertices of a1 means :: GRAPH_4:def 6
a3 is_oriented_vertex_seq_of a2;
existence
ex b1 being FinSequence of the Vertices of c1 st b1 is_oriented_vertex_seq_of c2 by Th10;
uniqueness
for b1, b2 being FinSequence of the Vertices of c1 st b1 is_oriented_vertex_seq_of c2 & b2 is_oriented_vertex_seq_of c2 holds
b1 = b2 by E8, Th11;
end;

:: deftheorem Def6 defines oriented-vertex-seq GRAPH_4:def 6 :
for b1 being Graph
for b2 being oriented Chain of b1 st b2 <> {} holds
for b3 being FinSequence of the Vertices of b1 holds
( b3 = oriented-vertex-seq b2 iff b3 is_oriented_vertex_seq_of b2 );

theorem Th12: :: GRAPH_4:12
for b1 being Nat
for b2 being Graph
for b3, b4 being FinSequence of the Vertices of b2
for b5, b6 being oriented Chain of b2 st b3 is_oriented_vertex_seq_of b5 & b6 = b5 | (Seg b1) & b4 = b3 | (Seg (b1 + 1)) holds
b4 is_oriented_vertex_seq_of b6
proof end;

theorem Th13: :: GRAPH_4:13
for b1 being FinSequence
for b2, b3 being Nat
for b4 being Graph
for b5 being oriented Chain of b4 st 1 <= b2 & b2 <= b3 & b3 <= len b5 & b1 = b2,b3 -cut b5 holds
b1 is oriented Chain of b4
proof end;

theorem Th14: :: GRAPH_4:14
for b1, b2 being Nat
for b3 being Graph
for b4, b5 being FinSequence of the Vertices of b3
for b6, b7 being oriented Chain of b3 st 1 <= b1 & b1 <= b2 & b2 <= len b6 & b7 = b1,b2 -cut b6 & b4 is_oriented_vertex_seq_of b6 & b5 = b1,(b2 + 1) -cut b4 holds
b5 is_oriented_vertex_seq_of b7
proof end;

theorem Th15: :: GRAPH_4:15
for b1 being Graph
for b2, b3 being FinSequence of the Vertices of b1
for b4, b5 being oriented Chain of b1 st b2 is_oriented_vertex_seq_of b4 & b3 is_oriented_vertex_seq_of b5 & b2 . (len b2) = b3 . 1 holds
b4 ^ b5 is oriented Chain of b1
proof end;

theorem Th16: :: GRAPH_4:16
for b1 being Graph
for b2, b3, b4 being FinSequence of the Vertices of b1
for b5, b6, b7 being oriented Chain of b1 st b2 is_oriented_vertex_seq_of b5 & b3 is_oriented_vertex_seq_of b6 & b2 . (len b2) = b3 . 1 & b7 = b5 ^ b6 & b4 = b2 ^' b3 holds
b4 is_oriented_vertex_seq_of b7
proof end;

Lemma12: for b1 being Graph
for b2 being Element of the Vertices of b1 holds <*b2*> is_oriented_vertex_seq_of {}
proof end;

definition
let c1 be Graph;
let c2 be oriented Chain of c1;
attr a2 is Simple means :Def7: :: GRAPH_4:def 7
ex b1 being FinSequence of the Vertices of a1 st
( b1 is_oriented_vertex_seq_of a2 & ( for b2, b3 being Nat st 1 <= b2 & b2 < b3 & b3 <= len b1 & b1 . b2 = b1 . b3 holds
( b2 = 1 & b3 = len b1 ) ) );
end;

:: deftheorem Def7 defines Simple GRAPH_4:def 7 :
for b1 being Graph
for b2 being oriented Chain of b1 holds
( b2 is Simple iff ex b3 being FinSequence of the Vertices of b1 st
( b3 is_oriented_vertex_seq_of b2 & ( for b4, b5 being Nat st 1 <= b4 & b4 < b5 & b5 <= len b3 & b3 . b4 = b3 . b5 holds
( b4 = 1 & b5 = len b3 ) ) ) );

registration
let c1 be Graph;
cluster oriented Simple Chain of a1;
existence
ex b1 being oriented Chain of c1 st b1 is Simple
proof end;
end;

registration
let c1 be Graph;
cluster oriented simple Chain of a1;
existence
ex b1 being Chain of c1 st
( b1 is oriented & b1 is simple )
proof end;
end;

theorem Th17: :: GRAPH_4:17
canceled;

theorem Th18: :: GRAPH_4:18
for b1 being Nat
for b2 being Graph
for b3 being oriented Chain of b2 holds b3 | (Seg b1) is oriented Chain of b2
proof end;

theorem Th19: :: GRAPH_4:19
for b1 being Nat
for b2 being Graph
for b3 being oriented simple Chain of b2 holds b3 | (Seg b1) is oriented simple Chain of b2 by Th18, GRAPH_2:49;

theorem Th20: :: GRAPH_4:20
for b1 being Graph
for b2 being oriented simple Chain of b1
for b3 being oriented Chain of b1 st b3 = b2 holds
b3 is Simple
proof end;

theorem Th21: :: GRAPH_4:21
for b1 being Graph
for b2 being oriented Simple Chain of b1 holds b2 is oriented simple Chain of b1
proof end;

theorem Th22: :: GRAPH_4:22
for b1 being Graph
for b2 being FinSequence of the Vertices of b1
for b3 being oriented Chain of b1 st not b3 is Simple & b2 is_oriented_vertex_seq_of b3 holds
ex b4 being FinSubsequence of b3ex b5 being FinSubsequence of b2ex b6 being oriented Chain of b1ex b7 being FinSequence of the Vertices of b1 st
( len b6 < len b3 & b7 is_oriented_vertex_seq_of b6 & len b7 < len b2 & b2 . 1 = b7 . 1 & b2 . (len b2) = b7 . (len b7) & Seq b4 = b6 & Seq b5 = b7 )
proof end;

theorem Th23: :: GRAPH_4:23
for b1 being Graph
for b2 being FinSequence of the Vertices of b1
for b3 being oriented Chain of b1 st b2 is_oriented_vertex_seq_of b3 holds
ex b4 being FinSubsequence of b3ex b5 being FinSubsequence of b2ex b6 being oriented simple Chain of b1ex b7 being FinSequence of the Vertices of b1 st
( Seq b4 = b6 & Seq b5 = b7 & b7 is_oriented_vertex_seq_of b6 & b2 . 1 = b7 . 1 & b2 . (len b2) = b7 . (len b7) )
proof end;

registration
let c1 be Graph;
cluster empty oriented -> V6 oriented Chain of a1;
correctness
coherence
for b1 being oriented Chain of c1 st b1 is empty holds
b1 is one-to-one;
;
end;

theorem Th24: :: GRAPH_4:24
for b1 being FinSequence
for b2 being Nat
for b3 being Graph st b1 is OrientedPath of b3 holds
b1 | (Seg b2) is OrientedPath of b3
proof end;

theorem Th25: :: GRAPH_4:25
for b1 being Graph
for b2 being oriented simple Chain of b1 holds b2 is OrientedPath of b1
proof end;

theorem Th26: :: GRAPH_4:26
for b1 being Graph
for b2 being FinSequence holds
( ( b2 is oriented Simple Chain of b1 implies b2 is oriented simple Chain of b1 ) & ( b2 is oriented simple Chain of b1 implies b2 is oriented Simple Chain of b1 ) & ( b2 is oriented simple Chain of b1 implies b2 is OrientedPath of b1 ) ) by Th20, Th21, Th25;