I'm brand new to LTL and working on becoming better with LTL formulae. I've got two examples where I am unsure whether my LTL formula is correct. I'm given the sentences, and my assumption is that $l$ is true: 1. $l$ is always false after $m$ LTL Translation: $G(m \to G(\neg l))$ i.e on all paths m implies on all paths not p 2. $l$ is false between $m$ and $n$ LTL Translation: $G((m \land Fn) \to \neg l \space Un)$ i.e on all paths m and finally n, implies not p until n Are these right? Thanks for the help!