:: by Krzysztof Retel

::

:: Received November 18, 2002

:: Copyright (c) 2002-2016 Association of Mizar Users

theorem :: NECKLACE:2

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;

::$CT

registration
end;

registration
end;

theorem :: NECKLACE:6

theorem Th6: :: NECKLACE:7

for f, g being one-to-one Function st dom f misses dom g & rng f misses rng g holds

(f +* g) " = (f ") +* (g ")

(f +* g) " = (f ") +* (g ")

proof end;

theorem Th9: :: NECKLACE:10

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

not ( ( a = b implies c = d ) & ( c = d implies a = b ) & not ((a,b) --> (c,d)) " = (c,d) --> (a,b) )

proof end;

definition

let R, S be RelStr ;

end;
pred S embeds R means :: NECKLACE:def 1

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

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

:: deftheorem defines embeds NECKLACE:def 1 :

for R, S being RelStr holds

( S embeds R iff 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 ) ) ) );

for R, S being RelStr holds

( S embeds R iff 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 ) ) ) );

definition

let R, S be non empty RelStr ;

:: original: embeds

redefine pred S embeds R;

reflexivity

for S being non empty RelStr holds (b_{1},b_{1})

end;
:: original: embeds

redefine pred S embeds R;

reflexivity

for S being non empty RelStr holds (b

proof end;

definition

let R, S be non empty RelStr ;

reflexivity

for R being non empty RelStr holds

( R embeds R & R embeds R ) ;

symmetry

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

( S embeds R & R embeds S ) ;

end;
reflexivity

for R being non empty RelStr holds

( R embeds R & R embeds R ) ;

symmetry

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

( S embeds R & R embeds S ) ;

:: deftheorem defines is_equimorphic_to NECKLACE:def 2 :

for R, S being non empty RelStr holds

( R is_equimorphic_to S iff ( R embeds S & S embeds R ) );

for R, S being non empty RelStr holds

( R is_equimorphic_to S iff ( R embeds S & S embeds R ) );

theorem :: NECKLACE:13

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 by Th11;

R is_equimorphic_to T by Th11;

definition

let R be RelStr ;

end;
attr R is symmetric means :Def3: :: NECKLACE:def 3

the InternalRel of R is_symmetric_in the carrier of R;

the InternalRel of R is_symmetric_in the carrier of R;

:: deftheorem Def3 defines symmetric NECKLACE:def 3 :

for R being RelStr holds

( R is symmetric iff the InternalRel of R is_symmetric_in the carrier of R );

for R being RelStr holds

( R is symmetric iff the InternalRel of R is_symmetric_in the carrier of R );

definition
end;

:: deftheorem defines asymmetric NECKLACE:def 4 :

for R being RelStr holds

( R is asymmetric iff the InternalRel of R is asymmetric );

for R being RelStr holds

( R is asymmetric iff the InternalRel of R is asymmetric );

definition

let R be RelStr ;

end;
attr R is irreflexive means :: NECKLACE:def 5

for x being set st x in the carrier of R holds

not [x,x] in the InternalRel of R;

for x being set st x in the carrier of R holds

not [x,x] in the InternalRel of R;

:: deftheorem defines irreflexive NECKLACE:def 5 :

for R being RelStr holds

( R is irreflexive iff for x being set st x in the carrier of R holds

not [x,x] in the InternalRel of R );

for R being RelStr holds

( R is irreflexive iff for x being set st x in the carrier of R holds

not [x,x] in the InternalRel of R );

definition

let n be Nat;

ex b_{1} being strict RelStr st

( the carrier of b_{1} = n & the InternalRel of b_{1} = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } )

for b_{1}, b_{2} being strict RelStr st the carrier of b_{1} = n & the InternalRel of b_{1} = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } & the carrier of b_{2} = n & the InternalRel of b_{2} = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } holds

b_{1} = b_{2}
;

end;
func n -SuccRelStr -> strict RelStr means :Def6: :: NECKLACE:def 6

( the carrier of it = n & the InternalRel of it = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } );

