NECKLA_2: The Class of Series-Parallel Graphs, {II}

:: The Class of Series-Parallel Graphs, {II}
:: by Krzysztof Retel
::
:: Received May 29, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users

theorem Th1: :: NECKLA_2:1

for U being Universe
for X, Y being set st X in U & Y in U holds
for R being Relation of X,Y holds R in U

proof end;

theorem Th2: :: NECKLA_2:2

the InternalRel of (Necklace 4) = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}

proof end;

registration

let n be Nat;

cluster -> finite for Element of Rank n;

proof end;

end;

theorem Th3: :: NECKLA_2:3

for x being set st x in FinSETS holds
x is finite

proof end;

registration

cluster -> finite for Element of FinSETS ;

coherence by Th3;

end;

definition

let G be non empty RelStr ;

attr G is N-free means :: NECKLA_2:def 1
not G embeds Necklace 4;

end;

:: deftheorem defines N-free NECKLA_2:def 1 :

registration

cluster non empty finite strict N-free for RelStr ;

proof end;

end;

definition

let R, S be RelStr ;

func union_of (R,S) -> strict RelStr means :Def2: :: NECKLA_2:def 2
( the carrier of it = the carrier of R \/ the carrier of S & the InternalRel of it = the InternalRel of R \/ the InternalRel of S );

proof end;

end;

:: deftheorem Def2 defines union_of NECKLA_2:def 2 :

definition

let R, S be RelStr ;

func sum_of (R,S) -> strict RelStr means :Def3: :: NECKLA_2:def 3
( the carrier of it = the carrier of R \/ the carrier of S & the InternalRel of it = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] );

proof end;

end;

:: deftheorem Def3 defines sum_of NECKLA_2:def 3 :

definition

func fin_RelStr -> set means :Def4: :: NECKLA_2:def 4
for X being object holds
( X in it iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) );

proof end;

proof end;

end;

:: deftheorem Def4 defines fin_RelStr NECKLA_2:def 4 :

registration

cluster fin_RelStr -> non empty ;

proof end;

end;

definition

func fin_RelStr_sp -> Subset of fin_RelStr means :Def5: :: NECKLA_2:def 5
( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in it ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in it & H2 in it holds
( union_of (H1,H2) in it & sum_of (H1,H2) in it ) ) & ( for M being Subset of fin_RelStr st ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in M ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in M & H2 in M holds
( union_of (H1,H2) in M & sum_of (H1,H2) in M ) ) holds
it c= M ) );

proof end;

proof end;

end;

:: deftheorem Def5 defines fin_RelStr_sp NECKLA_2:def 5 :

registration

cluster fin_RelStr_sp -> non empty ;

proof end;

end;

theorem Th4: :: NECKLA_2:4

for X being set st X in fin_RelStr_sp holds
X is non empty finite strict RelStr

proof end;

theorem :: NECKLA_2:5

for R being RelStr st R in fin_RelStr_sp holds
the carrier of R in FinSETS

proof end;

theorem Th6: :: NECKLA_2:6

for X being set holds
( not X in fin_RelStr_sp or X is 1 -element strict RelStr or ex H1, H2 being strict RelStr st
( the carrier of H1 misses the carrier of H2 & H1 in fin_RelStr_sp & H2 in fin_RelStr_sp & ( X = union_of (H1,H2) or X = sum_of (H1,H2) ) ) )

proof end;

Lm1: the carrier of (Necklace 4) = {0,1,2,3}
by NECKLACE:1, NECKLACE:20;

theorem :: NECKLA_2:7

for R being non empty strict RelStr st R in fin_RelStr_sp holds
R is N-free

proof end;