 3.8. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

42

Obvious

241

.

If

z

is a finite family of finitary tuples, it is concatenation of

dom

z

tuples in the usual sense (as it is commonly used in computer science).

Proposition

242

.

If

z

Q

(GR

F

) then concat

z

= uncurry(

z

)

(

L

(arity

F

))

1

.

Proof.

If

z

Q

(GR

F

) then dom

z

(

i

) = dom(GR

F

)

i

= dom

F

i

= arity

F

i

for every

i

dom

F

. Thus dom

z

= arity

F

.

Proposition

243

.

dom concat

z

=

P

i

dom

z

dom

z

i

.

Proof.

Because dom(

L

(dom

z

))

1

=

P

i

dom

f

(dom

z

), it is enough to

prove that

dom uncurry(

z

) = dom

M

(dom

z

)

.

Really,

X

i

dom

f

(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

.

3.8.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

(ord)

Y

=

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

(ord)

Y

F

= arity

F

0

+

. . .

+ arity

F

dom

F

1

.

The above formula can be shortened to

GR

(ord)

Y

F

=

concat

z

z

Q

(GR

F

)

.

3.8.4.4.

The definition.

Definition

244

.

The anchored relation (which I call

ordinated product

)

Q

(ord)

F

is defined by the formulas:

arity

(ord)

Y

F

=

X

(arity

f

);

GR

(ord)

Y

F

=

concat

z

z

Q

(GR

F

)

.

Proposition

245

.

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

).