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


begin

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
proofend;

theorem Th2: :: NECKLA_2:2
the InternalRel of (Necklace 4) = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}
proofend;

registration
let n be Nat;
cluster  ->  finite for Element of Rank n;
coherence
 for b1 being Element of Rank n holds b1 is finite
proofend;
end;

theorem Th3: :: NECKLA_2:3
for x being set st x in FinSETS holds
x is finite
proofend;

registration
cluster  ->  finite for Element of FinSETS ;
coherence
 for b1 being Element of FinSETS holds b1 is finite by Th3;
end;

definition
let G be non empty RelStr ;
attrG is N-free  means :Def1: :: NECKLA_2:def 1
 not G embeds Necklace 4;
end;

:: deftheorem Def1 defines N-free NECKLA_2:def_1_:_
 for G being non empty RelStr holds
( G is N-free iff not G embeds Necklace 4 );

registration
cluster non empty finite strict N-free for RelStr ;
existence
 ex b1 being non empty RelStr st
( b1 is strict & b1 is finite & b1 is N-free )
proofend;
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 );
existence
 ex b1 being strict RelStr st
( the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = the InternalRel of R \/ the InternalRel of S )
proofend;
uniqueness
 for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = the InternalRel of R \/ the InternalRel of S & the carrier of b2 = the carrier of R \/ the carrier of S & the InternalRel of b2 = the InternalRel of R \/ the InternalRel of S holds
b1 = b2 ;
end;

:: deftheorem Def2 defines union_of NECKLA_2:def_2_:_
 for R, S being RelStr
for b3 being strict RelStr holds
( b3 = union_of (R,S) iff ( the carrier of b3 = the carrier of R \/ the carrier of S & the InternalRel of b3 = the InternalRel of R \/ the InternalRel of S ) );

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:] );
existence
 ex b1 being strict RelStr st
( the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] )
proofend;
uniqueness
 for b1, b2 being strict RelStr st the carrier of b1 = the carrier of R \/ the carrier of S & the InternalRel of b1 = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] & the carrier of b2 = the carrier of R \/ the carrier of S & the InternalRel of b2 = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] holds
b1 = b2 ;
end;

:: deftheorem Def3 defines sum_of NECKLA_2:def_3_:_
 for R, S being RelStr
for b3 being strict RelStr holds
( b3 = sum_of (R,S) iff ( the carrier of b3 = the carrier of R \/ the carrier of S & the InternalRel of b3 = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] ) );

definition
func fin_RelStr  ->  set  means :Def4: :: NECKLA_2:def 4
 for X being set holds
( X in it iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) );
existence
 ex b1 being set st
for X being set holds
( X in b1 iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) )
proofend;
uniqueness
 for b1, b2 being set st ( for X being set holds
( X in b1 iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) ) ) & ( for X being set holds
( X in b2 iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) ) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def4 defines fin_RelStr NECKLA_2:def_4_:_
 for b1 being set holds
( b1 = fin_RelStr iff for X being set holds
( X in b1 iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) ) );

registration
cluster fin_RelStr  ->  non empty ;
correctness
coherence
not fin_RelStr is empty ;
proofend;
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 ) );
existence
 ex b1 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 b1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b1 & H2 in b1 holds
( union_of (H1,H2) in b1 & sum_of (H1,H2) in b1 ) ) & ( 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
b1 c= M ) )
proofend;
uniqueness
 for b1, b2 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 b1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b1 & H2 in b1 holds
( union_of (H1,H2) in b1 & sum_of (H1,H2) in b1 ) ) & ( 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
b1 c= M ) & ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in b2 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b2 & H2 in b2 holds
( union_of (H1,H2) in b2 & sum_of (H1,H2) in b2 ) ) & ( 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
b2 c= M ) holds
b1 = b2
proofend;
end;

:: deftheorem Def5 defines fin_RelStr_sp NECKLA_2:def_5_:_
 for b1 being Subset of fin_RelStr holds
( b1 = fin_RelStr_sp iff ( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds
R in b1 ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b1 & H2 in b1 holds
( union_of (H1,H2) in b1 & sum_of (H1,H2) in b1 ) ) & ( 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
b1 c= M ) ) );

registration
cluster fin_RelStr_sp  ->  non empty ;
correctness
coherence
not fin_RelStr_sp is empty ;
proofend;
end;

theorem Th4: :: NECKLA_2:4
for X being set st X in fin_RelStr_sp holds
X is non empty finite strict RelStr
proofend;

theorem :: NECKLA_2:5
for R being RelStr st R in fin_RelStr_sp holds
the carrier of R in FinSETS
proofend;

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) ) ) )
proofend;

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
proofend;