background image

Proof.

L

2

GR

DQ

(

C

)

f

EQ

Strd

a

,

L

2

GR StarComp

¡ Q

Strd

a

;

f

, 9

y

2

Q

i

2

dom

A

atoms

A

i

8

i

2

n

:

(

y

i

[

f

i

]

L

i

^

y

i

/

a

i

)

, 8

i

2

n

9

y

2

atoms

A

i

: (

y

[

f

i

]

L

i

^

y

/

a

i

)

, 8

i

2

n

:

a

i

[

f

i

]

L

i

, 8

i

2

n

:

L

i

/

h

f

i

i

a

i

,

L

2

GR

Q

i

2

n

Strd

h

f

i

i

a

i

.

Conjecture 17.155.

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

Denition 17.156.

Let

f

be an indexed family of pointfree funcoids with every Src

f

i

and Dst

f

i

(for all

i

2

dom

f

) being a poset with least element.

Simple product

of

f

is

Y

(

S

)

f

=

 

x

2

Y

i

2

dom

f

Src

f

i

:

i

2

dom

f

:

h

f

i

i

x

i

;

y

2

Y

i

2

dom

f

Dst

f

i

:

i

2

dom

f

:

h

f

i

¡

1

i

y

i

!

:

Proposition 17.157.

Simple product is a pointfree funcoid

Y

(

S

)

f

2

FCD

  Y

i

2

dom

f

Src

f

i

;

Y

i

2

dom

f

Dst

f

i

!

:

Proof.

Let

x

2

Q

i

2

dom

f

Src

f

i

and

y

2

Q

i

2

dom

f

Dst

f

i

. Then (take into account that Src

f

i

and Dst

f

i

are posets with least elements)

y

/

¡

x

2

Q

i

2

dom

f

Src

f

i

:

i

2

dom

f

:

h

f

i

i

x

i

x

,

y

/

i

2

dom

f

:

h

f

i

i

x

i

, 9

i

2

dom

f

:

y

i

/

h

f

i

i

x

i

, 9

i

2

dom

f

:

x

i

/

h

f

i

¡

1

i

y

i

,

x

/

i

2

dom

f

:

h

f

i

¡

1

i

y

i

,

x

/

¡

y

2

Q

i

2

dom

f

Dst

f

i

:

i

2

dom

f

:

h

f

i

¡

1

i

y

i

y

.

Obvious 17.158.

DQ

(

S

)

f

E

x

=

i

2

dom

f

:

h

f

i

i

x

i

for

x

2

Q

Src

f

i

.

Obvious 17.159.

DQ

(

S

)

f

E

x

i

=

h

f

i

i

x

i

for

x

2

Q

Src

f

i

.

Proposition 17.160.

f

i

can be restored if we know

Q

(

S

)

f

if

f

i

is a family of pointfree funcoids

between posets with least elements.

Proof.

Let's restore the value of

h

f

i

i

x

where

i

2

dom

f

and

x

2

Src

f

i

.

Let

x

i

0

=

x

and

x

j

0

= 0

for

j

=

/

i

.

Then

h

f

i

i

x

=

h

f

i

i

x

i

0

=

DQ

(

S

)

f

E

x

0

i

.

We have restored the value of

h

f

i

i

. Restoring the value of

h

f

i

¡

1

i

is similar.

Remark 17.161.

In the above proposition it is not required that

f

i

are non-zero.

Proposition 17.162.

 Q

(

S

)

g

 Q

(

S

)

f

=

Q

i

2

n

(

S

)

(

g

i

f

i

)

for

n

-indexed families

f

and

g

of

composable pointfree funcoids between posets with least elements.

Proof.

DQ

i

2

n

(

S

)

(

g

i

f

i

)

E

x

=

i

2

dom

f

:

h

g

i

f

i

i

x

i

=

i

2

dom

f

:

h

g

i

ih

f

i

i

x

i

=

DQ

(

S

)

g

E

i

2

dom

f

:

h

f

i

i

x

i

=

DQ

(

S

)

g

ED Q

(

S

)

f

E

x

=

D Q

(

S

)

g

 Q

(

S

)

f

E

x

.

Thus

DQ

i

2

n

(

S

)

(

g

i

f

i

)

E

=

D Q

(

S

)

g

 Q

(

S

)

f

E

.

D Q

(

S

)

(

g

i

f

i

)

¡

1

E

=

D Q

(

S

)

g

 Q

(

S

)

f

¡

1

E

is similar.

Corollary 17.163.

 Q

(

S

)

f

k

¡

1

:::

 Q

(

S

)

f

0

=

Q

i

2

n

(

S

)

(

f

k

¡

1

:::

f

0

)

for every

n

-indexed

families

f

0

; :::; f

n

¡

1

of composable pointfree funcoids between posets with least elements.

226

Multifuncoids and staroids