- Suppose M2 |= succ(F). Then M1 |= succ(τ (F)). Since M1 is a model of **Succ**τ (A),
M1 satisfies the above axiom about succ(τ (F)). Therefore M1 **satisfies the following**
formula:

$init(\tau(\varphi_{1}))\vee\cdots\lor init(\tau(\varphi_{n}))\vee$  $init(\tau(F))\wedge\neg[init(\tau(\phi_{1}))\vee\cdots\lor init(\tau(\phi_{m}))\vee$  $succ(\tau(\phi_{1}^{\prime}))\vee\cdots\lor succ(\tau(\phi_{k}^{\prime}))]$.  
Since the above formula does not mention any complex fluents and has no quantifiers, M2 **satisfies the corresponding formula:**

$init(\varphi_{1})\vee\cdots\lor init(\varphi_{n})\vee$  $init(F)\wedge\neg[init(\phi_{1})\vee\cdots\lor init(\phi_{m})\vee succ(\phi_{1}^{\prime})\vee\cdots\lor succ(\phi_{k}^{\prime})]$,
which is the right side of the equivalence of the pseudo-successor state axiom for succ(F) in **Succ**A.

- Now suppose M2 satisfies (19). We'll show that M1 **satisfies the right side of (18),**
thus M1 |= succ(τ (F)) so M2 |= succ(F**). There are two cases:**
- M2 **satisfies the following formula:**

$\downarrow$  . 
$$i n i t(\varphi_{1})\vee\cdots\lor i n i t(\varphi_{n}).$$
$\left(20\right)^3$
init(ϕ1) ∨ · · · ∨ init(ϕn). **(20)**
In this case, since the above formula does not mention any complex fluents and has no quantifier, M1 **satisfies the following corresponding formula:**

$$i n i t(\tau(\varphi_{1}))\lor\cdot\cdot\lor i n i t(\tau(\varphi_{n})).$$
init(τ (ϕ1)) ∨ · · · ∨ init(τ (ϕn)). **(21)**
Thus M1 **satisfies the right side of (18).**
- M2 **does not satisfy (20) but satisfies the following formula:**
init(F) ∧ ¬[init(φ1) ∨ · · · ∨ init(φm) ∨ **succ**(φ
′
1) ∨ · · · ∨ **succ**(φ
′
k)].

Thus M1 **satisfies the following formula:**

init(τ (F)) ∧ ¬[init(τ (φ1)) ∨ · · · ∨ init(τ (φm)) ∨ succ(τ (φ ′ 1)) ∨ · · · ∨ succ(τ (φ ′ k))].
So to show that the right side of the equivalence of (18) is satisfied by M1**, we**
need to show that M1 |= ¬succ(φ). Recall that φ **is a disjunction such that each**
disjunct α must correspond to a domain rule of the form Causes(α, ¬τ (F**)), and**
that α is of the form α1 ∧ G such that α1 **does not mention fluents, and** G is a fluent atom that mentions an object that does not occur in τ (A**). Note that**
init(α) ⊃ ¬init(τ (F)) is an axiom in Succτ (A), which is satisfied by M1**. Thus**
M1 |= ¬init(α). This means that either α1 or init(G) is false in M1**. If** α1 is false, then succ(α) is false since succ(α1) is the same as α1**. Suppose that**
init(G) is false in M1**. Notice that since there are no positive domain rules, and**