:: SGRAPH1 semantic presentation

Lemma1: for b₁ being set
for b₂ being Nat st b₁ in Seg b₂ holds
ex b₃ being Nat st
( b₁ = b₃ & 1 <= b₃ & b₃ <= b₂ )

proof end;

definition

let c₁, c₂ be natural number ;
func nat_interval c₁,c₂ -> Subset of NAT equals :: SGRAPH1:def 1
{ b₁ where B is Nat : ( a₁ <= b₁ & b₁ <= a₂ ) } ;
coherence

proof end;

end;

:: deftheorem Def1 defines nat_interval SGRAPH1:def 1 :

notation

let c₁, c₂ be natural number ;
synonym Seg c₁,c₂ for nat_interval c₁,c₂;

end;

registration

let c₁, c₂ be natural number ;
cluster nat_interval a₁,a₂ -> finite ;
coherence

proof end;

end;

theorem Th1: :: SGRAPH1:1

canceled;

theorem Th2: :: SGRAPH1:2

for b₁, b₂ being Nat
for b₃ being set holds
( b₃ in nat_interval b₁,b₂ iff ex b₄ being Nat st
( b₃ = b₄ & b₁ <= b₄ & b₄ <= b₂ ) ) ;

theorem Th3: :: SGRAPH1:3

for b₁, b₂, b₃ being Nat holds
( b₃ in nat_interval b₁,b₂ iff ( b₁ <= b₃ & b₃ <= b₂ ) )

proof end;

theorem Th4: :: SGRAPH1:4

for b₁ being Nat holds nat_interval 1,b₁ = Seg b₁

proof end;

theorem Th5: :: SGRAPH1:5

for b₁, b₂ being Nat st 1 <= b₁ holds
nat_interval b₁,b₂ c= Seg b₂

proof end;

theorem Th6: :: SGRAPH1:6

for b₁, b₂, b₃ being Nat st b₁ < b₂ holds
Seg b₁ misses nat_interval b₂,b₃

proof end;

theorem Th7: :: SGRAPH1:7

for b₁, b₂ being Nat st b₂ < b₁ holds
nat_interval b₁,b₂ = {}

proof end;

Lemma4: for b₁ being set
for b₂ being Subset of b₁
for b₃ being set st b₃ in b₁ holds
b₂ \/ {b₃} is Subset of b₁

proof end;

definition

let c₁ be set ;
canceled;
canceled;
func TWOELEMENTSETS c₁ -> set equals :: SGRAPH1:def 4
{ b₁ where B is finite Subset of a₁ : card b₁ = 2 } ;
coherence ;

end;

:: deftheorem Def2 SGRAPH1:def 2 :

:: deftheorem Def3 SGRAPH1:def 3 :

:: deftheorem Def4 defines TWOELEMENTSETS SGRAPH1:def 4 :

theorem Th8: :: SGRAPH1:8

canceled;

theorem Th9: :: SGRAPH1:9

for b₁, b₂ being set holds
( b₂ in TWOELEMENTSETS b₁ iff ex b₃ being finite Subset of b₁ st
( b₂ = b₃ & card b₃ = 2 ) ) ;

theorem Th10: :: SGRAPH1:10

for b₁, b₂ being set holds
( b₂ in TWOELEMENTSETS b₁ iff ( b₂ is finite Subset of b₁ & ex b₃, b₄ being set st
( b₃ in b₁ & b₄ in b₁ & b₃ <> b₄ & b₂ = {b₃,b₄} ) ) )

proof end;

theorem Th11: :: SGRAPH1:11

for b₁ being set holds TWOELEMENTSETS b₁ c= bool b₁

proof end;

theorem Th12: :: SGRAPH1:12

for b₁, b₂, b₃ being set st {b₂,b₃} in TWOELEMENTSETS b₁ holds
( b₂ in b₁ & b₃ in b₁ & b₂ <> b₃ )

proof end;

theorem Th13: :: SGRAPH1:13

TWOELEMENTSETS {} = {}

proof end;

theorem Th14: :: SGRAPH1:14

for b₁, b₂ being set st b₁ c= b₂ holds
TWOELEMENTSETS b₁ c= TWOELEMENTSETS b₂

proof end;

theorem Th15: :: SGRAPH1:15

