background image

The star-composition of

a

with

f

is an anchored relation of the form

λi

dom

A

:

Dst

f

i

defined

by the formula

L

GR StarComp

(

a

;

f

)

⇔ ∃

y

GR

a

Y

i

n

atoms

A

i

i

n

:

y

i

[

f

i

]

L

i

.

Definition 139.

I will call a poset

starrish

when

⋆a

is a free star for every element

a

of this poset.

Theorem 140.

1. If

a

is a pre-staroid then StarComp

(

a

;

f

)

is a staroid.

2. If

a

is a completary staroid and Dst

f

i

is a starrish join-semilattice for every

i

n

then

StarComp

(

a

;

f

)

is a completary staroid.

Proof.

1. First prove that StarComp

(

a

;

f

)

is a pre-staroid. We need to prove that

(

val

f

)

j

L

is a free

star, that is

{

X

(

form

f

)

j

|

L

∪ {

(

j

;

X

)

} ∈

GR

f

}

is a free star, that is the following is a

free star

{

X

(

form

f

)

j

|

R

(

X

)

}

where

R

(

X

) =

y

Q

i

n

atoms

A

i

: (

i

n

: (

i

j

y

i

[

f

i

]

L

i

)

y

j

[

f

i

]

X

y

a

)

.

R

=

y

Q

i

n

atoms

A

i

: (

i

n

: (

i

j

y

i

[

f

i

]

L

i

)

y

j

[

f

j

]

X

y

j

(

val

)

j

(

a

|

n

\{

j

}

)) =

y

Q

i

n

\{

j

}

atoms

A

i

, y

atoms

A

j

: (

i

n

:

y

i

[

f

i

]

L

i

y

[

f

j

]

X

y

(

val

)

j

(

a

|

n

\{

j

}

)) =

y

Q

i

n

\{

j

}

atoms

A

i

i

n

:

y

i

[

f

i

]

L

i

∧ ∃

y

atoms

A

j

: (

y

[

f

j

]

X

y

(

val

)

j

(

a

|

n

\{

j

}

))

If

y

Q

i

n

\{

j

}

atoms

A

i

i

n

:

y

i

[

f

i

]

L

i

is false our statement is obvious. We can

assume it is true.

So it is enough to prove that

{

X

(

form

f

)

j

| ∃

y

atoms

A

j

: (

y

[

f

j

]

X

y

(

val

)

j

(

a

|

n

\{

j

}

))

}

is a free star. That is

Q

=

{

X

(

form

f

)

j

| ∃

y

(

atoms

A

j

)

(

val

)

j

(

a

|

n

\{

j

}

):

y

[

f

j

]

X

}

is a free star.

0

(

form

f

)

j

Q

is obvious. That

Q

is an upper set is obvious. It remains to

prove that

X

0

X

1

Q

X

0

Q

X

1

Q

for every

X

0

, X

1

(

form

f

)

j

. Let

X

0

X

1

Q

.

Then there exist

y

(

atoms

A

j

)

(

val

)

j

(

a

|

n

\{

j

}

)

such that

y

[

f

j

]

X

0

X

1

. Consequently

y

[

f

j

]

X

0

y

[

f

j

]

X

1

. But then

X

0

Q

X

1

Q

.

To finish the proof we need to show that GR StarComp

(

a

;

f

)

is an upper set, but this

is obvious.

2. Let

a

is a completary staroid. Let

L

0

L

1

GR StarComp

(

a

;

f

)

that is

y

Q

i

n

atoms

A

i

:

(

i

n

:

y

i

[

f

i

]

L

0

i

L

1

i

y

a

)

that is

c

∈ {

0

,

1

}

n

, y

Q

i

n

atoms

A

i

: (

i

n

:

y

i

[

f

i

]

L

c

(

i

)

i

y

a

)

(taken into account that Dst

f

i

is starrish) that is

c

∈ {

0

,

1

}

n

:

(

λi

n

:

L

c

(

i

)

i

)

GR StarComp

(

a

;

f

)

. So GR StarComp

(

a

;

f

)

is a completary staroid.

Lemma 141.

b

Anch

(

A

)

StarComp

(

a

;

f

)

⇔ ∀

A

a, B

b, i

n

:

A

i

[

f

i

]

B

i

for anchored relations

a

and

b

.

Proof.

b

StarComp

(

a

;

f

)

x

Anch

(

A

): (

x

b

x

StarComp

(

a

;

f

))

x

Anch

(

A

): (

x

b

∧ ∀

B

x

:

B

StarComp

(

a

;

f

))

x

Anch

(

A

):

 

x

b

∧ ∀

B

x

A

Y

i

dom

A

A

i

: (

i

n

:

A

i

[

f

i

]

B

i

A

a

)

!

x

Anch

(

A

): (

x

b

∧ ∀

B

x, A

a, i

n

:

A

i

[

f

i

]

B

i

)

B

b, A

a, i

n

:

A

i

[

f

i

]

B

i

.

22

Section 11