was chosen arbitrarily.
PL↓ ⇒ P1↓:  Assume  τ is  PL↓.  Let  σ = t0, t1 be  an  arbitrary  path  of  length  1  in  G2.  Then  there  are  s0 ∈ f (t0) and 
s1 ∈ f (t1) such that s1 ∈ R1(s0) since τ is PL↓. It follows that τ is P1↓ since σ was chosen arbitrarily.
A-framework-for-analysing-state-abstraction-metho_2022_Artificial-Intelligen