LTL simplification: GFp0 U Gp0 should be FGp0
% ltlfilt --simplify -f 'GFp0 U Gp0'
GFp0 U Gp0We should have GFa U b rewritten as F b whenever b implies GFa.
% ltlfilt --simplify -f 'GFp0 U Gp0'
GFp0 U Gp0We should have GFa U b rewritten as F b whenever b implies GFa.