background image

Proof.

It follows from the theorem ?? in [3].

Conjecture 148.

GR StarComp

(

a

pFCD

b

;

f

) =

GR StarComp

(

a

;

f

)

pFCD

GR StarComp

(

b

;

f

)

if

f

is a pointfree funcoid and

a

,

b

are multifuncoids of the same form, composable with

f

.

12 More on cross-composition of funcoids

Lemma 149.

Let

f

is a staroid such that

(

form

f

)

i

is a boolean lattice for each

i

arity

f

. Let

a

Q

i

arity

f

F

(

form

f

)

i

.

If

f

Q

Strd

a

then

f

=

StarComp

f

;

λi

dom

A

:

I

a

i

FCD

(

A

i

)

.

Proof.

Let

f

Q

Strd

a

. Then

L

GR

f

L

a

.

L

GR StarComp

f

;

λi

dom

A

:

I

a

i

FCD

(

A

i

)

⇔ ∃

y

GR

f

Q

i

n

atoms

A

i

i

n

:

y

i

h

I

a

i

FCD

(

A

i

)

i

L

i

⇔ ∃

y

GR

f

Q

i

n

atoms

A

i

i

n

: (

y

i

L

i

y

i

a

i

)

⇔ ∃

y

GR

f

Q

i

n

atoms

A

i

i

n

: (

y

i

L

i

y

i

a

i

)

⇔ ∃

y

GR

f

Q

i

n

atoms

A

i

i

n

:

y

i

L

i

because

f

GR

g

y

a

.

If

L

f

then there exists

y

GR

f

Q

i

n

atoms

A

i

such as

y

L

and thus

i

n

:

y

i

L

i

(by the theorem 81).

We have

L

GR StarComp

f

;

λi

dom

A

:

I

a

i

FCD

(

A

i

)

L

f

that is GR StarComp

f

;

λi

dom

A

:

I

a

i

FCD

(

A

i

)

f

. The other directoin is obvious.

Theorem 150.

Let

f

is a staroid such that

(

form

f

)

i

is a boolean lattice for each

i

arity

f

. Let

a

Q

i

arity

f

F

(

form

f

)

i

. Then

f

FCD

(

form

f

)

Y

Strd

a

=

StarComp

f

;

λi

dom

A

:

I

a

i

FCD

(

A

i

)

.

Proof.

h

=

def

StarComp

f

;

λi

dom

A

:

I

a

i

FCD

(

A

i

)

.

Obviously

h

f

and

h

Q

Strd

a

.

Suppose

g

f

and

g

Q

Strd

a

.

x

g

x

StarComp

g

;

λi

dom

A

:

I

a

i

FCD

(

A

i

)

x

StarComp

f

;

λi

dom

A

:

I

a

i

FCD

(

A

i

)

x

h

(used the proposition above).

So

g

h

.

Corollary 151.

Let

f

is a completary staroid such that

(

form

f

)

i

is a boolean lattice for each

i

arity

f

. Let

a

Q

i

arity

f

F

(

form

f

)

i

. Then

f

cStrd

(

form

f

)

Y

Strd

a

=

StarComp

f

;

λi

dom

A

:

I

a

i

FCD

(

A

i

)

.

Proof.

Using the theorem 140.

Theorem 152.

Let

f

is a staroid such that

(

form

f

)

i

is a boolean lattice for each

i

arity

f

. Let

a

Q

i

arity

f

F

(

form

f

)

i

. Then

f

FCD

(

form

f

)

Q

Strd

a

a

f

.

Proof.

f

FCD

(

form

f

)

Q

Strd

a

f

FCD

(

form

f

)

Q

Strd

a

0

StarComp

f

;

λi

arity

f

:

I

a

i

FCD

(

A

i

)

0

FCD

(

form

f

)

⇔ ∃

L

n

, y

GR

f

Q

i

n

atoms

A

i

i

n

:

y

i

h

I

a

i

FCD

(

A

i

)

i

L

i

⇔ ∃

L

n

,

y

GR

f

Q

i

n

atoms

A

i

i

n

: (

y

i

a

i

y

i

L

i

)

⇔ ∃

y

GR

f

Q

i

n

atoms

A

i

i

n

:

y

i

a

i

GR

f

Q

i

n

atoms

a

i

∅ ⇔

a

f

.

Corollary 153.

Let

f

is a completary staroid such that

(

form

f

)

i

is a boolean lattice for each

i

arity

f

. Let

a

Q

i

arity

f

F

(

form

f

)

i

. Then

f

cStrd

(

form

f

)

Q

Strd

a

a

f

.

24

Section 12