background image

Proof.

dom concat

z

=

P

i

2

dom

F

dom

z

i

=

P

i

2

dom

F

arity

F

i

=

P

(

arity

F

)

.

3.8.4.5 Denition with composition for every multiplier

q

(

F

)

i

=

def

(

curry

(

L

(

arity

F

)))

i

.

Theorem 3.87.

GR

Q

(

ord

)

F

=

L

2

f

P

(

arity

F

)

j 8

i

2

dom

F

:

L

q

(

F

)

i

2

GR

F

i

 

.

Proof.

GR

Q

(

ord

)

F

=

f

concat

z

j

z

2

Q

(

GR

F

)

g

;

GR

Q

(

ord

)

F

=

uncurry

(

z

)

(

L

(

arity

F

))

¡

1

j

z

2

Q

i

2

dom

F

f

arity

F

i

;

8

i

2

dom

F

:

z

(

i

)

2

GR

F

i

 

.

Let

L

=

uncurry

(

z

)

. Then

z

=

curry

(

L

)

.

GR

Q

(

ord

)

F

=

L

(

L

(

arity

F

))

¡

1

j

curry

(

L

)

2

Q

i

2

dom

F

f

arity

F

i

;

8

i

2

dom

F

:

curry

(

L

)

i

2

GR

F

i

 

;

GR

Q

(

ord

)

F

=

n

L

(

L

(

arity

F

))

¡

1

j

L

2

f

`

i

2

dom

F

arity

F

i

;

8

i

2

dom

F

:

curry

(

L

)

i

2

GR

F

i

o

;

GR

Q

(

ord

)

F

=

L

2

f

P

(

arity

F

)

j 8

i

2

dom

F

:

curry

(

L

L

(

arity

F

))

i

2

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

2

f

P

(

arity

F

)

j 8

i

2

dom

F

:

L

q

(

F

)

i

2

GR

F

i

 

.

Corollary 3.88.

GR

Q

(

ord

)

F

=

L

2

(

S

im

(

GR

F

))

P

(

arity

F

)

j 8

i

2

dom

F

:

L

q

(

F

)

i

2

GR

F

i

 

.

Corollary 3.89.

GR

Q

(

ord

)

F

is small if

F

is small.

3.8.4.6 Denition with shifting arguments

Let

F

i

0

=

f

L

Pr

1

j

f

i

g

arity

F

i

j

L

2

GR

F

i

g

.

Proposition 3.90.

F

i

0

=

f

L

Pr

1

j

f

i

g

f

j

L

2

GR

F

i

g

.

Proof.

If

L

2

GR

F

i

then dom

L

=

arity

F

i

. Thus

L

Pr

1

j

f

i

g

arity

F

i

=

L

Pr

1

j

f

i

g

dom

L

=

L

Pr

1

j

f

i

g

f

:

Proposition 3.91.

F

i

0

is an

(

f

i

arity

F

i

)

-ary relation.

Proof.

We need to prove that dom

(

L

Pr

1

j

f

i

g

arity

F

i

) =

f

i

arity

F

i

for

L

2

GR

F

i

, but that's

obvious.

Obvious 3.92.

`

(

arity

F

) =

S

i

2

dom

F

(

f

i

arity

F

i

) =

S

i

2

dom

F

dom

F

i

0

.

Lemma 3.93.

P

2

Q

i

2

dom

F

F

i

0

,

curry

(

S

im

P

)

2

Q

(

GR

F

)

for a dom

F

indexed family

P

where

P

i

2

f

f

i

g

arity

F

i

for every

i

2

dom

F

, that is for

P

2

`

i

2

dom

F

f

f

i

g

arity

F

i

.

Proof.

For every

P

2

`

i

2

dom

F

f

f

i

g

arity

F

i

we have:

P

2

Q

i

2

dom

F

F

i

0

,

P

2 f

z

2

f

dom

F

j 8

i

2

dom

F

:

z

(

i

)

2

F

i

0

g ,

P

2

f

dom

F

^ 8

i

2

dom

F

:

P

(

i

)

2

F

i

0

,

P

2

f

dom

F

^ 8

i

2

dom

F

9

L

2

GR

F

i

:

P

i

=

L

(

Pr

1

j

f

i

g

f

)

,

P

2

f

dom

F

^

8

i

2

dom

F

9

L

2

GR

F

i

:

¡

P

i

2

f

f

i

g

arity

F

i

^ 8

x

2

arity

F

i

:

P

i

(

i

;

x

) =

L x

,

P

2

f

dom

F

^

8

i

2

dom

F

9

L

2

GR

F

i

:

¡

P

i

2

f

f

i

g

arity

F

i

^

curry

(

P

i

)

i

=

L

,

P

2

f

dom

F

^ 8

i

2

dom

F

:

¡

P

i

2

f

f

i

g

arity

F

i

^

curry

(

P

i

)

i

2

GR

F

i

, 8

i

2

dom

F

9

Q

i

2

(

f

arity

F

i

)

f

i

g

: (

P

i

=

uncurry

(

Q

i

)

^

(

Q

i

)

i

2

f

arity

F

i

^

Q

i

i

2

GR

F

i

)

,8

i

2

dom

F

9

Q

i

2

(

f

arity

F

i

)

f

i

g

¡

P

i

=

uncurry

(

Q

i

)

^

¡ S

i

2

dom

F

Q

i

i

2

GR

F

i

, 8

i

2

dom

F

9

Q

i

2

(

f

arity

F

i

)

f

i

g

¡

P

i

=

uncurry

(

Q

i

)

^

S

i

2

dom

F

Q

i

2

Q

(

GR

F

)

,

8

i

2

dom

F

:

S

i

2

dom

F

curry

(

P

i

)

2

Q

(

GR

F

)

,

curry

¡ S

i

2

dom

F

P

i

2

Q

(

GR

F

)

,

curry

(

S

im

P

)

2

Q

(

GR

F

)

.

46

More on order theory