background image

3.7. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

51

3.7.4.4.

The definition.

Definition

296

.

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

297

.

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

).

3.7.4.5.

Definition

with

composition

for

every

multiplier.

q

(

F

)

i

def

=

(curry(

L

(arity

F

)))

i

.

Proposition

298

.

Q

(ord)

F

=

L

f

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

f

arity

Fi

,

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

f

arity

Fi

,

i

dom

F

:curry(

L

)

i

GR

F

i

;

GR

Q

(ord)

F

=

(

L

(

L

(arity

f

)

)

1

L

f

`

i

dom

F

arity

Fi

,

i

dom

F

:curry(

L

)

i

GR

F

i

)

;

GR

Q

(ord)

F

=

L

f

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

;

Q

(ord)

F

=

L

f

P

(arity

F

)

i

dom

F

:

L

q

(

F

)

i

GR

F

i

.

Corollary

299

.

Q

(ord)

F

=

(

L

(

S

im(GR

F

)

)

P

(arity

F

)

i

dom

F

:

L

q

(

F

)

i

GR

F

i

)

.

Corollary

300

.

Q

(ord)

F

is small if

F

is small.

3.7.4.6.

Definition with shifting arguments.

Let

F

0

i

=

n

L

Pr

1

|

{

i

arity

Fi

L

GR

F

i

o

.

Proposition

301

.

F

0

i

=

n

L

Pr

1

|

{

i

f

L

GR

F

i

o

.

Proof.

If

L

GR

F

i

then dom

L

= arity

F

i

. Thus

L

Pr

1

|

{

i

arity

F

i

=

L

Pr

1

|

{

i

dom

L

=

L

Pr

1

|

{

i

f

.

Proposition

302

.

F

0

i

is an (

{

i

} ×

arity

F

i

)-ary relation.

Proof.

We need to prove that dom

L

Pr

1

|

{

i

arity

F

i

=

{

i

} ×

arity

F

i

for

L

GR

F

i

, but that’s obvious.