\expandafter\ifx\csname doTocEntry\endcsname\relax \expandafter\endinput\fi \doTocEntry\toclikechapter{}{\csname a:TocLink\endcsname{2}{x2-1000}{QQ2-2-1}{Contents}}{8}\relax \doTocEntry\toclikechapter{}{\csname a:TocLink\endcsname{3}{x3-2000}{QQ2-3-2}{List of Figures}}{15}\relax \doTocEntry\tocchapter{1}{\csname a:TocLink\endcsname{4}{x4-30001}{QQ2-4-3}{Introduction}}{3}\relax \doTocEntry\tocsection{1.1}{\csname a:TocLink\endcsname{4}{x4-40001.1}{QQ2-4-4}{Simplicity, expressiveness, and performance}}{3}\relax \doTocEntry\tocsubsection{1.1.1}{\csname a:TocLink\endcsname{4}{x4-50001.1.1}{QQ2-4-5}{Simplicity}}{3}\relax \doTocEntry\tocsubsection{1.1.2}{\csname a:TocLink\endcsname{4}{x4-60001.1.2}{QQ2-4-6}{Expressiveness}}{16}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{4}{x4-70001.1.2}{QQ2-4-7}{Equational pattern matching}}{17}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{4}{x4-80001.1.2}{QQ2-4-8}{User-definable syntax and data}}{18}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{4}{x4-90001.1.2}{QQ2-4-9}{Types, subtypes, and partiality}}{18}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{4}{x4-100001.1.2}{QQ2-4-10}{Generic types and modules}}{20}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{4}{x4-110001.1.2}{QQ2-4-11}{Support for objects}}{20}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{4}{x4-120001.1.2}{QQ2-4-12}{Reflection}}{21}\relax \doTocEntry\tocsubsection{1.1.3}{\csname a:TocLink\endcsname{4}{x4-130001.1.3}{QQ2-4-13}{Performance}}{21}\relax \doTocEntry\tocsection{1.2}{\csname a:TocLink\endcsname{4}{x4-140001.2}{QQ2-4-14}{The logical foundations of Maude}}{23}\relax \doTocEntry\tocsection{1.3}{\csname a:TocLink\endcsname{4}{x4-150001.3}{QQ2-4-15}{Programming, specification, and verification}}{27}\relax \doTocEntry\tocsection{1.4}{\csname a:TocLink\endcsname{4}{x4-160001.4}{QQ2-4-16}{A high-performance logical framework}}{31}\relax \doTocEntry\tocsection{1.5}{\csname a:TocLink\endcsname{4}{x4-170001.5}{QQ2-4-17}{Core Maude vs. Full Maude}}{33}\relax \doTocEntry\tocsection{1.6}{\csname a:TocLink\endcsname{4}{x4-180001.6}{QQ2-4-18}{Manual structure}}{34}\relax \doTocEntry\tocsection{1.7}{\csname a:TocLink\endcsname{4}{x4-190001.7}{QQ2-4-19}{The Maude book}}{36}\relax \doTocEntry\toclikesubsection{}{\csname a:TocLink\endcsname{4}{x4-200001.7}{QQ2-4-20}{Acknowledgements}}{37}\relax \doTocEntry\tocpart{I}{\csname a:TocLink\endcsname{12}{x12-21000I}{QQ2-12-21}{Core Maude}}{41}\relax \doTocEntry\tocchapter{2}{\csname a:TocLink\endcsname{13}{x13-220002}{QQ2-13-22}{Using Maude}}{44}\relax \doTocEntry\tocsection{2.1}{\csname a:TocLink\endcsname{13}{x13-230002.1}{QQ2-13-23}{Getting Maude}}{44}\relax \doTocEntry\toclof{2.1}{\csname a:TocLink\endcsname{13}{x13-230011}{}{\ignorespaces Maude home page at \texttt {maude.cs.uiuc.edu}}}{figure}\relax \doTocEntry\tocsection{2.2}{\csname a:TocLink\endcsname{13}{x13-240002.2}{QQ2-13-25}{Running Maude}}{48}\relax \doTocEntry\toclof{2.2}{\csname a:TocLink\endcsname{13}{x13-240292}{}{\ignorespaces Running Maude inside Emacs}}{figure}\relax \doTocEntry\tocsection{2.3}{\csname a:TocLink\endcsname{13}{x13-250002.3}{QQ2-13-27}{Getting support and more information}}{60}\relax \doTocEntry\tocsection{2.4}{\csname a:TocLink\endcsname{13}{x13-260002.4}{QQ2-13-28}{Reporting bugs in Maude}}{62}\relax \doTocEntry\tocchapter{3}{\csname a:TocLink\endcsname{15}{x15-270003}{QQ2-15-29}{Syntax and Basic Parsing}}{65}\relax \doTocEntry\tocsection{3.1}{\csname a:TocLink\endcsname{15}{x15-280003.1}{QQ2-15-30}{Identifiers}}{65}\relax \doTocEntry\tocsection{3.2}{\csname a:TocLink\endcsname{15}{x15-290003.2}{QQ2-15-31}{Modules}}{65}\relax \doTocEntry\tocsection{3.3}{\csname a:TocLink\endcsname{15}{x15-300003.3}{QQ2-15-32}{Sorts and subsorts}}{68}\relax \doTocEntry\tocsection{3.4}{\csname a:TocLink\endcsname{15}{x15-310003.4}{QQ2-15-33}{Operator declarations}}{75}\relax \doTocEntry\tocsection{3.5}{\csname a:TocLink\endcsname{15}{x15-320003.5}{QQ2-15-34}{Kinds}}{83}\relax \doTocEntry\tocsection{3.6}{\csname a:TocLink\endcsname{15}{x15-330003.6}{QQ2-15-35}{Operator overloading}}{86}\relax \doTocEntry\tocsection{3.7}{\csname a:TocLink\endcsname{15}{x15-340003.7}{QQ2-15-36}{Variables}}{87}\relax \doTocEntry\tocsection{3.8}{\csname a:TocLink\endcsname{15}{x15-350003.8}{QQ2-15-37}{Terms and preregularity}}{90}\relax \doTocEntry\tocsection{3.9}{\csname a:TocLink\endcsname{15}{x15-360003.9}{QQ2-15-38}{Parsing}}{93}\relax \doTocEntry\tocsubsection{3.9.1}{\csname a:TocLink\endcsname{15}{x15-370003.9.1}{QQ2-15-39}{Default precedence values}}{97}\relax \doTocEntry\tocsubsection{3.9.2}{\csname a:TocLink\endcsname{15}{x15-380003.9.2}{QQ2-15-40}{Default gathering patterns}}{97}\relax \doTocEntry\tocsubsection{3.9.3}{\csname a:TocLink\endcsname{15}{x15-390003.9.3}{QQ2-15-41}{The extended signature of a module}}{100}\relax \doTocEntry\tocsubsection{3.9.4}{\csname a:TocLink\endcsname{15}{x15-400003.9.4}{QQ2-15-42}{Parsing examples}}{102}\relax \doTocEntry\tocchapter{4}{\csname a:TocLink\endcsname{19}{x19-410004}{QQ2-19-43}{Functional Modules}}{111}\relax \doTocEntry\tocsection{4.1}{\csname a:TocLink\endcsname{19}{x19-420004.1}{QQ2-19-44}{Unconditional equations}}{112}\relax \doTocEntry\tocsection{4.2}{\csname a:TocLink\endcsname{19}{x19-430004.2}{QQ2-19-45}{Unconditional memberships}}{115}\relax \doTocEntry\tocsection{4.3}{\csname a:TocLink\endcsname{19}{x19-440004.3}{QQ2-19-46}{Conditional equations and memberships}}{116}\relax \doTocEntry\tocsection{4.4}{\csname a:TocLink\endcsname{19}{x19-450004.4}{QQ2-19-47}{Operator attributes}}{127}\relax \doTocEntry\tocsubsection{4.4.1}{\csname a:TocLink\endcsname{19}{x19-460004.4.1}{QQ2-19-48}{Equational attributes}}{127}\relax \doTocEntry\tocsubsection{4.4.2}{\csname a:TocLink\endcsname{19}{x19-470004.4.2}{QQ2-19-49}{The \texttt {iter} attribute}}{133}\relax \doTocEntry\tocsubsection{4.4.3}{\csname a:TocLink\endcsname{19}{x19-480004.4.3}{QQ2-19-50}{Constructors}}{134}\relax \doTocEntry\tocsubsection{4.4.4}{\csname a:TocLink\endcsname{19}{x19-490004.4.4}{QQ2-19-51}{Polymorphic operators}}{147}\relax \doTocEntry\tocsubsection{4.4.5}{\csname a:TocLink\endcsname{19}{x19-500004.4.5}{QQ2-19-52}{Format}}{149}\relax \doTocEntry\tocsubsection{4.4.6}{\csname a:TocLink\endcsname{19}{x19-510004.4.6}{QQ2-19-53}{Ditto}}{161}\relax \doTocEntry\tocsubsection{4.4.7}{\csname a:TocLink\endcsname{19}{x19-520004.4.7}{QQ2-19-54}{Operator evaluation strategies}}{162}\relax \doTocEntry\tocsubsection{4.4.8}{\csname a:TocLink\endcsname{19}{x19-530004.4.8}{QQ2-19-55}{Memo}}{168}\relax \doTocEntry\tocsubsection{4.4.9}{\csname a:TocLink\endcsname{19}{x19-540004.4.9}{QQ2-19-56}{Frozen arguments}}{178}\relax \doTocEntry\tocsubsection{4.4.10}{\csname a:TocLink\endcsname{19}{x19-550004.4.10}{QQ2-19-57}{Special}}{181}\relax \doTocEntry\tocsection{4.5}{\csname a:TocLink\endcsname{19}{x19-560004.5}{QQ2-19-58}{Statement attributes}}{182}\relax \doTocEntry\tocsubsection{4.5.1}{\csname a:TocLink\endcsname{19}{x19-570004.5.1}{QQ2-19-59}{Labels}}{182}\relax \doTocEntry\tocsubsection{4.5.2}{\csname a:TocLink\endcsname{19}{x19-580004.5.2}{QQ2-19-60}{Metadata}}{184}\relax \doTocEntry\tocsubsection{4.5.3}{\csname a:TocLink\endcsname{19}{x19-590004.5.3}{QQ2-19-61}{Nonexec}}{186}\relax \doTocEntry\tocsubsection{4.5.4}{\csname a:TocLink\endcsname{19}{x19-600004.5.4}{QQ2-19-62}{Otherwise}}{187}\relax \doTocEntry\tocsubsection{4.5.5}{\csname a:TocLink\endcsname{19}{x19-610004.5.5}{QQ2-19-63}{Print}}{204}\relax \doTocEntry\tocsection{4.6}{\csname a:TocLink\endcsname{19}{x19-620004.6}{QQ2-19-64}{Admissible functional modules}}{208}\relax \doTocEntry\tocsection{4.7}{\csname a:TocLink\endcsname{19}{x19-630004.7}{QQ2-19-65}{Matching and equational simplification}}{209}\relax \doTocEntry\toclof{4.1}{\csname a:TocLink\endcsname{19}{x19-630111}{}{\ignorespaces Confluence diagram}}{figure}\relax \doTocEntry\tocsection{4.8}{\csname a:TocLink\endcsname{19}{x19-640004.8}{QQ2-19-67}{More on matching and simplification modulo}}{216}\relax \doTocEntry\tocsection{4.9}{\csname a:TocLink\endcsname{19}{x19-650004.9}{QQ2-19-68}{The \texttt {reduce}, \texttt {match}, \texttt {trace}, and \texttt {show} commands}}{229}\relax \doTocEntry\tocchapter{5}{\csname a:TocLink\endcsname{37}{x37-660005}{QQ2-37-69}{System Modules}}{243}\relax \doTocEntry\tocsection{5.1}{\csname a:TocLink\endcsname{37}{x37-670005.1}{QQ2-37-70}{Unconditional rules}}{244}\relax \doTocEntry\tocsection{5.2}{\csname a:TocLink\endcsname{37}{x37-680005.2}{QQ2-37-71}{Conditional rules}}{247}\relax \doTocEntry\tocsection{5.3}{\csname a:TocLink\endcsname{37}{x37-690005.3}{QQ2-37-72}{Admissible system modules}}{249}\relax \doTocEntry\toclof{5.1}{\csname a:TocLink\endcsname{37}{x37-690091}{}{\ignorespaces Coherence diagram}}{figure}\relax \doTocEntry\tocsection{5.4}{\csname a:TocLink\endcsname{37}{x37-700005.4}{QQ2-37-74}{The \texttt {rewrite}, \texttt {frewrite}, and \texttt {search} commands}}{255}\relax \doTocEntry\tocsubsection{5.4.1}{\csname a:TocLink\endcsname{37}{x37-710005.4.1}{QQ2-37-75}{The \texttt {rewrite} command}}{257}\relax \doTocEntry\tocsubsection{5.4.2}{\csname a:TocLink\endcsname{37}{x37-720005.4.2}{QQ2-37-76}{The \texttt {frewrite} command}}{264}\relax \doTocEntry\tocsubsection{5.4.3}{\csname a:TocLink\endcsname{37}{x37-730005.4.3}{QQ2-37-77}{The \texttt {search} command}}{268}\relax \doTocEntry\toclof{5.2}{\csname a:TocLink\endcsname{37}{x37-730062}{}{\ignorespaces Graphical representation of search graph in example}}{figure}\relax \doTocEntry\tocchapter{6}{\csname a:TocLink\endcsname{41}{x41-740006}{QQ2-41-79}{Module Operations}}{283}\relax \doTocEntry\tocsection{6.1}{\csname a:TocLink\endcsname{41}{x41-750006.1}{QQ2-41-80}{Module importation}}{283}\relax \doTocEntry\tocsubsection{6.1.1}{\csname a:TocLink\endcsname{41}{x41-760006.1.1}{QQ2-41-81}{Protecting}}{285}\relax \doTocEntry\tocsubsection{6.1.2}{\csname a:TocLink\endcsname{41}{x41-770006.1.2}{QQ2-41-82}{Extending}}{286}\relax \doTocEntry\tocsubsection{6.1.3}{\csname a:TocLink\endcsname{41}{x41-780006.1.3}{QQ2-41-83}{Including}}{287}\relax \doTocEntry\tocsubsection{6.1.4}{\csname a:TocLink\endcsname{41}{x41-790006.1.4}{QQ2-41-84}{Default conventions in module importations}}{287}\relax \doTocEntry\tocsubsection{6.1.5}{\csname a:TocLink\endcsname{41}{x41-800006.1.5}{QQ2-41-85}{Some module hierarchy examples}}{288}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{41}{x41-810006.1.5}{QQ2-41-86}{Prime numbers sieve}}{288}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{41}{x41-820006.1.5}{QQ2-41-87}{Vending machine}}{289}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{41}{x41-830006.1.5}{QQ2-41-88}{Bank accounts and object configurations}}{290}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{41}{x41-840006.1.5}{QQ2-41-89}{Hierarchy of predefined modules}}{292}\relax \doTocEntry\tocsection{6.2}{\csname a:TocLink\endcsname{41}{x41-850006.2}{QQ2-41-90}{Module summation and renaming}}{292}\relax \doTocEntry\tocsubsection{6.2.1}{\csname a:TocLink\endcsname{41}{x41-860006.2.1}{QQ2-41-91}{The summation module expression}}{292}\relax \doTocEntry\tocsubsection{6.2.2}{\csname a:TocLink\endcsname{41}{x41-870006.2.2}{QQ2-41-92}{Module renaming}}{298}\relax \doTocEntry\tocsection{6.3}{\csname a:TocLink\endcsname{41}{x41-880006.3}{QQ2-41-93}{Parameterized programming}}{318}\relax \doTocEntry\tocsubsection{6.3.1}{\csname a:TocLink\endcsname{41}{x41-890006.3.1}{QQ2-41-94}{Theories}}{318}\relax \doTocEntry\toclof{6.1}{\csname a:TocLink\endcsname{41}{x41-890441}{}{\ignorespaces Hierarchy of order theories}}{figure}\relax \doTocEntry\tocsubsection{6.3.2}{\csname a:TocLink\endcsname{41}{x41-900006.3.2}{QQ2-41-96}{Views}}{336}\relax \doTocEntry\tocsubsection{6.3.3}{\csname a:TocLink\endcsname{41}{x41-910006.3.3}{QQ2-41-97}{Parameterized modules}}{349}\relax \doTocEntry\toclof{6.2}{\csname a:TocLink\endcsname{41}{x41-910192}{}{\ignorespaces Structure of \texttt {LEX-PAIR}}}{figure}\relax \doTocEntry\tocsubsection{6.3.4}{\csname a:TocLink\endcsname{41}{x41-920006.3.4}{QQ2-41-99}{Module instantiation}}{359}\relax \doTocEntry\tocsubsection{6.3.5}{\csname a:TocLink\endcsname{41}{x41-930006.3.5}{QQ2-41-100}{Lists}}{384}\relax \doTocEntry\tocsubsection{6.3.6}{\csname a:TocLink\endcsname{41}{x41-940006.3.6}{QQ2-41-101}{Sorted lists}}{389}\relax \doTocEntry\tocchapter{7}{\csname a:TocLink\endcsname{50}{x50-950007}{QQ2-50-102}{Predefined Data Modules}}{399}\relax \doTocEntry\toclof{7.1}{\csname a:TocLink\endcsname{50}{x50-950031}{}{\ignorespaces Importation (protecting) graph of predefined modules}}{figure}\relax \doTocEntry\tocsection{7.1}{\csname a:TocLink\endcsname{50}{x50-960007.1}{QQ2-50-104}{Boolean values}}{402}\relax \doTocEntry\tocsection{7.2}{\csname a:TocLink\endcsname{50}{x50-970007.2}{QQ2-50-105}{Natural numbers}}{415}\relax \doTocEntry\tocsection{7.3}{\csname a:TocLink\endcsname{50}{x50-980007.3}{QQ2-50-106}{Random numbers and counters}}{442}\relax \doTocEntry\tocsection{7.4}{\csname a:TocLink\endcsname{50}{x50-990007.4}{QQ2-50-107}{Integer numbers}}{456}\relax \doTocEntry\tocsection{7.5}{\csname a:TocLink\endcsname{50}{x50-1000007.5}{QQ2-50-108}{Machine integers}}{475}\relax \doTocEntry\tocsection{7.6}{\csname a:TocLink\endcsname{50}{x50-1010007.6}{QQ2-50-109}{Rational numbers}}{489}\relax \doTocEntry\tocsection{7.7}{\csname a:TocLink\endcsname{50}{x50-1020007.7}{QQ2-50-110}{Floating-point numbers}}{507}\relax \doTocEntry\tocsection{7.8}{\csname a:TocLink\endcsname{50}{x50-1030007.8}{QQ2-50-111}{Strings}}{548}\relax \doTocEntry\tocsection{7.9}{\csname a:TocLink\endcsname{50}{x50-1040007.9}{QQ2-50-112}{String and number conversions}}{578}\relax \doTocEntry\tocsection{7.10}{\csname a:TocLink\endcsname{50}{x50-1050007.10}{QQ2-50-113}{Quoted identifiers}}{593}\relax \doTocEntry\tocsection{7.11}{\csname a:TocLink\endcsname{50}{x50-1060007.11}{QQ2-50-114}{Basic theories and standard views}}{604}\relax \doTocEntry\tocsubsection{7.11.1}{\csname a:TocLink\endcsname{50}{x50-1070007.11.1}{QQ2-50-115}{\texttt {TRIV}}}{604}\relax \doTocEntry\tocsubsection{7.11.2}{\csname a:TocLink\endcsname{50}{x50-1080007.11.2}{QQ2-50-116}{\texttt {DEFAULT}}}{612}\relax \doTocEntry\tocsubsection{7.11.3}{\csname a:TocLink\endcsname{50}{x50-1090007.11.3}{QQ2-50-117}{\texttt {STRICT-WEAK-ORDER} and \texttt {STRICT-TOTAL-ORDER}}}{620}\relax \doTocEntry\tocsubsection{7.11.4}{\csname a:TocLink\endcsname{50}{x50-1100007.11.4}{QQ2-50-118}{\texttt {TOTAL-PREORDER} and \texttt {TOTAL-ORDER}}}{629}\relax \doTocEntry\tocsection{7.12}{\csname a:TocLink\endcsname{50}{x50-1110007.12}{QQ2-50-119}{Containers: lists and sets}}{638}\relax \doTocEntry\toclof{7.2}{\csname a:TocLink\endcsname{50}{x50-1110012}{}{\ignorespaces Importation graph of parameterized list and set modules}}{figure}\relax \doTocEntry\tocsubsection{7.12.1}{\csname a:TocLink\endcsname{50}{x50-1120007.12.1}{QQ2-50-121}{Lists}}{641}\relax \doTocEntry\tocsubsection{7.12.2}{\csname a:TocLink\endcsname{50}{x50-1130007.12.2}{QQ2-50-122}{Sets}}{653}\relax \doTocEntry\tocsubsection{7.12.3}{\csname a:TocLink\endcsname{50}{x50-1140007.12.3}{QQ2-50-123}{Relating lists and sets}}{667}\relax \doTocEntry\tocsubsection{7.12.4}{\csname a:TocLink\endcsname{50}{x50-1150007.12.4}{QQ2-50-124}{Generalized lists}}{674}\relax \doTocEntry\tocsubsection{7.12.5}{\csname a:TocLink\endcsname{50}{x50-1160007.12.5}{QQ2-50-125}{Generalized sets}}{684}\relax \doTocEntry\tocsubsection{7.12.6}{\csname a:TocLink\endcsname{50}{x50-1170007.12.6}{QQ2-50-126}{Sortable lists}}{697}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{50}{x50-1180007.12.6}{QQ2-50-127}{Sorting lists with respect to a strict weak order}}{697}\relax \doTocEntry\toclof{7.3}{\csname a:TocLink\endcsname{50}{x50-1180023}{}{\ignorespaces From lists to weakly sortable lists}}{figure}\relax \doTocEntry\toclof{7.4}{\csname a:TocLink\endcsname{50}{x50-1180054}{}{\ignorespaces From weakly sortable lists to sortable lists}}{figure}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{50}{x50-1190007.12.6}{QQ2-50-130}{Sorting lists with respect to a total preorder}}{714}\relax \doTocEntry\toclof{7.5}{\csname a:TocLink\endcsname{50}{x50-1190025}{}{\ignorespaces Another version of sortable lists}}{figure}\relax \doTocEntry\tocsubsection{7.12.7}{\csname a:TocLink\endcsname{50}{x50-1200007.12.7}{QQ2-50-132}{Making lists out of sets}}{724}\relax \doTocEntry\tocsection{7.13}{\csname a:TocLink\endcsname{50}{x50-1210007.13}{QQ2-50-133}{Maps and arrays}}{734}\relax \doTocEntry\tocsubsection{7.13.1}{\csname a:TocLink\endcsname{50}{x50-1220007.13.1}{QQ2-50-134}{Maps}}{734}\relax \doTocEntry\tocsubsection{7.13.2}{\csname a:TocLink\endcsname{50}{x50-1230007.13.2}{QQ2-50-135}{Arrays}}{742}\relax \doTocEntry\tocsection{7.14}{\csname a:TocLink\endcsname{50}{x50-1240007.14}{QQ2-50-136}{A linear Diophantine equation solver}}{750}\relax \doTocEntry\tocchapter{8}{\csname a:TocLink\endcsname{56}{x56-1250008}{QQ2-56-137}{Object-Based Programming}}{767}\relax \doTocEntry\tocsection{8.1}{\csname a:TocLink\endcsname{56}{x56-1260008.1}{QQ2-56-138}{Configurations}}{767}\relax \doTocEntry\toclof{8.1}{\csname a:TocLink\endcsname{56}{x56-1260141}{}{\ignorespaces Importation graph of bank modules}}{figure}\relax \doTocEntry\toclof{8.2}{\csname a:TocLink\endcsname{56}{x56-1260232}{}{\ignorespaces Importation graph of ticker modules}}{figure}\relax \doTocEntry\tocsection{8.2}{\csname a:TocLink\endcsname{56}{x56-1270008.2}{QQ2-56-141}{Object-message fair rewriting}}{806}\relax \doTocEntry\tocsection{8.3}{\csname a:TocLink\endcsname{56}{x56-1280008.3}{QQ2-56-142}{Example: data agents}}{808}\relax \doTocEntry\toclof{8.3}{\csname a:TocLink\endcsname{56}{x56-1280063}{}{\ignorespaces Importation graph of data-agents modules}}{figure}\relax \doTocEntry\tocsection{8.4}{\csname a:TocLink\endcsname{56}{x56-1290008.4}{QQ2-56-144}{External objects}}{823}\relax \doTocEntry\tocsubsection{8.4.1}{\csname a:TocLink\endcsname{56}{x56-1300008.4.1}{QQ2-56-145}{Sockets}}{824}\relax \doTocEntry\tocsubsection{8.4.2}{\csname a:TocLink\endcsname{56}{x56-1310008.4.2}{QQ2-56-146}{Buffered sockets}}{856}\relax \doTocEntry\tocchapter{9}{\csname a:TocLink\endcsname{61}{x61-1320009}{QQ2-61-147}{Model Checking Invariants Through Search}}{869}\relax \doTocEntry\tocsection{9.1}{\csname a:TocLink\endcsname{61}{x61-1330009.1}{QQ2-61-148}{Invariants}}{869}\relax \doTocEntry\tocsection{9.2}{\csname a:TocLink\endcsname{61}{x61-1340009.2}{QQ2-61-149}{Model checking of invariants}}{870}\relax \doTocEntry\tocsection{9.3}{\csname a:TocLink\endcsname{61}{x61-1350009.3}{QQ2-61-150}{Bounded model checking of invariants}}{880}\relax \doTocEntry\tocsection{9.4}{\csname a:TocLink\endcsname{61}{x61-1360009.4}{QQ2-61-151}{Verifying infinite-state systems through abstractions}}{885}\relax \doTocEntry\tocchapter{10}{\csname a:TocLink\endcsname{64}{x64-13700010}{QQ2-64-152}{LTL Model Checking}}{897}\relax \doTocEntry\tocsection{10.1}{\csname a:TocLink\endcsname{64}{x64-13800010.1}{QQ2-64-153}{LTL formulas and the \texttt {LTL} module}}{897}\relax \doTocEntry\tocsection{10.2}{\csname a:TocLink\endcsname{64}{x64-13900010.2}{QQ2-64-154}{Associating Kripke structures to rewrite theories}}{900}\relax \doTocEntry\tocsection{10.3}{\csname a:TocLink\endcsname{64}{x64-14000010.3}{QQ2-64-155}{LTL model checking}}{909}\relax \doTocEntry\toclof{10.1}{\csname a:TocLink\endcsname{64}{x64-1400151}{}{\ignorespaces Importation graph of model-checking modules}}{figure}\relax \doTocEntry\tocsection{10.4}{\csname a:TocLink\endcsname{64}{x64-14100010.4}{QQ2-64-157}{The LTL satisfiability and tautology checker}}{927}\relax \doTocEntry\toclof{10.2}{\csname a:TocLink\endcsname{64}{x64-1410062}{}{\ignorespaces Graphical representation of a Kripke structure}}{figure}\relax \doTocEntry\tocsection{10.5}{\csname a:TocLink\endcsname{64}{x64-14200010.5}{QQ2-64-159}{Other model-checking examples}}{934}\relax \doTocEntry\tocchapter{11}{\csname a:TocLink\endcsname{66}{x66-14300011}{QQ2-66-160}{Reflection, Metalevel Computation, and Strategies}}{937}\relax \doTocEntry\tocsection{11.1}{\csname a:TocLink\endcsname{66}{x66-14400011.1}{QQ2-66-161}{Reflection and metalevel computation}}{937}\relax \doTocEntry\toclof{11.1}{\csname a:TocLink\endcsname{66}{x66-1440041}{}{\ignorespaces Importation graph of metalevel modules}}{figure}\relax \doTocEntry\tocsection{11.2}{\csname a:TocLink\endcsname{66}{x66-14500011.2}{QQ2-66-163}{The \texttt {META-TERM} module}}{942}\relax \doTocEntry\tocsubsection{11.2.1}{\csname a:TocLink\endcsname{66}{x66-14600011.2.1}{QQ2-66-164}{Metarepresenting sorts and kinds}}{942}\relax \doTocEntry\tocsubsection{11.2.2}{\csname a:TocLink\endcsname{66}{x66-14700011.2.2}{QQ2-66-165}{Metarepresenting terms}}{943}\relax \doTocEntry\tocsection{11.3}{\csname a:TocLink\endcsname{66}{x66-14800011.3}{QQ2-66-166}{The \texttt {META-MODULE} module: Metarepresenting modules}}{949}\relax \doTocEntry\tocsection{11.4}{\csname a:TocLink\endcsname{66}{x66-14900011.4}{QQ2-66-167}{The \texttt {META-LEVEL} module: Metalevel operations}}{958}\relax \doTocEntry\tocsubsection{11.4.1}{\csname a:TocLink\endcsname{66}{x66-15000011.4.1}{QQ2-66-168}{Moving between reflection levels: \texttt {upModule}, \texttt {upTerm}, \texttt {downTerm}, and others}}{960}\relax \doTocEntry\tocsubsection{11.4.2}{\csname a:TocLink\endcsname{66}{x66-15100011.4.2}{QQ2-66-169}{Simplifying: \texttt {metaReduce} and \texttt {metaNormalize}}}{973}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-15200011.4.2}{QQ2-66-170}{\texttt {metaReduce}}}{973}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-15300011.4.2}{QQ2-66-171}{\texttt {metaNormalize}}}{977}\relax \doTocEntry\tocsubsection{11.4.3}{\csname a:TocLink\endcsname{66}{x66-15400011.4.3}{QQ2-66-172}{Rewriting: \texttt {metaRewrite} and \texttt {metaFrewrite}}}{980}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-15500011.4.3}{QQ2-66-173}{\texttt {metaRewrite}}}{980}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-15600011.4.3}{QQ2-66-174}{\texttt {metaFrewrite}}}{983}\relax \doTocEntry\tocsubsection{11.4.4}{\csname a:TocLink\endcsname{66}{x66-15700011.4.4}{QQ2-66-175}{Applying rules: \texttt {metaApply} and \texttt {metaXapply}}}{985}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-15800011.4.4}{QQ2-66-176}{\texttt {metaApply}}}{985}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-15900011.4.4}{QQ2-66-177}{\texttt {metaXapply}}}{991}\relax \doTocEntry\tocsubsection{11.4.5}{\csname a:TocLink\endcsname{66}{x66-16000011.4.5}{QQ2-66-178}{Matching: \texttt {metaMatch} and \texttt {metaXmatch}}}{995}\relax \doTocEntry\tocsubsection{11.4.6}{\csname a:TocLink\endcsname{66}{x66-16100011.4.6}{QQ2-66-179}{Searching: \texttt {metaSearch} and \texttt {metaSearchPath}}}{1007}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-16200011.4.6}{QQ2-66-180}{\texttt {metaSearch}}}{1007}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-16300011.4.6}{QQ2-66-181}{\texttt {metaSearchPath}}}{1010}\relax \doTocEntry\tocsubsection{11.4.7}{\csname a:TocLink\endcsname{66}{x66-16400011.4.7}{QQ2-66-182}{Parsing and pretty-printing: \texttt {metaParse} and \texttt {metaPrettyPrint}}}{1014}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-16500011.4.7}{QQ2-66-183}{\texttt {metaParse}}}{1014}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-16600011.4.7}{QQ2-66-184}{\texttt {metaPrettyPrint}}}{1017}\relax \doTocEntry\tocsubsection{11.4.8}{\csname a:TocLink\endcsname{66}{x66-16700011.4.8}{QQ2-66-185}{Sort operations}}{1024}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-16800011.4.8}{QQ2-66-186}{\texttt {sortLeq}}}{1024}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-16900011.4.8}{QQ2-66-187}{\texttt {sameKind}}}{1031}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-17000011.4.8}{QQ2-66-188}{\texttt {completeName}}}{1036}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-17100011.4.8}{QQ2-66-189}{\texttt {getKind} and \texttt {getKinds}}}{1039}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-17200011.4.8}{QQ2-66-190}{\texttt {lesserSorts}}}{1044}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-17300011.4.8}{QQ2-66-191}{\texttt {leastSort}}}{1050}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-17400011.4.8}{QQ2-66-192}{\texttt {glbSorts}}}{1052}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-17500011.4.8}{QQ2-66-193}{\texttt {maximalSorts} and \texttt {minimalSorts}}}{1063}\relax \doTocEntry\tocsubsubsection{}{\csname a:TocLink\endcsname{66}{x66-17600011.4.8}{QQ2-66-194}{\texttt {maximalAritySet}}}{1066}\relax \doTocEntry\tocsubsection{11.4.9}{\csname a:TocLink\endcsname{66}{x66-17700011.4.9}{QQ2-66-195}{Other metalevel operations: \texttt {wellFormed}}}{1073}\relax \doTocEntry\tocsection{11.5}{\csname a:TocLink\endcsname{66}{x66-17800011.5}{QQ2-66-196}{Internal strategies}}{1080}\relax \doTocEntry\tocchapter{12}{\csname a:TocLink\endcsname{67}{x67-17900012}{QQ2-67-197}{Unification}}{1091}\relax \doTocEntry\tocsection{12.1}{\csname a:TocLink\endcsname{67}{x67-18000012.1}{QQ2-67-198}{Introduction}}{1091}\relax \doTocEntry\tocsection{12.2}{\csname a:TocLink\endcsname{67}{x67-18100012.2}{QQ2-67-199}{Order-sorted unification modulo a set of axioms}}{1092}\relax \doTocEntry\tocsection{12.3}{\csname a:TocLink\endcsname{67}{x67-18200012.3}{QQ2-67-200}{Theories currently supported}}{1093}\relax \doTocEntry\tocsection{12.4}{\csname a:TocLink\endcsname{67}{x67-18300012.4}{QQ2-67-201}{The \texttt {unify} command}}{1094}\relax \doTocEntry\tocsection{12.5}{\csname a:TocLink\endcsname{67}{x67-18400012.5}{QQ2-67-202}{Unification at the metalevel: \texttt {metaUnify} and \texttt {metaDisjointUnify}}}{1108}\relax \doTocEntry\tocsection{12.6}{\csname a:TocLink\endcsname{67}{x67-18500012.6}{QQ2-67-203}{Some applications of unification}}{1118}\relax \doTocEntry\tocsubsection{12.6.1}{\csname a:TocLink\endcsname{67}{x67-18600012.6.1}{QQ2-67-204}{Narrowing-based unification}}{1118}\relax \doTocEntry\tocsubsection{12.6.2}{\csname a:TocLink\endcsname{67}{x67-18700012.6.2}{QQ2-67-205}{Symbolic reachability analysis in rewrite theories}}{1120}\relax \doTocEntry\tocsubsection{12.6.3}{\csname a:TocLink\endcsname{67}{x67-18800012.6.3}{QQ2-67-206}{Other automated deduction applications}}{1122}\relax \doTocEntry\tocsection{12.7}{\csname a:TocLink\endcsname{67}{x67-18900012.7}{QQ2-67-207}{Endogenous vs. exogenous order-sorted unification algorithms}}{1123}\relax \doTocEntry\tocchapter{13}{\csname a:TocLink\endcsname{71}{x71-19000013}{QQ2-71-208}{User Interfaces and Metalanguage Applications}}{1127}\relax \doTocEntry\tocsection{13.1}{\csname a:TocLink\endcsname{71}{x71-19100013.1}{QQ2-71-209}{The \texttt {LOOP-MODE} module}}{1127}\relax \doTocEntry\tocsection{13.2}{\csname a:TocLink\endcsname{71}{x71-19200013.2}{QQ2-71-210}{User interfaces}}{1128}\relax \doTocEntry\tocsection{13.3}{\csname a:TocLink\endcsname{71}{x71-19300013.3}{QQ2-71-211}{Using the loop}}{1145}\relax \doTocEntry\tocsection{13.4}{\csname a:TocLink\endcsname{71}{x71-19400013.4}{QQ2-71-212}{Tokens, bubbles, and metaparsing}}{1160}\relax \doTocEntry\tocchapter{14}{\csname a:TocLink\endcsname{72}{x72-19500014}{QQ2-72-213}{Debugging and Troubleshooting}}{1177}\relax \doTocEntry\tocsection{14.1}{\csname a:TocLink\endcsname{72}{x72-19600014.1}{QQ2-72-214}{Debugging approaches}}{1177}\relax \doTocEntry\tocsubsection{14.1.1}{\csname a:TocLink\endcsname{72}{x72-19700014.1.1}{QQ2-72-215}{Tracing}}{1177}\relax \doTocEntry\tocsubsection{14.1.2}{\csname a:TocLink\endcsname{72}{x72-19800014.1.2}{QQ2-72-216}{Term coloring}}{1191}\relax \doTocEntry\tocsubsection{14.1.3}{\csname a:TocLink\endcsname{72}{x72-19900014.1.3}{QQ2-72-217}{The debugger}}{1193}\relax \doTocEntry\tocsubsection{14.1.4}{\csname a:TocLink\endcsname{72}{x72-20000014.1.4}{QQ2-72-218}{The profiler}}{1199}\relax \doTocEntry\toclof{14.1}{\csname a:TocLink\endcsname{72}{x72-2000281}{}{\ignorespaces Number of rewrites and cpu time for different versions of the sorting algorithms}}{figure}\relax \doTocEntry\tocsubsection{14.1.5}{\csname a:TocLink\endcsname{72}{x72-20100014.1.5}{QQ2-72-220}{Performance note}}{1223}\relax \doTocEntry\tocsection{14.2}{\csname a:TocLink\endcsname{72}{x72-20200014.2}{QQ2-72-221}{Traps and known problems}}{1224}\relax \doTocEntry\tocsubsection{14.2.1}{\csname a:TocLink\endcsname{72}{x72-20300014.2.1}{QQ2-72-222}{Associativity and idempotency}}{1224}\relax \doTocEntry\tocsubsection{14.2.2}{\csname a:TocLink\endcsname{72}{x72-20400014.2.2}{QQ2-72-223}{Segmentation fault (core dumped)}}{1229}\relax \doTocEntry\tocsubsection{14.2.3}{\csname a:TocLink\endcsname{72}{x72-20500014.2.3}{QQ2-72-224}{Bare variable lefthand sides}}{1232}\relax \doTocEntry\tocsubsection{14.2.4}{\csname a:TocLink\endcsname{72}{x72-20600014.2.4}{QQ2-72-225}{Operator overloading and associativity}}{1233}\relax \doTocEntry\tocsubsection{14.2.5}{\csname a:TocLink\endcsname{72}{x72-20700014.2.5}{QQ2-72-226}{Preregularity and equational attributes}}{1237}\relax \doTocEntry\tocsubsection{14.2.6}{\csname a:TocLink\endcsname{72}{x72-20800014.2.6}{QQ2-72-227}{Collapse theories}}{1246}\relax \doTocEntry\tocsubsection{14.2.7}{\csname a:TocLink\endcsname{72}{x72-20900014.2.7}{QQ2-72-228}{One-sided identities and associativity}}{1251}\relax \doTocEntry\tocsubsection{14.2.8}{\csname a:TocLink\endcsname{72}{x72-21000014.2.8}{QQ2-72-229}{Memberships for associative operators}}{1262}\relax \doTocEntry\tocsubsection{14.2.9}{\csname a:TocLink\endcsname{72}{x72-21100014.2.9}{QQ2-72-230}{Memberships for iterated operators}}{1280}\relax \doTocEntry\tocsubsection{14.2.10}{\csname a:TocLink\endcsname{72}{x72-21200014.2.10}{QQ2-72-231}{Ambiguity in \texttt {print} attribute items}}{1288}\relax \doTocEntry\tocpart{II}{\csname a:TocLink\endcsname{75}{x75-213000II}{QQ2-75-232}{Full Maude}}{1297}\relax \doTocEntry\tocchapter{15}{\csname a:TocLink\endcsname{76}{x76-21400015}{QQ2-76-233}{Full Maude: Extending Core Maude}}{1299}\relax \doTocEntry\tocsection{15.1}{\csname a:TocLink\endcsname{76}{x76-21500015.1}{QQ2-76-234}{Running Full Maude}}{1300}\relax \doTocEntry\tocsection{15.2}{\csname a:TocLink\endcsname{76}{x76-21600015.2}{QQ2-76-235}{Using Core Maude modules in Full Maude}}{1315}\relax \doTocEntry\tocsection{15.3}{\csname a:TocLink\endcsname{76}{x76-21700015.3}{QQ2-76-236}{Additional module operations in Full Maude}}{1319}\relax \doTocEntry\tocsubsection{15.3.1}{\csname a:TocLink\endcsname{76}{x76-21800015.3.1}{QQ2-76-237}{The tuple and power module expressions}}{1324}\relax \doTocEntry\tocsubsection{15.3.2}{\csname a:TocLink\endcsname{76}{x76-21900015.3.2}{QQ2-76-238}{Parameterized views}}{1330}\relax \doTocEntry\tocsection{15.4}{\csname a:TocLink\endcsname{76}{x76-22000015.4}{QQ2-76-239}{Moving up and down between reflection levels}}{1336}\relax \doTocEntry\tocsubsection{15.4.1}{\csname a:TocLink\endcsname{76}{x76-22100015.4.1}{QQ2-76-240}{Up}}{1339}\relax \doTocEntry\tocsubsection{15.4.2}{\csname a:TocLink\endcsname{76}{x76-22200015.4.2}{QQ2-76-241}{Down}}{1344}\relax \doTocEntry\tocsection{15.5}{\csname a:TocLink\endcsname{76}{x76-22300015.5}{QQ2-76-242}{Differences between Full Maude and Core Maude}}{1348}\relax \doTocEntry\tocchapter{16}{\csname a:TocLink\endcsname{81}{x81-22400016}{QQ2-81-243}{Narrowing}}{1357}\relax \doTocEntry\tocsection{16.1}{\csname a:TocLink\endcsname{81}{x81-22500016.1}{QQ2-81-244}{Introduction}}{1357}\relax \doTocEntry\tocsection{16.2}{\csname a:TocLink\endcsname{81}{x81-22600016.2}{QQ2-81-245}{Completeness of narrowing}}{1360}\relax \doTocEntry\tocsection{16.3}{\csname a:TocLink\endcsname{81}{x81-22700016.3}{QQ2-81-246}{Theories supported}}{1361}\relax \doTocEntry\tocsection{16.4}{\csname a:TocLink\endcsname{81}{x81-22800016.4}{QQ2-81-247}{The narrowing search command}}{1363}\relax \doTocEntry\tocsection{16.5}{\csname a:TocLink\endcsname{81}{x81-22900016.5}{QQ2-81-248}{Unification with identities: The \texttt {id-unify} command}}{1375}\relax \doTocEntry\tocsection{16.6}{\csname a:TocLink\endcsname{81}{x81-23000016.6}{QQ2-81-249}{Reachability at the metalevel: \texttt {metaNarrowSearch}}}{1387}\relax \doTocEntry\tocsection{16.7}{\csname a:TocLink\endcsname{81}{x81-23100016.7}{QQ2-81-250}{Unification with identities at the metalevel: \texttt {metaACUUnify}}}{1392}\relax \doTocEntry\tocchapter{17}{\csname a:TocLink\endcsname{89}{x89-23200017}{QQ2-89-251}{Object-Oriented Modules}}{1397}\relax \doTocEntry\tocsection{17.1}{\csname a:TocLink\endcsname{89}{x89-23300017.1}{QQ2-89-252}{Object-oriented systems}}{1397}\relax \doTocEntry\tocsubsection{17.1.1}{\csname a:TocLink\endcsname{89}{x89-23400017.1.1}{QQ2-89-253}{Objects and messages}}{1397}\relax \doTocEntry\tocsubsection{17.1.2}{\csname a:TocLink\endcsname{89}{x89-23500017.1.2}{QQ2-89-254}{Classes}}{1401}\relax \doTocEntry\tocsubsection{17.1.3}{\csname a:TocLink\endcsname{89}{x89-23600017.1.3}{QQ2-89-255}{Inheritance}}{1406}\relax \doTocEntry\tocsubsection{17.1.4}{\csname a:TocLink\endcsname{89}{x89-23700017.1.4}{QQ2-89-256}{Object-oriented rules}}{1409}\relax \doTocEntry\tocsection{17.2}{\csname a:TocLink\endcsname{89}{x89-23800017.2}{QQ2-89-257}{Example: a rent-a-car store}}{1416}\relax \doTocEntry\tocsection{17.3}{\csname a:TocLink\endcsname{89}{x89-23900017.3}{QQ2-89-258}{Object-oriented parameterized programming}}{1426}\relax \doTocEntry\tocsubsection{17.3.1}{\csname a:TocLink\endcsname{89}{x89-24000017.3.1}{QQ2-89-259}{Theories}}{1426}\relax \doTocEntry\tocsubsection{17.3.2}{\csname a:TocLink\endcsname{89}{x89-24100017.3.2}{QQ2-89-260}{Views}}{1427}\relax \doTocEntry\tocsubsection{17.3.3}{\csname a:TocLink\endcsname{89}{x89-24200017.3.3}{QQ2-89-261}{Parameterized object-oriented modules}}{1428}\relax \doTocEntry\tocsection{17.4}{\csname a:TocLink\endcsname{89}{x89-24300017.4}{QQ2-89-262}{Module operations on object-oriented modules}}{1432}\relax \doTocEntry\tocsubsection{17.4.1}{\csname a:TocLink\endcsname{89}{x89-24400017.4.1}{QQ2-89-263}{Module summation and renaming}}{1432}\relax \doTocEntry\tocsubsection{17.4.2}{\csname a:TocLink\endcsname{89}{x89-24500017.4.2}{QQ2-89-264}{Module instantiation}}{1434}\relax \doTocEntry\tocsection{17.5}{\csname a:TocLink\endcsname{89}{x89-24600017.5}{QQ2-89-265}{Example: extended rent-a-car store}}{1436}\relax \doTocEntry\tocsection{17.6}{\csname a:TocLink\endcsname{89}{x89-24700017.6}{QQ2-89-266}{A strategy for sequential rule execution}}{1447}\relax \doTocEntry\tocsection{17.7}{\csname a:TocLink\endcsname{89}{x89-24800017.7}{QQ2-89-267}{Model checking a round-robin scheduling algorithm}}{1454}\relax \doTocEntry\tocsection{17.8}{\csname a:TocLink\endcsname{89}{x89-24900017.8}{QQ2-89-268}{From object-oriented modules to system modules}}{1465}\relax \doTocEntry\tocpart{III}{\csname a:TocLink\endcsname{95}{x95-250000III}{QQ2-95-269}{Reference}}{1479}\relax \doTocEntry\tocchapter{18}{\csname a:TocLink\endcsname{96}{x96-25100018}{QQ2-96-270}{Complete List of Maude Commands}}{1481}\relax \doTocEntry\tocsection{18.1}{\csname a:TocLink\endcsname{96}{x96-25200018.1}{QQ2-96-271}{Command line flags}}{1481}\relax \doTocEntry\tocsection{18.2}{\csname a:TocLink\endcsname{96}{x96-25300018.2}{QQ2-96-272}{Rewriting commands}}{1482}\relax \doTocEntry\tocsection{18.3}{\csname a:TocLink\endcsname{96}{x96-25400018.3}{QQ2-96-273}{Matching commands}}{1486}\relax \doTocEntry\tocsection{18.4}{\csname a:TocLink\endcsname{96}{x96-25500018.4}{QQ2-96-274}{Searching commands}}{1486}\relax \doTocEntry\tocsection{18.5}{\csname a:TocLink\endcsname{96}{x96-25600018.5}{QQ2-96-275}{Unification command}}{1487}\relax \doTocEntry\tocsection{18.6}{\csname a:TocLink\endcsname{96}{x96-25700018.6}{QQ2-96-276}{Tracing commands}}{1487}\relax \doTocEntry\tocsection{18.7}{\csname a:TocLink\endcsname{96}{x96-25800018.7}{QQ2-96-277}{Print attribute commands}}{1490}\relax \doTocEntry\tocsection{18.8}{\csname a:TocLink\endcsname{96}{x96-25900018.8}{QQ2-96-278}{Print option commands}}{1490}\relax \doTocEntry\tocsection{18.9}{\csname a:TocLink\endcsname{96}{x96-26000018.9}{QQ2-96-279}{Show option commands}}{1491}\relax \doTocEntry\tocsection{18.10}{\csname a:TocLink\endcsname{96}{x96-26100018.10}{QQ2-96-280}{Show commands}}{1492}\relax \doTocEntry\tocsection{18.11}{\csname a:TocLink\endcsname{96}{x96-26200018.11}{QQ2-96-281}{Profiler commands}}{1493}\relax \doTocEntry\tocsection{18.12}{\csname a:TocLink\endcsname{96}{x96-26300018.12}{QQ2-96-282}{Debugger commands}}{1493}\relax \doTocEntry\tocsection{18.13}{\csname a:TocLink\endcsname{96}{x96-26400018.13}{QQ2-96-283}{Miscellaneous commands}}{1495}\relax \doTocEntry\tocsection{18.14}{\csname a:TocLink\endcsname{96}{x96-26500018.14}{QQ2-96-284}{System level commands}}{1496}\relax \doTocEntry\tocchapter{19}{\csname a:TocLink\endcsname{97}{x97-26600019}{QQ2-97-285}{Core Maude Grammar}}{1501}\relax \doTocEntry\tocsection{19.1}{\csname a:TocLink\endcsname{97}{x97-26700019.1}{QQ2-97-286}{The grammar}}{1501}\relax \doTocEntry\tocsection{19.2}{\csname a:TocLink\endcsname{97}{x97-26800019.2}{QQ2-97-287}{Synonyms}}{1505}\relax \doTocEntry\tocsection{19.3}{\csname a:TocLink\endcsname{97}{x97-26900019.3}{QQ2-97-288}{Lexical Issues}}{1506}\relax \doTocEntry\toclikechapter{}{\csname a:TocLink\endcsname{98}{x98-27000019.3}{QQ2-98-289}{Bibliography}}{1509}\relax \doTocEntry\tocchapter{}{\csname a:TocLink\endcsname{98}{Q1-98-290}{}{Bibliography}}{1522}\relax \doTocEntry\toclikechapter{}{\csname a:TocLink\endcsname{99}{x99-27100019.3}{QQ2-99-291}{Index}}{1525}\relax \doTocEntry\toclikechapter{}{\csname a:TocLink\endcsname{100}{x100-27200019.3}{QQ2-100-292}{Index of Maude Modules}}{1539}\relax \doTocEntry\toclikechapter{}{\csname a:TocLink\endcsname{101}{x101-27300019.3}{QQ2-101-293}{Index of Maude Theories}}{1547}\relax \doTocEntry\toclikechapter{}{\csname a:TocLink\endcsname{102}{x102-27400019.3}{QQ2-102-294}{Index of Maude Views}}{1551}\relax \par