International Conference on Rewriting Techniques and Applications
Springer LNCS 4098, pages 166-180, August 2006.
\z.(let !y be M in let !x be L in N) > let !x be L in \z.(let !y be M in N)where z is *free* in M. Without this rule, the system is not locally confluent/coherent modulo the equivalence relation \sim^*. In particular, Lemma 1 in the paper fails. For example, consider
M = \z.(let !x be L in let !y be M in N) M1 = \z.(let !y be M in let !x be L in N) M2 = let !x be L in \z.(let !y be M in N)where x is not free in M, and z is free in M. Then M \sim M1 and M > M2 (via the rule com3), but in general M1 and M2 are not joinable modulo \sim^*, due to the side condition on com3.
After adding this rule, all the results in the paper are indeed valid.