specification, we will have that for action stack(a, c), succ(on(a, c)) and ¬succ(on(a, e**)) are** true. Furthermore, by changing the mapping for 3, we see that for any x **that is different**
from a and c (the mapping needs to be one-to-one), ¬succ(on(a, x**)) is true.**
Obviously, this is to be expected of the blocks world. We now proceed to show that for some general classes of domain descriptions, we can do this as well. We first make precise the mapping from one type specification to another.

Definition 2 **Given two type specifications** O:

```
Domain(p1, Dp1
           
           ), · · ·, Domain(pk, Dpk
                           ),

```

and O′:
$$D o m a i n(p_{1},D_{p_{1}}^{\prime}),\cdots,D o m a i n(p_{k},D_{p_{k}}^{\prime}),$$
an embedding from O to O′is a one-to-one mapping τ from Dp1**∪· · ·∪**Dpk to D′p1

∪· · ·∪D′pk such that for any 1 ≤ i ≤ k**, and any** a ∈ Dpi
, f(a) ∈ D′pi
.

Clearly, if there is an embedding of O to O′, then for each type p**, the size of the domain**
for p in O′ must be at least the size of the domain for p in O**. Given such an embedding**
τ , any expression β **(actions, propositions, formulas) in an action domain description** D
with O as its type specification can be mapped to τ (β) in the language of D′**: one simply**
replaces each object a in β by τ (a), where D′ differs from D only in that it uses O′ **as its**
type specification. Notice that only objects (those in the domain of some type) are to be replaced, not constants that may occur in the effect axioms or **domain rules.**
Definition 3 An action domain description belongs to simple-I **class if it does not mention**
any function of positive arity, does not mention any complex **fluents except in complex fluent**
definitions, and satisfies the following conditions:

1. If Precond(A, φA) is an action precondition definition, then φA **has the form**
(∀x, p)...(∀y,q)W, where W **is a fluent formula that does not have any quantifiers.**
2. If Effect(A, ϕ, F) or Effect(A, ϕ, ¬F) is an action effect axiom, then ϕ **does not have**
any quantifiers, and the variables in ϕ and F are among those in A**. That is, one** cannot have something like
Effect(explodeAt(x), nearby(y, x)**, dead**(y)).

3. If Causes(ϕ, F) or Causes(ϕ, ¬F) is a domain rule, then ϕ does not have any quantifiers, and all the variables in ϕ **must be in** F.

Theorem 2 Let D be a simple-I action domain description, and A **an action instance in**
D. Let D′be just like D except for the type specification. Then for any formula ψ **that**
does not mention any complex fluent and has no quantifiers, and any embedding τ **from**
the type specification of D to that of D′, we have that if InitA ∪ SuccA |= ψ in D**. then**
Initτ (A) ∪ **Succ**τ (A)|= τ (ψ) in D′.