We study higher-order rewrite systems (HRSs) which extend term rewriti
ng to lambda-terms. HRSs can describe computations over terms with bou
nd variables. We show that rewriting with HRSs is closely related to u
ndirected equational reasoning. We define pattern rewrite systems (PRS
s) as a special case of HRSs and extend three confluence results from
term rewriting to PRSs: the critical pair lemma by Knuth and Bendix, c
onfluence of rewriting module equations a la Huet, and confluence of o
rthogonal PRSs.