existence ( the carrier of it = n & the InternalRel of it = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def6 defines -SuccRelStr NECKLACE:def 6 :

for n being Nat

for b_{2} being strict RelStr holds

( b_{2} = n -SuccRelStr iff ( the carrier of b_{2} = n & the InternalRel of b_{2} = { [i,(i + 1)] where i is Element of NAT : i + 1 < n } ) );

for n being Nat

for b

( b

definition

let R be RelStr ;

ex b_{1} being strict RelStr st

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

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

b_{1} = b_{2}
;

end;
func SymRelStr R -> strict RelStr means :Def7: :: NECKLACE:def 7

( the carrier of it = the carrier of R & the InternalRel of it = the InternalRel of R \/ ( the InternalRel of R ~) );

existence ( the carrier of it = the carrier of R & the InternalRel of it = the InternalRel of R \/ ( the InternalRel of R ~) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def7 defines SymRelStr NECKLACE:def 7 :

for R being RelStr

for b_{2} being strict RelStr holds

( b_{2} = SymRelStr R iff ( the carrier of b_{2} = the carrier of R & the InternalRel of b_{2} = the InternalRel of R \/ ( the InternalRel of R ~) ) );

for R being RelStr

for b

( b

registration
end;

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

ex b_{1} being strict RelStr st

( the carrier of b_{1} = the carrier of R & the InternalRel of b_{1} = ( the InternalRel of R `) \ (id the carrier of R) )

for b_{1}, b_{2} being strict RelStr st the carrier of b_{1} = the carrier of R & the InternalRel of b_{1} = ( the InternalRel of R `) \ (id the carrier of R) & the carrier of b_{2} = the carrier of R & the InternalRel of b_{2} = ( the InternalRel of R `) \ (id the carrier of R) holds

b_{1} = b_{2}
;

end;
func ComplRelStr R -> strict RelStr means :Def8: :: NECKLACE:def 8

( the carrier of it = the carrier of R & the InternalRel of it = ( the InternalRel of R `) \ (id the carrier of R) );

existence ( the carrier of it = the carrier of R & the InternalRel of it = ( the InternalRel of R `) \ (id the carrier of R) );

ex b

( the carrier of b

proof end;

uniqueness for b

b

:: deftheorem Def8 defines ComplRelStr NECKLACE:def 8 :

for R being RelStr

for b_{2} being strict RelStr holds

( b_{2} = ComplRelStr R iff ( the carrier of b_{2} = the carrier of R & the InternalRel of b_{2} = ( the InternalRel of R `) \ (id the carrier of R) ) );

for R being RelStr

for b

( b

theorem Th16: :: NECKLACE:17

for S, R being RelStr st S,R are_isomorphic holds

card the InternalRel of S = card the InternalRel of R

card the InternalRel of S = card the InternalRel of R

proof end;

:: deftheorem defines Necklace NECKLACE:def 9 :

for n being Nat holds Necklace n = SymRelStr (n -SuccRelStr);

for n being Nat holds Necklace n = SymRelStr (n -SuccRelStr);

registration
end;

theorem Th17: :: NECKLACE:18

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

proof end;

theorem Th18: :: NECKLACE:19

for n being Nat

for x being set holds

( x in the InternalRel of (Necklace n) iff ex i being Element of NAT st

( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) )

for x being set holds

( x in the InternalRel of (Necklace n) iff ex i being Element of NAT st

( i + 1 < n & ( x = [i,(i + 1)] or x = [(i + 1),i] ) ) )

proof end;

theorem Th23: :: NECKLACE:24

for n, i, j being Nat holds

( not [i,j] in the InternalRel of (Necklace n) or i = j + 1 or j = i + 1 )

( not [i,j] in the InternalRel of (Necklace n) or i = j + 1 or j = i + 1 )

proof end;

theorem Th24: :: NECKLACE:25

for n, i, j being Nat 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)

[i,j] in the InternalRel of (Necklace n)

proof end;

theorem :: NECKLACE:30

for n being Nat holds

( not Necklace n, ComplRelStr (Necklace n) are_isomorphic or n = 0 or n = 1 or n = 4 )

( not Necklace n, ComplRelStr (Necklace n) are_isomorphic or n = 0 or n = 1 or n = 4 )

proof end;