 3.8. INFINITE ASSOCIATIVITY AND ORDINATED PRODUCT

46

3.8.4.7.

Associativity of ordinated product.

Let

f

be an ordinal variadic func-

tion.

Let

S

be an ordinal indexed family of functions of ordinal indexed families of

functions each taking an ordinal number of arguments in a set

X

.

I call

f

infinite associative

when

1

.

f

(

f

S

) =

f

(concat

S

) for every

S

;

2

.

f

(

J

x

K

) =

x

for

x

X

.

Infinite associativity implies associativity.

Proposition

260

.

Let

f

be an infinitely associative function taking an ordinal

number of arguments in a set

X

. Define

x ? y

=

f

J

x

;

y

K

for

x, y

X

. Then the

binary operation

?

is associative.

Proof.

Let

x, y, z

X

. Then (

x ? y

)

? z

=

f

J

f

J

x

;

y

K

;

z

K

=

f

(

f

J

x

;

y

K

;

f

J

z

K

) =

f

J

x

;

y

;

z

K

. Similarly

x ?

(

y ? z

) =

f

J

x

;

y

;

z

K

. So (

x ? y

)

? z

=

x ?

(

y ? z

).

Concatenation is associative.

First we will prove some lemmas.

Let

a

and

b

be functions on a poset. Let

a

b

iff there exist an order isomor-

phism

f

such that

a

=

b

f

. Evidently

is an equivalence relation.

Obvious

261

.

concat

a

= concat

b

uncurry(

a

)

uncurry(

b

) for every ordi-

nal indexed families

a

and

b

of functions taking an ordinal number of arguments.

Thank to the above, we can reduce properties of concat to properties of uncurry.

Lemma

262

.

a

b

uncurry

a

uncurry

b

for every ordinal indexed families

a

and

b

of functions taking an ordinal number of arguments.

Proof.

There exist an order isomorphism

f

such that

a

=

b

f

.

uncurry(

a

)(

x

;

y

) = (

ax

)

y

= (

bf x

)

y

= uncurry(

b

)(

f x

;

y

) = uncurry(

b

)

g

(

x

;

y

)

where

g

(

x

;

y

) = (

f x

;

y

).

g

is an order isomorphism because

g

(

x

0

;

y

0

)

g

(

x

1

;

y

1

)

(

x

0

;

y

0

)

(

x

1

;

y

1

).

(Injectivity and surjectivity are obvious.)

Lemma

263

.

Let

a

i

b

i

for every

i

. Then uncurry

a

uncurry

b

for every

ordinal indexed families

a

and

b

of ordinal indexed families of functions taking an

ordinal number of arguments.

Proof.

Let

a

i

=

b

i

f

i

where

f

i

is an order isomorphism for every

i

.

uncurry(

a

)(

i

;

y

) =

a

i

y

=

b

i

f

i

y

= uncurry(

b

)(

i

;

f

i

y

) = uncurry(

b

)

g

(

i

;

y

) =

(uncurry(

b

)

g

)(

i

;

y

) where

g

(

i

;

y

) = (

i

;

f

i

y

).

g

is an order isomorphism because

g

(

i

;

y

0

)

g

(

i

;

y

1

)

f

i

y

0

f

i

y

1

y

0

y

1

and

i

0

> i

1

g

(

i

;

y

0

)

> g

(

i

;

y

1

). (Injectivity and surjectivity are obvious.)

Let now

S

be an ordinal indexed family of ordinal indexed families of functions

taking an ordinal number of arguments.

Lemma

264

.

uncurry(uncurry

S

)

uncurry(uncurry

S

).

Proof.

uncurry

S

=

λi

S

: uncurry(

S

i

);

(uncurry(uncurry

S

))((

i

;

x

);

y

) = (uncurry

S

i

)(

x

;

y

) = (

S

i

x

)

y

;

(uncurry(uncurry

S

))((

i

;

x

);

y

) = ((uncurry

S

)(

i

;

x

))

y

= (

S

i

x

)

y

.

Thus (uncurry(uncurry

S

))((

i

;

x

);

y

) = (uncurry(uncurry

S

))((

i

;

x

);

y

) and

thus evidently uncurry(uncurry

S

)

uncurry(uncurry

S

).

Theorem

265

.

concat is an infinitely associative function.