begin
theorem Th1:
theorem Th2:
the
InternalRel of
(Necklace 4) = {[0,1],[1,0],[1,2],[2,1],[2,3],[3,2]}
theorem Th3:
:: 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 );
:: 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:
( 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:] )
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:] ) );
:: 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 ) ) );
definition
func fin_RelStr_sp -> Subset of
fin_RelStr means :
Def5:
( ( for
R being
strict RelStr st not the
carrier of
R is
empty & the
carrier of
R is
trivial & 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 not the
carrier of
R is
empty & the
carrier of
R is
trivial & 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 not the carrier of R is empty & the carrier of R is trivial & 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 not the carrier of R is empty & the carrier of R is trivial & 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 ) )
uniqueness
for b1, b2 being Subset of fin_RelStr st ( for R being strict RelStr st not the carrier of R is empty & the carrier of R is trivial & 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 not the carrier of R is empty & the carrier of R is trivial & 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 not the carrier of R is empty & the carrier of R is trivial & 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 not the carrier of R is empty & the carrier of R is trivial & 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
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 not the carrier of R is empty & the carrier of R is trivial & 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 not the carrier of R is empty & the carrier of R is trivial & 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 ) ) );
theorem Th4:
theorem
theorem Th6:
Lm1:
the carrier of (Necklace 4) = {0,1,2,3}
by NECKLACE:2, NECKLACE:21;
theorem