background image

21.8. ON PRODUCTS OF STAROIDS

333

Proof.

1

Let

q

arity

Q

(

D

)

F

that is

q

= (

i, j

) where

i

dom

F

,

j

arity

F

i

; let

L

Y

form

(

D

)

Y

F

|

arity

Q

(

D

)

F

\{

q

}

that is

L

(

i

0

,j

0

)

form

Q

(

D

)

F

(

i

0

,j

0

)

for every (

i

0

, j

0

)

arity

Q

(

D

)

F

\ {

q

}

, that

is

L

(

i

0

,j

0

)

(form

F

i

0

)

j

0

. We have

X

form

Q

(

D

)

F

(

i,j

)

X

(form

F

i

)

j

. So

val

(

D

)

Y

F

(

i,j

)

L

=

(

X

(form

F

i

)

j

L

∪ {

((

i, j

)

, X

)

} ∈

GR

Q

(

D

)

F

)

=

X

(form

F

i

)

j

z

Q

(GR

F

) :

L

∪ {

((

i, j

)

, X

)

}

= uncurry

z

=

X

(form

F

i

)

j

z

Q

(GR

F

)

|

arity

Q

(

D

)

F

\{

(

i,j

)

}

, v

GR

F

i

: (

L

= uncurry

z

v

j

=

X

)

=

X

(form

F

i

)

j

z

Q

(GR

F

)

|

arity

Q

(

D

)

F

\{

(

i,j

)

}

:

L

= uncurry

z

∧ ∃

v

GR

F

i

:

v

j

=

X

.

If

z

Q

(GR

F

)

|

arity

Q

(

D

)

F

\{

(

i,j

)

}

:

L

= uncurry

z

is false then

val

Q

(

D

)

F

(

i,j

)

L

=

is a free star. We can assume it is true. So

val

(

D

)

Y

F

(

i,j

)

L

=

X

(form

F

i

)

j

v

GR

F

i

:

v

j

=

X

=

X

(form

F

i

)

j

K

(form

F

i

)

|

(arity

F

i

)

\{

j

}

:

K

∪ {

(

j, X

)

} ∈

GR

F

i

=

X

(form

F

i

)

j

K

(form

F

i

)

|

(arity

F

i

)

\{

j

}

:

X

(val

F

i

)

j

K

.

Thus

A

t

B

val

(

D

)

Y

F

(

i,j

)

L

K

(form

F

i

)

|

(arity

F

i

)

\{

j

}

:

A

t

B

(val

F

i

)

j

K

K

(form

F

i

)

|

(arity

F

i

)

\{

j

}

: (

A

(val

F

i

)

j

K

B

(val

F

i

)

j

K

)

K

(form

F

i

)

|

(arity

F

i

)

\{

j

}

:

A

(val

F

i

)

j

K

K

(form

F

i

)

|

(arity

F

i

)

\{

j

}

:

B

(val

F

i

)

j

K

A

val

(

D

)

Y

F

(

i,j

)

L

B

val

(

D

)

Y

F

(

i,j

)

L.

Least element

is not in

val

Q

(

D

)

F

(

i,j

)

L

because

K

∪ {

(

j,

)

}

/

GR

F

i

.