1224:
1776:
1766:
1756:
1746:
691:. The proof is constructed and checked in Isabelle/HOL and comprises over 200,000 lines of proof script to verify 7,500 lines of C. The verification covers code, design, and implementation, and the main theorem states that the C code correctly implements the formal specification of the kernel. The proof uncovered 144 bugs in an early version of the C code of the seL4 kernel, and about 150 issues in each of design and specification.
38:
1626:
408:) to apply. While reflecting the procedure that a human mathematician might apply to proving a result, they are typically hard to read as they do not describe the outcome of these steps. Declarative proofs (supported by Isabelle's proof language, Isar), on the other hand, specify the actual mathematical operations to be performed, and are therefore more easily read and checked by humans.
1088:
Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009).
221:
Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories as well as implementations for code-generation, documentation, and specific support for a variety of
288:(ZFC). The most widely used object logic is Isabelle/HOL, although significant set theory developments were completed in Isabelle/ZF. Isabelle's main proof method is a higher-order version of
675:. Many of the formal proofs are, as mentioned, maintained in the Archive of Formal Proofs, which contains (as of 2019) at least 500 articles with over 2 million lines of proof in total.
1276:
366:
which are modules that structure large proofs. A locale fixes types, constants, and assumptions within a specified scope so that they do not have to be repeated for every
401:
218:
theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.
1770:
672:
1283:
683:
produced the first formal proof of functional correctness of a general-purpose operating system kernel: the seL4 (secure embedded
1811:
1760:
974:
17:
230:
for formal methods. In recent years, a substantial number of theories and system extensions have been collected in the
Isabelle
1229:
1310:
227:
656:
1203:, M. Johnson, editor, Sydney, Australia. Lecture Notes in Computer Science (LNCS) Vol. 1349, Springer Verlag, 1997.
152:
285:
1588:
1441:
1349:
730:
312:
72:
1806:
1361:
788:
419:
1383:
211:
125:
726:
304:
92:
1481:
1717:
1427:
1338:
1801:
1543:
1457:
1406:
1343:
1292:
757:
1707:
1003:
784:
717:
336:
324:
199:
1780:
1447:
1269:
397:
293:
68:
1178:
1582:
753:
744:
415:
393:
289:
1634:
1562:
684:
203:
1745:
1090:
1739:
664:
343:
proof method reconstructs resolution proofs generated by these ATPs). It also features two
1189:
8:
1315:
1162:
1051:
1047:
1007:
641:
367:
1648:
1196:
1112:
1026:
Jasmin
Christian Blanchette, Mathias Fleury, Peter Lammich & Christoph Weidenbach,
933:
915:
328:
320:
281:
215:
982:
1702:
1174:
1120:
929:
668:
299:
Though interactive, Isabelle features efficient automatic reasoning tools, such as a
277:
937:
1468:
925:
860:
818:
697:
652:
242:
164:
132:
56:
1697:
1548:
1028:"A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality"
660:
1144:
1712:
1654:
1556:
735:
701:
637:
348:
300:
223:
1660:
1207:
1066:
Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René.
951:
Eberl, Manuel; Klein, Gerwin; Nipkow, Tobias; Paulson, Larry; Thiemann, René.
246:
1795:
1390:
1185:
1124:
1046:
Andrew
Reynolds, Jasmin Christian Blanchette, Simon Cruanes, Cesare Tinelli,
253:
1678:
1672:
1666:
1534:
1418:
1246:
762:
381:
344:
1750:
1395:
1374:
797:
766:
688:
648:
411:
The procedural style has been deprecated in recent versions of
Isabelle.
273:
257:
207:
169:
157:
121:
1027:
1009:
International
Symposium on Frontiers of Combining Systems – FroCoS 2011
981:. Cambridge AR Research (The Automated Reasoning Group). Archived from
906:
Paulson, L. C. (1986). "Natural deduction as higher-order resolution".
405:
269:
63:
51:
1568:
1510:
1684:
1475:
1301:
1166:
920:
771:
708:
Larry
Paulson keeps a list of research projects that use Isabelle.
392:
Isabelle allows proofs to be written in two different styles, the
1614:
1528:
1498:
1452:
1261:
780:
141:
37:
1594:
1522:
1486:
1355:
1087:
775:
1197:"DOVE: A Tool for Design Oriented Verification and Evaluation"
869:
380:") is Isabelle's formal proof language. It is inspired by the
180:
1625:
1600:
1516:
1400:
1332:
1239:
793:
748:
739:
722:
Several languages and systems provide similar functionality:
680:
332:
145:
137:
43:
1504:
1492:
1324:
1251:
1067:
1006:, in: Cesare Tinelli, Viorica Sofronie-Stokkermans (eds.),
1002:
Jasmin
Christian Blanchette, Lukas Bulwahn, Tobias Nipkow,
952:
839:
830:
647:
Isabelle has been used to formalize numerous theorems from
316:
1256:
1208:"Isabelle/HOL – A Proof Assistant for Higher-Order Logic"
1053:
875:
824:
1173:, Volume 5, Issue 3 (September 1989), pages: 363–397,
1081:
878:
827:
821:
1219:
872:
842:
836:
1206:Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel,
866:
863:
833:
1098:22nd ACM Symposium on Operating System Principles
27:Higher-order logic (HOL) automated theorem prover
1793:
1110:
307:, various decision procedures, and, through the
1111:Strniša, Rok; Parkinson, Matthew (2011-02-07).
659:, Gödel's theorem about the consistency of the
1048:"Model Finding for Recursive Functions in SMT"
1004:"Automatic Proof and Disproof in Isabelle/HOL"
276:), which is used to encode object logics like
1277:
1195:M. A. Ozols, K. A. Eastaughffe, and A. Cant,
1050:, in: Nicola Olivetti, Ashish Tiwari (eds.),
1167:"The Foundation of a Generic Theorem Prover"
1091:"seL4: Formal verification of an OS kernel"
696:The definition of the programming language
1284:
1270:
36:
1100:. Big Sky, Montana, US. pp. 207–200.
919:
1642:
718:Proof assistant § System comparison
400:. Procedural proofs specify a series of
905:
640:for the specification, development and
204:higher-order logic (HOL) theorem prover
14:
1794:
972:
420:the square root of two is not rational
1265:
1190:"Isabelle Tutorial and User's Manual"
378:intelligible semi-automated reasoning
311:proof-automation interface, external
1230:Free and open-source software portal
1145:"Projects - Isabelle Community Wiki"
1022:
1020:
1018:
679:In 2009, the L4.verified project at
483:(auto simp add: power2_eq_square)
268:Isabelle is generic: it provides a
24:
1291:
1155:
644:of software and hardware systems.
25:
1823:
1215:
1015:
1775:
1774:
1765:
1764:
1755:
1754:
1744:
1624:
1222:
908:The Journal of Logic Programming
859:
817:
387:
1137:
1104:
711:
631:
494:of_nat_eq_iff power2_eq_square
473:(rule Rats_abs_nat_div_natE)
252:The Isabelle theorem prover is
98:Isabelle2024 / May 2024
1812:Software using the BSD license
1589:Logic for Computable Functions
1171:Journal of Automated Reasoning
1059:
1040:
1032:Journal of Automated Reasoning
996:
966:
944:
899:
852:
810:
673:programming language semantics
636:Isabelle has been used to aid
313:satisfiability modulo theories
73:Technical University of Munich
13:
1:
892:
256:, released under the revised
1252:The Archive of Formal Proofs
930:10.1016/0743-1066(86)90015-4
657:Gödel's completeness theorem
7:
973:Gordon, Mike (1994-11-16).
422:can be written as follows.
414:For example, a declarative
286:Zermelo–Fraenkel set theory
263:
100:; 4 months ago
10:
1828:
1247:Isabelle on Stack Overflow
1068:"Archive of Formal Proofs"
953:"Archive of Formal Proofs"
715:
42:Isabelle/jEdit running on
1726:
1633:
1622:
1542:
1467:
1416:
1407:Standard ML of New Jersey
1373:
1323:
1309:
1300:
758:Standard ML of New Jersey
325:automated theorem provers
315:(SMT) solvers (including
175:
163:
151:
131:
117:
113:
91:
87:
79:
62:
50:
35:
1708:Christine Paulin-Mohring
1184:Lawrence C. Paulson and
1117:Archive of Formal Proofs
1065:
950:
803:
787:, with a GUI written in
292:, based on higher-order
232:Archive of Formal Proofs
200:automated theorem prover
1781:Category:Software:OCaml
1201:Proceedings of AMAST 97
226:. It can be seen as an
69:University of Cambridge
18:Isabelle theorem prover
598:(rule gcd_greatest)
429:sqrt2_not_rational:
416:proof by contradiction
241:Isabelle was named by
1771:Category:Family:OCaml
1119:(Feb 2011 ed.).
716:Further information:
554:"2 * n^2 = 2^2 * k^2"
1807:Free theorem provers
1740:Open-source software
671:, and properties of
665:prime number theorem
406:functions/procedures
1163:Lawrence C. Paulson
32:
1761:Category:Family:ML
1649:Lennart Augustsson
1113:"Lightweight Java"
669:security protocols
478:"m^2 = ?x^2 * n^2"
362:Isabelle features
327:(ATPs), including
282:higher-order logic
52:Original author(s)
30:
1789:
1788:
1703:Steven G. Johnson
1693:
1692:
1610:
1609:
1469:Programming tools
1437:
1436:
1056:, Springer, 2016.
1012:, Springer, 2011.
667:, correctness of
404:(theorem proving
278:first-order logic
193:
192:
16:(Redirected from
1819:
1802:Proof assistants
1778:
1777:
1768:
1767:
1758:
1757:
1748:
1640:
1639:
1628:
1549:proof assistants
1321:
1320:
1307:
1306:
1286:
1279:
1272:
1263:
1262:
1243:
1242:
1240:Official website
1232:
1227:
1226:
1225:
1149:
1148:
1141:
1135:
1134:
1132:
1131:
1108:
1102:
1101:
1095:
1085:
1079:
1078:
1076:
1074:
1063:
1057:
1044:
1038:
1037::333–365 (2018).
1024:
1013:
1000:
994:
993:
991:
990:
979:Isabelle and HOL
970:
964:
963:
961:
959:
948:
942:
941:
923:
903:
886:
885:
884:
881:
880:
877:
874:
871:
868:
865:
856:
850:
849:
848:
845:
844:
841:
838:
835:
832:
829:
826:
823:
814:
698:Lightweight Java
653:computer science
627:
623:
619:
615:
611:
608:
605:
601:
597:
594:
591:
588:
585:
582:
578:
575:
572:
568:
565:
562:
558:
555:
552:
548:
544:
541:
537:
534:
531:
527:
524:
521:
517:
514:
511:
507:
504:
501:
497:
493:
490:
486:
482:
479:
476:
472:
469:
465:
462:
458:
455:m n :: nat
454:
451:
448:
445:
442:
438:
435:
432:
428:
243:Lawrence Paulson
189:
186:
184:
182:
133:Operating system
108:
106:
101:
57:Lawrence Paulson
40:
33:
29:
21:
1827:
1826:
1822:
1821:
1820:
1818:
1817:
1816:
1792:
1791:
1790:
1785:
1743:
1722:
1698:Thierry Coquand
1689:
1629:
1620:
1606:
1547:
1544:Theorem provers
1538:
1463:
1433:
1412:
1369:
1314:
1311:Implementations
1296:
1290:
1238:
1237:
1228:
1223:
1221:
1218:
1213:
1158:
1156:Further reading
1153:
1152:
1143:
1142:
1138:
1129:
1127:
1109:
1105:
1093:
1086:
1082:
1072:
1070:
1064:
1060:
1045:
1041:
1025:
1016:
1001:
997:
988:
986:
971:
967:
957:
955:
949:
945:
904:
900:
895:
890:
889:
862:
858:
857:
853:
820:
816:
815:
811:
806:
720:
714:
661:axiom of choice
634:
629:
628:
625:
621:
617:
613:
609:
606:
603:
599:
595:
593:"2 dvd gcd m n"
592:
589:
586:
583:
580:
576:
573:
570:
566:
563:
560:
556:
553:
550:
546:
542:
539:
535:
532:
529:
525:
522:
519:
515:
512:
509:
505:
502:
499:
495:
491:
489:"m^2 = 2 * n^2"
488:
484:
480:
477:
474:
470:
467:
463:
460:
456:
452:
449:
446:
443:
440:
436:
433:
430:
426:
390:
305:tableaux prover
266:
179:
109:
104:
102:
99:
80:Initial release
46:
28:
23:
22:
15:
12:
11:
5:
1825:
1815:
1814:
1809:
1804:
1787:
1786:
1784:
1735:
1733:= discontinued
1727:
1724:
1723:
1721:
1720:
1718:Simon Thompson
1715:
1713:Frank Pfenning
1710:
1705:
1700:
1694:
1691:
1690:
1688:
1682:
1676:
1670:
1664:
1658:
1655:Damien Doligez
1652:
1646:
1644:
1637:
1631:
1630:
1623:
1621:
1619:
1618:
1611:
1608:
1607:
1605:
1604:
1598:
1592:
1585:
1580:
1574:
1573:
1572:
1560:
1553:
1551:
1540:
1539:
1537:
1532:
1526:
1520:
1514:
1508:
1502:
1496:
1490:
1484:
1479:
1473:
1471:
1465:
1464:
1462:
1461:
1455:
1450:
1445:
1438:
1435:
1434:
1432:
1431:
1424:
1422:
1414:
1413:
1411:
1410:
1404:
1398:
1393:
1388:
1379:
1377:
1371:
1370:
1368:
1367:
1366:
1365:
1359:
1353:
1347:
1341:
1329:
1327:
1318:
1304:
1298:
1297:
1289:
1288:
1281:
1274:
1266:
1260:
1259:
1254:
1249:
1244:
1234:
1233:
1217:
1216:External links
1214:
1212:
1211:
1204:
1193:
1182:
1159:
1157:
1154:
1151:
1150:
1136:
1103:
1080:
1058:
1039:
1014:
995:
965:
943:
914:(3): 237–258.
897:
896:
894:
891:
888:
887:
851:
808:
807:
805:
802:
801:
800:
791:
778:
769:
760:
751:
742:
733:
713:
710:
706:
705:
693:
692:
638:formal methods
633:
630:
466:lowest_terms:
461:"¦?x¦ = m / n"
425:
424:
389:
386:
349:counterexample
301:term rewriting
265:
262:
224:formal methods
191:
190:
177:
173:
172:
167:
161:
160:
155:
149:
148:
135:
129:
128:
119:
115:
114:
111:
110:
97:
95:
93:Stable release
89:
88:
85:
84:
81:
77:
76:
66:
60:
59:
54:
48:
47:
41:
26:
9:
6:
4:
3:
2:
1824:
1813:
1810:
1808:
1805:
1803:
1800:
1799:
1797:
1783:
1782:
1773:
1772:
1763:
1762:
1753:
1752:
1747:
1742:
1741:
1736:
1734:
1731:
1728:
1725:
1719:
1716:
1714:
1711:
1709:
1706:
1704:
1701:
1699:
1696:
1695:
1686:
1683:
1681:(Extended ML)
1680:
1677:
1674:
1671:
1669:(Caml, OCaml)
1668:
1665:
1662:
1659:
1656:
1653:
1650:
1647:
1645:
1641:
1638:
1636:
1632:
1627:
1616:
1613:
1612:
1602:
1599:
1596:
1593:
1591:
1590:
1586:
1584:
1581:
1578:
1575:
1570:
1567:
1566:
1564:
1561:
1558:
1555:
1554:
1552:
1550:
1545:
1541:
1536:
1533:
1530:
1527:
1524:
1521:
1518:
1515:
1512:
1509:
1506:
1503:
1500:
1497:
1494:
1491:
1488:
1485:
1483:
1480:
1477:
1474:
1472:
1470:
1466:
1459:
1456:
1454:
1451:
1449:
1446:
1443:
1440:
1439:
1429:
1426:
1425:
1423:
1421:
1420:
1415:
1408:
1405:
1402:
1399:
1397:
1394:
1392:
1391:Concurrent ML
1389:
1386:
1385:
1381:
1380:
1378:
1376:
1372:
1363:
1360:
1357:
1354:
1351:
1348:
1345:
1342:
1340:
1337:
1336:
1334:
1331:
1330:
1328:
1326:
1322:
1319:
1317:
1312:
1308:
1305:
1303:
1299:
1294:
1287:
1282:
1280:
1275:
1273:
1268:
1267:
1264:
1258:
1255:
1253:
1250:
1248:
1245:
1241:
1236:
1235:
1231:
1220:
1209:
1205:
1202:
1198:
1194:
1191:
1187:
1186:Tobias Nipkow
1183:
1180:
1176:
1172:
1168:
1164:
1161:
1160:
1146:
1140:
1126:
1122:
1118:
1114:
1107:
1099:
1092:
1084:
1069:
1062:
1055:
1054:
1049:
1043:
1036:
1033:
1029:
1023:
1021:
1019:
1011:
1010:
1005:
999:
985:on 2017-03-05
984:
980:
976:
975:"1.2 History"
969:
954:
947:
939:
935:
931:
927:
922:
917:
913:
909:
902:
898:
883:
855:
847:
813:
809:
799:
796:, written in
795:
792:
790:
786:
783:, written in
782:
779:
777:
774:, written in
773:
770:
768:
765:, written in
764:
761:
759:
756:, written in
755:
752:
750:
747:, written in
746:
743:
741:
738:, written in
737:
734:
732:
729:, written in
728:
725:
724:
723:
719:
709:
703:
699:
695:
694:
690:
686:
682:
678:
677:
676:
674:
670:
666:
662:
658:
654:
650:
645:
643:
639:
602:lowest_terms
468:"coprime m n"
423:
421:
418:in Isar that
417:
412:
409:
407:
403:
399:
395:
388:Example proof
385:
383:
379:
375:
371:
369:
365:
360:
358:
354:
351:generators):
350:
346:
342:
338:
334:
330:
326:
322:
318:
314:
310:
306:
303:engine and a
302:
297:
295:
291:
287:
283:
279:
275:
271:
261:
259:
255:
254:free software
250:
249:'s daughter.
248:
244:
239:
237:
233:
229:
225:
219:
217:
213:
209:
206:, written in
205:
201:
198:
188:
178:
174:
171:
168:
166:
162:
159:
156:
154:
150:
147:
143:
139:
136:
134:
130:
127:
123:
120:
116:
112:
96:
94:
90:
86:
82:
78:
74:
70:
67:
65:
61:
58:
55:
53:
49:
45:
39:
34:
19:
1779:
1769:
1759:
1749:
1737:
1732:
1729:
1679:Don Sannella
1673:Robin Milner
1667:Xavier Leroy
1587:
1576:
1535:SLAM project
1419:Dependent ML
1417:
1382:
1200:
1170:
1139:
1128:. Retrieved
1116:
1106:
1097:
1083:
1071:. Retrieved
1061:
1052:
1042:
1034:
1031:
1008:
998:
987:. Retrieved
983:the original
978:
968:
956:. Retrieved
946:
911:
907:
901:
854:
812:
763:Mizar system
721:
712:Alternatives
707:
704:in Isabelle.
646:
642:verification
635:
632:Applications
498:fastforce
431:"sqrt 2 ∉ ℚ"
413:
410:
391:
382:Mizar system
377:
373:
372:
363:
361:
356:
352:
340:
309:Sledgehammer
308:
298:
267:
251:
240:
236:Isabelle AFP
235:
231:
220:
196:
194:
64:Developer(s)
1661:Gérard Huet
1396:Extended ML
1375:Standard ML
1295:programming
1257:IsarMathLib
798:Standard ML
767:Free Pascal
700:was proven
689:microkernel
649:mathematics
564:"2 dvd n^2"
543:"m = 2 * k"
503:"2 dvd m^2"
398:declarative
294:unification
274:type theory
258:BSD license
247:Gérard Huet
208:Standard ML
170:BSD license
158:Mathematics
122:Standard ML
1796:Categories
1409:° (SML/NJ)
1130:2019-11-25
1073:22 October
989:2016-04-28
921:cs/9301104
893:References
702:type-sound
459:sqrt_rat:
394:procedural
321:resolution
290:resolution
270:meta-logic
118:Written in
1651:(Lazy ML)
1643:Designers
1635:Community
1569:HOL Light
1511:Marionnet
1179:0168-7433
1125:2150-914X
607:"2 dvd 1"
587:‹2 dvd m›
574:"2 dvd n"
569:simp
559:simp
533:‹2 dvd m›
523:"2 dvd n"
513:"2 dvd m"
347:finders (
284:(HOL) or
216:LCF-style
1685:Don Syme
1577:Isabelle
1476:Alt-Ergo
1316:dialects
1302:Software
938:27085090
772:Metamath
620:odd_one
447:"?x ∈ ℚ"
441:"sqrt 2"
396:and the
357:Nunchaku
272:(a weak
264:Features
214:. As an
197:Isabelle
181:isabelle
31:Isabelle
1730:Italics
1657:(OCaml)
1615:GeneWeb
1529:Semgrep
1499:Frama-C
1453:MacroML
1448:Lazy ML
1442:Futhark
1210:, 2020.
1192:, 1990.
781:Prover9
731:Haskell
655:, like
612:simp
579:simp
545:..
518:simp
508:simp
427:theorem
402:tactics
364:locales
353:Nitpick
337:Vampire
323:-based
280:(FOL),
176:Website
165:License
142:Windows
105:2024-05
103: (
1663:(Caml)
1595:Matita
1523:Poplog
1487:Camlp4
1482:Astrée
1362:Reason
1356:JoCaml
1177:
1123:
936:
789:Python
776:ANSI C
663:, the
624:blast
616:False
536:obtain
528:-
453:obtain
444:assume
335:, and
319:) and
245:after
75:et al.
1601:Twelf
1517:MTASC
1401:MLton
1384:Alice
1333:OCaml
1094:(PDF)
958:1 May
934:S2CID
916:arXiv
804:Notes
794:Twelf
740:OCaml
681:NICTA
618:using
561:hence
540:where
526:proof
510:hence
500:hence
492:using
485:hence
475:hence
457:where
439:?x =
434:proof
368:lemma
345:model
341:Metis
339:(the
333:SPASS
212:Scala
202:is a
146:macOS
138:Linux
126:Scala
44:macOS
1751:Book
1738:° =
1687:(F#)
1675:(ML)
1583:LEGO
1505:Haxe
1493:FFTW
1325:Caml
1175:ISSN
1121:ISSN
1075:2019
960:2021
754:LEGO
745:Lean
727:Agda
651:and
614:thus
604:have
600:with
590:have
584:with
571:thus
551:have
547:with
530:from
520:have
487:eq:
450:then
374:Isar
355:and
317:CVC4
210:and
195:The
185:.tum
153:Type
124:and
83:1986
71:and
1563:HOL
1557:Coq
1428:ATS
1339:Eff
926:doi
749:C++
736:Coq
626:qed
581:qed
549:eq
464:and
437:let
370:.
228:IDE
187:.de
183:.in
1798::
1565:°
1458:Ur
1350:F#
1344:F*
1335:°
1293:ML
1199:,
1188:,
1169:,
1165:,
1115:.
1096:.
1035:61
1030:,
1017:^
977:.
932:.
924:.
910:.
870:iː
687:)
685:L4
622:by
610:by
596:by
577:by
567:by
557:by
538:k
516:by
506:by
496:by
481:by
471:by
384:.
376:("
359:.
331:,
296:.
260:.
238:)
144:,
140:,
1617:°
1603:°
1597:°
1579:°
1571:°
1559:°
1546:,
1531:°
1525:°
1519:°
1513:°
1507:°
1501:°
1495:°
1489:°
1478:°
1460:°
1444:°
1430:°
1403:°
1387:°
1364:°
1358:°
1352:°
1346:°
1313:,
1285:e
1278:t
1271:v
1181:.
1147:.
1133:.
1077:.
992:.
962:.
940:.
928::
918::
912:3
882:/
879:s
876:ɪ
873:t
867:m
864:ˈ
861:/
846:/
843:l
840:ɛ
837:b
834:ˈ
831:ə
828:z
825:ɪ
822:ˌ
819:/
785:C
329:E
234:(
107:)
20:)
Text is available under the Creative Commons Attribution-ShareAlike License. Additional terms may apply.
