Z. Zombori and P. Szeredi, “Loop elimination, a sound optimisation technique for PTTP related theorem proving”, Acta Cybern, vol. 20, no. 3, pp. 441-458, Jan. 2012.