possible translation improvement
Currently a U b
is translated as b ∨ (a ∧ X[a U b] ∧ P(b))
.
@max's idea: if a
is purely universal, we can translate a U b
as b ∨ (a ∧ X[F(b)] ∧ P(b))
.
Of course there is a dual rule for R
and pure eventuality.
Can this improve the translation?