Ramos, M. V. M.; Almeida, J. C. B.; Moreira, N.; de Queiroz, R. J. G. B. Formalization of the Pumping Lemma for Context-Free Languages. JFR 2016, 9, 53-68.