for b₁ being finite set holds TWOELEMENTSETS b₁ is finite

proof end;

theorem Th16: :: SGRAPH1:16

for b₁ being non trivial set holds not TWOELEMENTSETS b₁ is empty

proof end;

theorem Th17: :: SGRAPH1:17

for b₁ being set holds TWOELEMENTSETS {b₁} = {}

proof end;

registration

let c₁ be empty set ;
cluster -> empty Element of bool a₁;
coherence by XBOOLE_1:3;

end;

definition

attr a₁ is strict;
struct SimpleGraphStruct -> 1-sorted ;
aggr SimpleGraphStruct(# carrier, SEdges #) -> SimpleGraphStruct ;
sel SEdges c₁ -> Subset of (TWOELEMENTSETS the carrier of a₁);

end;

definition

let c₁ be set ;
canceled;
func SIMPLEGRAPHS c₁ -> set equals :: SGRAPH1:def 6
{ SimpleGraphStruct(# b₁,b₂ #) where B is finite Subset of a₁, B is finite Subset of (TWOELEMENTSETS b₁) : verum } ;
coherence ;

end;

:: deftheorem Def5 SGRAPH1:def 5 :

:: deftheorem Def6 defines SIMPLEGRAPHS SGRAPH1:def 6 :

theorem Th18: :: SGRAPH1:18

canceled;

theorem Th19: :: SGRAPH1:19

for b₁ being set holds SimpleGraphStruct(# {} ,({} (TWOELEMENTSETS {} )) #) in SIMPLEGRAPHS b₁

proof end;

registration

let c₁ be set ;
cluster SIMPLEGRAPHS a₁ -> non empty ;
coherence by Th19;

end;

definition

let c₁ be set ;
mode SimpleGraph of c₁ -> strict SimpleGraphStruct means :Def7: :: SGRAPH1:def 7
a₂ is Element of SIMPLEGRAPHS a₁;
existence

proof end;

end;

:: deftheorem Def7 defines SimpleGraph SGRAPH1:def 7 :

theorem Th20: :: SGRAPH1:20

canceled;

theorem Th21: :: SGRAPH1:21

for b₁, b₂ being set holds
( b₂ in SIMPLEGRAPHS b₁ iff ex b₃ being finite Subset of b₁ex b₄ being finite Subset of (TWOELEMENTSETS b₃) st b₂ = SimpleGraphStruct(# b₃,b₄ #) ) ;

theorem Th22: :: SGRAPH1:22

canceled;

theorem Th23: :: SGRAPH1:23

for b₁ being set
for b₂ being SimpleGraph of b₁ holds
( the carrier of b₂ c= b₁ & the SEdges of b₂ c= TWOELEMENTSETS the carrier of b₂ )

proof end;

theorem Th24: :: SGRAPH1:24

canceled;

theorem Th25: :: SGRAPH1:25

for b₁ being set
for b₂ being SimpleGraph of b₁
for b₃ being set st b₃ in the SEdges of b₂ holds
ex b₄, b₅ being set st
( b₄ in the carrier of b₂ & b₅ in the carrier of b₂ & b₄ <> b₅ & b₃ = {b₄,b₅} ) by Th10;

theorem Th26: :: SGRAPH1:26

for b₁ being set
for b₂ being SimpleGraph of b₁
for b₃, b₄ being set st {b₃,b₄} in the SEdges of b₂ holds
( b₃ in the carrier of b₂ & b₄ in the carrier of b₂ & b₃ <> b₄ ) by Th12;

theorem Th27: :: SGRAPH1:27

for b₁ being set
for b₂ being SimpleGraph of b₁ holds
( the carrier of b₂ is finite Subset of b₁ & the SEdges of b₂ is finite Subset of (TWOELEMENTSETS the carrier of b₂) )

proof end;

definition

let c₁ be set ;
let c₂, c₃ be SimpleGraph of c₁;
pred c₂ is_isomorphic_to c₃ means :: SGRAPH1:def 8
ex b₁ being Function of the carrier of a₂,the carrier of a₃ st
( b₁ is bijective & ( for b₂, b₃ being Element of a₂ holds
( {b₂,b₃} in the SEdges of a₂ iff {(b₁ . b₂),(b₁ . b₃)} in the SEdges of a₂ ) ) );

end;

:: deftheorem Def8 defines is_isomorphic_to SGRAPH1:def 8 :

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

for b₁ being set st b₁ in SIMPLEGRAPHS F₁() holds
P₁[b₁]

provided

E16: P₁[ SimpleGraphStruct(# {} ,({} (TWOELEMENTSETS {} )) #)] and
E17: for b₁ being SimpleGraph of F₁()
for b₂ being set st b₁ in SIMPLEGRAPHS F₁() & P₁[b₁] & b₂ in F₁() & not b₂ in the carrier of b₁ holds
P₁[ SimpleGraphStruct(# (the carrier of b₁ \/ {b₂}),({} (TWOELEMENTSETS (the carrier of b₁ \/ {b₂}))) #)] and
E18: for b₁ being SimpleGraph of F₁()
for b₂ being set st P₁[b₁] & b₂ in TWOELEMENTSETS the carrier of b₁ & not b₂ in the SEdges of b₁ holds
ex b₃ being Subset of (TWOELEMENTSETS the carrier of b₁) st
( b₃ = the SEdges of b₁ \/ {b₂} & P₁[ SimpleGraphStruct(# the carrier of b₁,b₃ #)] )

proof end;

theorem Th28: :: SGRAPH1:28

for b₁ being set
for b₂ being SimpleGraph of b₁ holds
( b₂ = SimpleGraphStruct(# {} ,({} (TWOELEMENTSETS {} )) #) or ex b₃ being set ex b₄ being Subset of (TWOELEMENTSETS b₃) st
( not b₃ is empty & b₂ = SimpleGraphStruct(# b₃,b₄ #) ) )

proof end;

theorem Th29: :: SGRAPH1:29

canceled;

theorem Th30: :: SGRAPH1:30

for b₁ being set
for b₂ being Subset of b₁
for b₃ being Subset of (TWOELEMENTSETS b₂)
for b₄ being set
for b₅ being finite Subset of (TWOELEMENTSETS (b₂ \/ {b₄})) st SimpleGraphStruct(# b₂,b₃ #) in SIMPLEGRAPHS b₁ & b₄ in b₁ & not b₄ in b₂ holds
SimpleGraphStruct(# (b₂ \/ {b₄}),b₅ #) in SIMPLEGRAPHS b₁

proof end;

theorem Th31: :: SGRAPH1:31

for b₁ being set
for b₂ being Subset of b₁
for b₃ being Subset of (TWOELEMENTSETS b₂)
for b₄, b₅ being set st b₄ in b₂ & b₅ in b₂ & b₄ <> b₅ & SimpleGraphStruct(# b₂,b₃ #) in SIMPLEGRAPHS b₁ holds
ex b₆ being finite Subset of (TWOELEMENTSETS b₂) st
( b₆ = b₃ \/ {{b₄,b₅}} & SimpleGraphStruct(# b₂,b₆ #) in SIMPLEGRAPHS b₁ )

proof end;

definition

let c₁, c₂ be set ;
pred c₂ is_SetOfSimpleGraphs_of c₁ means :Def9: :: SGRAPH1:def 9
( SimpleGraphStruct(# {} ,({} (TWOELEMENTSETS {} )) #) in a₂ & ( for b₁ being Subset of a₁
for b₂ being Subset of (TWOELEMENTSETS b₁)
for b₃ being set
for b₄ being finite Subset of (TWOELEMENTSETS (b₁ \/ {b₃})) st SimpleGraphStruct(# b₁,b₂ #) in a₂ & b₃ in a₁ & not b₃ in b₁ holds
SimpleGraphStruct(# (b₁ \/ {b₃}),b₄ #) in a₂ ) & ( for b₁ being Subset of a₁
for b₂ being Subset of (TWOELEMENTSETS b₁)
for b₃, b₄ being set st SimpleGraphStruct(# b₁,b₂ #) in a₂ & b₃ in b₁ & b₄ in b₁ & b₃ <> b₄ & not {b₃,b₄} in b₂ holds
ex b₅ being finite Subset of (TWOELEMENTSETS b₁) st
( b₅ = b₂ \/ {{b₃,b₄}} & SimpleGraphStruct(# b₁,b₅ #) in a₂ ) ) );

end;

:: deftheorem Def9 defines is_SetOfSimpleGraphs_of SGRAPH1:def 9 :

theorem Th32: :: SGRAPH1:32

canceled;

theorem Th33: :: SGRAPH1:33

canceled;

theorem Th34: :: SGRAPH1:34

canceled;

theorem Th35: :: SGRAPH1:35

for b₁ being set holds SIMPLEGRAPHS b₁ is_SetOfSimpleGraphs_of b₁

proof end;

theorem Th36: :: SGRAPH1:36

for b₁, b₂ being set st b₂ is_SetOfSimpleGraphs_of b₁ holds
SIMPLEGRAPHS b₁ c= b₂

proof end;

theorem Th37: :: SGRAPH1:37

for b₁ being set holds
( SIMPLEGRAPHS b₁ is_SetOfSimpleGraphs_of b₁ & ( for b₂ being set st b₂ is_SetOfSimpleGraphs_of b₁ holds
SIMPLEGRAPHS b₁ c= b₂ ) ) by Th35, Th36;

definition

let c₁ be set ;
let c₂ be SimpleGraph of c₁;
mode SubGraph of c₂ -> SimpleGraph of a₁ means :: SGRAPH1:def 10
( the carrier of a₃ c= the carrier of a₂ & the SEdges of a₃ c= the SEdges of a₂ );
existence ;

end;

:: deftheorem Def10 defines SubGraph SGRAPH1:def 10 :

definition

let c₁ be set ;
let c₂ be SimpleGraph of c₁;
let c₃ be set ;
func degree c₂,c₃ -> Nat means :Def11: :: SGRAPH1:def 11
ex b₁ being finite set st
( ( for b₂ being set holds
( b₂ in b₁ iff ( b₂ in the SEdges of a₂ & a₃ in b₂ ) ) ) & a₄ = card b₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines degree SGRAPH1:def 11 :

theorem Th38: :: SGRAPH1:38

canceled;

theorem Th39: :: SGRAPH1:39

for b₁ being non empty set
for b₂ being SimpleGraph of b₁
for b₃ being set ex b₄ being finite set st
( b₄ = { b₅ where B is Element of b₁ : ( b₅ in the carrier of b₂ & {b₃,b₅} in the SEdges of b₂ ) } & degree b₂,b₃ = card b₄ )

proof end;

theorem Th40: :: SGRAPH1:40

for b₁ being non empty set
for b₂ being SimpleGraph of b₁
for b₃ being set st b₃ in the carrier of b₂ holds
ex b₄ being finite set st
( b₄ = the carrier of b₂ & degree b₂,b₃ < card b₄ )

proof end;

theorem Th41: :: SGRAPH1:41

for b₁ being set
for b₂ being SimpleGraph of b₁
for b₃, b₄ being set st b₃ in the carrier of b₂ & b₄ in the SEdges of b₂ & degree b₂,b₃ = 0 holds
not b₃ in b₄

proof end;

theorem Th42: :: SGRAPH1:42

for b₁ being set
for b₂ being SimpleGraph of b₁
for b₃ being set
for b₄ being finite set st b₄ = the carrier of b₂ & b₃ in b₄ & 1 + (degree b₂,b₃) = card b₄ holds
for b₅ being Element of b₄ st b₃ <> b₅ holds
ex b₆ being set st
( b₆ in the SEdges of b₂ & b₆ = {b₃,b₅} )

proof end;

definition

let c₁ be set ;
let c₂ be SimpleGraph of c₁;
let c₃, c₄ be Element of c₂;
let c₅ be FinSequence of the carrier of c₂;
pred c₅ is_path_of c₃,c₄ means :Def12: :: SGRAPH1:def 12
( a₅ . 1 = a₃ & a₅ . (len a₅) = a₄ & ( for b₁ being Nat st 1 <= b₁ & b₁ < len a₅ holds
{(a₅ . b₁),(a₅ . (b₁ + 1))} in the SEdges of a₂ ) & ( for b₁, b₂ being Nat st 1 <= b₁ & b₁ < len a₅ & b₁ < b₂ & b₂ < len a₅ holds
( a₅ . b₁ <> a₅ . b₂ & {(a₅ . b₁),(a₅ . (b₁ + 1))} <> {(a₅ . b₂),(a₅ . (b₂ + 1))} ) ) );

end;

:: deftheorem Def12 defines is_path_of SGRAPH1:def 12 :

definition

let c₁ be set ;
let c₂ be SimpleGraph of c₁;
let c₃, c₄ be Element of the carrier of c₂;
func PATHS c₃,c₄ -> Subset of (the carrier of a₂ * ) equals :: SGRAPH1:def 13
{ b₁ where B is Element of the carrier of a₂ * : b₁ is_path_of a₃,a₄ } ;
coherence

proof end;

end;

:: deftheorem Def13 defines PATHS SGRAPH1:def 13 :

theorem Th43: :: SGRAPH1:43

canceled;

theorem Th44: :: SGRAPH1:44

for b₁ being set
for b₂ being SimpleGraph of b₁
for b₃, b₄ being Element of the carrier of b₂
for b₅ being set holds
( b₅ in PATHS b₃,b₄ iff ex b₆ being Element of the carrier of b₂ * st
( b₅ = b₆ & b₆ is_path_of b₃,b₄ ) ) ;

theorem Th45: :: SGRAPH1:45

for b₁ being set
for b₂ being SimpleGraph of b₁
for b₃, b₄ being Element of the carrier of b₂
for b₅ being Element of the carrier of b₂ * st b₅ is_path_of b₃,b₄ holds
b₅ in PATHS b₃,b₄ ;

definition

let c₁ be set ;
let c₂ be SimpleGraph of c₁;
let c₃ be set ;
pred c₃ is_cycle_of c₂ means :Def14: :: SGRAPH1:def 14
ex b₁ being Element of the carrier of a₂ st a₃ in PATHS b₁,b₁;

end;

:: deftheorem Def14 defines is_cycle_of SGRAPH1:def 14 :

definition

let c₁, c₂ be Nat;
canceled;
func K_ c₂,c₁ -> SimpleGraph of NAT means :: SGRAPH1:def 16
ex b₁ being Subset of (TWOELEMENTSETS (Seg (a₂ + a₁))) st
( b₁ = { {b₂,b₃} where B is Element of NAT , B is Element of NAT : ( b₂ in Seg a₂ & b₃ in nat_interval (a₂ + 1),(a₂ + a₁) ) } & a₃ = SimpleGraphStruct(# (Seg (a₂ + a₁)),b₁ #) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def15 SGRAPH1:def 15 :

:: deftheorem Def16 defines K_ SGRAPH1:def 16 :

definition

let c₁ be Nat;
func K_ c₁ -> SimpleGraph of NAT means :Def17: :: SGRAPH1:def 17
ex b₁ being finite Subset of (TWOELEMENTSETS (Seg a₁)) st
( b₁ = { {b₂,b₃} where B is Element of NAT , B is Element of NAT : ( b₂ in Seg a₁ & b₃ in Seg a₁ & b₂ <> b₃ ) } & a₂ = SimpleGraphStruct(# (Seg a₁),b₁ #) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def17 defines K_ SGRAPH1:def 17 :

definition

func TriangleGraph -> SimpleGraph of NAT equals :: SGRAPH1:def 18
K_ 3;
correctness ;

end;

:: deftheorem Def18 defines TriangleGraph SGRAPH1:def 18 :

theorem Th46: :: SGRAPH1:46

ex b₁ being Subset of (TWOELEMENTSETS (Seg 3)) st
( b₁ = {{1,2},{2,3},{3,1}} & TriangleGraph = SimpleGraphStruct(# (Seg 3),b₁ #) )

proof end;

theorem Th47: :: SGRAPH1:47

( the carrier of TriangleGraph = Seg 3 & the SEdges of TriangleGraph = {{1,2},{2,3},{3,1}} ) by Th46;

theorem Th48: :: SGRAPH1:48

( {1,2} in the SEdges of TriangleGraph & {2,3} in the SEdges of TriangleGraph & {3,1} in the SEdges of TriangleGraph ) by Th46, ENUMSET1:def 1;

theorem Th49: :: SGRAPH1:49

((<*1*> ^ <*2*>) ^ <*3*>) ^ <*1*> is_cycle_of TriangleGraph

proof end;