t1 = s1 (cid:4) post(a). Since  R(a, g(a)) holds by deﬁnition, it follows that τ is R↓. Then also suppose that  R((cid:2), g(a)) holds for 
some  (cid:2).  The  only  possibility  is  that  (cid:2) = a,  so  we  know  that (cid:3)s1, t1, a(cid:4) ∈ E1.  Furthermore,  t1[V C] = (s1 (cid:4) post(a))[V C] =
s1[V C] (cid:4) post(a)[V C] = s2 (cid:4) post(g(a)) = t2, i.e. t1 ∈ f (t2). It follows that τ is C↓.
(3) Assume τ is VDA. Then τ is M↑ since  f (s) = h(s) and h(s) ∈ S2 for s ∈ S1. Before continuing, we ﬁrst note that for 
all s, t ∈ S1 it holds that if s ⊆ t, then h(s) ⊆ h(t), and that h(s (cid:4) t) = h(s) (cid:4) h(t).
Suppose (cid:3)s1, t1, a(cid:4) ∈ E1. Then pre(a) ⊆ s1 must hold, so we get pre(g(a)) = h(pre(a)) ⊆ h(s1). Hence, (cid:3)h(s1), t2, g(a)(cid:4) ∈ E2, 
where t2 = h(s1) (cid:4) post(g(a)). Since also  R(a, g(a)) holds by deﬁnition it follows that  τ is R↑. Then also suppose  R(a, (cid:2))
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen