+ Proving completeness is probably not hard, but it could be a lot
+ of work. We have seen above that to prove completeness, we must
+ show that the normal set of our graph representation is a subset
+ of the intended normal set.
+
+ However, it is hard to systematically generate or reason about the
+ normal set, since it is defined as any nodes to which no
+ transformation applies. To determine this set, each transformation
+ must be considered and when a transformation is added, the entire
+ set should be re-evaluated. This means it is hard to show that
+ each node in the normal set is also in the intended normal set.
+ Reasoning about our intended normal set is easier, since we know
+ how to generate it from its definition. \refdef{intended normal
+ form definition}.
+
+ Fortunately, we can also prove the complement (which is
+ equivalent, since $A \subseteq B \Leftrightarrow \overline{B}
+ \subseteq \overline{A}$): Show that the set of nodes not in
+ intended normal form is a subset of the set of nodes not in normal
+ form. In other words, show that for every expression that is not
+ in intended normal form, that there is at least one transformation
+ that applies to it (since that means it is not in normal form
+ either and since $A \subseteq C \Leftrightarrow \forall x (x \in A
+ \rightarrow x \in C)$).
+
+ By systematically reviewing the entire Core language definition
+ along with the intended normal form definition (both of which have
+ a similar structure), it should be possible to identify all
+ possible (sets of) core expressions that are not in intended
+ normal form and identify a transformation that applies to it.
+
+ This approach is especially useful for proving completeness of our
+ system, since if expressions exist to which none of the
+ transformations apply (\ie if the system is not yet complete), it
+ is immediately clear which expressions these are and adding
+ (or modifying) transformations to fix this should be relatively
+ easy.
+
+ As observed above, applying this approach is a lot of work, since
+ we need to check every (set of) transformation(s) separately.