129:
33:
74:
2814:
3206:
325:
and coinductive logic programming, which in turn generalizes other extensions of logic programming, such as infinite trees, lazy predicates, and concurrent communicating predicates. Co-LP has applications to rational trees, verifying infinitary properties, lazy evaluation,
2634:
2014:
3055:
3061:
2200:, but it is nonetheless useful in programming and can be reasoned about. In any case, a stream is an infinite list of elements from which you may observe the first element, or place an element in front of to get another stream.
3533:
1397:
2623:
2448:
2877:
1483:
3586:
2809:{\displaystyle \mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ F(\mathrm {out} )=F\left({\overline {F(\mathrm {out} )}}\circ \mathrm {out} \right)}
518:
2346:
1931:
1783:
3870:
1883:
1939:
2049:
1818:
1281:
1194:
3660:
318:. Informally, rather than defining a function by pattern-matching on each of the inductive constructors, one defines each of the "destructors" or "observers" over the function result.
2913:
1311:
459:
2971:
3250:
3694:
2520:
1011:
953:
3802:
2090:
631:
587:
3348:
2286:
3740:
1099:
1512:
2483:
1684:
1552:
1331:
675:
3273:
2936:
2543:
2375:
1838:
1734:
1657:
1626:
1237:
1217:
1042:
884:
853:
727:
3760:
3718:
3450:
3293:
2238:
1704:
1592:
1572:
1532:
1123:
1070:
978:
920:
830:
791:
767:
747:
698:
541:
416:
396:
3201:{\displaystyle \mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ \mathrm {out} )=\mathrm {id} _{F(\nu F)}}
2979:
4167:
3462:
1336:
150:
143:
92:
2555:
1021:
The principles, as stated, are somewhat opaque, but can be usefully thought of in the following way. Suppose you wish to prove a property of
4122:
2383:
4126:
4085:
370:, it is useful to consider their somewhat generalized forms at once. In order to state the principles, a few preliminaries are required.
2822:
1405:
3541:
639:
467:
2292:
1895:
1747:
4196:
4047:
2093:
193:
3813:
2009:{\displaystyle \bot \times \bot \times \cdots =(\bot \times \bot \times \cdots )\times (\bot \times \bot \times \cdots )}
1850:
165:
2026:
1791:
1242:
1147:
230:
212:
110:
60:
3594:
172:
299:, coinduction describes how an object may be "observed", "broken down" or "destructed" into simpler objects. As a
4216:
4206:
3417:
These are easily seen to be mutually inverse, witnessing the isomorphism. See the reference for more details.
252:
3956:
339:
179:
2886:
1286:
424:
3908:
2941:
327:
46:
3980:
3214:
2020:
2197:
3668:
161:
4201:
2488:
805:
419:
304:
21:
987:
929:
3772:
2054:
601:
557:
296:
4011:
3312:
2250:
4211:
4113:
4163:
3723:
139:
4027:
1075:
4146:
4108:
4006:
3422:
1491:
266:
2456:
1669:
1537:
1316:
1239:, and (non-homogenous) lists. These types can be identified with strings over the alphabet
645:
3255:
2918:
2525:
2357:
1823:
1716:
1639:
1608:
1222:
1202:
1024:
866:
835:
270:
703:
8:
3050:{\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} =\mathrm {id} _{\nu F}}
321:
In programming, co-logic programming (co-LP for brevity) "is a natural generalization of
186:
3976:
3745:
3703:
3435:
3278:
2223:
2105:
1689:
1577:
1557:
1517:
1108:
1055:
963:
905:
815:
776:
752:
732:
683:
526:
401:
381:
289:
256:
797:
when all of your assertions are supported by other assertions (i.e. there are no "non-
4141:
4043:
2019:
The formal justification of this is technical and depends on interpreting strings as
322:
88:
4130:
4159:
4102:
4081:
4071:
4035:
2241:
244:
52:
3528:{\displaystyle 0\in P\land (n\in P\Rightarrow n+1\in P)\Rightarrow P=\mathbb {N} }
1392:{\displaystyle F:2^{\Sigma ^{\leq \omega }}\rightarrow 2^{\Sigma ^{\leq \omega }}}
4002:
3453:
315:
285:
17:
4039:
4034:. Lecture Notes in Computer Science. Vol. 7470. Springer. pp. 47–129.
303:
technique, it may be used to show that an equation is satisfied by all possible
4107:"A Tutorial on Co-induction and Functional Programming". 1994. pp. 78–95.
331:
4134:
680:
These terms can be intuitively understood in the following way. Suppose that
16:
This article is about computer science. For the term in abstract algebra, see
4190:
2218:
4180:
3998:
3928:
3898:
338:
proofs, etc." Experimental implementations of co-LP are available from the
335:
300:
1666:
To arrive at this conclusion, consider the set of all finite strings over
3903:
3893:
3888:
2618:{\displaystyle {\overline {F(\mathrm {out} )}}:F(\nu F)\rightarrow \nu F}
2205:
311:
347:
263:
2443:{\displaystyle \mathrm {out} :\nu F\rightarrow F(\nu F)=A\times \nu F}
1135:
1072:
for which the property holds. Dually, suppose you wish to show that
890:
sets. We can now state the principles of induction and coinduction.
773:
when you cannot conclude anymore than you've already asserted, while
274:
3456:. We will take the following definition of mathematical induction:
128:
2872:{\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} }
282:
4181:
Co-Logic
Programming: Extending Logic Programming with Coinduction
3957:"Logtalk3/Examples/Coinduction at master · LogtalkDotOrg/Logtalk3"
3942:
2099:
343:
251:
is a technique for defining and proving properties of systems of
3961:
1706:
cannot produce an infinite string, so it turns out this set is
1574:." We should now define our set of datatypes as a fixpoint of
1478:{\displaystyle F(X)=\{\bot ,\top \}\cup \{x\times y:x,y\in X\}}
3581:{\displaystyle F:2^{\mathbb {N} }\rightarrow 2^{\mathbb {N} }}
2051:. Intuitively, the argument is similar to the argument that
4137:) — describes induction and coinduction simultaneously
20:. For the use of this term in medicine and anaesthesia, see
3420:
513:{\displaystyle X\subseteq Y\Rightarrow F(X)\subseteq F(Y)}
3997:
2341:{\displaystyle F(f)=\langle \mathrm {id} _{A},f\rangle }
1926:{\displaystyle \bot \times \bot \times \cdots \in \nu F}
1778:{\displaystyle \bot \times \bot \times \cdots \in \nu F}
366:. While this article is not primarily concerned with
310:
To generate and manipulate codata, one typically uses
4168:
3816:
3775:
3748:
3726:
3706:
3671:
3597:
3544:
3465:
3438:
3315:
3281:
3258:
3217:
3064:
2982:
2944:
2921:
2889:
2825:
2637:
2558:
2528:
2491:
2459:
2386:
2360:
2295:
2253:
2226:
2057:
2029:
1942:
1898:
1853:
1826:
1794:
1750:
1719:
1692:
1672:
1642:
1611:
1580:
1560:
1540:
1520:
1494:
1408:
1339:
1319:
1289:
1245:
1225:
1205:
1199:
That is, the set of types includes the "bottom type"
1150:
1111:
1078:
1058:
1027:
990:
966:
932:
908:
869:
838:
818:
779:
755:
735:
706:
686:
648:
604:
560:
529:
470:
427:
404:
384:
2938:
is final, this homomorphism is unique and therefore
4183:— describes the co-logic programming paradigm
3865:{\displaystyle \{0\}\cup \{x+1:x\in P\}\subseteq P}
1878:{\displaystyle \{\bot \times \bot \times \cdots \}}
1736:as our set of datatypes. We would like to use the
83:
may be too technical for most readers to understand
3864:
3796:
3754:
3734:
3712:
3688:
3654:
3580:
3527:
3444:
3342:
3287:
3267:
3244:
3200:
3049:
2965:
2930:
2907:
2871:
2808:
2617:
2537:
2514:
2477:
2442:
2369:
2340:
2280:
2232:
2084:
2043:
2008:
1925:
1877:
1832:
1812:
1777:
1728:
1698:
1678:
1651:
1620:
1586:
1566:
1546:
1526:
1506:
1477:
1391:
1325:
1305:
1275:
1231:
1211:
1188:
1117:
1093:
1064:
1036:
1005:
972:
947:
914:
878:
847:
824:
785:
761:
741:
721:
692:
669:
625:
581:
535:
512:
453:
410:
390:
3929:"Co-Logic Programming | Lambda the Ultimate"
2203:
1933:. This depends on the suspicious statement that
729:is the operation that yields the consequences of
4188:
4090:Advanced Topics in Bisimulation and Coinduction
2377:has the following morphism associated with it:
2044:{\displaystyle \mathbb {N} \rightarrow \Sigma }
1813:{\displaystyle \bot \times \bot \times \cdots }
1276:{\displaystyle \Sigma =\{\bot ,\top ,\times \}}
1189:{\displaystyle T=\bot \;|\;\top \;|\;T\times T}
4164:On the Origins of Bisimulation and Coinduction
3975:
3298:
2100:Coinductive datatypes in programming languages
1133:
3655:{\displaystyle F(X)=\{0\}\cup \{x+1:x\in X\}}
1141:Consider the following grammar of datatypes:
358:In a concise statement is given of both the
4140:Eduardo Giménez and Pierre Castéran (2007).
4131:A Tutorial on (Co)Algebras and (Co)Induction
4076:Introduction to Bisimulation and Coinduction
3853:
3829:
3823:
3817:
3649:
3625:
3619:
3613:
3252:, which in categorical terms indicates that
2335:
2311:
1872:
1854:
1820:denotes the infinite list consisting of all
1472:
1442:
1436:
1424:
1313:denote all (possibly infinite) strings over
1270:
1252:
4119:— mathematically oriented description
3350:. Consider the following implementations:
2196:This would seem to be a definition that is
61:Learn how and when to remove these messages
4025:
1176:
1170:
1166:
1160:
4112:
4010:
3728:
3682:
3572:
3557:
3521:
2031:
231:Learn how and when to remove this message
213:Learn how and when to remove this message
111:Learn how and when to remove this message
95:, without removing the technical details.
3665:It should not be difficult to see that
2104:Consider the following definition of a
4189:
4142:"A Tutorial on Inductive Types in Coq"
4028:"Generic Programming with Adjunctions"
3309:is the final coalgebra of the functor
2908:{\displaystyle \nu F\rightarrow \nu F}
1306:{\displaystyle \Sigma ^{\leq \omega }}
855:) is given by the intersection of all
454:{\displaystyle 2^{U}\rightarrow 2^{U}}
149:Please improve this article by adding
3432:subsumes mathematical induction. Let
2966:{\displaystyle \mathrm {id} _{\nu F}}
1594:, but it matters whether we take the
93:make it understandable to non-experts
3700:, if we wish to prove some property
3245:{\displaystyle \nu F\simeq F(\nu F)}
1632:, we can prove the following claim:
1628:as our set of datatypes. Using the
122:
67:
26:
1514:means "the concatenation of string
13:
4060:
3689:{\displaystyle \mu F=\mathbb {N} }
3176:
3173:
3161:
3158:
3155:
3134:
3131:
3128:
3095:
3092:
3089:
3072:
3069:
3066:
3034:
3031:
3022:
3019:
3016:
2999:
2996:
2993:
2950:
2947:
2865:
2862:
2859:
2842:
2839:
2836:
2797:
2794:
2791:
2774:
2771:
2768:
2740:
2737:
2734:
2707:
2704:
2701:
2668:
2665:
2662:
2645:
2642:
2639:
2575:
2572:
2569:
2505:
2502:
2499:
2394:
2391:
2388:
2319:
2316:
2038:
1994:
1988:
1970:
1964:
1949:
1943:
1905:
1899:
1863:
1857:
1827:
1801:
1795:
1757:
1751:
1673:
1433:
1427:
1375:
1352:
1320:
1291:
1261:
1255:
1246:
1226:
1206:
1167:
1157:
1101:. Then it suffices to exhibit an
14:
4228:
3981:"Types and Programming Languages"
2515:{\displaystyle F(\mathrm {out} )}
2143:-- Stream "destructors"
42:This article has multiple issues.
1006:{\displaystyle X\subseteq \nu F}
948:{\displaystyle \mu F\subseteq X}
543:will be assumed to be monotone.
373:
127:
72:
31:
4032:Generic and Indexed Programming
3797:{\displaystyle F(P)\subseteq P}
3211:This witnesses the isomorphism
2453:This induces another coalgebra
2085:{\displaystyle 0.{\bar {0}}1=0}
886:) is given by the union of all
626:{\displaystyle X\subseteq F(X)}
582:{\displaystyle F(X)\subseteq X}
314:functions, in conjunction with
50:or discuss these issues on the
4019:
3991:
3969:
3949:
3935:
3921:
3785:
3779:
3607:
3601:
3563:
3511:
3508:
3490:
3478:
3343:{\displaystyle F(x)=A\times x}
3325:
3319:
3239:
3230:
3193:
3184:
3165:
3138:
3124:
3099:
3085:
3003:
2989:
2896:
2846:
2832:
2778:
2764:
2744:
2730:
2711:
2697:
2672:
2658:
2606:
2603:
2594:
2579:
2565:
2509:
2495:
2472:
2463:
2422:
2413:
2407:
2305:
2299:
2281:{\displaystyle F(x)=A\times x}
2263:
2257:
2067:
2035:
2003:
1985:
1979:
1961:
1740:to prove the following claim:
1418:
1412:
1366:
1172:
1162:
716:
710:
664:
658:
620:
614:
570:
564:
507:
501:
492:
486:
480:
438:
353:
1:
4092:. Cambridge University Press.
4078:. Cambridge University Press.
3914:
2549:, there is a unique morphism
1016:
893:
340:University of Texas at Dallas
151:secondary or tertiary sources
4197:Theoretical computer science
3909:Total functional programming
3735:{\displaystyle \mathbb {N} }
3428:We will demonstrate how the
3295:and justifies the notation.
3142:
3103:
3007:
2850:
2782:
2715:
2676:
2583:
1710:and the conclusion follows.
1125:is known to be a member of.
1048:, it suffices to exhibit an
700:is a set of assertions, and
328:concurrent logic programming
7:
4040:10.1007/978-3-642-32202-0_2
4005:. "Practical Coinduction".
3882:
3742:, it suffices to show that
3299:Stream as a final coalgebra
1128:
10:
4233:
4170:, Vol. 31, Nb 4, Mai 2009.
4149:— short introduction
3766:. In detail, we require:
3538:Now consider the function
1094:{\displaystyle x\in \nu F}
22:coinduction (anaesthetics)
15:
3943:"Gopal Gupta's Home Page"
2485:with associated morphism
1888:This set turns out to be
1713:Now suppose that we take
1507:{\displaystyle x\times y}
1333:. Consider the function
523:Unless otherwise stated,
346:(for examples see ) and
307:of such a specification.
3352:
2883:-coalgebra homomorphism
2478:{\displaystyle F(\nu F)}
2110:
1842:principle of coinduction
1738:principle of coinduction
958:Principle of coinduction
801:-logical assumptions").
364:principle of coinduction
273:. Coinductively defined
2973:. Altogether we have:
1679:{\displaystyle \Sigma }
1547:{\displaystyle \times }
1326:{\displaystyle \Sigma }
4217:Mathematical induction
4207:Functional programming
3877:mathematical induction
3866:
3798:
3756:
3736:
3714:
3698:principle of induction
3690:
3656:
3582:
3529:
3446:
3430:principle of induction
3423:mathematical induction
3344:
3289:
3269:
3246:
3202:
3051:
2967:
2932:
2909:
2873:
2810:
2619:
2539:
2516:
2479:
2444:
2371:
2342:
2282:
2234:
2086:
2045:
2023:, i.e. functions from
2010:
1927:
1879:
1834:
1814:
1779:
1730:
1700:
1680:
1653:
1630:principle of induction
1622:
1588:
1568:
1548:
1528:
1508:
1479:
1393:
1327:
1307:
1277:
1233:
1213:
1190:
1119:
1095:
1066:
1046:principle of induction
1038:
1007:
974:
949:
916:
900:Principle of induction
880:
849:
826:
806:Knaster–Tarski theorem
787:
763:
743:
723:
694:
671:
670:{\displaystyle X=F(X)}
627:
583:
537:
514:
455:
412:
392:
360:principle of induction
138:relies excessively on
3867:
3799:
3757:
3737:
3715:
3696:. Therefore, by the
3691:
3657:
3583:
3530:
3447:
3345:
3290:
3270:
3268:{\displaystyle \nu F}
3247:
3203:
3052:
2968:
2933:
2931:{\displaystyle \nu F}
2910:
2874:
2811:
2620:
2540:
2538:{\displaystyle \nu F}
2517:
2480:
2445:
2372:
2370:{\displaystyle \nu F}
2343:
2283:
2235:
2087:
2046:
2011:
1928:
1880:
1835:
1833:{\displaystyle \bot }
1815:
1780:
1731:
1729:{\displaystyle \nu F}
1701:
1681:
1654:
1652:{\displaystyle \mu F}
1623:
1621:{\displaystyle \mu F}
1589:
1569:
1549:
1529:
1509:
1480:
1394:
1328:
1308:
1278:
1234:
1232:{\displaystyle \top }
1214:
1212:{\displaystyle \bot }
1191:
1120:
1096:
1067:
1039:
1037:{\displaystyle \mu F}
1008:
975:
950:
917:
881:
879:{\displaystyle \nu F}
850:
848:{\displaystyle \mu F}
827:
788:
764:
744:
724:
695:
672:
628:
584:
538:
515:
456:
413:
393:
3814:
3773:
3746:
3724:
3704:
3669:
3595:
3542:
3463:
3452:be some property of
3436:
3313:
3279:
3256:
3215:
3062:
2980:
2942:
2919:
2887:
2823:
2635:
2556:
2526:
2489:
2457:
2384:
2358:
2293:
2251:
2224:
2055:
2027:
1940:
1896:
1851:
1844:, consider the set:
1824:
1792:
1748:
1717:
1690:
1670:
1640:
1609:
1578:
1558:
1538:
1518:
1492:
1406:
1337:
1317:
1287:
1243:
1223:
1203:
1148:
1109:
1076:
1056:
1025:
988:
964:
930:
906:
867:
861:greatest fixed-point
836:
816:
777:
753:
733:
722:{\displaystyle F(X)}
704:
684:
646:
602:
558:
527:
468:
425:
402:
382:
342:and in the language
271:structural induction
4026:Ralf Hinze (2012).
295:As a definition or
262:Coinduction is the
4097:Introductory texts
3977:Benjamin C. Pierce
3875:This is precisely
3862:
3794:
3752:
3732:
3710:
3686:
3652:
3578:
3525:
3442:
3421:Relationship with
3340:
3303:We will show that
3285:
3265:
3242:
3198:
3047:
2963:
2928:
2905:
2869:
2806:
2615:
2535:
2512:
2475:
2440:
2367:
2338:
2278:
2230:
2204:Relationship with
2082:
2041:
2006:
1923:
1875:
1830:
1810:
1775:
1726:
1696:
1676:
1649:
1618:
1584:
1564:
1544:
1524:
1504:
1475:
1389:
1323:
1303:
1273:
1229:
1209:
1186:
1134:Defining a set of
1115:
1091:
1062:
1034:
1003:
970:
945:
912:
876:
845:
822:
808:tells us that the
783:
759:
739:
719:
690:
667:
623:
579:
533:
510:
451:
408:
388:
281:and are typically
4202:Logic programming
4049:978-3-642-32201-3
3755:{\displaystyle P}
3713:{\displaystyle P}
3445:{\displaystyle P}
3288:{\displaystyle F}
3275:is a fixpoint of
3145:
3106:
3010:
2853:
2785:
2718:
2679:
2586:
2353:final F-coalgebra
2233:{\displaystyle F}
2094:Repeating decimal
2070:
1699:{\displaystyle F}
1636:All datatypes in
1587:{\displaystyle F}
1567:{\displaystyle y}
1527:{\displaystyle x}
1488:In this context,
1219:, the "top type"
1118:{\displaystyle x}
1065:{\displaystyle X}
973:{\displaystyle X}
915:{\displaystyle X}
825:{\displaystyle F}
810:least fixed-point
786:{\displaystyle X}
762:{\displaystyle X}
742:{\displaystyle X}
693:{\displaystyle X}
536:{\displaystyle F}
420:monotone function
411:{\displaystyle F}
391:{\displaystyle U}
323:logic programming
241:
240:
233:
223:
222:
215:
197:
121:
120:
113:
65:
4224:
4160:Davide Sangiorgi
4118:
4116:
4103:Andrew D. Gordon
4082:Davide Sangiorgi
4072:Davide Sangiorgi
4054:
4053:
4023:
4017:
4016:
4014:
3995:
3989:
3988:
3973:
3967:
3966:
3953:
3947:
3946:
3939:
3933:
3932:
3925:
3871:
3869:
3868:
3863:
3803:
3801:
3800:
3795:
3761:
3759:
3758:
3753:
3741:
3739:
3738:
3733:
3731:
3719:
3717:
3716:
3711:
3695:
3693:
3692:
3687:
3685:
3661:
3659:
3658:
3653:
3587:
3585:
3584:
3579:
3577:
3576:
3575:
3562:
3561:
3560:
3534:
3532:
3531:
3526:
3524:
3451:
3449:
3448:
3443:
3413:
3410:
3407:
3404:
3401:
3398:
3395:
3392:
3389:
3386:
3383:
3380:
3377:
3374:
3371:
3368:
3365:
3362:
3359:
3356:
3349:
3347:
3346:
3341:
3294:
3292:
3291:
3286:
3274:
3272:
3271:
3266:
3251:
3249:
3248:
3243:
3207:
3205:
3204:
3199:
3197:
3196:
3179:
3164:
3150:
3146:
3141:
3137:
3119:
3107:
3102:
3098:
3080:
3075:
3056:
3054:
3053:
3048:
3046:
3045:
3037:
3025:
3011:
3006:
3002:
2984:
2972:
2970:
2969:
2964:
2962:
2961:
2953:
2937:
2935:
2934:
2929:
2914:
2912:
2911:
2906:
2879:induces another
2878:
2876:
2875:
2870:
2868:
2854:
2849:
2845:
2827:
2819:The composition
2815:
2813:
2812:
2807:
2805:
2801:
2800:
2786:
2781:
2777:
2759:
2743:
2723:
2719:
2714:
2710:
2692:
2680:
2675:
2671:
2653:
2648:
2624:
2622:
2621:
2616:
2587:
2582:
2578:
2560:
2544:
2542:
2541:
2536:
2521:
2519:
2518:
2513:
2508:
2484:
2482:
2481:
2476:
2449:
2447:
2446:
2441:
2397:
2376:
2374:
2373:
2368:
2347:
2345:
2344:
2339:
2328:
2327:
2322:
2287:
2285:
2284:
2279:
2242:category of sets
2239:
2237:
2236:
2231:
2198:not well-founded
2192:
2189:
2186:
2183:
2180:
2177:
2174:
2171:
2168:
2165:
2162:
2159:
2156:
2153:
2150:
2147:
2144:
2141:
2138:
2135:
2132:
2129:
2126:
2123:
2120:
2117:
2114:
2091:
2089:
2088:
2083:
2072:
2071:
2063:
2050:
2048:
2047:
2042:
2034:
2015:
2013:
2012:
2007:
1932:
1930:
1929:
1924:
1892:, and therefore
1884:
1882:
1881:
1876:
1839:
1837:
1836:
1831:
1819:
1817:
1816:
1811:
1784:
1782:
1781:
1776:
1735:
1733:
1732:
1727:
1705:
1703:
1702:
1697:
1685:
1683:
1682:
1677:
1658:
1656:
1655:
1650:
1627:
1625:
1624:
1619:
1605:Suppose we take
1593:
1591:
1590:
1585:
1573:
1571:
1570:
1565:
1553:
1551:
1550:
1545:
1533:
1531:
1530:
1525:
1513:
1511:
1510:
1505:
1484:
1482:
1481:
1476:
1398:
1396:
1395:
1390:
1388:
1387:
1386:
1385:
1365:
1364:
1363:
1362:
1332:
1330:
1329:
1324:
1312:
1310:
1309:
1304:
1302:
1301:
1282:
1280:
1279:
1274:
1238:
1236:
1235:
1230:
1218:
1216:
1215:
1210:
1195:
1193:
1192:
1187:
1175:
1165:
1124:
1122:
1121:
1116:
1100:
1098:
1097:
1092:
1071:
1069:
1068:
1063:
1043:
1041:
1040:
1035:
1012:
1010:
1009:
1004:
979:
977:
976:
971:
954:
952:
951:
946:
921:
919:
918:
913:
885:
883:
882:
877:
859:sets, while the
854:
852:
851:
846:
831:
829:
828:
823:
792:
790:
789:
784:
768:
766:
765:
760:
748:
746:
745:
740:
728:
726:
725:
720:
699:
697:
696:
691:
676:
674:
673:
668:
632:
630:
629:
624:
588:
586:
585:
580:
542:
540:
539:
534:
519:
517:
516:
511:
460:
458:
457:
452:
450:
449:
437:
436:
417:
415:
414:
409:
397:
395:
394:
389:
245:computer science
236:
229:
218:
211:
207:
204:
198:
196:
155:
131:
123:
116:
109:
105:
102:
96:
76:
75:
68:
57:
35:
34:
27:
4232:
4231:
4227:
4226:
4225:
4223:
4222:
4221:
4212:Category theory
4187:
4186:
4106:
4063:
4061:Further reading
4058:
4057:
4050:
4024:
4020:
4012:10.1.1.252.3961
4003:Alexandra Silva
3996:
3992:
3974:
3970:
3955:
3954:
3950:
3941:
3940:
3936:
3927:
3926:
3922:
3917:
3885:
3815:
3812:
3811:
3774:
3771:
3770:
3747:
3744:
3743:
3727:
3725:
3722:
3721:
3705:
3702:
3701:
3681:
3670:
3667:
3666:
3596:
3593:
3592:
3571:
3570:
3566:
3556:
3555:
3551:
3543:
3540:
3539:
3520:
3464:
3461:
3460:
3454:natural numbers
3437:
3434:
3433:
3426:
3415:
3414:
3411:
3408:
3405:
3402:
3399:
3396:
3393:
3390:
3387:
3384:
3381:
3378:
3375:
3372:
3369:
3366:
3363:
3360:
3357:
3354:
3314:
3311:
3310:
3307:
3301:
3280:
3277:
3276:
3257:
3254:
3253:
3216:
3213:
3212:
3180:
3172:
3171:
3154:
3127:
3120:
3118:
3114:
3088:
3081:
3079:
3065:
3063:
3060:
3059:
3038:
3030:
3029:
3015:
2992:
2985:
2983:
2981:
2978:
2977:
2954:
2946:
2945:
2943:
2940:
2939:
2920:
2917:
2916:
2888:
2885:
2884:
2858:
2835:
2828:
2826:
2824:
2821:
2820:
2790:
2767:
2760:
2758:
2757:
2753:
2733:
2700:
2693:
2691:
2687:
2661:
2654:
2652:
2638:
2636:
2633:
2632:
2568:
2561:
2559:
2557:
2554:
2553:
2527:
2524:
2523:
2498:
2490:
2487:
2486:
2458:
2455:
2454:
2387:
2385:
2382:
2381:
2359:
2356:
2355:
2323:
2315:
2314:
2294:
2291:
2290:
2252:
2249:
2248:
2225:
2222:
2221:
2212:
2194:
2193:
2190:
2187:
2184:
2181:
2178:
2175:
2172:
2169:
2166:
2163:
2160:
2157:
2154:
2151:
2148:
2145:
2142:
2139:
2136:
2133:
2130:
2127:
2124:
2121:
2118:
2115:
2112:
2102:
2062:
2061:
2056:
2053:
2052:
2030:
2028:
2025:
2024:
1941:
1938:
1937:
1897:
1894:
1893:
1852:
1849:
1848:
1825:
1822:
1821:
1793:
1790:
1789:
1749:
1746:
1745:
1718:
1715:
1714:
1691:
1688:
1687:
1671:
1668:
1667:
1641:
1638:
1637:
1610:
1607:
1606:
1579:
1576:
1575:
1559:
1556:
1555:
1539:
1536:
1535:
1519:
1516:
1515:
1493:
1490:
1489:
1407:
1404:
1403:
1378:
1374:
1373:
1369:
1355:
1351:
1350:
1346:
1338:
1335:
1334:
1318:
1315:
1314:
1294:
1290:
1288:
1285:
1284:
1244:
1241:
1240:
1224:
1221:
1220:
1204:
1201:
1200:
1171:
1161:
1149:
1146:
1145:
1139:
1131:
1110:
1107:
1106:
1077:
1074:
1073:
1057:
1054:
1053:
1026:
1023:
1022:
1019:
989:
986:
985:
965:
962:
961:
931:
928:
927:
907:
904:
903:
896:
868:
865:
864:
837:
834:
833:
817:
814:
813:
778:
775:
774:
754:
751:
750:
734:
731:
730:
705:
702:
701:
685:
682:
681:
647:
644:
643:
603:
600:
599:
559:
556:
555:
528:
525:
524:
469:
466:
465:
445:
441:
432:
428:
426:
423:
422:
403:
400:
399:
383:
380:
379:
376:
356:
316:lazy evaluation
305:implementations
286:data structures
237:
226:
225:
224:
219:
208:
202:
199:
156:
154:
148:
144:primary sources
132:
117:
106:
100:
97:
89:help improve it
86:
77:
73:
36:
32:
25:
18:Change of rings
12:
11:
5:
4230:
4220:
4219:
4214:
4209:
4204:
4199:
4185:
4184:
4177:
4176:
4172:
4171:
4156:
4155:
4151:
4150:
4144:
4138:
4135:alternate link
4120:
4114:10.1.1.37.3914
4099:
4098:
4094:
4093:
4079:
4068:
4067:
4062:
4059:
4056:
4055:
4048:
4018:
3990:
3968:
3948:
3934:
3919:
3918:
3916:
3913:
3912:
3911:
3906:
3901:
3896:
3891:
3884:
3881:
3873:
3872:
3861:
3858:
3855:
3852:
3849:
3846:
3843:
3840:
3837:
3834:
3831:
3828:
3825:
3822:
3819:
3805:
3804:
3793:
3790:
3787:
3784:
3781:
3778:
3751:
3730:
3709:
3684:
3680:
3677:
3674:
3663:
3662:
3651:
3648:
3645:
3642:
3639:
3636:
3633:
3630:
3627:
3624:
3621:
3618:
3615:
3612:
3609:
3606:
3603:
3600:
3574:
3569:
3565:
3559:
3554:
3550:
3547:
3536:
3535:
3523:
3519:
3516:
3513:
3510:
3507:
3504:
3501:
3498:
3495:
3492:
3489:
3486:
3483:
3480:
3477:
3474:
3471:
3468:
3441:
3425:
3419:
3353:
3339:
3336:
3333:
3330:
3327:
3324:
3321:
3318:
3305:
3300:
3297:
3284:
3264:
3261:
3241:
3238:
3235:
3232:
3229:
3226:
3223:
3220:
3209:
3208:
3195:
3192:
3189:
3186:
3183:
3178:
3175:
3170:
3167:
3163:
3160:
3157:
3153:
3149:
3144:
3140:
3136:
3133:
3130:
3126:
3123:
3117:
3113:
3110:
3105:
3101:
3097:
3094:
3091:
3087:
3084:
3078:
3074:
3071:
3068:
3057:
3044:
3041:
3036:
3033:
3028:
3024:
3021:
3018:
3014:
3009:
3005:
3001:
2998:
2995:
2991:
2988:
2960:
2957:
2952:
2949:
2927:
2924:
2904:
2901:
2898:
2895:
2892:
2867:
2864:
2861:
2857:
2852:
2848:
2844:
2841:
2838:
2834:
2831:
2817:
2816:
2804:
2799:
2796:
2793:
2789:
2784:
2780:
2776:
2773:
2770:
2766:
2763:
2756:
2752:
2749:
2746:
2742:
2739:
2736:
2732:
2729:
2726:
2722:
2717:
2713:
2709:
2706:
2703:
2699:
2696:
2690:
2686:
2683:
2678:
2674:
2670:
2667:
2664:
2660:
2657:
2651:
2647:
2644:
2641:
2626:
2625:
2614:
2611:
2608:
2605:
2602:
2599:
2596:
2593:
2590:
2585:
2581:
2577:
2574:
2571:
2567:
2564:
2534:
2531:
2511:
2507:
2504:
2501:
2497:
2494:
2474:
2471:
2468:
2465:
2462:
2451:
2450:
2439:
2436:
2433:
2430:
2427:
2424:
2421:
2418:
2415:
2412:
2409:
2406:
2403:
2400:
2396:
2393:
2390:
2366:
2363:
2349:
2348:
2337:
2334:
2331:
2326:
2321:
2318:
2313:
2310:
2307:
2304:
2301:
2298:
2288:
2277:
2274:
2271:
2268:
2265:
2262:
2259:
2256:
2229:
2211:
2202:
2111:
2101:
2098:
2081:
2078:
2075:
2069:
2066:
2060:
2040:
2037:
2033:
2017:
2016:
2005:
2002:
1999:
1996:
1993:
1990:
1987:
1984:
1981:
1978:
1975:
1972:
1969:
1966:
1963:
1960:
1957:
1954:
1951:
1948:
1945:
1922:
1919:
1916:
1913:
1910:
1907:
1904:
1901:
1886:
1885:
1874:
1871:
1868:
1865:
1862:
1859:
1856:
1840:. To use the
1829:
1809:
1806:
1803:
1800:
1797:
1786:
1785:
1774:
1771:
1768:
1765:
1762:
1759:
1756:
1753:
1725:
1722:
1695:
1675:
1664:
1663:
1648:
1645:
1617:
1614:
1583:
1563:
1543:
1523:
1503:
1500:
1497:
1486:
1485:
1474:
1471:
1468:
1465:
1462:
1459:
1456:
1453:
1450:
1447:
1444:
1441:
1438:
1435:
1432:
1429:
1426:
1423:
1420:
1417:
1414:
1411:
1384:
1381:
1377:
1372:
1368:
1361:
1358:
1354:
1349:
1345:
1342:
1322:
1300:
1297:
1293:
1272:
1269:
1266:
1263:
1260:
1257:
1254:
1251:
1248:
1228:
1208:
1197:
1196:
1185:
1182:
1179:
1174:
1169:
1164:
1159:
1156:
1153:
1138:
1132:
1130:
1127:
1114:
1090:
1087:
1084:
1081:
1061:
1033:
1030:
1018:
1015:
1014:
1013:
1002:
999:
996:
993:
969:
955:
944:
941:
938:
935:
911:
895:
892:
875:
872:
844:
841:
821:
782:
758:
738:
718:
715:
712:
709:
689:
678:
677:
666:
663:
660:
657:
654:
651:
633:
622:
619:
616:
613:
610:
607:
589:
578:
575:
572:
569:
566:
563:
532:
521:
520:
509:
506:
503:
500:
497:
494:
491:
488:
485:
482:
479:
476:
473:
448:
444:
440:
435:
431:
407:
387:
375:
372:
355:
352:
332:model checking
239:
238:
221:
220:
135:
133:
126:
119:
118:
80:
78:
71:
66:
40:
39:
37:
30:
9:
6:
4:
3:
2:
4229:
4218:
4215:
4213:
4210:
4208:
4205:
4203:
4200:
4198:
4195:
4194:
4192:
4182:
4179:
4178:
4175:Miscellaneous
4174:
4173:
4169:
4165:
4161:
4158:
4157:
4153:
4152:
4148:
4145:
4143:
4139:
4136:
4132:
4128:
4124:
4121:
4115:
4110:
4104:
4101:
4100:
4096:
4095:
4091:
4087:
4083:
4080:
4077:
4073:
4070:
4069:
4065:
4064:
4051:
4045:
4041:
4037:
4033:
4029:
4022:
4013:
4008:
4004:
4000:
3994:
3986:
3985:The MIT Press
3982:
3978:
3972:
3964:
3963:
3958:
3952:
3944:
3938:
3930:
3924:
3920:
3910:
3907:
3905:
3902:
3900:
3897:
3895:
3892:
3890:
3887:
3886:
3880:
3878:
3859:
3856:
3850:
3847:
3844:
3841:
3838:
3835:
3832:
3826:
3820:
3810:
3809:
3808:
3791:
3788:
3782:
3776:
3769:
3768:
3767:
3765:
3749:
3707:
3699:
3678:
3675:
3672:
3646:
3643:
3640:
3637:
3634:
3631:
3628:
3622:
3616:
3610:
3604:
3598:
3591:
3590:
3589:
3567:
3552:
3548:
3545:
3517:
3514:
3505:
3502:
3499:
3496:
3493:
3487:
3484:
3481:
3475:
3472:
3469:
3466:
3459:
3458:
3457:
3455:
3439:
3431:
3424:
3418:
3351:
3337:
3334:
3331:
3328:
3322:
3316:
3304:
3296:
3282:
3262:
3259:
3236:
3233:
3227:
3224:
3221:
3218:
3190:
3187:
3181:
3168:
3151:
3147:
3121:
3115:
3111:
3108:
3082:
3076:
3058:
3042:
3039:
3026:
3012:
2986:
2976:
2975:
2974:
2958:
2955:
2925:
2922:
2902:
2899:
2893:
2890:
2882:
2855:
2829:
2802:
2787:
2761:
2754:
2750:
2747:
2727:
2724:
2720:
2694:
2688:
2684:
2681:
2655:
2649:
2631:
2630:
2629:
2612:
2609:
2600:
2597:
2591:
2588:
2562:
2552:
2551:
2550:
2548:
2532:
2529:
2492:
2469:
2466:
2460:
2437:
2434:
2431:
2428:
2425:
2419:
2416:
2410:
2404:
2401:
2398:
2380:
2379:
2378:
2364:
2361:
2354:
2332:
2329:
2324:
2308:
2302:
2296:
2289:
2275:
2272:
2269:
2266:
2260:
2254:
2247:
2246:
2245:
2243:
2227:
2220:
2217:Consider the
2215:
2210:
2208:
2201:
2199:
2109:
2107:
2097:
2095:
2079:
2076:
2073:
2064:
2058:
2022:
2000:
1997:
1991:
1982:
1976:
1973:
1967:
1958:
1955:
1952:
1946:
1936:
1935:
1934:
1920:
1917:
1914:
1911:
1908:
1902:
1891:
1869:
1866:
1860:
1847:
1846:
1845:
1843:
1807:
1804:
1798:
1772:
1769:
1766:
1763:
1760:
1754:
1743:
1742:
1741:
1739:
1723:
1720:
1711:
1709:
1693:
1662:
1646:
1643:
1635:
1634:
1633:
1631:
1615:
1612:
1603:
1601:
1597:
1581:
1561:
1554:, and string
1541:
1534:, the symbol
1521:
1501:
1498:
1495:
1469:
1466:
1463:
1460:
1457:
1454:
1451:
1448:
1445:
1439:
1430:
1421:
1415:
1409:
1402:
1401:
1400:
1382:
1379:
1370:
1359:
1356:
1347:
1343:
1340:
1298:
1295:
1267:
1264:
1258:
1249:
1183:
1180:
1177:
1154:
1151:
1144:
1143:
1142:
1137:
1126:
1112:
1104:
1088:
1085:
1082:
1079:
1059:
1051:
1047:
1031:
1028:
1000:
997:
994:
991:
983:
967:
959:
956:
942:
939:
936:
933:
925:
909:
901:
898:
897:
891:
889:
873:
870:
862:
858:
842:
839:
819:
811:
807:
802:
800:
796:
780:
772:
756:
736:
713:
707:
687:
661:
655:
652:
649:
641:
637:
634:
617:
611:
608:
605:
597:
593:
590:
576:
573:
567:
561:
553:
549:
546:
545:
544:
530:
504:
498:
495:
489:
483:
477:
474:
471:
464:
463:
462:
446:
442:
433:
429:
421:
405:
398:be a set and
385:
374:Preliminaries
371:
369:
365:
361:
351:
349:
345:
341:
337:
333:
329:
324:
319:
317:
313:
308:
306:
302:
298:
297:specification
293:
291:
287:
284:
280:
277:are known as
276:
272:
268:
265:
260:
258:
254:
250:
246:
235:
232:
217:
214:
206:
203:November 2019
195:
192:
188:
185:
181:
178:
174:
171:
167:
164: –
163:
162:"Coinduction"
159:
158:Find sources:
152:
146:
145:
141:
136:This article
134:
130:
125:
124:
115:
112:
104:
94:
90:
84:
81:This article
79:
70:
69:
64:
62:
55:
54:
49:
48:
43:
38:
29:
28:
23:
19:
4089:
4075:
4031:
4021:
3999:Dexter Kozen
3993:
3984:
3971:
3960:
3951:
3937:
3923:
3899:Bisimulation
3876:
3874:
3806:
3763:
3697:
3664:
3537:
3429:
3427:
3416:
3308:
3302:
3210:
2880:
2818:
2627:
2546:
2452:
2352:
2350:
2216:
2213:
2206:
2195:
2103:
2018:
1890:F-consistent
1889:
1887:
1841:
1787:
1737:
1712:
1707:
1665:
1660:
1629:
1604:
1599:
1595:
1487:
1198:
1140:
1103:F-consistent
1102:
1049:
1045:
1020:
982:F-consistent
981:
957:
923:
899:
888:F-consistent
887:
860:
856:
809:
803:
798:
795:F-consistent
794:
770:
679:
635:
596:F-consistent
595:
591:
551:
547:
522:
377:
367:
363:
359:
357:
336:bisimilarity
320:
309:
294:
278:
264:mathematical
261:
255:interacting
248:
242:
227:
209:
200:
190:
183:
176:
169:
157:
137:
107:
101:October 2011
98:
82:
58:
51:
45:
44:Please help
41:
4147:Coinduction
4123:Bart Jacobs
3904:Anamorphism
3894:Corecursion
3889:F-coalgebra
3879:as stated.
2522:. Because
2219:endofunctor
2209:-coalgebras
1686:. Clearly
640:fixed point
461:, that is:
354:Description
312:corecursive
249:coinduction
4191:Categories
4127:Jan Rutten
4086:Jan Rutten
3915:References
2628:such that
1602:fixpoint.
1044:. By the
1017:Discussion
894:Definition
348:SWI-Prolog
288:, such as
275:data types
253:concurrent
173:newspapers
140:references
47:improve it
4109:CiteSeerX
4066:Textbooks
4007:CiteSeerX
3857:⊆
3848:∈
3827:∪
3807:That is,
3789:⊆
3673:μ
3644:∈
3623:∪
3564:→
3512:⇒
3503:∈
3491:⇒
3485:∈
3476:∧
3470:∈
3335:×
3260:ν
3234:ν
3225:≃
3219:ν
3188:ν
3152:∘
3143:¯
3104:¯
3077:∘
3040:ν
3013:∘
3008:¯
2956:ν
2923:ν
2915:. Since
2900:ν
2897:→
2891:ν
2856:∘
2851:¯
2788:∘
2783:¯
2725:∘
2716:¯
2677:¯
2650:∘
2610:ν
2607:→
2598:ν
2584:¯
2530:ν
2467:ν
2435:ν
2432:×
2417:ν
2408:→
2402:ν
2362:ν
2336:⟩
2312:⟨
2273:×
2068:¯
2039:Σ
2036:→
2021:sequences
2001:⋯
1998:×
1995:⊥
1992:×
1989:⊥
1983:×
1977:⋯
1974:×
1971:⊥
1968:×
1965:⊥
1956:⋯
1953:×
1950:⊥
1947:×
1944:⊥
1918:ν
1915:∈
1912:⋯
1909:×
1906:⊥
1903:×
1900:⊥
1870:⋯
1867:×
1864:⊥
1861:×
1858:⊥
1828:⊥
1808:⋯
1805:×
1802:⊥
1799:×
1796:⊥
1770:ν
1767:∈
1764:⋯
1761:×
1758:⊥
1755:×
1752:⊥
1744:The type
1721:ν
1674:Σ
1644:μ
1613:μ
1542:×
1499:×
1467:∈
1449:×
1440:∪
1434:⊤
1428:⊥
1383:ω
1380:≤
1376:Σ
1367:→
1360:ω
1357:≤
1353:Σ
1321:Σ
1299:ω
1296:≤
1292:Σ
1268:×
1262:⊤
1256:⊥
1247:Σ
1227:⊤
1207:⊥
1181:×
1168:⊤
1158:⊥
1136:datatypes
1105:set that
1086:ν
1083:∈
1029:μ
998:ν
995:⊆
940:⊆
934:μ
871:ν
863:(denoted
840:μ
832:(denoted
609:⊆
574:⊆
496:⊆
481:⇒
475:⊆
439:→
368:induction
53:talk page
4129:(1997).
4105:(1994).
4088:(2011).
4074:(2012).
3883:See also
3764:F-closed
3385:out'
3306:Stream A
2214:Source:
1708:F-closed
1600:greatest
1129:Examples
1050:F-closed
924:F-closed
857:F-closed
771:F-closed
749:. Then
552:F-closed
362:and the
283:infinite
4154:History
3412:astream
3397:astream
3379:astream
3370:astream
3358:astream
2240:in the
2191:astream
2182:astream
2158:astream
1283:. Let
984:, then
926:, then
344:Logtalk
290:streams
257:objects
187:scholar
87:Please
4111:
4046:
4009:
3962:GitHub
2134:Stream
2116:Stream
2106:stream
1661:finite
279:codata
189:
182:
175:
168:
160:
2547:final
2092:(see
1788:Here
1596:least
960:: If
902:: If
638:is a
418:be a
301:proof
194:JSTOR
180:books
4125:and
4084:and
4044:ISBN
3376:tail
3367:head
2351:The
2170:tail
2146:head
2113:data
1659:are
1052:set
804:The
378:Let
267:dual
166:news
4166:",
4162:. "
4036:doi
3762:is
3720:of
3355:out
2545:is
2096:).
1598:or
980:is
922:is
812:of
793:is
769:is
642:if
598:if
594:is
554:if
550:is
269:to
243:In
142:to
91:to
4193::
4042:.
4030:.
4001:,
3983:.
3979:.
3959:.
3588::
2244::
2108::
2059:0.
1399::
350:.
334:,
330:,
292:.
259:.
247:,
153:.
56:.
4133:(
4117:.
4052:.
4038::
4015:.
3987:.
3965:.
3945:.
3931:.
3860:P
3854:}
3851:P
3845:x
3842::
3839:1
3836:+
3833:x
3830:{
3824:}
3821:0
3818:{
3792:P
3786:)
3783:P
3780:(
3777:F
3750:P
3729:N
3708:P
3683:N
3679:=
3676:F
3650:}
3647:X
3641:x
3638::
3635:1
3632:+
3629:x
3626:{
3620:}
3617:0
3614:{
3611:=
3608:)
3605:X
3602:(
3599:F
3573:N
3568:2
3558:N
3553:2
3549::
3546:F
3522:N
3518:=
3515:P
3509:)
3506:P
3500:1
3497:+
3494:n
3488:P
3482:n
3479:(
3473:P
3467:0
3440:P
3409:a
3406:S
3403:=
3400:)
3394:,
3391:a
3388:(
3382:)
3373:,
3364:(
3361:=
3338:x
3332:A
3329:=
3326:)
3323:x
3320:(
3317:F
3283:F
3263:F
3240:)
3237:F
3231:(
3228:F
3222:F
3194:)
3191:F
3185:(
3182:F
3177:d
3174:i
3169:=
3166:)
3162:t
3159:u
3156:o
3148:)
3139:)
3135:t
3132:u
3129:o
3125:(
3122:F
3116:(
3112:F
3109:=
3100:)
3096:t
3093:u
3090:o
3086:(
3083:F
3073:t
3070:u
3067:o
3043:F
3035:d
3032:i
3027:=
3023:t
3020:u
3017:o
3004:)
3000:t
2997:u
2994:o
2990:(
2987:F
2959:F
2951:d
2948:i
2926:F
2903:F
2894:F
2881:F
2866:t
2863:u
2860:o
2847:)
2843:t
2840:u
2837:o
2833:(
2830:F
2803:)
2798:t
2795:u
2792:o
2779:)
2775:t
2772:u
2769:o
2765:(
2762:F
2755:(
2751:F
2748:=
2745:)
2741:t
2738:u
2735:o
2731:(
2728:F
2721:)
2712:)
2708:t
2705:u
2702:o
2698:(
2695:F
2689:(
2685:F
2682:=
2673:)
2669:t
2666:u
2663:o
2659:(
2656:F
2646:t
2643:u
2640:o
2613:F
2604:)
2601:F
2595:(
2592:F
2589::
2580:)
2576:t
2573:u
2570:o
2566:(
2563:F
2533:F
2510:)
2506:t
2503:u
2500:o
2496:(
2493:F
2473:)
2470:F
2464:(
2461:F
2438:F
2429:A
2426:=
2423:)
2420:F
2414:(
2411:F
2405:F
2399::
2395:t
2392:u
2389:o
2365:F
2333:f
2330:,
2325:A
2320:d
2317:i
2309:=
2306:)
2303:f
2300:(
2297:F
2276:x
2270:A
2267:=
2264:)
2261:x
2258:(
2255:F
2228:F
2207:F
2188:=
2185:)
2179:a
2176:S
2173:(
2167:a
2164:=
2161:)
2155:a
2152:S
2149:(
2140:)
2137:a
2131:(
2128:a
2125:S
2122:=
2119:a
2080:0
2077:=
2074:1
2065:0
2032:N
2004:)
1986:(
1980:)
1962:(
1959:=
1921:F
1873:}
1855:{
1773:F
1724:F
1694:F
1647:F
1616:F
1582:F
1562:y
1522:x
1502:y
1496:x
1473:}
1470:X
1464:y
1461:,
1458:x
1455::
1452:y
1446:x
1443:{
1437:}
1431:,
1425:{
1422:=
1419:)
1416:X
1413:(
1410:F
1371:2
1348:2
1344::
1341:F
1271:}
1265:,
1259:,
1253:{
1250:=
1184:T
1178:T
1173:|
1163:|
1155:=
1152:T
1113:x
1089:F
1080:x
1060:X
1032:F
1001:F
992:X
968:X
943:X
937:F
910:X
874:F
843:F
820:F
799:F
781:X
757:X
737:X
717:)
714:X
711:(
708:F
688:X
665:)
662:X
659:(
656:F
653:=
650:X
636:X
621:)
618:X
615:(
612:F
606:X
592:X
577:X
571:)
568:X
565:(
562:F
548:X
531:F
508:)
505:Y
502:(
499:F
493:)
490:X
487:(
484:F
478:Y
472:X
447:U
443:2
434:U
430:2
406:F
386:U
234:)
228:(
216:)
210:(
205:)
201:(
191:·
184:·
177:·
170:·
147:.
114:)
108:(
103:)
99:(
85:.
63:)
59:(
24:.
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
