:: NECKLACE semantic presentation

definition

let c₁, c₂, c₃, c₄, c₅ be set ;
pred c₁,c₂,c₃,c₄,c₅ are_mutually_different means :Def1: :: NECKLACE:def 1
( a₁ <> a₂ & a₁ <> a₃ & a₁ <> a₄ & a₁ <> a₅ & a₂ <> a₃ & a₂ <> a₄ & a₂ <> a₅ & a₃ <> a₄ & a₃ <> a₅ & a₄ <> a₅ );

end;

:: deftheorem Def1 defines are_mutually_different NECKLACE:def 1 :

theorem Th1: :: NECKLACE:1

for b₁, b₂, b₃, b₄, b₅ being set st b₁,b₂,b₃,b₄,b₅ are_mutually_different holds
card {b₁,b₂,b₃,b₄,b₅} = 5

proof end;

theorem Th2: :: NECKLACE:2

4 = {0,1,2,3}

proof end;

theorem Th3: :: NECKLACE:3

for b₁, b₂, b₃, b₄, b₅, b₆ being set holds [:{b₁,b₂,b₃},{b₄,b₅,b₆}:] = {[b₁,b₄],[b₁,b₅],[b₁,b₆],[b₂,b₄],[b₂,b₅],[b₂,b₆],[b₃,b₄],[b₃,b₅],[b₃,b₆]}

proof end;

theorem Th4: :: NECKLACE:4

for b₁ being set
for b₂ being natural number st b₁ in b₂ holds
b₁ is natural number

proof end;

theorem Th5: :: NECKLACE:5

for b₁ being non empty natural number holds 0 in b₁

proof end;

registration

cluster natural -> cardinal set ;
coherence

proof end;

end;

registration

let c₁ be set ;
cluster delta a₁ -> one-to-one ;
coherence

proof end;

end;

theorem Th6: :: NECKLACE:6

for b₁ being set holds Card (id b₁) = Card b₁

proof end;

registration

let c₁ be trivial Relation;
cluster dom a₁ -> trivial ;
coherence

proof end;

end;

registration

cluster trivial -> one-to-one set ;
coherence

proof end;

end;

theorem Th7: :: NECKLACE:7

for b₁, b₂ being Function st dom b₁ misses dom b₂ holds
rng (b₁ +* b₂) = (rng b₁) \/ (rng b₂)

proof end;

theorem Th8: :: NECKLACE:8

