 17.3. DEFINITION OF STAROIDS

240

Proposition

1252

.

Every completary staroid is a staroid.

Proof.

Let

f

be a completary staroid.

Let

i

arity

f

,

K

Q

i

(arity

f

)

\{

i

}

(form

f

)

i

. Let

L

0

=

K

∪ {

(

i

;

X

0

)

}

,

L

1

=

K

∪ {

(

i

;

X

1

)

}

for some

X

0

, X

1

A

i

.

Let

Z

A

i

: (

Z

w

X

0

Z

w

X

1

Z

(val

f

)

i

K

);

then

Z

A

i

: (

Z

w

X

0

Z

w

X

1

K

∪ {

(

i

;

Z

)

} ∈

GR

f

)

.

If

z

w

L

0

z

w

L

1

then

z

w

K

∪ {

(

i

;

z

i

)

}

, thus taking into account that GR

f

is an

upper set,

z

Y

A

: (

z

w

L

0

z

w

L

1

K

∪ {

(

i

;

z

i

)

} ∈

GR

f

)

.

z

Y

A

: (

z

w

L

0

z

w

L

1

z

GR

f

)

.

Thus, by the definition of completary staroid,

L

0

GR

f

L

1

GR

f

that is

X

0

(val

f

)

i

K

X

1

(val

f

)

i

K.

So (val

f

)

i

K

is a free star (taken into account that

z

i

=

(form

f

)

i

z /

GR

f

and

that (val

f

)

i

K

is an upper set).

Exercise

1253

.

Write a simplified proof for the case if every (form

f

)

i

is a

join-semilattice.

Lemma

1254

.

Every finitary prestaroid is completary.

Proof.

FiXme

: It seems that the proof is with errors.

c

∈ {

0

,

1

}

n

: (

λi

n

:

L

c

(

i

)

i

)

GR

f

c

∈ {

0

,

1

}

n

1

:

(

{

(

n

1;

L

0

(

n

1))

} ∪

(

λi

n

1 :

L

c

(

i

)

i

))

GR

f

(

{

(

n

1;

L

1

(

n

1))

} ∪

(

λi

n

1 :

L

c

(

i

)

i

))

GR

f

!

c

∈ {

0

,

1

}

n

1

:

L

0

(

n

1)

(val

f

)

n

1

(

λi

n

1 :

L

c

(

i

)

i

)

L

1

(

n

1)

(val

f

)

n

1

(

λi

n

1 :

L

c

(

i

)

i

)

!

c

∈ {

0

,

1

}

n

1

K

(form

f

)

i

:

K

w

L

0

(

n

1)

K

w

L

1

(

n

1)

K

(val

f

)

n

1

(

λi

n

1 :

L

c

(

i

)

i

)

!

c

∈ {

0

,

1

}

n

1

K

(form

f

)

i

:

K

w

L

0

(

n

1)

K

w

L

1

(

n

1)

{

(

n

1;

K

)

} ∪

(

λi

n

1 :

L

c

(

i

)

i

)

GR

f

!

. . .

K

Y

form

f

: (

K

w

L

0

K

w

L

1

K

GR

f

)

.

Exercise

1255

.

Prove the simpler special case of the above theorem when the

form is a family of join-semilattices.

Theorem

1256

.

For finite arity the following are the same:

1

. prestaroids;

2

. staroids;

3

. completary staroids.

Proof.

f

is a finitary prestaroid

f

is a finitary completary staroid.

f

is a finitary completary staroid

f

is a finitary staroid.

f

is a finitary staroid

f

is a finitary prestaroid.