Page Comparison

This is for 

...

The algorithm is (men ~ patterns, women ~ terms):

    while ∃ free man m who still has a woman w to propose to {
       w = first woman on m’s list to whom m has not yet proposed
       if w is free
         (m, w) become engaged
       else some pair (m', w) already exists
         if w prefers m to m'
            m' becomes free
           (m, w) become engaged 
         else
           (m', w) remain engaged

This assumes that there are M patterns and N terms and that M = N. 
If M < N, there will not be a match unless there is a wildcard or a remainder (see their sections below) and we should short-circuit unless there is one.

...

The above match will though be successful, as one would expect. This is because, before we reach spatial matching phase, all the match target terms are (and patterns) are fully substituted. In place of each free variable that was defined in the target term's scope, there's now a concrete term.