:: by Karol P\kak

::

:: Received May 15, 2012

:: Copyright (c) 2012-2018 Association of Mizar Users

registration
end;

Lm1: for k, n being Nat holds

( n * k = n *` k & n + k = n +` k )

proof end;

Lm2: for x being object

for R being Relation st R is irreflexive holds

not [x,x] in R

proof end;

Lm3: for x, y being object

for R being Relation st R is symmetric & [x,y] in R holds

[y,x] in R

proof end;

Lm4: for k being Nat

for p being FinSequence st not k in dom p holds

(p /^ k) ^ (p | k) = p

proof end;

theorem Th3: :: FRIENDS1:3

for k, n being Nat

for p, q being FinSequence st (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) & k <= n & n <= len p holds

p = (q /^ (n -' k)) ^ (q | (n -' k))

for p, q being FinSequence st (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) & k <= n & n <= len p holds

p = (q /^ (n -' k)) ^ (q | (n -' k))

proof end;

theorem Th4: :: FRIENDS1:4

for n being Nat

for p, q being FinSequence st n in dom q & p = (q /^ n) ^ (q | n) holds

q = (p /^ ((len p) -' n)) ^ (p | ((len p) -' n))

for p, q being FinSequence st n in dom q & p = (q /^ n) ^ (q | n) holds

q = (p /^ ((len p) -' n)) ^ (p | ((len p) -' n))

proof end;

theorem Th5: :: FRIENDS1:5

for k, n being Nat

for p, q being FinSequence st (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) holds

ex i being Nat st p = (q /^ i) ^ (q | i)

for p, q being FinSequence st (p /^ k) ^ (p | k) = (q /^ n) ^ (q | n) holds

ex i being Nat st p = (q /^ i) ^ (q | i)

proof end;

scheme :: FRIENDS1:sch 1

Sch{ F_{1}() -> non empty set , F_{2}() -> non zero Nat, P_{1}[ set ] } :

Sch{ F

ex C being Cardinal st F_{2}() *` C = card { F where F is Element of F_{2}() -tuples_on F_{1}() : P_{1}[F] }

provided
A1:
for p, q being FinSequence of F_{1}() st p ^ q is F_{2}() -element & P_{1}[p ^ q] holds

P_{1}[q ^ p]
and

A2: for p being Element of F_{2}() -tuples_on F_{1}() st P_{1}[p] holds

for i being Nat st i < F_{2}() & p = (p /^ i) ^ (p | i) holds

i = 0

P

A2: for p being Element of F

for i being Nat st i < F

i = 0

proof end;

theorem Th6: :: FRIENDS1:6

for k, n being Nat

for X being non empty set

for A being non empty finite Subset of X

for P being Function of X,(bool X) st ( for x being object st x in X holds

card (P . x) = n ) holds

card { F where F is Element of (k + 1) -tuples_on X : ( F . 1 in A & ( for i being Nat st i in Seg k holds

F . (i + 1) in P . (F . i) ) ) } = (card A) * (n |^ k)

for X being non empty set

for A being non empty finite Subset of X

for P being Function of X,(bool X) st ( for x being object st x in X holds

card (P . x) = n ) holds

card { F where F is Element of (k + 1) -tuples_on X : ( F . 1 in A & ( for i being Nat st i in Seg k holds

F . (i + 1) in P . (F . i) ) ) } = (card A) * (n |^ k)

proof end;

theorem Th7: :: FRIENDS1:7

for p being FinSequence st len p is prime & ex i being Nat st

( 0 < i & i < len p & p = (p /^ i) ^ (p | i) ) holds

rng p c= {(p . 1)}

( 0 < i & i < len p & p = (p /^ i) ^ (p | i) ) holds

rng p c= {(p . 1)}

proof end;

:: deftheorem Def1 defines universal_friend FRIENDS1:def 1 :

for R being Relation

for x being Element of field R holds

( x is universal_friend iff for y being object st y in (field R) \ {x} holds

[x,y] in R );

for R being Relation

for x being Element of field R holds

( x is universal_friend iff for y being object st y in (field R) \ {x} holds

[x,y] in R );

definition

let R be Relation;

end;
attr R is with_universal_friend means :: FRIENDS1:def 2

ex x being Element of field R st x is universal_friend ;

ex x being Element of field R st x is universal_friend ;

:: deftheorem defines with_universal_friend FRIENDS1:def 2 :

for R being Relation holds

( R is with_universal_friend iff ex x being Element of field R st x is universal_friend );

for R being Relation holds

( R is with_universal_friend iff ex x being Element of field R st x is universal_friend );

:: deftheorem Def3 defines friendship_graph_like FRIENDS1:def 3 :

for R being Relation holds

( R is friendship_graph_like iff for x, y being object st x in field R & y in field R & x <> y holds

ex z being object st (Im (R,x)) /\ (Coim (R,y)) = {z} );

for R being Relation holds

( R is friendship_graph_like iff for x, y being object st x in field R & y in field R & x <> y holds

ex z being object st (Im (R,x)) /\ (Coim (R,y)) = {z} );

registration

existence

ex b_{1} being Relation st

( b_{1} is finite & b_{1} is symmetric & b_{1} is irreflexive & b_{1} is friendship_graph_like )

end;
ex b

( b

proof end;

:: Friendship graph

definition
end;

Lm5: for x, y, z being object

for P being finite Relation

for t being object st P is friendship_graph_like & x <> y & [x,z] in P & [z,y] in P & [x,t] in P & [t,y] in P holds

z = t

proof end;

theorem Th9: :: FRIENDS1:9

for x, y being object

for FSG being Friendship_Graph st x in field FSG & y in field FSG & not [x,y] in FSG holds

card (Im (FSG,x)) = card (Im (FSG,y))

for FSG being Friendship_Graph st x in field FSG & y in field FSG & not [x,y] in FSG holds

card (Im (FSG,x)) = card (Im (FSG,y))

proof end;

theorem Th10: :: FRIENDS1:10

for x being object

for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG holds

card (Im (FSG,x)) > 2

for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG holds

card (Im (FSG,x)) > 2

proof end;

theorem Th11: :: FRIENDS1:11

for x, y being object

for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG & y in field FSG holds

card (Im (FSG,x)) = card (Im (FSG,y))

for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG & y in field FSG holds

card (Im (FSG,x)) = card (Im (FSG,y))

proof end;

theorem Th12: :: FRIENDS1:12

for x being object

for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG holds

card (field FSG) = 1 + ((card (Im (FSG,x))) * ((card (Im (FSG,x))) - 1))

for FSG being Friendship_Graph st FSG is without_universal_friend & x in field FSG holds

card (field FSG) = 1 + ((card (Im (FSG,x))) * ((card (Im (FSG,x))) - 1))

proof end;

theorem :: FRIENDS1:13

for FSG being Friendship_Graph

for x, y being Element of field FSG st x is universal_friend & x <> y holds

ex z being object st

( Im (FSG,y) = {x,z} & Im (FSG,z) = {x,y} )

for x, y being Element of field FSG st x is universal_friend & x <> y holds

ex z being object st

( Im (FSG,y) = {x,z} & Im (FSG,z) = {x,y} )

proof end;