³As explained in Section 1.2, mathematically this is achieved by a logic inclusion, in which the functional world of equational theories is conservatively embedded in the nonfunctional, concurrent world of rewrite theories.