Andreka et al. (1995) obtained a large number of completeness results for discrete linear-time temporal logics. One of them is left open: the completeness of the logic of `initially' and `next', for which a deductive system is proposed. This simple logic is of practical importance, since the proof of program invariants only require these modalities. We show here that the conjectured medium completeness of this system indeed holds; further, we show that deciding this entailment is PSPACE-complete, while deciding validity is only coNP-complete.