Database Reference
In-Depth Information
1.
p
k
→
φ(p
k
)
(note that it can be the empty set
∅
as well);
2.
nil
→∅
, and
a
→∅
for each
a
∈
Act
;
3.
a.t
→{
(a,a
i
.t
i
)
|
(a
i
,t
i
)
∈
φ
#
(t)
}
if
|
φ
#
(t)
|≥
1
;∅
otherwise;
→
1
≤
i
≤
n
φ
#
(t
i
)
.
Let us show that this mapping satisfies the equation
φ
#
=
n
(t
1
,...,t
n
)
4.
F(μ
X
)
◦
λ
T
P
X
◦
T
P
(φ)
,
i.e., the diagram
1. In the case
t
=
p
k
∈
X
,
F(μ
X
)
◦
λ
T
P
X
◦
T
P
(φ)(p
k
)
=
F(μ
X
)
◦
λ
T
P
X
(φ(p
k
))
where
S
S
be-
cause in
S
all terms are fattened (they are the variables). While
φ
#
(p
k
)
=
φ(p
k
)
∈
F(
T
P
X)
, so that
F(μ
X
)
◦
λ
T
P
X
(S)
=
F(μ
X
)(S)
=
=
S
.
2. For any
a
φ(p
k
)
=
∈
Act
(or
nil
),
◦
λ
T
P
X
◦
T
P
(φ)(a)
=
◦
=
∅
=∅=
F(μ
X
)
F(μ
X
)
λ
T
P
X
(a)
F(μ
X
)(
)
φ
#
(a).
Let us show that this equation is valid by structural induction on the length of
terms (considered by a number of operators contained in a term), and assume
that it holds for the terms
t,t
1
,...,t
n
,
n
1, of the length
m
. Then we consider
a term with the length greater than
m
, that is, one of the following cases:
2.1. The case of a term
a.t
. Then
≥
◦
λ
T
P
X
◦
T
P
(φ)(a.t)
F(μ
X
)
λ
T
P
X
a.
T
P
(φ)(t)
=
F(μ
X
)
◦
F(μ
X
)
(a,a
k
.t
k
)
λ
T
P
X
T
P
(φ)(t)
=
|
(a
k
,t
k
)
∈
=
a,a
k
.F(μ
X
)(t
k
)
|
T
P
X
T
P
(φ)(t)
(a
k
,t
k
)
∈
λ
=
a,a
k
.t
k
|
a
k
,t
k
∈
F(μ
X
)
λ
T
P
X
T
P
(φ)(t)
=
a,a
k
.t
k
|
a
k
,t
k
∈
φ
#
(t)
=
φ
#
(a.t).
If
T
P
(φ)(t)
=∅
(for example,
t
is a constant or a variable
p
k
such that
), we obtain analogous result.
2.2. The case of a term
φ(p
k
)
=∅
n
(t
1
,...,t
n
)
. Then
T
P
X
◦
T
P
(φ)
n
(t
1
,...,t
n
)
F(μ
X
)
◦
λ
T
P
X
n
T
P
(φ)(t
1
),...,
T
P
(φ)(t
n
)
=
F(μ
X
)
◦
λ
