arbitrary transformations such that τ1◦τ2 is a transformation. Let  f3 = f1◦ f2, R3 = R1◦ R2 and τ3 = τ1◦τ2 = (cid:3) f3, R3(cid:4). If there are 
two sets M1, M2 ⊆ 2V 1·D1 of disjunctive landmarks and two bijections g1 : A1 → A2 and g2 : A2 → A3 such that both τ1 and τ2 are 
DLBS transformations, then there is a set M3 ⊆ 2V 1·D1 of disjunctive landmarks and a bijection g3 : A1 → A3 such that τ3 is DLBS.
Proof. We must prove that there is a set M3 of landmarks and a bijection  g3 : A1 → A3 such that τ3 is an DLBS transfor-
mation from F1 to F3. Choose  M3 = M1 ∪ M2 and  g3 = g1◦ g2, which is a bijection. We must prove that conditions (1–5) 
in Deﬁnition 40 hold. The proofs for (2) and (5) are like those for ABS.
(1) We know that V 2 = V 1 ∪ V M1,  D2 = D1 ∪ D M , since τ1 is DLBS, and that V 3 = V 2 ∪ V M2,  D3 = D2 ∪ D M , since also 
τ2 is DLBS. It follows that V 1 ∪ V M3 = V 1 ∪ V M1 ∪ V M2 = V 2 ∪ V M2 = V 3.
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen