Index

abort, 1 (debugger), 2 (debugger), 3 (debugger)
abstraction, see model checking
always-advise, 5
ansi-color, 6
AProVe, 7
array, 89
ASF+SDF, 10n, 11n, 12
assoc, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23
associative, see assoc
attribute, 2526
    equational, 2728
    statement, 2930

batch, 31
Boolean value, 3233
break point, 34, 35
break select, 36, 37
bubble, 38

CafeOBJ, 39
cd, 40
ceq, 41
ChC, 42, 43, 44, 45
check, 46, 47
Church-Rosser, 48
    context-sensitive, 49
    ground, 50
    modulo, 51
class, 52 (Full Maude)
    inheritance, 53 (Full Maude)
        multiple, 54 (Full Maude)
Clear, 55
cmb, 56
coherence, 57, 58
    checking, 59
    completion, 60 (Full Maude)
    ground, 61
collapse theory, 62, 63
comm, 64, 65, 66, 67, 68
comment, 69, 70
    multiline, 71
commutative, see comm
config, 73, 74, 75, 76
configuration, see config
confluence, 78
connected component, see subsort relation
constant, 80
    metarepresentation, 81
    qualified, 82
constructor, 8384
    non-free, 85
constructor, see ctor
cont, see continue
continue, 88, 89
core dumped, 90
Core Maude, 91
counter, 9293
cq, see ceq
CRC, 95, 96, 97, 98, 99
crl, 100
ctor, 101, 102
CVC4, 103104

deadlock freedom, 105
debug dsrewrite, 106
debug erewrite, 107
debug frewrite, 108
debug reduce, 109
debug rewrite, 110
debug srewrite, 111
debugger, 112, 113, 114115
debugging, 116, see tracing, term coloring, 118 (Full Maude)
dependent type, 119
descent function, 120, 121122
    downModule, 123
    metaApply, 124
    metaCheck, 125
    metFrewrite, 126
    metaGetVariant, 127
    metaNarrowingApply, 128
    metaNarrowingSearch, 129
    metaNarrowingSearchPath, 130
    metaNormalize, 131
    metaParse, 132
    metaPrettyPrint, 133
    metaReduce, 134
    metaRewrite, 135
    metaSrewrite, 136
    metaUnify, 137138
    metaVariantUnify, 139
    metaXapply, 140
    upModule, 141
    upTerm, 142
design, 143144
Diophantine equation solver, 145
distributed dataset, 146
ditto, 147
do clear memo, 148
dsrew, see dsrewrite
dsrewrite, 150, 151
    metarepresentation, see descent function

ELAN, 153, 154n, 155
eof, 156
eq, 157
equation, 158159
    executable, 160, 161
    metarepresentation, 162
equational condition, 163164
    abbreviated Boolean equation, 165, 166
    matching equation, 167, 168, 169
    ordinary equation, 170
    satisfaction, 171
equational simplification, 172
    modulo, 173, 174, 175
    sharing, 176n, 177
erew, see erewrite
erewrite, 179, 180, 181
erewrite-loop-mode, 182
evaluation strategy, see strategy
ex, see extending
expressiveness, 185186
extending, 187, 188
external object, 189190

File IO, 191192
file.maude, 193194
finite variant property, 195
    checking, 196
fmod, 197, 198
format, 199, 200, 201
formula
    satisfiable, 202
    unsatisfiable, 203
    valid, 204
foundations, 205206
frew, see frewrite
frewrite, 208, 209, 210, 211, 212
    metarepresentation, see descent function
frozen argument, see strategy
frozen, 215
fth, 216
Full Maude, 217, 218n, 219, 220, 221222
    differences with Core Maude, 223
fvu-narrow, 224
    metarepresentation, see descent function

gather, 226, 227
get irredundant variants, 228229, 230
get variants, 231232, 233

help, 234

id, 235, 236, 237, 238, 239, 240
idem, 241, 242, 243, 244, 245, 246, 247, 248, 249
idempotent, see idem
identifier, 251252, 253, 254, 255, 256, 257
    escape character, 258
    nonprinting characters, 259
    quoted, see quoted identifier
    special, 261
identity, see id
in, 263, 264, 265, 266
inc, see including
including, 268, 269, 270, 271
initial algebra, 272
interaction, 273274, 275 (Full Maude)
    interrupt, 276
    metarepresentation, see read-eval-print loop
interactive, 278
invariant, 279280
    model checking of, 281282
        bounded, 283284
    violation, 285
iter, 286, 287, 288, 289, 290, 291, 292
iterated, see iter

kind, 294295
    canonical representation, 296
    metarepresentation, 297
Kripke structure, 298
    associated to a module, 299

label, 300, 301, 302
left id, 303, 304, 305, 306
linear temporal logic, 307
    model checking, see model checking
    satisfiability, 309
linear.maude, 310
list
    from set, 311312
    generalized, 313314
    of sets, 315
    parameterized, 316, 317318
        sorted, 319
    sortable, 320321
        strict weak order, 322
        total preorder, 323
ll, 324
load, 325, 326, 327
logic programming, 328329
    cut, 330
    negation as failure, 331
loop, 332
ls, 333
LTL, see linear temporal logic

machine-int.maude, 335
map, 336337
match, 338, 339
    metarepresentation, see descent function
matching, 341
    modulo, 342, 343344, 345, 346
        with extension, 347, 348
Maude-NPA, 349
MAUDE_LIB, 350, 351
mb, 352
membership, 353354, 355
    metarepresentation, 356
membership equational logic, 357, 358
memo, 359
memoization, 360361
    table size, 362
message, 363 (Full Maude)
message, 364, 365
metadata, 366, 367, 368, 369, 370
meta-interpreter.maude, 371
MiniMaude, 372373
Mobile Maude, 374
mod, 375, 376
model checker
    implementation, 377
    procedure, 378
model checking, 379380
    abstraction, 381382
    logical, 383, 384, 385
model-checker.maude, 386, 387, 388, 389, 390
module, 391392
    algebra, 393
    database, 394 (Full Maude)
    expression, 395, 396, see module operation
    functional, 398, 399400
        admissible, 401402
        initial model, 403
        mathematical semantics, 404, 405, 406, 407, 408
        operational semantics, 409, 410, 411
    hierarchy, see module importation
    importation, 413414, 415, 416, 417
        extending, 418419
        implicit, 420
        including, 421422
        protecting, 423424
    metarepresentation, 425
    object-based, 426427
        asynchronous, 428
        configuration, 429
        fairness, 430
        synchronous, 431
        uniqueness, 432
    object-oriented, 433 (Full Maude)
        as system module, 434 (Full Maude)
        operation, 435 (Full Maude)
        parameterized, 436 (Full Maude)
    operation, 437
        instantiation, 438, 439, 440, 441, 442443
        metarepresentation, 444
        power, 445 (Full Maude)
        renaming, 446, 447448, 449, 450
        summation, 451, 452453, 454
        tuple, 455 (Full Maude)
    parameterized, 456, 457458
        bound parameter, 459
        free parameter, 460
        interface, 461
        metarepresentation, 462
        parameter, 463, 464
        parameter label, 465
        parameter theory, 466, 467, 468, 469
    predefined, 470471
    signature, 472
        extended, see parsing
    strategy, 474
        importation, 475
        parameterized, 476
    system, 477, 478479
        admissible, 480
        initial model, 481
        mathematical semantics, 482, 483
        operational semantics, 484, 485
monoid, 486
    commutative, 487
monomial, 488
msg, see message
MTT, 490, 491, 492, 493, 494

narrowing, 495, 496, 497498
    based unification, 499500
    completeness, 501502
    folding variant, 503, 504, 505, 506
    modulo axioms, 507
    with extra variables, 508
    with rules, 509
    with simplification, 510511
narrowing, 512
no-advise, 513
no-ansi-color, 514
no-banner, 515
no-mixfix, 516
no-prelude, 517
no-tecla, 518
no-wrap, 519
nonexec, 520, 521, 522, 523, 524
number
    floating-point, 525526
    integer, 527528
    machine, 529530
    natural, 531532
    random, 533534
    rational, 535536
    string conversion, 537538

OBJ, 539, 540, 541
obj, see object
OBJ3, 543n, 544, 545, 546, 547, 548
object, 549, see module object-based, 551 (Full Maude)
object, 552, 553, 554
op, 555, 556
operation
    metalevel, see descent function
    partial, 558
    total, 559
operator, 560561, 562
    arity, 563
    at the kind level, 564, 565
    at the sort level, 566
    built-in, 567, 568
    coarity, 569
    derived, see view
    domain sort, see operator arity
    gathering, see parsing
    iterated, see iter
    mapping, 574, see view, 576
    metarepresentation, 577
    name
        empty syntax, 578
        mixfix form, 579
        prefix form, 580, 581
        several identifiers, 582
    overloaded, 583584, 585
        ad-hoc, 586
        subsort, 587, 588
    polymorphic, 589, 590
    precedence, see parsing
    range sort, see operator coarity
ops, 593
optimizing, 594, see debugger, profiler
otherwise, 596, 597598, 599
overloading, see operator overloaded
owise, see otherwise

parse, 602, 603
    metarepresentation, see descent function
parsing, 605606
    extended grammar, 607
    gathering, 608
        default pattern, 609
    precedence, 610
        default value, 611
        overridden, 612
pattern, 613
performance, 614615, 616
poly, see polymorphic
polymorphic, 618, 619, 620, 621
polynomial, 622, 623
popd, 624
pr, see protecting
prec, see precedence
precedence, 627, 628
prelude.maude, 629, 630, 631, 632, 633, 634, 635, 636, 637, 638
preregularity, 639, 640
    modulo, 641
print, 642, 643, 644, 645
print conceal, 646
print reveal, 647
print-to-stderr, 648
printing
    format, 649650
        color, 651
        space, 652
    metarepresentation, see descent function
probabilistic models, 654
profiler, 655656
profiling, 657, 658 (Full Maude)
protecting, 659, 660
pushd, 661
pwd, 662

q, see quit
qidlist
    string conversion, 664665
quit, 666, 667
quoted identifier, 668669

random-seed, 670, 671
reachability problem, 672
read-eval-print loop, 673
Real-Time Maude, 674
red, see reduce
reduce, 676, 677, 678, 679
    metarepresentation, see descent function
reflection, 681
    moving between levels, see descent function, 683 (Full Maude)
    tower of, 684
resume, 685 (debugger), 686 (debugger)
rew, see rewrite
rewrite condition, 688689
    rewrite expression, 690
    satisfaction, 691
rewrite rule, 692
    executable, 693
    meaning
        computational, 694
        logical, 695
    metarepresentation, 696
    object-oriented, 697 (Full Maude)
rewrite, 698, 699, 700, 701, 702, 703
    metarepresentation, see descent function
rewriting
    modulo, 705
    sharing, 706n
rewriting logic
    proof equivalence, 707
    reflective, 708
    rewrite proof, 709
right id, 710, 711, 712, 713
ring, 714
rl, 715

SAT problem, 716
SAT solver, 717
satisfiability module theories, see SMT
SCC, 719, 720, 721, 722
search, 723, 724
    metarepresentation, see descent function
    object-oriented, 726 (Full Maude)
searching, see search
segmentation fault, 728
select, 729, 730
semiring, 731
set
    from list, 732733
    generalized, 734735
    parameterized, 736737
    partially ordered, 738
    totally ordered, 739
set clear memo, 740
set break, 741, 742
set clear memo, 743
set clear profile, 744, 745
set clear rules, 746
set extend, 747, 748
set include, 749
set print, 750
set print attribute, 751
set print attribute newline, 752
set print color, 753
set print conceal, 754
set print constants with sorts, 755
set print flattened, 756
set print format, 757
set print graph, 758
set print mixfix, 759
set print number, 760, 761
set print parentheses, 762
set print rat, 763
set print rational, 764
set print with aliases, 765
set profile, 766, 767
set protect, 768, 769
set show advisories, 770
set show breakdown, 771
set show command, 772
set show gc, 773
set show loop stats, 774
set show loop timing, 775
set show stats, 776
set show timing, 777
set trace, 778, 779, 780, 781
set trace body, 782
set trace builtin, 783
set trace condition, 784
set trace eq, 785
set trace mb, 786
set trace rewrite, 787
set trace rl, 788
set trace sd, 789
set trace select, 790, 791, 792
set trace substitution, 793
set trace whole, 794
set verbose, 795
set print format, 796
show, 797
show all, 798
show components, 799, 800
show eqs, 801
show mbs, 802
show module, 803
show modules, 804
show ops, 805
show path, 806
show path labels, 807
show profile, 808, 809
show rls, 810, 811
show sds, 812
show search graph, 813, 814
show sorts, 815, 816
show strats, 817
show summary, 818
show vars, 819
show view, 820
show views, 821
simplicity, 822823
sload, 824, 825
smod, 826
SMT, 827828
SMT-LIB, 829830
    Core, 831
    Ints, 832
    Reals, 833
    Reals-Ints, 834
socket, 835836
    buffered, 837838
socket.maude, 839
sort, 840841
    error supersort, see kind
    least sort, 843, 844
    mapping, 845, see view
    metarepresentation, 847
    name collision, 848
    parameterized, 849, 850
    structured, 851
sort decreasingness, 852
sort, 853
sorts, 854
special, 855, 856
srew, see srewrite
srewrite, 858, 859, 860
    metarepresentation, see descent function
stack, 862 (Full Maude)
standard streams, 863864
Status report, 865866
step, 867 (debugger), 868 (debugger)
sth, 869
strat, 870
Stratego, 871
strategy
    internal, 872, 873874
    object-message fair, 875, 876877
    operator, 878879
        bottom-up, see eager
        default, 881
        eager, 882
        frozen, 883, 884885, 886, 887
        lazy, 888
        operator-by-operator, 889, 890
strategy language, 891892
    all, 893
    alternative, 894
    amatch, 895
    amatchrew, 896, 897
    concatenation, 898
    conditional, 899
    csd, 900
    disjunction, 901
    fail, 902
    idle, 903
    iteration, 904
    match, 905
    matchrew, 906
    metarepresentation, 907
    named strategies, 908
    named strategy
        mapping, 909
        overloaded, 910
    negation, 911
    non-void iteration, 912
    normalization, 913
    not, 914
    one, 915
    or-else, 916
    rule application, 917
        initial substitution, 918
        rewriting condition, 919
    sd, 920
    set-theoretic semantics, 921, 922
    strat, 923
    strategy call, 924
    strategy combinator, 925
    strategy declaration, 926
    strategy definition, 927
    strategy expression, 928
    strategy module, see module > strategy
    subject sort, 930
    test, 931
    test, 932
    top, 933
    try, 934
    xmatch, 935
    xmatchrew, 936
strategy, see strat
string, 938939
    number conversion, 940941
    qidlist conversion, 942943
submodule, 944, see module importation
subsort relation, 946947
    connected component, 948
    metarepresentation, 949
    partial order, 950
subsort, 951
subsorts, 952
substitution, 953
    well-sorted, 954
sufficient completeness, 955
supermodule, 956, see module importation
symbolic reachability analysis, 958959, 960, 961

tautology checker, 962
tecla, 963
term, 964965
    canonical form, 966, 967
        relative to strategy, 968
    coloring, 969970
    error, 971
    flattened, 972
    ground, 973, 974
    metarepresentation, 975
    qualified, 976
    undefined, 977
termination, 978
    context-sensitive, 979
    ground, 980
    modulo, 981
th, 982
theory, 983, 984985
    flat, 986, 987n
    functional, 988
        admissible, 989
        mathematical semantics, 990
        operational semantics, 991
    importation, 992
        including, 993, 994
    metarepresentation, 995
    object-oriented, 996 (Full Maude)
    predefined, 997998
    strategy, 999
    structured, see theory importation
    system, 1001
        admissible, 1002
        mathematical semantics, 1003
        operational semantics, 1004
token, 1005, 1006
trace deselect, 1007
trace exclude, 1008
trace include, 1009
trace select, 1010, 1011, 1012
tracing, 10131014, 1015, 1016 (Full Maude)

unification, 10171018
    E-unification, 1019
    algorithm, 1020
        endogenous, 1021
        exogenous, 1022
        order-sorted, 10231024
    associative, 10251026
    associative-commutative, 10271028
    associative-commutative-identity, 10291030
    combination, 10311032
    equational, 1033
    finitary, 1034
    hybrid approach, 1035
    identity, 10361037
    implementation, 10381039
    iter, 10401041
    narrowing-based, 10421043
    order-sorted, 10441045
    problem, 1046
    semantic, 1047
    syntactic, 1048
    unitary, 1049
    variant-based, 10501051
unifier, 1052
    E-unifier, 1053
    complete set, 1054
    most general, 1055
    semantic, 1056
unify, 10571058, 1059
    metarepresentation, see descent function
universal theory, 1061
Universal, 1062, 1063, 1064

var, 1065
    in views, 1066
variable, 10671068
    fresh, 1069, 1070, 1071, 1072, 1073, 1074, 1075, 1076
    in a module, 1077, 1078
    metarepresentation, 1079
    on-the-fly, 1080, 1081
variant, 1082, 10831084
    based unification, 10851086
        incremental, 1087
        with irreducibility constraints, 1088, 1089
    complete set, 1090
    finite variant property, 1091
    generation, 10921093
        incremental, 1094
        with irreducibility constraints, 1095, 1096, 1097
    satisfiability, 1098
variant, 1099
variant unify, 11001101, 1102
    metarepresentation, see descent function
vars, 1104
vector, 1105
version, 1106
view, 1107, 11081109, 1110
    between theories, 1111, 1112
    metarepresentation, 1113, 1114
    object-oriented, 1115 (Full Maude)
    parameterized, 1116
    predefined, 11171118
view, 1119
vu-narrow, 1120
    metarepresentation, see descent function

where, 1122 (debugger), 1123 (debugger)

xmatch, 1124, 1125, 1126, 1127
    metarepresentation, see descent function
xml-log, 1129

Yices2, 11301131