1038:
1030:
28:
62:
643:
530:
This proof starts from the given group axioms A1–A3, and establishes five propositions R4, R6, R10, R11, and R12, each of them using some earlier ones, and R12 being the main theorem. Some of the proofs require non-obvious, or even creative, steps, like applying axiom A2 in reverse, thereby rewriting
68:
The usual rules of elementary arithmetic form an abstract rewriting system. For example, the expression (11 + 9) × (2 + 4) can be evaluated starting either at the left or at the right parentheses; however, in both cases the same result is eventually obtained. If every arithmetic expression evaluates
1365:
it is confluent. Because of this equivalence, a fair bit of variation in definitions is encountered in the literature. For instance, in "Terese" the Church–Rosser property and confluence are defined to be synonymous and identical to the definition of confluence presented here; Church–Rosser as
1374:
The definition of local confluence differs from that of global confluence in that only elements reached from a given element in a single rewriting step are considered. By considering one element reached in a single step and another element reached by an arbitrary sequence, we arrive at the
69:
to the same result regardless of reduction strategy, the arithmetic rewriting system is said to be ground-confluent. Arithmetic rewriting systems may be confluent or only ground-confluent depending on details of the rewriting system.
1354:; that is the normal form of an object is unique if it exists, but it may well not exist. In lambda calculus for instance, the expression (λx.xx)(λx.xx) does not have a normal form because there exists an infinite sequence of
617:
The success of that method does not depend on a certain sophisticated order in which to apply rewrite rules, as confluence ensures that any sequence of rule applications will eventually lead to the same result (while the
1291:
49:
systems, describing which terms in such a system can be rewritten in more than one way, to yield the same result. This article describes the properties in the most abstract setting of an
1321:
951:
1668:
626:, not a tinge of creativity is required to perform proofs of term equality; that task hence becomes amenable to computer programs. Modern approaches handle more general
1347:.) In a rewriting system with the Church–Rosser property the word problem may be reduced to the search for a common successor. In a Church–Rosser system, an object has
1477:
A semi-confluent element need not be confluent, but a semi-confluent rewriting system is necessarily confluent, and a confluent system is trivially semi-confluent.
622:
property ensures that any sequence will eventually reach an end at all). Therefore, if a confluent and terminating term rewriting system can be provided for some
658:
in zero or more rewrite steps (denoted by the asterisk). In order for the rewrite relation to be confluent, both reducts must in turn reduce to some common
1485:
Strong confluence is another variation on local confluence that allows us to conclude that a rewriting system is globally confluent. An element
1181:. Since a sequence of reduction sequences is again a reduction sequence (or, equivalently, since forming the reflexive-transitive closure is
1671:, with its propositions consistently numbered. Using it, a proof of e.g. R6 consists in applying R11 and R12 in any order to the term (
17:
1230:
A rewriting system may be locally confluent without being (globally) confluent. Examples are shown in figures 1 and 2. However,
1173:, introduced as a notation for reduction sequences, may be viewed as a rewriting system in its own right, whose relation is the
539:
was to avoid the need for such steps, which are difficult to find by an inexperienced human, let alone by a computer program .
1908:
1741:
1664:
1601:
811:
of →. Using the example from the previous paragraph, we have (11+9)×(2+4) → 20×(2+4) and 20×(2+4) → 20×6, so (11+9)×(2+4)
1343:
has this property; hence the name of the property. (The fact that lambda calculus has this property is also known as the
1257:
1731:
1577:
A confluent element need not be strongly confluent, but a strongly confluent rewriting system is necessarily confluent.
1234:
states that if a locally confluent rewriting system has no infinite reduction sequences (in which case it is said to be
1174:
808:
1880:
1769:
1366:
defined here remains unnamed, but is given as an equivalent property; this departure from other texts is deliberate.
1631:
1351:
1296:
1037:
1898:
1828:
928:
1029:
1667:
can be used to compute such a system from a given set of equations. Such a system e.g. for groups is shown
1962:
670:
in which nodes represent expressions and edges represent rewrites. So, for example, if the expression
543:
1608:
1344:
50:
77:
1797:
Alonzo Church and J. Barkley Rosser. Some properties of conversion. Trans. AMS, 39:472-482, 1936
27:
1626:
1041:
Figure 2: Infinite non-cyclic, locally-confluent, but not globally confluent rewrite system
552:, a straightforward method exists to prove equality between two expressions (also known as
8:
1621:
1591:
1182:
73:
1760:
N. Dershowitz and J.-P. Jouannaud (1990). "Rewrite
Systems". In Jan van Leeuwen (ed.).
570:, apply equalities from left to right as long as possible, eventually obtaining a term
535:⋅ a" in the first step of R6's proof. One of the historical motivations to develop the
1935:
1904:
1876:
1824:
1765:
1764:. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320.
1737:
1336:
1231:
961:
is confluent, we say that → is confluent. This property is also sometimes called the
623:
1005:. The single-reduction variant is strictly stronger than the multi-reduction one.
965:, after the shape of the diagram shown on the right. Some authors reserve the term
1701:
1595:
969:
for a variant of the diagram with single reductions everywhere; that is, whenever
1868:
1340:
548:
1875:. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.
728:. Intuitively, this means that the corresponding graph has a directed edge from
61:
1938:
1362:
667:
1355:
1033:
Figure 1: Cyclic, locally-confluent, but not globally confluent rewrite system
37:
is inspired from geography, where it means the meeting of two bodies of water.
1956:
1894:
1332:
72:
A second, more abstract example is obtained from the following proof of each
1890:
554:
1155:
in one step. In analogy with this, confluence is sometimes referred to as
1018:
1139:
is locally confluent, then → is called locally confluent, or having the
1587:
33:
1943:
46:
1720:, p. 134: axiom and proposition names follow the original text
1759:
1755:
1753:
634:
rewriting systems; the latter are a special case of the former.
614:
that can be proven equal at all can be done so by that method.
1750:
1574:
is strongly confluent, we say that → is strongly confluent.
825:
With this established, confluence can be defined as follows.
642:
598:
are proven equal. More importantly, if they disagree, then
1837:
1800:
1594:
is a confluent rewrite system provided one works with a
1361:
A rewriting system possesses the Church–Rosser property
788:, indicating the existence of a reduction sequence from
1779:
1730:
Robinson, Alan J. A.; Voronkov, Andrei (5 July 2001).
1474:
is semi-confluent, we say that → is semi-confluent.
1299:
1260:
1021:
is confluent, that is, every term without variables.
931:
1849:
1823:. Boca Raton: Chapman & Hall/CRC. p. 184.
1286:{\displaystyle x{\stackrel {*}{\leftrightarrow }}y}
1933:
1315:
1285:
945:
1954:
1729:
1580:
1216:. It follows that → is confluent if and only if
1917:
1717:
1604:follows from confluence of the braid relations.
1918:Bläsius, K. H.; Bürckert, H.-J., eds. (1992).
1699:
1736:. Gulf Professional Publishing. p. 560.
712:). This is represented using arrow notation;
1889:
1843:
1806:
1654:to emphasize their left-to-right orientation
1143:. This is different from confluence in that
1607:β-reduction of λ-terms is confluent by the
739:If there is a path between two graph nodes
1316:{\displaystyle x{\mathbin {\downarrow }}y}
1250:A rewriting system is said to possess the
637:
1375:intermediate concept of semi-confluence:
1245:
946:{\displaystyle b\mathbin {\downarrow } c}
666:A rewriting system can be expressed as a
1702:"Rewrite systems for integer arithmetic"
1036:
1028:
641:
606:cannot be equal. That is, any two terms
26:
1700:Walters, H.R.; Zantema, H. (Oct 1994).
14:
1955:
1866:
1855:
1818:
1785:
1358:(λx.xx)(λx.xx) → (λx.xx)(λx.xx) → ...
56:
1934:
41:In computer science and mathematics,
1480:
1008:
1024:
24:
1369:
1242:), then it is globally confluent.
60:
25:
1974:
1927:
1665:Knuth–Bendix completion algorithm
1679:; no other rules are applicable.
1632:Normal form (abstract rewriting)
582:in a similar way. If both terms
1812:
1733:Handbook of Automated Reasoning
1903:. Cambridge University Press.
1791:
1723:
1711:
1693:
1657:
1644:
1305:
1268:
936:
13:
1:
1686:
1581:Examples of confluent systems
1175:reflexive-transitive closure
809:reflexive-transitive closure
7:
1900:Term Rewriting and All That
1762:Formal Models and Semantics
1718:Bläsius & Bürckert 1992
1615:
1141:weak Church–Rosser property
1013:A term rewriting system is
10:
1979:
1922:. Oldenbourg. p. 291.
1871:; de Vrijer, Roel (2003).
628:abstract rewriting systems
511:by R11(r)
51:abstract rewriting system
1844:Baader & Nipkow 1998
1807:Baader & Nipkow 1998
1637:
537:theory of term rewriting
227:by A3(r)
1867:"Terese"; Bezem, Marc;
1675:)⋅1 to obtain the term
751:. So, for instance, if
638:General case and theory
1873:Term rewriting systems
1819:Cooper, S. B. (2004).
1776:Here: p.268, Fig.2a+b.
1317:
1287:
1252:Church–Rosser property
1246:Church–Rosser property
1227:is locally confluent.
1042:
1034:
947:
674:can be rewritten into
663:
590:literally agree, then
76:element equalling the
65:
38:
18:Church–Rosser property
1707:. Utrecht University.
1627:Critical pair (logic)
1609:Church–Rosser theorem
1345:Church–Rosser theorem
1318:
1288:
1151:must be reduced from
1040:
1032:
985:, there must exist a
948:
645:
544:term rewriting system
64:
30:
1821:Computability theory
1339:proved in 1936 that
1297:
1258:
1240:strongly normalizing
929:
771:, then we can write
1622:Convergence (logic)
1602:Matsumoto's theorem
678:, then we say that
484:
426:
348:
273:
186:
85:
57:Motivating examples
1936:Weisstein, Eric W.
1495:strongly confluent
1313:
1283:
1043:
1035:
943:
749:reduction sequence
747:, then it forms a
664:
471:
413:
327:
260:
165:
83:
66:
39:
1963:Rewriting systems
1920:Deduktionssysteme
1910:978-0-521-77920-3
1788:, pp. 10–11.
1743:978-0-444-82949-8
1481:Strong confluence
1337:J. Barkley Rosser
1277:
1157:global confluence
1055:locally confluent
1009:Ground confluence
883:, there exists a
837:if for all pairs
646:In this diagram,
624:equational theory
546:is confluent and
528:
527:
469:
468:
411:
410:
325:
324:
258:
257:
163:
162:
45:is a property of
16:(Redirected from
1970:
1949:
1948:
1923:
1914:
1886:
1869:Klop, Jan Willem
1859:
1853:
1847:
1841:
1835:
1834:
1816:
1810:
1804:
1798:
1795:
1789:
1783:
1777:
1775:
1757:
1748:
1747:
1727:
1721:
1715:
1709:
1708:
1706:
1697:
1680:
1661:
1655:
1648:
1546:
1545:
1544:
1541:
1462:
1461:
1460:
1457:
1445:
1444:
1443:
1440:
1420:
1419:
1418:
1415:
1323:for all objects
1322:
1320:
1319:
1314:
1309:
1308:
1292:
1290:
1289:
1284:
1279:
1278:
1276:
1271:
1266:
1226:
1225:
1224:
1221:
1215:
1214:
1213:
1210:
1204:
1203:
1202:
1201:
1200:
1199:
1196:
1190:
1172:
1171:
1170:
1167:
1127:
1126:
1125:
1122:
1110:
1109:
1108:
1105:
1059:weakly confluent
1025:Local confluence
1015:ground confluent
967:diamond property
963:diamond property
952:
950:
949:
944:
939:
921:
920:
919:
916:
904:
903:
902:
899:
879:
878:
877:
874:
862:
861:
860:
857:
821:
820:
819:
816:
806:
805:
804:
801:
784:
783:
782:
779:
690:(alternatively,
661:
657:
653:
650:reduces to both
649:
566:: Starting with
485:
470:
427:
412:
349:
326:
274:
259:
187:
164:
86:
82:
80:of its inverse:
21:
1978:
1977:
1973:
1972:
1971:
1969:
1968:
1967:
1953:
1952:
1930:
1911:
1883:
1863:
1862:
1854:
1850:
1842:
1838:
1831:
1817:
1813:
1805:
1801:
1796:
1792:
1784:
1780:
1772:
1758:
1751:
1744:
1728:
1724:
1716:
1712:
1704:
1698:
1694:
1689:
1684:
1683:
1662:
1658:
1649:
1645:
1640:
1618:
1583:
1542:
1539:
1538:
1537:
1483:
1458:
1455:
1454:
1453:
1441:
1438:
1437:
1436:
1416:
1413:
1412:
1411:
1372:
1370:Semi-confluence
1341:lambda calculus
1304:
1303:
1298:
1295:
1294:
1272:
1267:
1265:
1264:
1259:
1256:
1255:
1254:if and only if
1248:
1222:
1219:
1218:
1217:
1211:
1208:
1207:
1206:
1197:
1194:
1193:
1192:
1191:
1188:
1187:
1186:
1168:
1165:
1164:
1163:
1123:
1120:
1119:
1118:
1106:
1103:
1102:
1101:
1027:
1011:
935:
930:
927:
926:
917:
914:
913:
912:
900:
897:
896:
895:
875:
872:
871:
870:
858:
855:
854:
853:
817:
814:
813:
812:
802:
799:
798:
797:
780:
777:
776:
775:
720:indicates that
659:
655:
651:
647:
640:
59:
23:
22:
15:
12:
11:
5:
1976:
1966:
1965:
1951:
1950:
1929:
1928:External links
1926:
1925:
1924:
1915:
1909:
1895:Nipkow, Tobias
1887:
1881:
1861:
1860:
1848:
1836:
1829:
1811:
1799:
1790:
1778:
1770:
1749:
1742:
1722:
1710:
1691:
1690:
1688:
1685:
1682:
1681:
1656:
1642:
1641:
1639:
1636:
1635:
1634:
1629:
1624:
1617:
1614:
1613:
1612:
1605:
1599:
1582:
1579:
1493:is said to be
1482:
1479:
1385:semi-confluent
1383:is said to be
1371:
1368:
1363:if and only if
1312:
1307:
1302:
1282:
1275:
1270:
1263:
1247:
1244:
1232:Newman's lemma
1053:is said to be
1026:
1023:
1010:
1007:
942:
938:
934:
668:directed graph
639:
636:
574:. Obtain from
526:
525:
522:
517:
513:
512:
509:
502:
498:
497:
495:
488:
467:
466:
463:
458:
454:
453:
450:
443:
439:
438:
436:
430:
409:
408:
405:
396:
392:
391:
388:
369:
365:
364:
362:
352:
323:
322:
319:
314:
310:
309:
306:
291:
287:
286:
284:
277:
256:
255:
252:
247:
243:
242:
239:
233:
229:
228:
225:
211:
207:
206:
204:
190:
161:
160:
145:
131:
124:
123:
120:
111:
105:
104:
98:
92:
58:
55:
9:
6:
4:
3:
2:
1975:
1964:
1961:
1960:
1958:
1946:
1945:
1940:
1937:
1932:
1931:
1921:
1916:
1912:
1906:
1902:
1901:
1896:
1892:
1891:Baader, Franz
1888:
1884:
1882:0-521-39115-6
1878:
1874:
1870:
1865:
1864:
1858:, p. 11.
1857:
1852:
1846:, p. 11.
1845:
1840:
1832:
1826:
1822:
1815:
1808:
1803:
1794:
1787:
1782:
1773:
1771:0-444-88074-7
1767:
1763:
1756:
1754:
1745:
1739:
1735:
1734:
1726:
1719:
1714:
1703:
1696:
1692:
1678:
1674:
1670:
1666:
1660:
1653:
1652:rewrite rules
1647:
1643:
1633:
1630:
1628:
1625:
1623:
1620:
1619:
1610:
1606:
1603:
1600:
1597:
1596:Gröbner basis
1593:
1589:
1586:Reduction of
1585:
1584:
1578:
1575:
1573:
1569:
1565:
1561:
1557:
1553:
1549:
1536:
1532:
1528:
1525:there exists
1524:
1520:
1516:
1512:
1508:
1504:
1500:
1496:
1492:
1488:
1478:
1475:
1473:
1469:
1465:
1452:
1448:
1435:
1431:
1427:
1424:there exists
1423:
1410:
1406:
1402:
1398:
1394:
1390:
1386:
1382:
1378:
1367:
1364:
1359:
1357:
1353:
1350:
1346:
1342:
1338:
1334:
1333:Alonzo Church
1330:
1326:
1310:
1300:
1280:
1273:
1261:
1253:
1243:
1241:
1237:
1233:
1228:
1184:
1180:
1176:
1162:The relation
1160:
1158:
1154:
1150:
1146:
1142:
1138:
1134:
1130:
1117:
1113:
1100:
1096:
1092:
1089:there exists
1088:
1084:
1080:
1076:
1072:
1068:
1064:
1061:) if for all
1060:
1056:
1052:
1048:
1039:
1031:
1022:
1020:
1016:
1006:
1004:
1000:
996:
992:
988:
984:
980:
976:
972:
968:
964:
960:
956:
940:
932:
924:
911:
907:
894:
890:
886:
882:
869:
865:
852:
848:
844:
840:
836:
832:
828:
823:
810:
795:
791:
787:
774:
770:
766:
762:
758:
754:
750:
746:
742:
737:
735:
731:
727:
723:
719:
715:
711:
707:
703:
699:
696:
693:
689:
685:
681:
677:
673:
669:
644:
635:
633:
629:
625:
621:
615:
613:
609:
605:
601:
597:
593:
589:
585:
581:
577:
573:
569:
565:
561:
557:
556:
551:
550:
545:
540:
538:
534:
523:
521:
518:
515:
514:
510:
507:
503:
500:
499:
496:
493:
489:
487:
486:
483:
479:
475:
464:
462:
459:
456:
455:
451:
448:
444:
441:
440:
437:
434:
431:
429:
428:
425:
421:
417:
406:
404:
400:
397:
394:
393:
389:
386:
382:
378:
374:
370:
367:
366:
363:
361:
357:
353:
351:
350:
347:
343:
339:
335:
331:
320:
318:
315:
312:
311:
307:
304:
300:
296:
292:
289:
288:
285:
282:
278:
276:
275:
272:
268:
264:
253:
251:
248:
245:
244:
240:
238:
234:
231:
230:
226:
224:
220:
216:
212:
209:
208:
205:
202:
198:
194:
191:
189:
188:
185:
181:
177:
173:
169:
158:
154:
150:
146:
144:
140:
136:
132:
130:
129:
126:
125:
121:
119:
115:
112:
110:
107:
106:
103:
99:
97:
93:
91:
88:
87:
84:Group axioms
81:
79:
75:
70:
63:
54:
52:
48:
44:
36:
35:
29:
19:
1942:
1919:
1899:
1872:
1851:
1839:
1820:
1814:
1809:, p. 9.
1802:
1793:
1781:
1761:
1732:
1725:
1713:
1695:
1676:
1672:
1659:
1651:
1650:then called
1646:
1576:
1571:
1567:
1563:
1559:
1555:
1551:
1547:
1534:
1530:
1526:
1522:
1518:
1514:
1510:
1506:
1502:
1498:
1494:
1490:
1486:
1484:
1476:
1471:
1467:
1463:
1450:
1446:
1433:
1429:
1425:
1421:
1408:
1404:
1400:
1396:
1392:
1388:
1384:
1380:
1376:
1373:
1360:
1356:β-reductions
1348:
1328:
1324:
1251:
1249:
1239:
1235:
1229:
1178:
1161:
1156:
1152:
1148:
1144:
1140:
1136:
1132:
1128:
1115:
1111:
1098:
1094:
1090:
1086:
1082:
1078:
1074:
1070:
1066:
1062:
1058:
1054:
1050:
1046:
1044:
1014:
1012:
1002:
998:
994:
990:
986:
982:
978:
974:
970:
966:
962:
958:
954:
953:). If every
922:
909:
905:
892:
888:
884:
880:
867:
863:
850:
846:
842:
838:
834:
830:
826:
824:
796:. Formally,
793:
789:
785:
772:
768:
764:
760:
756:
752:
748:
744:
740:
738:
733:
729:
725:
721:
717:
713:
709:
705:
701:
697:
694:
691:
687:
683:
679:
675:
671:
665:
631:
630:rather than
627:
619:
616:
611:
607:
603:
599:
595:
591:
587:
583:
579:
575:
571:
567:
563:
559:
553:
547:
541:
536:
532:
529:
519:
505:
491:
481:
477:
473:
460:
446:
432:
423:
419:
415:
402:
398:
384:
380:
376:
372:
359:
355:
345:
341:
337:
333:
329:
316:
302:
298:
294:
280:
270:
266:
262:
249:
236:
222:
218:
214:
200:
196:
192:
183:
179:
175:
171:
167:
156:
152:
148:
142:
138:
134:
127:
117:
113:
108:
101:
95:
89:
71:
67:
42:
40:
32:
1939:"Confluent"
1856:Terese 2003
1786:Terese 2003
1588:polynomials
1566:; if every
1550:and either
1497:if for all
1466:; if every
1387:if for all
1352:normal form
1349:at most one
1236:terminating
1131:. If every
1045:An element
1019:ground term
724:reduces to
620:termination
549:terminating
1830:1584882379
1687:References
1590:modulo an
1183:idempotent
989:such that
849:such that
833:is deemed
695:reduces to
452:by R10(r)
43:confluence
34:confluence
1944:MathWorld
1306:↓
1274:∗
1269:↔
1017:if every
937:↓
925:(denoted
835:confluent
706:expansion
472:Proof of
414:Proof of
390:by R4(r)
328:Proof of
308:by A2(r)
261:Proof of
166:Proof of
47:rewriting
31:The name
1957:Category
1897:(1998).
1616:See also
1293:implies
763:→ ... →
531:"1" to "
269:) ⋅ 1 =
807:is the
578:a term
78:inverse
1907:
1879:
1827:
1768:
1740:
822:20×6.
704:is an
684:reduct
524:by R6
465:by R6
422:⋅ 1 =
407:by R4
321:by R4
254:by A1
241:by A2
1705:(PDF)
1638:Notes
1592:ideal
1533:with
1509:with
1432:with
1399:with
1097:with
1073:with
891:with
700:, or
682:is a
555:terms
542:If a
508:) ⋅ 1
449:) ⋅ 1
375:) ⋅ (
297:) ⋅ (
283:) ⋅ 1
74:group
1905:ISBN
1877:ISBN
1825:ISBN
1766:ISBN
1738:ISBN
1669:here
1663:The
1517:and
1449:and
1407:and
1335:and
1147:and
1114:and
1081:and
1057:(or
997:and
977:and
908:and
866:and
743:and
632:term
610:and
602:and
594:and
586:and
562:and
480:) =
358:) ⋅
336:) ⋅
235:1 ⋅
221:) ⋅
182:) =
141:) ⋅
122:= 1
94:1 ⋅
1558:or
1238:or
1185:),
1177:of
1159:.
792:to
761:c′′
732:to
708:of
686:of
654:or
476:: (
474:R12
435:⋅ 1
416:R11
379:⋅ (
332:: (
330:R10
265:: (
195:⋅ (
151:⋅ (
1959::
1941:.
1893:;
1752:^
1570:∈
1562:=
1554:→
1529:∈
1521:→
1513:→
1505:∈
1501:,
1489:∈
1470:∈
1428:∈
1403:→
1395:∈
1391:,
1379:∈
1331:.
1327:,
1205:=
1135:∈
1093:∈
1085:→
1077:→
1069:∈
1065:,
1049:∈
1001:→
993:→
981:→
973:→
957:∈
887:∈
845:∈
841:,
829:∈
767:→
765:d′
759:→
757:c′
755:→
736:.
716:→
588:t′
584:s′
580:t′
572:s′
558:)
418::
401:⋅
387:))
383:⋅
344:⋅
340:=
301:⋅
263:R6
217:⋅
199:⋅
174:⋅(
170::
168:R4
159:)
155:⋅
147:=
137:⋅
128:A3
116:⋅
109:A2
100:=
90:A1
53:.
1947:.
1913:.
1885:.
1833:.
1774:.
1746:.
1677:a
1673:a
1611:.
1598:.
1572:S
1568:a
1564:d
1560:c
1556:d
1552:c
1548:d
1543:→
1540:∗
1535:b
1531:S
1527:d
1523:c
1519:a
1515:b
1511:a
1507:S
1503:c
1499:b
1491:S
1487:a
1472:S
1468:a
1464:d
1459:→
1456:∗
1451:c
1447:d
1442:→
1439:∗
1434:b
1430:S
1426:d
1422:c
1417:→
1414:∗
1409:a
1405:b
1401:a
1397:S
1393:c
1389:b
1381:S
1377:a
1329:y
1325:x
1311:y
1301:x
1281:y
1262:x
1223:→
1220:∗
1212:→
1209:∗
1198:→
1195:∗
1189:∗
1179:→
1169:→
1166:∗
1153:a
1149:c
1145:b
1137:S
1133:a
1129:d
1124:→
1121:∗
1116:c
1112:d
1107:→
1104:∗
1099:b
1095:S
1091:d
1087:c
1083:a
1079:b
1075:a
1071:S
1067:c
1063:b
1051:S
1047:a
1003:d
999:c
995:d
991:b
987:d
983:c
979:a
975:b
971:a
959:S
955:a
941:c
933:b
923:d
918:→
915:∗
910:c
906:d
901:→
898:∗
893:b
889:S
885:d
881:c
876:→
873:∗
868:a
864:b
859:→
856:∗
851:a
847:S
843:c
839:b
831:S
827:a
818:→
815:∗
803:→
800:∗
794:d
790:c
786:d
781:→
778:∗
773:c
769:d
753:c
745:d
741:c
734:b
730:a
726:b
722:a
718:b
714:a
710:b
702:a
698:b
692:a
688:a
680:b
676:b
672:a
662:.
660:d
656:c
652:b
648:a
612:t
608:s
604:t
600:s
596:t
592:s
576:t
568:s
564:t
560:s
533:a
520:a
516:=
506:a
504:(
501:=
494:)
492:a
490:(
482:a
478:a
461:a
457:=
447:a
445:(
442:=
433:a
424:a
420:a
403:b
399:a
395:=
385:b
381:a
377:a
373:a
371:(
368:=
360:b
356:a
354:(
346:b
342:a
338:b
334:a
317:a
313:=
305:)
303:a
299:a
295:a
293:(
290:=
281:a
279:(
271:a
267:a
250:b
246:=
237:b
232:=
223:b
219:a
215:a
213:(
210:=
203:)
201:b
197:a
193:a
184:b
180:b
178:⋅
176:a
172:a
157:c
153:b
149:a
143:c
139:b
135:a
133:(
118:a
114:a
102:a
96:a
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
