LTL simplifications suggestions
Consider the formula (F(p & r) | G(Fq & F!q)) & FG(q) & G(r)
. Currently, it is not simplified.
Because we have G(r)
at the top level, we could replace all the other r
by 1
.
It would also be nice to find a way to kill G(Fq & F!q)
because of FG(q)
.