background image

x

FCD

y

2

atoms

d

FCD

(¡(

A

;

B

)

\

GR

f

)

, 8

K

2

¡(

A

;

B

)

\

GR

f

:

x

FCD

y

2

atoms

K

(

8

K

2

GR

f

:

x

FCD

y

2

atoms

K

,

x

RLD

y

/

f

.

??
It's enough to prove up

¡(

A

;

B

)

(

FCD

)

f

= ¡(

A

;

B

)

\

GR

f

.

Really, up

¡(

A

;

B

)

(

FCD

)

f

=

up

¡(

A

;

B

)

d

FCD

GR

f

K

2

up

¡(

A

;

B

)

d

FCD

GR

f

)

K

w

d

FCD

GR

f

[TODO: To continue this implication we MUST

use that

K

2

¡

(otherwise take thick identity as a counterexample)]

??

Theorem 55.

b

/

Anch

(

A

)

StarComp

(

a

;

f

)

, 8

A

2

GR

a; B

2

GR

b; i

2

n

:

A

i

[

f

i

]

B

i

for anchored

relations

a

and

b

, provided that

Src

f

i

are atomic posets.

Proof.

b

/

Anch

(

A

)

StarComp

(

a

;

f

)

,

9

x

2

Anch

(

A

)

n f?g

: (

x

v

b

^

x

v

StarComp

(

a

;

f

))

,

9

x

2

Anch

(

A

)

n f?g

: (

x

v

b

^ 8

B

2

GR

x

:

B

2

GR StarComp

(

a

;

f

))

,

9

x

2

Anch

(

A

)

n f?g

: (

x

v

b

^ 8

B

2

GR

x

: (

i

2

n

:

h

f

i

¡

1

i

B

i

)

2

GR

a

)

,

remove

?

9

x

2

Anch

(

A

)

n f?g

: (

8

B

2

GR

x

:

B

2

GR

b

^ 8

B

2

GR

x

: (

i

2

n

:

h

f

i

¡

1

i

B

i

)

2

GR

a

)

,

9

x

2

Anch

(

A

)

n f?g 8

B

2

GR

x

: (

B

2

GR

b

^

(

i

2

n

:

h

f

i

¡

1

i

B

i

)

2

GR

a

)

,

??

8

A

2

GR

a; B

2

GR

b; i

2

n

:

A

i

/

h

f

i

¡

1

i

B

i

,

8

A

2

GR

a; B

2

GR

b; i

2

n

:

A

i

[

f

i

]

B

i

:

,

??

9

x

2

Anch

(

A

)

n f?g

: (

8

A

2

GR

x

: (

A

2

GR

a

^

(

i

2

n

:

h

f

i

i

A

i

)

2

GR

b

))

9

x

2

Anch

(

A

)

n f?g

: (

x

v

a

^ 8

A

2

GR

x

: (

i

2

n

:

h

f

i

i

A

i

)

2

GR

b

)

9

x

2

Anch

(

A

)

n f?g

: (

x

v

a

^ 8

A

2

GR

x

:

A

2

GR StarComp

(

b

;

f

y

))

9

x

2

Anch

(

A

)

n f?g

: (

x

v

a

^

x

v

StarComp

(

b

;

f

y

))

,

a

/

Anch

(

A

)

StarComp

(

b

;

f

y

)

16

Section 7