RRAb: Identical to RRAa, except that we prove condition (3b) instead of (3a).
(3b) We know that {(cid:3)s, t(cid:4) | t ∈ R1(s)} = {(cid:3)s, t(cid:4) | t ∈ R2(s)}, since  τ1 is RRAb, and that {(cid:3)s, t(cid:4) | t ∈ R2(s)} = {(cid:3)s, t(cid:4) | t ∈
R3(s)}, since τ2 is RRAb. It follows that {(cid:3)s, t(cid:4) | t ∈ R1(s)} = {(cid:3)s, t(cid:4) | t ∈ R3(s)}.
GIDL: Suppose both τ1 and τ2 are GIDL transformations. Then there are two corresponding bijections  g1 : A1 → A2 and 
g2 : A2 → A3 such that Deﬁnition 38 is satisﬁed for both τ1 and τ2. We must prove that there is a bijection  g3 : A1 → A3
such that τ3 is a GIDL transformation from F1 to F3. Choose g3 = g1◦g2, which is a bijection. We must prove that conditions 
(1)–(5) in Deﬁnition 38 hold. The proofs for (1), (2) and (5) are identical to ABS and the proof for (4) is identical to RRA.
=1 = post(g2(g1(a))) and  analo-
(3) For  all  a ∈ A1,  it  holds  that  post(g3(a)) = post(a)
gously for pre(g3(a)). (cid:2)

=1 = post(g1(a))
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen