 Denition 17.49.

A

prestaroid

is an anchored relation

f

between posets such that

(

val

f

)

i

L

is a

free star for every

i

2

arity

f

,

L

2

Q

(

form

f

)

j

(

arity

f

)

nf

i

g

.

Denition 17.50.

A

staroid

is a prestaroid whose graph is an upper set (on the poset

Q

form

(

f

)

).

Proposition 17.51.

If

L

2

Q

form

f

and

L

i

= 0

(

form

f

)

i

for some

i

2

arity

f

then

L

2

/

f

if

f

is a

prestaroid.

Proof.

Let

K

=

L

j

(

arity

f

)

nf

i

g

. We have

0

2

/ (

val

f

)

i

K

;

K

[ f

(

i

; 0)

g 2

/

f

;

L

2

/

f

.

Denition 17.52.

Innitary anchored relation

is such an anchored relation whose arity is innite;

nitary anchored relation

is such an anchored relation whose arity is nite.

Next we will dene

completary staroids

. First goes the general case, next simpler case for the

special case of join-semilattices instead of arbitrary posets.

Denition 17.53.

A

completary staroid

is an anchored relation between posets conforming to the

formulas:

1.

8

K

2

Q

form

f

: (

K

w

L

0

^

K

w

L

1

)

K

2

GR

f

)

, 9

c

2 f

0

;

1

g

n

: (

i

2

n

:

L

c

(

i

)

i

)

2

GR

f

for

every

L

0

; L

1

2

Q

form

f

.

2. If

L

2

Q

form

f

and

L

i

= 0

(

form

f

)

i

for some

i

2

arity

f

then

L

2

/

GR

f

.

Lemma 17.54.

Every graph of completary staroid is an upper set.

Proof.

Let

f

be a completary staroid. Let

L

0

v

L

1

for some

L

0

; L

1

2

Q

form

f

and

L

0

2

GR

f

.

Then taking

c

=

n

f

0

g

we get

i

2

n

:

L

c

(

i

)

i

=

i

2

n

:

L

0

i

=

L

0

2

GR

f

and thus

L

1

2

GR

f

because

L

1

w

L

0

^

L

1

w

L

1

.

Proposition 17.55.

A relation between posets whose form is a family of join-semilattices is a

completary staroid i both:

1.

L

0

t

L

1

2

GR

f

, 9

c

2 f

0

;

1

g

n

: (

i

2

n

:

L

c

(

i

)

i

)

2

GR

f

for every

L

0

; L

1

2

Q

form

f

.

2. If

L

2

Q

form

f

and

L

i

= 0

(

form

f

)

i

for some

i

2

arity

f

then

L

2

/

GR

f

.

Proof.

Let the formulas (1) and (2) hold. Then

f

is an upper set: Let

L

0

v

L

1

for some

L

0

;

L

1

2

Q

form

f

and

L

0

2

f

. Then taking

c

=

n

f

0

g

we get

i

2

n

:

L

c

(

i

)

i

=

i

2

n

:

L

0

i

=

L

0

2

GR

f

and thus

L

1

=

L

0

t

L

1

2

f

.

Thus to nish the proof it is enough to show that

L

0

t

L

1

2

GR

f

, 8

K

2

Y

form

f

: (

K

w

L

0

^

K

w

L

1

)

K

2

GR

f

)

under condition that GR

f

is an upper set. But this is obvious.

Proposition 17.56.

Every completary staroid is a staroid.

Proof.

Let

f

be a completary staroid.

Let

i

2

arity

f

,

K

2

Q

i

2

(

arity

f

)

nf

i

g

(

form

f

)

i

. Let

L

0

=

K

[ f

(

i

;

X

0

)

g

,

L

1

=

K

[ f

(

i

;

X

1

)

g

for

some

X

0

; X

1

2

A

i

.

Let

8

Z

2

A

i

: (

Z

w

X

0

^

Z

w

X

1

)

Z

2

(

val

f

)

i

K

);

then

8

Z

2

A

i

: (

Z

w

X

0

^

Z

w

X

1

)

K

[ f

(

i

;

Z

)

g 2

GR

f

)

:

If

z

w

L

0

^

z

w

L

1

then

z

w

K

[ f

(

i

;

z

i

)

g

, thus taking into account that GR

f

is an upper set,

8

z

2

Y

A

: (

z

w

L

0

^

z

w

L

1

)

K

[ f

(

i

;

z

i

)

g 2

GR

f

)

:

8

z

2

Y

A

: (

z

w

L

0

^

z

w

L

1

)

z

2

GR

f

)

:

17.3 Definition of staroids

209