¹⁹However, this sharing—i.e., treating the term as a dag instead of as a tree—is not done in a maximal way, so that all subterms that can be shared are; instead, term sharing is itself introduced incrementally by equational simplification, since Maude analyzes righthand sides of equations to identify its shared subterms. As explained by Eker in [50], in the presence of operator evaluation strategies (Section 4.4.7) term sharing has to be done carefully. Furthermore, when rewriting is performed with a rule in a system module (see Chapter 5), rather than with an equation, Maude will incrementally unshare those parts of the subject term needed to ensure that all possible rewrite with rules are considered. This is because rules in system modules need not be confluent. As a consequence, two identical subterms could be rewritten in totally different ways; but this of course would be prevented if they were to be shared.