Information Technology Reference
In-Depth Information
-
N
−
M
≥
2
m
+1
−i
,
-
∀
j
≤
i
:
p
j
≤
M
or
p
j
≥
N
.
We do this inductively as follows. We let
M
:= 1 and
N
:=
n
,for
i
=0.Since
n
=2
m
+2
, clearly the conditions above hold. Assume that
M
and
N
are defined
for
i
so that the conditions above hold; we define
M
and
N
for
i
+1 as follows:
1. If
p
i
+1
−
p
i
+1
,thenwelet
M
:= max
and
N
:=
N
.
M
≤
N
−
{
M,p
i
+1
}
p
i
+1
,thenwelet
M
:=
M
and
N
:= min
2. If
p
i
+1
−
M>N
−
{
N,p
i
+1
}
.
Note that in both cases
∀j ≤ i
+1:
p
j
≤ M
or
p
j
≥ N
,and
N
−
M
N
−
M
≥
2
m
+1
−
(
i
+1)
.
≥
2
Proceeding in this way we conclude that at the final stage
m
we have
N
−
M
≥
2
with no
p
1
,...,p
m
stricly in between
M
and
N
. We then choose mid(
)asany
number in ]
M,N
[. Note that defining mid in this way we are able to meet the
conditions 1-3.
After this we define a mapping
h
:
{x
1
,...,x
m
}
A
p
→
{x
1
,...,x
m
}
A
. For an assign-
ment
s
:
{
x
1
,...,x
m
}→
A
, the assignment
h
(
s
):
{
x
1
,...,x
m
}→
A
is defined
as follows:
h
(
s
)(
x
i
)=
s
(
x
i
)
if ro (
s
(
x
i
))
<
mid(row(
s
(
x
)))
,
ʵ
ⓦ
s
(
x
i
) frow
s
(
x
i
))
>
mid(row(
s
(
x
)))
,
where
x
:= (
x
1
,...,x
m
). For a team
Z
of
A
with Dom(
Z
)=
{
x
1
,...,x
m
}
,we
now let
swap(
Z
):=
{
h
(
s
)
|
s
∈
Z
}
,
and define, for each
Y
ↆ
X
,
Y
∗
:= swap(auto(
Y
))
.
With
X
∗
now defined, we next show that (7) holds. Without loss of generality
we may assume that if a constant symbol
b
j
(or
c
j
) appears in an atomic subfor-
mula
ʱ
of
ʸ
,then
ʱ
is of the form
x
i
=
b
j
(or
x
i
=
c
j
)where
x
i
is an existentially
quantified variable of the quantifier prefix. Hence and by (6), it now suces to
show that for all
Y
ↆ
X
and all quantifier-free
ˈ
∈
FO(
ↆ
)(
k
−
1-inc)[
˄
] with
the above restriction for constants,
(
A
,
b
,
c
)
|
=
Y
ˈ
⃒
(
A
,
b
,ʵ
(
c
))
|
=
Y
∗
ˈ.
This can be done by induction on the complexity of the quantifier-free
ˈ
.Since
Y
∗
∪
Z
∗
=(
Y
Z
)
∗
,for
Y,Z
X
, it suces to consider only the case where
ˈ
is an atomic or negated atomic formula. For this, assume that (
∪
ↆ
A
,
b
,
c
)
|
=
Y
ˈ
;
we show that
(
A
,
b
,ʵ
(
c
))
|
=
Y
∗
ˈ.
(8)
Now
ˈ
is either of the form
x
i
=
b
j
,
x
i
=
c
j
,
x
i
=
x
j
,
¬
x
i
=
x
j
,
E
(
x
i
,x
j
),
¬
E
(
x
i
,x
j
)or
y
ↆ
z
where
b
j
,c
j
are constant symbols and
y
,
z
are sequences of
variables from
{
x
1
,...,x
m
}
with
|
y
|
=
|
z
|≤
k
−
1.