for b₁, b₂ being one-to-one Function st dom b₁ misses dom b₂ & rng b₁ misses rng b₂ holds
(b₁ +* b₂) " = (b₁ " ) +* (b₂ " )

proof end;

theorem Th9: :: NECKLACE:9

for b₁, b₂, b₃ being set holds (b₁ --> b₂) +* (b₁ --> b₃) = b₁ --> b₃

proof end;

theorem Th10: :: NECKLACE:10

for b₁, b₂ being set holds (b₁ .--> b₂) " = b₂ .--> b₁

proof end;

theorem Th11: :: NECKLACE:11

for b₁, b₂, b₃, b₄ being set holds
not ( ( b₁ = b₂ implies b₃ = b₄ ) & ( b₃ = b₄ implies b₁ = b₂ ) & not (b₁,b₂ --> b₃,b₄) " = b₃,b₄ --> b₁,b₂ )

proof end;

scheme :: NECKLACE:sch 1
s1{ F₁() -> non empty set , F₂() -> Relation, F₃( set ) -> set , F₄( set ) -> set , P₁[ set ] } :

F₂() ~ = { [F₃(b₁),F₄(b₁)] where B is Element of F₁() : P₁[b₁] }

provided

E11: F₂() = { [F₄(b₁),F₃(b₁)] where B is Element of F₁() : P₁[b₁] }

proof end;

theorem Th12: :: NECKLACE:12

for b₁, b₂, b₃ being natural number st b₁ < b₂ & b₂ in b₃ holds
b₁ in b₃

proof end;

definition

let c₁, c₂ be RelStr ;
pred c₂ embeds c₁ means :Def2: :: NECKLACE:def 2
ex b₁ being Function of a₁,a₂ st
( b₁ is one-to-one & ( for b₂, b₃ being Element of a₁ holds
( [b₂,b₃] in the InternalRel of a₁ iff [(b₁ . b₂),(b₁ . b₃)] in the InternalRel of a₂ ) ) );

end;

:: deftheorem Def2 defines embeds NECKLACE:def 2 :

definition

let c₁, c₂ be non empty RelStr ;
redefine pred embeds as c₂ embeds c₁;
reflexivity

proof end;

end;

theorem Th13: :: NECKLACE:13

for b₁, b₂, b₃ being non empty RelStr st b₁ embeds b₂ & b₂ embeds b₃ holds
b₁ embeds b₃

proof end;

definition

let c₁, c₂ be non empty RelStr ;
pred c₁ is_equimorphic_to c₂ means :Def3: :: NECKLACE:def 3
( a₁ embeds a₂ & a₂ embeds a₁ );
reflexivity ;
symmetry ;

end;

:: deftheorem Def3 defines is_equimorphic_to NECKLACE:def 3 :

theorem Th14: :: NECKLACE:14

for b₁, b₂, b₃ being non empty RelStr st b₁ is_equimorphic_to b₂ & b₂ is_equimorphic_to b₃ holds
b₁ is_equimorphic_to b₃

proof end;

notation

let c₁ be non empty RelStr ;
synonym parallel c₁ for connected c₁;

end;

definition

let c₁ be RelStr ;
attr a₁ is symmetric means :Def4: :: NECKLACE:def 4
the InternalRel of a₁ is_symmetric_in the carrier of a₁;

end;

:: deftheorem Def4 defines symmetric NECKLACE:def 4 :

definition

let c₁ be RelStr ;
attr a₁ is asymmetric means :Def5: :: NECKLACE:def 5
the InternalRel of a₁ is asymmetric;

end;

:: deftheorem Def5 defines asymmetric NECKLACE:def 5 :

theorem Th15: :: NECKLACE:15

for b₁ being RelStr st b₁ is asymmetric holds
the InternalRel of b₁ misses the InternalRel of b₁ ~

proof end;

definition

let c₁ be RelStr ;
attr a₁ is irreflexive means :: NECKLACE:def 6
for b₁ being set st b₁ in the carrier of a₁ holds
not [b₁,b₁] in the InternalRel of a₁;

end;

:: deftheorem Def6 defines irreflexive NECKLACE:def 6 :

definition

let c₁ be natural number ;
func c₁ -SuccRelStr -> strict RelStr means :Def7: :: NECKLACE:def 7
( the carrier of a₂ = a₁ & the InternalRel of a₂ = { [b₁,(b₁ + 1)] where B is Nat : b₁ + 1 < a₁ } );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines -SuccRelStr NECKLACE:def 7 :

theorem Th16: :: NECKLACE:16

for b₁ being natural number holds b₁ -SuccRelStr is asymmetric

proof end;

theorem Th17: :: NECKLACE:17

for b₁ being natural number st b₁ > 0 holds
Card the InternalRel of (b₁ -SuccRelStr ) = b₁ - 1

proof end;

definition

let c₁ be RelStr ;
func SymRelStr c₁ -> strict RelStr means :Def8: :: NECKLACE:def 8
( the carrier of a₂ = the carrier of a₁ & the InternalRel of a₂ = the InternalRel of a₁ \/ (the InternalRel of a₁ ~ ) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def8 defines SymRelStr NECKLACE:def 8 :

registration

let c₁ be RelStr ;
cluster SymRelStr a₁ -> strict symmetric ;
coherence

proof end;

end;

registration

cluster non empty symmetric RelStr ;
existence

proof end;

end;

registration

let c₁ be symmetric RelStr ;
cluster the InternalRel of a₁ -> symmetric ;
coherence

proof end;

end;

Lemma19: for b₁, b₂ being non empty RelStr st b₁,b₂ are_isomorphic holds
Card the InternalRel of b₁ = Card the InternalRel of b₂

proof end;

definition

let c₁ be RelStr ;
func ComplRelStr c₁ -> strict RelStr means :Def9: :: NECKLACE:def 9
( the carrier of a₂ = the carrier of a₁ & the InternalRel of a₂ = (the InternalRel of a₁ ` ) \ (id the carrier of a₁) );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def9 defines ComplRelStr NECKLACE:def 9 :

registration

let c₁ be non empty RelStr ;
cluster ComplRelStr a₁ -> non empty strict ;
coherence

proof end;

end;

theorem Th18: :: NECKLACE:18

for b₁, b₂ being RelStr st b₁,b₂ are_isomorphic holds
Card the InternalRel of b₁ = Card the InternalRel of b₂

proof end;

definition

let c₁ be natural number ;
func Necklace c₁ -> strict RelStr equals :: NECKLACE:def 10
SymRelStr (a₁ -SuccRelStr );
coherence ;

end;

:: deftheorem Def10 defines Necklace NECKLACE:def 10 :

registration

let c₁ be natural number ;
cluster Necklace a₁ -> strict symmetric ;
coherence ;

end;

theorem Th19: :: NECKLACE:19

for b₁ being natural number holds the InternalRel of (Necklace b₁) = { [b₂,(b₂ + 1)] where B is Nat : b₂ + 1 < b₁ } \/ { [(b₂ + 1),b₂] where B is Nat : b₂ + 1 < b₁ }

proof end;

theorem Th20: :: NECKLACE:20

for b₁ being natural number
for b₂ being set holds
( b₂ in the InternalRel of (Necklace b₁) iff ex b₃ being Nat st
( b₃ + 1 < b₁ & ( b₂ = [b₃,(b₃ + 1)] or b₂ = [(b₃ + 1),b₃] ) ) )

proof end;

registration

let c₁ be natural number ;
cluster Necklace a₁ -> strict symmetric irreflexive ;
coherence

proof end;

end;

theorem Th21: :: NECKLACE:21

for b₁ being natural number holds the carrier of (Necklace b₁) = b₁

proof end;

registration

let c₁ be non empty natural number ;
cluster Necklace a₁ -> non empty strict symmetric irreflexive ;
coherence

proof end;

end;

registration

let c₁ be natural number ;
cluster the carrier of (Necklace a₁) -> finite ;
coherence by Th21;

end;

theorem Th22: :: NECKLACE:22

for b₁, b₂ being natural number st b₂ + 1 < b₁ holds
[b₂,(b₂ + 1)] in the InternalRel of (Necklace b₁)

proof end;

theorem Th23: :: NECKLACE:23

for b₁, b₂ being natural number st b₂ in the carrier of (Necklace b₁) holds
b₂ < b₁

proof end;

theorem Th24: :: NECKLACE:24

for b₁ being non empty natural number holds not Necklace b₁ is parallel

proof end;

theorem Th25: :: NECKLACE:25

for b₁ being natural number
for b₂, b₃ being natural number holds
( not [b₂,b₃] in the InternalRel of (Necklace b₁) or b₂ = b₃ + 1 or b₃ = b₂ + 1 )

proof end;

theorem Th26: :: NECKLACE:26

for b₁ being natural number
for b₂, b₃ being natural number st ( b₂ = b₃ + 1 or b₃ = b₂ + 1 ) & b₂ in the carrier of (Necklace b₁) & b₃ in the carrier of (Necklace b₁) holds
[b₂,b₃] in the InternalRel of (Necklace b₁)

proof end;

theorem Th27: :: NECKLACE:27

for b₁ being natural number st b₁ > 0 holds
Card { [(b₂ + 1),b₂] where B is Nat : b₂ + 1 < b₁ } = b₁ - 1

proof end;

theorem Th28: :: NECKLACE:28

for b₁ being natural number st b₁ > 0 holds
Card the InternalRel of (Necklace b₁) = 2 * (b₁ - 1)

proof end;

theorem Th29: :: NECKLACE:29

Necklace 1, ComplRelStr (Necklace 1) are_isomorphic

proof end;

theorem Th30: :: NECKLACE:30

Necklace 4, ComplRelStr (Necklace 4) are_isomorphic

proof end;

theorem Th31: :: NECKLACE:31

for b₁ being natural number holds
( not Necklace b₁, ComplRelStr (Necklace b₁) are_isomorphic or b₁ = 0 or b₁ = 1 or b₁ = 4 )

proof end;