background image

17.9. ON PRODUCTS OF STAROIDS

251

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

)

j

. 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

.

2

From the lemma.