is the identity function.

We then show that the remaining properties from Deﬁnition 9 do not generally hold.

Theorem 43. 
(1) ABS (cid:3) M↑,
(4) VDA (cid:3) M↓,
(7) GIDL (cid:3) C↑,

(2) ABS (cid:3) M↓,
(5) RRAa (cid:3) R↑,
(8) GIDL (cid:3) C↓,

(3) VP (cid:3) M↓,
(6) RRAb (cid:3) R↑,
(9) DLBS (cid:3) M↑

Proof. (1–6,9) Examples 31, 33, 35, 37 and 41 constitute counterexamples.
(7–8) Consider  the  transformation  τ in  Example 39.  We  have  R(a, g(a)) and (cid:3){u, v},{u, v}, a(cid:4) ∈ E1,  but  there  is  no  (cid:2)
such  that (cid:3){u, v},{u, v}, (cid:2)(cid:4) ∈ E2 Hence,  τ is  not  C↑.  We  also  have (cid:3){u, v},{u, v}, g(a)(cid:4) ∈ E2 but  there  is  no  (cid:2) such  that 
(cid:3){u, v},{u, v}, (cid:2)(cid:4) ∈ E1. Hence, τ is not C↓ either. (cid:2)

The following reﬁnement properties can be immediately deduced from the preceding theorems. They are summarised in 

column 3 of Table 1.
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen