It is suﬃcient to combine conditional admissibility with the weakest form of completeness to get full admissibility, as 

the following theorem demonstrates.
Theorem 49. M↑P1↑AC↓ ⇒ A↓
Proof. Let G1 = (cid:3)S1, E1(cid:4) and G2 = (cid:3)S2, E2(cid:4) be arbitrary STGs and let τ = (cid:3) f , R, w1, w2(cid:4) be an arbitrary M↑P1↑AC↓ trans-
formation. Let  s, s
) holds trivially, so suppose 
(cid:10).  Since  τ is  M↑ and  P1↑ there  are  states 
c1(s, s
t0, . . . , tn ∈ S2 such  that  ti = f (si) for  all  i (0 ≤ i ≤ n)  and  ti ∈ R2(ti−1) for  all  i (1 ≤ i ≤ n).  Hence,  tn ∈ R2(t0),  i.e. 

) < ∞.  Then  there  is  a  path  s0, . . . , sn in  G1,  where  s0 = s and  sn = s

(cid:10) be two arbitrary states in  S1. If c1(s, s

) = ∞, then c2( f (s), f (s

)) ≤ c1(s, s

(cid:10)

(cid:10)

(cid:10)

(cid:10)

26

C. Bäckström and P. Jonsson

Artiﬁcial Intelligence 302 (2022) 103608

G2:

1

f

11

12

G1:

2

21

22

3

31

32

G2:

1

f

11

12

G1:

2

21

22

3

31

32
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen