Definition 5.4.3.  Let V ⊆ Var such that V is finite,  ⊆ Rewr(TV), L, R ∈ TV. We define:
L →R  :⇔  (L → R) ∈  or {false if R = (z) (z ∈ V)[{false if L = (y) (y ∈ V)∀ v ∈ Fresh(V) : Mv →Nv if L = λy. My (My ∈ TV ∪ {y} for each y ∈ Fresh(V), [∀ a, b ∈ Fresh(V) : Ma[a:= b] = Mb])false if L = MN (M, N ∈ TV)] if R = λz. Nz (Nz ∈ TV ∪ {z} for each z ∈ Fresh(V), [∀ a, b ∈ Fresh(V) : Na[a:= b] = Nb])[{false if L = (y) (y ∈ V)false if L = λy. My (My ∈ TV ∪ {y} for each y ∈ Fresh(V), [∀ a, b ∈ Fresh(V) : Ma[a:= b] = Mb])[M →O and N = P] or [M = O and N →P] if L = MN (M, N ∈ TV)] if R = OP (O, P ∈ TV)
L ↛R  :⇔  not [L →R]
Remarks.

This definition checks whether a rewrite rule matches a pair of terms. It considers both the pair itself as well as all subterms. Structural induction on both sides makes the definition a bit complicated.