background image

Thus, by the denition of completary staroid,

L

0

2

GR

f

_

L

1

2

GR

f

that is

X

0

2

(

val

f

)

i

K

_

X

1

2

(

val

f

)

i

K:

So

(

val

f

)

i

K

is a free star (taken into account that

z

i

= 0

(

form

f

)

i

)

z

2

/

GR

f

and that

(

val

f

)

i

K

is

an upper set).

Exercise 17.2.

Write a simplied proof for the case if every

(

form

f

)

i

is a join-semilattice.

Lemma 17.57.

Every nitary prestaroid is completary.

Proof.

9

c

2 f

0

;

1

g

n

: (

i

2

n

:

L

c

(

i

)

i

)

2

GR

f

, 9

c

2 f

0

;

1

g

n

¡

1

: (

f

(

n

¡

1;

L

0

(

n

¡

1))

g [

(

i

2

n

¡

1:

L

c

(

i

)

i

))

2

GR

f

_

(

f

(

n

¡

1;

L

1

(

n

¡

1))

g [

(

 i

2

n

¡

1:

L

c

(

i

)

i

))

2

GR

f

, 9

c

2 f

0

;

1

g

n

¡

1

:

L

0

(

n

¡

1)

2

(

val

f

)

n

¡

1

(

i

2

n

¡

1:

L

c

(

i

)

i

)

_

L

1

(

n

¡

1)

2

(

val

f

)

n

¡

1

(

i

2

n

¡

1:

L

c

(

i

)

i

)

, 9

c

2 f

0

;

1

g

n

¡

1

8

K

2

(

form

f

)

n

¡

1

: (

K

w

L

0

(

n

¡

1)

_

K

w

L

1

(

n

¡

1)

)

K

2

(

val

f

)

n

¡

1

(

 i

2

n

¡

1:

L

c

(

i

)

i

))

, 9

c

2 f

0

;

1

g

n

¡

1

8

K

2

(

form

f

)

n

¡

1

: (

K

w

L

0

(

n

¡

1)

_

K

w

L

1

(

n

¡

1)

) f

(

n

¡

1;

K

)

g [

(

i

2

n

¡

1:

L

c

(

i

)

i

))

2

GR

f

,

:::

, 8

K

2

Q

form

f

: (

K

w

L

0

^

K

w

L

1

)

K

2

GR

f

)

.

Exercise 17.3.

Prove the simpler special case of the above theorem when the form is a family of join-semilat-

tices.

Theorem 17.58.

For nite arity the following are the same:

1. prestaroids;
2. staroids;
3. completary staroids.

Proof.

f

is a nitary prestaroid

)

f

is a nitary completary staroid.

f

is a nitary completary staroid

)

f

is a nitary staroid.

f

is a nitary staroid

)

f

is a nitary prestaroid.

Denition 17.59.

We will denote the set of staroids, prestaroids, and completary staroids of a

form

A

correspondingly as

Strd

(

A

)

,

pStrd

(

A

)

, and

cStrd

(

A

)

.

17.4 Upgrading and downgrading a set regarding a ltrator

Let x a ltrator

(

A

;

Z

)

.

Denition 17.60.

f

=

f

\

Z

for every

f

2

P

A

(

downgrading

f

).

Denition 17.61.

f

=

f

L

2

A

j

up

L

f

g

for every

f

2

P

Z

(

upgrading

f

).

Obvious 17.62.

a

2

f

,

up

a

f

for every

f

2

P

Z

and

a

2

A

.

Proposition 17.63.

f

=

f

if

f

is an upper set for every

f

2

P

Z

.

Proof.

f

=

f

\

Z

=

f

L

2

Z

j

up

L

f

g

=

f

L

2

Z

j

L

2

f

g

=

f

\

Z

=

f

.

17.4.1 Upgrading and downgrading staroids

Let x a family

(

A

;

Z

)

of ltrators.

For a graph

f

of a staroid dene

f

and

f

taking the ltrator of

(

Q

A

;

Q

Z

)

.

For a staroid

f

dene:

[TODO: Dene for all anchored relations.]

form

f

=

Z

and GR

f

=

GR

f

;

form

f

=

A

and GR

f

=

GR

f :

Proposition 17.64.

(

val

f

)

i

L

= (

val

f

)

i

L

\

Z

i

for every

L

2

Q

Z

j

(

arity

f

)

nf

i

g

.

210

Multifuncoids and staroids