4180:
4104:
696:
6688:
6395:
6217:
489:
5007:
1843:
From the above examples, it is clear that we can think of rewriting systems in an abstract manner. We need to specify a set of objects and the rules that can be applied to transform them. The most general (unidimensional) setting of this notion is called an
3752:
6033:
451:) indicates that an expression matching the left hand side of the rule can be rewritten to one formed by the right hand side, and the symbols each denote a subexpression. In such a system, each rule is chosen so that the left side is
8017:
483:. For example, the numbers 0, 1, 2, and 3 are represented by the terms 0, S(0), S(S(0)), and S(S(S(0))), respectively. The following term rewriting system can then be used to compute sum and product of given natural numbers.
691:{\displaystyle {\begin{aligned}A+0&\to A&{\textrm {(1)}},\\A+S(B)&\to S(A+B)&{\textrm {(2)}},\\A\cdot 0&\to 0&{\textrm {(3)}},\\A\cdot S(B)&\to A+(A\cdot B)&{\textrm {(4)}}.\end{aligned}}}
2602:
2427:
2298:
8281:
3983:
5117:
6683:{\displaystyle {\begin{aligned}&f(g(0,1),g(0,1),g(0,1))\\\rightarrow &f(0,g(0,1),g(0,1))\\\rightarrow &f(0,1,g(0,1))\\\rightarrow &f(g(0,1),g(0,1),g(0,1))\\\rightarrow &\cdots \end{aligned}}}
7578:. This is the most recent comprehensive monograph. It uses however a fair deal of non-yet-standard notations and definitions. For instance, the Church–Rosser property is defined to be identical with confluence.
3388:
455:
to the right side, and consequently when the left side matches a subexpression, performing a rewrite of that subexpression from left to right maintains logical consistency and value of the entire expression.
3685:
3646:
3538:
3498:
5346:
5281:
3338:
426:
5645:
343:
5212:
5149:
3614:
3300:
3163:
1650:
4932:
268:
209:
6400:
6038:
494:
6000:
5909:
5798:
5575:
4313:
2335:
2072:
2003:
4837:
2922:
2173:
1551:
1442:
1309:
1191:
1016:
911:
806:
4870:
4046:
1400:
5399:
5243:
5180:
3466:
3237:
3090:
2803:
6290:
1908:
1823:
5464:
2535:
2505:
1267:
3439:
2973:
1765:
6385:
6340:
1149:
974:
869:
4804:
4134:
3838:
2889:
1509:
1952:
150:
7132:
5707:
1612:
764:
8343:
4530:
4482:
3898:
3803:
2206:
2118:
1708:
1074:
2453:
2361:
2236:
4003:
2027:
1976:
1932:
4086:
3870:
3779:
3190:
3117:
2850:
2729:
4388:
80:. One rule to rewrite a term could be applied in many different ways to that term, or more than one rule could be applicable. Rewriting systems then do not provide an
7070:
4703:
4629:
4580:
4414:
4362:
4222:
4174:
3933:
2749:
6862:
6835:
6800:
6773:
6746:
6719:
5065:
5034:
4927:
4900:
3693:
3037:
3005:
449:
5307:
4416:. Also present in the rules are variables, which represent any possible term (though a single variable always represents the same term throughout a single rule).
3063:
84:
for changing one term to another, but a set of possible rule applications. When combined with an appropriate algorithm, however, rewrite systems can be viewed as
5818:
5484:
5368:
4771:
4751:
4723:
4683:
4600:
4154:
3582:
3562:
3257:
3210:
2823:
2769:
2686:
5800:, which is the result term of applying the rewrite rule. Altogether, applying the rewrite rule has achieved what is called "applying the associativity law for
7696:
6212:{\displaystyle {\begin{aligned}f(x,x)&\rightarrow g(x),\\f(x,g(x))&\rightarrow b,\\h(c,x)&\rightarrow f(h(x,c),h(x,x)).\\\end{aligned}}}
6023:
left-hand side is undecidable. Termination is also undecidable for systems using only unary function symbols; however, it is decidable for finite
2548:
2386:
2257:
8219:
7890:
3938:
2006:
6952:
8198:
8070:
8027:
7545:
5070:
8383:
3343:
8490:
3658:
3619:
3511:
3471:
8425:
8287:
7857:
7773:
7737:
7607:
7575:
6887:, allowing higher order functions and bound variables. Various results about first-order TRSs can be reformulated for HRSs as well.
5313:
5248:
3305:
354:
8310:
5580:
274:
5185:
5122:
3587:
3273:
3122:
2125:
93:
8458:
1616:
7635:
4419:
In contrast to string rewriting systems, whose objects are sequences of symbols, the objects of a term rewriting system form a
2616:
2364:
1783:, expressing the fact that A can be replaced by X in generating the constituent structure of a sentence. For example, the rule
7597:
8146:
6872:
5002:{\displaystyle t_{1}{\underset {R}{\rightarrow }}t_{2}{\underset {R}{\rightarrow }}\cdots {\underset {R}{\rightarrow }}t_{n}}
7670:
4179:
4103:
220:
161:
5911:" in elementary algebra. Alternately, the rule could have been applied to the denominator of the original term, yielding
7753:
5914:
5823:
5712:
5489:
4227:
2307:
2044:
1911:
8495:
2665:
1981:
153:
77:
4809:
2894:
2301:
2139:
1513:
1404:
1271:
1153:
978:
873:
768:
4842:
4016:
1313:
8500:
5377:
5221:
5158:
4053:
3444:
3215:
3068:
2781:
2627:
2030:
1737:, as a means of generating the grammatically correct sentences of a language. Such a rule typically takes the form
31:
6227:
1886:
1829:(VP); further rules will specify what sub-constituents a noun phrase and a verb phrase can consist of, and so on.
8485:
6012:
2661:
1838:
1786:
89:
73:). In their most basic form, they consist of a set of objects, plus relations on how to transform those objects.
5407:
2510:
2478:
117:(CNF) of a formula can be implemented as a rewriting system. The rules of an example of such a system would be:
7838:"Proving and Rewriting" International Conference on Algebraic and Logic Programming, 1990 Nancy, France pp 1-24
6963:
3652:
1195:
7647:
7805:
3393:
2927:
2643:
1740:
114:
8060:
8043:
Jürgen
Avenhaus; Klaus Madlener (1990). "Term Rewriting and Equational Reasoning". In R.B. Banerji (ed.).
7704:
Jürgen
Avenhaus and Klaus Madlener. "Term rewriting and equational reasoning". In Ranan B. Banerji (Ed.),
6346:
6301:
1776:
1092:
4091:
The word problem for a semi-Thue system is undecidable in general; this result is sometimes known as the
915:
810:
8375:
7585:
6942:
5215:
4776:
4113:
3812:
2855:
1726:
3903:
We immediately get some very useful connections with other areas of algebra. For example, the alphabet
1446:
6016:. For term rewriting systems in particular, the following additional subtleties are to be considered.
1937:
123:
8249:
7801:
7650:(1980) Stanford Verification Group, Report N° 15 Computer Science Department Report N° STAN-CS-80-785
7075:
6899:
5650:
4560:
3505:
1555:
707:
7849:
7766:
Computability, Complexity, and
Languages: Fundamentals of Theoretical Computer Science – 2nd edition
7563:
4509:
4461:
4423:. A term can be visualized as a tree of symbols, the set of admitted symbols being fixed by a given
3879:
3784:
2186:
2097:
1654:
1020:
7983:
Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Quesada, J.F. (2002).
6969:
6911:
4432:
3873:
3501:
2631:
2432:
2340:
2215:
701:
For example, the computation of 2+2 to result in 4 can be duplicated by term rewriting as follows:
452:
212:
54:
7687:
3988:
2012:
1961:
1917:
8431:
7882:
7729:
7691:
7626:
5466:
is a rewrite rule, commonly used to establish a normal form with respect to the associativity of
5152:
4059:
3843:
3757:
3260:
3168:
3095:
2828:
2702:
1768:
1734:
477:
7555:
7757:
4367:
8421:
8368:
8066:
8023:
7874:
7769:
7761:
7603:
7581:
7571:
7541:
6691:
4424:
3747:{\displaystyle {\mathcal {M}}_{R}=\Sigma ^{*}/{\overset {*}{\underset {R}{\leftrightarrow }}}}
2692:
strings in the alphabet that contain left- and respectively right-hand sides of some rules as
2623:
1955:
7797:
7037:
6883:
Higher-order rewriting systems are a generalization of first-order term rewriting systems to
4688:
4614:
4565:
4393:
4341:
4189:
4159:
4088:, i.e. it may always be presented by a semi-Thue system, possibly over an infinite alphabet.
3906:
2734:
8413:
8333:
8325:
8228:
7996:
7960:
7927:
7866:
6974:
4338:
above is a term rewriting system. The terms in this system are composed of binary operators
85:
42:
6840:
6813:
6778:
6751:
6724:
6697:
5043:
5012:
4905:
4878:
3010:
2978:
8176:
8172:
7657:
7653:
7630:
7592:
7559:
6895:
6030:
The following term rewrite system is normalizing, but not terminating, and not confluent:
5647:, see picture 2. Applying that substitution to the rule's right-hand side yields the term
4049:
1861:
434:
8277:
5286:
4332:, which are expressions with nested sub-expressions. For example, the system shown under
3042:
7815:
7622:
7718:
7643:
7618:
7588:
6930:
5803:
5469:
5353:
4756:
4736:
4708:
4668:
4585:
4428:
4139:
3567:
3547:
3242:
3195:
2808:
2754:
2671:
465:
346:
8278:"Relating Innermost, Weak, Uniform, and Modular Termination of Term Rewriting Systems"
8001:
7984:
7965:
7948:
6925:
provides a means for discussing multiprocessing in more formal terms, such as via the
2626:(a terminating ARS is confluent if and only if it is locally confluent), and that the
8479:
8450:
8329:
8233:
8214:
7932:
7915:
7835:
7683:
7679:
7661:
7533:
6868:
3688:
2771:
is a binary relation between some (fixed) strings in the alphabet, called the set of
8435:
8183:. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320.
7886:
7614:
of this chapter is freely available from the authors, but it is missing the figures.
8195:
Max
Dauchet (1989). "Simulation of Turing Machines by a Left-Linear Rewrite Rule".
7529:
6926:
6922:
6907:
6803:
6221:
The following two examples of terminating term rewrite systems are due to Toyama:
6024:
6020:
4650:
4603:
4550:
4546:
4455:
4420:
4328:
4006:
473:
469:
17:
8283:
Proc. International
Conference on Logic Programming and Automated Reasoning (LPAR)
8135:
3508:(by definition) and it is also compatible with string concatenation. The relation
3165:
fits the definition of an abstract rewriting system. Since the empty string is in
7665:
6903:
6884:
2657:
1826:
1772:
1722:
38:
7914:
Hsiang, Jieh; Kirchner, Hélène; Lescanne, Pierre; Rusinowitch, Michaël (1992).
7870:
6875:
for ordering relations used in termination proofs for term rewriting systems.
4010:
3806:
8417:
8311:"Counterexamples to Termination for the Direct Sum of Term Rewriting Systems"
7878:
4056:
for monoids and groups. In fact, every monoid has a presentation of the form
4444:
2693:
1883:
Many notions and notations can be defined in the general setting of an ARS.
81:
464:
Term rewriting systems can be employed to compute arithmetic operations on
2597:{\displaystyle x_{0}\rightarrow x_{1}\rightarrow x_{2}\rightarrow \cdots }
2422:{\displaystyle x{\overset {*}{\leftarrow }}w{\overset {*}{\rightarrow }}y}
2293:{\displaystyle x{\overset {*}{\rightarrow }}z{\overset {*}{\leftarrow }}y}
7611:
6957:
6947:
3978:{\displaystyle \{ab\rightarrow \varepsilon ,ba\rightarrow \varepsilon \}}
1780:
4052:. Thus semi-Thue systems constitute a natural framework for solving the
8338:
7792:
6993:
This variant of the previous rule is needed since the commutative law
1825:
means that a sentence can consist of a noun phrase (NP) followed by a
8455:
Automated
Deduction - A Basis for Applications. Volume I: Foundations
7818:— a software implementation of a generic term rewriting system.
7810:
7362:) can be rewritten any further, therefore the system is not confluent
6694:, who claimed that the union of two terminating term rewrite systems
5112:{\displaystyle t_{1}{\overset {+}{\underset {R}{\rightarrow }}}t_{n}}
2615:
Important theorems for abstract rewriting systems are that an ARS is
7697:
Handbook of Logic in
Artificial Intelligence and Logic Programming
5370:
of rules can be viewed as an abstract rewriting system as defined
4635:. The subterm matching the left hand side of the rule is called a
4178:
4102:
2697:
2208:. If every object has at least one normal form, the ARS is called
110:
46:
6898:
are another generalization of term rewrite systems, operating on
3383:{\displaystyle uxv{\overset {*}{\underset {R}{\rightarrow }}}uyv}
6010:
Termination issues of rewrite systems in general are handled in
4427:. As a formalism, term rewriting systems have the full power of
3651:
The notion of a semi-Thue system essentially coincides with the
1713:
where the last step comprises the previous example computation.
3680:{\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}
3641:{\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}
3533:{\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}
3493:{\displaystyle {\overset {*}{\underset {R}{\leftrightarrow }}}}
7034:
since applying that substitution to the rule's left hand side
2619:
7787:
5341:{\displaystyle s{\overset {+}{\underset {R}{\rightarrow }}}t}
5276:{\displaystyle s{\overset {*}{\underset {R}{\rightarrow }}}t}
3333:{\displaystyle x{\overset {*}{\underset {R}{\rightarrow }}}y}
421:{\displaystyle A\lor (B\land C)\to (A\lor B)\land (A\lor C),}
5640:{\displaystyle \{x\mapsto a,\;y\mapsto a+1,\;z\mapsto a+2\}}
4110:
Schematic triangle diagram of application of a rewrite rule
3885:
3819:
3790:
3700:
338:{\displaystyle (A\land B)\lor C\to (A\lor C)\land (B\lor C)}
6864:. All these properties are satisfied by Toyama's examples.
6019:
Termination even of a system consisting of one rule with a
5207:{\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}
5144:{\displaystyle {\overset {+}{\underset {R}{\rightarrow }}}}
3609:{\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}
3441:. Similarly, the reflexive transitive symmetric closure of
3295:{\displaystyle {\overset {*}{\underset {R}{\rightarrow }}}}
3158:{\displaystyle (\Sigma ^{*},{\underset {R}{\rightarrow }})}
7916:"The term rewriting approach to automated theorem proving"
7706:
Formal
Techniques in Artificial Intelligence: A Sourcebook
1645:{\displaystyle \;\;{\stackrel {\textrm {s.a.}}{\to }}\;\;}
53:
covers a wide range of methods of replacing subterms of a
8251:
On the
Uniform Halting Problem for Term Rewriting Systems
8215:"Simulation of Turing machines by a regular rewrite rule"
7985:"Maude: Specification and programming in rewriting logic"
7978:
7976:
6933:. Rewriting can be performed in trace systems as well.
5486:. That rule can be applied at the numerator in the term
8084:
8082:
1086:
As another example, the computation of 2⋅2 looks like:
468:. To this end, each such number has to be encoded as a
7848:
Sculthorpe, Neil; Frisby, Nicolas; Gill, Andy (2014).
3302:
is compatible with the monoid operation, meaning that
7078:
7040:
6843:
6816:
6781:
6754:
6727:
6700:
6398:
6349:
6304:
6230:
6036:
6013:
Abstract rewriting system#Termination and convergence
5917:
5826:
5806:
5715:
5653:
5583:
5492:
5472:
5410:
5380:
5356:
5316:
5289:
5251:
5224:
5188:
5161:
5125:
5073:
5046:
5015:
4935:
4908:
4881:
4845:
4812:
4779:
4759:
4739:
4711:
4691:
4671:
4617:
4588:
4568:
4512:
4464:
4396:
4370:
4344:
4230:
4192:
4162:
4142:
4116:
4062:
4019:
3991:
3941:
3909:
3882:
3846:
3815:
3787:
3760:
3696:
3661:
3622:
3590:
3570:
3550:
3514:
3474:
3447:
3396:
3346:
3308:
3276:
3245:
3218:
3198:
3171:
3125:
3098:
3071:
3045:
3013:
2981:
2930:
2897:
2858:
2831:
2811:
2784:
2757:
2737:
2705:
2674:
2551:
2513:
2481:
2435:
2389:
2343:
2310:
2260:
2218:
2189:
2142:
2100:
2047:
2015:
1984:
1964:
1940:
1920:
1889:
1789:
1743:
1657:
1619:
1558:
1516:
1449:
1407:
1316:
1274:
1198:
1156:
1095:
1023:
981:
918:
876:
813:
771:
710:
492:
437:
357:
277:
223:
164:
126:
7025:
would cause the rewrite system to be nonterminating.
263:{\displaystyle \neg (A\lor B)\to \neg A\land \neg B}
204:{\displaystyle \neg (A\land B)\to \neg A\lor \neg B}
8382:. LNCS. Vol. 220. Springer. pp. 180–224.
8286:. LNAI. Vol. 624. Springer. pp. 285–296.
8202:. LNCS. Vol. 355. Springer. pp. 109–120.
7949:"Theory and practice of constraint handling rules"
7142:i.e. for each term, some normal form exists, e.g.
7126:
7064:
7009:cannot be turned into a rewrite rule. A rule like
6856:
6829:
6794:
6767:
6740:
6713:
6682:
6379:
6334:
6284:
6211:
5995:{\displaystyle {\frac {a*((a+1)*(a+2))}{(1*2)*3}}}
5994:
5904:{\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}
5903:
5812:
5793:{\displaystyle {\frac {(a*(a+1))*(a+2)}{1*(2*3)}}}
5792:
5709:, and replacing the numerator by that term yields
5701:
5639:
5570:{\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}
5569:
5478:
5458:
5393:
5362:
5340:
5301:
5275:
5237:
5206:
5174:
5143:
5111:
5059:
5028:
5001:
4921:
4894:
4864:
4831:
4798:
4765:
4745:
4717:
4697:
4677:
4623:
4594:
4574:
4524:
4476:
4408:
4382:
4356:
4308:{\displaystyle {\frac {a*((a+1)*(a+2))}{1*(2*3)}}}
4307:
4216:
4168:
4148:
4128:
4080:
4040:
3997:
3977:
3927:
3892:
3864:
3832:
3797:
3773:
3746:
3679:
3640:
3608:
3576:
3556:
3532:
3492:
3460:
3433:
3382:
3332:
3294:
3251:
3231:
3204:
3184:
3157:
3111:
3084:
3057:
3031:
2999:
2967:
2916:
2883:
2844:
2817:
2797:
2763:
2743:
2723:
2680:
2596:
2529:
2499:
2447:
2421:
2355:
2330:{\displaystyle x{\overset {*}{\leftrightarrow }}y}
2329:
2292:
2230:
2200:
2167:
2112:
2067:{\displaystyle x{\overset {*}{\leftrightarrow }}y}
2066:
2021:
1997:
1970:
1946:
1926:
1902:
1817:
1759:
1702:
1644:
1606:
1545:
1503:
1436:
1394:
1303:
1261:
1185:
1143:
1068:
1010:
968:
905:
863:
800:
758:
690:
443:
420:
337:
262:
203:
144:
57:with other terms. Such methods may be achieved by
8451:"Higher-Order Rewriting and Equational Reasoning"
7680:"Equational reasoning and term rewriting systems"
7673:, Volume 2: Background: Computational Structures
4443:"Redex" redirects here. For the medication, see
4013:on one generator. If instead the rules are just
1998:{\displaystyle {\overset {*}{\leftrightarrow }}}
27:Replacing subterm in a formula with another term
6748:is again terminating if all left-hand sides of
6390:Their union is a non-terminating system, since
5371:
4832:{\displaystyle s{\underset {R}{\rightarrow }}t}
4649:of this rule application is then the result of
2917:{\displaystyle s{\underset {R}{\rightarrow }}t}
2168:{\displaystyle x{\stackrel {*}{\rightarrow }}y}
1546:{\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}
1437:{\displaystyle \;\;{\stackrel {(3)}{\to }}\;\;}
1304:{\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}
1186:{\displaystyle \;\;{\stackrel {(4)}{\to }}\;\;}
1011:{\displaystyle \;\;{\stackrel {(1)}{\to }}\;\;}
906:{\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}
801:{\displaystyle \;\;{\stackrel {(2)}{\to }}\;\;}
472:. The simplest encoding is the one used in the
8412:. Cambridge University Press. pp. 47–50.
7570:("TeReSe"), Cambridge University Press, 2003,
4902:can be rewritten in several steps into a term
4865:{\displaystyle s{\overset {R}{\rightarrow }}t}
4041:{\displaystyle \{ab\rightarrow \varepsilon \}}
1395:{\displaystyle S(S(0))+S(S(0))+S(S(0))\cdot 0}
8019:Programming with Constraints: An Introduction
7728:Benjamin Benninghofen, Susanne Kemmerich and
5394:{\displaystyle {\underset {R}{\rightarrow }}}
5238:{\displaystyle {\underset {R}{\rightarrow }}}
5175:{\displaystyle {\underset {R}{\rightarrow }}}
3461:{\displaystyle {\underset {R}{\rightarrow }}}
3232:{\displaystyle {\underset {R}{\rightarrow }}}
3085:{\displaystyle {\underset {R}{\rightarrow }}}
2798:{\displaystyle {\underset {R}{\rightarrow }}}
2183:is unique, then this is usually denoted with
8:
8449:Nipkow, Tobias; Prehofer, Christian (1998).
8045:Formal Techniques in Artificial Intelligence
6285:{\displaystyle f(0,1,x)\rightarrow f(x,x,x)}
5634:
5584:
4035:
4020:
3972:
3942:
3922:
3910:
2604:. A confluent and terminating ARS is called
1903:{\displaystyle {\overset {*}{\rightarrow }}}
8124:Dershowitz, Jouannaud (1990), sect.1, p.245
7371:i.e., there are infinite derivations, e.g.
6960:specify rewriting that is done in parallel.
4611:is the result of applying the substitution
4435:can be defined by a term rewriting system.
1818:{\displaystyle {\rm {S\rightarrow NP\ VP}}}
1079:where the rule numbers are given above the
5618:
5599:
5459:{\displaystyle x*(y*z)\rightarrow (x*y)*z}
4326:) is a rewriting system whose objects are
2530:{\displaystyle x{\mathbin {\downarrow }}y}
2500:{\displaystyle x\leftarrow w\rightarrow y}
1641:
1640:
1621:
1620:
1542:
1541:
1518:
1517:
1433:
1432:
1409:
1408:
1300:
1299:
1276:
1275:
1182:
1181:
1158:
1157:
1007:
1006:
983:
982:
959:
931:
902:
901:
878:
877:
857:
820:
797:
796:
773:
772:
8337:
8232:
8000:
7964:
7931:
7656:. "Term Rewriting Systems", Chapter 1 in
7077:
7039:
6848:
6842:
6821:
6815:
6786:
6780:
6759:
6753:
6732:
6726:
6705:
6699:
6399:
6397:
6348:
6303:
6229:
6037:
6035:
5918:
5916:
5827:
5825:
5805:
5716:
5714:
5652:
5582:
5493:
5491:
5471:
5409:
5381:
5379:
5355:
5320:
5315:
5288:
5255:
5250:
5225:
5223:
5189:
5187:
5162:
5160:
5126:
5124:
5103:
5084:
5078:
5072:
5051:
5045:
5020:
5014:
4993:
4979:
4966:
4960:
4946:
4940:
4934:
4913:
4907:
4886:
4880:
4849:
4844:
4816:
4811:
4787:
4778:
4758:
4738:
4710:
4690:
4670:
4616:
4587:
4567:
4511:
4463:
4395:
4369:
4343:
4231:
4229:
4191:
4161:
4141:
4115:
4061:
4018:
3990:
3940:
3908:
3884:
3883:
3881:
3845:
3824:
3818:
3817:
3814:
3789:
3788:
3786:
3765:
3759:
3729:
3724:
3718:
3705:
3699:
3698:
3695:
3662:
3660:
3623:
3621:
3591:
3589:
3569:
3549:
3515:
3513:
3475:
3473:
3448:
3446:
3425:
3395:
3356:
3345:
3312:
3307:
3277:
3275:
3244:
3219:
3217:
3197:
3176:
3170:
3142:
3133:
3124:
3103:
3097:
3072:
3070:
3044:
3012:
2980:
2959:
2929:
2901:
2896:
2875:
2857:
2836:
2830:
2810:
2785:
2783:
2756:
2736:
2704:
2673:
2582:
2569:
2556:
2550:
2518:
2517:
2512:
2480:
2434:
2406:
2393:
2388:
2342:
2314:
2309:
2277:
2264:
2259:
2217:
2193:
2188:
2154:
2149:
2147:
2146:
2141:
2099:
2051:
2046:
2014:
1985:
1983:
1963:
1939:
1919:
1890:
1888:
1791:
1790:
1788:
1745:
1744:
1742:
1656:
1631:
1630:
1625:
1623:
1622:
1618:
1557:
1527:
1522:
1520:
1519:
1515:
1448:
1418:
1413:
1411:
1410:
1406:
1315:
1285:
1280:
1278:
1277:
1273:
1262:{\displaystyle S(S(0))+S(S(0))\cdot S(0)}
1197:
1167:
1162:
1160:
1159:
1155:
1094:
1022:
992:
987:
985:
984:
980:
917:
887:
882:
880:
879:
875:
812:
782:
777:
775:
774:
770:
709:
675:
674:
613:
612:
578:
577:
519:
518:
493:
491:
476:, based on the constant 0 (zero) and the
436:
356:
276:
222:
163:
125:
8257:(Technical report). IRIA. p. 8. 283
8143:Papers by Nachum Dershowitz and students
7600:, Volume B: Formal Models and Semantics.
7598:Handbook of Theoretical Computer Science
1779:, and X is a sequence of such labels or
8248:Gerard Huet, D.S. Lankford (Mar 1978).
8016:Kim Marriott; Peter J. Stuckey (1998).
7828:
6986:
4490:can be replaced by the right-hand side
4048:, then we obtain a presentation of the
8047:. Sourcebook. Elsevier. pp. 1–43.
7850:"The Kansas University rewrite engine"
6690:This result disproves a conjecture of
4705:applied, see picture 1. In this case,
4484:, to indicate that the left-hand side
4156:in a term, with matching substitution
3434:{\displaystyle x,y,u,v\in \Sigma ^{*}}
2968:{\displaystyle x,y,u,v\in \Sigma ^{*}}
2179:is irreducible. If the normal form of
2007:reflexive transitive symmetric closure
1760:{\displaystyle {\rm {A\rightarrow X}}}
8199:Rewriting Techniques and Applications
8115:Martin Davis et al. 1994, p. 178
7671:Handbook of Logic in Computer Science
7648:Equations and Rewrite Rules, A Survey
7:
8453:. In Bibel, W.; Schmitt, P. (eds.).
6380:{\displaystyle g(x,y)\rightarrow y.}
6335:{\displaystyle g(x,y)\rightarrow x,}
3781:by the Thue congruence. If a monoid
2751:is a (usually finite) alphabet, and
1144:{\displaystyle S(S(0))\cdot S(S(0))}
8152:from the original on 15 August 2021
8145:. Tel Aviv University. p. 12.
3687:is a congruence, we can define the
3616:coincides with the Thue congruence
3584:is symmetric, the rewrite relation
2696:. Formally a semi-Thue system is a
2622:it has the Church–Rosser property,
969:{\displaystyle S(S(\;S(S(0))+0\;))}
864:{\displaystyle S(\;S(S(0))+S(0)\;)}
4799:{\displaystyle s\rightarrow _{R}t}
4400:
4129:{\displaystyle l\longrightarrow r}
4066:
3850:
3833:{\displaystyle {\mathcal {M}}_{R}}
3762:
3715:
3422:
3173:
3130:
3100:
2956:
2884:{\displaystyle s,t\in \Sigma ^{*}}
2872:
2833:
2738:
2709:
1810:
1807:
1801:
1798:
1792:
1752:
1746:
254:
245:
224:
195:
186:
165:
130:
127:
113:, the procedure for obtaining the
25:
7858:Journal of Functional Programming
6953:Knuth–Bendix completion algorithm
3270:In a SRS, the reduction relation
2033:for an ARS is determining, given
1504:{\displaystyle S(S(0))+S(S(0))+0}
94:declarative programming languages
8062:Foundations of Generative Syntax
8049:Here: Example in sect.4.1, p.24.
7953:The Journal of Logic Programming
7920:The Journal of Logic Programming
7602:, Elsevier and MIT Press, 1990,
5374:, with terms as its objects and
5350:A term rewriting given by a set
2668:to extend a rewriting relation,
2300:. An ARS is said to possess the
1947:{\displaystyle \leftrightarrow }
145:{\displaystyle \neg \neg A\to A}
8461:from the original on 2021-08-16
8389:from the original on 2013-11-12
8349:from the original on 2019-11-13
8290:from the original on 2016-03-04
7896:from the original on 2017-09-22
7636:Handbook of Automated Reasoning
7127:{\displaystyle a*((a+1)*(a+2))}
5702:{\displaystyle (a*(a+1))*(a+2)}
5577:with the matching substitution
5119:. In other words, the relation
1607:{\displaystyle S(S(0))+S(S(0))}
759:{\displaystyle S(S(0))+S(S(0))}
8276:Bernhard Gramlich (Jun 1993).
7610:, pp. 243–320. The
7540:. Cambridge University Press.
7121:
7118:
7106:
7100:
7088:
7085:
7059:
7047:
6879:Higher-order rewriting systems
6873:Path ordering (term rewriting)
6666:
6659:
6656:
6644:
6635:
6623:
6614:
6602:
6596:
6588:
6581:
6578:
6566:
6548:
6540:
6533:
6530:
6518:
6509:
6497:
6485:
6477:
6470:
6467:
6455:
6446:
6434:
6425:
6413:
6407:
6368:
6365:
6353:
6323:
6320:
6308:
6279:
6261:
6255:
6252:
6234:
6199:
6196:
6184:
6175:
6163:
6157:
6151:
6144:
6132:
6116:
6109:
6106:
6100:
6088:
6075:
6069:
6063:
6056:
6044:
5980:
5968:
5963:
5960:
5948:
5942:
5930:
5927:
5895:
5883:
5872:
5869:
5857:
5851:
5839:
5836:
5784:
5772:
5761:
5749:
5743:
5740:
5728:
5719:
5696:
5684:
5678:
5675:
5663:
5654:
5622:
5603:
5590:
5561:
5549:
5538:
5535:
5523:
5517:
5505:
5502:
5447:
5435:
5432:
5429:
5417:
5383:
5323:
5258:
5227:
5192:
5164:
5129:
5087:
4981:
4968:
4948:
4851:
4818:
4784:
4525:{\displaystyle l\rightarrow r}
4516:
4477:{\displaystyle l\rightarrow r}
4468:
4403:
4397:
4377:
4371:
4351:
4345:
4299:
4287:
4276:
4273:
4261:
4255:
4243:
4240:
4211:
4199:
4120:
4075:
4063:
4029:
3966:
3951:
3893:{\displaystyle {\mathcal {M}}}
3859:
3847:
3798:{\displaystyle {\mathcal {M}}}
3732:
3665:
3626:
3594:
3518:
3478:
3450:
3359:
3315:
3280:
3263:, then the system is called a
3221:
3152:
3144:
3126:
3074:
2903:
2787:
2718:
2706:
2588:
2575:
2562:
2545:if there is no infinite chain
2519:
2491:
2485:
2439:
2408:
2395:
2347:
2316:
2279:
2266:
2222:
2201:{\displaystyle x{\downarrow }}
2194:
2150:
2113:{\displaystyle x\rightarrow y}
2104:
2053:
2016:
1987:
1965:
1941:
1921:
1892:
1795:
1749:
1733:, are used in some systems of
1703:{\displaystyle S(S(S(S(0)))),}
1694:
1691:
1688:
1685:
1679:
1673:
1667:
1661:
1626:
1601:
1598:
1592:
1586:
1577:
1574:
1568:
1562:
1534:
1528:
1523:
1492:
1489:
1483:
1477:
1468:
1465:
1459:
1453:
1425:
1419:
1414:
1383:
1380:
1374:
1368:
1359:
1356:
1350:
1344:
1335:
1332:
1326:
1320:
1292:
1286:
1281:
1256:
1250:
1241:
1238:
1232:
1226:
1217:
1214:
1208:
1202:
1174:
1168:
1163:
1138:
1135:
1129:
1123:
1114:
1111:
1105:
1099:
1069:{\displaystyle S(S(S(S(0)))),}
1060:
1057:
1054:
1051:
1045:
1039:
1033:
1027:
999:
993:
988:
963:
960:
950:
947:
941:
935:
928:
922:
894:
888:
883:
858:
854:
848:
839:
836:
830:
824:
817:
789:
783:
778:
753:
750:
744:
738:
729:
726:
720:
714:
669:
657:
648:
641:
635:
604:
572:
560:
554:
547:
541:
510:
438:
412:
400:
394:
382:
379:
376:
364:
332:
320:
314:
302:
299:
290:
278:
242:
239:
227:
183:
180:
168:
136:
1:
8280:. In Voronkov, Andrei (ed.).
8002:10.1016/S0304-3975(01)00359-0
7966:10.1016/S0743-1066(98)10005-5
6810:" between left-hand sides of
2448:{\displaystyle x\downarrow y}
2356:{\displaystyle x\downarrow y}
2231:{\displaystyle x\downarrow y}
96:are based on term rewriting.
8457:. Kluwer. pp. 399–430.
8330:10.1016/0020-0190(87)90122-0
8234:10.1016/0304-3975(92)90022-8
8220:Theoretical Computer Science
8022:. MIT Press. pp. 436–.
7989:Theoretical Computer Science
7933:10.1016/0743-1066(92)90047-7
5216:reflexive-transitive closure
4559:, that is, if there is some
3998:{\displaystyle \varepsilon }
3840:, then the semi-Thue system
3564:. In a Thue system, i.e. if
2132:is called a "normal form of
2022:{\displaystyle \rightarrow }
1971:{\displaystyle \rightarrow }
1927:{\displaystyle \rightarrow }
1912:reflexive transitive closure
1860:of objects, together with a
8410:The Clausal Theory of Types
7538:Term rewriting and all that
5182:; often, also the notation
4081:{\displaystyle (\Sigma ,R)}
4009:, is a presentation of the
3865:{\displaystyle (\Sigma ,R)}
3774:{\displaystyle \Sigma ^{*}}
3185:{\displaystyle \Sigma ^{*}}
3112:{\displaystyle \Sigma ^{*}}
2845:{\displaystyle \Sigma ^{*}}
2777:one-step rewriting relation
2724:{\displaystyle (\Sigma ,R)}
2086:if there exists some other
154:double negation elimination
8517:
4442:
4334:
2641:
1856:). An ARS is simply a set
1836:
1833:Abstract rewriting systems
32:Rewriting (disambiguation)
29:
8491:Logic in computer science
8309:Yoshihito Toyama (1987).
7871:10.1017/S0956796814000185
7743:, Springer-Verlag (1987).
5401:as its rewrite relation.
4582:such that the subterm of
4383:{\displaystyle (\wedge )}
2120:; otherwise it is called
1850:abstract rewriting system
1846:abstract reduction system
1839:Abstract rewriting system
8418:10.1017/CBO9780511569906
8213:Max Dauchet (Sep 1992).
8197:Proc. 3rd Int. Conf. on
8136:"Term Rewriting Systems"
7947:Frühwirth, Thom (1998).
7798:Researchers in rewriting
7723:String-Rewriting Systems
6964:Referential transparency
6837:and right-hand sides of
6775:and right-hand sides of
3653:presentation of a monoid
2638:String rewriting systems
8408:Wolfram, D. A. (1993).
8059:Robert Freidin (1992).
7806:University of Innsbruck
7154:) has the normal forms
7065:{\displaystyle x*(y*z)}
6918:Trace rewriting systems
6891:Graph rewriting systems
4698:{\displaystyle \sigma }
4624:{\displaystyle \sigma }
4575:{\displaystyle \sigma }
4409:{\displaystyle (\neg )}
4390:and the unary operator
4357:{\displaystyle (\vee )}
4217:{\displaystyle x*(y*z)}
4169:{\displaystyle \sigma }
3928:{\displaystyle \{a,b\}}
2744:{\displaystyle \Sigma }
2650:string rewriting system
2644:String rewriting system
2537:. An ARS is said to be
2459:if and only if for all
2254:with the property that
115:conjunctive normal form
8367:N. Dershowitz (1985).
8185:; here: Sect. 2.3
7793:IFIP Working Group 1.6
7617:Nachum Dershowitz and
7568:Term Rewriting Systems
7128:
7066:
6910:/ their corresponding
6858:
6831:
6796:
6769:
6742:
6715:
6684:
6381:
6336:
6286:
6213:
5996:
5905:
5814:
5794:
5703:
5641:
5571:
5480:
5460:
5395:
5364:
5342:
5303:
5277:
5239:
5214:is used to denote the
5208:
5176:
5145:
5113:
5067:, formally denoted as
5061:
5030:
5003:
4923:
4896:
4866:
4833:
4800:
4773:, formally denoted as
4767:
4747:
4719:
4699:
4685:with the substitution
4679:
4625:
4596:
4576:
4526:
4506:of such rules. A rule
4478:
4458:, commonly written as
4410:
4384:
4358:
4315:
4309:
4218:
4176:
4170:
4150:
4130:
4099:Term rewriting systems
4082:
4042:
3999:
3979:
3929:
3894:
3866:
3834:
3799:
3775:
3748:
3681:
3642:
3610:
3578:
3558:
3534:
3494:
3462:
3435:
3384:
3334:
3296:
3253:
3233:
3206:
3186:
3159:
3113:
3086:
3059:
3033:
3001:
2969:
2918:
2891:are any strings, then
2885:
2846:
2819:
2799:
2765:
2745:
2725:
2682:
2598:
2531:
2501:
2449:
2423:
2357:
2331:
2302:Church–Rosser property
2294:
2232:
2202:
2169:
2114:
2068:
2023:
1999:
1972:
1948:
1928:
1904:
1819:
1761:
1727:phrase structure rules
1704:
1646:
1608:
1547:
1505:
1438:
1396:
1305:
1263:
1187:
1145:
1070:
1012:
970:
907:
865:
802:
760:
692:
445:
422:
339:
264:
205:
146:
8376:Jean-Pierre Jouannaud
7734:Systems of Reductions
7586:Jean-Pierre Jouannaud
7129:
7072:yields the numerator
7067:
6943:Critical pair (logic)
6896:Graph rewrite systems
6859:
6857:{\displaystyle R_{2}}
6832:
6830:{\displaystyle R_{1}}
6797:
6795:{\displaystyle R_{2}}
6770:
6768:{\displaystyle R_{1}}
6743:
6741:{\displaystyle R_{2}}
6716:
6714:{\displaystyle R_{1}}
6685:
6382:
6337:
6287:
6214:
5997:
5906:
5815:
5795:
5704:
5642:
5572:
5481:
5461:
5396:
5365:
5343:
5304:
5278:
5240:
5209:
5177:
5146:
5114:
5062:
5060:{\displaystyle t_{n}}
5031:
5029:{\displaystyle t_{1}}
5004:
4924:
4922:{\displaystyle t_{n}}
4897:
4895:{\displaystyle t_{1}}
4867:
4834:
4801:
4768:
4748:
4727:rewritten in one step
4720:
4700:
4680:
4651:replacing the subterm
4626:
4597:
4577:
4527:
4498:term rewriting system
4479:
4411:
4385:
4359:
4320:term rewriting system
4310:
4219:
4182:
4171:
4151:
4131:
4106:
4083:
4043:
4000:
3980:
3930:
3895:
3867:
3835:
3800:
3776:
3749:
3682:
3643:
3611:
3579:
3559:
3535:
3495:
3463:
3436:
3385:
3335:
3297:
3254:
3234:
3207:
3187:
3160:
3114:
3087:
3060:
3034:
3032:{\displaystyle t=xvy}
3002:
3000:{\displaystyle s=xuy}
2970:
2919:
2886:
2847:
2820:
2800:
2766:
2746:
2726:
2683:
2652:(SRS), also known as
2599:
2532:
2502:
2450:
2424:
2358:
2332:
2295:
2250:if there exists some
2233:
2203:
2170:
2115:
2069:
2024:
2000:
1973:
1949:
1929:
1905:
1820:
1762:
1705:
1647:
1609:
1548:
1506:
1439:
1397:
1306:
1264:
1188:
1146:
1071:
1013:
971:
908:
866:
803:
761:
693:
446:
423:
340:
265:
206:
147:
8088:Book and Otto, p. 10
7721:and Friedrich Otto,
7076:
7038:
6841:
6814:
6806:, and there are no "
6779:
6752:
6725:
6698:
6396:
6347:
6302:
6228:
6034:
5915:
5824:
5804:
5713:
5651:
5581:
5490:
5470:
5408:
5378:
5354:
5314:
5287:
5249:
5222:
5186:
5159:
5123:
5071:
5044:
5013:
4933:
4906:
4879:
4843:
4810:
4777:
4757:
4737:
4709:
4689:
4669:
4641:reducible expression
4615:
4586:
4566:
4510:
4462:
4394:
4368:
4342:
4228:
4190:
4160:
4140:
4114:
4060:
4017:
3989:
3939:
3907:
3880:
3844:
3813:
3785:
3758:
3694:
3659:
3620:
3588:
3568:
3548:
3512:
3506:equivalence relation
3472:
3445:
3394:
3344:
3306:
3274:
3243:
3216:
3196:
3169:
3123:
3096:
3069:
3043:
3011:
2979:
2928:
2895:
2856:
2829:
2809:
2782:
2755:
2735:
2703:
2672:
2549:
2511:
2479:
2433:
2387:
2341:
2308:
2258:
2216:
2187:
2140:
2098:
2045:
2013:
1982:
1962:
1938:
1918:
1887:
1787:
1741:
1655:
1617:
1556:
1514:
1447:
1405:
1314:
1272:
1196:
1154:
1093:
1021:
979:
916:
874:
811:
769:
708:
490:
444:{\displaystyle \to }
435:
355:
275:
221:
162:
124:
30:For other uses, see
8097:Bezem et al., p. 7,
7788:Rewriting Home Page
6970:Regulated rewriting
6966:in computer science
5302:{\displaystyle s=t}
4433:computable function
4093:Post–Markov theorem
3874:monoid presentation
3754:of the free monoid
3504:, meaning it is an
3058:{\displaystyle uRv}
18:Term rewrite system
8496:Mathematical logic
8318:Inf. Process. Lett
8106:Bezem et al., p. 7
7811:Termination Portal
7768:, Academic Press,
7730:Michael M. Richter
7725:, Springer (1993).
7708:, Elsevier (1990).
7692:John Alan Robinson
7627:John Alan Robinson
7124:
7062:
6854:
6827:
6792:
6765:
6738:
6711:
6680:
6678:
6377:
6332:
6282:
6209:
6207:
5992:
5901:
5810:
5790:
5699:
5637:
5567:
5476:
5456:
5391:
5389:
5360:
5338:
5329:
5299:
5273:
5264:
5235:
5233:
5204:
5198:
5172:
5170:
5153:transitive closure
5141:
5135:
5109:
5093:
5057:
5026:
4999:
4987:
4974:
4954:
4919:
4892:
4862:
4829:
4824:
4796:
4763:
4743:
4731:rewritten directly
4715:
4695:
4675:
4643:. The result term
4621:
4592:
4572:
4522:
4474:
4439:Formal definition
4406:
4380:
4354:
4316:
4305:
4214:
4177:
4166:
4146:
4126:
4078:
4038:
3995:
3975:
3925:
3890:
3862:
3830:
3795:
3771:
3744:
3738:
3677:
3671:
3638:
3632:
3606:
3600:
3574:
3554:
3530:
3524:
3490:
3484:
3458:
3456:
3431:
3380:
3365:
3330:
3321:
3292:
3286:
3249:
3239:. If the relation
3229:
3227:
3202:
3182:
3155:
3150:
3109:
3082:
3080:
3055:
3029:
2997:
2965:
2914:
2909:
2881:
2852:is defined as: if
2842:
2815:
2795:
2793:
2761:
2741:
2721:
2678:
2594:
2527:
2497:
2445:
2419:
2353:
2327:
2290:
2228:
2198:
2165:
2110:
2064:
2019:
1995:
1968:
1944:
1924:
1900:
1870:reduction relation
1815:
1769:syntactic category
1757:
1735:generative grammar
1700:
1642:
1604:
1543:
1501:
1434:
1392:
1301:
1259:
1183:
1141:
1066:
1008:
966:
903:
861:
798:
756:
688:
686:
478:successor function
441:
431:where the symbol (
418:
335:
260:
201:
142:
8501:Rewriting systems
8299:Here: Example 3.3
8072:978-0-262-06144-5
8029:978-0-262-13341-8
7762:Elaine J. Weyuker
7589:"Rewrite Systems"
7582:Nachum Dershowitz
7547:978-0-521-77920-3
5990:
5899:
5813:{\displaystyle *}
5788:
5565:
5479:{\displaystyle *}
5382:
5363:{\displaystyle R}
5333:
5322:
5268:
5257:
5226:
5202:
5191:
5163:
5139:
5128:
5097:
5086:
4980:
4967:
4947:
4872:by some authors.
4857:
4817:
4766:{\displaystyle R}
4746:{\displaystyle t}
4718:{\displaystyle s}
4678:{\displaystyle r}
4595:{\displaystyle s}
4542:if the left term
4431:, that is, every
4303:
4224:matching in term
4149:{\displaystyle p}
3742:
3731:
3675:
3664:
3636:
3625:
3604:
3593:
3577:{\displaystyle R}
3557:{\displaystyle R}
3528:
3517:
3488:
3477:
3449:
3369:
3358:
3325:
3314:
3290:
3279:
3252:{\displaystyle R}
3220:
3205:{\displaystyle R}
3143:
3092:is a relation on
3073:
2902:
2818:{\displaystyle R}
2786:
2764:{\displaystyle R}
2681:{\displaystyle R}
2660:structure of the
2457:locally confluent
2414:
2401:
2322:
2285:
2272:
2159:
2059:
1993:
1956:symmetric closure
1898:
1806:
1637:
1634:
1538:
1429:
1296:
1178:
1003:
898:
793:
678:
616:
581:
522:
86:computer programs
78:non-deterministic
76:Rewriting can be
71:reduction systems
59:rewriting systems
16:(Redirected from
8508:
8486:Formal languages
8470:
8469:
8467:
8466:
8446:
8440:
8439:
8405:
8399:
8397:
8395:
8394:
8388:
8373:
8364:
8358:
8357:
8355:
8354:
8348:
8341:
8315:
8306:
8300:
8298:
8296:
8295:
8273:
8267:
8266:
8264:
8262:
8256:
8245:
8239:
8238:
8236:
8210:
8204:
8203:
8192:
8186:
8184:
8168:
8162:
8161:
8159:
8157:
8151:
8140:
8131:
8125:
8122:
8116:
8113:
8107:
8104:
8098:
8095:
8089:
8086:
8077:
8076:
8056:
8050:
8048:
8040:
8034:
8033:
8013:
8007:
8006:
8004:
7980:
7971:
7970:
7968:
7944:
7938:
7937:
7935:
7911:
7905:
7904:
7902:
7901:
7895:
7854:
7845:
7839:
7833:
7713:String rewriting
7678:David Plaisted.
7646:et Derek Oppen,
7551:
7516:
7369:
7363:
7140:
7134:
7133:
7131:
7130:
7125:
7071:
7069:
7068:
7063:
7032:
7026:
6991:
6975:Interaction Nets
6914:representation.
6863:
6861:
6860:
6855:
6853:
6852:
6836:
6834:
6833:
6828:
6826:
6825:
6801:
6799:
6798:
6793:
6791:
6790:
6774:
6772:
6771:
6766:
6764:
6763:
6747:
6745:
6744:
6739:
6737:
6736:
6720:
6718:
6717:
6712:
6710:
6709:
6689:
6687:
6686:
6681:
6679:
6402:
6386:
6384:
6383:
6378:
6341:
6339:
6338:
6333:
6291:
6289:
6288:
6283:
6218:
6216:
6215:
6210:
6208:
6001:
5999:
5998:
5993:
5991:
5989:
5966:
5919:
5910:
5908:
5907:
5902:
5900:
5898:
5875:
5828:
5819:
5817:
5816:
5811:
5799:
5797:
5796:
5791:
5789:
5787:
5764:
5717:
5708:
5706:
5705:
5700:
5646:
5644:
5643:
5638:
5576:
5574:
5573:
5568:
5566:
5564:
5541:
5494:
5485:
5483:
5482:
5477:
5465:
5463:
5462:
5457:
5400:
5398:
5397:
5392:
5390:
5369:
5367:
5366:
5361:
5349:
5347:
5345:
5344:
5339:
5334:
5321:
5308:
5306:
5305:
5300:
5282:
5280:
5279:
5274:
5269:
5256:
5244:
5242:
5241:
5236:
5234:
5213:
5211:
5210:
5205:
5203:
5190:
5181:
5179:
5178:
5173:
5171:
5155:of the relation
5150:
5148:
5147:
5142:
5140:
5127:
5118:
5116:
5115:
5110:
5108:
5107:
5098:
5085:
5083:
5082:
5066:
5064:
5063:
5058:
5056:
5055:
5035:
5033:
5032:
5027:
5025:
5024:
5008:
5006:
5005:
5000:
4998:
4997:
4988:
4975:
4965:
4964:
4955:
4945:
4944:
4928:
4926:
4925:
4920:
4918:
4917:
4901:
4899:
4898:
4893:
4891:
4890:
4871:
4869:
4868:
4863:
4858:
4850:
4838:
4836:
4835:
4830:
4825:
4805:
4803:
4802:
4797:
4792:
4791:
4772:
4770:
4769:
4764:
4752:
4750:
4749:
4744:
4724:
4722:
4721:
4716:
4704:
4702:
4701:
4696:
4684:
4682:
4681:
4676:
4664:
4658:
4648:
4634:
4630:
4628:
4627:
4622:
4610:
4601:
4599:
4598:
4593:
4581:
4579:
4578:
4573:
4558:
4545:
4541:
4531:
4529:
4528:
4523:
4505:
4495:
4489:
4483:
4481:
4480:
4475:
4415:
4413:
4412:
4407:
4389:
4387:
4386:
4381:
4363:
4361:
4360:
4355:
4314:
4312:
4311:
4306:
4304:
4302:
4279:
4232:
4223:
4221:
4220:
4215:
4175:
4173:
4172:
4167:
4155:
4153:
4152:
4147:
4135:
4133:
4132:
4127:
4087:
4085:
4084:
4079:
4047:
4045:
4044:
4039:
4004:
4002:
4001:
3996:
3984:
3982:
3981:
3976:
3934:
3932:
3931:
3926:
3899:
3897:
3896:
3891:
3889:
3888:
3871:
3869:
3868:
3863:
3839:
3837:
3836:
3831:
3829:
3828:
3823:
3822:
3804:
3802:
3801:
3796:
3794:
3793:
3780:
3778:
3777:
3772:
3770:
3769:
3753:
3751:
3750:
3745:
3743:
3730:
3728:
3723:
3722:
3710:
3709:
3704:
3703:
3686:
3684:
3683:
3678:
3676:
3663:
3647:
3645:
3644:
3639:
3637:
3624:
3615:
3613:
3612:
3607:
3605:
3592:
3583:
3581:
3580:
3575:
3563:
3561:
3560:
3555:
3539:
3537:
3536:
3531:
3529:
3516:
3499:
3497:
3496:
3491:
3489:
3476:
3467:
3465:
3464:
3459:
3457:
3440:
3438:
3437:
3432:
3430:
3429:
3390:for all strings
3389:
3387:
3386:
3381:
3370:
3357:
3339:
3337:
3336:
3331:
3326:
3313:
3301:
3299:
3298:
3293:
3291:
3278:
3258:
3256:
3255:
3250:
3238:
3236:
3235:
3230:
3228:
3211:
3209:
3208:
3203:
3191:
3189:
3188:
3183:
3181:
3180:
3164:
3162:
3161:
3156:
3151:
3138:
3137:
3118:
3116:
3115:
3110:
3108:
3107:
3091:
3089:
3088:
3083:
3081:
3064:
3062:
3061:
3056:
3038:
3036:
3035:
3030:
3006:
3004:
3003:
2998:
2974:
2972:
2971:
2966:
2964:
2963:
2923:
2921:
2920:
2915:
2910:
2890:
2888:
2887:
2882:
2880:
2879:
2851:
2849:
2848:
2843:
2841:
2840:
2824:
2822:
2821:
2816:
2804:
2802:
2801:
2796:
2794:
2770:
2768:
2767:
2762:
2750:
2748:
2747:
2742:
2730:
2728:
2727:
2722:
2687:
2685:
2684:
2679:
2664:(words) over an
2654:semi-Thue system
2603:
2601:
2600:
2595:
2587:
2586:
2574:
2573:
2561:
2560:
2536:
2534:
2533:
2528:
2523:
2522:
2506:
2504:
2503:
2498:
2454:
2452:
2451:
2446:
2428:
2426:
2425:
2420:
2415:
2407:
2402:
2394:
2362:
2360:
2359:
2354:
2336:
2334:
2333:
2328:
2323:
2315:
2299:
2297:
2296:
2291:
2286:
2278:
2273:
2265:
2237:
2235:
2234:
2229:
2207:
2205:
2204:
2199:
2197:
2174:
2172:
2171:
2166:
2161:
2160:
2158:
2153:
2148:
2119:
2117:
2116:
2111:
2073:
2071:
2070:
2065:
2060:
2052:
2028:
2026:
2025:
2020:
2004:
2002:
2001:
1996:
1994:
1986:
1977:
1975:
1974:
1969:
1953:
1951:
1950:
1945:
1933:
1931:
1930:
1925:
1909:
1907:
1906:
1901:
1899:
1891:
1874:rewrite relation
1824:
1822:
1821:
1816:
1814:
1813:
1804:
1766:
1764:
1763:
1758:
1756:
1755:
1709:
1707:
1706:
1701:
1651:
1649:
1648:
1643:
1639:
1638:
1636:
1635:
1632:
1629:
1624:
1613:
1611:
1610:
1605:
1552:
1550:
1549:
1544:
1540:
1539:
1537:
1526:
1521:
1510:
1508:
1507:
1502:
1443:
1441:
1440:
1435:
1431:
1430:
1428:
1417:
1412:
1401:
1399:
1398:
1393:
1310:
1308:
1307:
1302:
1298:
1297:
1295:
1284:
1279:
1268:
1266:
1265:
1260:
1192:
1190:
1189:
1184:
1180:
1179:
1177:
1166:
1161:
1150:
1148:
1147:
1142:
1075:
1073:
1072:
1067:
1017:
1015:
1014:
1009:
1005:
1004:
1002:
991:
986:
975:
973:
972:
967:
912:
910:
909:
904:
900:
899:
897:
886:
881:
870:
868:
867:
862:
807:
805:
804:
799:
795:
794:
792:
781:
776:
765:
763:
762:
757:
697:
695:
694:
689:
687:
680:
679:
676:
618:
617:
614:
583:
582:
579:
524:
523:
520:
450:
448:
447:
442:
427:
425:
424:
419:
344:
342:
341:
336:
269:
267:
266:
261:
213:De Morgan's laws
210:
208:
207:
202:
151:
149:
148:
143:
43:computer science
21:
8516:
8515:
8511:
8510:
8509:
8507:
8506:
8505:
8476:
8475:
8474:
8473:
8464:
8462:
8448:
8447:
8443:
8428:
8407:
8406:
8402:
8392:
8390:
8386:
8371:
8366:
8365:
8361:
8352:
8350:
8346:
8313:
8308:
8307:
8303:
8293:
8291:
8275:
8274:
8270:
8260:
8258:
8254:
8247:
8246:
8242:
8212:
8211:
8207:
8194:
8193:
8189:
8181:Rewrite Systems
8177:Jan van Leeuwen
8173:J.-P. Jouannaud
8171:N. Dershowitz,
8170:
8169:
8165:
8155:
8153:
8149:
8138:
8133:
8132:
8128:
8123:
8119:
8114:
8110:
8105:
8101:
8096:
8092:
8087:
8080:
8073:
8058:
8057:
8053:
8042:
8041:
8037:
8030:
8015:
8014:
8010:
7982:
7981:
7974:
7959:(1–3): 95–138.
7946:
7945:
7941:
7913:
7912:
7908:
7899:
7897:
7893:
7852:
7847:
7846:
7842:
7834:
7830:
7825:
7802:Aart Middeldorp
7783:
7658:Samson Abramsky
7654:Jan Willem Klop
7631:Andrei Voronkov
7625:, Chapter 9 in
7593:Jan van Leeuwen
7591:, Chapter 6 in
7560:Jan Willem Klop
7548:
7528:
7525:
7523:Further reading
7520:
7519:
7370:
7366:
7141:
7137:
7074:
7073:
7036:
7035:
7033:
7029:
6992:
6988:
6983:
6939:
6920:
6893:
6881:
6844:
6839:
6838:
6817:
6812:
6811:
6782:
6777:
6776:
6755:
6750:
6749:
6728:
6723:
6722:
6701:
6696:
6695:
6677:
6676:
6669:
6663:
6662:
6591:
6585:
6584:
6543:
6537:
6536:
6480:
6474:
6473:
6394:
6393:
6345:
6344:
6300:
6299:
6226:
6225:
6206:
6205:
6147:
6126:
6125:
6112:
6082:
6081:
6059:
6032:
6031:
6008:
5967:
5920:
5913:
5912:
5876:
5829:
5822:
5821:
5802:
5801:
5765:
5718:
5711:
5710:
5649:
5648:
5579:
5578:
5542:
5495:
5488:
5487:
5468:
5467:
5406:
5405:
5376:
5375:
5352:
5351:
5312:
5311:
5310:
5285:
5284:
5247:
5246:
5220:
5219:
5184:
5183:
5157:
5156:
5121:
5120:
5099:
5074:
5069:
5068:
5047:
5042:
5041:
5016:
5011:
5010:
4989:
4956:
4936:
4931:
4930:
4909:
4904:
4903:
4882:
4877:
4876:
4841:
4840:
4808:
4807:
4783:
4775:
4774:
4755:
4754:
4735:
4734:
4707:
4706:
4687:
4686:
4667:
4666:
4660:
4654:
4644:
4632:
4613:
4612:
4606:
4602:rooted at some
4584:
4583:
4564:
4563:
4554:
4543:
4537:
4508:
4507:
4501:
4491:
4485:
4460:
4459:
4448:
4441:
4429:Turing machines
4392:
4391:
4366:
4365:
4340:
4339:
4280:
4233:
4226:
4225:
4188:
4187:
4158:
4157:
4138:
4137:
4112:
4111:
4101:
4058:
4057:
4050:bicyclic monoid
4015:
4014:
3987:
3986:
3937:
3936:
3935:with the rules
3905:
3904:
3878:
3877:
3842:
3841:
3816:
3811:
3810:
3783:
3782:
3761:
3756:
3755:
3714:
3697:
3692:
3691:
3657:
3656:
3618:
3617:
3586:
3585:
3566:
3565:
3546:
3545:
3542:Thue congruence
3510:
3509:
3470:
3469:
3443:
3442:
3421:
3392:
3391:
3342:
3341:
3304:
3303:
3272:
3271:
3241:
3240:
3214:
3213:
3212:is a subset of
3194:
3193:
3172:
3167:
3166:
3129:
3121:
3120:
3099:
3094:
3093:
3067:
3066:
3041:
3040:
3009:
3008:
2977:
2976:
2955:
2926:
2925:
2924:if there exist
2893:
2892:
2871:
2854:
2853:
2832:
2827:
2826:
2807:
2806:
2780:
2779:
2753:
2752:
2733:
2732:
2701:
2700:
2670:
2669:
2656:, exploits the
2646:
2640:
2578:
2565:
2552:
2547:
2546:
2509:
2508:
2477:
2476:
2431:
2430:
2385:
2384:
2339:
2338:
2306:
2305:
2256:
2255:
2246:are said to be
2214:
2213:
2185:
2184:
2138:
2137:
2096:
2095:
2043:
2042:
2011:
2010:
1980:
1979:
1960:
1959:
1936:
1935:
1916:
1915:
1885:
1884:
1862:binary relation
1841:
1835:
1785:
1784:
1771:label, such as
1767:, where A is a
1739:
1738:
1719:
1653:
1652:
1615:
1614:
1554:
1553:
1512:
1511:
1445:
1444:
1403:
1402:
1312:
1311:
1270:
1269:
1194:
1193:
1152:
1151:
1091:
1090:
1019:
1018:
977:
976:
914:
913:
872:
871:
809:
808:
767:
766:
706:
705:
685:
684:
672:
644:
623:
622:
610:
600:
588:
587:
575:
550:
529:
528:
516:
506:
488:
487:
466:natural numbers
462:
433:
432:
353:
352:
273:
272:
219:
218:
160:
159:
122:
121:
107:
102:
90:theorem provers
67:rewrite engines
63:rewrite systems
61:(also known as
35:
28:
23:
22:
15:
12:
11:
5:
8514:
8512:
8504:
8503:
8498:
8493:
8488:
8478:
8477:
8472:
8471:
8441:
8426:
8400:
8359:
8324:(3): 141–143.
8301:
8268:
8240:
8227:(2): 409–420.
8205:
8187:
8163:
8126:
8117:
8108:
8099:
8090:
8078:
8071:
8051:
8035:
8028:
8008:
7995:(2): 187–243.
7972:
7939:
7926:(1–2): 71–99.
7906:
7865:(4): 434–473.
7840:
7827:
7826:
7824:
7821:
7820:
7819:
7813:
7808:
7795:
7790:
7782:
7781:External links
7779:
7778:
7777:
7750:
7749:
7745:
7744:
7726:
7719:Ronald V. Book
7715:
7714:
7710:
7709:
7702:
7676:
7651:
7641:
7619:David Plaisted
7615:
7579:
7564:Roel de Vrijer
7553:
7546:
7534:Nipkow, Tobias
7524:
7521:
7518:
7517:
7364:
7135:
7123:
7120:
7117:
7114:
7111:
7108:
7105:
7102:
7099:
7096:
7093:
7090:
7087:
7084:
7081:
7061:
7058:
7055:
7052:
7049:
7046:
7043:
7027:
6985:
6984:
6982:
6979:
6978:
6977:
6972:
6967:
6961:
6955:
6950:
6945:
6938:
6935:
6931:history monoid
6919:
6916:
6892:
6889:
6880:
6877:
6851:
6847:
6824:
6820:
6789:
6785:
6762:
6758:
6735:
6731:
6708:
6704:
6675:
6672:
6670:
6668:
6665:
6664:
6661:
6658:
6655:
6652:
6649:
6646:
6643:
6640:
6637:
6634:
6631:
6628:
6625:
6622:
6619:
6616:
6613:
6610:
6607:
6604:
6601:
6598:
6595:
6592:
6590:
6587:
6586:
6583:
6580:
6577:
6574:
6571:
6568:
6565:
6562:
6559:
6556:
6553:
6550:
6547:
6544:
6542:
6539:
6538:
6535:
6532:
6529:
6526:
6523:
6520:
6517:
6514:
6511:
6508:
6505:
6502:
6499:
6496:
6493:
6490:
6487:
6484:
6481:
6479:
6476:
6475:
6472:
6469:
6466:
6463:
6460:
6457:
6454:
6451:
6448:
6445:
6442:
6439:
6436:
6433:
6430:
6427:
6424:
6421:
6418:
6415:
6412:
6409:
6406:
6403:
6401:
6388:
6387:
6376:
6373:
6370:
6367:
6364:
6361:
6358:
6355:
6352:
6342:
6331:
6328:
6325:
6322:
6319:
6316:
6313:
6310:
6307:
6293:
6292:
6281:
6278:
6275:
6272:
6269:
6266:
6263:
6260:
6257:
6254:
6251:
6248:
6245:
6242:
6239:
6236:
6233:
6204:
6201:
6198:
6195:
6192:
6189:
6186:
6183:
6180:
6177:
6174:
6171:
6168:
6165:
6162:
6159:
6156:
6153:
6150:
6148:
6146:
6143:
6140:
6137:
6134:
6131:
6128:
6127:
6124:
6121:
6118:
6115:
6113:
6111:
6108:
6105:
6102:
6099:
6096:
6093:
6090:
6087:
6084:
6083:
6080:
6077:
6074:
6071:
6068:
6065:
6062:
6060:
6058:
6055:
6052:
6049:
6046:
6043:
6040:
6039:
6007:
6004:
5988:
5985:
5982:
5979:
5976:
5973:
5970:
5965:
5962:
5959:
5956:
5953:
5950:
5947:
5944:
5941:
5938:
5935:
5932:
5929:
5926:
5923:
5897:
5894:
5891:
5888:
5885:
5882:
5879:
5874:
5871:
5868:
5865:
5862:
5859:
5856:
5853:
5850:
5847:
5844:
5841:
5838:
5835:
5832:
5809:
5786:
5783:
5780:
5777:
5774:
5771:
5768:
5763:
5760:
5757:
5754:
5751:
5748:
5745:
5742:
5739:
5736:
5733:
5730:
5727:
5724:
5721:
5698:
5695:
5692:
5689:
5686:
5683:
5680:
5677:
5674:
5671:
5668:
5665:
5662:
5659:
5656:
5636:
5633:
5630:
5627:
5624:
5621:
5617:
5614:
5611:
5608:
5605:
5602:
5598:
5595:
5592:
5589:
5586:
5563:
5560:
5557:
5554:
5551:
5548:
5545:
5540:
5537:
5534:
5531:
5528:
5525:
5522:
5519:
5516:
5513:
5510:
5507:
5504:
5501:
5498:
5475:
5455:
5452:
5449:
5446:
5443:
5440:
5437:
5434:
5431:
5428:
5425:
5422:
5419:
5416:
5413:
5388:
5385:
5359:
5337:
5332:
5328:
5325:
5319:
5298:
5295:
5292:
5272:
5267:
5263:
5260:
5254:
5232:
5229:
5201:
5197:
5194:
5169:
5166:
5138:
5134:
5131:
5106:
5102:
5096:
5092:
5089:
5081:
5077:
5054:
5050:
5036:is said to be
5023:
5019:
4996:
4992:
4986:
4983:
4978:
4973:
4970:
4963:
4959:
4953:
4950:
4943:
4939:
4929:, that is, if
4916:
4912:
4889:
4885:
4861:
4856:
4853:
4848:
4828:
4823:
4820:
4815:
4795:
4790:
4786:
4782:
4762:
4753:by the system
4742:
4725:is said to be
4714:
4694:
4674:
4620:
4591:
4571:
4521:
4518:
4515:
4473:
4470:
4467:
4440:
4437:
4405:
4402:
4399:
4379:
4376:
4373:
4353:
4350:
4347:
4301:
4298:
4295:
4292:
4289:
4286:
4283:
4278:
4275:
4272:
4269:
4266:
4263:
4260:
4257:
4254:
4251:
4248:
4245:
4242:
4239:
4236:
4213:
4210:
4207:
4204:
4201:
4198:
4195:
4186:Rule lhs term
4165:
4145:
4125:
4122:
4119:
4100:
4097:
4077:
4074:
4071:
4068:
4065:
4037:
4034:
4031:
4028:
4025:
4022:
3994:
3974:
3971:
3968:
3965:
3962:
3959:
3956:
3953:
3950:
3947:
3944:
3924:
3921:
3918:
3915:
3912:
3887:
3861:
3858:
3855:
3852:
3849:
3827:
3821:
3792:
3768:
3764:
3741:
3737:
3734:
3727:
3721:
3717:
3713:
3708:
3702:
3674:
3670:
3667:
3635:
3631:
3628:
3603:
3599:
3596:
3573:
3553:
3540:is called the
3527:
3523:
3520:
3487:
3483:
3480:
3455:
3452:
3428:
3424:
3420:
3417:
3414:
3411:
3408:
3405:
3402:
3399:
3379:
3376:
3373:
3368:
3364:
3361:
3355:
3352:
3349:
3329:
3324:
3320:
3317:
3311:
3289:
3285:
3282:
3248:
3226:
3223:
3201:
3179:
3175:
3154:
3149:
3146:
3141:
3136:
3132:
3128:
3106:
3102:
3079:
3076:
3054:
3051:
3048:
3028:
3025:
3022:
3019:
3016:
2996:
2993:
2990:
2987:
2984:
2962:
2958:
2954:
2951:
2948:
2945:
2942:
2939:
2936:
2933:
2913:
2908:
2905:
2900:
2878:
2874:
2870:
2867:
2864:
2861:
2839:
2835:
2814:
2792:
2789:
2760:
2740:
2720:
2717:
2714:
2711:
2708:
2677:
2642:Main article:
2639:
2636:
2630:for an ARS is
2624:Newman's lemma
2593:
2590:
2585:
2581:
2577:
2572:
2568:
2564:
2559:
2555:
2526:
2521:
2516:
2496:
2493:
2490:
2487:
2484:
2444:
2441:
2438:
2418:
2413:
2410:
2405:
2400:
2397:
2392:
2352:
2349:
2346:
2326:
2321:
2318:
2313:
2289:
2284:
2281:
2276:
2271:
2268:
2263:
2227:
2224:
2221:
2196:
2192:
2164:
2157:
2152:
2145:
2109:
2106:
2103:
2063:
2058:
2055:
2050:
2018:
1992:
1989:
1967:
1943:
1923:
1897:
1894:
1837:Main article:
1834:
1831:
1812:
1809:
1803:
1800:
1797:
1794:
1754:
1751:
1748:
1729:, also called
1718:
1715:
1711:
1710:
1699:
1696:
1693:
1690:
1687:
1684:
1681:
1678:
1675:
1672:
1669:
1666:
1663:
1660:
1628:
1603:
1600:
1597:
1594:
1591:
1588:
1585:
1582:
1579:
1576:
1573:
1570:
1567:
1564:
1561:
1536:
1533:
1530:
1525:
1500:
1497:
1494:
1491:
1488:
1485:
1482:
1479:
1476:
1473:
1470:
1467:
1464:
1461:
1458:
1455:
1452:
1427:
1424:
1421:
1416:
1391:
1388:
1385:
1382:
1379:
1376:
1373:
1370:
1367:
1364:
1361:
1358:
1355:
1352:
1349:
1346:
1343:
1340:
1337:
1334:
1331:
1328:
1325:
1322:
1319:
1294:
1291:
1288:
1283:
1258:
1255:
1252:
1249:
1246:
1243:
1240:
1237:
1234:
1231:
1228:
1225:
1222:
1219:
1216:
1213:
1210:
1207:
1204:
1201:
1176:
1173:
1170:
1165:
1140:
1137:
1134:
1131:
1128:
1125:
1122:
1119:
1116:
1113:
1110:
1107:
1104:
1101:
1098:
1077:
1076:
1065:
1062:
1059:
1056:
1053:
1050:
1047:
1044:
1041:
1038:
1035:
1032:
1029:
1026:
1001:
998:
995:
990:
965:
962:
958:
955:
952:
949:
946:
943:
940:
937:
934:
930:
927:
924:
921:
896:
893:
890:
885:
860:
856:
853:
850:
847:
844:
841:
838:
835:
832:
829:
826:
823:
819:
816:
791:
788:
785:
780:
755:
752:
749:
746:
743:
740:
737:
734:
731:
728:
725:
722:
719:
716:
713:
699:
698:
683:
673:
671:
668:
665:
662:
659:
656:
653:
650:
647:
645:
643:
640:
637:
634:
631:
628:
625:
624:
621:
611:
609:
606:
603:
601:
599:
596:
593:
590:
589:
586:
576:
574:
571:
568:
565:
562:
559:
556:
553:
551:
549:
546:
543:
540:
537:
534:
531:
530:
527:
517:
515:
512:
509:
507:
505:
502:
499:
496:
495:
461:
458:
440:
429:
428:
417:
414:
411:
408:
405:
402:
399:
396:
393:
390:
387:
384:
381:
378:
375:
372:
369:
366:
363:
360:
350:
347:distributivity
334:
331:
328:
325:
322:
319:
316:
313:
310:
307:
304:
301:
298:
295:
292:
289:
286:
283:
280:
270:
259:
256:
253:
250:
247:
244:
241:
238:
235:
232:
229:
226:
216:
200:
197:
194:
191:
188:
185:
182:
179:
176:
173:
170:
167:
157:
141:
138:
135:
132:
129:
106:
103:
101:
98:
88:, and several
26:
24:
14:
13:
10:
9:
6:
4:
3:
2:
8513:
8502:
8499:
8497:
8494:
8492:
8489:
8487:
8484:
8483:
8481:
8460:
8456:
8452:
8445:
8442:
8437:
8433:
8429:
8427:9780521395380
8423:
8419:
8415:
8411:
8404:
8401:
8398:; here: p.210
8385:
8381:
8377:
8370:
8369:"Termination"
8363:
8360:
8345:
8340:
8335:
8331:
8327:
8323:
8319:
8312:
8305:
8302:
8289:
8285:
8284:
8279:
8272:
8269:
8253:
8252:
8244:
8241:
8235:
8230:
8226:
8222:
8221:
8216:
8209:
8206:
8201:
8200:
8191:
8188:
8182:
8178:
8174:
8167:
8164:
8148:
8144:
8137:
8130:
8127:
8121:
8118:
8112:
8109:
8103:
8100:
8094:
8091:
8085:
8083:
8079:
8074:
8068:
8065:. MIT Press.
8064:
8063:
8055:
8052:
8046:
8039:
8036:
8031:
8025:
8021:
8020:
8012:
8009:
8003:
7998:
7994:
7990:
7986:
7979:
7977:
7973:
7967:
7962:
7958:
7954:
7950:
7943:
7940:
7934:
7929:
7925:
7921:
7917:
7910:
7907:
7892:
7888:
7884:
7880:
7876:
7872:
7868:
7864:
7860:
7859:
7851:
7844:
7841:
7837:
7836:Joseph Goguen
7832:
7829:
7822:
7817:
7814:
7812:
7809:
7807:
7803:
7799:
7796:
7794:
7791:
7789:
7785:
7784:
7780:
7775:
7774:0-12-206382-1
7771:
7767:
7763:
7759:
7755:
7752:
7751:
7747:
7746:
7742:
7739:
7735:
7731:
7727:
7724:
7720:
7717:
7716:
7712:
7711:
7707:
7703:
7700:
7698:
7693:
7689:
7685:
7684:Dov M. Gabbay
7681:
7677:
7674:
7672:
7667:
7663:
7662:Dov M. Gabbay
7659:
7655:
7652:
7649:
7645:
7642:
7639:
7637:
7632:
7628:
7624:
7620:
7616:
7613:
7609:
7608:0-444-88074-7
7605:
7601:
7599:
7594:
7590:
7587:
7583:
7580:
7577:
7576:0-521-39115-6
7573:
7569:
7565:
7561:
7557:
7554:
7549:
7543:
7539:
7535:
7531:
7530:Baader, Franz
7527:
7526:
7522:
7514:
7510:
7506:
7502:
7498:
7494:
7490:
7486:
7482:
7478:
7474:
7470:
7466:
7462:
7458:
7454:
7450:
7446:
7442:
7438:
7434:
7430:
7426:
7422:
7418:
7414:
7410:
7406:
7402:
7398:
7394:
7390:
7386:
7382:
7378:
7374:
7368:
7365:
7361:
7357:
7353:
7349:
7345:
7341:
7337:
7333:
7329:
7325:
7321:
7317:
7313:
7309:
7305:
7301:
7297:
7293:
7289:
7285:
7281:
7277:
7273:
7269:
7265:
7261:
7257:
7253:
7249:
7245:
7241:
7237:
7233:
7229:
7225:
7221:
7217:
7213:
7209:
7205:
7201:
7197:
7193:
7189:
7185:
7181:
7177:
7173:
7169:
7165:
7161:
7157:
7153:
7149:
7145:
7139:
7136:
7115:
7112:
7109:
7103:
7097:
7094:
7091:
7082:
7079:
7056:
7053:
7050:
7044:
7041:
7031:
7028:
7024:
7020:
7016:
7012:
7008:
7004:
7000:
6996:
6990:
6987:
6980:
6976:
6973:
6971:
6968:
6965:
6962:
6959:
6956:
6954:
6951:
6949:
6946:
6944:
6941:
6940:
6936:
6934:
6932:
6928:
6924:
6917:
6915:
6913:
6909:
6905:
6901:
6897:
6890:
6888:
6886:
6878:
6876:
6874:
6870:
6869:Rewrite order
6865:
6849:
6845:
6822:
6818:
6809:
6805:
6787:
6783:
6760:
6756:
6733:
6729:
6706:
6702:
6693:
6673:
6671:
6653:
6650:
6647:
6641:
6638:
6632:
6629:
6626:
6620:
6617:
6611:
6608:
6605:
6599:
6593:
6575:
6572:
6569:
6563:
6560:
6557:
6554:
6551:
6545:
6527:
6524:
6521:
6515:
6512:
6506:
6503:
6500:
6494:
6491:
6488:
6482:
6464:
6461:
6458:
6452:
6449:
6443:
6440:
6437:
6431:
6428:
6422:
6419:
6416:
6410:
6404:
6391:
6374:
6371:
6362:
6359:
6356:
6350:
6343:
6329:
6326:
6317:
6314:
6311:
6305:
6298:
6297:
6296:
6276:
6273:
6270:
6267:
6264:
6258:
6249:
6246:
6243:
6240:
6237:
6231:
6224:
6223:
6222:
6219:
6202:
6193:
6190:
6187:
6181:
6178:
6172:
6169:
6166:
6160:
6154:
6149:
6141:
6138:
6135:
6129:
6122:
6119:
6114:
6103:
6097:
6094:
6091:
6085:
6078:
6072:
6066:
6061:
6053:
6050:
6047:
6041:
6028:
6026:
6022:
6017:
6015:
6014:
6005:
6003:
5986:
5983:
5977:
5974:
5971:
5957:
5954:
5951:
5945:
5939:
5936:
5933:
5924:
5921:
5892:
5889:
5886:
5880:
5877:
5866:
5863:
5860:
5854:
5848:
5845:
5842:
5833:
5830:
5807:
5781:
5778:
5775:
5769:
5766:
5758:
5755:
5752:
5746:
5737:
5734:
5731:
5725:
5722:
5693:
5690:
5687:
5681:
5672:
5669:
5666:
5660:
5657:
5631:
5628:
5625:
5619:
5615:
5612:
5609:
5606:
5600:
5596:
5593:
5587:
5558:
5555:
5552:
5546:
5543:
5532:
5529:
5526:
5520:
5514:
5511:
5508:
5499:
5496:
5473:
5453:
5450:
5444:
5441:
5438:
5426:
5423:
5420:
5414:
5411:
5404:For example,
5402:
5386:
5373:
5357:
5335:
5330:
5326:
5317:
5296:
5293:
5290:
5270:
5265:
5261:
5252:
5230:
5217:
5199:
5195:
5167:
5154:
5136:
5132:
5104:
5100:
5094:
5090:
5079:
5075:
5052:
5048:
5039:
5021:
5017:
4994:
4990:
4984:
4976:
4971:
4961:
4957:
4951:
4941:
4937:
4914:
4910:
4887:
4883:
4873:
4859:
4854:
4846:
4826:
4821:
4813:
4793:
4788:
4780:
4760:
4740:
4732:
4728:
4712:
4692:
4672:
4665:by the term
4663:
4657:
4652:
4647:
4642:
4638:
4618:
4609:
4605:
4589:
4569:
4562:
4557:
4552:
4548:
4540:
4535:
4519:
4513:
4504:
4499:
4494:
4488:
4471:
4465:
4457:
4454:is a pair of
4453:
4446:
4438:
4436:
4434:
4430:
4426:
4422:
4417:
4374:
4348:
4337:
4336:
4331:
4330:
4325:
4321:
4296:
4293:
4290:
4284:
4281:
4270:
4267:
4264:
4258:
4252:
4249:
4246:
4237:
4234:
4208:
4205:
4202:
4196:
4193:
4185:
4181:
4163:
4143:
4123:
4117:
4109:
4105:
4098:
4096:
4094:
4089:
4072:
4069:
4055:
4051:
4032:
4026:
4023:
4012:
4008:
3992:
3969:
3963:
3960:
3957:
3954:
3948:
3945:
3919:
3916:
3913:
3901:
3875:
3856:
3853:
3825:
3808:
3766:
3739:
3735:
3725:
3719:
3711:
3706:
3690:
3689:factor monoid
3672:
3668:
3654:
3649:
3633:
3629:
3601:
3597:
3571:
3551:
3544:generated by
3543:
3525:
3521:
3507:
3503:
3485:
3481:
3453:
3426:
3418:
3415:
3412:
3409:
3406:
3403:
3400:
3397:
3377:
3374:
3371:
3366:
3362:
3353:
3350:
3347:
3327:
3322:
3318:
3309:
3287:
3283:
3268:
3266:
3262:
3246:
3224:
3199:
3177:
3147:
3139:
3134:
3104:
3077:
3052:
3049:
3046:
3026:
3023:
3020:
3017:
3014:
2994:
2991:
2988:
2985:
2982:
2960:
2952:
2949:
2946:
2943:
2940:
2937:
2934:
2931:
2911:
2906:
2898:
2876:
2868:
2865:
2862:
2859:
2837:
2812:
2790:
2778:
2774:
2773:rewrite rules
2758:
2715:
2712:
2699:
2695:
2691:
2675:
2667:
2663:
2659:
2655:
2651:
2645:
2637:
2635:
2633:
2629:
2625:
2621:
2618:
2613:
2611:
2607:
2591:
2583:
2579:
2570:
2566:
2557:
2553:
2544:
2540:
2524:
2514:
2494:
2488:
2482:
2474:
2470:
2466:
2462:
2458:
2442:
2436:
2416:
2411:
2403:
2398:
2390:
2382:
2378:
2374:
2370:
2366:
2350:
2344:
2324:
2319:
2311:
2303:
2287:
2282:
2274:
2269:
2261:
2253:
2249:
2245:
2241:
2225:
2219:
2211:
2190:
2182:
2178:
2162:
2155:
2143:
2135:
2131:
2127:
2123:
2107:
2101:
2093:
2089:
2085:
2081:
2077:
2061:
2056:
2048:
2040:
2036:
2032:
2008:
1990:
1957:
1913:
1895:
1881:
1879:
1875:
1871:
1867:
1863:
1859:
1855:
1852:(abbreviated
1851:
1847:
1840:
1832:
1830:
1828:
1782:
1778:
1774:
1770:
1736:
1732:
1731:rewrite rules
1728:
1724:
1716:
1714:
1697:
1682:
1676:
1670:
1664:
1658:
1595:
1589:
1583:
1580:
1571:
1565:
1559:
1531:
1498:
1495:
1486:
1480:
1474:
1471:
1462:
1456:
1450:
1422:
1389:
1386:
1377:
1371:
1365:
1362:
1353:
1347:
1341:
1338:
1329:
1323:
1317:
1289:
1253:
1247:
1244:
1235:
1229:
1223:
1220:
1211:
1205:
1199:
1171:
1132:
1126:
1120:
1117:
1108:
1102:
1096:
1089:
1088:
1087:
1084:
1082:
1063:
1048:
1042:
1036:
1030:
1024:
996:
956:
953:
944:
938:
932:
925:
919:
891:
851:
845:
842:
833:
827:
821:
814:
786:
747:
741:
735:
732:
723:
717:
711:
704:
703:
702:
681:
666:
663:
660:
654:
651:
646:
638:
632:
629:
626:
619:
607:
602:
597:
594:
591:
584:
569:
566:
563:
557:
552:
544:
538:
535:
532:
525:
513:
508:
503:
500:
497:
486:
485:
484:
482:
479:
475:
471:
467:
459:
457:
454:
415:
409:
406:
403:
397:
391:
388:
385:
373:
370:
367:
361:
358:
351:
348:
329:
326:
323:
317:
311:
308:
305:
296:
293:
287:
284:
281:
271:
257:
251:
248:
236:
233:
230:
217:
214:
198:
192:
189:
177:
174:
171:
158:
155:
139:
133:
120:
119:
118:
116:
112:
104:
100:Example cases
99:
97:
95:
91:
87:
83:
79:
74:
72:
68:
64:
60:
56:
52:
48:
44:
40:
33:
19:
8463:. Retrieved
8454:
8444:
8409:
8403:
8391:. Retrieved
8379:
8362:
8351:. Retrieved
8321:
8317:
8304:
8292:. Retrieved
8282:
8271:
8259:. Retrieved
8250:
8243:
8224:
8218:
8208:
8196:
8190:
8180:
8166:
8154:. Retrieved
8142:
8134:Klop, J. W.
8129:
8120:
8111:
8102:
8093:
8061:
8054:
8044:
8038:
8018:
8011:
7992:
7988:
7956:
7952:
7942:
7923:
7919:
7909:
7898:. Retrieved
7862:
7856:
7843:
7831:
7816:Maude System
7765:
7754:Martin Davis
7740:
7733:
7722:
7705:
7695:
7688:C. J. Hogger
7669:
7634:
7596:
7567:
7566:("Terese"),
7537:
7512:
7508:
7504:
7500:
7496:
7492:
7488:
7484:
7480:
7476:
7472:
7468:
7464:
7460:
7456:
7452:
7448:
7444:
7440:
7436:
7432:
7428:
7424:
7420:
7416:
7412:
7408:
7404:
7400:
7396:
7392:
7388:
7384:
7380:
7376:
7372:
7367:
7359:
7355:
7351:
7347:
7343:
7339:
7335:
7331:
7327:
7323:
7319:
7315:
7311:
7307:
7303:
7299:
7295:
7291:
7287:
7283:
7279:
7275:
7271:
7267:
7263:
7259:
7255:
7251:
7247:
7243:
7239:
7235:
7231:
7227:
7223:
7219:
7215:
7211:
7207:
7203:
7199:
7195:
7191:
7187:
7183:
7179:
7175:
7171:
7167:
7163:
7159:
7155:
7151:
7147:
7143:
7138:
7030:
7022:
7018:
7014:
7010:
7006:
7002:
6998:
6994:
6989:
6927:trace monoid
6923:Trace theory
6921:
6902:instead of (
6894:
6885:lambda terms
6882:
6866:
6807:
6392:
6389:
6294:
6220:
6029:
6018:
6011:
6009:
5403:
5037:
4874:
4730:
4726:
4661:
4655:
4653:at position
4645:
4640:
4636:
4631:to the term
4607:
4561:substitution
4555:
4538:
4533:
4502:
4497:
4492:
4486:
4452:rewrite rule
4451:
4449:
4421:term algebra
4418:
4335:§ Logic
4333:
4327:
4323:
4319:
4317:
4183:
4136:at position
4107:
4092:
4090:
4054:word problem
4007:empty string
3902:
3872:is called a
3650:
3541:
3269:
3264:
2776:
2772:
2689:
2653:
2649:
2647:
2634:in general.
2628:word problem
2614:
2609:
2605:
2542:
2538:
2472:
2468:
2464:
2460:
2456:
2455:. An ARS is
2380:
2376:
2372:
2368:
2363:. An ARS is
2251:
2247:
2243:
2239:
2209:
2180:
2176:
2133:
2129:
2128:. An object
2121:
2091:
2087:
2083:
2079:
2075:
2074:. An object
2038:
2034:
2031:word problem
1882:
1877:
1873:
1869:
1865:
1857:
1853:
1849:
1845:
1842:
1730:
1720:
1712:
1085:
1080:
1078:
700:
480:
474:Peano axioms
463:
430:
108:
75:
70:
66:
62:
58:
50:
36:
7666:Tom Maibaum
7644:Gérard Huet
7623:"Rewriting"
7350:); neither
7342:)) → ... →
6006:Termination
5245:, that is,
5009:, the term
3265:Thue system
3119:, the pair
2805:induced by
2658:free monoid
2632:undecidable
2539:terminating
2367:if for all
2210:normalizing
2126:normal form
2122:irreducible
1868:called the
1827:verb phrase
1773:noun phrase
1723:linguistics
1717:Linguistics
1081:rewrites-to
39:mathematics
8480:Categories
8465:2021-08-16
8393:2013-06-16
8353:2019-11-13
8339:2433/99946
8294:2014-06-19
7900:2019-02-12
7823:References
7699:, Volume 1
7638:, Volume 1
7556:Marc Bezem
7552:316 pages.
6692:Dershowitz
4875:If a term
4536:to a term
4011:free group
3807:isomorphic
3502:congruence
3468:, denoted
2975:such that
2694:substrings
2606:convergent
2543:noetherian
2094:such that
2082:is called
2041:, whether
460:Arithmetic
453:equivalent
8380:Proc. RTA
8156:14 August
7879:0956-7968
7764:, (1994)
7758:Ron Sigal
7166:), since
7104:∗
7083:∗
7054:∗
7045:∗
6958:L-systems
6674:⋯
6667:→
6589:→
6541:→
6478:→
6369:→
6324:→
6256:→
6152:→
6117:→
6064:→
6027:systems.
5984:∗
5975:∗
5946:∗
5925:∗
5890:∗
5881:∗
5855:∗
5834:∗
5808:∗
5779:∗
5770:∗
5747:∗
5726:∗
5682:∗
5661:∗
5623:↦
5604:↦
5591:↦
5556:∗
5547:∗
5521:∗
5500:∗
5474:∗
5451:∗
5442:∗
5433:→
5424:∗
5415:∗
5384:→
5324:→
5266:∗
5259:→
5228:→
5200:∗
5193:→
5165:→
5130:→
5088:→
5038:rewritten
4982:→
4977:⋯
4969:→
4949:→
4852:→
4819:→
4785:→
4693:σ
4619:σ
4570:σ
4517:→
4500:is a set
4469:→
4445:Tadalafil
4425:signature
4401:¬
4375:∧
4349:∨
4294:∗
4285:∗
4259:∗
4238:∗
4206:∗
4197:∗
4164:σ
4121:⟶
4067:Σ
4033:ε
4030:→
3993:ε
3970:ε
3967:→
3955:ε
3952:→
3851:Σ
3767:∗
3763:Σ
3740:∗
3733:↔
3720:∗
3716:Σ
3673:∗
3666:↔
3634:∗
3627:↔
3602:∗
3595:→
3526:∗
3519:↔
3486:∗
3479:↔
3451:→
3427:∗
3423:Σ
3419:∈
3367:∗
3360:→
3323:∗
3316:→
3288:∗
3281:→
3261:symmetric
3222:→
3178:∗
3174:Σ
3145:→
3135:∗
3131:Σ
3105:∗
3101:Σ
3075:→
2961:∗
2957:Σ
2953:∈
2904:→
2877:∗
2873:Σ
2869:∈
2838:∗
2834:Σ
2788:→
2739:Σ
2710:Σ
2617:confluent
2610:canonical
2592:⋯
2589:→
2576:→
2563:→
2520:↓
2492:→
2486:←
2440:↓
2412:∗
2409:→
2399:∗
2396:←
2365:confluent
2348:↓
2320:∗
2317:↔
2283:∗
2280:←
2270:∗
2267:→
2223:↓
2195:↓
2156:∗
2151:→
2105:→
2084:reducible
2057:∗
2054:↔
2017:→
1991:∗
1988:↔
1966:→
1942:↔
1922:→
1896:∗
1893:→
1878:reduction
1796:→
1781:morphemes
1750:→
1627:→
1524:→
1415:→
1387:⋅
1282:→
1245:⋅
1164:→
1118:⋅
989:→
884:→
779:→
664:⋅
649:→
630:⋅
605:→
595:⋅
555:→
511:→
439:→
407:∨
398:∧
389:∨
380:→
371:∧
362:∨
327:∨
318:∧
309:∨
300:→
294:∨
285:∧
255:¬
252:∧
246:¬
243:→
234:∨
225:¬
196:¬
193:∨
187:¬
184:→
175:∧
166:¬
137:→
131:¬
128:¬
82:algorithm
51:rewriting
8459:Archived
8436:42331173
8384:Archived
8344:Archived
8288:Archived
8175:(1990).
8147:Archived
7891:Archived
7887:16807490
7694:(Eds.),
7668:(Eds.),
7633:(Eds.),
7612:preprint
7536:(1999).
7515:)) → ...
7282:))) →
6948:Compiler
6937:See also
6929:and the
6808:overlaps
4839:, or as
4604:position
3985:, where
3655:. Since
3340:implies
3065:. Since
2666:alphabet
2507:implies
2429:implies
2337:implies
2248:joinable
1876:or just
1777:sentence
8378:(ed.).
8261:16 June
8179:(ed.).
7595:(Ed.),
5151:is the
4551:subterm
4547:matches
4534:applied
4532:can be
4005:is the
3500:, is a
2662:strings
2005:is the
1954:is the
1910:is the
1083:arrow.
55:formula
8434:
8424:
8069:
8026:
7885:
7877:
7772:
7606:
7574:
7544:
7286:, and
7250:))) →
6904:ground
6900:graphs
6804:linear
6025:ground
6021:linear
4184:Pic.2:
4108:Pic.1:
3039:, and
2775:. The
2731:where
2467:, and
2375:, and
2175:, and
2029:. The
1805:
45:, and
8432:S2CID
8387:(PDF)
8374:. In
8372:(PDF)
8347:(PDF)
8314:(PDF)
8255:(PDF)
8150:(PDF)
8139:(PDF)
7894:(PDF)
7883:S2CID
7853:(PDF)
7748:Other
7682:, in
7455:)) →
7411:)) →
7326:)) →
7206:)) →
6981:Notes
6908:terms
6295:and
5372:above
4733:, to
4729:, or
4637:redex
4549:some
4456:terms
4329:terms
3809:with
2698:tuple
2688:, to
2136:" if
2124:or a
1864:→ on
111:logic
105:Logic
69:, or
47:logic
8422:ISBN
8263:2013
8158:2021
8067:ISBN
8024:ISBN
7875:ISSN
7786:The
7770:ISBN
7738:LNCS
7690:and
7664:and
7629:and
7604:ISBN
7584:and
7572:ISBN
7542:ISBN
7503:)) ,
7443:)) ,
7383:) →
7354:nor
7298:) →
7178:) →
7158:and
6912:tree
6871:and
6867:See
6802:are
6721:and
4496:. A
4364:and
2242:and
2037:and
1633:s.a.
470:term
92:and
8414:doi
8334:hdl
8326:doi
8229:doi
8225:103
7997:doi
7993:285
7961:doi
7928:doi
7867:doi
7800:by
7741:277
7491:)),
6906:-)
5820:to
5309:or
5283:if
5218:of
5040:to
4659:in
4639:or
4553:of
4324:TRS
3876:of
3805:is
3259:is
2825:on
2690:all
2620:iff
2608:or
2541:or
2475:,
2471:in
2383:,
2379:in
2304:if
2238:or
2090:in
2078:in
2009:of
1958:of
1914:of
1854:ARS
1848:or
1775:or
1721:In
677:(4)
615:(3)
580:(2)
521:(1)
109:In
37:In
8482::
8430:.
8420:.
8342:.
8332:.
8322:25
8320:.
8316:.
8223:.
8217:.
8141:.
8081:^
7991:.
7987:.
7975:^
7957:37
7955:.
7951:.
7924:14
7922:.
7918:.
7889:.
7881:.
7873:.
7863:24
7861:.
7855:.
7804:,
7760:,
7756:,
7736:.
7732:,
7686:,
7660:,
7621:.
7562:,
7558:,
7532:;
7479:),
7431:),
7399:),
7314:),
7266:),
7238:),
7222:),
7194:),
7017:→
7001:=
6002:.
4806:,
4450:A
4318:A
4095:.
3900:.
3648:.
3267:.
3192:,
3007:,
2648:A
2612:.
2463:,
2371:,
2212:.
1978:.
1934:.
1880:.
1872:,
1725:,
65:,
49:,
41:,
8468:.
8438:.
8416::
8396:.
8356:.
8336::
8328::
8297:.
8265:.
8237:.
8231::
8160:.
8075:.
8032:.
8005:.
7999::
7969:.
7963::
7936:.
7930::
7903:.
7869::
7776:.
7701:.
7675:.
7640:.
7550:.
7513:c
7511:,
7509:c
7507:(
7505:h
7501:c
7499:,
7497:c
7495:(
7493:h
7489:c
7487:,
7485:c
7483:(
7481:h
7477:c
7475:,
7473:c
7471:(
7469:h
7467:(
7465:f
7463:(
7461:f
7459:(
7457:f
7453:c
7451:,
7449:c
7447:(
7445:h
7441:c
7439:,
7437:c
7435:(
7433:h
7429:c
7427:,
7425:c
7423:(
7421:h
7419:(
7417:f
7415:(
7413:f
7409:c
7407:,
7405:c
7403:(
7401:h
7397:c
7395:,
7393:c
7391:(
7389:h
7387:(
7385:f
7381:c
7379:,
7377:c
7375:(
7373:h
7360:b
7358:(
7356:g
7352:b
7348:b
7346:(
7344:g
7340:c
7338:,
7336:c
7334:(
7332:h
7330:(
7328:g
7324:c
7322:,
7320:c
7318:(
7316:h
7312:c
7310:,
7308:c
7306:(
7304:h
7302:(
7300:f
7296:c
7294:,
7292:c
7290:(
7288:h
7284:b
7280:c
7278:,
7276:c
7274:(
7272:h
7270:(
7268:g
7264:c
7262:,
7260:c
7258:(
7256:h
7254:(
7252:f
7248:c
7246:,
7244:c
7242:(
7240:h
7236:c
7234:,
7232:c
7230:(
7228:h
7226:(
7224:f
7220:c
7218:,
7216:c
7214:(
7212:h
7210:(
7208:f
7204:c
7202:,
7200:c
7198:(
7196:h
7192:c
7190:,
7188:c
7186:(
7184:h
7182:(
7180:f
7176:c
7174:,
7172:c
7170:(
7168:h
7164:b
7162:(
7160:g
7156:b
7152:c
7150:,
7148:c
7146:(
7144:h
7122:)
7119:)
7116:2
7113:+
7110:a
7107:(
7101:)
7098:1
7095:+
7092:a
7089:(
7086:(
7080:a
7060:)
7057:z
7051:y
7048:(
7042:x
7023:A
7021:∨
7019:B
7015:B
7013:∨
7011:A
7007:A
7005:∨
7003:B
6999:B
6997:∨
6995:A
6850:2
6846:R
6823:1
6819:R
6788:2
6784:R
6761:1
6757:R
6734:2
6730:R
6707:1
6703:R
6660:)
6657:)
6654:1
6651:,
6648:0
6645:(
6642:g
6639:,
6636:)
6633:1
6630:,
6627:0
6624:(
6621:g
6618:,
6615:)
6612:1
6609:,
6606:0
6603:(
6600:g
6597:(
6594:f
6582:)
6579:)
6576:1
6573:,
6570:0
6567:(
6564:g
6561:,
6558:1
6555:,
6552:0
6549:(
6546:f
6534:)
6531:)
6528:1
6525:,
6522:0
6519:(
6516:g
6513:,
6510:)
6507:1
6504:,
6501:0
6498:(
6495:g
6492:,
6489:0
6486:(
6483:f
6471:)
6468:)
6465:1
6462:,
6459:0
6456:(
6453:g
6450:,
6447:)
6444:1
6441:,
6438:0
6435:(
6432:g
6429:,
6426:)
6423:1
6420:,
6417:0
6414:(
6411:g
6408:(
6405:f
6375:.
6372:y
6366:)
6363:y
6360:,
6357:x
6354:(
6351:g
6330:,
6327:x
6321:)
6318:y
6315:,
6312:x
6309:(
6306:g
6280:)
6277:x
6274:,
6271:x
6268:,
6265:x
6262:(
6259:f
6253:)
6250:x
6247:,
6244:1
6241:,
6238:0
6235:(
6232:f
6203:.
6200:)
6197:)
6194:x
6191:,
6188:x
6185:(
6182:h
6179:,
6176:)
6173:c
6170:,
6167:x
6164:(
6161:h
6158:(
6155:f
6145:)
6142:x
6139:,
6136:c
6133:(
6130:h
6123:,
6120:b
6110:)
6107:)
6104:x
6101:(
6098:g
6095:,
6092:x
6089:(
6086:f
6079:,
6076:)
6073:x
6070:(
6067:g
6057:)
6054:x
6051:,
6048:x
6045:(
6042:f
5987:3
5981:)
5978:2
5972:1
5969:(
5964:)
5961:)
5958:2
5955:+
5952:a
5949:(
5943:)
5940:1
5937:+
5934:a
5931:(
5928:(
5922:a
5896:)
5893:3
5887:2
5884:(
5878:1
5873:)
5870:)
5867:2
5864:+
5861:a
5858:(
5852:)
5849:1
5846:+
5843:a
5840:(
5837:(
5831:a
5785:)
5782:3
5776:2
5773:(
5767:1
5762:)
5759:2
5756:+
5753:a
5750:(
5744:)
5741:)
5738:1
5735:+
5732:a
5729:(
5723:a
5720:(
5697:)
5694:2
5691:+
5688:a
5685:(
5679:)
5676:)
5673:1
5670:+
5667:a
5664:(
5658:a
5655:(
5635:}
5632:2
5629:+
5626:a
5620:z
5616:,
5613:1
5610:+
5607:a
5601:y
5597:,
5594:a
5588:x
5585:{
5562:)
5559:3
5553:2
5550:(
5544:1
5539:)
5536:)
5533:2
5530:+
5527:a
5524:(
5518:)
5515:1
5512:+
5509:a
5506:(
5503:(
5497:a
5454:z
5448:)
5445:y
5439:x
5436:(
5430:)
5427:z
5421:y
5418:(
5412:x
5387:R
5358:R
5348:.
5336:t
5331:+
5327:R
5318:s
5297:t
5294:=
5291:s
5271:t
5262:R
5253:s
5231:R
5196:R
5168:R
5137:+
5133:R
5105:n
5101:t
5095:+
5091:R
5080:1
5076:t
5053:n
5049:t
5022:1
5018:t
4995:n
4991:t
4985:R
4972:R
4962:2
4958:t
4952:R
4942:1
4938:t
4915:n
4911:t
4888:1
4884:t
4860:t
4855:R
4847:s
4827:t
4822:R
4814:s
4794:t
4789:R
4781:s
4761:R
4741:t
4713:s
4673:r
4662:s
4656:p
4646:t
4633:l
4608:p
4590:s
4556:s
4544:l
4539:s
4520:r
4514:l
4503:R
4493:r
4487:l
4472:r
4466:l
4447:.
4404:)
4398:(
4378:)
4372:(
4352:)
4346:(
4322:(
4300:)
4297:3
4291:2
4288:(
4282:1
4277:)
4274:)
4271:2
4268:+
4265:a
4262:(
4256:)
4253:1
4250:+
4247:a
4244:(
4241:(
4235:a
4212:)
4209:z
4203:y
4200:(
4194:x
4144:p
4124:r
4118:l
4076:)
4073:R
4070:,
4064:(
4036:}
4027:b
4024:a
4021:{
3973:}
3964:a
3961:b
3958:,
3949:b
3946:a
3943:{
3923:}
3920:b
3917:,
3914:a
3911:{
3886:M
3860:)
3857:R
3854:,
3848:(
3826:R
3820:M
3791:M
3736:R
3726:/
3712:=
3707:R
3701:M
3669:R
3630:R
3598:R
3572:R
3552:R
3522:R
3482:R
3454:R
3416:v
3413:,
3410:u
3407:,
3404:y
3401:,
3398:x
3378:v
3375:y
3372:u
3363:R
3354:v
3351:x
3348:u
3328:y
3319:R
3310:x
3284:R
3247:R
3225:R
3200:R
3153:)
3148:R
3140:,
3127:(
3078:R
3053:v
3050:R
3047:u
3027:y
3024:v
3021:x
3018:=
3015:t
2995:y
2992:u
2989:x
2986:=
2983:s
2950:v
2947:,
2944:u
2941:,
2938:y
2935:,
2932:x
2912:t
2907:R
2899:s
2866:t
2863:,
2860:s
2813:R
2791:R
2759:R
2719:)
2716:R
2713:,
2707:(
2676:R
2584:2
2580:x
2571:1
2567:x
2558:0
2554:x
2525:y
2515:x
2495:y
2489:w
2483:x
2473:A
2469:y
2465:x
2461:w
2443:y
2437:x
2417:y
2404:w
2391:x
2381:A
2377:y
2373:x
2369:w
2351:y
2345:x
2325:y
2312:x
2288:y
2275:z
2262:x
2252:z
2244:y
2240:x
2226:y
2220:x
2191:x
2181:x
2177:y
2163:y
2144:x
2134:x
2130:y
2108:y
2102:x
2092:A
2088:y
2080:A
2076:x
2062:y
2049:x
2039:y
2035:x
1866:A
1858:A
1811:P
1808:V
1802:P
1799:N
1793:S
1753:X
1747:A
1698:,
1695:)
1692:)
1689:)
1686:)
1683:0
1680:(
1677:S
1674:(
1671:S
1668:(
1665:S
1662:(
1659:S
1602:)
1599:)
1596:0
1593:(
1590:S
1587:(
1584:S
1581:+
1578:)
1575:)
1572:0
1569:(
1566:S
1563:(
1560:S
1535:)
1532:1
1529:(
1499:0
1496:+
1493:)
1490:)
1487:0
1484:(
1481:S
1478:(
1475:S
1472:+
1469:)
1466:)
1463:0
1460:(
1457:S
1454:(
1451:S
1426:)
1423:3
1420:(
1390:0
1384:)
1381:)
1378:0
1375:(
1372:S
1369:(
1366:S
1363:+
1360:)
1357:)
1354:0
1351:(
1348:S
1345:(
1342:S
1339:+
1336:)
1333:)
1330:0
1327:(
1324:S
1321:(
1318:S
1293:)
1290:4
1287:(
1257:)
1254:0
1251:(
1248:S
1242:)
1239:)
1236:0
1233:(
1230:S
1227:(
1224:S
1221:+
1218:)
1215:)
1212:0
1209:(
1206:S
1203:(
1200:S
1175:)
1172:4
1169:(
1139:)
1136:)
1133:0
1130:(
1127:S
1124:(
1121:S
1115:)
1112:)
1109:0
1106:(
1103:S
1100:(
1097:S
1064:,
1061:)
1058:)
1055:)
1052:)
1049:0
1046:(
1043:S
1040:(
1037:S
1034:(
1031:S
1028:(
1025:S
1000:)
997:1
994:(
964:)
961:)
957:0
954:+
951:)
948:)
945:0
942:(
939:S
936:(
933:S
929:(
926:S
923:(
920:S
895:)
892:2
889:(
859:)
855:)
852:0
849:(
846:S
843:+
840:)
837:)
834:0
831:(
828:S
825:(
822:S
818:(
815:S
790:)
787:2
784:(
754:)
751:)
748:0
745:(
742:S
739:(
736:S
733:+
730:)
727:)
724:0
721:(
718:S
715:(
712:S
682:.
670:)
667:B
661:A
658:(
655:+
652:A
642:)
639:B
636:(
633:S
627:A
620:,
608:0
598:0
592:A
585:,
573:)
570:B
567:+
564:A
561:(
558:S
548:)
545:B
542:(
539:S
536:+
533:A
526:,
514:A
504:0
501:+
498:A
481:S
416:,
413:)
410:C
404:A
401:(
395:)
392:B
386:A
383:(
377:)
374:C
368:B
365:(
359:A
349:)
345:(
333:)
330:C
324:B
321:(
315:)
312:C
306:A
303:(
297:C
291:)
288:B
282:A
279:(
258:B
249:A
240:)
237:B
231:A
228:(
215:)
211:(
199:B
190:A
181:)
178:B
172:A
169:(
156:)
152:(
140:A
134:A
34:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.