background image

This article presents another version of star-composition of funcoids.
Let

a

be a an anchored relation of the form

A

and dom

A

=

n

.

Let every

f

i

(for all

i

2

n

) be a pointfree funcoid with Src

f

i

=

A

i

.

The star-composition of

a

with

f

is an anchored relation of the form

i

2

dom

A

:

Dst

f

i

dened by

the formula

[TODO: it should have a distinct notation with the other star-composition of staroids]

L

2

GR StarComp

(

a

;

f

)

,

(

i

2

n

:

h

f

i

¡

1

i

L

i

)

2

GR

a:

Theorem 1.

Let Src

f

i

be separable join-semilattice and Dst

f

i

be a starrish join-semilattice for

every

i

2

n

for a set

n

. Let form

a

=

Q

i

2

n

(

Src

f

i

)

1. If

a

is a prestaroid then StarComp

(

a

;

f

)

is a prestaroid.

2. If

a

is a staroid then StarComp

(

a

;

f

)

is a staroid.

3. If

a

is a completary staroid and then StarComp

(

a

;

f

)

is a completary staroid.

Proof.

We have

h

f

i

¡

1

i

(

X

t

Y

) =

h

f

i

¡

1

i

X

t h

f

i

¡

1

i

Y

.

1. Let

L

2

Q

i

2

(

arity

f

)

nf

k

g

(

form

f

i

)

for some

k

2

n

and

X ; Y

2

form

f

k

. Then

X

t

Y

2 h

StarComp

(

a

;

f

)

i

k

L

,

i

2

dom

f

:

h

f

i

¡

1

i

X

t

Y

if

i

=

k

L

i

if

i

=

/

k

i

2

GR

a

,

 

i

2

dom

f

:

 (

h

f

i

¡

1

i

X

t h

f

i

¡

1

i

Y

if

i

=

k

h

f

i

¡

1

i

L

i

if

i

=

/

k

!

i

!

2

GR

a

,

h

f

i

¡

1

i

X

t h

f

i

¡

1

i

Y

2 h

a

i

k

(

i

2

(

dom

f

)

n f

k

g

:

h

f

i

¡

1

i

L

i

)

,

h

f

i

¡

1

i

X

2 h

a

i

k

(

i

2

n

n f

k

g

:

h

f

i

¡

1

i

L

i

)

_ h

f

i

¡

1

i

Y

2 h

a

i

k

(

i

2

n

n f

k

g

:

h

f

i

¡

1

i

L

i

)

,

 

 i

2

dom

f

:

 (

h

f

i

¡

1

i

X

if

i

=

k

h

f

i

¡

1

i

L

i

if

i

=

/

k

!

i

!

2

GR

a

_

 

 i

2

dom

f

:

 (

h

f

i

¡

1

i

Y

if

i

=

k

h

f

i

¡

1

i

L

i

if

i

=

/

k

!

i

!

2

GR

a

,

 i

2

dom

f

:

h

f

i

¡

1

i

X

if

i

=

k

L

i

if

i

=

/

k

i

2

GR

a

_

 i

2

dom

f

:

h

f

i

¡

1

i

Y

if

i

=

k

L

i

if

i

=

/

k

i

2

GR

a

,

X

2 h

StarComp

(

a

;

f

)

i

k

L

_

Y

2 h

StarComp

(

a

;

f

)

i

k

L:

Thus StarComp

(

a

;

f

)

is a pre-staroid.

2.

h

f

i

i

are monotone functions by the proposition 15.14. Thus

h

f

i

¡

1

i

X

i

v h

f

i

¡

1

i

Y

i

if

X ;

Y

2

Q

i

2

(

arity

f

)

nf

k

g

(

form

f

i

)

and

X

v

Y

. So if

a

is a staroid and

X

2

GR StarComp

(

a

;

f

)

then

(

 i

2

dom

f

:

h

f

i

¡

1

i

X

i

)

2

GR

a

then

(

 i

2

dom

f

:

h

f

i

¡

1

i

Y

i

)

2

GR

a

that is

Y

2

GR StarComp

(

a

;

f

)

.

3.

L

0

t

L

1

2

GR StarComp

(

a

;

f

)

,

(

i

2

n

:

h

f

i

¡

1

i

(

L

0

t

L

1

)

i

)

2

GR

a

,

(

i

2

n

:

h

f

i

¡

1

i

L

0

i

t h

f

i

¡

1

i

L

1

i

)

2

GR

a

,

9

c

2 f

0

;

1

g

: (

i

2

n

:

h

f

i

¡

1

i

L

c

(

i

)

i

)

2

GR

a

,

9

c

2 f

0

;

1

g

: (

i

2

n

:

L

c

(

i

)

i

)

2

GR StarComp

(

a

;

f

)

:

1