Infer definedness of sub-terms

[ttuegel]

In the implication checking document, I mentioned that:

If we checked ⌈t(X)⌉ ∧ P(X) [during the implication check], then we could infer that the configuration is defined, allowing us to do subsequent rewriting without generating extra definedness conditions. The efficiency of this method merits investigation.

We will add an internal node to TermLike called Defined. Defined will have a single child. As a pattern, it will take all its synthetic attributes from the child, except that the Defined node is always a defined pattern. During the implication check, after we check that the configuration's term is defined, we will push a Defined node down onto the term. We will push the Defined node down onto subterms as appropriate; for example,

#defined(\and(φ₁, φ₂)) = #defined(\and(#defined(φ₁), #defined(φ₂)))
#defined(σ(φ₁, ...)) = #defined(σ(#defined(φ₁), ...))  // remove the outer-most #defined if σ is a functional symbol

We will need to add unification and matching cases which strip the virtual #defined node from the pattern.

The \ceil simplifier already takes advantage of the definedness pattern attribute. The backend will now check definedness of the term in advance and avoid re-checking terms that are already known to be defined.