17.3. DEFINITION OF STAROIDS

239

Obvious

1243

.

X

(val

f

)

i

L

L

∪ {

(

i

;

X

)

} ∈

GR

f

.

Proposition

1244

.

f

can be restored knowing form(

f

) and (val

f

)

i

for some

i

arity

f

.

Proof.

GR

f

=

K

Q

form

f

K

GR

f

=

L

∪ {

(

i

;

X

)

}

L

Q

(form

f

)

|

(arity

f

)

\{

i

}

, X

(form

f

)

i

, L

∪ {

(

i

;

X

)

} ∈

GR

f

=

L

∪ {

(

i

;

X

)

}

L

Q

(form

f

)

|

(arity

f

)

\{

i

}

, X

(val

f

)

i

L

.

Definition

1245

.

A

prestaroid

is an anchored relation

f

between posets such

that (val

f

)

i

L

is a free star for every

i

arity

f

,

L

Q

(form

f

)

|

(arity

f

)

\{

i

}

.

Definition

1246

.

A

staroid

is a prestaroid whose graph is an upper set (on

the poset

Q

form(

f

)).

Proposition

1247

.

If

L

Q

form

f

and

L

i

=

(form

f

)

i

for some

i

arity

f

then

L /

f

if

f

is a prestaroid.

Proof.

Let

K

=

L

|

(arity

f

)

\{

i

}

. We have

/

(val

f

)

i

K

;

K

∪ {

(

i

; 0)

}

/

f

;

L /

f

.

Definition

1248

.

Infinitary anchored relation

is such an anchored relation

whose arity is infinite;

finitary anchored relation

is such an anchored relation whose

arity is finite.

FiXme

: Move this definition up.

Next we will define

completary staroids

. First goes the general case, next sim-

pler case for the special case of join-semilattices instead of arbitrary posets.

Definition

1249

.

A

completary staroid

is an anchored relation between posets

conforming to the formulas:

1

.

K

Q

form

f

: (

K

w

L

0

K

w

L

1

K

GR

f

) is equivalent to

c

∈ {

0

,

1

}

n

: (

λi

n

:

L

c

(

i

)

i

)

GR

f

for every

L

0

, L

1

Q

form

f

.

2

. If

L

Q

form

f

and

L

i

=

(form

f

)

i

for some

i

arity

f

then

L /

GR

f

.

Lemma

1250

.

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

Q

form

f

and

L

0

GR

f

. Then taking

c

=

n

× {

0

}

we get

λi

n

:

L

c

(

i

)

i

=

λi

n

:

L

0

i

=

L

0

GR

f

and thus

L

1

GR

f

because

L

1

w

L

0

L

1

w

L

1

.

Proposition

1251

.

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

semilattices is a completary staroid iff both:

1

.

L

0

t

L

1

GR

f

⇔ ∃

c

∈ {

0

,

1

}

n

: (

λi

n

:

L

c

(

i

)

i

)

GR

f

for every

L

0

, L

1

Q

form

f

.

2

. If

L

Q

form

f

and

L

i

=

(form

f

)

i

for some

i

arity

f

then

L /

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

Q

form

f

and

L

0

f

. Then taking

c

=

n

× {

0

}

we get

λi

n

:

L

c

(

i

)

i

=

λi

n

:

L

0

i

=

L

0

GR

f

and thus

L

1

=

L

0

t

L

1

f

.

Thus to finish the proof it is enough to show that

L

0

t

L

1

GR

f

⇔ ∀

K

Y

form

f

: (

K

w

L

0

K

w

L

1

K

GR

f

)

under condition that GR

f

is an upper set. But this is obvious.