background image

Proof.

We need to prove that

Q

(

D

)

F

is an upper set. Let

a

2

Q

(

D

)

F

and an anchored relation

b

w

a

of the same form as

a

. We have

a

=

uncurry

z

for some

z

2

Q

F

that is

a

(

i

;

j

) = (

zi

)

j

for all

i

2

dom

F

and

j

2

dom

F

i

where

zi

2

F

i

. Also

b

(

i

;

j

)

w

a

(

i

;

j

)

. Thus

(

curry

b

)

i

w

zi

; curry

b

2

Q

F

because every

F

i

is an upper set and so

b

2

Q

(

D

)

F

.

Proposition 17.116.

Let

F

be an indexed family of anchored relations and every

(

form

F

)

i

is a

join-semilattice.

1.

Q

(

D

)

F

is a prestaroid if every

F

i

is a prestaroid.

2.

Q

(

D

)

F

is a staroid if every

F

i

is a staroid.

3.

Q

(

D

)

F

is a completary staroid if every

F

i

is a completary staroid.

Proof.

1. Let

q

2

arity

Q

(

D

)

F

that is

q

= (

i

;

j

)

where

i

2

dom

F

,

j

2

arity

F

i

; let

L

2

Y

0

@

 

form

Y

(

D

)

F

!

j

¡

arity

Q

(

D

)

F

nf

q

g

1

A

that is

L

(

i

0

;

j

0

)

2

form

Q

(

D

)

F

(

i

0

;

j

0

)

for every

(

i

0

;

j

0

)

2

arity

Q

(

D

)

F

n f

q

g

, that is

L

(

i

0

;

j

0

)

2

(

form

F

i

)

j

. We have

X

2

form

Q

(

D

)

F

(

i

;

j

)

,

X

2

(

form

F

i

)

j

. So

 

val

Y

(

D

)

F

!

(

i

;

j

)

L

=

(

X

2

(

form

F

i

)

j

j

L

[ f

((

i

;

j

);

X

)

g 2

GR

Y

(

D

)

F

)

;

 

val

Y

(

D

)

F

!

(

i

;

j

)

L

=

X

2

(

form

F

i

)

j

j 9

z

2

Y

(

GR

F

):

L

[ f

((

i

;

j

);

X

)

g

=

uncurry

z

 

;

 

val

Y

(

D

)

F

!

(

i

;

j

)

L

=

n

X

2

(

form

F

i

)

j

j 9

z

2

(

GR

F

)

j

¡

arity

Q

(

D

)

F

nf

(

i

;

j

)

g

; v

2

GR

F

i

:

(

L

=

uncurry

z

^

v

j

=

X

)

o

;

val

Q

(

D

)

F

(

i

;

j

)

L

=

n

X

2

(

form

F

i

)

j

j 9

z

2

(

GR

F

)

j

¡

arity

Q

(

D

)

F

nf

(

i

;

j

)

g

:

L

=

uncurry

z

^ 9

v

2

GR

F

i

:

v

j

=

X

o

.

If

9

z

2

(

GR

F

)

j

¡

arity

Q

(

D

)

F

nf

(

i

;

j

)

g

:

L

=

uncurry

z

is false then

val

Q

(

D

)

F

(

i

;

j

)

L

=

;

is a free star. We can assume it is true. So

 

val

Y

(

D

)

F

!

(

i

;

j

)

L

=

f

X

2

(

form

F

i

)

j

j 9

v

2

GR

F

i

:

v

j

=

X

g

:

Thus

 

val

Y

(

D

)

F

!

(

i

;

j

)

L

=

f

X

2

(

form

F

i

)

j

j 9

K

2

(

form

F

i

)

j

(

arity

F

i

)

nf

j

g

:

K

[ f

(

j

;

X

)

g 2

GR

F

i

g

=

f

X

2

(

form

F

i

)

j

j 9

K

2

(

form

F

i

)

j

(

arity

F

i

)

nf

j

g

:

X

2

(

val

F

i

)

j

K

g

:

Thus

A

t

B

2

val

Q

(

D

)

F

(

i

;

j

)

L

, 9

K

2

(

form

F

i

)

j

(

arity

F

i

)

nf

j

g

:

A

t

B

2

(

val

F

i

)

j

K

,

9

K

2

(

form

F

i

)

j

(

arity

F

i

)

nf

j

g

: (

A

2

(

val

F

i

)

j

K

_

B

2

(

val

F

i

)

j

K

)

, 9

K

2

(

form

F

i

)

j

(

arity

F

i

)

nf

j

g

:

A

2

(

val

F

i

)

j

K

_ 9

K

2

(

form

F

i

)

j

(

arity

F

i

)

nf

j

g

:

B

2

(

val

F

i

)

j

K

,

A

2

val

Q

(

D

)

F

(

i

;

j

)

L

_

B

2

val

Q

(

D

)

F

(

i

;

j

)

L

. Least element

0

is not in

val

Q

(

D

)

F

(

i

;

j

)

L

because

K

[ f

(

j

;

0)

g 2

/

GR

F

i

.

17.9 On products of staroids

217