:: The Class of Series-Parallel Graphs, {II}
:: by Krzysztof Retel
::
:: 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 () = {[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;
coherence
for b1 being Element of Rank n holds b1 is finite
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
for b1 being Element of FinSETS holds b1 is finite
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 :
for G being non empty RelStr holds
( G is N-free iff not G embeds Necklace 4 );

registration
existence
ex b1 being non empty RelStr st
( b1 is strict & b1 is finite & b1 is N-free )
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 );
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 )
proof end;
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:] )
proof end;
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 object 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 object holds
( X in b1 iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) )
proof end;
uniqueness
for b1, b2 being set st ( for X being object holds
( X in b1 iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) ) ) & ( for X being object holds
( X in b2 iff ex R being strict RelStr st
( X = R & the carrier of R in FinSETS ) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines fin_RelStr NECKLA_2:def 4 :
for b1 being set holds
( b1 = fin_RelStr iff for X being object 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
;
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 ) );
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 ) )
proof end;
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
proof end;
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
correctness
coherence
not fin_RelStr_sp is 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 () = {0,1,2,3}
by ;

theorem :: NECKLA_2:7
for R being non empty strict RelStr st R in fin_RelStr_sp holds
R is N-free
proof end;