background image

4.6 Definition with shifting arguments

Let

F

i

=

{

L

Pr

1

|

{

i

arity

F

i

|

L

GR

F

i

}

.

Proposition 21.

F

i

=

{

L

Pr

1

|

{

i

|

L

GR

F

i

}

.

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

.

Proposition 22.

F

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.

Obvious 23.

`

(

arity

F

) =

S

i

dom

F

(

{

i

} ×

arity

F

i

) =

S

i

dom

F

dom

F

i

.

Lemma 24.

P

Q

i

dom

F

F

i

curry

(

S

im

P

)

Q

(

GR

F

)

for a dom

F

indexed family

P

where

P

i

{

i

arity

F

i

for every

i

dom

F

, that is for

P

`

i

dom

F

{

i

arity

F

i

.

Proof.

For every

P

`

i

dom

F

{

i

arity

F

i

we have:

P

Q

i

dom

F

F

i

P

∈ {

z

dom

F

| ∀

i

dom

F

:

z

(

i

)

F

i

} ⇔

P

dom

F

∧ ∀

i

dom

F

:

P

(

i

)

F

i

P

dom

F

∧ ∀

i

dom

F

L

GR

F

i

:

P

i

=

L

(

Pr

1

|

{

i

)

P

dom

F

i

dom

F

L

GR

F

i

:

P

i

{

i

arity

F

i

∧ ∀

x

arity

F

i

:

P

i

(

i

;

x

) =

L x

P

dom

F

i

dom

F

L

GR

F

i

:

P

i

{

i

arity

F

i

curry

(

P

i

)

i

=

L

P

dom

F

∧ ∀

i

dom

F

:

P

i

{

i

arity

F

i

curry

(

P

i

)

GR

F

i

⇔ ∀

i

dom

F

Q

i

(

arity

F

i

)

{

i

}

: (

P

i

=

uncurry

(

Q

i

)

(

Q

i

)

i

arity

F

i

Q

i

i

GR

F

i

)

⇔ ∀

i

dom

F

Q

i

(

arity

F

i

)

{

i

}

P

i

=

uncurry

(

Q

i

)

S

i

dom

F

Q

i

i

GR

F

i

⇔ ∀

i

dom

F

Q

i

(

arity

F

i

)

{

i

}

P

i

=

uncurry

(

Q

i

)

S

i

dom

F

Q

i

Q

(

GR

F

)

i

dom

F

:

S

i

dom

F

curry

(

P

i

)

Q

(

GR

F

)

curry

S

i

dom

F

P

i

Q

(

GR

F

)

curry

(

S

im

P

)

Q

(

GR

F

)

.

Lemma 25.

n

curry

(

f

)

L

(

arity

F

)

|

f

GR

Q

(

ord

)

F

o

=

Q

(

GR

F

)

.

Proof.

First GR

Q

(

ord

)

F

=

{

uncurry

(

z

)

(

L

(

dom

z

))

1

|

z

Q

(

GR

F

)

}

, that is

n

f

|

f

GR

Q

(

ord

)

F

o

=

{

uncurry

(

z

)

(

L

(

arity

F

))

1

|

z

Q

(

GR

F

)

}

.

Since

L

(

arity

F

)

is a bijection, we have

n

f

L

(

arity

F

)

|

f

GR

Q

(

ord

)

F

o

=

{

uncurry

(

z

)

|

z

Q

(

GR

F

)

}

what is equivalent to

n

curry

(

f

)

L

(

arity

F

)

|

f

GR

Q

(

ord

)

F

o

=

{

z

|

z

Q

(

GR

F

)

}

that is

n

curry

(

f

)

L

(

arity

F

)

|

f

GR

Q

(

ord

)

F

o

=

Q

(

GR

F

)

.

Lemma 26.

S

im

P

|

P

`

i

dom

F

{

i

arity

F

i

curry

(

S

im

P

)

Q

(

GR

F

)

 

=

n

L

|

L

`

i

X

arity

F

i

curry

(

L

)

Q

(

GR

F

)

o

.

Proof.

Let

L

n

L

|

L

`

i

X

arity

F

i

curry

(

L

)

Q

(

GR

F

)

o

. Then

L

`

i

X

arity

F

i

and

curry

(

L

)

Q

(

GR

F

)

.

Let

P

=

λi

dom

F

:

L

|

{

i

arity

F

i

. Then

P

`

i

dom

F

{

i

arity

F

i

and

S

im

P

=

L

. So

L

S

im

P

|

P

`

i

dom

F

{

i

arity

F

i

curry

(

S

im

P

)

Q

(

GR

F

)

 

.

Let now

L

S

im

P

|

P

`

i

dom

F

{

i

arity

F

i

curry

(

S

im

P

)

Q

(

GR

F

)

 

. Then there

exists

P

`

i

dom

F

{

i

arity

F

i

such that

L

=

S

im

P

and curry

(

L

)

Q

(

GR

F

)

. Evidently

L

`

i

X

arity

F

i

. So

L

S

im

P

|

P

`

i

dom

F

{

i

arity

F

i

curry

(

S

im

P

)

Q

(

GR

F

)

 

.

Ordinated product

5