background image

2.

Q

(

D

)

F

is a staroid if every

F

i

is a staroid.

3.

Q

(

D

)

F

is a completary staroid if every

F

i

is a completary staroid.

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

Y

(

D

)

F

!

|

arity

Q

(

D

)

F

\{

q

}

that is

L

(

i

;

j

)

form

Q

(

D

)

F

(

i

;

j

)

for every

(

i

;

j

)

arity

Q

(

D

)

F

\ {

q

}

, that is

L

(

i

;

j

)

(

form

F

i

)

j

. We have

X

form

Q

(

D

)

F

(

i

;

j

)

X

(

form

F

i

)

j

. So

 

val

Y

(

D

)

F

!

(

i

;

j

)

L

=

(

X

(

form

F

i

)

j

|

L

∪ {

((

i

;

j

);

X

)

} ∈

GR

Y

(

D

)

F

)

 

val

Y

(

D

)

F

!

(

i

;

j

)

L

=

X

(

form

F

i

)

j

| ∃

z

Y

(

GR

F

):

L

∪ {

((

i

;

j

);

X

)

}

=

uncurry

z

 

 

val

Y

(

D

)

F

!

(

i

;

j

)

L

=

n

X

(

form

F

i

)

j

| ∃

z

(

GR

F

)

|

arity

Q

(

D

)

F

\{

(

i

;

j

)

}

, v

GR

F

i

:

(

L

=

uncurry

z

v

j

=

X

)

o

val

Q

(

D

)

F

(

i

;

j

)

L

=

n

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

o

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

Y

(

D

)

F

!

(

i

;

j

)

L

=

{

X

(

form

F

i

)

j

| ∃

v

GR

F

i

:

v

j

=

X

}

.

Thus

 

val

Y

(

D

)

F

!

(

i

;

j

)

L

=

{

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

}

:

K

∪ {

(

j

;

X

)

} ∈

GR

F

i

}

=

{

X

(

form

F

i

)

j

| ∃

K

(

form

F

i

)

|

(

arity

F

i

)

\{

j

}

:

X

(

val

F

j

)

K

}

.

Thus

A

B

val

Q

(

D

)

F

(

i

;

j

)

L

⇔ ∃

K

(

form

F

i

)

|

(

arity

F

i

)

\{

j

}

:

A

B

(

val

F

j

)

K

K

(

form

F

i

)

|

(

arity

F

i

)

\{

j

}

: (

A

(

val

F

j

)

B

(

val

F

j

))

⇔ ∃

K

(

form

F

i

)

|

(

arity

F

i

)

\{

j

}

:

A

(

val

F

j

)

K

∨ ∃

K

(

form

F

i

)

|

(

arity

F

i

)

\{

j

}

:

A

(

val

F

j

)

K

A

val

Q

(

D

)

F

(

i

;

j

)

L

B

val

Q

(

D

)

F

(

i

;

j

)

L

. Least element

0

is not in

val

Q

(

D

)

F

(

i

;

j

)

L

because

K

∪ {

(

j

;

0)

}

GR

F

i

.

2. From the lemma.

3. We need to prove

L

0

L

1

GR

Y

(

D

)

F

⇔ ∃

c

∈ {

0

,

1

}

arity

Q

(

D

)

F

:

 

λi

arity

Y

(

D

)

F

:

L

c

(

i

)

i

!

GR

Y

(

D

)

F

14

Section 9