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