Undecidable properties of flat term rewrite systems

Reachability, joinability and confluence properties are known to be undecidable for flat term rewrite systems (TRS). We give shorter and conceptually simpler proofs of these results. We also prove undecidability of weak normalization and unique normalization properties for flat TRS. The first author was supported by Spanish Ministry of Education and Science by the FORMALISM project (TIN2007-66523) and by the LOGICTOOLS-2 project (TIN2007-68093-C02-01). The second author was supported by Spanish Ministry of Education and Science by the FORMALISM project (TIN2007-66523).