14328:
13357:
4952:
14323:{\displaystyle {\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {or} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ p\ q)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)=\operatorname {true} \\\operatorname {not} _{1}\ \operatorname {true} &=(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda c.b)\ a=\lambda a.\lambda b.b=\operatorname {false} \\\operatorname {not} _{2}\ \operatorname {true} &=(\lambda p.p\ (\lambda a.\lambda b.b)(\lambda a.\lambda b.a))(\lambda a.\lambda b.a)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=(\lambda b.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a)=\lambda a.\lambda b.b=\operatorname {false} \end{aligned}}}
4282:
4947:{\displaystyle {\begin{array}{r|r|r}{\text{Number}}&{\text{Using init}}&{\text{Using const}}\\\hline 0&\operatorname {init} =\operatorname {value} \ x&\\1&\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f\ x)&\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x\\2&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} )=\operatorname {value} \ (f\ (f\ x))&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} )=\operatorname {value} \ (f\ x)\\3&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} ))=\operatorname {value} \ (f\ (f\ (f\ x)))&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} ))=\operatorname {value} \ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f^{n}\ x)=\operatorname {value} \ (n\ f\ x)&n\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ (f^{n-1}\ x)=\operatorname {value} \ ((n-1)\ f\ x)\\\end{array}}}
7461:
7139:
16653:
7456:{\displaystyle {\begin{aligned}\operatorname {pred} \operatorname {three} =&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} ))))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {one} )))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {one} \ \operatorname {two} ))\\=&\ \operatorname {first} \ (\operatorname {pair} \ \operatorname {two} \ \operatorname {three} )\\=&\ \operatorname {two} \end{aligned}}}
13346:
9643:
16237:
12355:
11926:
905:
7102:
12938:
9014:
19363:
16648:{\displaystyle {\begin{aligned}\operatorname {nil} &\equiv \lambda c.\lambda n.n\\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda h.\lambda t.\operatorname {false} )\ \operatorname {true} \\\operatorname {cons} &\equiv \lambda h.\lambda t.\lambda c.\lambda n.c\ h\ (t\ c\ n)\\\operatorname {head} &\equiv \lambda l.l\ (\lambda h.\lambda t.h)\ \operatorname {false} \\\operatorname {tail} &\equiv \lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda t.\lambda g.g\ h\ (t\ c))\ (\lambda t.n)\ (\lambda h.\lambda t.t)\end{aligned}}}
12048:
11619:
16011:
417:
6855:
13341:{\displaystyle {\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}}
8709:
15361:
9638:{\displaystyle \scriptstyle \operatorname {divide} =\lambda n.((\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x)))\ (\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.(\lambda n.n\ (\lambda x.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a))\ d\ ((\lambda f.\lambda x.x)\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ ((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u))m)\ n\ m)))\ ((\lambda n.\lambda f.\lambda x.f\ (n\ f\ x))\ n)}
12350:{\displaystyle \operatorname {divide} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}
11921:{\displaystyle \operatorname {mult} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}
10047:
15862:
900:{\displaystyle {\begin{array}{r|l|l}{\text{Number}}&{\text{Function definition}}&{\text{Lambda expression}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\\1&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\\2&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\\3&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=f^{n}\ x&n=\lambda f.\lambda x.f^{\circ n}\ x\end{array}}}
7097:{\displaystyle {\begin{aligned}\operatorname {f} =&\ \lambda p.\ \operatorname {pair} \ (\operatorname {second} \ p)\ (\operatorname {succ} \ (\operatorname {second} \ p))\\\operatorname {zero} =&\ (\lambda f.\lambda x.\ x)\\\operatorname {pc0} =&\ \operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} \\\operatorname {pred} =&\ \lambda n.\ \operatorname {first} \ (n\ \operatorname {f} \ \operatorname {pc0} )\\\end{aligned}}}
10262:
5615:
8416:
5858:
14960:
5315:
11217:
10758:
36:
14949:
9849:
16006:{\displaystyle {\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \\\operatorname {head} &\equiv \operatorname {first} \\\operatorname {tail} &\equiv \operatorname {second} \\\operatorname {nil} &\equiv \operatorname {false} \\\operatorname {isnil} &\equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\operatorname {false} )\operatorname {true} \end{aligned}}}
9003:
10058:
8704:{\displaystyle {\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\0&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}}
5372:
5646:
15356:{\displaystyle {\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ ((\lambda x.\lambda y.\lambda z.z\ x\ y)\ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ (\lambda z.z\ a\ b)\\=&(\lambda z.z\ a\ b)\ (\lambda x.\lambda y.x)\\=&(\lambda x.\lambda y.x)\ a\ b=a\end{aligned}}}
5108:
11039:
10580:
8340:
14765:
10042:{\displaystyle \operatorname {OneZero} =\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (\operatorname {OneZero} \ \operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x))))}
7904:
10257:{\displaystyle \operatorname {OneZ} =\lambda c.\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (c\ \operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x))))}
8809:
16214:
12369:
may also be encoded in lambda calculus. Rational numbers may be encoded as a pair of signed numbers. Computable real numbers may be encoded by a limiting process that guarantees that the difference from the real value differs by a number which may be made as small as we need. The references given
17136:
Scott encoding can be done in untyped lambda calculus, whereas its use with types requires a type system with recursion and type polymorphism. A list with element type E in this representation that is used to compute values of type C would have the following recursive type definition, where '=>'
12744:
8801:
5610:{\displaystyle \operatorname {pred} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {const} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ ((n-1)\ f\ x))=\lambda n.\lambda f.\lambda x.(n-1)\ f\ x=\lambda n.(n-1)}
5853:{\displaystyle {\begin{aligned}\operatorname {value} &=\lambda v.(\lambda h.h\ v)\\\operatorname {extract} k&=k\ \lambda u.u\\\operatorname {inc} &=\lambda g.\lambda h.h\ (g\ f)\\\operatorname {init} &=\lambda h.h\ x\\\operatorname {const} &=\lambda u.x\end{aligned}}}
914:
represents the action of applying any given function three times to a value. The supplied function is first applied to a supplied parameter and then successively to its own result. The end result is not the numeral 3 (unless the supplied parameter happens to be 0 and the function is a
5310:{\displaystyle \operatorname {samenum} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {init} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ (n\ f\ x))=\lambda n.\lambda f.\lambda x.n\ f\ x=\lambda n.n}
2085:
11212:{\displaystyle \operatorname {minus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))}
15684:
14735:
10753:{\displaystyle \operatorname {plus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))}
6011:
9834:
12026:
14944:{\displaystyle {\begin{aligned}\operatorname {pair} &\equiv \lambda x.\lambda y.\lambda z.z\ x\ y\\\operatorname {first} &\equiv \lambda p.p\ (\lambda x.\lambda y.x)\\\operatorname {second} &\equiv \lambda p.p\ (\lambda x.\lambda y.y)\end{aligned}}}
8151:
4209:
14565:
15565:
14485:
3703:
7580:
7730:
15819:
15754:
12888:
11608:
8405:
1191:
8998:{\displaystyle {\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}}
6229:
5029:
1591:
8059:
362:
2173:
3492:
16841:
213:
Church encoding is complete but only representationally. Additional functions are needed to translate the representation into common data types, for display to people. It is not possible in general to decide if two functions are
17010:
16022:
6681:
1357:
12658:
8715:
9741:
9655:
divide = (\n.((\f.(\x.x x) (\x.f (x x))) (\c.\n.\m.\f.\x.(\d.(\n.n (\x.(\a.\b.b)) (\a.\b.a)) d ((\f.\x.x) f x) (f (c d m f x))) ((\m.\n.n (\n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)) m) n m))) ((\n.\f.\x. f (n f x)) n))
8112:
11028:
10569:
3564:
3888:
7667:
6753:
5089:
2720:
6397:
3345:
3033:
15601:
1904:
16910:
6460:
2952:
6135:
2633:
1947:
15612:
14639:
10294:
7611:
takes many beta reductions. Unless doing the reduction by hand, this doesn't matter that much, but it is preferable to not have to do this calculation twice. The simplest predicate for testing numbers is
1096:
3264:
1502:
7131:
5873:
3939:
2768:
2368:
9752:
2440:
3099:
6335:
8140:
1848:
14755:(two-tuple) type. The pair is represented as a function that takes a function argument. When given its argument it will apply the argument to the two components of the pair. The definition in
16242:
15867:
14965:
14770:
13362:
12943:
12663:
8814:
8720:
8421:
7144:
6860:
5651:
6835:
6073:
14628:
6606:
11945:
8335:{\displaystyle \operatorname {div} =\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}
3831:
1645:
6559:
1410:
1001:
7942:
4118:
1238:
6794:
6270:
226:. The translation may apply the function in some way to retrieve the value it represents, or look up its value as a literal lambda term. Lambda calculus is usually interpreted as using
4052:
1277:
2874:
3390:
2549:
1939:
14496:
14360:
17292:
Jansen, Jan Martin; Koopman, Pieter W. M.; Plasmeijer, Marinus J. (2006). "Efficient interpretation by transforming data types and patterns to functions". In
Nilsson, Henrik (ed.).
15487:
However this does not give a representation of the empty list, because there is no "null" pointer. To represent null, the pair may be wrapped in another pair, giving three values:
14420:
15526:
14428:
14380:
3571:
7899:{\displaystyle \operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}
2296:
7480:
206:. Nonetheless Church encoding is often used in theoretical arguments, as it is a natural representation for partial evaluation and theorem proving. Operations can be typed using
17263:. 19th International Workshop, IFL 2007, Freiburg, Germany, September 27–29, 2007 Revised Selected Papers. Lecture Notes in Computer Science. Vol. 5083. pp. 228–229.
15768:
4097:
3186:
1785:
1696:
15703:
12759:
12370:
describe software that could, in theory, be translated into lambda calculus. Once real numbers are defined, complex numbers are naturally encoded as a pair of real numbers.
11233:
8351:
6508:
4000:
1734:
16231:. For example, a list of three elements x, y and z can be encoded by a higher-order function that when applied to a combinator c and a value n returns c x (c y (c z n)).
1104:
17257:
Trancón y
Widemann, Baltasar; Parnas, David Lorge (2008). "Tabular Expressions and Total Functional Programming". In Olaf Chitil; Zoltán Horváth; Viktória Zsók (eds.).
9680:
is to use a Church pair, containing Church numerals representing a positive and a negative value. The integer value is the difference between the two Church numerals.
7982:
7696:
6163:
4963:
1510:
8005:
7722:
17131:
17104:
3134:
288:
176:
147:
7609:
3743:
3424:
2802:
2477:
2231:
2119:
3430:
17077:
17057:
17037:
16808:
14400:
272:
196:
16209:{\displaystyle \operatorname {process-list} \equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\operatorname {head-and-tail-clause} )\operatorname {nil-clause} }
4244:
Before implementing the predecessor function, here is a scheme that wraps the value in a container function. We will define new functions to use in place of
57:
16929:
12753:) to directly act as if-clauses. A function returning a Boolean, which is then applied to two parameters, returns either the first or the second parameter:
12739:{\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}
8796:{\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}
6642:
1285:
17742:
198:
is the size of the data structure, making Church encoding impractical. Research has shown that this can be addressed by targeted optimizations, but most
9689:
8082:
18417:
10769:
10310:
3498:
12928:
choose the first or second parameter they may be combined to provide logic operators. Note that there are multiple possible implementations of
3837:
7622:
6687:
5044:
2639:
231:
227:
6346:
18500:
17641:
17499:
Jansen, Jan Martin (2013). "Programming in the λ-Calculus: From Church to Scott and Back". In Achten, Peter; Koopman, Pieter W. M. (eds.).
12373:
The data types and functions described above demonstrate that any data type or calculation may be encoded in lambda calculus. This is the
100:
Terms that are usually considered primitive in other notations (such as integers, Booleans, pairs, lists, and tagged unions) are mapped to
7724:. If this expression is used then the mathematical definition of division given above is translated into function on Church numerals as,
3270:
2958:
2080:{\displaystyle \operatorname {pred} \equiv \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}
15580:
1859:
210:, and primitive recursion is easily accessible. The assumption that functions are the only primitive data types streamlines many proofs.
16868:
15679:{\displaystyle \operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \operatorname {false} \ (\operatorname {pair} h\ t)}
14730:{\displaystyle \operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)}
6403:
2880:
6084:
2555:
4287:
44:
10270:
6006:{\displaystyle \operatorname {pred} =\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}
1006:
422:
9829:{\displaystyle \operatorname {neg} _{s}=\lambda x.\operatorname {pair} \ (\operatorname {second} \ x)\ (\operatorname {first} \ x)}
3192:
1415:
19399:
18814:
7110:
3897:
2726:
2302:
2374:
19586:
18972:
17465:
17436:
17311:
17276:
3039:
234:
with the interpretation of results because of the difference between the intensional and extensional definition of equality.
17760:
17383:
6281:
282:. In simpler terms, the "value" of the numeral is equivalent to the number of times the function encapsulates its argument.
18827:
18150:
8119:
1793:
17594:(PhD). School of Information Technology and Electrical Engineering, The University of Queensland. pp. 14–17, 93–145.
17606:
All about Church and other similar encodings, including how to derive them and operations on them, from first principles
12393:
functions convert between nonnegative integers and their corresponding Church numerals. The functions are given here in
12021:{\displaystyle \operatorname {divZ} =\lambda x.\lambda y.\operatorname {IsZero} \ y\ 0\ (\operatorname {divide} \ x\ y)}
6805:
18832:
18822:
18559:
18412:
17765:
6031:
17756:
14577:
6570:
19602:
18968:
11931:
A similar definition is given here for division, except in this definition, one value in each pair must be zero (see
4204:{\displaystyle \operatorname {pred} (n)={\begin{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}}
3749:
1599:
18310:
6523:
1365:
956:
19065:
18809:
17634:
16681:
In this approach, we use the fact that lists can be observed using pattern matching expression. For example, using
17232:
7912:
1199:
18370:
18063:
17423:
6764:
6240:
17:
17804:
14560:{\displaystyle \operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)}
4019:
1247:
19326:
19028:
18791:
18786:
18611:
18032:
17716:
12394:
2808:
219:
15560:{\displaystyle \operatorname {nil} \equiv \operatorname {pair} \ \operatorname {true} \ \operatorname {true} }
14480:{\displaystyle \operatorname {IsZero} =\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} }
3698:{\displaystyle \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)}
3351:
2483:
1912:
19500:
19485:
19321:
19104:
19021:
18734:
18665:
18542:
17784:
14345:
942:
operations on numbers may be represented by functions on Church numerals. These functions may be defined in
14405:
7575:{\displaystyle n/m=\operatorname {if} \ n\geq m\ \operatorname {then} \ 1+(n-m)/m\ \operatorname {else} \ 0}
19490:
19427:
19246:
19072:
18758:
18392:
17991:
16682:
16228:
15455:
14365:
17609:
17346:
2237:
947:
19392:
19124:
19119:
18729:
18468:
18397:
17726:
17627:
17501:
The Beauty of
Functional Code - Essays Dedicated to Rinus Plasmeijer on the Occasion of His 61st Birthday
17227:
16675:
15814:{\displaystyle \operatorname {tail} \equiv \lambda z.\operatorname {second} \ (\operatorname {second} z)}
12621:
108:
asserts that any computable operator (and its operands) can be represented under Church encoding. In the
15749:{\displaystyle \operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)}
12883:{\displaystyle \operatorname {predicate-} x\ \operatorname {then-clause} \ \operatorname {else-clause} }
19053:
18643:
18037:
18005:
17696:
16227:
As an alternative to the encoding using Church pairs, a list can be encoded by identifying it with its
11603:{\displaystyle x*y=*=(x_{p}-x_{n})*(y_{p}-y_{n})=(x_{p}*y_{p}+x_{n}*y_{n})-(x_{p}*y_{n}+x_{n}*y_{p})=}
8400:{\displaystyle \operatorname {divide} =\lambda n.\operatorname {divide1} \ (\operatorname {succ} \ n)}
4058:
3140:
1739:
1650:
19449:
19444:
19343:
19292:
19189:
18687:
18648:
18125:
17770:
12616:
Some programming languages use these as an implementation model for
Boolean arithmetic; examples are
17799:
17600:
17541:
4145:
19628:
19432:
19184:
19114:
18653:
18505:
18488:
18211:
17691:
17614:
17302:
12374:
6478:
3967:
1701:
1186:{\displaystyle \operatorname {plus} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)}
105:
17362:"Andrej's answer to a question; "Representing negative and complex numbers using lambda calculus""
19016:
18993:
18954:
18840:
18781:
18427:
18347:
18191:
18135:
17748:
17327:
5336:
receives a special container that ignores its argument allowing to skip the first application of
49:
17567:
7107:
This is a simpler definition but leads to a more complex expression for pred. The expansion for
6224:{\displaystyle \operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)}
5024:{\displaystyle \operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)}
2106:, which is initialized in a way that omits the application of the function the first time. See
1586:{\displaystyle \operatorname {mult} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x}
1241:
19495:
19385:
19306:
19033:
19011:
18978:
18871:
18717:
18702:
18675:
18626:
18510:
18445:
18270:
18236:
18231:
18105:
17936:
17913:
17595:
17536:
17297:
8068:
8054:{\displaystyle \operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {succ} \ n)}
7471:
199:
17258:
14490:
The following predicate tests whether the first argument is less-than-or-equal-to the second:
19480:
19236:
19089:
18881:
18599:
18335:
18241:
18100:
18085:
17966:
17941:
7947:
7675:
357:{\displaystyle f^{\circ n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ times}}}.\,}
247:
101:
17453:
7701:
2168:{\displaystyle \operatorname {minus} \equiv \lambda m.\lambda n.(n\operatorname {pred} )\ m}
19581:
19209:
19171:
19048:
18852:
18692:
18616:
18594:
18422:
18380:
18279:
18246:
18110:
17898:
17809:
17109:
17082:
15461:
Represent the list using Scott's encoding that takes cases of match expression as arguments
9665:
Using a lambda calculus calculator, the above expression reduces to 3, using normal order.
3487:{\displaystyle \operatorname {inc} ^{n}\operatorname {con} =\operatorname {val} (f^{n-1}x)}
3112:
928:
279:
93:
are a representation of the natural numbers using lambda notation. The method is named for
19525:
17195:
A list that can be used to compute arbitrary types would have a type that quantifies over
16836:{\displaystyle \operatorname {list} \ \operatorname {nilCode} \ \operatorname {consCode} }
4215:
We need a way of applying the function 1 fewer times to build the predecessor. A numeral
152:
123:
8:
19515:
19470:
19338:
19229:
19214:
19194:
19151:
19038:
18988:
18914:
18859:
18796:
18589:
18584:
18532:
18300:
18289:
17961:
17861:
17789:
17780:
17776:
17711:
17706:
17016:
12401:
corresponds to the λ of Lambda calculus. Implementations in other languages are similar.
12034:
is then used in the following formula, which is the same as for multiplication, but with
7588:
3722:
3403:
2781:
2456:
2210:
223:
203:
19545:
19510:
19367:
19136:
19099:
19084:
19077:
19060:
18864:
18846:
18712:
18638:
18621:
18574:
18387:
18296:
18130:
18115:
18075:
18027:
18012:
18000:
17956:
17931:
17701:
17650:
17554:
17418:
17062:
17042:
17022:
17005:{\displaystyle \operatorname {cons} \ h\ t\ \ \equiv \ \ \lambda n.\lambda c.\ c\ h\ t}
14385:
2203:
916:
257:
207:
181:
18320:
6676:{\displaystyle \operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x}
1352:{\displaystyle \operatorname {succ} \equiv \lambda n.\lambda f.\lambda x.f\ (n\ f\ x)}
120:
A straightforward implementation of Church encoding slows some access operations from
19550:
19362:
19302:
19109:
18919:
18909:
18801:
18682:
18517:
18493:
18274:
18258:
18163:
18140:
18017:
17986:
17951:
17846:
17681:
17588:"§2.4.1 Church Naturals, §2.4.2 Church Booleans, Ch. 5 Derivation techniques for TFP"
17461:
17432:
17307:
17272:
12366:
17558:
17521:
19565:
19540:
19535:
19475:
19316:
19311:
19204:
19161:
18983:
18944:
18939:
18924:
18750:
18707:
18604:
18402:
18352:
17926:
17888:
17546:
17504:
17264:
15376:
15372:
2094:
times. The predecessor function must return a function that applies its parameter
17587:
9736:{\displaystyle \operatorname {convert} _{s}=\lambda x.\operatorname {pair} \ x\ 0}
19520:
19422:
19297:
19287:
19241:
19224:
19141:
19043:
18963:
18770:
18697:
18670:
18658:
18564:
18478:
18452:
18407:
18375:
18176:
17978:
17921:
17871:
17836:
17794:
17578:
17508:
17503:. Lecture Notes in Computer Science. Vol. 8106. Springer. pp. 168–180.
17375:
17268:
17216:
14756:
9839:
The integer value is more naturally represented if one of the pair is zero. The
943:
380:
109:
86:
19560:
19282:
19261:
19219:
19199:
19094:
18949:
18547:
18537:
18527:
18522:
18456:
18330:
18206:
18095:
18090:
18068:
17669:
3105:
2774:
243:
215:
17550:
16802:
as arguments, so that instead of the above pattern match we may simply write:
14342:
is a function that returns a
Boolean value. The most fundamental predicate is
19622:
19408:
19256:
18934:
18441:
18226:
18216:
18186:
18171:
17841:
17328:"Predecessor and lists are not representable in simply typed lambda calculus"
5034:
If there is also a function to retrieve the value from the container (called
367:
All Church numerals are functions that take two parameters. Church numerals
94:
19156:
19003:
18904:
18896:
18776:
18724:
18633:
18569:
18552:
18483:
18342:
18201:
17903:
17686:
16671:
8107:{\displaystyle \operatorname {divide1} \rightarrow \operatorname {div} \ c}
2113:
The subtraction function can be written based on the predecessor function.
17398:
11023:{\displaystyle x-y=-=x_{p}-x_{n}-y_{p}+y_{n}=(x_{p}+y_{n})-(x_{n}+y_{p})=}
10564:{\displaystyle x+y=+=x_{p}-x_{n}+y_{p}-y_{n}=(x_{p}+y_{p})-(x_{n}+y_{n})=}
3559:{\displaystyle \operatorname {if} (n==0)\ 0\ \operatorname {else} \ (n-1)}
19607:
19530:
19505:
19465:
19266:
19146:
18325:
18315:
18262:
17946:
17866:
17851:
17731:
17676:
12750:
3710:
78:
16670:
An alternative representation is Scott encoding, which uses the idea of
12385:
Most real-world languages have support for machine-native integers; the
6025:
The value container applies a function to its value. It is defined by,
5332:
to its container argument, we can arrange that on the first application
3883:{\displaystyle \operatorname {minus} \ m\ n=(n\operatorname {pred} )\ m}
19555:
18196:
18051:
18022:
17828:
15379:
is constructed from list nodes. The basic operations on the list are;
9662:
divide (\f.\x.f (f (f (f (f (f (f (f (f x))))))))) (\f.\x.f (f (f x)))
8071:
may be used to implement the recursion. Create a new function called
7662:{\displaystyle \operatorname {IsZero} \ (\operatorname {minus} \ n\ m)}
6748:{\displaystyle \lambda h.h\ (\operatorname {const} \ f)=\lambda h.h\ x}
5084:{\displaystyle \operatorname {extract} \ (\operatorname {value} \ v)=v}
2715:{\displaystyle \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)}
939:
919:). The function itself, and not its end result, is the Church numeral
202:
languages instead expand their intermediate representations to contain
17592:
Theoretical
Foundations for Practical 'Totally Functional Programming'
17361:
6392:{\displaystyle \operatorname {inc} \ g=\operatorname {value} \ (g\ f)}
19348:
19251:
18304:
18221:
18181:
18145:
18081:
17893:
17883:
17856:
17619:
17428:
12627:
Boolean logic may be considered as a choice. The Church encoding of
12617:
17476:
15510:
Using this idea the basic list operations can be defined like this:
3340:{\displaystyle \lambda m.\lambda n.\lambda f.\lambda x.(n\ m)\ f\ x}
3028:{\displaystyle \lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x}
19333:
19131:
18579:
18284:
17878:
17221:
16659:
15596:{\displaystyle \operatorname {isnil} \equiv \operatorname {first} }
2449:
1899:{\displaystyle \operatorname {exp} \equiv \lambda m.\lambda n.n\ m}
16905:{\displaystyle \operatorname {nil} \equiv \lambda n.\lambda c.\ n}
11939:
function allows us to ignore the value that has a zero component.
6455:{\displaystyle \operatorname {inc} =\lambda g.\lambda h.h\ (g\ f)}
5344:. The right-hand side of the above table shows the expansions of
2947:{\displaystyle \operatorname {multiply} \ m\ n\ f\ x=m\ (n\ f)\ x}
18929:
17721:
9677:
6130:{\displaystyle \operatorname {value} =\lambda v.(\lambda h.h\ v)}
2628:{\displaystyle \operatorname {plus} \ m\ n\ f\ x=m\ f\ (n\ f\ x)}
19377:
946:, or implemented in most functional programming languages (see
35:
17403:
15448:
Build each list node from two pairs (to allow for empty lists).
10289:{\displaystyle \operatorname {OneZero} =Y\operatorname {OneZ} }
27:
Representation of the natural numbers as higher-order functions
6472:
The value may be extracted by applying the identity function,
1091:{\displaystyle f^{\circ (m+n)}(x)=f^{\circ m}(f^{\circ n}(x))}
18473:
17819:
17664:
17106:
arguments, the corresponding parameter of the encoding takes
16794:. We therefore define a list as a function that accepts such
7944:. However the result is that this formula gives the value of
3714:
3259:{\displaystyle \operatorname {exp} \ m\ n\ f\ x=(n\ m)\ f\ x}
1497:{\displaystyle f^{\circ (m*n)}(x)=(f^{\circ n})^{\circ m}(x)}
12749:
This definition allows predicates (i.e. functions returning
16862:. The empty list is the one that returns the nil argument:
16016:
where the last definition is a special case of the general
14752:
14746:
11613:
The last expression is translated into lambda calculus as,
10574:
The last expression is translated into lambda calculus as,
7126:{\displaystyle \operatorname {pred} \operatorname {three} }
4197:
3934:{\displaystyle \lambda m.\lambda n.n\operatorname {pred} m}
2763:{\displaystyle \lambda m.\lambda n.n\operatorname {succ} m}
2363:{\displaystyle \operatorname {succ} \ n\ f\ x=f\ (n\ f\ x)}
16665:
15688:
Create a list node, which is not null, and give it a head
2435:{\displaystyle \lambda n.\lambda f.\lambda x.f\ (n\ f\ x)}
97:, who first encoded data in the lambda calculus this way.
12380:
10052:
The recursion may be implemented using the Y combinator,
4112:
The predecessor function used in the Church encoding is,
17256:
3954:
2178:
2098:
times. This is achieved by building a container around
17291:
15444:
We give four different representations of lists below:
3396:
3094:{\displaystyle \lambda m.\lambda n.\lambda f.m\ (n\ f)}
2107:
17260:
17235:— another way to encode natural numbers: as sets
16219:
9018:
6330:{\displaystyle g\ f=\operatorname {value} \ v\ f=f\ v}
4188:
4154:
17112:
17085:
17065:
17045:
17025:
16932:
16871:
16811:
16240:
16025:
15865:
15771:
15706:
15615:
15583:
15529:
15470:
A nonempty list can be implemented by a Church pair;
14963:
14768:
14642:
14580:
14499:
14431:
14408:
14388:
14368:
14348:
13360:
12941:
12762:
12661:
12051:
11948:
11622:
11236:
11042:
10772:
10583:
10313:
10273:
10061:
9852:
9755:
9692:
9683:
A natural number is converted to a signed number by,
9676:
One simple approach for extending Church
Numerals to
9017:
8812:
8718:
8419:
8354:
8154:
8135:{\displaystyle \operatorname {divide1} \rightarrow c}
8122:
8085:
8008:
7950:
7915:
7733:
7704:
7678:
7625:
7591:
7483:
7142:
7113:
6858:
6808:
6767:
6690:
6645:
6573:
6526:
6481:
6406:
6349:
6284:
6243:
6166:
6087:
6034:
5876:
5649:
5375:
5111:
5047:
4966:
4285:
4121:
4107:
4061:
4022:
3970:
3900:
3840:
3752:
3725:
3574:
3501:
3433:
3406:
3354:
3273:
3195:
3143:
3115:
3042:
2961:
2883:
2811:
2784:
2729:
2642:
2558:
2486:
2459:
2377:
2305:
2240:
2213:
2122:
1950:
1915:
1862:
1843:{\displaystyle \operatorname {exp} \ m\ n=m^{n}=n\ m}
1796:
1742:
1704:
1653:
1602:
1513:
1418:
1368:
1288:
1250:
1202:
1107:
1009:
959:
420:
291:
260:
184:
155:
126:
85:
is a means of representing data and operators in the
10304:Addition is defined mathematically on the pair by,
4264:. The left-hand side of the table shows a numeral
3960:This formula is the definition of a Church numeral
934:
927:means simply to do anything three times. It is an
17458:Randomness And Complexity, From Leibniz To Chaitin
17454:"14. Binary Lambda Calculus and Combinatory Logic"
17125:
17098:
17071:
17051:
17031:
17004:
16904:
16835:
16647:
16208:
16005:
15813:
15748:
15678:
15595:
15559:
15418:Prepend a given value to a (possibly empty) list.
15355:
14943:
14729:
14622:
14559:
14479:
14414:
14394:
14374:
14354:
14322:
13340:
12882:
12738:
12652:The two definitions are known as Church Booleans:
12349:
12020:
11920:
11602:
11211:
11022:
10752:
10563:
10288:
10256:
10041:
9828:
9735:
9637:
8997:
8795:
8703:
8399:
8334:
8134:
8106:
8053:
7976:
7936:
7898:
7716:
7690:
7661:
7603:
7574:
7455:
7125:
7096:
6830:{\displaystyle \operatorname {const} =\lambda u.x}
6829:
6788:
6747:
6675:
6600:
6553:
6502:
6454:
6391:
6329:
6264:
6223:
6129:
6067:
6005:
5852:
5609:
5324:function is not intrinsically useful. However, as
5309:
5083:
5023:
4946:
4203:
4091:
4046:
3994:
3933:
3882:
3825:
3737:
3697:
3558:
3486:
3418:
3384:
3339:
3258:
3180:
3128:
3093:
3027:
2946:
2868:
2796:
2762:
2714:
2627:
2543:
2471:
2434:
2362:
2290:
2225:
2167:
2079:
1933:
1898:
1842:
1779:
1728:
1690:
1639:
1585:
1496:
1404:
1351:
1271:
1232:
1185:
1090:
995:
899:
356:
266:
190:
170:
141:
7909:As desired, this definition has a single call to
6068:{\displaystyle \operatorname {value} \ v\ h=h\ v}
4230:. The predecessor function must use the numeral
931:demonstration of what is meant by "three times".
19620:
14623:{\displaystyle x=y\equiv (x\leq y\land y\leq x)}
6601:{\displaystyle \operatorname {extract} \ k=k\ I}
6844:
3826:{\displaystyle f^{m-n}\ x=(f^{-1})^{n}(f^{m}x)}
1647:is given by the definition of Church numerals,
1640:{\displaystyle \operatorname {exp} (m,n)=m^{n}}
17615:Lambda Calculus Live Tutorial: Boolean Algebra
17477:"Binary Lambda Calculus and Combinatory Logic"
16658:This list representation can be given type in
12608:are the Church encoding of the Boolean values
9746:Negation is performed by swapping the values.
6554:{\displaystyle \operatorname {value} \ v\ I=v}
1405:{\displaystyle \operatorname {mult} (m,n)=m*n}
996:{\displaystyle \operatorname {plus} (m,n)=m+n}
393:not applying the function at all, proceed with
112:the only primitive data type is the function.
19393:
17635:
15605:Retrieve the null (or empty list) indicator.
14633:The test for equality may be implemented as,
14422:if its argument is any other Church numeral:
7987:This problem may be corrected by adding 1 to
17610:Some interactive examples of Church numerals
14751:Church pairs are the Church encoding of the
12360:
7937:{\displaystyle \operatorname {minus} \ n\ m}
1233:{\displaystyle \operatorname {succ} (n)=n+1}
15465:
6789:{\displaystyle \operatorname {const} \ f=x}
6265:{\displaystyle g=\operatorname {value} \ v}
242:Church numerals are the representations of
19400:
19386:
17827:
17642:
17628:
17294:Trends in functional programming. Volume 7
17252:
17250:
17248:
15851:
7474:of natural numbers may be implemented by,
5366:function we get the predecessor function,
4047:{\displaystyle \operatorname {pred} (0)=0}
1941:function is more difficult to understand.
1272:{\displaystyle (\operatorname {plus} \ 1)}
948:converting lambda expressions to functions
17599:
17540:
17301:
2869:{\displaystyle f^{m*n}\ x=(f^{m})^{n}\ x}
353:
17568:"Church numerals and booleans explained"
16674:and can lead to simpler code. (see also
6149:function should take a value containing
3385:{\displaystyle \lambda m.\lambda n.n\ m}
2544:{\displaystyle f^{m+n}\ x=f^{m}(f^{n}x)}
1934:{\displaystyle \operatorname {pred} (n)}
60:of all important aspects of the article.
17245:
17224:for Church numerals in a typed calculus
16666:Represent the list using Scott encoding
14355:{\displaystyle \operatorname {IsZero} }
409:applying the function three times, etc.
14:
19621:
17649:
17565:
17522:"Directly reflective meta-programming"
17498:
17460:. World Scientific. pp. 237–262.
17417:
17332:Lambda Calculus and Lambda Calculators
17296:. Bristol: Intellect. pp. 73–90.
14415:{\displaystyle \operatorname {false} }
14382:if its argument is the Church numeral
12381:Translation with other representations
11222:
6849:Pred may also be defined using pairs:
5863:Which gives the lambda expression for
56:Please consider expanding the lead to
19587:University of California, Los Angeles
19381:
17623:
17519:
17474:
17451:
17396:
17039:alternatives becomes a function with
14375:{\displaystyle \operatorname {true} }
2179:Table of functions on Church numerals
379:, ..., are defined as follows in the
254:is a function that maps any function
17585:
17399:"Real number computational software"
16701:we can inspect the list and compute
15848:are only applied to nonempty lists.
7672:But this condition is equivalent to
6153:, and return a new value containing
4260:. The container function is called
4010:
4008:
2291:{\displaystyle f^{n+1}\ x=f(f^{n}x)}
2090:A Church numeral applies a function
29:
17397:Bauer, Andrej (26 September 2022).
17344:
15451:Build each list node from one pair.
15428:Get the first element of the list.
9659:For example, 9/3 is represented by
5340:. Call this new initial container
1853:which gives the lambda expression,
24:
17233:Von Neumann definition of ordinals
16202:
16199:
16196:
16193:
16190:
16187:
16181:
16178:
16175:
16167:
16164:
16161:
16158:
16155:
16152:
16146:
16143:
16140:
16137:
16131:
16128:
16125:
16119:
16116:
16113:
16110:
16060:
16057:
16054:
16051:
16045:
16042:
16039:
16036:
16033:
16030:
16027:
12876:
12873:
12870:
12867:
12864:
12861:
12855:
12852:
12849:
12846:
12835:
12832:
12829:
12826:
12823:
12820:
12814:
12811:
12808:
12805:
12788:
12785:
12782:
12779:
12776:
12773:
12770:
12767:
12764:
12600:
11227:Multiplication may be defined by,
10763:Similarly subtraction is defined,
9843:function achieves this condition,
7347:
7281:
7269:
7200:
7188:
7176:
7075:
6863:
6234:Letting g be the value container,
6020:
4108:Derivation of predecessor function
237:
25:
19640:
19603:Alonzo Church (college president)
19407:
17359:
15840:is never accessed, provided that
15569:The first element of the pair is
15366:
12635:are functions of two parameters:
10299:
9671:
5620:As explained below the functions
4005:
2110:for a more detailed explanation.
19361:
17386:from the original on 2015-03-26.
15494:- the null pointer (empty list).
8067:is a recursive definition. The
4957:The general recurrence rule is,
4092:{\displaystyle m\leq n\to m-n=0}
3181:{\displaystyle n\ m\ f=m^{n}\ f}
1780:{\displaystyle n\ m\ f=m^{n}\ f}
1698:. In the definition substitute
1691:{\displaystyle n\ h\ x=h^{n}\ x}
935:Calculation with Church numerals
34:
17492:
17456:. In Calude, Cristian S (ed.).
17445:
17424:Types and Programming Languages
17411:
16920:
16916:
16859:
16858:the parameter corresponding to
16855:
16851:
16850:the parameter corresponding to
16847:
16799:
16795:
16791:
16787:
16783:
16706:
14740:
250:that represents natural number
48:may be too short to adequately
17390:
17368:
17353:
17338:
17320:
17285:
16705:in case the list is empty and
16638:
16614:
16608:
16593:
16587:
16584:
16572:
16530:
16474:
16450:
16418:
16400:
16329:
16305:
16171:
16079:
15993:
15960:
15808:
15796:
15743:
15731:
15673:
15655:
15328:
15304:
15290:
15266:
15260:
15233:
15219:
15192:
15186:
15183:
15159:
15141:
15127:
15112:
15067:
15064:
15058:
15055:
15031:
15013:
14999:
14978:
14934:
14910:
14878:
14854:
14724:
14703:
14697:
14676:
14617:
14593:
14554:
14533:
14468:
14453:
14283:
14259:
14253:
14250:
14226:
14214:
14208:
14184:
14181:
14157:
14154:
14130:
14124:
14100:
14097:
14094:
14070:
14067:
14043:
14025:
13956:
13941:
13905:
13881:
13857:
13833:
13830:
13785:
13746:
13722:
13716:
13692:
13686:
13662:
13656:
13632:
13626:
13602:
13596:
13572:
13566:
13530:
13486:
13462:
13423:
13387:
13269:
13254:
13189:
13165:
13159:
13135:
12344:
12341:
12338:
12323:
12317:
12302:
12290:
12284:
12281:
12266:
12260:
12245:
12233:
12221:
12215:
12212:
12209:
12194:
12188:
12173:
12161:
12155:
12152:
12137:
12131:
12116:
12104:
12092:
12015:
11994:
11915:
11912:
11909:
11894:
11888:
11873:
11861:
11855:
11852:
11837:
11831:
11816:
11804:
11792:
11786:
11783:
11780:
11765:
11759:
11744:
11732:
11726:
11723:
11708:
11702:
11687:
11675:
11663:
11597:
11493:
11487:
11435:
11429:
11377:
11371:
11345:
11339:
11313:
11307:
11281:
11275:
11249:
11206:
11203:
11200:
11185:
11179:
11164:
11152:
11146:
11143:
11128:
11122:
11107:
11095:
11083:
11017:
10965:
10959:
10933:
10927:
10901:
10843:
10817:
10811:
10785:
10747:
10744:
10741:
10726:
10720:
10705:
10693:
10687:
10684:
10669:
10663:
10648:
10636:
10624:
10558:
10506:
10500:
10474:
10468:
10442:
10384:
10358:
10352:
10326:
10251:
10248:
10245:
10242:
10227:
10215:
10209:
10206:
10191:
10179:
10161:
10149:
10134:
10122:
10110:
10095:
10036:
10033:
10030:
10027:
10012:
10000:
9994:
9991:
9976:
9964:
9943:
9931:
9916:
9904:
9892:
9877:
9823:
9808:
9802:
9787:
9631:
9622:
9619:
9601:
9565:
9562:
9556:
9553:
9550:
9535:
9529:
9526:
9511:
9505:
9490:
9484:
9481:
9469:
9442:
9406:
9382:
9379:
9373:
9370:
9367:
9337:
9328:
9322:
9307:
9283:
9280:
9268:
9265:
9241:
9235:
9232:
9208:
9196:
9178:
9166:
9118:
9112:
9109:
9106:
9094:
9076:
9070:
9049:
9037:
9034:
8988:
8973:
8967:
8952:
8946:
8943:
8931:
8904:
8688:
8673:
8606:
8603:
8591:
8573:
8567:
8564:
8552:
8534:
8508:
8490:
8394:
8379:
8329:
8308:
8302:
8299:
8296:
8266:
8257:
8251:
8233:
8206:
8126:
8089:
8048:
8033:
7963:
7951:
7893:
7872:
7866:
7863:
7860:
7827:
7818:
7812:
7794:
7767:
7656:
7635:
7546:
7534:
7431:
7407:
7383:
7380:
7356:
7344:
7320:
7317:
7314:
7290:
7278:
7266:
7242:
7239:
7236:
7233:
7209:
7197:
7185:
7173:
7087:
7066:
6991:
6964:
6946:
6943:
6928:
6916:
6910:
6895:
6721:
6706:
6624:function is replaced with the
6449:
6437:
6386:
6374:
6218:
6206:
6191:
6176:
6124:
6103:
6000:
5985:
5979:
5964:
5958:
5955:
5943:
5916:
5785:
5773:
5694:
5673:
5604:
5592:
5565:
5553:
5520:
5517:
5502:
5490:
5487:
5475:
5433:
5418:
5244:
5241:
5223:
5211:
5169:
5154:
5072:
5057:
5018:
5006:
4991:
4976:
4937:
4922:
4910:
4907:
4892:
4867:
4835:
4817:
4802:
4783:
4727:
4724:
4712:
4703:
4688:
4685:
4670:
4658:
4644:
4641:
4638:
4626:
4617:
4608:
4593:
4590:
4575:
4563:
4542:
4530:
4515:
4500:
4486:
4483:
4471:
4462:
4447:
4432:
4382:
4370:
4134:
4128:
4071:
4035:
4029:
3986:
3974:
3871:
3862:
3820:
3804:
3795:
3778:
3692:
3677:
3671:
3656:
3650:
3647:
3635:
3608:
3553:
3541:
3520:
3508:
3481:
3459:
3322:
3310:
3241:
3229:
3088:
3076:
3016:
3004:
2935:
2923:
2851:
2837:
2709:
2691:
2622:
2604:
2538:
2522:
2429:
2411:
2357:
2339:
2285:
2269:
2156:
2147:
2074:
2059:
2053:
2038:
2032:
2029:
2017:
1990:
1928:
1922:
1720:
1708:
1621:
1609:
1574:
1562:
1491:
1485:
1473:
1456:
1450:
1444:
1439:
1427:
1387:
1375:
1346:
1328:
1266:
1251:
1215:
1209:
1180:
1162:
1085:
1082:
1076:
1060:
1041:
1035:
1030:
1018:
978:
966:
785:
782:
770:
761:
726:
723:
711:
702:
666:
654:
619:
607:
165:
159:
136:
130:
58:provide an accessible overview
13:
1:
19322:History of mathematical logic
17239:
17190:// result of pattern matching
16915:The non-empty list with head
16786:is given by how it acts upon
15454:Represent the list using the
14333:
12648:chooses the second parameter.
6503:{\displaystyle I=\lambda u.u}
3995:{\displaystyle f\to m,x\to f}
1729:{\displaystyle h\to m,x\to f}
404:applying the function twice,
220:undecidability of equivalence
19428:Simply typed lambda calculus
19247:Primitive recursive function
17509:10.1007/978-3-642-40355-2_12
17269:10.1007/978-3-540-85373-2_13
16709:when the list is not empty:
12642:chooses the first parameter.
6845:Another way of defining pred
1596:The exponentiation function
1362:The multiplication function
399:applying the function once,
246:under Church encoding. The
104:under Church encoding. The
7:
17475:Tromp, John (14 May 2014).
17210:
7616:so consider the condition.
7466:
6799:Or as a lambda expression,
10:
19645:
18311:Schröder–Bernstein theorem
18038:Monadic predicate calculus
17697:Foundations of mathematics
17347:"Lambda Calculus Integers"
15573:meaning the list is null.
15438:Get the rest of the list.
14744:
6467:
5362:in the expression for the
5098:may be used to define the
19595:
19574:
19458:
19415:
19357:
19344:Philosophy of mathematics
19293:Automated theorem proving
19275:
19170:
19002:
18895:
18747:
18464:
18440:
18418:Von Neumann–Bernays–Gödel
18363:
18257:
18161:
18059:
18050:
17977:
17912:
17818:
17740:
17657:
17551:10.1007/s10990-007-9022-0
16220:Represent the list using
15398:Construct an empty list.
14571:Because of the identity,
12361:Rational and real numbers
6465:
6018:
3567:
2197:
17139:
16711:
16689:denotes a value of type
15466:Two pairs as a list node
12403:
9648:Or as text, using \ for
6611:
4014:In the Church encoding,
18994:Self-verifying theories
18815:Tarski's axiomatization
17766:Tarski's undefinability
17761:incompleteness theorems
17376:"Exact real arithmetic"
17228:Mogensen–Scott encoding
17137:denotes function type:
16676:Mogensen–Scott encoding
15852:One pair as a list node
15408:Test if list is empty.
12367:computable real numbers
8116:In the right hand side
7977:{\displaystyle (n-1)/m}
7691:{\displaystyle n\leq m}
6758:Which is satisfied if,
1196:The successor function
110:untyped lambda calculus
19368:Mathematics portal
18979:Proof of impossibility
18627:propositional variable
17937:Propositional calculus
17529:High-Order Symb Comput
17207:as the type argument.
17127:
17100:
17073:
17053:
17033:
17006:
16906:
16837:
16649:
16210:
16007:
15856:Alternatively, define
15815:
15750:
15680:
15597:
15561:
15357:
14945:
14731:
14624:
14561:
14481:
14416:
14396:
14376:
14356:
14324:
13342:
12884:
12740:
12351:
12022:
11922:
11604:
11213:
11024:
10754:
10565:
10290:
10258:
10043:
9830:
9737:
9639:
8999:
8797:
8705:
8401:
8336:
8136:
8108:
8079:In the left hand side
8055:
7978:
7938:
7900:
7718:
7717:{\displaystyle n<m}
7692:
7663:
7605:
7576:
7457:
7127:
7098:
6831:
6790:
6749:
6677:
6602:
6555:
6504:
6456:
6393:
6331:
6266:
6225:
6140:
6131:
6069:
6007:
5854:
5611:
5311:
5085:
5025:
4948:
4234:to apply the function
4205:
4093:
4048:
3996:
3935:
3884:
3827:
3739:
3699:
3560:
3488:
3420:
3386:
3341:
3260:
3182:
3130:
3095:
3029:
2948:
2870:
2798:
2764:
2716:
2629:
2545:
2473:
2436:
2364:
2292:
2227:
2169:
2081:
1935:
1900:
1844:
1781:
1730:
1692:
1641:
1587:
1498:
1406:
1353:
1273:
1234:
1187:
1092:
997:
953:The addition function
923:. The Church numeral
901:
358:
268:
200:functional programming
192:
172:
143:
115:
102:higher-order functions
19481:George Alfred Barnard
19450:Church–Rosser theorem
19445:Frege–Church ontology
19237:Kolmogorov complexity
19190:Computably enumerable
19090:Model complete theory
18882:Principia Mathematica
17942:Propositional formula
17771:Banach–Tarski paradox
17199:. A list generic in
17128:
17126:{\displaystyle n_{i}}
17101:
17099:{\displaystyle n_{i}}
17074:
17059:parameters. When the
17054:
17034:
17007:
16907:
16838:
16650:
16211:
16008:
15816:
15751:
15681:
15598:
15562:
15358:
14946:
14732:
14625:
14562:
14482:
14417:
14397:
14377:
14357:
14325:
13343:
12885:
12741:
12352:
12023:
11923:
11605:
11214:
11025:
10755:
10566:
10291:
10259:
10044:
9831:
9738:
9640:
9000:
8798:
8706:
8402:
8337:
8137:
8109:
8056:
7979:
7939:
7901:
7719:
7693:
7664:
7606:
7577:
7458:
7128:
7099:
6832:
6791:
6750:
6678:
6603:
6556:
6505:
6457:
6394:
6332:
6267:
6226:
6132:
6070:
6008:
5855:
5612:
5354:. Then by replacing
5328:delegates calling of
5312:
5086:
5026:
4949:
4219:applies the function
4206:
4094:
4049:
3997:
3936:
3885:
3828:
3740:
3700:
3561:
3489:
3421:
3387:
3342:
3261:
3183:
3131:
3129:{\displaystyle m^{n}}
3096:
3030:
2949:
2871:
2799:
2765:
2717:
2630:
2546:
2474:
2437:
2365:
2293:
2228:
2170:
2082:
1936:
1901:
1845:
1782:
1731:
1693:
1642:
1588:
1499:
1407:
1354:
1274:
1235:
1188:
1093:
998:
902:
359:
269:
248:higher-order function
193:
173:
144:
19582:Princeton University
19433:Church–Turing thesis
19185:Church–Turing thesis
19172:Computability theory
18381:continuum hypothesis
17899:Square of opposition
17757:Gödel's completeness
17586:Kemp, Colin (2007).
17566:Cartwright, Robert.
17452:Tromp, John (2007).
17110:
17083:
17063:
17043:
17023:
16930:
16869:
16809:
16238:
16023:
15863:
15769:
15704:
15613:
15581:
15527:
14961:
14766:
14640:
14578:
14497:
14429:
14406:
14386:
14366:
14346:
13358:
12939:
12760:
12659:
12375:Church–Turing thesis
12049:
11946:
11620:
11234:
11223:Multiply and divide
11040:
10770:
10581:
10311:
10271:
10059:
9850:
9753:
9690:
9668:\f.\x.f (f (f (x)))
9015:
8810:
8716:
8417:
8352:
8152:
8120:
8083:
8006:
7995:. The definition of
7948:
7913:
7731:
7702:
7676:
7623:
7589:
7481:
7140:
7111:
6856:
6806:
6765:
6688:
6643:
6628:that does not apply
6571:
6524:
6479:
6404:
6347:
6282:
6241:
6164:
6085:
6032:
5874:
5647:
5373:
5109:
5045:
4964:
4283:
4119:
4059:
4020:
3968:
3898:
3838:
3750:
3723:
3572:
3499:
3431:
3404:
3352:
3271:
3193:
3141:
3113:
3040:
2959:
2881:
2809:
2782:
2727:
2640:
2556:
2484:
2457:
2375:
2303:
2238:
2211:
2195:Function definition
2120:
1948:
1913:
1860:
1794:
1740:
1702:
1651:
1600:
1511:
1416:
1366:
1286:
1248:
1200:
1105:
1007:
957:
418:
289:
258:
228:intensional equality
204:algebraic data types
182:
171:{\displaystyle O(n)}
153:
142:{\displaystyle O(1)}
124:
106:Church–Turing thesis
19516:Stephen Cole Kleene
19471:C. Anthony Anderson
19339:Mathematical object
19230:P versus NP problem
19195:Computable function
18989:Reverse mathematics
18915:Logical consequence
18792:primitive recursive
18787:elementary function
18560:Free/bound variable
18413:Tarski–Grothendieck
17932:Logical connectives
17862:Logical equivalence
17712:Logical consequence
17575:Comp 311 — Review 2
17419:Pierce, Benjamin C.
17133:arguments as well.
17079:th constructor has
17017:algebraic data type
17015:More generally, an
16229:right fold function
15456:right fold function
7604:{\displaystyle n-m}
5640:may be defined as,
3738:{\displaystyle m-n}
3419:{\displaystyle n-1}
2797:{\displaystyle m*n}
2472:{\displaystyle m+n}
2226:{\displaystyle n+1}
2198:Lambda expressions
910:The Church numeral
434:Function definition
208:higher-ranked types
19546:Hartley Rogers, Jr
19511:John George Kemeny
19137:Transfer principle
19100:Semantics of logic
19085:Categorical theory
19061:Non-standard model
18575:Logical connective
17702:Information theory
17651:Mathematical logic
17520:Stump, A. (2009).
17123:
17096:
17069:
17049:
17029:
17002:
16902:
16833:
16645:
16643:
16206:
16003:
16001:
15811:
15746:
15676:
15593:
15557:
15506:contains the tail.
15500:contains the head.
15483:contains the tail.
15477:contains the head.
15353:
15351:
14941:
14939:
14727:
14620:
14557:
14477:
14412:
14392:
14372:
14352:
14320:
14318:
13338:
13336:
12880:
12736:
12734:
12347:
12018:
11918:
11600:
11209:
11020:
10750:
10561:
10286:
10254:
10039:
9826:
9733:
9635:
9634:
8995:
8993:
8793:
8791:
8701:
8699:
8397:
8332:
8132:
8104:
8051:
7974:
7934:
7896:
7714:
7688:
7659:
7601:
7572:
7453:
7451:
7123:
7094:
7092:
6827:
6786:
6745:
6673:
6598:
6551:
6500:
6452:
6389:
6327:
6262:
6221:
6127:
6065:
6003:
5850:
5848:
5607:
5307:
5081:
5021:
4944:
4942:
4201:
4196:
4192:
4158:
4089:
4044:
3992:
3931:
3880:
3823:
3735:
3695:
3556:
3484:
3416:
3382:
3337:
3256:
3178:
3126:
3091:
3025:
2944:
2866:
2794:
2760:
2712:
2625:
2541:
2469:
2432:
2360:
2288:
2223:
2165:
2077:
1931:
1896:
1840:
1777:
1726:
1688:
1637:
1583:
1494:
1412:uses the identity
1402:
1349:
1269:
1230:
1183:
1088:
1003:uses the identity
993:
917:successor function
897:
895:
354:
349:
337:
264:
232:potential problems
188:
168:
139:
19616:
19615:
19551:J. Barkley Rosser
19375:
19374:
19307:Abstract category
19110:Theories of truth
18920:Rule of inference
18910:Natural deduction
18891:
18890:
18436:
18435:
18141:Cartesian product
18046:
18045:
17952:Many-valued logic
17927:Boolean functions
17810:Russell's paradox
17785:diagonal argument
17682:First-order logic
17467:978-981-4474-39-9
17438:978-0-262-16209-8
17313:978-1-84150-188-8
17278:978-3-540-85372-5
17072:{\displaystyle i}
17052:{\displaystyle m}
17032:{\displaystyle m}
16998:
16992:
16986:
16965:
16962:
16956:
16953:
16947:
16941:
16898:
16846:Let us denote by
16829:
16820:
16613:
16592:
16580:
16571:
16565:
16529:
16479:
16449:
16414:
16408:
16399:
16393:
16334:
16304:
16186:
16151:
16136:
16124:
16050:
15830:
15829:
15795:
15730:
15669:
15654:
15553:
15544:
15442:
15441:
15339:
15333:
15265:
15256:
15250:
15215:
15209:
15191:
15158:
15123:
15117:
15108:
15102:
15063:
15030:
14995:
14989:
14977:
14909:
14853:
14821:
14815:
14720:
14714:
14702:
14693:
14687:
14675:
14550:
14544:
14532:
14473:
14452:
14395:{\displaystyle 0}
14258:
14042:
14014:
13961:
13916:
13910:
13826:
13820:
13774:
13691:
13661:
13601:
13571:
13562:
13556:
13437:
13428:
13419:
13413:
13330:
13324:
13274:
13265:
13253:
13164:
13134:
13095:
13089:
13032:
13026:
12985:
12979:
12860:
12844:
12819:
12803:
12793:
12334:
12322:
12313:
12301:
12289:
12277:
12265:
12256:
12244:
12232:
12220:
12205:
12193:
12184:
12172:
12160:
12148:
12136:
12127:
12115:
12103:
12091:
12011:
12005:
11993:
11987:
11981:
11905:
11893:
11884:
11872:
11860:
11848:
11836:
11827:
11815:
11803:
11791:
11776:
11764:
11755:
11743:
11731:
11719:
11707:
11698:
11686:
11674:
11662:
11196:
11184:
11175:
11163:
11151:
11139:
11127:
11118:
11106:
11094:
11082:
10737:
10725:
10716:
10704:
10692:
10680:
10668:
10659:
10647:
10635:
10623:
10238:
10226:
10214:
10202:
10190:
10178:
10169:
10160:
10154:
10145:
10133:
10121:
10115:
10106:
10094:
10023:
10011:
9999:
9987:
9975:
9963:
9954:
9942:
9936:
9927:
9915:
9903:
9897:
9888:
9876:
9819:
9807:
9798:
9786:
9729:
9723:
9627:
9615:
9609:
9600:
9561:
9546:
9540:
9510:
9489:
9477:
9468:
9441:
9378:
9363:
9357:
9351:
9345:
9336:
9327:
9318:
9312:
9279:
9273:
9240:
9195:
9117:
9102:
9093:
9075:
9066:
8972:
8951:
8939:
8930:
8903:
8693:
8672:
8599:
8590:
8572:
8560:
8551:
8504:
8498:
8489:
8439:
8390:
8378:
8325:
8319:
8307:
8292:
8286:
8280:
8274:
8265:
8256:
8247:
8241:
8232:
8226:
8100:
8044:
8032:
8017:
7930:
7924:
7889:
7883:
7871:
7856:
7850:
7844:
7838:
7826:
7817:
7808:
7802:
7793:
7787:
7760:
7754:
7748:
7742:
7652:
7646:
7634:
7568:
7559:
7527:
7518:
7506:
7445:
7427:
7418:
7406:
7397:
7376:
7367:
7355:
7343:
7334:
7310:
7301:
7289:
7277:
7265:
7256:
7229:
7220:
7208:
7196:
7184:
7172:
7163:
7083:
7074:
7065:
7056:
7044:
7026:
7017:
7008:
6987:
6963:
6939:
6927:
6915:
6906:
6894:
6885:
6873:
6842:
6841:
6776:
6741:
6717:
6705:
6669:
6654:
6594:
6582:
6541:
6535:
6445:
6436:
6382:
6373:
6358:
6323:
6311:
6305:
6290:
6258:
6214:
6205:
6187:
6175:
6120:
6061:
6049:
6043:
5984:
5963:
5951:
5942:
5915:
5816:
5781:
5772:
5722:
5690:
5576:
5570:
5513:
5507:
5486:
5474:
5417:
5288:
5282:
5237:
5231:
5222:
5210:
5153:
5068:
5056:
5014:
5005:
4987:
4975:
4933:
4927:
4906:
4888:
4866:
4851:
4831:
4825:
4816:
4798:
4782:
4767:
4720:
4711:
4702:
4681:
4669:
4657:
4634:
4625:
4616:
4607:
4586:
4574:
4562:
4538:
4529:
4511:
4499:
4479:
4470:
4461:
4443:
4431:
4410:
4395:
4378:
4369:
4354:
4332:
4307:
4300:
4293:
4191:
4157:
3944:
3943:
3876:
3855:
3849:
3771:
3676:
3655:
3643:
3634:
3607:
3540:
3531:
3525:
3378:
3333:
3327:
3318:
3252:
3246:
3237:
3222:
3216:
3210:
3204:
3174:
3155:
3149:
3084:
3075:
3021:
3012:
3003:
2940:
2931:
2922:
2910:
2904:
2898:
2892:
2862:
2830:
2705:
2699:
2690:
2684:
2618:
2612:
2603:
2597:
2585:
2579:
2573:
2567:
2505:
2425:
2419:
2410:
2353:
2347:
2338:
2326:
2320:
2314:
2259:
2161:
2058:
2037:
2025:
2016:
1989:
1892:
1836:
1811:
1805:
1773:
1754:
1748:
1684:
1665:
1659:
1579:
1570:
1561:
1342:
1336:
1327:
1262:
1176:
1170:
1161:
1155:
889:
844:
825:
819:
778:
769:
760:
719:
710:
701:
689:
683:
662:
653:
615:
606:
594:
588:
570:
535:
523:
517:
464:
458:
442:
441:Lambda expression
435:
428:
346:
310:
308:
267:{\displaystyle f}
218:equal due to the
191:{\displaystyle n}
75:
74:
16:(Redirected from
19636:
19566:Raymond Smullyan
19541:Nicholas Rescher
19536:Michael O. Rabin
19402:
19395:
19388:
19379:
19378:
19366:
19365:
19317:History of logic
19312:Category of sets
19205:Decision problem
18984:Ordinal analysis
18925:Sequent calculus
18823:Boolean algebras
18763:
18762:
18737:
18708:logical/constant
18462:
18461:
18448:
18371:Zermelo–Fraenkel
18122:Set operations:
18057:
18056:
17994:
17825:
17824:
17805:Löwenheim–Skolem
17692:Formal semantics
17644:
17637:
17630:
17621:
17620:
17605:
17603:
17582:
17572:
17562:
17544:
17526:
17513:
17512:
17496:
17490:
17489:
17487:
17486:
17481:
17471:
17449:
17443:
17442:
17415:
17409:
17408:
17394:
17388:
17387:
17372:
17366:
17365:
17357:
17351:
17350:
17345:Allison, Lloyd.
17342:
17336:
17335:
17324:
17318:
17317:
17305:
17289:
17283:
17282:
17254:
17206:
17203:would also take
17202:
17198:
17191:
17188:
17185:
17184:// cons argument
17182:
17179:
17176:
17173:
17170:
17167:
17164:
17161:
17158:
17155:
17152:
17149:
17146:
17143:
17132:
17130:
17129:
17124:
17122:
17121:
17105:
17103:
17102:
17097:
17095:
17094:
17078:
17076:
17075:
17070:
17058:
17056:
17055:
17050:
17038:
17036:
17035:
17030:
17011:
17009:
17008:
17003:
16996:
16990:
16984:
16963:
16960:
16954:
16951:
16945:
16939:
16922:
16918:
16911:
16909:
16908:
16903:
16896:
16861:
16857:
16853:
16849:
16842:
16840:
16839:
16834:
16827:
16818:
16801:
16797:
16793:
16789:
16785:
16778:
16775:
16772:
16769:
16766:
16763:
16760:
16757:
16754:
16751:
16748:
16745:
16742:
16739:
16736:
16733:
16730:
16727:
16724:
16721:
16718:
16715:
16708:
16704:
16700:
16697:and constructor
16696:
16693:with empty list
16692:
16688:
16654:
16652:
16651:
16646:
16644:
16611:
16590:
16578:
16569:
16563:
16527:
16477:
16447:
16412:
16406:
16397:
16391:
16332:
16302:
16215:
16213:
16212:
16207:
16205:
16184:
16170:
16149:
16134:
16122:
16063:
16048:
16012:
16010:
16009:
16004:
16002:
15820:
15818:
15817:
15812:
15793:
15755:
15753:
15752:
15747:
15728:
15685:
15683:
15682:
15677:
15667:
15652:
15602:
15600:
15599:
15594:
15566:
15564:
15563:
15558:
15551:
15542:
15513:
15512:
15382:
15381:
15362:
15360:
15359:
15354:
15352:
15337:
15331:
15263:
15254:
15248:
15213:
15207:
15189:
15156:
15121:
15115:
15106:
15100:
15061:
15028:
14993:
14987:
14975:
14967:
14950:
14948:
14947:
14942:
14940:
14907:
14851:
14819:
14813:
14736:
14734:
14733:
14728:
14718:
14712:
14700:
14691:
14685:
14673:
14629:
14627:
14626:
14621:
14566:
14564:
14563:
14558:
14548:
14542:
14530:
14486:
14484:
14483:
14478:
14471:
14450:
14421:
14419:
14418:
14413:
14401:
14399:
14398:
14393:
14381:
14379:
14378:
14373:
14362:, which returns
14361:
14359:
14358:
14353:
14329:
14327:
14326:
14321:
14319:
14256:
14040:
14012:
14008:
14007:
13959:
13914:
13908:
13824:
13818:
13772:
13768:
13767:
13689:
13659:
13599:
13569:
13560:
13554:
13435:
13426:
13417:
13411:
13347:
13345:
13344:
13339:
13337:
13328:
13322:
13272:
13263:
13251:
13162:
13132:
13112:
13111:
13093:
13087:
13049:
13048:
13030:
13024:
12983:
12977:
12889:
12887:
12886:
12881:
12879:
12858:
12842:
12838:
12817:
12801:
12794:
12791:
12745:
12743:
12742:
12737:
12735:
12596:
12593:
12590:
12587:
12584:
12581:
12578:
12575:
12572:
12569:
12566:
12563:
12560:
12557:
12554:
12551:
12548:
12545:
12542:
12539:
12536:
12533:
12530:
12527:
12524:
12521:
12518:
12515:
12512:
12509:
12506:
12503:
12500:
12497:
12494:
12491:
12488:
12485:
12482:
12479:
12476:
12473:
12470:
12467:
12464:
12461:
12458:
12455:
12452:
12449:
12446:
12443:
12440:
12437:
12434:
12431:
12428:
12425:
12422:
12419:
12416:
12413:
12410:
12407:
12400:
12356:
12354:
12353:
12348:
12332:
12320:
12311:
12299:
12287:
12275:
12263:
12254:
12242:
12230:
12218:
12203:
12191:
12182:
12170:
12158:
12146:
12134:
12125:
12113:
12101:
12089:
12061:
12060:
12027:
12025:
12024:
12019:
12009:
12003:
11991:
11985:
11979:
11927:
11925:
11924:
11919:
11903:
11891:
11882:
11870:
11858:
11846:
11834:
11825:
11813:
11801:
11789:
11774:
11762:
11753:
11741:
11729:
11717:
11705:
11696:
11684:
11672:
11660:
11632:
11631:
11609:
11607:
11606:
11601:
11596:
11595:
11583:
11582:
11570:
11569:
11557:
11556:
11544:
11543:
11531:
11530:
11518:
11517:
11505:
11504:
11486:
11485:
11473:
11472:
11460:
11459:
11447:
11446:
11428:
11427:
11415:
11414:
11402:
11401:
11389:
11388:
11370:
11369:
11357:
11356:
11338:
11337:
11325:
11324:
11306:
11305:
11293:
11292:
11274:
11273:
11261:
11260:
11218:
11216:
11215:
11210:
11194:
11182:
11173:
11161:
11149:
11137:
11125:
11116:
11104:
11092:
11080:
11052:
11051:
11029:
11027:
11026:
11021:
11016:
11015:
11003:
11002:
10990:
10989:
10977:
10976:
10958:
10957:
10945:
10944:
10926:
10925:
10913:
10912:
10897:
10896:
10884:
10883:
10871:
10870:
10858:
10857:
10842:
10841:
10829:
10828:
10810:
10809:
10797:
10796:
10759:
10757:
10756:
10751:
10735:
10723:
10714:
10702:
10690:
10678:
10666:
10657:
10645:
10633:
10621:
10593:
10592:
10570:
10568:
10567:
10562:
10557:
10556:
10544:
10543:
10531:
10530:
10518:
10517:
10499:
10498:
10486:
10485:
10467:
10466:
10454:
10453:
10438:
10437:
10425:
10424:
10412:
10411:
10399:
10398:
10383:
10382:
10370:
10369:
10351:
10350:
10338:
10337:
10295:
10293:
10292:
10287:
10263:
10261:
10260:
10255:
10236:
10224:
10212:
10200:
10188:
10176:
10167:
10158:
10152:
10143:
10131:
10119:
10113:
10104:
10092:
10048:
10046:
10045:
10040:
10021:
10009:
9997:
9985:
9973:
9961:
9952:
9940:
9934:
9925:
9913:
9901:
9895:
9886:
9874:
9835:
9833:
9832:
9827:
9817:
9805:
9796:
9784:
9765:
9764:
9742:
9740:
9739:
9734:
9727:
9721:
9702:
9701:
9651:
9644:
9642:
9641:
9636:
9625:
9613:
9607:
9598:
9559:
9544:
9538:
9508:
9487:
9475:
9466:
9439:
9376:
9361:
9355:
9349:
9343:
9334:
9325:
9316:
9310:
9277:
9271:
9238:
9193:
9115:
9100:
9091:
9073:
9064:
9004:
9002:
9001:
8996:
8994:
8970:
8949:
8937:
8928:
8901:
8802:
8800:
8799:
8794:
8792:
8710:
8708:
8707:
8702:
8700:
8691:
8670:
8597:
8588:
8570:
8558:
8549:
8502:
8496:
8487:
8437:
8406:
8404:
8403:
8398:
8388:
8376:
8341:
8339:
8338:
8333:
8323:
8317:
8305:
8290:
8284:
8278:
8272:
8263:
8254:
8245:
8239:
8230:
8224:
8141:
8139:
8138:
8133:
8113:
8111:
8110:
8105:
8098:
8060:
8058:
8057:
8052:
8042:
8030:
8015:
7983:
7981:
7980:
7975:
7970:
7943:
7941:
7940:
7935:
7928:
7922:
7905:
7903:
7902:
7897:
7887:
7881:
7869:
7854:
7848:
7842:
7836:
7824:
7815:
7806:
7800:
7791:
7785:
7758:
7752:
7746:
7740:
7723:
7721:
7720:
7715:
7697:
7695:
7694:
7689:
7668:
7666:
7665:
7660:
7650:
7644:
7632:
7610:
7608:
7607:
7602:
7581:
7579:
7578:
7573:
7566:
7557:
7553:
7525:
7516:
7504:
7491:
7462:
7460:
7459:
7454:
7452:
7443:
7425:
7416:
7404:
7395:
7374:
7365:
7353:
7341:
7332:
7308:
7299:
7287:
7275:
7263:
7254:
7227:
7218:
7206:
7194:
7182:
7170:
7161:
7132:
7130:
7129:
7124:
7103:
7101:
7100:
7095:
7093:
7081:
7072:
7063:
7054:
7042:
7024:
7015:
7006:
6985:
6961:
6937:
6925:
6913:
6904:
6892:
6883:
6871:
6836:
6834:
6833:
6828:
6795:
6793:
6792:
6787:
6774:
6754:
6752:
6751:
6746:
6739:
6715:
6703:
6682:
6680:
6679:
6674:
6667:
6652:
6635:
6631:
6627:
6623:
6619:
6607:
6605:
6604:
6599:
6592:
6580:
6560:
6558:
6557:
6552:
6539:
6533:
6516:
6509:
6507:
6506:
6501:
6461:
6459:
6458:
6453:
6443:
6434:
6398:
6396:
6395:
6390:
6380:
6371:
6356:
6336:
6334:
6333:
6328:
6321:
6309:
6303:
6288:
6271:
6269:
6268:
6263:
6256:
6230:
6228:
6227:
6222:
6212:
6203:
6185:
6173:
6156:
6152:
6148:
6136:
6134:
6133:
6128:
6118:
6074:
6072:
6071:
6066:
6059:
6047:
6041:
6016:
6015:
6012:
6010:
6009:
6004:
5982:
5961:
5949:
5940:
5913:
5866:
5859:
5857:
5856:
5851:
5849:
5814:
5779:
5770:
5720:
5688:
5639:
5635:
5631:
5627:
5623:
5616:
5614:
5613:
5608:
5574:
5568:
5511:
5505:
5484:
5472:
5415:
5365:
5361:
5357:
5353:
5350:
5347:
5343:
5339:
5335:
5331:
5327:
5323:
5316:
5314:
5313:
5308:
5286:
5280:
5235:
5229:
5220:
5208:
5151:
5101:
5097:
5090:
5088:
5087:
5082:
5066:
5054:
5037:
5030:
5028:
5027:
5022:
5012:
5003:
4985:
4973:
4953:
4951:
4950:
4945:
4943:
4931:
4925:
4904:
4886:
4885:
4884:
4864:
4849:
4829:
4823:
4814:
4796:
4795:
4794:
4780:
4765:
4718:
4709:
4700:
4679:
4667:
4655:
4632:
4623:
4614:
4605:
4584:
4572:
4560:
4536:
4527:
4509:
4497:
4477:
4468:
4459:
4441:
4429:
4408:
4393:
4376:
4367:
4352:
4337:
4330:
4308:
4305:
4301:
4298:
4294:
4291:
4275:
4271:
4267:
4263:
4259:
4255:
4251:
4247:
4240:
4233:
4229:
4225:
4222:
4218:
4210:
4208:
4207:
4202:
4200:
4199:
4193:
4189:
4159:
4155:
4101:
4098:
4096:
4095:
4090:
4053:
4051:
4050:
4045:
4012:
4003:
4001:
3999:
3998:
3993:
3963:
3958:
3940:
3938:
3937:
3932:
3889:
3887:
3886:
3881:
3874:
3853:
3847:
3832:
3830:
3829:
3824:
3816:
3815:
3803:
3802:
3793:
3792:
3769:
3768:
3767:
3744:
3742:
3741:
3736:
3704:
3702:
3701:
3696:
3674:
3653:
3641:
3632:
3605:
3565:
3563:
3562:
3557:
3538:
3529:
3523:
3493:
3491:
3490:
3485:
3477:
3476:
3443:
3442:
3425:
3423:
3422:
3417:
3391:
3389:
3388:
3383:
3376:
3346:
3344:
3343:
3338:
3331:
3325:
3316:
3265:
3263:
3262:
3257:
3250:
3244:
3235:
3220:
3214:
3208:
3202:
3187:
3185:
3184:
3179:
3172:
3171:
3170:
3153:
3147:
3135:
3133:
3132:
3127:
3125:
3124:
3100:
3098:
3097:
3092:
3082:
3073:
3034:
3032:
3031:
3026:
3019:
3010:
3001:
2953:
2951:
2950:
2945:
2938:
2929:
2920:
2908:
2902:
2896:
2890:
2875:
2873:
2872:
2867:
2860:
2859:
2858:
2849:
2848:
2828:
2827:
2826:
2803:
2801:
2800:
2795:
2769:
2767:
2766:
2761:
2721:
2719:
2718:
2713:
2703:
2697:
2688:
2682:
2634:
2632:
2631:
2626:
2616:
2610:
2601:
2595:
2583:
2577:
2571:
2565:
2550:
2548:
2547:
2542:
2534:
2533:
2521:
2520:
2503:
2502:
2501:
2478:
2476:
2475:
2470:
2441:
2439:
2438:
2433:
2423:
2417:
2408:
2369:
2367:
2366:
2361:
2351:
2345:
2336:
2324:
2318:
2312:
2297:
2295:
2294:
2289:
2281:
2280:
2257:
2256:
2255:
2232:
2230:
2229:
2224:
2183:
2182:
2174:
2172:
2171:
2166:
2159:
2086:
2084:
2083:
2078:
2056:
2035:
2023:
2014:
1987:
1940:
1938:
1937:
1932:
1905:
1903:
1902:
1897:
1890:
1849:
1847:
1846:
1841:
1834:
1827:
1826:
1809:
1803:
1786:
1784:
1783:
1778:
1771:
1770:
1769:
1752:
1746:
1735:
1733:
1732:
1727:
1697:
1695:
1694:
1689:
1682:
1681:
1680:
1663:
1657:
1646:
1644:
1643:
1638:
1636:
1635:
1592:
1590:
1589:
1584:
1577:
1568:
1559:
1503:
1501:
1500:
1495:
1484:
1483:
1471:
1470:
1443:
1442:
1411:
1409:
1408:
1403:
1358:
1356:
1355:
1350:
1340:
1334:
1325:
1278:
1276:
1275:
1270:
1260:
1239:
1237:
1236:
1231:
1192:
1190:
1189:
1184:
1174:
1168:
1159:
1153:
1097:
1095:
1094:
1089:
1075:
1074:
1059:
1058:
1034:
1033:
1002:
1000:
999:
994:
906:
904:
903:
898:
896:
887:
886:
885:
842:
841:
840:
823:
817:
776:
767:
758:
717:
708:
699:
687:
681:
660:
651:
613:
604:
592:
586:
568:
533:
521:
515:
462:
456:
443:
440:
436:
433:
429:
426:
363:
361:
360:
355:
348:
347:
344:
338:
333:
304:
303:
273:
271:
270:
265:
224:Church's theorem
197:
195:
194:
189:
177:
175:
174:
169:
148:
146:
145:
140:
70:
67:
61:
38:
30:
21:
19644:
19643:
19639:
19638:
19637:
19635:
19634:
19633:
19629:Lambda calculus
19619:
19618:
19617:
19612:
19591:
19570:
19521:Simon B. Kochen
19454:
19438:Church encoding
19423:Lambda calculus
19411:
19406:
19376:
19371:
19360:
19353:
19298:Category theory
19288:Algebraic logic
19271:
19242:Lambda calculus
19180:Church encoding
19166:
19142:Truth predicate
18998:
18964:Complete theory
18887:
18756:
18752:
18748:
18743:
18735:
18455: and
18451:
18446:
18432:
18408:New Foundations
18376:axiom of choice
18359:
18321:Gödel numbering
18261: and
18253:
18157:
18042:
17992:
17973:
17922:Boolean algebra
17908:
17872:Equiconsistency
17837:Classical logic
17814:
17795:Halting problem
17783: and
17759: and
17747: and
17746:
17741:Theorems (
17736:
17653:
17648:
17601:10.1.1.149.3505
17579:Rice University
17570:
17542:10.1.1.489.5018
17524:
17516:
17497:
17493:
17484:
17482:
17479:
17472:
17468:
17450:
17446:
17439:
17431:. p. 500.
17416:
17412:
17395:
17391:
17374:
17373:
17369:
17360:Bauer, Andrej.
17358:
17354:
17343:
17339:
17326:
17325:
17321:
17314:
17290:
17286:
17279:
17255:
17246:
17242:
17217:Lambda calculus
17213:
17204:
17200:
17196:
17193:
17192:
17189:
17186:
17183:
17180:
17177:
17174:
17171:
17168:
17165:
17162:
17159:
17157:// nil argument
17156:
17153:
17150:
17147:
17144:
17141:
17117:
17113:
17111:
17108:
17107:
17090:
17086:
17084:
17081:
17080:
17064:
17061:
17060:
17044:
17041:
17040:
17024:
17021:
17020:
16931:
16928:
16927:
16870:
16867:
16866:
16810:
16807:
16806:
16780:
16779:
16776:
16773:
16770:
16767:
16764:
16761:
16758:
16755:
16752:
16749:
16746:
16743:
16740:
16737:
16734:
16731:
16728:
16725:
16722:
16719:
16716:
16713:
16702:
16698:
16694:
16690:
16686:
16668:
16642:
16641:
16490:
16484:
16483:
16428:
16422:
16421:
16345:
16339:
16338:
16283:
16277:
16276:
16248:
16241:
16239:
16236:
16235:
16225:
16174:
16109:
16026:
16024:
16021:
16020:
16000:
15999:
15941:
15935:
15934:
15924:
15918:
15917:
15907:
15901:
15900:
15890:
15884:
15883:
15873:
15866:
15864:
15861:
15860:
15854:
15770:
15767:
15766:
15705:
15702:
15701:
15614:
15611:
15610:
15582:
15579:
15578:
15528:
15525:
15524:
15468:
15369:
15350:
15349:
15300:
15294:
15293:
15229:
15223:
15222:
15137:
15131:
15130:
15009:
15003:
15002:
14964:
14962:
14959:
14958:
14938:
14937:
14888:
14882:
14881:
14832:
14826:
14825:
14776:
14769:
14767:
14764:
14763:
14757:lambda calculus
14749:
14743:
14641:
14638:
14637:
14579:
14576:
14575:
14498:
14495:
14494:
14430:
14427:
14426:
14407:
14404:
14403:
14387:
14384:
14383:
14367:
14364:
14363:
14347:
14344:
14343:
14336:
14317:
14316:
14018:
14003:
13999:
13996:
13995:
13778:
13763:
13759:
13756:
13755:
13523:
13505:
13504:
13380:
13361:
13359:
13356:
13355:
13351:Some examples:
13335:
13334:
13285:
13279:
13278:
13223:
13217:
13216:
13113:
13107:
13103:
13100:
13099:
13050:
13044:
13040:
13037:
13036:
12996:
12990:
12989:
12949:
12942:
12940:
12937:
12936:
12845:
12804:
12763:
12761:
12758:
12757:
12733:
12732:
12704:
12698:
12697:
12669:
12662:
12660:
12657:
12656:
12606:Church Booleans
12603:
12601:Church Booleans
12598:
12597:
12594:
12591:
12588:
12585:
12582:
12579:
12576:
12573:
12570:
12567:
12564:
12561:
12558:
12555:
12552:
12549:
12546:
12543:
12540:
12537:
12534:
12531:
12528:
12525:
12522:
12519:
12516:
12513:
12510:
12507:
12504:
12501:
12498:
12495:
12492:
12489:
12486:
12483:
12480:
12477:
12474:
12471:
12468:
12465:
12462:
12459:
12456:
12453:
12450:
12447:
12444:
12441:
12438:
12435:
12432:
12429:
12426:
12423:
12420:
12417:
12414:
12411:
12408:
12405:
12398:
12383:
12363:
12056:
12052:
12050:
12047:
12046:
11947:
11944:
11943:
11627:
11623:
11621:
11618:
11617:
11591:
11587:
11578:
11574:
11565:
11561:
11552:
11548:
11539:
11535:
11526:
11522:
11513:
11509:
11500:
11496:
11481:
11477:
11468:
11464:
11455:
11451:
11442:
11438:
11423:
11419:
11410:
11406:
11397:
11393:
11384:
11380:
11365:
11361:
11352:
11348:
11333:
11329:
11320:
11316:
11301:
11297:
11288:
11284:
11269:
11265:
11256:
11252:
11235:
11232:
11231:
11225:
11047:
11043:
11041:
11038:
11037:
11011:
11007:
10998:
10994:
10985:
10981:
10972:
10968:
10953:
10949:
10940:
10936:
10921:
10917:
10908:
10904:
10892:
10888:
10879:
10875:
10866:
10862:
10853:
10849:
10837:
10833:
10824:
10820:
10805:
10801:
10792:
10788:
10771:
10768:
10767:
10588:
10584:
10582:
10579:
10578:
10552:
10548:
10539:
10535:
10526:
10522:
10513:
10509:
10494:
10490:
10481:
10477:
10462:
10458:
10449:
10445:
10433:
10429:
10420:
10416:
10407:
10403:
10394:
10390:
10378:
10374:
10365:
10361:
10346:
10342:
10333:
10329:
10312:
10309:
10308:
10302:
10272:
10269:
10268:
10060:
10057:
10056:
9851:
9848:
9847:
9760:
9756:
9754:
9751:
9750:
9697:
9693:
9691:
9688:
9687:
9674:
9669:
9663:
9657:
9649:
9016:
9013:
9012:
8992:
8991:
8864:
8858:
8857:
8820:
8813:
8811:
8808:
8807:
8790:
8789:
8761:
8755:
8754:
8726:
8719:
8717:
8714:
8713:
8698:
8697:
8651:
8645:
8644:
8616:
8610:
8609:
8518:
8512:
8511:
8450:
8444:
8443:
8427:
8420:
8418:
8415:
8414:
8353:
8350:
8349:
8153:
8150:
8149:
8121:
8118:
8117:
8084:
8081:
8080:
8007:
8004:
8003:
7991:before calling
7966:
7949:
7946:
7945:
7914:
7911:
7910:
7732:
7729:
7728:
7703:
7700:
7699:
7677:
7674:
7673:
7624:
7621:
7620:
7590:
7587:
7586:
7549:
7487:
7482:
7479:
7478:
7469:
7450:
7449:
7441:
7435:
7434:
7393:
7387:
7386:
7330:
7324:
7323:
7252:
7246:
7245:
7159:
7143:
7141:
7138:
7137:
7112:
7109:
7108:
7091:
7090:
7040:
7031:
7030:
7004:
6995:
6994:
6959:
6950:
6949:
6869:
6859:
6857:
6854:
6853:
6847:
6807:
6804:
6803:
6766:
6763:
6762:
6689:
6686:
6685:
6644:
6641:
6640:
6633:
6629:
6625:
6621:
6617:
6614:
6572:
6569:
6568:
6525:
6522:
6521:
6514:
6480:
6477:
6476:
6470:
6405:
6402:
6401:
6348:
6345:
6344:
6283:
6280:
6279:
6242:
6239:
6238:
6165:
6162:
6161:
6154:
6150:
6146:
6143:
6086:
6083:
6082:
6033:
6030:
6029:
6023:
6021:Value container
5875:
5872:
5871:
5864:
5847:
5846:
5827:
5821:
5820:
5795:
5789:
5788:
5742:
5736:
5735:
5710:
5698:
5697:
5657:
5650:
5648:
5645:
5644:
5637:
5633:
5629:
5625:
5621:
5374:
5371:
5370:
5363:
5359:
5355:
5351:
5348:
5345:
5341:
5337:
5333:
5329:
5325:
5321:
5110:
5107:
5106:
5099:
5095:
5046:
5043:
5042:
5035:
4965:
4962:
4961:
4941:
4940:
4874:
4870:
4838:
4790:
4786:
4754:
4748:
4747:
4742:
4737:
4731:
4730:
4647:
4552:
4546:
4545:
4489:
4421:
4415:
4414:
4385:
4344:
4338:
4336:
4316:
4310:
4309:
4304:
4302:
4297:
4295:
4290:
4286:
4284:
4281:
4280:
4273:
4269:
4265:
4261:
4257:
4253:
4249:
4245:
4235:
4231:
4227:
4223:
4220:
4216:
4195:
4194:
4187:
4185:
4173:
4172:
4153:
4151:
4141:
4140:
4120:
4117:
4116:
4110:
4105:
4104:
4060:
4057:
4056:
4021:
4018:
4017:
4013:
4006:
3969:
3966:
3965:
3961:
3959:
3955:
3899:
3896:
3895:
3839:
3836:
3835:
3811:
3807:
3798:
3794:
3785:
3781:
3757:
3753:
3751:
3748:
3747:
3724:
3721:
3720:
3573:
3570:
3569:
3500:
3497:
3496:
3466:
3462:
3438:
3434:
3432:
3429:
3428:
3405:
3402:
3401:
3353:
3350:
3349:
3272:
3269:
3268:
3194:
3191:
3190:
3166:
3162:
3142:
3139:
3138:
3120:
3116:
3114:
3111:
3110:
3041:
3038:
3037:
2960:
2957:
2956:
2882:
2879:
2878:
2854:
2850:
2844:
2840:
2816:
2812:
2810:
2807:
2806:
2783:
2780:
2779:
2728:
2725:
2724:
2641:
2638:
2637:
2557:
2554:
2553:
2529:
2525:
2516:
2512:
2491:
2487:
2485:
2482:
2481:
2458:
2455:
2454:
2376:
2373:
2372:
2304:
2301:
2300:
2276:
2272:
2245:
2241:
2239:
2236:
2235:
2212:
2209:
2208:
2181:
2121:
2118:
2117:
1949:
1946:
1945:
1914:
1911:
1910:
1861:
1858:
1857:
1822:
1818:
1795:
1792:
1791:
1765:
1761:
1741:
1738:
1737:
1703:
1700:
1699:
1676:
1672:
1652:
1649:
1648:
1631:
1627:
1601:
1598:
1597:
1512:
1509:
1508:
1476:
1472:
1463:
1459:
1423:
1419:
1417:
1414:
1413:
1367:
1364:
1363:
1287:
1284:
1283:
1249:
1246:
1245:
1201:
1198:
1197:
1106:
1103:
1102:
1067:
1063:
1051:
1047:
1014:
1010:
1008:
1005:
1004:
958:
955:
954:
944:lambda calculus
937:
894:
893:
878:
874:
848:
836:
832:
812:
806:
805:
800:
795:
789:
788:
729:
676:
670:
669:
622:
581:
575:
574:
539:
510:
504:
503:
474:
451:
445:
444:
439:
437:
432:
430:
425:
421:
419:
416:
415:
381:lambda calculus
343:
339:
311:
309:
296:
292:
290:
287:
286:
259:
256:
255:
244:natural numbers
240:
238:Church numerals
183:
180:
179:
154:
151:
150:
125:
122:
121:
118:
91:Church numerals
87:lambda calculus
83:Church encoding
71:
65:
62:
55:
43:This article's
39:
28:
23:
22:
18:Church numerals
15:
12:
11:
5:
19642:
19632:
19631:
19614:
19613:
19611:
19610:
19605:
19599:
19597:
19593:
19592:
19590:
19589:
19584:
19578:
19576:
19572:
19571:
19569:
19568:
19563:
19561:Norman Shapiro
19558:
19553:
19548:
19543:
19538:
19533:
19528:
19526:Maurice L'Abbé
19523:
19518:
19513:
19508:
19503:
19498:
19496:William Easton
19493:
19488:
19483:
19478:
19473:
19468:
19462:
19460:
19456:
19455:
19453:
19452:
19447:
19442:
19441:
19440:
19435:
19430:
19419:
19417:
19413:
19412:
19405:
19404:
19397:
19390:
19382:
19373:
19372:
19358:
19355:
19354:
19352:
19351:
19346:
19341:
19336:
19331:
19330:
19329:
19319:
19314:
19309:
19300:
19295:
19290:
19285:
19283:Abstract logic
19279:
19277:
19273:
19272:
19270:
19269:
19264:
19262:Turing machine
19259:
19254:
19249:
19244:
19239:
19234:
19233:
19232:
19227:
19222:
19217:
19212:
19202:
19200:Computable set
19197:
19192:
19187:
19182:
19176:
19174:
19168:
19167:
19165:
19164:
19159:
19154:
19149:
19144:
19139:
19134:
19129:
19128:
19127:
19122:
19117:
19107:
19102:
19097:
19095:Satisfiability
19092:
19087:
19082:
19081:
19080:
19070:
19069:
19068:
19058:
19057:
19056:
19051:
19046:
19041:
19036:
19026:
19025:
19024:
19019:
19012:Interpretation
19008:
19006:
19000:
18999:
18997:
18996:
18991:
18986:
18981:
18976:
18966:
18961:
18960:
18959:
18958:
18957:
18947:
18942:
18932:
18927:
18922:
18917:
18912:
18907:
18901:
18899:
18893:
18892:
18889:
18888:
18886:
18885:
18877:
18876:
18875:
18874:
18869:
18868:
18867:
18862:
18857:
18837:
18836:
18835:
18833:minimal axioms
18830:
18819:
18818:
18817:
18806:
18805:
18804:
18799:
18794:
18789:
18784:
18779:
18766:
18764:
18745:
18744:
18742:
18741:
18740:
18739:
18727:
18722:
18721:
18720:
18715:
18710:
18705:
18695:
18690:
18685:
18680:
18679:
18678:
18673:
18663:
18662:
18661:
18656:
18651:
18646:
18636:
18631:
18630:
18629:
18624:
18619:
18609:
18608:
18607:
18602:
18597:
18592:
18587:
18582:
18572:
18567:
18562:
18557:
18556:
18555:
18550:
18545:
18540:
18530:
18525:
18523:Formation rule
18520:
18515:
18514:
18513:
18508:
18498:
18497:
18496:
18486:
18481:
18476:
18471:
18465:
18459:
18442:Formal systems
18438:
18437:
18434:
18433:
18431:
18430:
18425:
18420:
18415:
18410:
18405:
18400:
18395:
18390:
18385:
18384:
18383:
18378:
18367:
18365:
18361:
18360:
18358:
18357:
18356:
18355:
18345:
18340:
18339:
18338:
18331:Large cardinal
18328:
18323:
18318:
18313:
18308:
18294:
18293:
18292:
18287:
18282:
18267:
18265:
18255:
18254:
18252:
18251:
18250:
18249:
18244:
18239:
18229:
18224:
18219:
18214:
18209:
18204:
18199:
18194:
18189:
18184:
18179:
18174:
18168:
18166:
18159:
18158:
18156:
18155:
18154:
18153:
18148:
18143:
18138:
18133:
18128:
18120:
18119:
18118:
18113:
18103:
18098:
18096:Extensionality
18093:
18091:Ordinal number
18088:
18078:
18073:
18072:
18071:
18060:
18054:
18048:
18047:
18044:
18043:
18041:
18040:
18035:
18030:
18025:
18020:
18015:
18010:
18009:
18008:
17998:
17997:
17996:
17983:
17981:
17975:
17974:
17972:
17971:
17970:
17969:
17964:
17959:
17949:
17944:
17939:
17934:
17929:
17924:
17918:
17916:
17910:
17909:
17907:
17906:
17901:
17896:
17891:
17886:
17881:
17876:
17875:
17874:
17864:
17859:
17854:
17849:
17844:
17839:
17833:
17831:
17822:
17816:
17815:
17813:
17812:
17807:
17802:
17797:
17792:
17787:
17775:Cantor's
17773:
17768:
17763:
17753:
17751:
17738:
17737:
17735:
17734:
17729:
17724:
17719:
17714:
17709:
17704:
17699:
17694:
17689:
17684:
17679:
17674:
17673:
17672:
17661:
17659:
17655:
17654:
17647:
17646:
17639:
17632:
17624:
17618:
17617:
17612:
17607:
17583:
17563:
17535:(2): 115–144.
17515:
17514:
17491:
17466:
17444:
17437:
17410:
17389:
17367:
17352:
17337:
17319:
17312:
17303:10.1.1.73.9841
17284:
17277:
17243:
17241:
17238:
17237:
17236:
17230:
17225:
17219:
17212:
17209:
17140:
17120:
17116:
17093:
17089:
17068:
17048:
17028:
17013:
17012:
17001:
16995:
16989:
16983:
16980:
16977:
16974:
16971:
16968:
16959:
16950:
16944:
16938:
16935:
16913:
16912:
16901:
16895:
16892:
16889:
16886:
16883:
16880:
16877:
16874:
16844:
16843:
16832:
16826:
16823:
16817:
16814:
16712:
16707:consCode(h, t)
16667:
16664:
16656:
16655:
16640:
16637:
16634:
16631:
16628:
16625:
16622:
16619:
16616:
16610:
16607:
16604:
16601:
16598:
16595:
16589:
16586:
16583:
16577:
16574:
16568:
16562:
16559:
16556:
16553:
16550:
16547:
16544:
16541:
16538:
16535:
16532:
16526:
16523:
16520:
16517:
16514:
16511:
16508:
16505:
16502:
16499:
16496:
16493:
16491:
16489:
16486:
16485:
16482:
16476:
16473:
16470:
16467:
16464:
16461:
16458:
16455:
16452:
16446:
16443:
16440:
16437:
16434:
16431:
16429:
16427:
16424:
16423:
16420:
16417:
16411:
16405:
16402:
16396:
16390:
16387:
16384:
16381:
16378:
16375:
16372:
16369:
16366:
16363:
16360:
16357:
16354:
16351:
16348:
16346:
16344:
16341:
16340:
16337:
16331:
16328:
16325:
16322:
16319:
16316:
16313:
16310:
16307:
16301:
16298:
16295:
16292:
16289:
16286:
16284:
16282:
16279:
16278:
16275:
16272:
16269:
16266:
16263:
16260:
16257:
16254:
16251:
16249:
16247:
16244:
16243:
16224:
16218:
16217:
16216:
16204:
16201:
16198:
16195:
16192:
16189:
16183:
16180:
16177:
16173:
16169:
16166:
16163:
16160:
16157:
16154:
16148:
16145:
16142:
16139:
16133:
16130:
16127:
16121:
16118:
16115:
16112:
16108:
16105:
16102:
16099:
16096:
16093:
16090:
16087:
16084:
16081:
16078:
16075:
16072:
16069:
16066:
16062:
16059:
16056:
16053:
16047:
16044:
16041:
16038:
16035:
16032:
16029:
16014:
16013:
15998:
15995:
15992:
15989:
15986:
15983:
15980:
15977:
15974:
15971:
15968:
15965:
15962:
15959:
15956:
15953:
15950:
15947:
15944:
15942:
15940:
15937:
15936:
15933:
15930:
15927:
15925:
15923:
15920:
15919:
15916:
15913:
15910:
15908:
15906:
15903:
15902:
15899:
15896:
15893:
15891:
15889:
15886:
15885:
15882:
15879:
15876:
15874:
15872:
15869:
15868:
15853:
15850:
15828:
15827:
15821:
15810:
15807:
15804:
15801:
15798:
15792:
15789:
15786:
15783:
15780:
15777:
15774:
15763:
15762:
15756:
15745:
15742:
15739:
15736:
15733:
15727:
15724:
15721:
15718:
15715:
15712:
15709:
15698:
15697:
15686:
15675:
15672:
15666:
15663:
15660:
15657:
15651:
15648:
15645:
15642:
15639:
15636:
15633:
15630:
15627:
15624:
15621:
15618:
15607:
15606:
15603:
15592:
15589:
15586:
15575:
15574:
15567:
15556:
15550:
15547:
15541:
15538:
15535:
15532:
15521:
15520:
15517:
15508:
15507:
15501:
15495:
15485:
15484:
15478:
15467:
15464:
15463:
15462:
15459:
15452:
15449:
15440:
15439:
15436:
15430:
15429:
15426:
15420:
15419:
15416:
15410:
15409:
15406:
15400:
15399:
15396:
15390:
15389:
15386:
15368:
15367:List encodings
15365:
15364:
15363:
15348:
15345:
15342:
15336:
15330:
15327:
15324:
15321:
15318:
15315:
15312:
15309:
15306:
15303:
15301:
15299:
15296:
15295:
15292:
15289:
15286:
15283:
15280:
15277:
15274:
15271:
15268:
15262:
15259:
15253:
15247:
15244:
15241:
15238:
15235:
15232:
15230:
15228:
15225:
15224:
15221:
15218:
15212:
15206:
15203:
15200:
15197:
15194:
15188:
15185:
15182:
15179:
15176:
15173:
15170:
15167:
15164:
15161:
15155:
15152:
15149:
15146:
15143:
15140:
15138:
15136:
15133:
15132:
15129:
15126:
15120:
15114:
15111:
15105:
15099:
15096:
15093:
15090:
15087:
15084:
15081:
15078:
15075:
15072:
15069:
15066:
15060:
15057:
15054:
15051:
15048:
15045:
15042:
15039:
15036:
15033:
15027:
15024:
15021:
15018:
15015:
15012:
15010:
15008:
15005:
15004:
15001:
14998:
14992:
14986:
14983:
14980:
14974:
14971:
14968:
14966:
14952:
14951:
14936:
14933:
14930:
14927:
14924:
14921:
14918:
14915:
14912:
14906:
14903:
14900:
14897:
14894:
14891:
14889:
14887:
14884:
14883:
14880:
14877:
14874:
14871:
14868:
14865:
14862:
14859:
14856:
14850:
14847:
14844:
14841:
14838:
14835:
14833:
14831:
14828:
14827:
14824:
14818:
14812:
14809:
14806:
14803:
14800:
14797:
14794:
14791:
14788:
14785:
14782:
14779:
14777:
14775:
14772:
14771:
14742:
14739:
14738:
14737:
14726:
14723:
14717:
14711:
14708:
14705:
14699:
14696:
14690:
14684:
14681:
14678:
14672:
14669:
14666:
14663:
14660:
14657:
14654:
14651:
14648:
14645:
14631:
14630:
14619:
14616:
14613:
14610:
14607:
14604:
14601:
14598:
14595:
14592:
14589:
14586:
14583:
14569:
14568:
14556:
14553:
14547:
14541:
14538:
14535:
14529:
14526:
14523:
14520:
14517:
14514:
14511:
14508:
14505:
14502:
14488:
14487:
14476:
14470:
14467:
14464:
14461:
14458:
14455:
14449:
14446:
14443:
14440:
14437:
14434:
14411:
14391:
14371:
14351:
14335:
14332:
14331:
14330:
14315:
14312:
14309:
14306:
14303:
14300:
14297:
14294:
14291:
14288:
14285:
14282:
14279:
14276:
14273:
14270:
14267:
14264:
14261:
14255:
14252:
14249:
14246:
14243:
14240:
14237:
14234:
14231:
14228:
14225:
14222:
14219:
14216:
14213:
14210:
14207:
14204:
14201:
14198:
14195:
14192:
14189:
14186:
14183:
14180:
14177:
14174:
14171:
14168:
14165:
14162:
14159:
14156:
14153:
14150:
14147:
14144:
14141:
14138:
14135:
14132:
14129:
14126:
14123:
14120:
14117:
14114:
14111:
14108:
14105:
14102:
14099:
14096:
14093:
14090:
14087:
14084:
14081:
14078:
14075:
14072:
14069:
14066:
14063:
14060:
14057:
14054:
14051:
14048:
14045:
14039:
14036:
14033:
14030:
14027:
14024:
14021:
14019:
14017:
14011:
14006:
14002:
13998:
13997:
13994:
13991:
13988:
13985:
13982:
13979:
13976:
13973:
13970:
13967:
13964:
13958:
13955:
13952:
13949:
13946:
13943:
13940:
13937:
13934:
13931:
13928:
13925:
13922:
13919:
13913:
13907:
13904:
13901:
13898:
13895:
13892:
13889:
13886:
13883:
13880:
13877:
13874:
13871:
13868:
13865:
13862:
13859:
13856:
13853:
13850:
13847:
13844:
13841:
13838:
13835:
13832:
13829:
13823:
13817:
13814:
13811:
13808:
13805:
13802:
13799:
13796:
13793:
13790:
13787:
13784:
13781:
13779:
13777:
13771:
13766:
13762:
13758:
13757:
13754:
13751:
13748:
13745:
13742:
13739:
13736:
13733:
13730:
13727:
13724:
13721:
13718:
13715:
13712:
13709:
13706:
13703:
13700:
13697:
13694:
13688:
13685:
13682:
13679:
13676:
13673:
13670:
13667:
13664:
13658:
13655:
13652:
13649:
13646:
13643:
13640:
13637:
13634:
13631:
13628:
13625:
13622:
13619:
13616:
13613:
13610:
13607:
13604:
13598:
13595:
13592:
13589:
13586:
13583:
13580:
13577:
13574:
13568:
13565:
13559:
13553:
13550:
13547:
13544:
13541:
13538:
13535:
13532:
13529:
13526:
13524:
13522:
13519:
13516:
13513:
13510:
13507:
13506:
13503:
13500:
13497:
13494:
13491:
13488:
13485:
13482:
13479:
13476:
13473:
13470:
13467:
13464:
13461:
13458:
13455:
13452:
13449:
13446:
13443:
13440:
13434:
13431:
13425:
13422:
13416:
13410:
13407:
13404:
13401:
13398:
13395:
13392:
13389:
13386:
13383:
13381:
13379:
13376:
13373:
13370:
13367:
13364:
13363:
13349:
13348:
13333:
13327:
13321:
13318:
13315:
13312:
13309:
13306:
13303:
13300:
13297:
13294:
13291:
13288:
13286:
13284:
13281:
13280:
13277:
13271:
13268:
13262:
13259:
13256:
13250:
13247:
13244:
13241:
13238:
13235:
13232:
13229:
13226:
13224:
13222:
13219:
13218:
13215:
13212:
13209:
13206:
13203:
13200:
13197:
13194:
13191:
13188:
13185:
13182:
13179:
13176:
13173:
13170:
13167:
13161:
13158:
13155:
13152:
13149:
13146:
13143:
13140:
13137:
13131:
13128:
13125:
13122:
13119:
13116:
13114:
13110:
13106:
13102:
13101:
13098:
13092:
13086:
13083:
13080:
13077:
13074:
13071:
13068:
13065:
13062:
13059:
13056:
13053:
13051:
13047:
13043:
13039:
13038:
13035:
13029:
13023:
13020:
13017:
13014:
13011:
13008:
13005:
13002:
12999:
12997:
12995:
12992:
12991:
12988:
12982:
12976:
12973:
12970:
12967:
12964:
12961:
12958:
12955:
12952:
12950:
12948:
12945:
12944:
12891:
12890:
12878:
12875:
12872:
12869:
12866:
12863:
12857:
12854:
12851:
12848:
12841:
12837:
12834:
12831:
12828:
12825:
12822:
12816:
12813:
12810:
12807:
12800:
12797:
12790:
12787:
12784:
12781:
12778:
12775:
12772:
12769:
12766:
12751:logical values
12747:
12746:
12731:
12728:
12725:
12722:
12719:
12716:
12713:
12710:
12707:
12705:
12703:
12700:
12699:
12696:
12693:
12690:
12687:
12684:
12681:
12678:
12675:
12672:
12670:
12668:
12665:
12664:
12650:
12649:
12643:
12602:
12599:
12404:
12382:
12379:
12362:
12359:
12358:
12357:
12346:
12343:
12340:
12337:
12331:
12328:
12325:
12319:
12316:
12310:
12307:
12304:
12298:
12295:
12292:
12286:
12283:
12280:
12274:
12271:
12268:
12262:
12259:
12253:
12250:
12247:
12241:
12238:
12235:
12229:
12226:
12223:
12217:
12214:
12211:
12208:
12202:
12199:
12196:
12190:
12187:
12181:
12178:
12175:
12169:
12166:
12163:
12157:
12154:
12151:
12145:
12142:
12139:
12133:
12130:
12124:
12121:
12118:
12112:
12109:
12106:
12100:
12097:
12094:
12088:
12085:
12082:
12079:
12076:
12073:
12070:
12067:
12064:
12059:
12055:
12029:
12028:
12017:
12014:
12008:
12002:
11999:
11996:
11990:
11984:
11978:
11975:
11972:
11969:
11966:
11963:
11960:
11957:
11954:
11951:
11929:
11928:
11917:
11914:
11911:
11908:
11902:
11899:
11896:
11890:
11887:
11881:
11878:
11875:
11869:
11866:
11863:
11857:
11854:
11851:
11845:
11842:
11839:
11833:
11830:
11824:
11821:
11818:
11812:
11809:
11806:
11800:
11797:
11794:
11788:
11785:
11782:
11779:
11773:
11770:
11767:
11761:
11758:
11752:
11749:
11746:
11740:
11737:
11734:
11728:
11725:
11722:
11716:
11713:
11710:
11704:
11701:
11695:
11692:
11689:
11683:
11680:
11677:
11671:
11668:
11665:
11659:
11656:
11653:
11650:
11647:
11644:
11641:
11638:
11635:
11630:
11626:
11611:
11610:
11599:
11594:
11590:
11586:
11581:
11577:
11573:
11568:
11564:
11560:
11555:
11551:
11547:
11542:
11538:
11534:
11529:
11525:
11521:
11516:
11512:
11508:
11503:
11499:
11495:
11492:
11489:
11484:
11480:
11476:
11471:
11467:
11463:
11458:
11454:
11450:
11445:
11441:
11437:
11434:
11431:
11426:
11422:
11418:
11413:
11409:
11405:
11400:
11396:
11392:
11387:
11383:
11379:
11376:
11373:
11368:
11364:
11360:
11355:
11351:
11347:
11344:
11341:
11336:
11332:
11328:
11323:
11319:
11315:
11312:
11309:
11304:
11300:
11296:
11291:
11287:
11283:
11280:
11277:
11272:
11268:
11264:
11259:
11255:
11251:
11248:
11245:
11242:
11239:
11224:
11221:
11220:
11219:
11208:
11205:
11202:
11199:
11193:
11190:
11187:
11181:
11178:
11172:
11169:
11166:
11160:
11157:
11154:
11148:
11145:
11142:
11136:
11133:
11130:
11124:
11121:
11115:
11112:
11109:
11103:
11100:
11097:
11091:
11088:
11085:
11079:
11076:
11073:
11070:
11067:
11064:
11061:
11058:
11055:
11050:
11046:
11031:
11030:
11019:
11014:
11010:
11006:
11001:
10997:
10993:
10988:
10984:
10980:
10975:
10971:
10967:
10964:
10961:
10956:
10952:
10948:
10943:
10939:
10935:
10932:
10929:
10924:
10920:
10916:
10911:
10907:
10903:
10900:
10895:
10891:
10887:
10882:
10878:
10874:
10869:
10865:
10861:
10856:
10852:
10848:
10845:
10840:
10836:
10832:
10827:
10823:
10819:
10816:
10813:
10808:
10804:
10800:
10795:
10791:
10787:
10784:
10781:
10778:
10775:
10761:
10760:
10749:
10746:
10743:
10740:
10734:
10731:
10728:
10722:
10719:
10713:
10710:
10707:
10701:
10698:
10695:
10689:
10686:
10683:
10677:
10674:
10671:
10665:
10662:
10656:
10653:
10650:
10644:
10641:
10638:
10632:
10629:
10626:
10620:
10617:
10614:
10611:
10608:
10605:
10602:
10599:
10596:
10591:
10587:
10572:
10571:
10560:
10555:
10551:
10547:
10542:
10538:
10534:
10529:
10525:
10521:
10516:
10512:
10508:
10505:
10502:
10497:
10493:
10489:
10484:
10480:
10476:
10473:
10470:
10465:
10461:
10457:
10452:
10448:
10444:
10441:
10436:
10432:
10428:
10423:
10419:
10415:
10410:
10406:
10402:
10397:
10393:
10389:
10386:
10381:
10377:
10373:
10368:
10364:
10360:
10357:
10354:
10349:
10345:
10341:
10336:
10332:
10328:
10325:
10322:
10319:
10316:
10301:
10300:Plus and minus
10298:
10297:
10296:
10285:
10282:
10279:
10276:
10265:
10264:
10253:
10250:
10247:
10244:
10241:
10235:
10232:
10229:
10223:
10220:
10217:
10211:
10208:
10205:
10199:
10196:
10193:
10187:
10184:
10181:
10175:
10172:
10166:
10163:
10157:
10151:
10148:
10142:
10139:
10136:
10130:
10127:
10124:
10118:
10112:
10109:
10103:
10100:
10097:
10091:
10088:
10085:
10082:
10079:
10076:
10073:
10070:
10067:
10064:
10050:
10049:
10038:
10035:
10032:
10029:
10026:
10020:
10017:
10014:
10008:
10005:
10002:
9996:
9993:
9990:
9984:
9981:
9978:
9972:
9969:
9966:
9960:
9957:
9951:
9948:
9945:
9939:
9933:
9930:
9924:
9921:
9918:
9912:
9909:
9906:
9900:
9894:
9891:
9885:
9882:
9879:
9873:
9870:
9867:
9864:
9861:
9858:
9855:
9837:
9836:
9825:
9822:
9816:
9813:
9810:
9804:
9801:
9795:
9792:
9789:
9783:
9780:
9777:
9774:
9771:
9768:
9763:
9759:
9744:
9743:
9732:
9726:
9720:
9717:
9714:
9711:
9708:
9705:
9700:
9696:
9678:signed numbers
9673:
9672:Signed numbers
9670:
9667:
9661:
9654:
9646:
9645:
9633:
9630:
9624:
9621:
9618:
9612:
9606:
9603:
9597:
9594:
9591:
9588:
9585:
9582:
9579:
9576:
9573:
9570:
9567:
9564:
9558:
9555:
9552:
9549:
9543:
9537:
9534:
9531:
9528:
9525:
9522:
9519:
9516:
9513:
9507:
9504:
9501:
9498:
9495:
9492:
9486:
9483:
9480:
9474:
9471:
9465:
9462:
9459:
9456:
9453:
9450:
9447:
9444:
9438:
9435:
9432:
9429:
9426:
9423:
9420:
9417:
9414:
9411:
9408:
9405:
9402:
9399:
9396:
9393:
9390:
9387:
9384:
9381:
9375:
9372:
9369:
9366:
9360:
9354:
9348:
9342:
9339:
9333:
9330:
9324:
9321:
9315:
9309:
9306:
9303:
9300:
9297:
9294:
9291:
9288:
9285:
9282:
9276:
9270:
9267:
9264:
9261:
9258:
9255:
9252:
9249:
9246:
9243:
9237:
9234:
9231:
9228:
9225:
9222:
9219:
9216:
9213:
9210:
9207:
9204:
9201:
9198:
9192:
9189:
9186:
9183:
9180:
9177:
9174:
9171:
9168:
9165:
9162:
9159:
9156:
9153:
9150:
9147:
9144:
9141:
9138:
9135:
9132:
9129:
9126:
9123:
9120:
9114:
9111:
9108:
9105:
9099:
9096:
9090:
9087:
9084:
9081:
9078:
9072:
9069:
9063:
9060:
9057:
9054:
9051:
9048:
9045:
9042:
9039:
9036:
9033:
9030:
9027:
9024:
9021:
9006:
9005:
8990:
8987:
8984:
8981:
8978:
8975:
8969:
8966:
8963:
8960:
8957:
8954:
8948:
8945:
8942:
8936:
8933:
8927:
8924:
8921:
8918:
8915:
8912:
8909:
8906:
8900:
8897:
8894:
8891:
8888:
8885:
8882:
8879:
8876:
8873:
8870:
8867:
8865:
8863:
8860:
8859:
8856:
8853:
8850:
8847:
8844:
8841:
8838:
8835:
8832:
8829:
8826:
8823:
8821:
8819:
8816:
8815:
8805:
8804:
8803:
8788:
8785:
8782:
8779:
8776:
8773:
8770:
8767:
8764:
8762:
8760:
8757:
8756:
8753:
8750:
8747:
8744:
8741:
8738:
8735:
8732:
8729:
8727:
8725:
8722:
8721:
8696:
8690:
8687:
8684:
8681:
8678:
8675:
8669:
8666:
8663:
8660:
8657:
8654:
8652:
8650:
8647:
8646:
8643:
8640:
8637:
8634:
8631:
8628:
8625:
8622:
8619:
8617:
8615:
8612:
8611:
8608:
8605:
8602:
8596:
8593:
8587:
8584:
8581:
8578:
8575:
8569:
8566:
8563:
8557:
8554:
8548:
8545:
8542:
8539:
8536:
8533:
8530:
8527:
8524:
8521:
8519:
8517:
8514:
8513:
8510:
8507:
8501:
8495:
8492:
8486:
8483:
8480:
8477:
8474:
8471:
8468:
8465:
8462:
8459:
8456:
8453:
8451:
8449:
8446:
8445:
8442:
8436:
8433:
8430:
8428:
8426:
8423:
8422:
8408:
8407:
8396:
8393:
8387:
8384:
8381:
8375:
8372:
8369:
8366:
8363:
8360:
8357:
8343:
8342:
8331:
8328:
8322:
8316:
8313:
8310:
8304:
8301:
8298:
8295:
8289:
8283:
8277:
8271:
8268:
8262:
8259:
8253:
8250:
8244:
8238:
8235:
8229:
8223:
8220:
8217:
8214:
8211:
8208:
8205:
8202:
8199:
8196:
8193:
8190:
8187:
8184:
8181:
8178:
8175:
8172:
8169:
8166:
8163:
8160:
8157:
8143:
8142:
8131:
8128:
8125:
8114:
8103:
8097:
8094:
8091:
8088:
8062:
8061:
8050:
8047:
8041:
8038:
8035:
8029:
8026:
8023:
8020:
8014:
8011:
7973:
7969:
7965:
7962:
7959:
7956:
7953:
7933:
7927:
7921:
7918:
7907:
7906:
7895:
7892:
7886:
7880:
7877:
7874:
7868:
7865:
7862:
7859:
7853:
7847:
7841:
7835:
7832:
7829:
7823:
7820:
7814:
7811:
7805:
7799:
7796:
7790:
7784:
7781:
7778:
7775:
7772:
7769:
7766:
7763:
7757:
7751:
7745:
7739:
7736:
7713:
7710:
7707:
7687:
7684:
7681:
7670:
7669:
7658:
7655:
7649:
7643:
7640:
7637:
7631:
7628:
7600:
7597:
7594:
7583:
7582:
7571:
7565:
7562:
7556:
7552:
7548:
7545:
7542:
7539:
7536:
7533:
7530:
7524:
7521:
7515:
7512:
7509:
7503:
7500:
7497:
7494:
7490:
7486:
7468:
7465:
7464:
7463:
7448:
7442:
7440:
7437:
7436:
7433:
7430:
7424:
7421:
7415:
7412:
7409:
7403:
7400:
7394:
7392:
7389:
7388:
7385:
7382:
7379:
7373:
7370:
7364:
7361:
7358:
7352:
7349:
7346:
7340:
7337:
7331:
7329:
7326:
7325:
7322:
7319:
7316:
7313:
7307:
7304:
7298:
7295:
7292:
7286:
7283:
7280:
7274:
7271:
7268:
7262:
7259:
7253:
7251:
7248:
7247:
7244:
7241:
7238:
7235:
7232:
7226:
7223:
7217:
7214:
7211:
7205:
7202:
7199:
7193:
7190:
7187:
7181:
7178:
7175:
7169:
7166:
7160:
7158:
7155:
7152:
7149:
7146:
7145:
7122:
7119:
7116:
7105:
7104:
7089:
7086:
7080:
7077:
7071:
7068:
7062:
7059:
7053:
7050:
7047:
7041:
7039:
7036:
7033:
7032:
7029:
7023:
7020:
7014:
7011:
7005:
7003:
7000:
6997:
6996:
6993:
6990:
6984:
6981:
6978:
6975:
6972:
6969:
6966:
6960:
6958:
6955:
6952:
6951:
6948:
6945:
6942:
6936:
6933:
6930:
6924:
6921:
6918:
6912:
6909:
6903:
6900:
6897:
6891:
6888:
6882:
6879:
6876:
6870:
6868:
6865:
6862:
6861:
6846:
6843:
6840:
6839:
6838:
6837:
6826:
6823:
6820:
6817:
6814:
6811:
6797:
6796:
6785:
6782:
6779:
6773:
6770:
6756:
6755:
6744:
6738:
6735:
6732:
6729:
6726:
6723:
6720:
6714:
6711:
6708:
6702:
6699:
6696:
6693:
6683:
6672:
6666:
6663:
6660:
6657:
6651:
6648:
6613:
6610:
6609:
6608:
6597:
6591:
6588:
6585:
6579:
6576:
6562:
6561:
6550:
6547:
6544:
6538:
6532:
6529:
6511:
6510:
6499:
6496:
6493:
6490:
6487:
6484:
6469:
6466:
6464:
6463:
6462:
6451:
6448:
6442:
6439:
6433:
6430:
6427:
6424:
6421:
6418:
6415:
6412:
6409:
6399:
6388:
6385:
6379:
6376:
6370:
6367:
6364:
6361:
6355:
6352:
6338:
6337:
6326:
6320:
6317:
6314:
6308:
6302:
6299:
6296:
6293:
6287:
6273:
6272:
6261:
6255:
6252:
6249:
6246:
6232:
6231:
6220:
6217:
6211:
6208:
6202:
6199:
6196:
6193:
6190:
6184:
6181:
6178:
6172:
6169:
6142:
6139:
6138:
6137:
6126:
6123:
6117:
6114:
6111:
6108:
6105:
6102:
6099:
6096:
6093:
6090:
6076:
6075:
6064:
6058:
6055:
6052:
6046:
6040:
6037:
6022:
6019:
6014:
6013:
6002:
5999:
5996:
5993:
5990:
5987:
5981:
5978:
5975:
5972:
5969:
5966:
5960:
5957:
5954:
5948:
5945:
5939:
5936:
5933:
5930:
5927:
5924:
5921:
5918:
5912:
5909:
5906:
5903:
5900:
5897:
5894:
5891:
5888:
5885:
5882:
5879:
5861:
5860:
5845:
5842:
5839:
5836:
5833:
5830:
5828:
5826:
5823:
5822:
5819:
5813:
5810:
5807:
5804:
5801:
5798:
5796:
5794:
5791:
5790:
5787:
5784:
5778:
5775:
5769:
5766:
5763:
5760:
5757:
5754:
5751:
5748:
5745:
5743:
5741:
5738:
5737:
5734:
5731:
5728:
5725:
5719:
5716:
5713:
5711:
5709:
5706:
5703:
5700:
5699:
5696:
5693:
5687:
5684:
5681:
5678:
5675:
5672:
5669:
5666:
5663:
5660:
5658:
5656:
5653:
5652:
5618:
5617:
5606:
5603:
5600:
5597:
5594:
5591:
5588:
5585:
5582:
5579:
5573:
5567:
5564:
5561:
5558:
5555:
5552:
5549:
5546:
5543:
5540:
5537:
5534:
5531:
5528:
5525:
5522:
5519:
5516:
5510:
5504:
5501:
5498:
5495:
5492:
5489:
5483:
5480:
5477:
5471:
5468:
5465:
5462:
5459:
5456:
5453:
5450:
5447:
5444:
5441:
5438:
5435:
5432:
5429:
5426:
5423:
5420:
5414:
5411:
5408:
5405:
5402:
5399:
5396:
5393:
5390:
5387:
5384:
5381:
5378:
5318:
5317:
5306:
5303:
5300:
5297:
5294:
5291:
5285:
5279:
5276:
5273:
5270:
5267:
5264:
5261:
5258:
5255:
5252:
5249:
5246:
5243:
5240:
5234:
5228:
5225:
5219:
5216:
5213:
5207:
5204:
5201:
5198:
5195:
5192:
5189:
5186:
5183:
5180:
5177:
5174:
5171:
5168:
5165:
5162:
5159:
5156:
5150:
5147:
5144:
5141:
5138:
5135:
5132:
5129:
5126:
5123:
5120:
5117:
5114:
5092:
5091:
5080:
5077:
5074:
5071:
5065:
5062:
5059:
5053:
5050:
5032:
5031:
5020:
5017:
5011:
5008:
5002:
4999:
4996:
4993:
4990:
4984:
4981:
4978:
4972:
4969:
4955:
4954:
4939:
4936:
4930:
4924:
4921:
4918:
4915:
4912:
4909:
4903:
4900:
4897:
4894:
4891:
4883:
4880:
4877:
4873:
4869:
4863:
4860:
4857:
4854:
4848:
4845:
4842:
4839:
4837:
4834:
4828:
4822:
4819:
4813:
4810:
4807:
4804:
4801:
4793:
4789:
4785:
4779:
4776:
4773:
4770:
4764:
4761:
4758:
4755:
4753:
4750:
4749:
4746:
4743:
4741:
4738:
4736:
4733:
4732:
4729:
4726:
4723:
4717:
4714:
4708:
4705:
4699:
4696:
4693:
4690:
4687:
4684:
4678:
4675:
4672:
4666:
4663:
4660:
4654:
4651:
4648:
4646:
4643:
4640:
4637:
4631:
4628:
4622:
4619:
4613:
4610:
4604:
4601:
4598:
4595:
4592:
4589:
4583:
4580:
4577:
4571:
4568:
4565:
4559:
4556:
4553:
4551:
4548:
4547:
4544:
4541:
4535:
4532:
4526:
4523:
4520:
4517:
4514:
4508:
4505:
4502:
4496:
4493:
4490:
4488:
4485:
4482:
4476:
4473:
4467:
4464:
4458:
4455:
4452:
4449:
4446:
4440:
4437:
4434:
4428:
4425:
4422:
4420:
4417:
4416:
4413:
4407:
4404:
4401:
4398:
4392:
4389:
4386:
4384:
4381:
4375:
4372:
4366:
4363:
4360:
4357:
4351:
4348:
4345:
4343:
4340:
4339:
4335:
4329:
4326:
4323:
4320:
4317:
4315:
4312:
4311:
4303:
4296:
4289:
4288:
4213:
4212:
4198:
4186:
4184:
4181:
4178:
4175:
4174:
4171:
4168:
4165:
4162:
4152:
4150:
4147:
4146:
4144:
4139:
4136:
4133:
4130:
4127:
4124:
4109:
4106:
4103:
4102:
4100:
4099:
4088:
4085:
4082:
4079:
4076:
4073:
4070:
4067:
4064:
4054:
4043:
4040:
4037:
4034:
4031:
4028:
4025:
4004:
3991:
3988:
3985:
3982:
3979:
3976:
3973:
3952:
3951:
3942:
3941:
3930:
3927:
3924:
3921:
3918:
3915:
3912:
3909:
3906:
3903:
3893:
3890:
3879:
3873:
3870:
3867:
3864:
3861:
3858:
3852:
3846:
3843:
3833:
3822:
3819:
3814:
3810:
3806:
3801:
3797:
3791:
3788:
3784:
3780:
3777:
3774:
3766:
3763:
3760:
3756:
3745:
3734:
3731:
3728:
3718:
3707:
3706:
3694:
3691:
3688:
3685:
3682:
3679:
3673:
3670:
3667:
3664:
3661:
3658:
3652:
3649:
3646:
3640:
3637:
3631:
3628:
3625:
3622:
3619:
3616:
3613:
3610:
3604:
3601:
3598:
3595:
3592:
3589:
3586:
3583:
3580:
3577:
3566:
3555:
3552:
3549:
3546:
3543:
3537:
3534:
3528:
3522:
3519:
3516:
3513:
3510:
3507:
3504:
3494:
3483:
3480:
3475:
3472:
3469:
3465:
3461:
3458:
3455:
3452:
3449:
3446:
3441:
3437:
3426:
3415:
3412:
3409:
3399:
3393:
3392:
3381:
3375:
3372:
3369:
3366:
3363:
3360:
3357:
3347:
3336:
3330:
3324:
3321:
3315:
3312:
3309:
3306:
3303:
3300:
3297:
3294:
3291:
3288:
3285:
3282:
3279:
3276:
3266:
3255:
3249:
3243:
3240:
3234:
3231:
3228:
3225:
3219:
3213:
3207:
3201:
3198:
3188:
3177:
3169:
3165:
3161:
3158:
3152:
3146:
3136:
3123:
3119:
3108:
3106:Exponentiation
3102:
3101:
3090:
3087:
3081:
3078:
3072:
3069:
3066:
3063:
3060:
3057:
3054:
3051:
3048:
3045:
3035:
3024:
3018:
3015:
3009:
3006:
3000:
2997:
2994:
2991:
2988:
2985:
2982:
2979:
2976:
2973:
2970:
2967:
2964:
2954:
2943:
2937:
2934:
2928:
2925:
2919:
2916:
2913:
2907:
2901:
2895:
2889:
2886:
2876:
2865:
2857:
2853:
2847:
2843:
2839:
2836:
2833:
2825:
2822:
2819:
2815:
2804:
2793:
2790:
2787:
2777:
2775:Multiplication
2771:
2770:
2759:
2756:
2753:
2750:
2747:
2744:
2741:
2738:
2735:
2732:
2722:
2711:
2708:
2702:
2696:
2693:
2687:
2681:
2678:
2675:
2672:
2669:
2666:
2663:
2660:
2657:
2654:
2651:
2648:
2645:
2635:
2624:
2621:
2615:
2609:
2606:
2600:
2594:
2591:
2588:
2582:
2576:
2570:
2564:
2561:
2551:
2540:
2537:
2532:
2528:
2524:
2519:
2515:
2511:
2508:
2500:
2497:
2494:
2490:
2479:
2468:
2465:
2462:
2452:
2446:
2445:
2442:
2431:
2428:
2422:
2416:
2413:
2407:
2404:
2401:
2398:
2395:
2392:
2389:
2386:
2383:
2380:
2370:
2359:
2356:
2350:
2344:
2341:
2335:
2332:
2329:
2323:
2317:
2311:
2308:
2298:
2287:
2284:
2279:
2275:
2271:
2268:
2265:
2262:
2254:
2251:
2248:
2244:
2233:
2222:
2219:
2216:
2206:
2200:
2199:
2196:
2193:
2190:
2187:
2180:
2177:
2176:
2175:
2164:
2158:
2155:
2152:
2149:
2146:
2143:
2140:
2137:
2134:
2131:
2128:
2125:
2088:
2087:
2076:
2073:
2070:
2067:
2064:
2061:
2055:
2052:
2049:
2046:
2043:
2040:
2034:
2031:
2028:
2022:
2019:
2013:
2010:
2007:
2004:
2001:
1998:
1995:
1992:
1986:
1983:
1980:
1977:
1974:
1971:
1968:
1965:
1962:
1959:
1956:
1953:
1930:
1927:
1924:
1921:
1918:
1907:
1906:
1895:
1889:
1886:
1883:
1880:
1877:
1874:
1871:
1868:
1865:
1851:
1850:
1839:
1833:
1830:
1825:
1821:
1817:
1814:
1808:
1802:
1799:
1776:
1768:
1764:
1760:
1757:
1751:
1745:
1725:
1722:
1719:
1716:
1713:
1710:
1707:
1687:
1679:
1675:
1671:
1668:
1662:
1656:
1634:
1630:
1626:
1623:
1620:
1617:
1614:
1611:
1608:
1605:
1594:
1593:
1582:
1576:
1573:
1567:
1564:
1558:
1555:
1552:
1549:
1546:
1543:
1540:
1537:
1534:
1531:
1528:
1525:
1522:
1519:
1516:
1493:
1490:
1487:
1482:
1479:
1475:
1469:
1466:
1462:
1458:
1455:
1452:
1449:
1446:
1441:
1438:
1435:
1432:
1429:
1426:
1422:
1401:
1398:
1395:
1392:
1389:
1386:
1383:
1380:
1377:
1374:
1371:
1360:
1359:
1348:
1345:
1339:
1333:
1330:
1324:
1321:
1318:
1315:
1312:
1309:
1306:
1303:
1300:
1297:
1294:
1291:
1268:
1265:
1259:
1256:
1253:
1229:
1226:
1223:
1220:
1217:
1214:
1211:
1208:
1205:
1194:
1193:
1182:
1179:
1173:
1167:
1164:
1158:
1152:
1149:
1146:
1143:
1140:
1137:
1134:
1131:
1128:
1125:
1122:
1119:
1116:
1113:
1110:
1087:
1084:
1081:
1078:
1073:
1070:
1066:
1062:
1057:
1054:
1050:
1046:
1043:
1040:
1037:
1032:
1029:
1026:
1023:
1020:
1017:
1013:
992:
989:
986:
983:
980:
977:
974:
971:
968:
965:
962:
936:
933:
908:
907:
892:
884:
881:
877:
873:
870:
867:
864:
861:
858:
855:
852:
849:
847:
839:
835:
831:
828:
822:
816:
813:
811:
808:
807:
804:
801:
799:
796:
794:
791:
790:
787:
784:
781:
775:
772:
766:
763:
757:
754:
751:
748:
745:
742:
739:
736:
733:
730:
728:
725:
722:
716:
713:
707:
704:
698:
695:
692:
686:
680:
677:
675:
672:
671:
668:
665:
659:
656:
650:
647:
644:
641:
638:
635:
632:
629:
626:
623:
621:
618:
612:
609:
603:
600:
597:
591:
585:
582:
580:
577:
576:
573:
567:
564:
561:
558:
555:
552:
549:
546:
543:
540:
538:
532:
529:
526:
520:
514:
511:
509:
506:
505:
502:
499:
496:
493:
490:
487:
484:
481:
478:
475:
473:
470:
467:
461:
455:
452:
450:
447:
446:
438:
431:
424:
423:
365:
364:
352:
342:
336:
332:
329:
326:
323:
320:
317:
314:
307:
302:
299:
295:
263:
239:
236:
187:
167:
164:
161:
158:
138:
135:
132:
129:
117:
114:
73:
72:
52:the key points
42:
40:
33:
26:
9:
6:
4:
3:
2:
19641:
19630:
19627:
19626:
19624:
19609:
19606:
19604:
19601:
19600:
19598:
19594:
19588:
19585:
19583:
19580:
19579:
19577:
19573:
19567:
19564:
19562:
19559:
19557:
19554:
19552:
19549:
19547:
19544:
19542:
19539:
19537:
19534:
19532:
19529:
19527:
19524:
19522:
19519:
19517:
19514:
19512:
19509:
19507:
19504:
19502:
19501:Alfred Foster
19499:
19497:
19494:
19492:
19489:
19487:
19486:William Boone
19484:
19482:
19479:
19477:
19476:Peter Andrews
19474:
19472:
19469:
19467:
19464:
19463:
19461:
19457:
19451:
19448:
19446:
19443:
19439:
19436:
19434:
19431:
19429:
19426:
19425:
19424:
19421:
19420:
19418:
19416:Notable ideas
19414:
19410:
19409:Alonzo Church
19403:
19398:
19396:
19391:
19389:
19384:
19383:
19380:
19370:
19369:
19364:
19356:
19350:
19347:
19345:
19342:
19340:
19337:
19335:
19332:
19328:
19325:
19324:
19323:
19320:
19318:
19315:
19313:
19310:
19308:
19304:
19301:
19299:
19296:
19294:
19291:
19289:
19286:
19284:
19281:
19280:
19278:
19274:
19268:
19265:
19263:
19260:
19258:
19257:Recursive set
19255:
19253:
19250:
19248:
19245:
19243:
19240:
19238:
19235:
19231:
19228:
19226:
19223:
19221:
19218:
19216:
19213:
19211:
19208:
19207:
19206:
19203:
19201:
19198:
19196:
19193:
19191:
19188:
19186:
19183:
19181:
19178:
19177:
19175:
19173:
19169:
19163:
19160:
19158:
19155:
19153:
19150:
19148:
19145:
19143:
19140:
19138:
19135:
19133:
19130:
19126:
19123:
19121:
19118:
19116:
19113:
19112:
19111:
19108:
19106:
19103:
19101:
19098:
19096:
19093:
19091:
19088:
19086:
19083:
19079:
19076:
19075:
19074:
19071:
19067:
19066:of arithmetic
19064:
19063:
19062:
19059:
19055:
19052:
19050:
19047:
19045:
19042:
19040:
19037:
19035:
19032:
19031:
19030:
19027:
19023:
19020:
19018:
19015:
19014:
19013:
19010:
19009:
19007:
19005:
19001:
18995:
18992:
18990:
18987:
18985:
18982:
18980:
18977:
18974:
18973:from ZFC
18970:
18967:
18965:
18962:
18956:
18953:
18952:
18951:
18948:
18946:
18943:
18941:
18938:
18937:
18936:
18933:
18931:
18928:
18926:
18923:
18921:
18918:
18916:
18913:
18911:
18908:
18906:
18903:
18902:
18900:
18898:
18894:
18884:
18883:
18879:
18878:
18873:
18872:non-Euclidean
18870:
18866:
18863:
18861:
18858:
18856:
18855:
18851:
18850:
18848:
18845:
18844:
18842:
18838:
18834:
18831:
18829:
18826:
18825:
18824:
18820:
18816:
18813:
18812:
18811:
18807:
18803:
18800:
18798:
18795:
18793:
18790:
18788:
18785:
18783:
18780:
18778:
18775:
18774:
18772:
18768:
18767:
18765:
18760:
18754:
18749:Example
18746:
18738:
18733:
18732:
18731:
18728:
18726:
18723:
18719:
18716:
18714:
18711:
18709:
18706:
18704:
18701:
18700:
18699:
18696:
18694:
18691:
18689:
18686:
18684:
18681:
18677:
18674:
18672:
18669:
18668:
18667:
18664:
18660:
18657:
18655:
18652:
18650:
18647:
18645:
18642:
18641:
18640:
18637:
18635:
18632:
18628:
18625:
18623:
18620:
18618:
18615:
18614:
18613:
18610:
18606:
18603:
18601:
18598:
18596:
18593:
18591:
18588:
18586:
18583:
18581:
18578:
18577:
18576:
18573:
18571:
18568:
18566:
18563:
18561:
18558:
18554:
18551:
18549:
18546:
18544:
18541:
18539:
18536:
18535:
18534:
18531:
18529:
18526:
18524:
18521:
18519:
18516:
18512:
18509:
18507:
18506:by definition
18504:
18503:
18502:
18499:
18495:
18492:
18491:
18490:
18487:
18485:
18482:
18480:
18477:
18475:
18472:
18470:
18467:
18466:
18463:
18460:
18458:
18454:
18449:
18443:
18439:
18429:
18426:
18424:
18421:
18419:
18416:
18414:
18411:
18409:
18406:
18404:
18401:
18399:
18396:
18394:
18393:Kripke–Platek
18391:
18389:
18386:
18382:
18379:
18377:
18374:
18373:
18372:
18369:
18368:
18366:
18362:
18354:
18351:
18350:
18349:
18346:
18344:
18341:
18337:
18334:
18333:
18332:
18329:
18327:
18324:
18322:
18319:
18317:
18314:
18312:
18309:
18306:
18302:
18298:
18295:
18291:
18288:
18286:
18283:
18281:
18278:
18277:
18276:
18272:
18269:
18268:
18266:
18264:
18260:
18256:
18248:
18245:
18243:
18240:
18238:
18237:constructible
18235:
18234:
18233:
18230:
18228:
18225:
18223:
18220:
18218:
18215:
18213:
18210:
18208:
18205:
18203:
18200:
18198:
18195:
18193:
18190:
18188:
18185:
18183:
18180:
18178:
18175:
18173:
18170:
18169:
18167:
18165:
18160:
18152:
18149:
18147:
18144:
18142:
18139:
18137:
18134:
18132:
18129:
18127:
18124:
18123:
18121:
18117:
18114:
18112:
18109:
18108:
18107:
18104:
18102:
18099:
18097:
18094:
18092:
18089:
18087:
18083:
18079:
18077:
18074:
18070:
18067:
18066:
18065:
18062:
18061:
18058:
18055:
18053:
18049:
18039:
18036:
18034:
18031:
18029:
18026:
18024:
18021:
18019:
18016:
18014:
18011:
18007:
18004:
18003:
18002:
17999:
17995:
17990:
17989:
17988:
17985:
17984:
17982:
17980:
17976:
17968:
17965:
17963:
17960:
17958:
17955:
17954:
17953:
17950:
17948:
17945:
17943:
17940:
17938:
17935:
17933:
17930:
17928:
17925:
17923:
17920:
17919:
17917:
17915:
17914:Propositional
17911:
17905:
17902:
17900:
17897:
17895:
17892:
17890:
17887:
17885:
17882:
17880:
17877:
17873:
17870:
17869:
17868:
17865:
17863:
17860:
17858:
17855:
17853:
17850:
17848:
17845:
17843:
17842:Logical truth
17840:
17838:
17835:
17834:
17832:
17830:
17826:
17823:
17821:
17817:
17811:
17808:
17806:
17803:
17801:
17798:
17796:
17793:
17791:
17788:
17786:
17782:
17778:
17774:
17772:
17769:
17767:
17764:
17762:
17758:
17755:
17754:
17752:
17750:
17744:
17739:
17733:
17730:
17728:
17725:
17723:
17720:
17718:
17715:
17713:
17710:
17708:
17705:
17703:
17700:
17698:
17695:
17693:
17690:
17688:
17685:
17683:
17680:
17678:
17675:
17671:
17668:
17667:
17666:
17663:
17662:
17660:
17656:
17652:
17645:
17640:
17638:
17633:
17631:
17626:
17625:
17622:
17616:
17613:
17611:
17608:
17602:
17597:
17593:
17589:
17584:
17580:
17576:
17569:
17564:
17560:
17556:
17552:
17548:
17543:
17538:
17534:
17530:
17523:
17518:
17517:
17510:
17506:
17502:
17495:
17478:
17469:
17463:
17459:
17455:
17448:
17440:
17434:
17430:
17426:
17425:
17420:
17414:
17406:
17405:
17400:
17393:
17385:
17381:
17377:
17371:
17363:
17356:
17348:
17341:
17333:
17329:
17323:
17315:
17309:
17304:
17299:
17295:
17288:
17280:
17274:
17270:
17266:
17262:
17261:
17253:
17251:
17249:
17244:
17234:
17231:
17229:
17226:
17223:
17220:
17218:
17215:
17214:
17208:
17138:
17134:
17118:
17114:
17091:
17087:
17066:
17046:
17026:
17018:
16999:
16993:
16987:
16981:
16978:
16975:
16972:
16969:
16966:
16957:
16948:
16942:
16936:
16933:
16926:
16925:
16924:
16899:
16893:
16890:
16887:
16884:
16881:
16878:
16875:
16872:
16865:
16864:
16863:
16830:
16824:
16821:
16815:
16812:
16805:
16804:
16803:
16710:
16685:notation, if
16684:
16679:
16677:
16673:
16672:continuations
16663:
16661:
16635:
16632:
16629:
16626:
16623:
16620:
16617:
16605:
16602:
16599:
16596:
16581:
16575:
16566:
16560:
16557:
16554:
16551:
16548:
16545:
16542:
16539:
16536:
16533:
16524:
16521:
16518:
16515:
16512:
16509:
16506:
16503:
16500:
16497:
16494:
16492:
16487:
16480:
16471:
16468:
16465:
16462:
16459:
16456:
16453:
16444:
16441:
16438:
16435:
16432:
16430:
16425:
16415:
16409:
16403:
16394:
16388:
16385:
16382:
16379:
16376:
16373:
16370:
16367:
16364:
16361:
16358:
16355:
16352:
16349:
16347:
16342:
16335:
16326:
16323:
16320:
16317:
16314:
16311:
16308:
16299:
16296:
16293:
16290:
16287:
16285:
16280:
16273:
16270:
16267:
16264:
16261:
16258:
16255:
16252:
16250:
16245:
16234:
16233:
16232:
16230:
16223:
16106:
16103:
16100:
16097:
16094:
16091:
16088:
16085:
16082:
16076:
16073:
16070:
16067:
16064:
16019:
16018:
16017:
15996:
15990:
15987:
15984:
15981:
15978:
15975:
15972:
15969:
15966:
15963:
15957:
15954:
15951:
15948:
15945:
15943:
15938:
15931:
15928:
15926:
15921:
15914:
15911:
15909:
15904:
15897:
15894:
15892:
15887:
15880:
15877:
15875:
15870:
15859:
15858:
15857:
15849:
15847:
15843:
15839:
15835:
15826:is the tail.
15825:
15824:second.second
15822:
15805:
15802:
15799:
15790:
15787:
15784:
15781:
15778:
15775:
15772:
15765:
15764:
15761:is the head.
15760:
15757:
15740:
15737:
15734:
15725:
15722:
15719:
15716:
15713:
15710:
15707:
15700:
15699:
15695:
15691:
15687:
15670:
15664:
15661:
15658:
15649:
15646:
15643:
15640:
15637:
15634:
15631:
15628:
15625:
15622:
15619:
15616:
15609:
15608:
15604:
15590:
15587:
15584:
15577:
15576:
15572:
15568:
15554:
15548:
15545:
15539:
15536:
15533:
15530:
15523:
15522:
15518:
15515:
15514:
15511:
15505:
15504:Second.Second
15502:
15499:
15496:
15493:
15490:
15489:
15488:
15482:
15479:
15476:
15473:
15472:
15471:
15460:
15457:
15453:
15450:
15447:
15446:
15445:
15437:
15435:
15432:
15431:
15427:
15425:
15422:
15421:
15417:
15415:
15412:
15411:
15407:
15405:
15402:
15401:
15397:
15395:
15392:
15391:
15387:
15384:
15383:
15380:
15378:
15374:
15346:
15343:
15340:
15334:
15325:
15322:
15319:
15316:
15313:
15310:
15307:
15302:
15297:
15287:
15284:
15281:
15278:
15275:
15272:
15269:
15257:
15251:
15245:
15242:
15239:
15236:
15231:
15226:
15216:
15210:
15204:
15201:
15198:
15195:
15180:
15177:
15174:
15171:
15168:
15165:
15162:
15153:
15150:
15147:
15144:
15139:
15134:
15124:
15118:
15109:
15103:
15097:
15094:
15091:
15088:
15085:
15082:
15079:
15076:
15073:
15070:
15052:
15049:
15046:
15043:
15040:
15037:
15034:
15025:
15022:
15019:
15016:
15011:
15006:
14996:
14990:
14984:
14981:
14972:
14969:
14957:
14956:
14955:
14954:For example,
14931:
14928:
14925:
14922:
14919:
14916:
14913:
14904:
14901:
14898:
14895:
14892:
14890:
14885:
14875:
14872:
14869:
14866:
14863:
14860:
14857:
14848:
14845:
14842:
14839:
14836:
14834:
14829:
14822:
14816:
14810:
14807:
14804:
14801:
14798:
14795:
14792:
14789:
14786:
14783:
14780:
14778:
14773:
14762:
14761:
14760:
14758:
14754:
14748:
14721:
14715:
14709:
14706:
14694:
14688:
14682:
14679:
14670:
14667:
14664:
14661:
14658:
14655:
14652:
14649:
14646:
14643:
14636:
14635:
14634:
14614:
14611:
14608:
14605:
14602:
14599:
14596:
14590:
14587:
14584:
14581:
14574:
14573:
14572:
14551:
14545:
14539:
14536:
14527:
14524:
14521:
14518:
14515:
14512:
14509:
14506:
14503:
14500:
14493:
14492:
14491:
14474:
14465:
14462:
14459:
14456:
14447:
14444:
14441:
14438:
14435:
14432:
14425:
14424:
14423:
14409:
14389:
14369:
14349:
14341:
14313:
14310:
14307:
14304:
14301:
14298:
14295:
14292:
14289:
14286:
14280:
14277:
14274:
14271:
14268:
14265:
14262:
14247:
14244:
14241:
14238:
14235:
14232:
14229:
14223:
14220:
14217:
14211:
14205:
14202:
14199:
14196:
14193:
14190:
14187:
14178:
14175:
14172:
14169:
14166:
14163:
14160:
14151:
14148:
14145:
14142:
14139:
14136:
14133:
14127:
14121:
14118:
14115:
14112:
14109:
14106:
14103:
14091:
14088:
14085:
14082:
14079:
14076:
14073:
14064:
14061:
14058:
14055:
14052:
14049:
14046:
14037:
14034:
14031:
14028:
14022:
14020:
14015:
14009:
14004:
14000:
13992:
13989:
13986:
13983:
13980:
13977:
13974:
13971:
13968:
13965:
13962:
13953:
13950:
13947:
13944:
13938:
13935:
13932:
13929:
13926:
13923:
13920:
13917:
13911:
13902:
13899:
13896:
13893:
13890:
13887:
13884:
13878:
13875:
13872:
13869:
13866:
13863:
13860:
13854:
13851:
13848:
13845:
13842:
13839:
13836:
13827:
13821:
13815:
13812:
13809:
13806:
13803:
13800:
13797:
13794:
13791:
13788:
13782:
13780:
13775:
13769:
13764:
13760:
13752:
13749:
13743:
13740:
13737:
13734:
13731:
13728:
13725:
13719:
13713:
13710:
13707:
13704:
13701:
13698:
13695:
13683:
13680:
13677:
13674:
13671:
13668:
13665:
13653:
13650:
13647:
13644:
13641:
13638:
13635:
13629:
13623:
13620:
13617:
13614:
13611:
13608:
13605:
13593:
13590:
13587:
13584:
13581:
13578:
13575:
13563:
13557:
13551:
13548:
13545:
13542:
13539:
13536:
13533:
13527:
13525:
13520:
13517:
13514:
13511:
13508:
13501:
13498:
13495:
13492:
13489:
13483:
13480:
13477:
13474:
13471:
13468:
13465:
13459:
13456:
13453:
13450:
13447:
13444:
13441:
13438:
13432:
13429:
13420:
13414:
13408:
13405:
13402:
13399:
13396:
13393:
13390:
13384:
13382:
13377:
13374:
13371:
13368:
13365:
13354:
13353:
13352:
13331:
13325:
13319:
13316:
13313:
13310:
13307:
13304:
13301:
13298:
13295:
13292:
13289:
13287:
13282:
13275:
13266:
13260:
13257:
13248:
13245:
13242:
13239:
13236:
13233:
13230:
13227:
13225:
13220:
13213:
13210:
13207:
13204:
13201:
13198:
13195:
13192:
13186:
13183:
13180:
13177:
13174:
13171:
13168:
13156:
13153:
13150:
13147:
13144:
13141:
13138:
13129:
13126:
13123:
13120:
13117:
13115:
13108:
13104:
13096:
13090:
13084:
13081:
13078:
13075:
13072:
13069:
13066:
13063:
13060:
13057:
13054:
13052:
13045:
13041:
13033:
13027:
13021:
13018:
13015:
13012:
13009:
13006:
13003:
13000:
12998:
12993:
12986:
12980:
12974:
12971:
12968:
12965:
12962:
12959:
12956:
12953:
12951:
12946:
12935:
12934:
12933:
12931:
12927:
12923:
12918:
12916:
12913:evaluates to
12912:
12908:
12904:
12901:evaluates to
12900:
12896:
12893:evaluates to
12839:
12798:
12795:
12756:
12755:
12754:
12752:
12729:
12726:
12723:
12720:
12717:
12714:
12711:
12708:
12706:
12701:
12694:
12691:
12688:
12685:
12682:
12679:
12676:
12673:
12671:
12666:
12655:
12654:
12653:
12647:
12644:
12641:
12638:
12637:
12636:
12634:
12630:
12625:
12623:
12619:
12615:
12611:
12607:
12402:
12396:
12392:
12388:
12378:
12376:
12371:
12368:
12365:Rational and
12335:
12329:
12326:
12314:
12308:
12305:
12296:
12293:
12278:
12272:
12269:
12257:
12251:
12248:
12239:
12236:
12227:
12224:
12206:
12200:
12197:
12185:
12179:
12176:
12167:
12164:
12149:
12143:
12140:
12128:
12122:
12119:
12110:
12107:
12098:
12095:
12086:
12083:
12080:
12077:
12074:
12071:
12068:
12065:
12062:
12057:
12053:
12045:
12044:
12043:
12041:
12037:
12033:
12012:
12006:
12000:
11997:
11988:
11982:
11976:
11973:
11970:
11967:
11964:
11961:
11958:
11955:
11952:
11949:
11942:
11941:
11940:
11938:
11935:above). The
11934:
11906:
11900:
11897:
11885:
11879:
11876:
11867:
11864:
11849:
11843:
11840:
11828:
11822:
11819:
11810:
11807:
11798:
11795:
11777:
11771:
11768:
11756:
11750:
11747:
11738:
11735:
11720:
11714:
11711:
11699:
11693:
11690:
11681:
11678:
11669:
11666:
11657:
11654:
11651:
11648:
11645:
11642:
11639:
11636:
11633:
11628:
11624:
11616:
11615:
11614:
11592:
11588:
11584:
11579:
11575:
11571:
11566:
11562:
11558:
11553:
11549:
11545:
11540:
11536:
11532:
11527:
11523:
11519:
11514:
11510:
11506:
11501:
11497:
11490:
11482:
11478:
11474:
11469:
11465:
11461:
11456:
11452:
11448:
11443:
11439:
11432:
11424:
11420:
11416:
11411:
11407:
11403:
11398:
11394:
11390:
11385:
11381:
11374:
11366:
11362:
11358:
11353:
11349:
11342:
11334:
11330:
11326:
11321:
11317:
11310:
11302:
11298:
11294:
11289:
11285:
11278:
11270:
11266:
11262:
11257:
11253:
11246:
11243:
11240:
11237:
11230:
11229:
11228:
11197:
11191:
11188:
11176:
11170:
11167:
11158:
11155:
11140:
11134:
11131:
11119:
11113:
11110:
11101:
11098:
11089:
11086:
11077:
11074:
11071:
11068:
11065:
11062:
11059:
11056:
11053:
11048:
11044:
11036:
11035:
11034:
11012:
11008:
11004:
10999:
10995:
10991:
10986:
10982:
10978:
10973:
10969:
10962:
10954:
10950:
10946:
10941:
10937:
10930:
10922:
10918:
10914:
10909:
10905:
10898:
10893:
10889:
10885:
10880:
10876:
10872:
10867:
10863:
10859:
10854:
10850:
10846:
10838:
10834:
10830:
10825:
10821:
10814:
10806:
10802:
10798:
10793:
10789:
10782:
10779:
10776:
10773:
10766:
10765:
10764:
10738:
10732:
10729:
10717:
10711:
10708:
10699:
10696:
10681:
10675:
10672:
10660:
10654:
10651:
10642:
10639:
10630:
10627:
10618:
10615:
10612:
10609:
10606:
10603:
10600:
10597:
10594:
10589:
10585:
10577:
10576:
10575:
10553:
10549:
10545:
10540:
10536:
10532:
10527:
10523:
10519:
10514:
10510:
10503:
10495:
10491:
10487:
10482:
10478:
10471:
10463:
10459:
10455:
10450:
10446:
10439:
10434:
10430:
10426:
10421:
10417:
10413:
10408:
10404:
10400:
10395:
10391:
10387:
10379:
10375:
10371:
10366:
10362:
10355:
10347:
10343:
10339:
10334:
10330:
10323:
10320:
10317:
10314:
10307:
10306:
10305:
10283:
10280:
10277:
10274:
10267:
10266:
10239:
10233:
10230:
10221:
10218:
10203:
10197:
10194:
10185:
10182:
10173:
10170:
10164:
10155:
10146:
10140:
10137:
10128:
10125:
10116:
10107:
10101:
10098:
10089:
10086:
10083:
10080:
10077:
10074:
10071:
10068:
10065:
10062:
10055:
10054:
10053:
10024:
10018:
10015:
10006:
10003:
9988:
9982:
9979:
9970:
9967:
9958:
9955:
9949:
9946:
9937:
9928:
9922:
9919:
9910:
9907:
9898:
9889:
9883:
9880:
9871:
9868:
9865:
9862:
9859:
9856:
9853:
9846:
9845:
9844:
9842:
9820:
9814:
9811:
9799:
9793:
9790:
9781:
9778:
9775:
9772:
9769:
9766:
9761:
9757:
9749:
9748:
9747:
9730:
9724:
9718:
9715:
9712:
9709:
9706:
9703:
9698:
9694:
9686:
9685:
9684:
9681:
9679:
9666:
9660:
9653:
9628:
9616:
9610:
9604:
9595:
9592:
9589:
9586:
9583:
9580:
9577:
9574:
9571:
9568:
9547:
9541:
9532:
9523:
9520:
9517:
9514:
9502:
9499:
9496:
9493:
9478:
9472:
9463:
9460:
9457:
9454:
9451:
9448:
9445:
9436:
9433:
9430:
9427:
9424:
9421:
9418:
9415:
9412:
9409:
9403:
9400:
9397:
9394:
9391:
9388:
9385:
9364:
9358:
9352:
9346:
9340:
9331:
9319:
9313:
9304:
9301:
9298:
9295:
9292:
9289:
9286:
9274:
9262:
9259:
9256:
9253:
9250:
9247:
9244:
9229:
9226:
9223:
9220:
9217:
9214:
9211:
9205:
9202:
9199:
9190:
9187:
9184:
9181:
9175:
9172:
9169:
9163:
9160:
9157:
9154:
9151:
9148:
9145:
9142:
9139:
9136:
9133:
9130:
9127:
9124:
9121:
9103:
9097:
9088:
9085:
9082:
9079:
9067:
9061:
9058:
9055:
9052:
9046:
9043:
9040:
9031:
9028:
9025:
9022:
9019:
9011:
9010:
9009:
8985:
8982:
8979:
8976:
8964:
8961:
8958:
8955:
8940:
8934:
8925:
8922:
8919:
8916:
8913:
8910:
8907:
8898:
8895:
8892:
8889:
8886:
8883:
8880:
8877:
8874:
8871:
8868:
8866:
8861:
8854:
8851:
8848:
8845:
8842:
8839:
8836:
8833:
8830:
8827:
8824:
8822:
8817:
8806:
8786:
8783:
8780:
8777:
8774:
8771:
8768:
8765:
8763:
8758:
8751:
8748:
8745:
8742:
8739:
8736:
8733:
8730:
8728:
8723:
8712:
8711:
8694:
8685:
8682:
8679:
8676:
8667:
8664:
8661:
8658:
8655:
8653:
8648:
8641:
8638:
8635:
8632:
8629:
8626:
8623:
8620:
8618:
8613:
8600:
8594:
8585:
8582:
8579:
8576:
8561:
8555:
8546:
8543:
8540:
8537:
8531:
8528:
8525:
8522:
8520:
8515:
8505:
8499:
8493:
8484:
8481:
8478:
8475:
8472:
8469:
8466:
8463:
8460:
8457:
8454:
8452:
8447:
8440:
8434:
8431:
8429:
8424:
8413:
8412:
8411:
8391:
8385:
8382:
8373:
8370:
8367:
8364:
8361:
8358:
8355:
8348:
8347:
8346:
8326:
8320:
8314:
8311:
8293:
8287:
8281:
8275:
8269:
8260:
8248:
8242:
8236:
8227:
8221:
8218:
8215:
8212:
8209:
8203:
8200:
8197:
8194:
8191:
8188:
8185:
8182:
8179:
8176:
8173:
8170:
8167:
8164:
8161:
8158:
8155:
8148:
8147:
8146:
8129:
8123:
8115:
8101:
8095:
8092:
8086:
8078:
8077:
8076:
8074:
8070:
8066:
8045:
8039:
8036:
8027:
8024:
8021:
8018:
8012:
8009:
8002:
8001:
8000:
7998:
7994:
7990:
7985:
7971:
7967:
7960:
7957:
7954:
7931:
7925:
7919:
7916:
7890:
7884:
7878:
7875:
7857:
7851:
7845:
7839:
7833:
7830:
7821:
7809:
7803:
7797:
7788:
7782:
7779:
7776:
7773:
7770:
7764:
7761:
7755:
7749:
7743:
7737:
7734:
7727:
7726:
7725:
7711:
7708:
7705:
7685:
7682:
7679:
7653:
7647:
7641:
7638:
7629:
7626:
7619:
7618:
7617:
7615:
7598:
7595:
7592:
7569:
7563:
7560:
7554:
7550:
7543:
7540:
7537:
7531:
7528:
7522:
7519:
7513:
7510:
7507:
7501:
7498:
7495:
7492:
7488:
7484:
7477:
7476:
7475:
7473:
7446:
7438:
7428:
7422:
7419:
7413:
7410:
7401:
7398:
7390:
7377:
7371:
7368:
7362:
7359:
7350:
7338:
7335:
7327:
7311:
7305:
7302:
7296:
7293:
7284:
7272:
7260:
7257:
7249:
7230:
7224:
7221:
7215:
7212:
7203:
7191:
7179:
7167:
7164:
7156:
7153:
7150:
7147:
7136:
7135:
7134:
7120:
7117:
7114:
7084:
7078:
7069:
7060:
7057:
7051:
7048:
7045:
7037:
7034:
7027:
7021:
7018:
7012:
7009:
7001:
6998:
6988:
6982:
6979:
6976:
6973:
6970:
6967:
6956:
6953:
6940:
6934:
6931:
6922:
6919:
6907:
6901:
6898:
6889:
6886:
6880:
6877:
6874:
6866:
6852:
6851:
6850:
6824:
6821:
6818:
6815:
6812:
6809:
6802:
6801:
6800:
6783:
6780:
6777:
6771:
6768:
6761:
6760:
6759:
6742:
6736:
6733:
6730:
6727:
6724:
6718:
6712:
6709:
6700:
6697:
6694:
6691:
6684:
6670:
6664:
6661:
6658:
6655:
6649:
6646:
6639:
6638:
6637:
6616:To implement
6595:
6589:
6586:
6583:
6577:
6574:
6567:
6566:
6565:
6548:
6545:
6542:
6536:
6530:
6527:
6520:
6519:
6518:
6497:
6494:
6491:
6488:
6485:
6482:
6475:
6474:
6473:
6446:
6440:
6431:
6428:
6425:
6422:
6419:
6416:
6413:
6410:
6407:
6400:
6383:
6377:
6368:
6365:
6362:
6359:
6353:
6350:
6343:
6342:
6341:
6324:
6318:
6315:
6312:
6306:
6300:
6297:
6294:
6291:
6285:
6278:
6277:
6276:
6259:
6253:
6250:
6247:
6244:
6237:
6236:
6235:
6215:
6209:
6200:
6197:
6194:
6188:
6182:
6179:
6170:
6167:
6160:
6159:
6158:
6121:
6115:
6112:
6109:
6106:
6100:
6097:
6094:
6091:
6088:
6081:
6080:
6079:
6062:
6056:
6053:
6050:
6044:
6038:
6035:
6028:
6027:
6026:
6017:
5997:
5994:
5991:
5988:
5976:
5973:
5970:
5967:
5952:
5946:
5937:
5934:
5931:
5928:
5925:
5922:
5919:
5910:
5907:
5904:
5901:
5898:
5895:
5892:
5889:
5886:
5883:
5880:
5877:
5870:
5869:
5868:
5843:
5840:
5837:
5834:
5831:
5829:
5824:
5817:
5811:
5808:
5805:
5802:
5799:
5797:
5792:
5782:
5776:
5767:
5764:
5761:
5758:
5755:
5752:
5749:
5746:
5744:
5739:
5732:
5729:
5726:
5723:
5717:
5714:
5712:
5707:
5704:
5701:
5691:
5685:
5682:
5679:
5676:
5670:
5667:
5664:
5661:
5659:
5654:
5643:
5642:
5641:
5601:
5598:
5595:
5589:
5586:
5583:
5580:
5577:
5571:
5562:
5559:
5556:
5550:
5547:
5544:
5541:
5538:
5535:
5532:
5529:
5526:
5523:
5514:
5508:
5499:
5496:
5493:
5481:
5478:
5469:
5466:
5463:
5460:
5457:
5454:
5451:
5448:
5445:
5442:
5439:
5436:
5430:
5427:
5424:
5421:
5412:
5409:
5406:
5403:
5400:
5397:
5394:
5391:
5388:
5385:
5382:
5379:
5376:
5369:
5368:
5367:
5304:
5301:
5298:
5295:
5292:
5289:
5283:
5277:
5274:
5271:
5268:
5265:
5262:
5259:
5256:
5253:
5250:
5247:
5238:
5232:
5226:
5217:
5214:
5205:
5202:
5199:
5196:
5193:
5190:
5187:
5184:
5181:
5178:
5175:
5172:
5166:
5163:
5160:
5157:
5148:
5145:
5142:
5139:
5136:
5133:
5130:
5127:
5124:
5121:
5118:
5115:
5112:
5105:
5104:
5103:
5102:function as,
5078:
5075:
5069:
5063:
5060:
5051:
5048:
5041:
5040:
5039:
5015:
5009:
5000:
4997:
4994:
4988:
4982:
4979:
4970:
4967:
4960:
4959:
4958:
4934:
4928:
4919:
4916:
4913:
4901:
4898:
4895:
4889:
4881:
4878:
4875:
4871:
4861:
4858:
4855:
4852:
4846:
4843:
4840:
4832:
4826:
4820:
4811:
4808:
4805:
4799:
4791:
4787:
4777:
4774:
4771:
4768:
4762:
4759:
4756:
4751:
4744:
4739:
4734:
4721:
4715:
4706:
4697:
4694:
4691:
4682:
4676:
4673:
4664:
4661:
4652:
4649:
4635:
4629:
4620:
4611:
4602:
4599:
4596:
4587:
4581:
4578:
4569:
4566:
4557:
4554:
4549:
4539:
4533:
4524:
4521:
4518:
4512:
4506:
4503:
4494:
4491:
4480:
4474:
4465:
4456:
4453:
4450:
4444:
4438:
4435:
4426:
4423:
4418:
4411:
4405:
4402:
4399:
4396:
4390:
4387:
4379:
4373:
4364:
4361:
4358:
4355:
4349:
4346:
4341:
4333:
4327:
4324:
4321:
4318:
4313:
4279:
4278:
4277:
4242:
4238:
4182:
4179:
4176:
4169:
4166:
4163:
4160:
4148:
4142:
4137:
4131:
4125:
4122:
4115:
4114:
4113:
4086:
4083:
4080:
4077:
4074:
4068:
4065:
4062:
4055:
4041:
4038:
4032:
4026:
4023:
4016:
4015:
4011:
4009:
3989:
3983:
3980:
3977:
3971:
3957:
3953:
3950:
3948:
3928:
3925:
3922:
3919:
3916:
3913:
3910:
3907:
3904:
3901:
3894:
3891:
3877:
3868:
3865:
3859:
3856:
3850:
3844:
3841:
3834:
3817:
3812:
3808:
3799:
3789:
3786:
3782:
3775:
3772:
3764:
3761:
3758:
3754:
3746:
3732:
3729:
3726:
3719:
3716:
3712:
3709:
3708:
3705:
3689:
3686:
3683:
3680:
3668:
3665:
3662:
3659:
3644:
3638:
3629:
3626:
3623:
3620:
3617:
3614:
3611:
3602:
3599:
3596:
3593:
3590:
3587:
3584:
3581:
3578:
3575:
3550:
3547:
3544:
3535:
3532:
3526:
3517:
3514:
3511:
3505:
3502:
3495:
3478:
3473:
3470:
3467:
3463:
3456:
3453:
3450:
3447:
3444:
3439:
3435:
3427:
3413:
3410:
3407:
3400:
3398:
3395:
3394:
3379:
3373:
3370:
3367:
3364:
3361:
3358:
3355:
3348:
3334:
3328:
3319:
3313:
3307:
3304:
3301:
3298:
3295:
3292:
3289:
3286:
3283:
3280:
3277:
3274:
3267:
3253:
3247:
3238:
3232:
3226:
3223:
3217:
3211:
3205:
3199:
3196:
3189:
3175:
3167:
3163:
3159:
3156:
3150:
3144:
3137:
3121:
3117:
3109:
3107:
3104:
3103:
3085:
3079:
3070:
3067:
3064:
3061:
3058:
3055:
3052:
3049:
3046:
3043:
3036:
3022:
3013:
3007:
2998:
2995:
2992:
2989:
2986:
2983:
2980:
2977:
2974:
2971:
2968:
2965:
2962:
2955:
2941:
2932:
2926:
2917:
2914:
2911:
2905:
2899:
2893:
2887:
2884:
2877:
2863:
2855:
2845:
2841:
2834:
2831:
2823:
2820:
2817:
2813:
2805:
2791:
2788:
2785:
2778:
2776:
2773:
2772:
2757:
2754:
2751:
2748:
2745:
2742:
2739:
2736:
2733:
2730:
2723:
2706:
2700:
2694:
2685:
2679:
2676:
2673:
2670:
2667:
2664:
2661:
2658:
2655:
2652:
2649:
2646:
2643:
2636:
2619:
2613:
2607:
2598:
2592:
2589:
2586:
2580:
2574:
2568:
2562:
2559:
2552:
2535:
2530:
2526:
2517:
2513:
2509:
2506:
2498:
2495:
2492:
2488:
2480:
2466:
2463:
2460:
2453:
2451:
2448:
2447:
2443:
2426:
2420:
2414:
2405:
2402:
2399:
2396:
2393:
2390:
2387:
2384:
2381:
2378:
2371:
2354:
2348:
2342:
2333:
2330:
2327:
2321:
2315:
2309:
2306:
2299:
2282:
2277:
2273:
2266:
2263:
2260:
2252:
2249:
2246:
2242:
2234:
2220:
2217:
2214:
2207:
2205:
2202:
2201:
2194:
2191:
2188:
2185:
2184:
2162:
2153:
2150:
2144:
2141:
2138:
2135:
2132:
2129:
2126:
2123:
2116:
2115:
2114:
2111:
2109:
2105:
2101:
2097:
2093:
2071:
2068:
2065:
2062:
2050:
2047:
2044:
2041:
2026:
2020:
2011:
2008:
2005:
2002:
1999:
1996:
1993:
1984:
1981:
1978:
1975:
1972:
1969:
1966:
1963:
1960:
1957:
1954:
1951:
1944:
1943:
1942:
1925:
1919:
1916:
1893:
1887:
1884:
1881:
1878:
1875:
1872:
1869:
1866:
1863:
1856:
1855:
1854:
1837:
1831:
1828:
1823:
1819:
1815:
1812:
1806:
1800:
1797:
1790:
1789:
1788:
1774:
1766:
1762:
1758:
1755:
1749:
1743:
1723:
1717:
1714:
1711:
1705:
1685:
1677:
1673:
1669:
1666:
1660:
1654:
1632:
1628:
1624:
1618:
1615:
1612:
1606:
1603:
1580:
1571:
1565:
1556:
1553:
1550:
1547:
1544:
1541:
1538:
1535:
1532:
1529:
1526:
1523:
1520:
1517:
1514:
1507:
1506:
1505:
1488:
1480:
1477:
1467:
1464:
1460:
1453:
1447:
1436:
1433:
1430:
1424:
1420:
1399:
1396:
1393:
1390:
1384:
1381:
1378:
1372:
1369:
1343:
1337:
1331:
1322:
1319:
1316:
1313:
1310:
1307:
1304:
1301:
1298:
1295:
1292:
1289:
1282:
1281:
1280:
1263:
1257:
1254:
1243:
1227:
1224:
1221:
1218:
1212:
1206:
1203:
1177:
1171:
1165:
1156:
1150:
1147:
1144:
1141:
1138:
1135:
1132:
1129:
1126:
1123:
1120:
1117:
1114:
1111:
1108:
1101:
1100:
1099:
1079:
1071:
1068:
1064:
1055:
1052:
1048:
1044:
1038:
1027:
1024:
1021:
1015:
1011:
990:
987:
984:
981:
975:
972:
969:
963:
960:
951:
949:
945:
941:
932:
930:
926:
922:
918:
913:
890:
882:
879:
875:
871:
868:
865:
862:
859:
856:
853:
850:
845:
837:
833:
829:
826:
820:
814:
809:
802:
797:
792:
779:
773:
764:
755:
752:
749:
746:
743:
740:
737:
734:
731:
720:
714:
705:
696:
693:
690:
684:
678:
673:
663:
657:
648:
645:
642:
639:
636:
633:
630:
627:
624:
616:
610:
601:
598:
595:
589:
583:
578:
571:
565:
562:
559:
556:
553:
550:
547:
544:
541:
536:
530:
527:
524:
518:
512:
507:
500:
497:
494:
491:
488:
485:
482:
479:
476:
471:
468:
465:
459:
453:
448:
414:
413:
412:
410:
407:
403:
402:
397:
394:
391:
388:
387:Starting with
384:
382:
378:
374:
370:
350:
340:
334:
330:
327:
324:
321:
318:
315:
312:
305:
300:
297:
293:
285:
284:
283:
281:
277:
261:
253:
249:
245:
235:
233:
230:. There are
229:
225:
221:
217:
216:extensionally
211:
209:
205:
201:
185:
162:
156:
133:
127:
113:
111:
107:
103:
98:
96:
95:Alonzo Church
92:
88:
84:
80:
69:
59:
53:
51:
46:
41:
37:
32:
31:
19:
19575:Institutions
19491:Martin Davis
19437:
19359:
19179:
19157:Ultraproduct
19004:Model theory
18969:Independence
18905:Formal proof
18897:Proof theory
18880:
18853:
18810:real numbers
18782:second-order
18693:Substitution
18570:Metalanguage
18511:conservative
18484:Axiom schema
18428:Constructive
18398:Morse–Kelley
18364:Set theories
18343:Aleph number
18336:inaccessible
18242:Grothendieck
18126:intersection
18013:Higher-order
18001:Second-order
17947:Truth tables
17904:Venn diagram
17687:Formal proof
17591:
17574:
17532:
17528:
17500:
17494:
17483:. Retrieved
17457:
17447:
17422:
17413:
17402:
17392:
17379:
17370:
17355:
17340:
17334:. okmij.org.
17331:
17322:
17293:
17287:
17259:
17194:
17135:
17014:
16923:is given by
16914:
16845:
16781:
16680:
16669:
16657:
16226:
16221:
16015:
15855:
15845:
15841:
15837:
15833:
15831:
15823:
15759:second.first
15758:
15693:
15689:
15570:
15519:Description
15509:
15503:
15498:Second.First
15497:
15491:
15486:
15480:
15474:
15469:
15443:
15433:
15423:
15413:
15403:
15393:
15388:Description
15370:
14953:
14750:
14741:Church pairs
14632:
14570:
14489:
14339:
14337:
13350:
12929:
12925:
12921:
12919:
12914:
12910:
12906:
12902:
12898:
12894:
12892:
12748:
12651:
12645:
12639:
12632:
12628:
12626:
12613:
12609:
12605:
12604:
12397:, where the
12390:
12386:
12384:
12372:
12364:
12039:
12038:replaced by
12035:
12031:
12030:
11936:
11932:
11930:
11612:
11226:
11032:
10762:
10573:
10303:
10051:
9840:
9838:
9745:
9682:
9675:
9664:
9658:
9647:
9007:
8409:
8344:
8144:
8072:
8069:Y combinator
8064:
8063:
7996:
7992:
7988:
7986:
7908:
7671:
7613:
7585:Calculating
7584:
7470:
7106:
6848:
6798:
6757:
6636:to satisfy,
6615:
6563:
6512:
6471:
6339:
6274:
6233:
6144:
6077:
6024:
5862:
5619:
5319:
5093:
5033:
4956:
4243:
4236:
4214:
4111:
3956:
3946:
3945:
3568:
2112:
2103:
2099:
2095:
2091:
2089:
1908:
1852:
1595:
1361:
1242:β-equivalent
1195:
952:
938:
924:
920:
911:
909:
408:
405:
400:
398:
395:
392:
389:
386:
385:
376:
372:
368:
366:
275:
251:
241:
212:
119:
99:
90:
82:
76:
63:
47:
45:lead section
19608:A. C. Croom
19531:Gary R. Mar
19506:Leon Henkin
19466:Alan Turing
19267:Type theory
19215:undecidable
19147:Truth value
19034:equivalence
18713:non-logical
18326:Enumeration
18316:Isomorphism
18263:cardinality
18247:Von Neumann
18212:Ultrafilter
18177:Uncountable
18111:equivalence
18028:Quantifiers
18018:Fixed-point
17987:First-order
17867:Consistency
17852:Proposition
17829:Traditional
17800:Lindström's
17790:Compactness
17732:Type theory
17677:Cardinality
15692:and a tail
12911:predicate-x
12907:else-clause
12899:predicate-x
12895:then-clause
6632:. We need
4306:Using const
4268:applied to
3711:Subtraction
3397:Predecessor
2108:predecessor
345: times
280:composition
79:mathematics
19556:Dana Scott
19078:elementary
18771:arithmetic
18639:Quantifier
18617:functional
18489:Expression
18207:Transitive
18151:identities
18136:complement
18069:hereditary
18052:Set theory
17485:2017-11-24
17240:References
16699:Cons(h, t)
16222:right fold
15516:Expression
14745:See also:
14334:Predicates
4299:Using init
940:Arithmetic
19349:Supertask
19252:Recursion
19210:decidable
19044:saturated
19022:of models
18945:deductive
18940:axiomatic
18860:Hilbert's
18847:Euclidean
18828:canonical
18751:axiomatic
18683:Signature
18612:Predicate
18501:Extension
18423:Ackermann
18348:Operation
18227:Universal
18217:Recursive
18192:Singleton
18187:Inhabited
18172:Countable
18162:Types of
18146:power set
18116:partition
18033:Predicate
17979:Predicate
17894:Syllogism
17884:Soundness
17857:Inference
17847:Tautology
17749:paradoxes
17596:CiteSeerX
17537:CiteSeerX
17429:MIT Press
17298:CiteSeerX
16976:λ
16967:λ
16958:≡
16937:
16919:and tail
16888:λ
16879:λ
16876:≡
16825:
16816:
16627:λ
16618:λ
16597:λ
16552:λ
16543:λ
16534:λ
16516:λ
16507:λ
16498:λ
16495:≡
16463:λ
16454:λ
16436:λ
16433:≡
16380:λ
16371:λ
16362:λ
16353:λ
16350:≡
16318:λ
16309:λ
16291:λ
16288:≡
16265:λ
16256:λ
16253:≡
16101:λ
16092:λ
16083:λ
16068:λ
16065:≡
15982:λ
15973:λ
15964:λ
15949:λ
15946:≡
15929:≡
15912:≡
15895:≡
15878:≡
15803:
15791:
15779:λ
15776:≡
15738:
15726:
15714:λ
15711:≡
15662:
15650:
15644:
15632:λ
15623:λ
15620:≡
15588:≡
15549:
15540:
15534:≡
15373:immutable
15317:λ
15308:λ
15279:λ
15270:λ
15237:λ
15196:λ
15172:λ
15163:λ
15145:λ
15089:λ
15080:λ
15071:λ
15044:λ
15035:λ
15017:λ
14985:
14973:
14923:λ
14914:λ
14896:λ
14893:≡
14867:λ
14858:λ
14840:λ
14837:≡
14802:λ
14793:λ
14784:λ
14781:≡
14710:
14683:
14671:
14659:λ
14650:λ
14612:≤
14606:∧
14600:≤
14591:≡
14540:
14528:
14516:λ
14507:λ
14457:λ
14439:λ
14340:predicate
14299:λ
14290:λ
14272:λ
14263:λ
14239:λ
14230:λ
14218:λ
14197:λ
14188:λ
14170:λ
14161:λ
14143:λ
14134:λ
14113:λ
14104:λ
14083:λ
14074:λ
14056:λ
14047:λ
14029:λ
14010:
13978:λ
13969:λ
13945:λ
13933:λ
13924:λ
13894:λ
13885:λ
13873:λ
13864:λ
13846:λ
13837:λ
13807:λ
13798:λ
13789:λ
13770:
13735:λ
13726:λ
13705:λ
13696:λ
13675:λ
13666:λ
13645:λ
13636:λ
13615:λ
13606:λ
13585:λ
13576:λ
13543:λ
13534:λ
13518:
13512:
13493:
13475:λ
13466:λ
13454:
13448:
13433:
13400:λ
13391:λ
13375:
13369:
13311:λ
13302:λ
13293:λ
13261:
13240:λ
13231:λ
13211:
13196:λ
13178:λ
13169:λ
13148:λ
13139:λ
13121:λ
13076:λ
13067:λ
13058:λ
13013:λ
13004:λ
12966:λ
12957:λ
12905:, and to
12840:
12796:
12721:λ
12712:λ
12709:≡
12686:λ
12677:λ
12674:≡
12618:Smalltalk
12330:
12309:
12297:
12273:
12252:
12240:
12228:
12201:
12180:
12168:
12144:
12123:
12111:
12099:
12087:
12075:λ
12066:λ
12001:
11977:
11965:λ
11956:λ
11901:
11880:
11868:
11844:
11823:
11811:
11799:
11772:
11751:
11739:
11715:
11694:
11682:
11670:
11658:
11646:λ
11637:λ
11585:∗
11559:∗
11533:∗
11507:∗
11475:∗
11449:∗
11433:−
11417:∗
11391:∗
11359:−
11343:∗
11327:−
11279:∗
11241:∗
11192:
11171:
11159:
11135:
11114:
11102:
11090:
11078:
11066:λ
11057:λ
10931:−
10873:−
10860:−
10815:−
10777:−
10733:
10712:
10700:
10676:
10655:
10643:
10631:
10619:
10607:λ
10598:λ
10472:−
10427:−
10401:−
10234:
10222:
10198:
10186:
10174:
10141:
10129:
10102:
10090:
10078:λ
10069:λ
10019:
10007:
9983:
9971:
9959:
9950:
9923:
9911:
9884:
9872:
9860:λ
9815:
9794:
9782:
9770:λ
9719:
9707:λ
9587:λ
9578:λ
9569:λ
9515:λ
9494:λ
9455:λ
9446:λ
9428:λ
9419:λ
9410:λ
9395:λ
9386:λ
9296:λ
9287:λ
9254:λ
9245:λ
9221:λ
9212:λ
9200:λ
9182:λ
9170:λ
9158:λ
9149:λ
9140:λ
9131:λ
9122:λ
9080:λ
9053:λ
9041:λ
9026:λ
8977:λ
8956:λ
8917:λ
8908:λ
8890:λ
8881:λ
8872:λ
8852:
8837:λ
8828:λ
8778:λ
8769:λ
8766:≡
8743:λ
8734:λ
8731:≡
8677:λ
8659:λ
8633:λ
8624:λ
8577:λ
8538:λ
8526:λ
8476:λ
8467:λ
8458:λ
8386:
8374:
8362:λ
8315:
8222:
8210:λ
8198:λ
8189:λ
8180:λ
8171:λ
8162:λ
8127:→
8096:
8090:→
8040:
8028:
8013:
7999:is then,
7958:−
7920:
7879:
7834:
7783:
7771:λ
7738:
7683:≤
7642:
7630:
7596:−
7564:
7541:−
7523:
7511:≥
7502:
7423:
7414:
7402:
7372:
7363:
7351:
7339:
7306:
7297:
7285:
7273:
7261:
7225:
7216:
7204:
7192:
7180:
7168:
7151:
7118:
7079:
7061:
7046:λ
7022:
7013:
6977:λ
6968:λ
6935:
6923:
6902:
6890:
6875:λ
6816:λ
6772:
6728:λ
6713:
6692:λ
6665:
6650:
6578:
6531:
6489:λ
6423:λ
6414:λ
6369:
6354:
6301:
6254:
6201:
6183:
6171:
6107:λ
6095:λ
6039:
5989:λ
5968:λ
5929:λ
5920:λ
5902:λ
5893:λ
5884:λ
5835:λ
5803:λ
5759:λ
5750:λ
5724:λ
5705:
5677:λ
5665:λ
5599:−
5584:λ
5560:−
5545:λ
5536:λ
5527:λ
5497:−
5482:
5470:
5458:λ
5449:λ
5440:λ
5428:
5413:
5401:λ
5392:λ
5383:λ
5296:λ
5269:λ
5260:λ
5251:λ
5218:
5206:
5194:λ
5185:λ
5176:λ
5164:
5149:
5137:λ
5128:λ
5119:λ
5064:
5052:
5001:
4983:
4971:
4917:−
4902:
4879:−
4862:
4847:
4812:
4778:
4763:
4745:⋮
4740:⋮
4735:⋮
4698:
4677:
4665:
4653:
4603:
4582:
4570:
4558:
4525:
4507:
4495:
4457:
4439:
4427:
4406:
4391:
4365:
4350:
4328:
4252:, called
4226:times to
4190:otherwise
4180:−
4126:
4078:−
4072:→
4066:≤
4027:
3987:→
3975:→
3926:
3911:λ
3902:λ
3845:
3787:−
3762:−
3730:−
3681:λ
3660:λ
3621:λ
3612:λ
3594:λ
3585:λ
3576:λ
3548:−
3536:
3506:
3471:−
3457:
3445:
3411:−
3365:λ
3356:λ
3302:λ
3293:λ
3284:λ
3275:λ
3200:
3062:λ
3053:λ
3044:λ
2990:λ
2981:λ
2972:λ
2963:λ
2888:
2821:∗
2789:∗
2755:
2740:λ
2731:λ
2671:λ
2662:λ
2653:λ
2644:λ
2563:
2397:λ
2388:λ
2379:λ
2310:
2204:Successor
2139:λ
2130:λ
2127:≡
2063:λ
2042:λ
2003:λ
1994:λ
1976:λ
1967:λ
1958:λ
1955:≡
1920:
1879:λ
1870:λ
1867:≡
1801:
1721:→
1709:→
1607:
1548:λ
1539:λ
1530:λ
1521:λ
1518:≡
1478:∘
1465:∘
1434:∗
1425:∘
1397:∗
1373:
1314:λ
1305:λ
1296:λ
1293:≡
1258:
1207:
1142:λ
1133:λ
1124:λ
1115:λ
1112:≡
1069:∘
1053:∘
1016:∘
964:
929:ostensive
880:∘
866:λ
857:λ
803:⋮
798:⋮
793:⋮
747:λ
738:λ
640:λ
631:λ
557:λ
548:λ
492:λ
483:λ
335:⏟
328:∘
325:⋯
322:∘
316:∘
298:∘
66:July 2023
50:summarize
19623:Category
19459:Students
19334:Logicism
19327:timeline
19303:Concrete
19162:Validity
19132:T-schema
19125:Kripke's
19120:Tarski's
19115:semantic
19105:Strength
19054:submodel
19049:spectrum
19017:function
18865:Tarski's
18854:Elements
18841:geometry
18797:Robinson
18718:variable
18703:function
18676:spectrum
18666:Sentence
18622:variable
18565:Language
18518:Relation
18479:Automata
18469:Alphabet
18453:language
18307:-jection
18285:codomain
18271:Function
18232:Universe
18202:Infinite
18106:Relation
17889:Validity
17879:Argument
17777:theorem,
17559:16124152
17473:As PDF:
17421:(2002).
17384:Archived
17222:System F
17211:See also
16860:consCode
16831:consCode
16800:consCode
16792:consCode
16759:consCode
16660:System F
15385:Function
12920:Because
12571:unchurch
12553:unchurch
12391:unchurch
11033:giving,
8145:to get,
7472:Division
7467:Division
4156:if
2885:multiply
2450:Addition
2192:Identity
2186:Function
178:, where
19276:Related
19073:Diagram
18971: (
18950:Hilbert
18935:Systems
18930:Theorem
18808:of the
18753:systems
18533:Formula
18528:Grammar
18444: (
18388:General
18101:Forcing
18086:Element
18006:Monadic
17781:paradox
17722:Theorem
17658:General
17380:Haskell
16854:and by
16852:nilCode
16822:nilCode
16796:nilCode
16788:nilCode
16732:nilCode
16703:nilCode
12568:Integer
12562:Integer
12460:Integer
12451:Integer
12395:Haskell
11933:OneZero
11075:OneZero
10616:OneZero
10275:OneZero
9947:OneZero
9854:OneZero
9841:OneZero
9695:convert
9008:Gives,
8425:divide1
8410:where,
8371:divide1
8124:divide1
8087:divide1
8065:divide1
8025:divide1
7831:divide1
7735:divide1
6575:extract
6468:Extract
5702:extract
5638:extract
5467:extract
5410:extract
5322:samenum
5203:extract
5146:extract
5113:samenum
5100:samenum
5096:extract
5049:extract
5036:extract
4241:times.
2189:Algebra
1736:to get
274:to its
19596:Family
19039:finite
18802:Skolem
18755:
18730:Theory
18698:Symbol
18688:String
18671:atomic
18548:ground
18543:closed
18538:atomic
18494:ground
18457:syntax
18353:binary
18280:domain
18197:Finite
17962:finite
17820:Logics
17779:
17727:Theory
17598:
17557:
17539:
17464:
17435:
17404:GitHub
17310:
17300:
17275:
16997:
16991:
16985:
16964:
16961:
16955:
16952:
16946:
16940:
16897:
16828:
16819:
16612:
16591:
16579:
16570:
16564:
16528:
16478:
16448:
16413:
16407:
16398:
16392:
16333:
16303:
15915:second
15838:second
15800:second
15794:
15788:second
15735:second
15729:
15668:
15653:
15552:
15543:
15481:Second
15338:
15332:
15264:
15255:
15249:
15214:
15208:
15190:
15157:
15122:
15116:
15107:
15101:
15062:
15029:
14994:
14988:
14976:
14908:
14886:second
14852:
14820:
14814:
14719:
14713:
14701:
14692:
14686:
14674:
14549:
14543:
14531:
14525:IsZero
14472:
14451:
14433:IsZero
14402:, and
14350:IsZero
14257:
14041:
14013:
13960:
13915:
13909:
13825:
13819:
13773:
13690:
13660:
13600:
13570:
13561:
13555:
13436:
13427:
13418:
13412:
13329:
13323:
13273:
13264:
13252:
13163:
13133:
13094:
13088:
13031:
13025:
12984:
12978:
12843:
12802:
12614:false.
12559:Church
12526:church
12493:church
12463:church
12457:Church
12445:church
12409:Church
12387:church
12333:
12321:
12312:
12306:second
12300:
12288:
12276:
12270:second
12264:
12255:
12243:
12231:
12219:
12204:
12198:second
12192:
12183:
12177:second
12171:
12159:
12147:
12135:
12126:
12114:
12102:
12090:
12054:divide
12010:
12004:
11998:divide
11992:
11986:
11980:
11974:IsZero
11904:
11892:
11883:
11877:second
11871:
11859:
11847:
11841:second
11835:
11826:
11814:
11802:
11790:
11775:
11769:second
11763:
11754:
11748:second
11742:
11730:
11718:
11706:
11697:
11685:
11673:
11661:
11195:
11183:
11174:
11168:second
11162:
11150:
11138:
11132:second
11126:
11117:
11105:
11093:
11081:
10736:
10730:second
10724:
10715:
10709:second
10703:
10691:
10679:
10667:
10658:
10646:
10634:
10622:
10237:
10231:second
10225:
10213:
10201:
10189:
10177:
10168:
10159:
10153:
10144:
10138:second
10132:
10126:IsZero
10120:
10114:
10105:
10093:
10087:IsZero
10022:
10016:second
10010:
9998:
9986:
9974:
9962:
9953:
9941:
9935:
9926:
9920:second
9914:
9908:IsZero
9902:
9896:
9887:
9875:
9869:IsZero
9818:
9806:
9797:
9791:second
9785:
9728:
9722:
9650:λ
9626:
9614:
9608:
9599:
9560:
9545:
9539:
9509:
9488:
9476:
9467:
9440:
9377:
9362:
9356:
9350:
9344:
9335:
9326:
9317:
9311:
9278:
9272:
9239:
9194:
9116:
9101:
9092:
9074:
9065:
9020:divide
8971:
8950:
8938:
8929:
8902:
8692:
8671:
8649:IsZero
8598:
8589:
8571:
8559:
8550:
8503:
8497:
8488:
8438:
8389:
8377:
8356:divide
8345:Then,
8324:
8318:
8306:
8291:
8285:
8279:
8273:
8264:
8255:
8246:
8240:
8231:
8225:
8219:IsZero
8099:
8043:
8031:
8016:
8010:divide
7997:divide
7993:divide
7929:
7923:
7888:
7882:
7870:
7855:
7849:
7843:
7837:
7825:
7816:
7807:
7801:
7792:
7786:
7780:IsZero
7759:
7753:
7747:
7741:
7698:, not
7651:
7645:
7633:
7627:IsZero
7614:IsZero
7567:
7558:
7526:
7517:
7505:
7444:
7426:
7417:
7405:
7396:
7375:
7366:
7354:
7342:
7333:
7309:
7300:
7288:
7276:
7264:
7255:
7228:
7219:
7207:
7195:
7183:
7171:
7162:
7082:
7073:
7064:
7055:
7043:
7025:
7016:
7007:
6986:
6962:
6938:
6932:second
6926:
6914:
6905:
6899:second
6893:
6884:
6872:
6775:
6740:
6716:
6704:
6668:
6653:
6593:
6581:
6540:
6534:
6513:Using
6444:
6435:
6381:
6372:
6357:
6322:
6310:
6304:
6289:
6275:then,
6257:
6213:
6204:
6186:
6174:
6119:
6060:
6048:
6042:
5983:
5962:
5950:
5941:
5914:
5815:
5780:
5771:
5721:
5689:
5575:
5569:
5512:
5506:
5485:
5473:
5416:
5287:
5281:
5236:
5230:
5221:
5209:
5152:
5067:
5055:
5013:
5004:
4986:
4974:
4932:
4926:
4905:
4887:
4865:
4850:
4830:
4824:
4815:
4797:
4781:
4766:
4719:
4710:
4701:
4680:
4668:
4656:
4633:
4624:
4615:
4606:
4585:
4573:
4561:
4537:
4528:
4510:
4498:
4478:
4469:
4460:
4442:
4430:
4409:
4394:
4377:
4368:
4353:
4331:
4292:Number
3875:
3854:
3848:
3770:
3675:
3654:
3642:
3633:
3606:
3539:
3530:
3524:
3377:
3332:
3326:
3317:
3251:
3245:
3236:
3221:
3215:
3209:
3203:
3173:
3154:
3148:
3083:
3074:
3020:
3011:
3002:
2939:
2930:
2921:
2909:
2903:
2897:
2891:
2861:
2829:
2704:
2698:
2689:
2683:
2617:
2611:
2602:
2596:
2584:
2578:
2572:
2566:
2504:
2424:
2418:
2409:
2352:
2346:
2337:
2325:
2319:
2313:
2258:
2160:
2057:
2036:
2024:
2015:
1988:
1891:
1835:
1810:
1804:
1772:
1753:
1747:
1683:
1664:
1658:
1578:
1569:
1560:
1341:
1335:
1326:
1261:
1175:
1169:
1160:
1154:
888:
843:
824:
818:
777:
768:
759:
718:
709:
700:
688:
682:
661:
652:
614:
605:
593:
587:
569:
534:
522:
516:
463:
457:
427:Number
278:-fold
89:. The
19029:Model
18777:Peano
18634:Proof
18474:Arity
18403:Naive
18290:image
18222:Fuzzy
18182:Empty
18131:union
18076:Class
17717:Model
17707:Lemma
17665:Axiom
17571:(PDF)
17555:S2CID
17525:(PDF)
17480:(PDF)
17181:=>
17172:=>
17166:=>
17154:=>
17019:with
16756:=>
16729:=>
16717:match
16683:Scala
16481:false
16327:false
16281:isnil
15991:false
15939:isnil
15932:false
15898:first
15836:node
15832:In a
15723:first
15647:false
15591:first
15585:isnil
15492:First
15475:First
15404:isnil
14970:first
14830:first
14537:minus
14466:false
14410:false
14314:false
13993:false
13521:false
13502:false
13490:false
13451:false
13439:false
13378:false
13208:false
12926:false
12915:false
12702:false
12646:false
12633:false
12565:->
12517:->
12508:->
12487:->
12478:->
12454:->
12439:->
12433:->
12424:->
12327:first
12249:first
12141:first
12120:first
11898:first
11820:first
11712:first
11691:first
11189:first
11111:first
11045:minus
10673:first
10652:first
10195:first
10099:first
9980:first
9881:first
9812:first
8818:minus
8759:false
8686:false
8312:minus
7917:minus
7876:minus
7639:minus
7429:three
7399:first
7336:first
7258:first
7165:first
7154:three
7121:three
7058:first
6810:const
6769:const
6710:const
6662:value
6656:const
6634:const
6626:const
6612:Const
6528:value
6366:value
6298:value
6251:value
6198:value
6180:value
6089:value
6036:value
5825:const
5655:value
5634:value
5630:const
5479:value
5431:const
5360:const
5358:with
5352:const
5342:const
5215:value
5094:Then
5061:value
4998:value
4980:value
4899:value
4859:value
4853:const
4809:value
4775:value
4695:value
4683:const
4600:value
4522:value
4513:const
4454:value
4403:value
4397:const
4362:value
4325:value
4262:value
3964:with
3947:Notes
3842:minus
3715:Monus
2124:minus
2096:n - 1
1787:and,
222:from
19152:Type
18955:list
18759:list
18736:list
18725:Term
18659:rank
18553:open
18447:list
18259:Maps
18164:sets
18023:Free
17993:list
17743:list
17670:list
17462:ISBN
17433:ISBN
17308:ISBN
17273:ISBN
17169:List
17145:List
17142:type
16934:cons
16813:list
16798:and
16790:and
16784:list
16782:The
16738:Cons
16735:case
16723:case
16714:list
16691:List
16687:list
16488:tail
16426:head
16343:cons
16336:true
15997:true
15905:tail
15888:head
15881:pair
15871:cons
15846:tail
15844:and
15842:head
15773:tail
15708:head
15659:pair
15641:pair
15617:cons
15571:true
15555:true
15546:true
15537:pair
15434:tail
15424:head
15414:cons
15377:list
15371:An (
14982:pair
14774:pair
14759:is,
14753:pair
14747:Cons
14475:true
14370:true
14016:true
13776:true
13753:true
13515:true
13496:true
13457:true
13445:true
13430:true
13372:true
13214:true
12924:and
12922:true
12903:true
12667:true
12640:true
12631:and
12629:true
12622:Pico
12620:and
12612:and
12610:true
12406:type
12389:and
12294:divZ
12237:divZ
12225:plus
12165:divZ
12108:divZ
12096:plus
12084:pair
12040:divZ
12036:mult
12032:divZ
11950:divZ
11937:divZ
11865:mult
11808:mult
11796:plus
11736:mult
11679:mult
11667:plus
11655:pair
11625:mult
11156:plus
11099:plus
11087:pair
10697:plus
10640:plus
10628:pair
10586:plus
10284:OneZ
10219:pred
10183:pred
10171:pair
10063:OneZ
10004:pred
9968:pred
9956:pair
9779:pair
9716:pair
8862:pred
8849:pred
8724:true
8695:true
8448:succ
8383:succ
8075:by;
8037:succ
7709:<
7561:else
7520:then
7411:pair
7360:pair
7303:zero
7294:pair
7231:zero
7222:zero
7213:pair
7148:pred
7115:pred
7035:pred
7028:zero
7019:zero
7010:pair
6954:zero
6920:succ
6887:pair
6622:init
6620:the
6618:pred
6564:so,
6340:so,
6145:The
6078:so,
5878:pred
5867:as,
5865:pred
5793:init
5636:and
5626:init
5377:pred
5364:same
5356:init
5320:The
5167:init
4769:init
4588:init
4445:init
4356:init
4319:init
4274:init
4272:and
4258:init
4256:and
4248:and
4123:pred
4024:pred
3923:pred
3869:pred
3533:else
2752:succ
2560:plus
2444:...
2307:succ
2154:pred
2102:and
1952:pred
1917:pred
1909:The
1515:mult
1370:mult
1290:succ
1255:plus
1204:succ
1109:plus
961:plus
18839:of
18821:of
18769:of
18301:Sur
18275:Map
18082:Ur-
18064:Set
17547:doi
17505:doi
17265:doi
16873:nil
16726:Nil
16695:Nil
16678:).
16246:nil
15922:nil
15834:nil
15531:nil
15394:nil
14707:LEQ
14680:LEQ
14668:and
14501:LEQ
14001:not
13761:not
13366:and
13258:not
13221:xor
13105:not
13042:not
12947:and
12930:not
12909:if
12897:if
9758:neg
8441:div
8156:div
8093:div
8073:div
7447:two
7420:two
7378:two
7369:one
7312:one
7085:pc0
6999:pc0
6647:inc
6408:inc
6351:inc
6168:inc
6155:f v
6147:inc
6141:Inc
5740:inc
5622:inc
5425:inc
5349:inc
5334:inc
5326:inc
5161:inc
5038:),
4968:inc
4844:inc
4760:inc
4674:inc
4662:inc
4650:inc
4579:inc
4567:inc
4555:inc
4504:inc
4492:inc
4436:inc
4424:inc
4388:inc
4347:inc
4270:inc
4254:inc
3892:...
3454:val
3448:con
3436:inc
3197:exp
1864:exp
1798:exp
1604:exp
1244:to
1240:is
950:).
149:to
116:Use
77:In
19625::
19225:NP
18849::
18843::
18773::
18450:),
18305:Bi
18297:In
17590:.
17577:.
17573:.
17553:.
17545:.
17533:22
17531:.
17527:.
17427:.
17401:.
17382:.
17378:.
17330:.
17306:.
17271:.
17247:^
16662:.
15696:.
15375:)
14644:EQ
14338:A
13509:or
13283:if
12994:or
12932:.
12917:.
12624:.
12580:cn
12574:cn
12556:::
12448:::
12377:.
12042:.
9652:,
7984:.
7499:if
7133::
6517:,
6157:.
5632:,
5628:,
5624:,
4276:.
4239:-1
4007:^
3949::
3515:==
3503:if
1504:.
1279:.
1098:.
411::
383:.
375:,
371:,
81:,
19401:e
19394:t
19387:v
19305:/
19220:P
18975:)
18761:)
18757:(
18654:∀
18649:!
18644:∃
18605:=
18600:↔
18595:→
18590:∧
18585:∨
18580:¬
18303:/
18299:/
18273:/
18084:)
18080:(
17967:∞
17957:3
17745:)
17643:e
17636:t
17629:v
17604:.
17581:.
17561:.
17549::
17511:.
17507::
17488:.
17470:.
17441:.
17407:.
17364:.
17349:.
17316:.
17281:.
17267::
17205:E
17201:E
17197:C
17187:C
17178:)
17175:C
17163:E
17160:(
17151:C
17148:=
17119:i
17115:n
17092:i
17088:n
17067:i
17047:m
17027:m
17000:t
16994:h
16988:c
16982:.
16979:c
16973:.
16970:n
16949:t
16943:h
16921:t
16917:h
16900:n
16894:.
16891:c
16885:.
16882:n
16856:c
16848:n
16777:}
16774:)
16771:t
16768:,
16765:h
16762:(
16753:)
16750:t
16747:,
16744:h
16741:(
16720:{
16639:)
16636:t
16633:.
16630:t
16624:.
16621:h
16615:(
16609:)
16606:n
16603:.
16600:t
16594:(
16588:)
16585:)
16582:c
16576:t
16573:(
16567:h
16561:g
16558:.
16555:g
16549:.
16546:t
16540:.
16537:h
16531:(
16525:l
16522:.
16519:n
16513:.
16510:c
16504:.
16501:l
16475:)
16472:h
16469:.
16466:t
16460:.
16457:h
16451:(
16445:l
16442:.
16439:l
16419:)
16416:n
16410:c
16404:t
16401:(
16395:h
16389:c
16386:.
16383:n
16377:.
16374:c
16368:.
16365:t
16359:.
16356:h
16330:)
16324:.
16321:t
16315:.
16312:h
16306:(
16300:l
16297:.
16294:l
16274:n
16271:.
16268:n
16262:.
16259:c
16203:e
16200:s
16197:u
16194:a
16191:l
16188:c
16185:-
16182:l
16179:i
16176:n
16172:)
16168:e
16165:s
16162:u
16159:a
16156:l
16153:c
16150:-
16147:l
16144:i
16141:a
16138:t
16135:-
16132:d
16129:n
16126:a
16123:-
16120:d
16117:a
16114:e
16111:h
16107:.
16104:d
16098:.
16095:t
16089:.
16086:h
16080:(
16077:l
16074:.
16071:l
16061:t
16058:s
16055:i
16052:l
16049:-
16046:s
16043:s
16040:e
16037:c
16034:o
16031:r
16028:p
15994:)
15988:.
15985:d
15979:.
15976:t
15970:.
15967:h
15961:(
15958:l
15955:.
15952:l
15809:)
15806:z
15797:(
15785:.
15782:z
15744:)
15741:z
15732:(
15720:.
15717:z
15694:t
15690:h
15674:)
15671:t
15665:h
15656:(
15638:.
15635:t
15629:.
15626:h
15458:.
15347:a
15344:=
15341:b
15335:a
15329:)
15326:x
15323:.
15320:y
15314:.
15311:x
15305:(
15298:=
15291:)
15288:x
15285:.
15282:y
15276:.
15273:x
15267:(
15261:)
15258:b
15252:a
15246:z
15243:.
15240:z
15234:(
15227:=
15220:)
15217:b
15211:a
15205:z
15202:.
15199:z
15193:(
15187:)
15184:)
15181:x
15178:.
15175:y
15169:.
15166:x
15160:(
15154:p
15151:.
15148:p
15142:(
15135:=
15128:)
15125:b
15119:a
15113:)
15110:y
15104:x
15098:z
15095:.
15092:z
15086:.
15083:y
15077:.
15074:x
15068:(
15065:(
15059:)
15056:)
15053:x
15050:.
15047:y
15041:.
15038:x
15032:(
15026:p
15023:.
15020:p
15014:(
15007:=
15000:)
14997:b
14991:a
14979:(
14935:)
14932:y
14929:.
14926:y
14920:.
14917:x
14911:(
14905:p
14902:.
14899:p
14879:)
14876:x
14873:.
14870:y
14864:.
14861:x
14855:(
14849:p
14846:.
14843:p
14823:y
14817:x
14811:z
14808:.
14805:z
14799:.
14796:y
14790:.
14787:x
14725:)
14722:m
14716:n
14704:(
14698:)
14695:n
14689:m
14677:(
14665:.
14662:n
14656:.
14653:m
14647:=
14618:)
14615:x
14609:y
14603:y
14597:x
14594:(
14588:y
14585:=
14582:x
14567:,
14555:)
14552:n
14546:m
14534:(
14522:.
14519:n
14513:.
14510:m
14504:=
14469:)
14463:.
14460:x
14454:(
14448:n
14445:.
14442:n
14436:=
14390:0
14311:=
14308:b
14305:.
14302:b
14296:.
14293:a
14287:=
14284:)
14281:a
14278:.
14275:b
14269:.
14266:a
14260:(
14254:)
14251:)
14248:b
14245:.
14242:b
14236:.
14233:a
14227:(
14224:.
14221:b
14215:(
14212:=
14209:)
14206:a
14203:.
14200:b
14194:.
14191:a
14185:(
14182:)
14179:b
14176:.
14173:b
14167:.
14164:a
14158:(
14155:)
14152:a
14149:.
14146:b
14140:.
14137:a
14131:(
14128:=
14125:)
14122:a
14119:.
14116:b
14110:.
14107:a
14101:(
14098:)
14095:)
14092:a
14089:.
14086:b
14080:.
14077:a
14071:(
14068:)
14065:b
14062:.
14059:b
14053:.
14050:a
14044:(
14038:p
14035:.
14032:p
14026:(
14023:=
14005:2
13990:=
13987:b
13984:.
13981:b
13975:.
13972:a
13966:=
13963:a
13957:)
13954:b
13951:.
13948:c
13942:(
13939:.
13936:b
13930:.
13927:a
13921:=
13918:a
13912:b
13906:)
13903:a
13900:.
13897:b
13891:.
13888:a
13882:(
13879:.
13876:b
13870:.
13867:a
13861:=
13858:)
13855:a
13852:.
13849:b
13843:.
13840:a
13834:(
13831:)
13828:a
13822:b
13816:p
13813:.
13810:b
13804:.
13801:a
13795:.
13792:p
13786:(
13783:=
13765:1
13750:=
13747:)
13744:a
13741:.
13738:b
13732:.
13729:a
13723:(
13720:=
13717:)
13714:b
13711:.
13708:b
13702:.
13699:a
13693:(
13687:)
13684:a
13681:.
13678:b
13672:.
13669:a
13663:(
13657:)
13654:a
13651:.
13648:b
13642:.
13639:a
13633:(
13630:=
13627:)
13624:b
13621:.
13618:b
13612:.
13609:a
13603:(
13597:)
13594:a
13591:.
13588:b
13582:.
13579:a
13573:(
13567:)
13564:q
13558:p
13552:p
13549:.
13546:q
13540:.
13537:p
13531:(
13528:=
13499:=
13487:)
13484:a
13481:.
13478:b
13472:.
13469:a
13463:(
13460:=
13442:=
13424:)
13421:p
13415:q
13409:p
13406:.
13403:q
13397:.
13394:p
13388:(
13385:=
13332:b
13326:a
13320:p
13317:.
13314:b
13308:.
13305:a
13299:.
13296:p
13290:=
13276:b
13270:)
13267:b
13255:(
13249:a
13246:.
13243:b
13237:.
13234:a
13228:=
13205:p
13202:.
13199:p
13193:=
13190:)
13187:a
13184:.
13181:b
13175:.
13172:a
13166:(
13160:)
13157:b
13154:.
13151:b
13145:.
13142:a
13136:(
13130:p
13127:.
13124:p
13118:=
13109:2
13097:a
13091:b
13085:p
13082:.
13079:b
13073:.
13070:a
13064:.
13061:p
13055:=
13046:1
13034:q
13028:p
13022:p
13019:.
13016:q
13010:.
13007:p
13001:=
12987:p
12981:q
12975:p
12972:.
12969:q
12963:.
12960:p
12954:=
12877:e
12874:s
12871:u
12868:a
12865:l
12862:c
12859:-
12856:e
12853:s
12850:l
12847:e
12836:e
12833:s
12830:u
12827:a
12824:l
12821:c
12818:-
12815:n
12812:e
12809:h
12806:t
12799:x
12792:-
12789:e
12786:t
12783:a
12780:c
12777:i
12774:d
12771:e
12768:r
12765:p
12730:b
12727:.
12724:b
12718:.
12715:a
12695:a
12692:.
12689:b
12683:.
12680:a
12595:0
12592:)
12589:1
12586:+
12583:(
12577:=
12550:)
12547:x
12544:f
12541:)
12538:1
12535:-
12532:n
12529:(
12523:(
12520:f
12514:x
12511:\
12505:f
12502:\
12499:=
12496:n
12490:x
12484:x
12481:\
12475:f
12472:\
12469:=
12466:0
12442:a
12436:a
12430:)
12427:a
12421:a
12418:(
12415:=
12412:a
12399:\
12345:)
12342:)
12339:)
12336:y
12324:(
12318:)
12315:x
12303:(
12291:(
12285:)
12282:)
12279:y
12267:(
12261:)
12258:x
12246:(
12234:(
12222:(
12216:)
12213:)
12210:)
12207:y
12195:(
12189:)
12186:x
12174:(
12162:(
12156:)
12153:)
12150:y
12138:(
12132:)
12129:x
12117:(
12105:(
12093:(
12081:.
12078:y
12072:.
12069:x
12063:=
12058:s
12016:)
12013:y
12007:x
11995:(
11989:0
11983:y
11971:.
11968:y
11962:.
11959:x
11953:=
11916:)
11913:)
11910:)
11907:y
11895:(
11889:)
11886:x
11874:(
11862:(
11856:)
11853:)
11850:y
11838:(
11832:)
11829:x
11817:(
11805:(
11793:(
11787:)
11784:)
11781:)
11778:y
11766:(
11760:)
11757:x
11745:(
11733:(
11727:)
11724:)
11721:y
11709:(
11703:)
11700:x
11688:(
11676:(
11664:(
11652:.
11649:y
11643:.
11640:x
11634:=
11629:s
11598:]
11593:p
11589:y
11580:n
11576:x
11572:+
11567:n
11563:y
11554:p
11550:x
11546:,
11541:n
11537:y
11528:n
11524:x
11520:+
11515:p
11511:y
11502:p
11498:x
11494:[
11491:=
11488:)
11483:p
11479:y
11470:n
11466:x
11462:+
11457:n
11453:y
11444:p
11440:x
11436:(
11430:)
11425:n
11421:y
11412:n
11408:x
11404:+
11399:p
11395:y
11386:p
11382:x
11378:(
11375:=
11372:)
11367:n
11363:y
11354:p
11350:y
11346:(
11340:)
11335:n
11331:x
11322:p
11318:x
11314:(
11311:=
11308:]
11303:n
11299:y
11295:,
11290:p
11286:y
11282:[
11276:]
11271:n
11267:x
11263:,
11258:p
11254:x
11250:[
11247:=
11244:y
11238:x
11207:)
11204:)
11201:)
11198:y
11186:(
11180:)
11177:x
11165:(
11153:(
11147:)
11144:)
11141:y
11129:(
11123:)
11120:x
11108:(
11096:(
11084:(
11072:.
11069:y
11063:.
11060:x
11054:=
11049:s
11018:]
11013:p
11009:y
11005:+
11000:n
10996:x
10992:,
10987:n
10983:y
10979:+
10974:p
10970:x
10966:[
10963:=
10960:)
10955:p
10951:y
10947:+
10942:n
10938:x
10934:(
10928:)
10923:n
10919:y
10915:+
10910:p
10906:x
10902:(
10899:=
10894:n
10890:y
10886:+
10881:p
10877:y
10868:n
10864:x
10855:p
10851:x
10847:=
10844:]
10839:n
10835:y
10831:,
10826:p
10822:y
10818:[
10812:]
10807:n
10803:x
10799:,
10794:p
10790:x
10786:[
10783:=
10780:y
10774:x
10748:)
10745:)
10742:)
10739:y
10727:(
10721:)
10718:x
10706:(
10694:(
10688:)
10685:)
10682:y
10670:(
10664:)
10661:x
10649:(
10637:(
10625:(
10613:.
10610:y
10604:.
10601:x
10595:=
10590:s
10559:]
10554:n
10550:y
10546:+
10541:n
10537:x
10533:,
10528:p
10524:y
10520:+
10515:p
10511:x
10507:[
10504:=
10501:)
10496:n
10492:y
10488:+
10483:n
10479:x
10475:(
10469:)
10464:p
10460:y
10456:+
10451:p
10447:x
10443:(
10440:=
10435:n
10431:y
10422:p
10418:y
10414:+
10409:n
10405:x
10396:p
10392:x
10388:=
10385:]
10380:n
10376:y
10372:,
10367:p
10363:y
10359:[
10356:+
10353:]
10348:n
10344:x
10340:,
10335:p
10331:x
10327:[
10324:=
10321:y
10318:+
10315:x
10281:Y
10278:=
10252:)
10249:)
10246:)
10243:)
10240:x
10228:(
10216:(
10210:)
10207:)
10204:x
10192:(
10180:(
10165:c
10162:(
10156:x
10150:)
10147:x
10135:(
10123:(
10117:x
10111:)
10108:x
10096:(
10084:.
10081:x
10075:.
10072:c
10066:=
10037:)
10034:)
10031:)
10028:)
10025:x
10013:(
10001:(
9995:)
9992:)
9989:x
9977:(
9965:(
9944:(
9938:x
9932:)
9929:x
9917:(
9905:(
9899:x
9893:)
9890:x
9878:(
9866:.
9863:x
9857:=
9824:)
9821:x
9809:(
9803:)
9800:x
9788:(
9776:.
9773:x
9767:=
9762:s
9731:0
9725:x
9713:.
9710:x
9704:=
9699:s
9632:)
9629:n
9623:)
9620:)
9617:x
9611:f
9605:n
9602:(
9596:f
9593:.
9590:x
9584:.
9581:f
9575:.
9572:n
9566:(
9563:(
9557:)
9554:)
9551:)
9548:m
9542:n
9536:)
9533:m
9530:)
9527:)
9524:u
9521:.
9518:u
9512:(
9506:)
9503:x
9500:.
9497:u
9491:(
9485:)
9482:)
9479:f
9473:g
9470:(
9464:h
9461:.
9458:h
9452:.
9449:g
9443:(
9437:n
9434:.
9431:x
9425:.
9422:f
9416:.
9413:n
9407:(
9404:n
9401:.
9398:n
9392:.
9389:m
9383:(
9380:(
9374:)
9371:)
9368:)
9365:x
9359:f
9353:m
9347:d
9341:c
9338:(
9332:f
9329:(
9323:)
9320:x
9314:f
9308:)
9305:x
9302:.
9299:x
9293:.
9290:f
9284:(
9281:(
9275:d
9269:)
9266:)
9263:a
9260:.
9257:b
9251:.
9248:a
9242:(
9236:)
9233:)
9230:b
9227:.
9224:b
9218:.
9215:a
9209:(
9206:.
9203:x
9197:(
9191:n
9188:.
9185:n
9179:(
9176:.
9173:d
9167:(
9164:.
9161:x
9155:.
9152:f
9146:.
9143:m
9137:.
9134:n
9128:.
9125:c
9119:(
9113:)
9110:)
9107:)
9104:x
9098:x
9095:(
9089:f
9086:.
9083:x
9077:(
9071:)
9068:x
9062:x
9059:.
9056:x
9050:(
9047:.
9044:f
9038:(
9035:(
9032:.
9029:n
9023:=
8989:)
8986:u
8983:.
8980:u
8974:(
8968:)
8965:x
8962:.
8959:u
8953:(
8947:)
8944:)
8941:f
8935:g
8932:(
8926:h
8923:.
8920:h
8914:.
8911:g
8905:(
8899:n
8896:.
8893:x
8887:.
8884:f
8878:.
8875:n
8869:=
8855:m
8846:n
8843:.
8840:n
8834:.
8831:m
8825:=
8787:b
8784:.
8781:b
8775:.
8772:a
8752:a
8749:.
8746:b
8740:.
8737:a
8689:)
8683:.
8680:x
8674:(
8668:n
8665:.
8662:n
8656:=
8642:x
8639:.
8636:x
8630:.
8627:f
8621:=
8614:0
8607:)
8604:)
8601:x
8595:x
8592:(
8586:f
8583:.
8580:x
8574:(
8568:)
8565:)
8562:x
8556:x
8553:(
8547:f
8544:.
8541:x
8535:(
8532:.
8529:f
8523:=
8516:Y
8509:)
8506:x
8500:f
8494:n
8491:(
8485:f
8482:.
8479:x
8473:.
8470:f
8464:.
8461:n
8455:=
8435:Y
8432:=
8395:)
8392:n
8380:(
8368:.
8365:n
8359:=
8330:)
8327:m
8321:n
8309:(
8303:)
8300:)
8297:)
8294:x
8288:f
8282:m
8276:d
8270:c
8267:(
8261:f
8258:(
8252:)
8249:x
8243:f
8237:0
8234:(
8228:d
8216:.
8213:d
8207:(
8204:.
8201:x
8195:.
8192:f
8186:.
8183:m
8177:.
8174:n
8168:.
8165:c
8159:=
8130:c
8102:c
8049:)
8046:n
8034:(
8022:=
8019:n
7989:n
7972:m
7968:/
7964:)
7961:1
7955:n
7952:(
7932:m
7926:n
7894:)
7891:m
7885:n
7873:(
7867:)
7864:)
7861:)
7858:x
7852:f
7846:m
7840:d
7828:(
7822:f
7819:(
7813:)
7810:x
7804:f
7798:0
7795:(
7789:d
7777:.
7774:d
7768:(
7765:=
7762:x
7756:f
7750:m
7744:n
7712:m
7706:n
7686:m
7680:n
7657:)
7654:m
7648:n
7636:(
7599:m
7593:n
7570:0
7555:m
7551:/
7547:)
7544:m
7538:n
7535:(
7532:+
7529:1
7514:m
7508:n
7496:=
7493:m
7489:/
7485:n
7439:=
7432:)
7408:(
7391:=
7384:)
7381:)
7357:(
7348:f
7345:(
7328:=
7321:)
7318:)
7315:)
7291:(
7282:f
7279:(
7270:f
7267:(
7250:=
7243:)
7240:)
7237:)
7234:)
7210:(
7201:f
7198:(
7189:f
7186:(
7177:f
7174:(
7157:=
7088:)
7076:f
7070:n
7067:(
7052:.
7049:n
7038:=
7002:=
6992:)
6989:x
6983:.
6980:x
6974:.
6971:f
6965:(
6957:=
6947:)
6944:)
6941:p
6929:(
6917:(
6911:)
6908:p
6896:(
6881:.
6878:p
6867:=
6864:f
6825:x
6822:.
6819:u
6813:=
6784:x
6781:=
6778:f
6743:x
6737:h
6734:.
6731:h
6725:=
6722:)
6719:f
6707:(
6701:h
6698:.
6695:h
6671:x
6659:=
6630:f
6596:I
6590:k
6587:=
6584:k
6549:v
6546:=
6543:I
6537:v
6515:I
6498:u
6495:.
6492:u
6486:=
6483:I
6450:)
6447:f
6441:g
6438:(
6432:h
6429:.
6426:h
6420:.
6417:g
6411:=
6387:)
6384:f
6378:g
6375:(
6363:=
6360:g
6325:v
6319:f
6316:=
6313:f
6307:v
6295:=
6292:f
6286:g
6260:v
6248:=
6245:g
6219:)
6216:v
6210:f
6207:(
6195:=
6192:)
6189:v
6177:(
6151:v
6125:)
6122:v
6116:h
6113:.
6110:h
6104:(
6101:.
6098:v
6092:=
6063:v
6057:h
6054:=
6051:h
6045:v
6001:)
5998:u
5995:.
5992:u
5986:(
5980:)
5977:x
5974:.
5971:u
5965:(
5959:)
5956:)
5953:f
5947:g
5944:(
5938:h
5935:.
5932:h
5926:.
5923:g
5917:(
5911:n
5908:.
5905:x
5899:.
5896:f
5890:.
5887:n
5881:=
5844:x
5841:.
5838:u
5832:=
5818:x
5812:h
5809:.
5806:h
5800:=
5786:)
5783:f
5777:g
5774:(
5768:h
5765:.
5762:h
5756:.
5753:g
5747:=
5733:u
5730:.
5727:u
5718:k
5715:=
5708:k
5695:)
5692:v
5686:h
5683:.
5680:h
5674:(
5671:.
5668:v
5662:=
5605:)
5602:1
5596:n
5593:(
5590:.
5587:n
5581:=
5578:x
5572:f
5566:)
5563:1
5557:n
5554:(
5551:.
5548:x
5542:.
5539:f
5533:.
5530:n
5524:=
5521:)
5518:)
5515:x
5509:f
5503:)
5500:1
5494:n
5491:(
5488:(
5476:(
5464:.
5461:x
5455:.
5452:f
5446:.
5443:n
5437:=
5434:)
5422:n
5419:(
5407:.
5404:x
5398:.
5395:f
5389:.
5386:n
5380:=
5346:n
5338:f
5330:f
5305:n
5302:.
5299:n
5293:=
5290:x
5284:f
5278:n
5275:.
5272:x
5266:.
5263:f
5257:.
5254:n
5248:=
5245:)
5242:)
5239:x
5233:f
5227:n
5224:(
5212:(
5200:.
5197:x
5191:.
5188:f
5182:.
5179:n
5173:=
5170:)
5158:n
5155:(
5143:.
5140:x
5134:.
5131:f
5125:.
5122:n
5116:=
5079:v
5076:=
5073:)
5070:v
5058:(
5019:)
5016:v
5010:f
5007:(
4995:=
4992:)
4989:v
4977:(
4938:)
4935:x
4929:f
4923:)
4920:1
4914:n
4911:(
4908:(
4896:=
4893:)
4890:x
4882:1
4876:n
4872:f
4868:(
4856:=
4841:n
4836:)
4833:x
4827:f
4821:n
4818:(
4806:=
4803:)
4800:x
4792:n
4788:f
4784:(
4772:=
4757:n
4752:n
4728:)
4725:)
4722:x
4716:f
4713:(
4707:f
4704:(
4692:=
4689:)
4686:)
4671:(
4659:(
4645:)
4642:)
4639:)
4636:x
4630:f
4627:(
4621:f
4618:(
4612:f
4609:(
4597:=
4594:)
4591:)
4576:(
4564:(
4550:3
4543:)
4540:x
4534:f
4531:(
4519:=
4516:)
4501:(
4487:)
4484:)
4481:x
4475:f
4472:(
4466:f
4463:(
4451:=
4448:)
4433:(
4419:2
4412:x
4400:=
4383:)
4380:x
4374:f
4371:(
4359:=
4342:1
4334:x
4322:=
4314:0
4266:n
4250:x
4246:f
4237:n
4232:n
4228:x
4224:n
4221:f
4217:n
4211:.
4183:1
4177:n
4170:,
4167:0
4164:=
4161:n
4149:0
4143:{
4138:=
4135:)
4132:n
4129:(
4087:0
4084:=
4081:n
4075:m
4069:n
4063:m
4042:0
4039:=
4036:)
4033:0
4030:(
4002:.
3990:f
3984:x
3981:,
3978:m
3972:f
3962:n
3929:m
3920:n
3917:.
3914:n
3908:.
3905:m
3878:m
3872:)
3866:n
3863:(
3860:=
3857:n
3851:m
3821:)
3818:x
3813:m
3809:f
3805:(
3800:n
3796:)
3790:1
3783:f
3779:(
3776:=
3773:x
3765:n
3759:m
3755:f
3733:n
3727:m
3717:)
3713:(
3693:)
3690:u
3687:.
3684:u
3678:(
3672:)
3669:x
3666:.
3663:u
3657:(
3651:)
3648:)
3645:f
3639:g
3636:(
3630:h
3627:.
3624:h
3618:.
3615:g
3609:(
3603:n
3600:.
3597:x
3591:.
3588:f
3582:.
3579:n
3554:)
3551:1
3545:n
3542:(
3527:0
3521:)
3518:0
3512:n
3509:(
3482:)
3479:x
3474:1
3468:n
3464:f
3460:(
3451:=
3440:n
3414:1
3408:n
3380:m
3374:n
3371:.
3368:n
3362:.
3359:m
3335:x
3329:f
3323:)
3320:m
3314:n
3311:(
3308:.
3305:x
3299:.
3296:f
3290:.
3287:n
3281:.
3278:m
3254:x
3248:f
3242:)
3239:m
3233:n
3230:(
3227:=
3224:x
3218:f
3212:n
3206:m
3176:f
3168:n
3164:m
3160:=
3157:f
3151:m
3145:n
3122:n
3118:m
3089:)
3086:f
3080:n
3077:(
3071:m
3068:.
3065:f
3059:.
3056:n
3050:.
3047:m
3023:x
3017:)
3014:f
3008:n
3005:(
2999:m
2996:.
2993:x
2987:.
2984:f
2978:.
2975:n
2969:.
2966:m
2942:x
2936:)
2933:f
2927:n
2924:(
2918:m
2915:=
2912:x
2906:f
2900:n
2894:m
2864:x
2856:n
2852:)
2846:m
2842:f
2838:(
2835:=
2832:x
2824:n
2818:m
2814:f
2792:n
2786:m
2758:m
2749:n
2746:.
2743:n
2737:.
2734:m
2710:)
2707:x
2701:f
2695:n
2692:(
2686:f
2680:m
2677:.
2674:x
2668:.
2665:f
2659:.
2656:n
2650:.
2647:m
2623:)
2620:x
2614:f
2608:n
2605:(
2599:f
2593:m
2590:=
2587:x
2581:f
2575:n
2569:m
2539:)
2536:x
2531:n
2527:f
2523:(
2518:m
2514:f
2510:=
2507:x
2499:n
2496:+
2493:m
2489:f
2467:n
2464:+
2461:m
2430:)
2427:x
2421:f
2415:n
2412:(
2406:f
2403:.
2400:x
2394:.
2391:f
2385:.
2382:n
2358:)
2355:x
2349:f
2343:n
2340:(
2334:f
2331:=
2328:x
2322:f
2316:n
2286:)
2283:x
2278:n
2274:f
2270:(
2267:f
2264:=
2261:x
2253:1
2250:+
2247:n
2243:f
2221:1
2218:+
2215:n
2163:m
2157:)
2151:n
2148:(
2145:.
2142:n
2136:.
2133:m
2104:x
2100:f
2092:n
2075:)
2072:u
2069:.
2066:u
2060:(
2054:)
2051:x
2048:.
2045:u
2039:(
2033:)
2030:)
2027:f
2021:g
2018:(
2012:h
2009:.
2006:h
2000:.
1997:g
1991:(
1985:n
1982:.
1979:x
1973:.
1970:f
1964:.
1961:n
1929:)
1926:n
1923:(
1894:m
1888:n
1885:.
1882:n
1876:.
1873:m
1838:m
1832:n
1829:=
1824:n
1820:m
1816:=
1813:n
1807:m
1775:f
1767:n
1763:m
1759:=
1756:f
1750:m
1744:n
1724:f
1718:x
1715:,
1712:m
1706:h
1686:x
1678:n
1674:h
1670:=
1667:x
1661:h
1655:n
1633:n
1629:m
1625:=
1622:)
1619:n
1616:,
1613:m
1610:(
1581:x
1575:)
1572:f
1566:n
1563:(
1557:m
1554:.
1551:x
1545:.
1542:f
1536:.
1533:n
1527:.
1524:m
1492:)
1489:x
1486:(
1481:m
1474:)
1468:n
1461:f
1457:(
1454:=
1451:)
1448:x
1445:(
1440:)
1437:n
1431:m
1428:(
1421:f
1400:n
1394:m
1391:=
1388:)
1385:n
1382:,
1379:m
1376:(
1347:)
1344:x
1338:f
1332:n
1329:(
1323:f
1320:.
1317:x
1311:.
1308:f
1302:.
1299:n
1267:)
1264:1
1252:(
1228:1
1225:+
1222:n
1219:=
1216:)
1213:n
1210:(
1181:)
1178:x
1172:f
1166:n
1163:(
1157:f
1151:m
1148:.
1145:x
1139:.
1136:f
1130:.
1127:n
1121:.
1118:m
1086:)
1083:)
1080:x
1077:(
1072:n
1065:f
1061:(
1056:m
1049:f
1045:=
1042:)
1039:x
1036:(
1031:)
1028:n
1025:+
1022:m
1019:(
1012:f
991:n
988:+
985:m
982:=
979:)
976:n
973:,
970:m
967:(
925:3
921:3
912:3
891:x
883:n
876:f
872:.
869:x
863:.
860:f
854:=
851:n
846:x
838:n
834:f
830:=
827:x
821:f
815:n
810:n
786:)
783:)
780:x
774:f
771:(
765:f
762:(
756:f
753:.
750:x
744:.
741:f
735:=
732:3
727:)
724:)
721:x
715:f
712:(
706:f
703:(
697:f
694:=
691:x
685:f
679:3
674:3
667:)
664:x
658:f
655:(
649:f
646:.
643:x
637:.
634:f
628:=
625:2
620:)
617:x
611:f
608:(
602:f
599:=
596:x
590:f
584:2
579:2
572:x
566:f
563:.
560:x
554:.
551:f
545:=
542:1
537:x
531:f
528:=
525:x
519:f
513:1
508:1
501:x
498:.
495:x
489:.
486:f
480:=
477:0
472:x
469:=
466:x
460:f
454:0
449:0
406:3
401:2
396:1
390:0
377:2
373:1
369:0
351:.
341:n
331:f
319:f
313:f
306:=
301:n
294:f
276:n
262:f
252:n
186:n
166:)
163:n
160:(
157:O
137:)
134:1
131:(
128:O
68:)
64:(
54:.
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
