 Proof.

a

RLD

c

= (

b

RLD

c

)

(

a

RLD

b

) =

(corollary 7.18)

=

F

RLD

f

G

F

j

F

2

atoms

RLD

(

a

RLD

b

)

;

G

2

atoms

RLD

(

b

RLD

c

)

g

.

Theorem 25.

(

RLD

)

in

(

g

f

) = (

RLD

)

in

g

(

RLD

)

in

f

for every composable funcoids

f

and

g

.

[TODO: remove the conjecture as it is now proved.]

Proof.

(

RLD

)

in

g

(

RLD

)

in

f

=

(corollary 7.18)

=

F

RLD

f

G

F

j

F

2

atoms

RLD

(

RLD

)

in

f ;

G

2

atoms

RLD

(

RLD

)

in

g

g

Let

F

be an atom of the poset

RLD

(

Src

f

;

Dst

f

)

.

F

2

atoms

RLD

(

RLD

)

in

f

)

dom

F

RLD

im

F

/

atoms

RLD

(

RLD

)

in

f

)

(because

(

RLD

)

in

f

is a funcoidal reloid)

)

dom

F

RLD

im

F

v

atoms

RLD

(

RLD

)

in

f

but dom

F

RLD

im

F

v

atoms

RLD

(

RLD

)

in

f

)

F

2

atoms

RLD

(

RLD

)

in

f

is obvious.

So

F

2

atoms

RLD

(

RLD

)

in

f

,

dom

F

RLD

im

F

v

(

RLD

)

in

f

)

(

FCD

)(

dom

F

RLD

im

F

)

v

(

FCD

)(

RLD

)

in

f

,

dom

F

FCD

im

F

v

f

.

But dom

F

FCD

im

F

v

f

)

(

RLD

)

in

(

dom

F

FCD

im

F

)

v

(

RLD

)

in

f

,

dom

F

RLD

im

F

v

(

RLD

)

in

f

.

So

F

2

atoms

RLD

(

RLD

)

in

f

,

dom

F

FCD

im

F

v

f

.

dom

F

RLD

im

G

=

F

RLD

f

G

0

F

0

j

F

0

2

atoms

RLD

(

dom

F

RLD

im

F

)

; G

0

2

atoms

RLD

(

im

F

RLD

im

G

)

g v

F

RLD

G

0

F

0

j

F

0

2

atoms

RLD

(

Src

F

;

Dst

F

)

; G

0

2

atoms

RLD

(

Src

G

;

Dst

G

)

;

F

0

v

(

RLD

)

in

f ; G

0

v

(

RLD

)

in

g

=

F

RLD

f

G

0

F

0

j

F

0

2

atoms

RLD

(

RLD

)

in

f ; G

0

2

atoms

RLD

(

RLD

)

in

g

g

= (

RLD

)

in

g

(

RLD

)

in

f

.

Thus

(

RLD

)

in

g

(

RLD

)

in

f

w

F

RLD

f

dom

F

RLD

im

G

j

F

2

atoms

RLD

(

RLD

)

in

f ; G

2

atoms

RLD

(

RLD

)

in

g

g

But

(

RLD

)

in

g

(

RLD

)

in

f

v

F

RLD

f

(

dom

G

RLD

im

G

)

(

dom

F

RLD

im

F

)

j

F

2

atoms

RLD

(

RLD

)

in

f ; G

2

atoms

RLD

(

RLD

)

in

g

g

.

Thus

(

RLD

)

in

g

(

RLD

)

in

f

=

F

RLD

f

dom

F

RLD

im

G

j

F

2

atoms

RLD

(

RLD

)

in

f ; G

2

atoms

RLD

(

RLD

)

in

g

g

=

F

RLD

dom

F

RLD

im

G

j

F

2

atoms

RLD

(

Src

f

;

Dst

f

)

; G

2

atoms

RLD

(

Dst

f

;

Dst

g

)

;

dom

F

FCD

im

F

v

f ;

dom

G

FCD

im

G

v

g

.

But

(

RLD

)

in

(

g

f

) =

G

RLD

f

a

RLD

c

j

a

2

F

(

Src

f

)

; b

2

F

(

Dst

f

)

; c

2

F

(

Dst

g

)

; a

FCD

b

2

atoms

FCD

f ;

b

FCD

c

2

atoms

FCD

g

g

:

Now it becomes obvious that

(

RLD

)

in

g

(

RLD

)

in

f

= (

RLD

)

in

(

g

f

)

.

8.3 Complete reloids

Theorem 26.

(

FCD

)

and

(

RLD

)

out

form mutually inverse bijections between complete reloids and

complete funcoids.

Proof.

Consider the bijection

F

x

2

Src

f

(

f

x

RLD

h

f

if

x

g

)

7!

F

x

2

Src

f

(

f

x

FCD

h

f

if

x

g

)

from complete reloids into complete funcoids, where

f

ranges the set of complete

funcoids. But this bijection is exactly

(

FCD

):

Compl

RLD

(

A

;

B

)

!

Compl

FCD

(

A

;

B

)

because

(

FCD

)

F

x

2

Src

f

(

f

x

RLD

h

f

if

x

g

) =

F

x

2

Src

f

(

FCD

)(

f

x

RLD

h

f

if

x

g

) =

F

x

2

Src

f

(

f

x

FCD

h

f

if

x

g

)

. Thus we have proved that

(

FCD

):

Compl

RLD

(

A

;

B

)

!

Compl

FCD

(

A

;

B

)

is a bijection.

It remains to prove that

(

RLD

)

out

g

=

F

x

2

Src

f

(

f

x

RLD

h

g

if

x

g

)

for every complete funcoid

g

(because

g

=

F

x

2

Src

f

(

f

x

FCD

h

g

if

x

g

)

).

Really,

(

RLD

)

out

g

w

F

x

2

Src

f

(

f

x

RLD

h

g

if

x

g

)

.

It remains to prove that

F

x

2

Src

f

(

f

x

RLD

h

g

if

x

g

)

w

(

RLD

)

out

g

.

Let

L

2

up

F

x

2

Src

f

(

f

x

RLD

h

g

if

x

g

)

. We will prove

L

2

up

(

RLD

)

out

g

.

6

Section 8