3. Suppose Defined(F, ψ**) is an instantiation of a complex fluent definition such that**
F ≡ ψ is in Init. For it to be in Init, Fluent(F) must be true. Thus M **must satisfy**
H(F, S) ≡ H(ψ, S). By the construction of MS,A, it satisfies init(F) ≡ init(**ψ, S**).

4. Suppose Precond(A, φA) is the precondition axiom for A. Since M satisfies Poss(**A, S**)
and Action(A) (because A **is one of the action instances generated by the procedure),**
thus M satisfies H(φA, S). So MS,A satisfies **init**(φA).
We now show that MS,A is a model of Succ**, that is, for each primitive fluent atom** F
generated by the procedure in Step 1, the pseudo-successor state axiom (1) holds. Referring to the notation in the axiom, we need to show that M **satisfies the following formula:**

H(F, do(A, S)) ≡ H(ϕ1, S) ∨ · · · ∨ H(ϕn, S) ∨ H(ϕ ′ 1, do(A, S))∨ · · · ∨ H(ϕ ′ l, do(A, S))∨ H(F, S) ∧ ¬[H(φ1, S) ∨ · · · ∨ H(φm, S) ∨
$\left(\frac{1}{2}\right)\left(\frac{1}{2}\right)$ 7. 
$\mathbf{v}$ 2. 
H(φ
′
1, do(A, S))**∨ · · · ∨** H(φ
′
k, do(A, S))].
First of all, instantiating the generic successor state axiom (5) over A and S**, we get:**
Poss(A, S) ⊃ H(F, do(**A, S**)) ≡
[Caused(F, true, do(A, S))∨ H(F, S) ∧ ¬Caused(F, false, do(A, S))].

Since M is a model of Poss(A, S**), we have**
H(F, do(A, S)) ≡ (8)

$\sim J/\sim$
$$[C a u s e d(F,t r u e,d o(A,S))\lor H(F,S)\land\neg C a u s e d(F,f a l s e,d o(A,S))].$$
Now consider the circumscription of Caused in T **with all other predicates fixed. Notice that**
all axioms about Caused in T have the form W ⊃ Caused(x, y, z), where W **is a formula** that does not mention Caused. Therefore the circumscription of Caused **is equivalent to** the predicate completion of Caused. Suppose F is f(t**), and that all of the axioms about** Caused(f(x), v, s) in T **are as follows:**
W1 ⊃ Caused(f(x), v, s), · · ·, Wi ⊃ Caused(f(x)**, v, s**).

Because of the unique names axioms about fluents, the result of predicate completion on Caused **will entail:**
Caused(f(x), v, s) ≡ W1 **∨ · · · ∨** Wi.

Now W1,...,Wi are from action effect axioms and domain rules about f**. By the way that**
(1) is generated, and noting that Action(A), Fluent(F), and Poss(A, S**) are true, one can** see that when the above equivalence is instantiated by replacing t for x, true for v**, and** S
for s**, we will get**
Caused(F, true, do(A, S)) ≡ H(ϕ1, S) ∨ · · · ∨ H(ϕn, S) ∨
H(ϕ
′
1, do(A, S))**∨ · · · ∨** H(ϕ
′
l, do(**A, S**)).