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