Information Technology Reference
In-Depth Information
Foreveryothervariable
v
in
Q
∃
we obtain
v
Φ
ϕ
=
v
(
Q
∃
ρ ◦ ϕ
)
vρϕ
=
vϕ
=
=
vϕ.
Case
flex-flex with different heads, i.e.,
U
is
Q.u
y
=
v
z
∧C
.Let
w
be an enu-
λ
y
.u
w
,λ
z
.u
w
meration of the variables both in
y
and in
z
.Then
ρ
=[
u, v
:=
],
Q
is
∃u
inserted, and
U
=
Q
Cρ
Q
with
∃u, ∃v
removed and
.
Φ
ϕ
U
-solution, i.e., assume that
Cρϕ
1.
is well-defined: Let
be a
holds.
ρ ◦ ϕ
)
We must show that
ϕ
:= (
Q
∃
is a
U
-solution.
uρϕ
)
For
u
y
=
v
z
: We need to show (
uϕ
)
y
=(
vϕ
)
z
.But(
uϕ
)
y
=(
y
=
u
ϕ
)
u
ϕ
)
u
ϕ
)
(
λ
y
.
(
w
)
y
=(
w
, and similarly (
vϕ
)
z
=(
w
.
u
is a new variable,
For (
r
=
s
)
∈ C
: We need to show (
r
=
s
)
ϕ
. But since
ρ ◦ ϕ
coincide on all variables free in
ρϕ
by
ϕ
and
r
=
s
, and we have (
r
=
s
)
assumption.
2. Definition of
→U
-solutions. Let a
Φ
:
U
-solutions
Q
-substitution
ϕ
be
givensuchthat(
u
y
=
v
z
)
ϕ
and
Cϕ
. Define
u
(
Φϕ
):=
λ
w
.
(
uϕ
)
w
0
w.l.o.g.;
0
arbitrary
v
(
Φϕ
):=
λ
w
.
(
vϕ
)
0
w
u
,v
,u
w
(
Φϕ
):=
wϕ
otherwise, i.e.,
w
=
flexible.
Since by assumption (
uϕ
)
y
=(
vϕ
)
z
, the normal forms of both (
uϕ
)
y
and (
vϕ
)
z
ϕ
:=
can only contain the common variables
w
from
y
,
z
free. Hence, for
Φϕ
,
uρϕ
=
vρϕ
=
uϕ
by the argument in the previous case, and similarly
vϕ
.Since
rϕ
=
sϕ
((
r
=
s
)
∈ C
arbitrary) by assumption, and
ρ
only affects
u
and
v
,
rρϕ
sρϕ
, as required.
Φ
(
we obtain
=
Φϕ
)=
ϕ
can now be proved as in the
previous case.
Case
flex-rigid,
U
is
Q.u
y
=
t ∧ C
.
Subcase
occurrence check:
t
contains (a critical subterm with head)
u
.Then
clearly there is no
Q
-substitution
ϕ
such that (
uϕ
)
y
=
tϕ
.
Subcase
pruning: Here
t
contains a subterm
v
w
1
z
w
2
with
∃v
in
Q
,and
z
λ
w
1
,z,
w
2
.v
w
1
w
2
],
Q
is
∃v
,
free in
t
.Then
ρ
=[
v
:=
Q
with
∃v
replaced by
U
=
Q
.u
y
and
=
tρ ∧ Cρ
.
Φ
is well-defined: Let
ϕ
be a
U
-solution, i.e., (
uϕ
)
tρϕ
,and
rρϕ
=
1.
y
=
sρϕ
for (
ρ ◦ ϕ
)
r
=
s
)
∈ C
. We must show that
ϕ
:= (
Q
∃
is a
U
-solution.
tρϕ
.But
For
u
y
=
t
: We need to show (
uϕ
)
y
=
uρϕ
)
(
uϕ
)
y
=(
y
uϕ
)
=(
y
since
ρ
does not touch
u
tρϕ
=
by assumption.
v
For (
r
=
s
)
∈ C
: We need to show (
r
=
s
)
ϕ
. But since
is a new variable,
ρ ◦ ϕ
)
ρ ◦ ϕ
coincide on all variables free in
ϕ
=(
Q
∃
and
r
=
s
, and the claim
ρϕ
.
follows from (
r
=
s
)
Search WWH ::
Custom Search