Ramos, Marcus V M, et al. “Formalization of the Pumping Lemma for Context-Free Languages”. Journal of Formalized Reasoning, vol. 9, no. 2, Jan. 2016, pp. 53-68, doi:10.6092/issn.1972-5787/5595.