Weak orthogonality implies confluence:
the higher-order case


In this paper we prove confluence for weakly orthogonal Higher-Order Rewriting Systems. This generalises all the known `confluence by orthogonality' results.