:: 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

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;

registration
end;

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

for G being non empty RelStr holds

( G is N-free iff not G embeds Necklace 4 );

registration

existence

ex b_{1} being non empty RelStr st

( b_{1} is strict & b_{1} is finite & b_{1} is N-free )

end;
ex b

( b

proof end;

definition

let R, S be RelStr ;

ex b_{1} being strict RelStr st

( the carrier of b_{1} = the carrier of R \/ the carrier of S & the InternalRel of b_{1} = the InternalRel of R \/ the InternalRel of S )

for b_{1}, b_{2} being strict RelStr st the carrier of b_{1} = the carrier of R \/ the carrier of S & the InternalRel of b_{1} = the InternalRel of R \/ the InternalRel of S & the carrier of b_{2} = the carrier of R \/ the carrier of S & the InternalRel of b_{2} = the InternalRel of R \/ the InternalRel of S holds

b_{1} = b_{2}
;

end;
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 ( the carrier of it = the carrier of R \/ the carrier of S & the InternalRel of it = the InternalRel of R \/ the InternalRel of S );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def2 defines union_of NECKLA_2:def 2 :

for R, S being RelStr

for b_{3} being strict RelStr holds

( b_{3} = union_of (R,S) iff ( the carrier of b_{3} = the carrier of R \/ the carrier of S & the InternalRel of b_{3} = the InternalRel of R \/ the InternalRel of S ) );

for R, S being RelStr

for b

( b

definition

let R, S be RelStr ;

ex b_{1} being strict RelStr st

( the carrier of b_{1} = the carrier of R \/ the carrier of S & the InternalRel of b_{1} = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] )

for b_{1}, b_{2} being strict RelStr st the carrier of b_{1} = the carrier of R \/ the carrier of S & the InternalRel of b_{1} = (( 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 b_{2} = the carrier of R \/ the carrier of S & the InternalRel of b_{2} = (( 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

b_{1} = b_{2}
;

end;
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 ( 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:] );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def3 defines sum_of NECKLA_2:def 3 :

for R, S being RelStr

for b_{3} being strict RelStr holds

( b_{3} = sum_of (R,S) iff ( the carrier of b_{3} = the carrier of R \/ the carrier of S & the InternalRel of b_{3} = (( the InternalRel of R \/ the InternalRel of S) \/ [: the carrier of R, the carrier of S:]) \/ [: the carrier of S, the carrier of R:] ) );

for R, S being RelStr

for b

( b

definition

ex b_{1} being set st

for X being object holds

( X in b_{1} iff ex R being strict RelStr st

( X = R & the carrier of R in FinSETS ) )

for b_{1}, b_{2} being set st ( for X being object holds

( X in b_{1} iff ex R being strict RelStr st

( X = R & the carrier of R in FinSETS ) ) ) & ( for X being object holds

( X in b_{2} iff ex R being strict RelStr st

( X = R & the carrier of R in FinSETS ) ) ) holds

b_{1} = b_{2}
end;

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 for X being object holds

( X in it iff ex R being strict RelStr st

( X = R & the carrier of R in FinSETS ) );

ex b

for X being object holds

( X in b

( X = R & the carrier of R in FinSETS ) )

proof end;

uniqueness for b

( X in b

( X = R & the carrier of R in FinSETS ) ) ) & ( for X being object holds

( X in b

( X = R & the carrier of R in FinSETS ) ) ) holds

b

proof end;

:: deftheorem Def4 defines fin_RelStr NECKLA_2:def 4 :

for b_{1} being set holds

( b_{1} = fin_RelStr iff for X being object holds

( X in b_{1} iff ex R being strict RelStr st

( X = R & the carrier of R in FinSETS ) ) );

for b

( b

( X in b

( X = R & the carrier of R in FinSETS ) ) );

registration
end;

definition

ex b_{1} 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 b_{1} ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b_{1} & H2 in b_{1} holds

( union_of (H1,H2) in b_{1} & sum_of (H1,H2) in b_{1} ) ) & ( 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

b_{1} c= M ) )

for b_{1}, b_{2} 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 b_{1} ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b_{1} & H2 in b_{1} holds

( union_of (H1,H2) in b_{1} & sum_of (H1,H2) in b_{1} ) ) & ( 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

b_{1} c= M ) & ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds

R in b_{2} ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b_{2} & H2 in b_{2} holds

( union_of (H1,H2) in b_{2} & sum_of (H1,H2) in b_{2} ) ) & ( 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

b_{2} c= M ) holds

b_{1} = b_{2}
end;

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

ex b

( ( for R being strict RelStr st the carrier of R is 1 -element & the carrier of R in FinSETS holds

R in b

( union_of (H1,H2) in b

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

b

proof end;

uniqueness for b

R in b

( union_of (H1,H2) in b

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

b

R in b

( union_of (H1,H2) in b

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

b

b

proof end;

:: deftheorem Def5 defines fin_RelStr_sp NECKLA_2:def 5 :

for b_{1} being Subset of fin_RelStr holds

( b_{1} = 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 b_{1} ) & ( for H1, H2 being strict RelStr st the carrier of H1 misses the carrier of H2 & H1 in b_{1} & H2 in b_{1} holds

( union_of (H1,H2) in b_{1} & sum_of (H1,H2) in b_{1} ) ) & ( 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

b_{1} c= M ) ) );

for b

( b

R in b

( union_of (H1,H2) in b

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

b

registration
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) ) ) )

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