@article{oai:repository.nii.ac.jp:00001267, author = {龍田, 真 and Tatsuta, Makoto}, journal = {NIIテクニカル・レポート, NII Technical Report}, month = {Feb}, note = {This paper formalizes the proof of Lemma A13 given in the paper ``Compositional characterizations of lambda-terms using intersection types'' by M.~Dezani-Ciancaglini et al, so that one can verify it by a theorem prover such as HOL by typing the content of this paper. The proof in the original paper is simplified by reorganizing case analysis. Several properties implicitly used in the original paper are explicitly stated and proved.}, pages = {1--25}, title = {NII Technical Report (NII-2012-002E):Formalization of Lemma for Adjacent Replacement Paths}, year = {2012} }