M. V. M. Ramos, J. C. B. Almeida, N. Moreira, and R. J. G. B. de Queiroz, “Formalization of the pumping lemma for context-free languages”, JFR, vol. 9, no. 2, pp. 53–68, Jan. 2016.