background image

17.12. MULTIRELOIDS

266

Proof.

FiXme

: Is there necessity to consider

S

=

special case?

If

S

=

then

d

 Q

RLD

a

a

S

=

d

=

>

RLD

(

A

)

and

RLD

Y

i

dom

A

l

D

F

(

A

i

)

E

Pr

i

S

=

RLD

Y

i

dom

A

l

D

F

(

A

i

)

E

=

RLD

Y

i

dom

A

l

=

RLD

Y

i

dom

A

>

F

(

A

i

)

=

>

RLD

(

A

)

,

thus

d

 Q

RLD

a

a

S

=

Q

RLD

i

dom

A

d

F

(

A

i

)

Pr

i

S

.

Let

S

6

=

.

d

F

(

A

i

)

Pr

i

S

v

d

F

(

A

i

)

{

a

i

}

=

a

i

for every

a

S

because

a

i

Pr

i

S

.

Thus

Q

RLD

i

dom

A

d

F

(

A

i

)

Pr

i

S

v

Q

RLD

a

;

l

(

Q

RLD

a

a

S

)

w

RLD

Y

i

dom

A

l

D

F

(

A

i

)

E

Pr

i

S.

Now suppose

F

GR

Q

RLD

i

dom

A

d

F

(

A

i

)

Pr

i

S

. Then there exists

X

Q

i

dom

A

d

F

(

A

i

)

Pr

i

S

such that

F

Q

X

. It is enough to prove that there

exist

a

S

such that

F

GR

Q

RLD

a

. For this it is enough

Q

X

GR

Q

RLD

a

.

Really,

X

i

d

F

(

A

i

)

Pr

i

S

thus

X

i

a

i

for every

A

S

because Pr

i

S

{

a

i

}

.

Thus

Q

X

GR

Q

RLD

a

.

Definition

1372

.

I call a multireloid

principal

iff its graph is a principal fil-

ter.

FiXme

: Prove that principal multireloids are the same as multireloid correspond-

ing to a relation.

Definition

1373

.

I call a multireloid

convex

iff it is a join of reloidal products.

Theorem

1374

.

StarComp(

a

t

b

;

f

) = StarComp(

a

;

f

)

t

StarComp(

b

;

f

) for

multireloids

a

,

b

and an indexed family

f

of reloids with Src

f

i

= (form

a

)

i

=

(form

b

)

i

.

Proof.

GR(StarComp(

a

;

f

)

t

StarComp(

b

;

f

)) =

l

RLD

(form

a

)

StarComp(

A

;

F

)

A

GR

a, F

Q

i

n

GR

f

i

t

l

RLD

(form

b

)

StarComp(

B

;

F

)

B

GR

b, F

Q

i

n

GR

f

i

=

l

RLD

(form

a

)

StarComp(

A

;

F

)

t ↑

RLD

(form

b

)

StarComp(

B

;

F

)

A

GR

a, B

GR

b, F

Q

i

n

GR

f

i

=

l

RLD

(form

a

)

(StarComp(

A

;

F

)

StarComp(

B

;

F

))

A

GR

a, B

GR

b, F

Q

i

n

GR

f

i

=

l

RLD

(form

a

)

StarComp(

A

B

;

F

)

A

GR

a, B

GR

b, F

Q

i

n

GR

f

i

=

l

RLD

(form

a

)

StarComp(

C

;

F

)

C

GR(

a

t

b

)

, F

Q

i

n

GR

f

i

=

GR StarComp(

a

t

b

;

f

)

.