background image

17.11. PRODUCT OF AN ARBITRARY NUMBER OF FUNCOIDS

261

L

GR StarComp(

a

;

f

)

⇔ ∃

y

GR

a

Q

i

n

atoms

A

i

:

y R

(

f

)

L

.

L

GR StarComp(StarComp(

a

;

f

);

g

)

p

GR StarComp(

a

;

f

)

Y

i

n

atoms

A

i

:

p R

(

g

)

L

p, y

GR

a

Y

i

n

atoms

A

i

: (

y R

(

f

)

p

p R

(

g

)

L

)

y

GR

a

Y

i

n

atoms

A

i

y

:(

R

(

g

)

R

(

f

))

L

y

GR

a

Y

i

n

atoms

A

i

y

:

R

(

λi

n

:

g

i

f

i

)

L

y

GR

a

Y

i

n

atoms

A

i

y

i

n

:

y

i

[

g

i

f

i

]

L

i

L

GR StarComp(

a

;

λi

n

:

g

i

f

i

)

because

p

GR StarComp(

a

;

f

)

⇔ ∃

y

GR

a

Q

i

n

atoms

A

i

y

:

y R

(

f

)

p

.

2

Obvious.

3

It follows from the lemma above.

Theorem

1351

.

D

Q

(

C

)

f

E

Q

Strd

a

=

Q

Strd

i

n

h

f

i

i

a

i

for every families

f

=

f

i

n

of

pointfree funcoids between atomic posets and

a

=

a

i

n

where

a

i

Src

f

i

.

Proof.

L

GR

*

(

C

)

Y

f

+

Strd

Y

a

L

GR StarComp(

Strd

Y

a

;

f

)

y

Y

i

dom

A

atoms

A

i

i

n

: (

y

i

[

f

i

]

L

i

y

i

6

a

i

)

i

n

y

atoms

A

i

: (

y

[

f

i

]

L

i

y

6

a

i

)

i

n

:

a

i

[

f

i

]

L

i

i

n

:

L

i

6 h

f

i

i

a

i

L

GR

Strd

Y

i

n

h

f

i

i

a

i

.

Conjecture

1352

.

StarComp(

a

t

b

;

f

) = StarComp(

a

;

f

)

t

StarComp(

b

;

f

)

for anchored relations

a

,

b

of a form

A

, where every

A

i

is a distributive lattice, and

an indexed family

f

of pointfree funcoids with Src

f

i

=

A

i

.

17.11.6. Simple product of pointfree funcoids.

Definition

1353

.

Let

f

be an indexed family of pointfree funcoids with every

Src

f

i

and Dst

f

i

(for all

i

dom

f

) being a poset with least element.

Simple product

of

f

is

(

S

)

Y

f

=

λx

Y

i

dom

f

Src

f

i

:

λi

dom

f

:

h

f

i

i

x

i

;

λy

Y

i

dom

f

Dst

f

i

:

λi

dom

f

:

f

1

i

y

i

.