List of Figures

2.1 Maude home page at
2.2 Running Maude inside Emacs
4.1 Confluence diagram
5.1 Coherence diagram
5.2 Graphical representation of search graph in example
6.1 Hierarchy of order theories
6.2 Structure of LEX-PAIR
7.1 Importation (protecting) graph of predefined modules
7.2 Importation graph of parameterized list and set modules
7.3 From lists to weakly sortable lists
7.4 From weakly sortable lists to sortable lists
7.5 Another version of sortable lists
8.1 Importation graph of bank modules
8.2 Importation graph of ticker modules
8.3 Importation graph of data-agents modules
10.1 Behavior of the amatchrew combinator
10.2 Family tree defined by the example predicates
12.1 Importation graph of model-checking modules
12.2 Graphical representation of a Kripke structure
17.1 Importation graph of metalevel modules
17.2 Folding variant narrowing tree for the term < $ q q X Y >.
19.1 MiniMaude‚Äôs statechart.
20.1 Number of rewrites and CPU time for different versions of the sorting algorithms