missed LTL simplification
For any φ we have that F(Fp0 & (p0 | φ))
is equivalent to F(p0)
. Can we generalize and recognize this pattern?
This is based on a mail by @ythierry.
For any φ we have that F(Fp0 & (p0 | φ))
is equivalent to F(p0)
. Can we generalize and recognize this pattern?
This is based on a mail by @ythierry.