:: NECKLACE semantic presentation

definition

let x1, x2, x3, x4, x5 be set ;
pred x1,x2,x3,x4,x5 are_mutually_different means :Def1: :: NECKLACE:def 1
( x1 <> x2 & x1 <> x3 & x1 <> x4 & x1 <> x5 & x2 <> x3 & x2 <> x4 & x2 <> x5 & x3 <> x4 & x3 <> x5 & x4 <> x5 );

end;

:: deftheorem Def1 defines are_mutually_different NECKLACE:def 1 :

theorem :: NECKLACE:1

for x1, x2, x3, x4, x5 being set st x1,x2,x3,x4,x5 are_mutually_different holds
card {x1,x2,x3,x4,x5} = 5

proof end;

theorem Th2: :: NECKLACE:2

4 = {0,1,2,3}

proof end;

theorem Th3: :: NECKLACE:3

for x1, x2, x3, y1, y2, y3 being set holds [:{x1,x2,x3},{y1,y2,y3}:] = {[x1,y1],[x1,y2],[x1,y3],[x2,y1],[x2,y2],[x2,y3],[x3,y1],[x3,y2],[x3,y3]}

proof end;

theorem Th4: :: NECKLACE:4

for x being set
for n being natural number st x in n holds
x is natural number

proof end;

theorem Th5: :: NECKLACE:5

for x being non empty natural number holds 0 in x

proof end;

registration

cluster natural -> cardinal set ;
coherence

proof end;

end;

registration

let X be set ;
cluster delta X -> one-to-one ;
coherence

proof end;

end;

theorem Th6: :: NECKLACE:6

for X being set holds Card (id X) = Card X

proof end;

registration

let R be trivial Relation;
cluster dom R -> trivial ;
coherence

proof end;

end;

registration

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

proof end;

end;

theorem Th7: :: NECKLACE:7

for f, g being Function st dom f misses dom g holds
rng (f +* g) = (rng f) \/ (rng g)

proof end;

theorem Th8: :: NECKLACE:8

for f, g being one-to-one Function st dom f misses dom g & rng f misses rng g holds
(f +* g) " = (f " ) +* (g " )

proof end;

theorem :: NECKLACE:9

for A, a, b being set holds (A --> a) +* (A --> b) = A --> b

proof end;

theorem Th10: :: NECKLACE:10

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

proof end;

theorem Th11: :: NECKLACE:11

for a, b, c, d being set holds
not ( ( a = b implies c = d ) & ( c = d implies a = b ) & not (a,b --> c,d) " = c,d --> a,b )

proof end;

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

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

provided

A1: F₂() = { [F₄(x),F₃(x)] where x is Element of F₁() : P₁[x] }

proof end;

theorem :: NECKLACE:12

for i, j, n being natural number st i < j & j in n holds
i in n

proof end;

definition

let R, S be RelStr ;
pred S embeds R means :Def2: :: NECKLACE:def 2
ex f being Function of R,S st
( f is one-to-one & ( for x, y being Element of R holds
( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) ) );

end;

:: deftheorem Def2 defines embeds NECKLACE:def 2 :

definition

let R, S be non empty RelStr ;
:: original: embeds
redefine pred S embeds R;
reflexivity

proof end;

end;

theorem Th13: :: NECKLACE:13

for R, S, T being non empty RelStr st R embeds S & S embeds T holds
R embeds T

proof end;

definition

let R, S be non empty RelStr ;
pred R is_equimorphic_to S means :Def3: :: NECKLACE:def 3
( R embeds S & S embeds R );
reflexivity ;
symmetry ;

end;

:: deftheorem Def3 defines is_equimorphic_to NECKLACE:def 3 :

theorem :: NECKLACE:14

for R, S, T being non empty RelStr st R is_equimorphic_to S & S is_equimorphic_to T holds
R is_equimorphic_to T

proof end;

notation

let R be non empty RelStr ;
synonym parallel R for connected R;

end;

definition

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

end;

:: deftheorem Def4 defines symmetric NECKLACE:def 4 :

definition

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

end;

:: deftheorem Def5 defines asymmetric NECKLACE:def 5 :

theorem :: NECKLACE:15

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

proof end;

definition

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

end;

:: deftheorem defines irreflexive NECKLACE:def 6 :

definition

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

proof end;

uniqueness ;

end;

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

theorem :: NECKLACE:16

for n being natural number holds n -SuccRelStr is asymmetric

proof end;

theorem Th17: :: NECKLACE:17

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

proof end;

definition

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

proof end;

uniqueness ;

end;

:: deftheorem Def8 defines SymRelStr NECKLACE:def 8 :

registration

let R be RelStr ;
cluster SymRelStr R -> strict symmetric ;
coherence

proof end;

end;

registration

cluster non empty symmetric RelStr ;
existence

proof end;

end;

registration

let R be symmetric RelStr ;
cluster the InternalRel of R -> symmetric ;
coherence

proof end;

end;

Lm1: for S, R being non empty RelStr st S,R are_isomorphic holds
Card the InternalRel of S = Card the InternalRel of R

proof end;

definition

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

proof end;

uniqueness ;

end;

:: deftheorem Def9 defines ComplRelStr NECKLACE:def 9 :

registration

let R be non empty RelStr ;
cluster ComplRelStr R -> non empty strict ;
coherence

proof end;

end;

theorem Th18: :: NECKLACE:18

for S, R being RelStr st S,R are_isomorphic holds
Card the InternalRel of S = Card the InternalRel of R

proof end;

definition

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

end;

:: deftheorem defines Necklace NECKLACE:def 10 :

registration

let n be natural number ;
cluster Necklace n -> strict symmetric ;
coherence ;

end;

theorem Th19: :: NECKLACE:19

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

proof end;

theorem Th20: :: NECKLACE:20

for n being natural number
for x being set holds
( x in the InternalRel of (Necklace n) iff ex i being Nat st
( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) )

proof end;

registration

let n be natural number ;
cluster Necklace n -> strict symmetric irreflexive ;
coherence

proof end;

end;

theorem Th21: :: NECKLACE:21

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

proof end;

registration

let n be non empty natural number ;
cluster Necklace n -> non empty strict symmetric irreflexive ;
coherence

proof end;

end;

registration

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

end;

theorem Th22: :: NECKLACE:22

for n, i being natural number st i + 1 < n holds
[i,(i + 1)] in the InternalRel of (Necklace n)

proof end;

theorem Th23: :: NECKLACE:23

for n, i being natural number st i in the carrier of (Necklace n) holds
i < n

proof end;

theorem :: NECKLACE:24

for n being non empty natural number holds not Necklace n is parallel

proof end;

theorem Th25: :: NECKLACE:25

for n being natural number
for i, j being natural number holds
( not [i,j] in the InternalRel of (Necklace n) or i = j + 1 or j = i + 1 )

proof end;

theorem Th26: :: NECKLACE:26

for n being natural number
for i, j being natural number st ( i = j + 1 or j = i + 1 ) & i in the carrier of (Necklace n) & j in the carrier of (Necklace n) holds
[i,j] in the InternalRel of (Necklace n)

proof end;

theorem Th27: :: NECKLACE:27

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

proof end;

theorem Th28: :: NECKLACE:28

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

proof end;

theorem :: NECKLACE:29

Necklace 1, ComplRelStr (Necklace 1) are_isomorphic

proof end;

theorem :: NECKLACE:30

Necklace 4, ComplRelStr (Necklace 4) are_isomorphic

proof end;

theorem :: NECKLACE:31

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

proof end;