:: GRAPH_1 semantic presentation

definition

attr a₁ is strict;
struct MultiGraphStruct -> ;
aggr MultiGraphStruct(# Vertices, Edges, Source, Target #) -> MultiGraphStruct ;
sel Vertices c₁ -> set ;
sel Edges c₁ -> set ;
sel Source c₁ -> Function of the Edges of a₁,the Vertices of a₁;
sel Target c₁ -> Function of the Edges of a₁,the Vertices of a₁;

end;

set c₁ = {1,2};

reconsider c₂ = {} as Function of {} ,{1,2} by FUNCT_2:55, RELAT_1:60;

definition

let c₃ be MultiGraphStruct ;
attr a₁ is Graph-like means :Def1: :: GRAPH_1:def 1
the Vertices of a₁ is non empty set ;

end;

:: deftheorem Def1 defines Graph-like GRAPH_1:def 1 :

registration

cluster strict Graph-like MultiGraphStruct ;
existence

proof end;

end;

definition

mode Graph is Graph-like MultiGraphStruct ;

end;

Lemma2: for b₁ being Graph holds
( dom the Source of b₁ = the Edges of b₁ & dom the Target of b₁ = the Edges of b₁ & rng the Source of b₁ c= the Vertices of b₁ & rng the Target of b₁ c= the Vertices of b₁ )

proof end;

Lemma3: for b₁ being Graph
for b₂ being Element of the Vertices of b₁ holds b₂ in the Vertices of b₁

proof end;

definition

let c₃, c₄ be Graph;
assume E4: ( the Source of c₃ tolerates the Source of c₄ & the Target of c₃ tolerates the Target of c₄ ) ;
func c₁ \/ c₂ -> strict Graph means :Def2: :: GRAPH_1:def 2
( the Vertices of a₃ = the Vertices of a₁ \/ the Vertices of a₂ & the Edges of a₃ = the Edges of a₁ \/ the Edges of a₂ & ( for b₁ being set st b₁ in the Edges of a₁ holds
( the Source of a₃ . b₁ = the Source of a₁ . b₁ & the Target of a₃ . b₁ = the Target of a₁ . b₁ ) ) & ( for b₁ being set st b₁ in the Edges of a₂ holds
( the Source of a₃ . b₁ = the Source of a₂ . b₁ & the Target of a₃ . b₁ = the Target of a₂ . b₁ ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines \/ GRAPH_1:def 2 :

definition

let c₃, c₄, c₅ be Graph;
pred c₁ is_sum_of c₂,c₃ means :Def3: :: GRAPH_1:def 3
( the Target of a₂ tolerates the Target of a₃ & the Source of a₂ tolerates the Source of a₃ & MultiGraphStruct(# the Vertices of a₁,the Edges of a₁,the Source of a₁,the Target of a₁ #) = a₂ \/ a₃ );

end;

:: deftheorem Def3 defines is_sum_of GRAPH_1:def 3 :

definition

let c₃ be Graph;
attr a₁ is oriented means :Def4: :: GRAPH_1:def 4
for b₁, b₂ being set st b₁ in the Edges of a₁ & b₂ in the Edges of a₁ & the Source of a₁ . b₁ = the Source of a₁ . b₂ & the Target of a₁ . b₁ = the Target of a₁ . b₂ holds
b₁ = b₂;
attr a₁ is non-multi means :Def5: :: GRAPH_1:def 5
for b₁, b₂ being set st b₁ in the Edges of a₁ & b₂ in the Edges of a₁ & ( ( the Source of a₁ . b₁ = the Source of a₁ . b₂ & the Target of a₁ . b₁ = the Target of a₁ . b₂ ) or ( the Source of a₁ . b₁ = the Target of a₁ . b₂ & the Source of a₁ . b₂ = the Target of a₁ . b₁ ) ) holds
b₁ = b₂;
attr a₁ is simple means :Def6: :: GRAPH_1:def 6
for b₁ being set holds
( not b₁ in the Edges of a₁ or not the Source of a₁ . b₁ = the Target of a₁ . b₁ );
attr a₁ is connected means :Def7: :: GRAPH_1:def 7
for b₁, b₂ being Graph holds
( not the Vertices of b₁ misses the Vertices of b₂ or not a₁ is_sum_of b₁,b₂ );

end;

:: deftheorem Def4 defines oriented GRAPH_1:def 4 :

:: deftheorem Def5 defines non-multi GRAPH_1:def 5 :

:: deftheorem Def6 defines simple GRAPH_1:def 6 :

:: deftheorem Def7 defines connected GRAPH_1:def 7 :

definition

let c₃ be MultiGraphStruct ;
attr a₁ is finite means :Def8: :: GRAPH_1:def 8
( the Vertices of a₁ is finite & the Edges of a₁ is finite );

end;

:: deftheorem Def8 defines finite GRAPH_1:def 8 :

registration

cluster finite MultiGraphStruct ;
existence

proof end;

cluster oriented non-multi simple connected finite MultiGraphStruct ;
existence

proof end;

end;

definition

let c₃ be Graph;
let c₄, c₅ be Element of the Vertices of c₃;
let c₆ be set ;
pred c₄ joins c₂,c₃ means :: GRAPH_1:def 9
( ( the Source of a₁ . a₄ = a₂ & the Target of a₁ . a₄ = a₃ ) or ( the Source of a₁ . a₄ = a₃ & the Target of a₁ . a₄ = a₂ ) );

end;

:: deftheorem Def9 defines joins GRAPH_1:def 9 :

definition

let c₃ be Graph;
let c₄, c₅ be Element of the Vertices of c₃;
pred c₂,c₃ are_incydent means :: GRAPH_1:def 10
ex b₁ being set st
( b₁ in the Edges of a₁ & b₁ joins a₂,a₃ );

end;

:: deftheorem Def10 defines are_incydent GRAPH_1:def 10 :

definition

let c₃ be Graph;
mode Chain of c₁ -> FinSequence means :Def11: :: GRAPH_1:def 11
( ( for b₁ being Nat st 1 <= b₁ & b₁ <= len a₂ holds
a₂ . b₁ in the Edges of a₁ ) & ex b₁ being FinSequence st
( len b₁ = (len a₂) + 1 & ( for b₂ being Nat st 1 <= b₂ & b₂ <= len b₁ holds
b₁ . b₂ in the Vertices of a₁ ) & ( for b₂ being Nat st 1 <= b₂ & b₂ <= len a₂ holds
ex b₃, b₄ being Element of the Vertices of a₁ st
( b₃ = b₁ . b₂ & b₄ = b₁ . (b₂ + 1) & a₂ . b₂ joins b₃,b₄ ) ) ) );
existence

proof end;

end;

:: deftheorem Def11 defines Chain GRAPH_1:def 11 :

Lemma12: for b₁ being Graph holds {} is Chain of b₁

proof end;

definition

let c₃ be Graph;
redefine mode Chain as Chain of c₁ -> FinSequence of the Edges of a₁;
coherence

proof end;

end;

definition

let c₃ be Graph;
let c₄ be Chain of c₃;
attr a₂ is oriented means :Def12: :: GRAPH_1:def 12
for b₁ being Nat st 1 <= b₁ & b₁ < len a₂ holds
the Source of a₁ . (a₂ . (b₁ + 1)) = the Target of a₁ . (a₂ . b₁);

end;

:: deftheorem Def12 defines oriented GRAPH_1:def 12 :

registration

let c₃ be Graph;
cluster oriented Chain of a₁;
existence

proof end;

end;

Lemma14: for b₁ being Graph holds {} is oriented Chain of b₁

proof end;

definition

let c₃ be Graph;
let c₄ be Chain of c₃;
redefine attr one-to-one as a₂ is one-to-one means :: GRAPH_1:def 13
for b₁, b₂ being Nat st 1 <= b₁ & b₁ < b₂ & b₂ <= len a₂ holds
a₂ . b₁ <> a₂ . b₂;
compatibility

proof end;

end;

:: deftheorem Def13 defines one-to-one GRAPH_1:def 13 :

registration

let c₃ be Graph;
cluster V5 Chain of a₁;
existence

proof end;

end;

definition

let c₃ be Graph;
mode Path of a₁ is V5 Chain of a₁;

end;

registration

let c₃ be Graph;
cluster V5 oriented Chain of a₁;
existence

proof end;

end;

definition

let c₃ be Graph;
mode OrientedPath of a₁ is V5 oriented Chain of a₁;

end;

definition

let c₃ be Graph;
let c₄ be Path of c₃;
canceled;
attr a₂ is cyclic means :Def15: :: GRAPH_1:def 15
ex b₁ being FinSequence st
( len b₁ = (len a₂) + 1 & ( for b₂ being Nat st 1 <= b₂ & b₂ <= len b₁ holds
b₁ . b₂ in the Vertices of a₁ ) & ( for b₂ being Nat st 1 <= b₂ & b₂ <= len a₂ holds
ex b₃, b₄ being Element of the Vertices of a₁ st
( b₃ = b₁ . b₂ & b₄ = b₁ . (b₂ + 1) & a₂ . b₂ joins b₃,b₄ ) ) & b₁ . 1 = b₁ . (len b₁) );

end;

:: deftheorem Def14 GRAPH_1:def 14 :

:: deftheorem Def15 defines cyclic GRAPH_1:def 15 :

registration

let c₃ be Graph;
cluster cyclic Chain of a₁;
existence

proof end;

end;

definition

let c₃ be Graph;
mode Cycle of a₁ is cyclic Path of a₁;

end;

Lemma16: for b₁ being Graph holds {} is Cycle of b₁

proof end;

registration

let c₃ be Graph;
cluster cyclic Chain of a₁;
existence

proof end;

end;

definition

let c₃ be Graph;
mode OrientedCycle of a₁ is cyclic OrientedPath of a₁;

end;

Lemma17: for b₁ being Graph
for b₂ being set st b₂ in the Edges of b₁ holds
( the Source of b₁ . b₂ in the Vertices of b₁ & the Target of b₁ . b₂ in the Vertices of b₁ )

proof end;

definition

let c₃ be Graph;
canceled;
mode Subgraph of c₁ -> Graph means :Def17: :: GRAPH_1:def 17
( the Vertices of a₂ c= the Vertices of a₁ & the Edges of a₂ c= the Edges of a₁ & ( for b₁ being set st b₁ in the Edges of a₂ holds
( the Source of a₂ . b₁ = the Source of a₁ . b₁ & the Target of a₂ . b₁ = the Target of a₁ . b₁ & the Source of a₁ . b₁ in the Vertices of a₂ & the Target of a₁ . b₁ in the Vertices of a₂ ) ) );
existence

proof end;

end;

:: deftheorem Def16 GRAPH_1:def 16 :

:: deftheorem Def17 defines Subgraph GRAPH_1:def 17 :

registration

let c₃ be Graph;
cluster strict Subgraph of a₁;
existence

proof end;

end;

definition

let c₃ be finite Graph;
func VerticesCount c₁ -> Nat means :: GRAPH_1:def 18
ex b₁ being finite set st
( b₁ = the Vertices of a₁ & a₂ = card b₁ );
existence

proof end;

uniqueness ;
func EdgesCount c₁ -> Nat means :: GRAPH_1:def 19
ex b₁ being finite set st
( b₁ = the Edges of a₁ & a₂ = card b₁ );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def18 defines VerticesCount GRAPH_1:def 18 :

:: deftheorem Def19 defines EdgesCount GRAPH_1:def 19 :

definition

let c₃ be finite Graph;
let c₄ be Element of the Vertices of c₃;
func EdgesIn c₂ -> Nat means :: GRAPH_1:def 20
ex b₁ being finite set st
( ( for b₂ being set holds
( b₂ in b₁ iff ( b₂ in the Edges of a₁ & the Target of a₁ . b₂ = a₂ ) ) ) & a₃ = card b₁ );
existence

proof end;

uniqueness

proof end;

func EdgesOut c₂ -> Nat means :: GRAPH_1:def 21
ex b₁ being finite set st
( ( for b₂ being set holds
( b₂ in b₁ iff ( b₂ in the Edges of a₁ & the Source of a₁ . b₂ = a₂ ) ) ) & a₃ = card b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def20 defines EdgesIn GRAPH_1:def 20 :

:: deftheorem Def21 defines EdgesOut GRAPH_1:def 21 :

definition

let c₃ be finite Graph;
let c₄ be Element of the Vertices of c₃;
func Degree c₂ -> Nat equals :: GRAPH_1:def 22
(EdgesIn a₂) + (EdgesOut a₂);
correctness ;

end;

:: deftheorem Def22 defines Degree GRAPH_1:def 22 :

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

proof end;

Lemma20: for b₁ being Graph
for b₂, b₃ being strict Subgraph of b₁ st the Vertices of b₂ = the Vertices of b₃ & the Edges of b₂ = the Edges of b₃ holds
b₂ = b₃

proof end;

definition

let c₃, c₄ be Graph;
pred c₁ c= c₂ means :Def23: :: GRAPH_1:def 23
a₁ is Subgraph of a₂;
reflexivity

proof end;

end;

:: deftheorem Def23 defines c= GRAPH_1:def 23 :

Lemma22: for b₁ being Graph
for b₂ being Subgraph of b₁ holds
( the Source of b₂ in PFuncs the Edges of b₁,the Vertices of b₁ & the Target of b₂ in PFuncs the Edges of b₁,the Vertices of b₁ )

proof end;

definition

let c₃ be Graph;
func bool c₁ -> set means :Def24: :: GRAPH_1:def 24
for b₁ being set holds
( b₁ in a₂ iff b₁ is strict Subgraph of a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def24 defines bool GRAPH_1:def 24 :

scheme :: GRAPH_1:sch 1
s1{ F₁() -> Graph, P₁[ set ] } :

ex b₁ being set st
for b₂ being set holds
( b₂ in b₁ iff ( b₂ is strict Subgraph of F₁() & P₁[b₂] ) )

proof end;

theorem Th1: :: GRAPH_1:1

for b₁ being Graph holds
( dom the Source of b₁ = the Edges of b₁ & dom the Target of b₁ = the Edges of b₁ & rng the Source of b₁ c= the Vertices of b₁ & rng the Target of b₁ c= the Vertices of b₁ ) by Lemma2;

theorem Th2: :: GRAPH_1:2

for b₁ being Graph
for b₂ being Element of the Vertices of b₁ holds b₂ in the Vertices of b₁ by Lemma3;

theorem Th3: :: GRAPH_1:3

for b₁ being Graph
for b₂ being set st b₂ in the Edges of b₁ holds
( the Source of b₁ . b₂ in the Vertices of b₁ & the Target of b₁ . b₂ in the Vertices of b₁ ) by Lemma17;

theorem Th4: :: GRAPH_1:4

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

theorem Th5: :: GRAPH_1:5

for b₁, b₂ being Graph st b₁ c= b₂ holds
( the Source of b₁ c= the Source of b₂ & the Target of b₁ c= the Target of b₂ )

proof end;

theorem Th6: :: GRAPH_1:6

for b₁, b₂ being Graph st the Source of b₁ tolerates the Source of b₂ & the Target of b₁ tolerates the Target of b₂ holds
( the Source of (b₁ \/ b₂) = the Source of b₁ \/ the Source of b₂ & the Target of (b₁ \/ b₂) = the Target of b₁ \/ the Target of b₂ )

proof end;

theorem Th7: :: GRAPH_1:7

for b₁ being strict Graph holds b₁ = b₁ \/ b₁

proof end;

theorem Th8: :: GRAPH_1:8

for b₁, b₂ being Graph st the Source of b₁ tolerates the Source of b₂ & the Target of b₁ tolerates the Target of b₂ holds
b₁ \/ b₂ = b₂ \/ b₁

proof end;

theorem Th9: :: GRAPH_1:9

for b₁, b₂, b₃ being Graph st the Source of b₁ tolerates the Source of b₂ & the Target of b₁ tolerates the Target of b₂ & the Source of b₁ tolerates the Source of b₃ & the Target of b₁ tolerates the Target of b₃ & the Source of b₂ tolerates the Source of b₃ & the Target of b₂ tolerates the Target of b₃ holds
(b₁ \/ b₂) \/ b₃ = b₁ \/ (b₂ \/ b₃)

proof end;

theorem Th10: :: GRAPH_1:10

for b₁, b₂, b₃ being Graph st b₁ is_sum_of b₂,b₃ holds
b₁ is_sum_of b₃,b₂

proof end;

theorem Th11: :: GRAPH_1:11

for b₁ being strict Graph holds b₁ is_sum_of b₁,b₁

proof end;

theorem Th12: :: GRAPH_1:12

for b₁, b₂ being Graph st ex b₃ being Graph st
( b₁ c= b₃ & b₂ c= b₃ ) holds
b₁ \/ b₂ = b₂ \/ b₁

proof end;

theorem Th13: :: GRAPH_1:13

for b₁, b₂, b₃ being Graph st ex b₄ being Graph st
( b₁ c= b₄ & b₂ c= b₄ & b₃ c= b₄ ) holds
(b₁ \/ b₂) \/ b₃ = b₁ \/ (b₂ \/ b₃)

proof end;

theorem Th14: :: GRAPH_1:14

for b₁ being Graph holds {} is oriented cyclic Path of b₁ by Lemma14, Lemma16;

theorem Th15: :: GRAPH_1:15

for b₁ being Graph
for b₂, b₃ being strict Subgraph of b₁ st the Vertices of b₂ = the Vertices of b₃ & the Edges of b₂ = the Edges of b₃ holds
b₂ = b₃ by Lemma20;

theorem Th16: :: GRAPH_1:16

for b₁, b₂ being strict Graph st b₁ c= b₂ & b₂ c= b₁ holds
b₁ = b₂

proof end;

theorem Th17: :: GRAPH_1:17

for b₁, b₂, b₃ being Graph st b₁ c= b₂ & b₂ c= b₃ holds
b₁ c= b₃

proof end;

theorem Th18: :: GRAPH_1:18

for b₁, b₂, b₃ being Graph st b₁ is_sum_of b₂,b₃ holds
( b₂ c= b₁ & b₃ c= b₁ )

proof end;

theorem Th19: :: GRAPH_1:19

for b₁, b₂ being Graph st the Source of b₁ tolerates the Source of b₂ & the Target of b₁ tolerates the Target of b₂ holds
( b₁ c= b₁ \/ b₂ & b₂ c= b₁ \/ b₂ )

proof end;

theorem Th20: :: GRAPH_1:20

for b₁, b₂ being Graph st ex b₃ being Graph st
( b₁ c= b₃ & b₂ c= b₃ ) holds
( b₁ c= b₁ \/ b₂ & b₂ c= b₁ \/ b₂ )

proof end;

theorem Th21: :: GRAPH_1:21

for b₁, b₂, b₃, b₄ being Graph st b₁ c= b₂ & b₃ c= b₂ & b₄ is_sum_of b₁,b₃ holds
b₄ c= b₂

proof end;

theorem Th22: :: GRAPH_1:22

for b₁, b₂, b₃ being Graph st b₁ c= b₂ & b₃ c= b₂ holds
b₁ \/ b₃ c= b₂

proof end;

theorem Th23: :: GRAPH_1:23

for b₁, b₂ being strict Graph st b₁ c= b₂ holds
( b₁ \/ b₂ = b₂ & b₂ \/ b₁ = b₂ )

proof end;

theorem Th24: :: GRAPH_1:24

for b₁, b₂ being Graph st the Source of b₁ tolerates the Source of b₂ & the Target of b₁ tolerates the Target of b₂ & ( b₁ \/ b₂ = b₂ or b₂ \/ b₁ = b₂ ) holds
b₁ c= b₂

proof end;

theorem Th25: :: GRAPH_1:25

canceled;

theorem Th26: :: GRAPH_1:26

canceled;

theorem Th27: :: GRAPH_1:27

for b₁ being Graph
for b₂ being oriented Graph st b₁ c= b₂ holds
b₁ is oriented

proof end;

theorem Th28: :: GRAPH_1:28

for b₁ being Graph
for b₂ being non-multi Graph st b₁ c= b₂ holds
b₁ is non-multi

proof end;

theorem Th29: :: GRAPH_1:29

for b₁ being Graph
for b₂ being simple Graph st b₁ c= b₂ holds
b₁ is simple

proof end;

theorem Th30: :: GRAPH_1:30

for b₁ being Graph
for b₂ being strict Graph holds
( b₂ in bool b₁ iff b₂ c= b₁ )

proof end;

theorem Th31: :: GRAPH_1:31

for b₁ being strict Graph holds b₁ in bool b₁

proof end;

theorem Th32: :: GRAPH_1:32

for b₁ being Graph
for b₂ being strict Graph holds
( b₂ c= b₁ iff bool b₂ c= bool b₁ )

proof end;

theorem Th33: :: GRAPH_1:33

canceled;

theorem Th34: :: GRAPH_1:34

for b₁ being strict Graph holds {b₁} c= bool b₁

proof end;

theorem Th35: :: GRAPH_1:35

for b₁, b₂ being strict Graph st the Source of b₁ tolerates the Source of b₂ & the Target of b₁ tolerates the Target of b₂ & bool (b₁ \/ b₂) c= (bool b₁) \/ (bool b₂) & not b₁ c= b₂ holds
b₂ c= b₁

proof end;

theorem Th36: :: GRAPH_1:36

for b₁, b₂ being Graph st the Source of b₁ tolerates the Source of b₂ & the Target of b₁ tolerates the Target of b₂ holds
(bool b₁) \/ (bool b₂) c= bool (b₁ \/ b₂)

proof end;

theorem Th37: :: GRAPH_1:37

for b₁, b₂, b₃ being Graph st b₁ in bool b₂ & b₃ in bool b₂ holds
b₁ \/ b₃ in bool b₂

proof end;