BEGIN-INLINE-LATEX
\correctnessthm{}
END-INLINE-LATEX
Proof:
If b ∈ matches[| G, p, t |], then (•, b) ∈ M[| G, p, t |],
which by the soundness lemma below, implies G ⊢ t : p | b.
If G ⊢ t : p | b, then (•, b) ∈ M[| G, p, t |] by the completeness lemmma below;
consequently b ∈ matches[| G, p, t |].

Lemma (Soundness):
For all G, p, t, b, C, and t',
1. (•, b) ∈ M[| G, p, t |] implies G ⊢ t : p | b, and
2. ((C, t'), b) ∈ M[| G, p, t |] implies G ⊢ t = C[t'] : p | b.
Proof: By induction on the M derivation.

Case: hole (and t = hole)
  Given:
    M[| G, hole, hole |] = {((hole, hole), ∅), (•, ∅)}
  By the hole decomposition rule,
    G ⊢ hole = hole[hole] : hole | ∅
  By the hole matching rule,
    G ⊢ hole : hole | ∅

Case: hole (and t ≠ hole)
  Given: 
    M[| G, hole, t |] = {((hole, t), ∅)}
  By the hole decomposition rule, 
    G ⊢ t = hole[t] : hole | ∅

Case: atom
  Given:
    M[| G, a, a |] = {(•, ∅)}, and
  By the atom matching rule,
    G ⊢ a : a | ∅

Case: cons
  Let (d, b) ∈ M[| G, (cons p_1 p_2), (k t_1 t_2) |], i.e.,
    1. (d_1, b_1) ∈ M[| G, p_1, t_1 |],
    2. (d_2, b_2) ∈ M[| G, p_2, t_2 |],
    3. b_1 ⊔ b_2 = b, and
    4. d ∈ select[| t_1, d_1, t_2, d_2 |].

  Subcase: d_1 = d_2 = •
    Then d = • by the first `select' clause, requiring
      G ⊢ (k t_1 t_2) : (cons p_1 p_2) : b,
    which holds by the cons matching rule, since:
      1. G ⊢ t_1 : p_1 | b_1 by induction,
      2. G ⊢ t_2 : p_2 | b_2 by induction, and
      3. b_1 ⊔ b_2 = b by hypothesis.

  Subcase: d_1 = • and d_2 = (C, t_2')
    Then d = ((right t_1 C), t_2') by the third `select' clause, requiring
      G ⊢ (k t_1 t_2) = (right t_1 C)[t_2'] : (:cons p_1 p_2) : b,
    which holds by the cons-right decomposition rule, since:
      1. G ⊢ t_1 : p_1 | b_1 by induction,
      2. G ⊢ t_2 = C[t_2'] : p_2 | b_2 by induction, and
      3. b_1 ⊔ b_2 = b by hypothesis.

  Subcase: d_1 = (C, t_1') and d_2 = •
    Similarly, using the second `select' rule and the cons-left 
    decomposition rule. 

  Subcase: d_1 = (C_1, t_1') and d_2 = (C_2, t_2')
    Impossible since select[| t_1, (C_1, t_1'), t_2, (C_2, t_2') |] = ∅

Case: in-hole
  Let (d, b) ∈ M[| G, (in-hole p_1 p_2), t |], i.e.,
    1. ((C_1, t_1), b_1) ∈ M[| G, p_1, t |],
    2. (d_2, b_2) ∈ M[| G, p_2, t_1 |],
    3. b_1 ⊔ b_2 = b, and
    4. d = combine[| C_1, d_2 |].

  Subcase: d_2 = •
    combine[| C_1, • |] = •, requiring:
      G ⊢ t : (in-hole p_1 p_2) | b,
    which holds by the in-hole matching rule, since:
      1. G ⊢ t = C_1[t_1] : p_1 | b_1 by induction,
      2. G ⊢ t_1 : p_2 | b_2 by induction, and
      3. b_1 ⊔ b_2 = b by hypothesis.

  Subcase: d_2 = (C_2, t_2)
    combine[| C_1, (C_2, t_2) |] = (C_1 ++ C_2, t_2), requiring:
      G ⊢ t = (C_1 ++ C_2)[t_2] : (in-hole p_1 p_2) | b,
    which holds by the in-hole decomposition rule, since:
      1. G ⊢ t = C_1[t_1] : p_1 | b_1 by induction,
      2. G ⊢ t_1 = C_2[t_2] : p_2 | b_2 by induction, and
      3. b_1 ⊔ b_2 = b by hypothesis.

Case: name 
  Let (d, b') ∈ M[| G, (name x p), t |], i.e.,
    1. (d, b) ∈ M[| G, p, t |],
    2. {(x, named[| d, t |])} ⊔ b = b'.

  Subcase: d = •
    By the name matching rule, G ⊢ t : (name x p) | b' since:
      1. G ⊢ t : p | b, by induction, and
      2. {(x, t)} ⊔ b = b', since {(x, named[| d, t |])} ⊔ b = b' 
      and named[| •, t |] = t by the first `named' clause.
 
  Subcase: d = (C, t')
    By the name decomposition rule, G ⊢ t = C[t'] : (name x p) | b' since:
      1. G ⊢ t = C[t'] : p | b, by induction, and
      2. {(x, C)} ⊔ b = b', since {(x, named[| (C, t'), t |])} ⊔ b = b' 
      and named[| (C, t'), t |] = C by the second `named' clause.

Case: nt 
  Let (d, ∅) ∈ M[| G, (nt n), t |], i.e.,
    1. p ∈ G(n), and
    2. (d, b) ∈ M[| G, p, t |].

  Subcase: d = •
    By the nt matching rule, G ⊢ t : (nt n) | ∅ since:
      1. p ∈ G(n) by hypotheis, and
      2. G ⊢ t : p | b by induction.

  Subcase: d = (C, t')
    Similarly by the nt decomposition rule.

Case: the "else" clause
  Impossible since M[| G, p, t |] = ∅

Lemma (Completeness): 
For all G, p, t, b, C, and t', if G is not left recursive, then
1. G ⊢ t : p | b implies (•, b) ∈ M[| G, p, t |], and
2. G ⊢ t = C[t'] : p | b implies ((C, t'), b) ∈ M[| G, p, t |].
Proof: By (mutual) induction on the matching/decomposition derivation.

Case: atom matching
  Given: G ⊢ a : a | ∅
  (•, ∅) ∈ M[| G, a, a |] by M's atom case

Case: hole matching
  Given: G ⊢ hole : hole | ∅
  (•, ∅) ∈ M[| G, hole, hole |] by M's hole case for the term hole

Case: name matching
  Given: 
    1. G ⊢ t : (name x p) | b', 
    2. G ⊢ t : p | b, and 
    3. b ⊔ {(x, t)} = b'
  By M's name clause, (•, b) ∈ M[| G, (name x p), t |] since:
    1. (•, b) ∈ M[| G, p, t |] by induction.
    2. named[| •, t |] = t by definition.
    3. b ⊔ {(x, t)} = b' by hypothesis.

Case: nt matching
  Given:
    1. G ⊢ t : (:nt n) | ∅,
    2. p ∈ G(n), and
    3. G ⊢ t : p | b. 
  By M's nt clause, (•, ∅) ∈ M[| G, (nt n), t |] since:
    1. p ∈ G(n) by hypothesis.
    2. (•, b) ∈ M[| G, p, t |] by induction.
    3. M[| G, p', t |] terminates for n's other productions p' by the 
    termination lemma below

Case: cons matching
  Given:
    1. G ⊢ (k t_1 t_2) : (cons p_1 p_2) | b,
    2. G ⊢ t_1 : p_1 | b_1,
    3. G ⊢ t_2 : p_2 | b_2, and
    4. b_1 ⊔ b_2 = b.
  By M's cons clause, (•, b) ∈ M[| G, (cons p_1 p_2), (k t_1 t_2) |] since:
    1. (•, b_1) ∈ M[| G, p_1, t_1 |] by induction,
    2. (•, b_2) ∈ M[| G, p_2, t_2 |] by induction,
    3. b_1 ⊔ b_2 = b by hypothesis, and
    4. • ∈ select[| t_1, •, t_2, • |] by its first clause

Case: in-hole matching
  Given:
    1. G ⊢ t : (in-hole p_1 p_2) | b,
    2. G ⊢ t = C[t'] : p_1 | b_1,
    3. G ⊢ t' : p_2 | b_2, and
    4. b_1 ⊔ b_2 = b.
  By M's in-hole clause, (•, b) ∈ M[| G, (in_hole p_1 p_2), t |] since:
    1. ((C, t'), b_1) ∈ M[| G, p_1, t |] by induction,
    2. (•, b_2) ∈ M[| G, p_2, t' |] by induction,
    3. b_1 ⊔ b_2 = b by hypothesis, and
    4. • = combine[| C, • |] by its first clause.

Case: hole decomposition
  Given: G ⊢ t = hole[t] : :hole | ∅
  Subcase: t = hole
    By the M clause that applies when the pattern and term are hole,
      ((hole, hole), ∅) ∈ M[| G, hole, t |]
  Subcase: t ≠ :hole
    By the M clause that applies when the pattern is hole but the term is not,
      ((hole, t), ∅) ∈ M[| G, hole, t |]

Case: cons-left decomposition
  Given:
    1. G ⊢ (k t_1 t_2) = (left C t_2)[t_1'] : (cons p_1 p_2) | b,
    2. G ⊢ t_1 = C[t_1'] : p_1 | b_1,
    3. G ⊢ t_2 : p_2 | b_2, and
    4. b_1 ⊔ b_2 = b'.
  By M's cons clause,
    (((left C t_2), t_1'), b) ∈ M[| G, (cons p_1 p_2), (k t_1 t_2) |] 
  since:
    1. ((C, t_1'), b_1) ∈ M[| G, p_1, t_1 |] by induction,
    2. (•, b_2) ∈ M[| G, p_2, t_2 |] by induction,
    3. b_1 ⊔ b_2 = b' by hypothesis, and
    4. ((left C t_2), t_1') ∈ select[| t_1, (C, t_1'), t_2, • |]
       by its second clause.

Case: cons-right decomposition
  Similar to cons-left composition

Case: nt decomposition
  Given:
    1. G ⊢ t = C[t'] : (nt n) | ∅,
    2. p ∈ G(n), and
    3. G ⊢ t = C[t'] : p | b.
  By M's nt clause, ((C, t'), ∅) ∈ M[| G, (nt n), t |] since:
    1. p ∈ G(n) by hypothesis, 
    2. ((C, t'), b) ∈ M[| G, p, t |] by induction, and
    3. M[| G, p', t |] terminates for n's other productions p' by the 
    termination lemma below.

Case: in-hole decomposition
  Given:
    1. G ⊢ t = (C_1 ++ C_2)[t_2] : (in-hole p_1 p_2) | b,
    2. G ⊢ t = C_1[t_1] : p_1 | b_1,
    3. G ⊢ t_1 = C_2[t_2] : p_2 | b_2, and
    4. b_1 ⊔ b_2 = b'.
  By M's in-hole clause, 
    ((C_1 ++ C_2, t_2), b) ∈ M[| G, (in-hole p_1 p_2), t |] 
  since:
    1. ((C_1, t_1), b_1) ∈ M[| G, p_1, t |] by induction,
    2. ((C_2, t_2), b_2) ∈ M[| G, p_2, t_1 |] by induction,
    3. b_1 ⊔ b_2 = b' by hypothesis, and
    4. combine[| C_1, (C_2, t_2) |] = C_1 ++ C_2 by its second clause.

Case: name decomposition
  Given:
    1. G ⊢ t = C[t'] : (name x p) | b',
    2. G ⊢ t = C[t'] : p | b, and
    3. b ⊔ {(x, C)} = b'.
  By M's name clause, ((C, t'), b') ∈ M[| G, (name x p), t |] since:
    1. ((C, t'), b) ∈ M[| G, p, t |] by induction,
    2. named[| (C, t'), t |] = C by its second clause,
    3. b ⊔ {(x, C)} = b' by hypothesis.

Lemma (Termination): 
For all G, p, and t, M[| G, p, t |] terminates if G is not left recursive.
Proof:
Patterns and terms can be assigned sizes such that each recursive call of M
supplies smaller arguments than the ones it received. In particular,
we interpret the size |t| of a term t as:

|a| = 1
|(cons t t')| = 1 + |t| + |t'|
|hole| = 1
|(left C t)| = 1 + |C| + |t|
|(right t C)| = 1 + |t| + |C|

and the size |p| of a pattern p as:

|a| = 0
|(name x p)| = 1 + |p|
|(nt n)| = 1 + max({|p| | p ∈ G(n)|})|
|(in-hole p p')| = 1 + max({|p|, |p'|})|
|(cons p p')| = 0
|hole| = 0

This assignment of pattern sizes is possible because the graph induced
by ->_G has no cycles. The assignment can be constructed bottom-up, by 
beginning with non-terminals n_0 for which n_0 -/>_G^* n for any 
non-terminal n, proceeding with the non-terminals n_1 for which 
n_1 ->_G^* n_0 for only the previous n_0, and so on.

We interpret the overall size of the combined arguments
lexicographically, treating the term argument as more significant than
the pattern argument.

Each recursive call supplies either a smaller term or a term of the
same size and a smaller pattern.

Case: within `cons' clause
Each call supplies a strictly smaller term.

Case: within `in-hole' clause
The first call supplies the same term and a pattern whose size is at most
|(in-hole p_c p_h)| - 1.

The second call supplies a term that's no larger than the input term
(by the non-increasing subterms lemma below) and a pattern whose size is 
at most |(in-hole p_c p_h)| - 1.

Case: within `name' clause
The call supplies the same term and strips the `name' from the
pattern, decreasing its size by 1.

Case: within `nt' clause
Each call supplies the same term and a pattern whose size is at most
|(nt n)| - 1.

Lemma (Non-increasing subterms)
If ((C, t'), b) ∈ M[| G, p, t |], then |t'| ≤ |t|.
Proof: By induction on the M derivation.

Case: hole (and t = hole)
t = t'

Case: hole (and t ≠ hole)
t = t'

Case: atom
Impossible, since the result is not a decomposition.

Case: cons
By the definition of `select', there are two possibilities that make
the result a decomposition:
  Subcase: d_l = (C_l, t_l') and d_r = •.

    Then select[| t_l, (C_l, t_l'), t_r, • |] = {((left C_l t_r), t_l')}
    |t_l'| ≤ |t_l| by induction
           < |(cons t_l t_r)|

  Subcase: d_l = • and d_r = (C_r, t_r').

    By a similar argument.

Case: in-hole
By the definition of `combine', there is one possibility that makes
the result a decomposition:

d_h = ((C_h, t_h), b_h) ∈ M[| G, p_h, t_c |].
Then combine[| C, (C_h, t_h) |] = (C ++ C_h, t_h).
|t_h| ≤ |t_c| and |t_c| ≤ |t|, both by induction.

Case: name
Suppose d = ((C, t'), b) ∈ M[| G, p, t |].
By induction, |t'| ≤ |t|.

Case: M-nt
Similar to the `name' case. 