possible translation improvement
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?
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information