background image

Really,

dom

M

(

dom

z

) =

{

(

i

;

x

)

|

i

dom

(

dom

z

)

, x

dom

z

i

}

=

{

(

i

;

x

)

|

i

dom

z, x

dom

z

i

}

=

a

z

and dom uncurry

(

z

) =

`

i

X

z

i

=

`

z

.

4.3 Finite example

If

F

is a finite family (indexed by a natural number dom

F

) of anchored finitary relations, then by

definition GR

Q

(

ord

)

F

=

{

J

a

0

,

0

;

 

;

a

0

,

arity

F

0

1

;

 

;

a

dom

F

1

,

0

;

 

;

a

dom

F

1

,

arity

F

dom

F

1

1

K

|

J

a

0

,

0

;

 

;

a

0

,

arity

F

0

1

K

GR

F

0

 

J

a

dom

F

1

,

arity

F

dom

F

1

1

K

GR

F

dom

F

1

}

and

arity

Y

(

ord

)

F

=

arity

F

0

+

 

+

arity

F

dom

F

1

.

The above formula can be shortened to

GR

Y

(

ord

)

F

=

concat

z

|

z

Y

(

GR

F

)

 

.

4.4 The definition

Definition 16.

The anchored relation (which I call

ordinated product

)

Q

(

ord

)

F

is defined by the

formulas:

arity

Y

(

ord

)

F

=

X

(

arity

F

);

GR

Y

(

ord

)

F

=

concat

z

|

z

Y

(

GR

F

)

 

.

Theorem 17.

Q

(

ord

)

F

is a properly defined anchored relation.

Proof.

dom concat

z

=

P

i

dom

F

dom

z

i

=

P

i

dom

F

arity

F

i

=

P

(

arity

F

)

.

4.5 Definition with composition for every multiplier

q

(

F

)

i

=

def

(

curry

(

L

(

arity

F

)))

i

.

Theorem 18.

GR

Q

(

ord

)

F

=

L

P

(

arity

F

)

| ∀

i

dom

F

:

L

q

(

F

)

i

GR

F

i

 

.

Proof.

GR

Q

(

ord

)

F

=

{

concat

z

|

z

Q

(

GR

F

)

}

;

GR

Q

(

ord

)

F

=

uncurry

(

z

)

(

L

(

arity

F

))

1

|

z

Q

i

dom

F

arity

F

i

,

i

dom

F

:

z

(

i

)

GR

F

i

 

;

Let

L

=

uncurry

(

z

)

. Then

z

=

curry

(

L

)

.

GR

Q

(

ord

)

F

=

L

(

L

(

arity

F

))

1

|

curry

(

L

)

Q

i

dom

F

arity

F

i

,

i

dom

F

:

curry

(

L

)

i

GR

F

i

 

;

GR

Q

(

ord

)

F

=

n

L

(

L

(

arity

F

))

1

|

L

`

i

dom

F

arity

F

i

,

i

dom

F

:

curry

(

L

)

i

GR

F

i

o

;

GR

Q

(

ord

)

F

=

L

P

(

arity

F

)

| ∀

i

dom

F

:

curry

(

L

L

(

arity

F

))

i

GR

F

i

 

;

(

curry

(

L

L

(

arity

F

))

i

)

x

=

L

((

curry

(

L

(

arity

F

))

i

)

x

) =

L

(

q

(

F

)

i

x

) = (

L

q

(

F

)

i

)

x

;

curry

(

L

L

(

arity

F

))

i

=

L

q

(

F

)

i

;

GR

Q

(

ord

)

F

=

L

P

(

arity

F

)

| ∀

i

dom

F

:

L

q

(

F

)

i

GR

F

i

 

.

Corollary 19.

GR

Q

(

ord

)

F

=

L

(

S

im

(

GR

F

))

P

(

arity

F

)

| ∀

i

dom

F

:

L

q

(

F

)

i

GR

F

i

 

.

Corollary 20.

GR

Q

(

ord

)

F

is small if

F

is small.

4

Section 4