and is thus a conditional term rewrite system; if needed, it could easily be turned into a non-conditional term rewrite system by slightly modifying the definitions of three functions (i.e., adding extra parameters and auxiliary functions), as explained in Annex \[ANNEX-REC\]. Our main results are the following:

-   Our model is [*large*]{}. It is 1575-line long and contains 13 sorts, 18 constructors, 644 non-constructors, and 684 rewrite rules. Although research on term rewriting led to a wealth of scientific publications, it is difficult to find concrete examples of large term-rewrite systems: for instance, in the data base of models accumulated during the three Rewrite Engines Competition (2006, 2008, and 2010), the largest models are less than 300-line long. There exist indeed larger (e.g., 10,000-line long) term rewrite systems, but they are either generated automatically (and, thus, difficult to understand by humans) or they are actual implementations of compilers or translators (and, often, are not “pure” term rewrite systems, as they rely upon higher-level features, e.g., subsorts or strategies).

-   Our model is [*exhaustive*]{}, as it fully describes the MAA algorithm, including its “mode of operation” and its segmentation of messages larger than 1024 bytes.

-   Our model is [*self-contained*]{}, as 