Quelle  AOT_keys.ML

val AOT_items = [
    (1, "simple-terms"),
    (2, "primitive-expressions"),
    (3, "syntax"),
    (4, "bnf"),
    (5, "conventions2"),
    (6, "df-subformula"),
    (7, "df-subterm"),
    (8, "enc-form-sub"),
    (9, "free-in"),
    (10, "open-formulas-terms"),
    (11, "closures"),
    (12, "term-same-type"),
    (13, "identity-remark"),
    (14, "substitutions"),
    (15, "substitutable"),
    (16, "alphabetic-variants"),
    (17, "two-defs"),
    (18, "conventions"),
    (19, "conventions3"),
    (20, "existence"),
    (21, "studied-amb"),
    (22, "oa"),
    (23, "identity"),
    (24, "=-infix"),
    (25, "lang-conc-rem"),
    (26, "alpha-bet-rem"),
    (27, "identity-pre"),
    (28, "identity-pre2"),
    (29, "convention-rem"),
    (30, "pre-exists"),
    (31, "exp-sub"),
    (32, "exp-sub2"),
    (33, "exist-just"),
    (34, "no-rel-prop"),
    (35, "identity-rem"),
    (36, "p-identity-rem"),
    (37, "p-identity2-rem"),
    (38, "pl"),
    (39, "cqt"),
    (40, "cqt-just"),
    (41, "l-identity"),
    (42, "m-fragile"),
    (43, "logic-actual"),
    (44, "logic-actual-nec"),
    (45, "qml"),
    (46, "qml-act"),
    (47, "descriptions"),
    (48, "lambda-predicates"),
    (49, "safe-ext"),
    (50, "nary-encoding"),
    (51, "encoding"),
    (52, "nocoder"),
    (53, "A-objects"),
    (54, "no-immediate-contra"),
    (55, "cqt-expl"),
    (56, "qml4-remark"),
    (57, "coexist-rm"),
    (58, "modus-ponens"),
    (59, "theoremhood"),
    (60, "Box-theoremhood"),
    (61, "metarules"),
    (62, "non-con-thm-thm"),
    (63, "vdash-properties"),
    (64, "df-noncon-thm"),
    (65, "dependence"),
    (66, "rule-gen"),
    (67, "rule-convention"),
    (68, "RN"),
    (69, "preserve-GEN-RN"),
    (70, "RN-w-cont"),
    (71, "RN-converse-rem"),
    (72, "df-rules-formulas"),
    (73, "df-rules-terms"),
    (74, "if-p-then-p"),
    (75, "deduction-theorem"),
    (76, "ded-thm-cor"),
    (77, "useful-tautologies"),
    (78, "dn-i-e"),
    (79, "modus-tollens"),
    (80, "contraposition"),
    (81, "reductio-aa"),
    (82, "in-el-i-e"),
    (83, "exc-mid"),
    (84, "non-contradiction"),
    (85, "con-dis-taut"),
    (86, "con-dis-i-e"),
    (87, "raa-cor"),
    (88, "oth-class-taut"),
    (89, "intro-elim"),
    (90, "rule-eq-df"),
    (91, "df-simplify"),
    (92, "remark-taut"),
    (93, "rule-ui"),
    (94, "misuse-substitution"),
    (95, "cqt-orig"),
    (96, "universal"),
    (97, "rereplace-lem"),
    (98, "rereplace-rmk"),
    (99, "cqt-basic"),
    (100, "universal-cor"),
    (101, "existential"),
    (102, "instantiation"),
    (103, "cqt-further"),
    (104, "log-prop-prop"),
    (105, "safe-ext-rem"),
    (106, "exist-nec"),
    (107, "t=t-proper"),
    (108, "id-rel-nec-equiv"),
    (109, "df-equiv-id"),
    (110, "rule=E"),
    (111, "propositions-lemma"),
    (112, "rem-truth"),
    (113, "remark-on-tautologies"),
    (114, "dr-alphabetic-rules"),
    (115, "oa-exist"),
    (116, "p-identity-thm2"),
    (117, "id-eq"),
    (118, "rule=I"),
    (119, "rule-id-df-rem"),
    (120, "rule-id-df"),
    (121, "free-thms"),
    (122, "free-thms-rem"),
    (123, "ex"),
    (124, "all-self="),
    (125, "id-nec"),
    (126, "term-out"),
    (127, "uniqueness"),
    (128, "uni-most"),
    (129, "nec-exist-!"),
    (130, "act-cond"),
    (131, "nec-imp-act"),
    (132, "act-conj-act"),
    (133, "closure-act"),
    (134, "RA"),
    (135, "meta-rule"),
    (136, "logic-actual-rem"),
    (137, "ANeg"),
    (138, "Act-Basic"),
    (139, "act-quant-uniq"),
    (140, "fund-cont-desc"),
    (141, "hintikka"),
    (142, "russell-axiom"),
    (143, "!-exists"),
    (144, "y-in"),
    (145, "act-quant-nec"),
    (146, "equi-desc-descA"),
    (147, "nec-hintikka-scheme"),
    (148, "equiv-desc-eq"),
    (149, "equiv-desc-eq2"),
    (150, "nec-russell-axiom"),
    (151, "actual-desc"),
    (152, "!box-desc"),
    (153, "dr-alphabetic-thm"),
    (154, "cqt-remark"),
    (155, "taut-nec"),
    (156, "RM"),
    (157, "KBasic"),
    (158, "rule-sub-lem"),
    (159, "rule-sub-nec"),
    (160, "rule-sub-remark"),
    (161, "KBasic2"),
    (162, "T-S5-fund"),
    (163, "Act-Sub"),
    (164, "S5Basic"),
    (165, "derived-S5-rules"),
    (166, "BFs"),
    (167, "sign-S5-thm"),
    (168, "exist-nec2"),
    (169, "id-nec2"),
    (170, "sc-eq-box-box"),
    (171, "west-mmrule"),
    (172, "sc-eq-fur"),
    (173, "id-act"),
    (174, "A-Exists"),
    (175, "id-act-desc"),
    (176, "pre-en-eq"),
    (177, "en-eq"),
    (178, "oa-facts"),
    (179, "beta-C-meta"),
    (180, "beta-free-rem"),
    (181, "beta-C-cor"),
    (182, "betaC"),
    (183, "eta-variants"),
    (184, "eta-conversion-lemma1"),
    (185, "eta-conversion-lemma2"),
    (186, "sub-des-lam"),
    (187, "prop-equiv"),
    (188, "prop-rem"),
    (189, "relations"),
    (190, "block-paradox"),
    (191, "block-paradox2"),
    (192, "propositions"),
    (193, "pos-not-equiv-ne"),
    (194, "df-relation-negation"),
    (195, "rel-neg-T"),
    (196, "df-rel-neg-rem"),
    (197, "thm-relation-negation"),
    (198, "contingent-properties"),
    (199, "cont-prop-rem"),
    (200, "thm-cont-prop"),
    (201, "thm-noncont-e-e"),
    (202, "lem-cont-e"),
    (203, "thm-cont-e"),
    (204, "property-facts"),
    (205, "thm-cont-propos"),
    (206, "thm-noncont-propos"),
    (207, "no-cnac"),
    (208, "pos-not-pna"),
    (209, "basic-prop"),
    (210, "proposition-facts"),
    (211, "cont-tf"),
    (212, "cont-true-cont"),
    (213, "q0cf"),
    (214, "q0cf-rem"),
    (215, "cont-tf-thm"),
    (216, "rem-conting"),
    (217, "property-facts1"),
    (218, "eq-not-nec"),
    (219, "eqnotnec"),
    (220, "oa-contingent"),
    (221, "df-cont-nec"),
    (222, "cont-nec-fact1"),
    (223, "cont-nec-fact2"),
    (224, "sixteen"),
    (225, "o-objects-exist"),
    (226, "partition"),
    (227, "=E"),
    (228, "=E-infix"),
    (229, "haecceity-expanded"),
    (230, "=E-simple"),
    (231, "id-nec3"),
    (232, "non-=E"),
    (233, "thm-neg=E"),
    (234, "id-nec4"),
    (235, "id-act2"),
    (236, "ord=Eequiv"),
    (237, "ord-=E="),
    (238, "ind-nec"),
    (239, "ord=E"),
    (240, "ord=E2"),
    (241, "ordnecfail"),
    (242, "ab-obey"),
    (243, "encoders-are-abstract"),
    (244, "denote="),
    (245, "denote=rem"),
    (246, "A-obj-ex"),
    (247, "A-objects!"),
    (248, "obj-oth"),
    (249, "A-descriptions"),
    (250, "can-ind"),
    (251, "thm-can-terms2"),
    (252, "can-ab2"),
    (253, "desc-encode"),
    (254, "abstraction-contingent"),
    (255, "desc-nec-encode"),
    (256, "Box-desc-encode"),
    (257, "strict-can"),
    (258, "box-phi-a"),
    (259, "strict-can-rem2"),
    (260, "df-null-uni"),
    (261, "null-uni-uniq"),
    (262, "df-null-uni-terms"),
    (263, "null-uni-facts"),
    (264, "null-uni-rmk2"),
    (265, "aclassical"),
    (266, "aclassical2"),
    (267, "kirchner-thm-rem"),
    (268, "kirchner-thm"),
    (269, "kirchner-thm-cor"),
    (270, "prop-prop1"),
    (271, "prop-prop2"),
    (272, "prop-indis"),
    (273, "prop-in-thm"),
    (274, "prop-in-f"),
    (275, "prop-prop-nec"),
    (276, "enc-prop-nec"),
    (277, "def-omit"),
    (278, "t-dfs"),
    (279, "df-fragile-axiom"),
    (280, "tvalues-remark"),
    (281, "tv-p"),
    (282, "tv-p-rem"),
    (283, "p-has-!tv"),
    (284, "uni-tv"),
    (285, "the-tv-p"),
    (286, "prop-enc"),
    (287, "tv-id"),
    (288, "not-can-thm"),
    (289, "t-prov-can"),
    (290, "T-lem"),
    (291, "ab-T"),
    (292, "TV-lem1"),
    (293, "T-value"),
    (294, "TVp-TV"),
    (295, "TV-lem2"),
    (296, "the-true"),
    (297, "T-T-value"),
    (298, "two-T"),
    (299, "valueof-facts"),
    (300, "q-True"),
    (301, "exten-p"),
    (302, "extof-e"),
    (303, "ext-p-tv"),
    (304, "set-remark"),
    (305, "tv-v-class"),
    (306, "naive-logical"),
    (307, "exten-property"),
    (308, "exten-remark"),
    (309, "pre-LawV"),
    (310, "unique-ext-of"),
    (311, "mat-eq-cont1"),
    (312, "membership"),
    (313, "in-no-col"),
    (314, "mem-exem"),
    (315, "fund-thm-class"),
    (316, "the-extG"),
    (317, "no-imprac"),
    (318, "extG-id"),
    (319, "mat-eq-cont2"),
    (320, "eG-not-sc"),
    (321, "ext-features"),
    (322, "lawV"),
    (323, "Frege-notation"),
    (324, "Frege-lawV"),
    (325, "no-lawV-pred"),
    (326, "frege-members"),
    (327, "mem-exem-cor"),
    (328, "extG-class"),
    (329, "eG-not-sc-rem"),
    (330, "res-var"),
    (331, "res-var-bound"),
    (332, "res-var-df"),
    (333, "res-var-term"),
    (334, "res-var-bound-reas"),
    (335, "res-var-free"),
    (336, "res-var-empty"),
    (337, "extensionality"),
    (338, "df-null"),
    (339, "null"),
    (340, "null-symbol"),
    (341, "null-exists"),
    (342, "df-universall"),
    (343, "universal-class"),
    (344, "df-unions"),
    (345, "unions"),
    (346, "unions2"),
    (347, "unions3"),
    (348, "unions-df"),
    (349, "unions-prin"),
    (350, "df-complements"),
    (351, "complements"),
    (352, "complements2"),
    (353, "df-intersections"),
    (354, "intersections"),
    (355, "intersections2"),
    (356, "intersect-df"),
    (357, "int-mem"),
    (358, "cond-set-comprehension"),
    (359, "res-meta"),
    (360, "set-comp-df"),
    (361, "t-defs4"),
    (362, "class-ab-prin"),
    (363, "class-ab-id"),
    (364, "separation"),
    (365, "separation2"),
    (366, "separation-ab"),
    (367, "sep-ab-prin"),
    (368, "ab-inter"),
    (369, "collection"),
    (370, "pre-singletons"),
    (371, "singletons"),
    (372, "single-df"),
    (373, "singleton-facts"),
    (374, "singleton-facts2"),
    (375, "pairs"),
    (376, "adjunction"),
    (377, "ex-anti-ext"),
    (378, "log-obj"),
    (379, "df-equiv-cond"),
    (380, "thm-equiv-cond"),
    (381, "notate-ab"),
    (382, "Frege-p"),
    (383, "axiom-lines"),
    (384, "lem-lines"),
    (385, "df-direction"),
    (386, "direct-line"),
    (387, "direct-line2"),
    (388, "direction-df"),
    (389, "para-dir"),
    (390, "directions"),
    (391, "exist-dir"),
    (392, "remark-shapes"),
    (393, "lem-shapes"),
    (394, "df-shape"),
    (395, "shape-figure"),
    (396, "shape-figure2"),
    (397, "shape-df"),
    (398, "shape-thm"),
    (399, "shapes2"),
    (400, "exist-shape"),
    (401, "equiv-rel"),
    (402, "R1"),
    (403, "equiv-rest"),
    (404, "lem-Rab"),
    (405, "df-ab"),
    (406, "ab-exists"),
    (407, "ab-exists2"),
    (408, "df-by-ab"),
    (409, "R-ab"),
    (410, "form-remark"),
    (411, "form-of"),
    (412, "forms-exist"),
    (413, "phi-G"),
    (414, "phiG-id"),
    (415, "phiG-sc"),
    (416, "TheFormGFormG"),
    (417, "pre-sp"),
    (418, "participation"),
    (419, "pre-OM-weak"),
    (420, "part=ex"),
    (421, "om"),
    (422, "counter-sp"),
    (423, "forms-encode"),
    (424, "sp-remark"),
    (425, "forms"),
    (426, "TheFormGForm"),
    (427, "rem-no-par"),
    (428, "platonic-being"),
    (429, "form-part"),
    (430, "third-man"),
    (431, "tforms-remark"),
    (432, "F-imp-G"),
    (433, "imp-facts"),
    (434, "tform-of"),
    (435, "tforms-exist"),
    (436, "tphi-G"),
    (437, "tphiG-id"),
    (438, "tphiG-sc"),
    (439, "tTheFormGFormG"),
    (440, "geach"),
    (441, "tparticipation"),
    (442, "tpre-OM-weak"),
    (443, "counter-tpre-rl"),
    (444, "tpart=ex"),
    (445, "tpta-ex"),
    (446, "tom"),
    (447, "tcounter-sp"),
    (448, "tforms-encode"),
    (449, "tforms"),
    (450, "tTheFormGForm"),
    (451, "SPa-b"),
    (452, "tpart-con"),
    (453, "tform-syl"),
    (454, "tforms-NI"),
    (455, "sit-remark"),
    (456, "situations"),
    (457, "T-sit"),
    (458, "possit-sit"),
    (459, "true-in-s"),
    (460, "lem1"),
    (461, "lem1-rem"),
    (462, "lem2"),
    (463, "sit-identity"),
    (464, "sit-part-whole"),
    (465, "part"),
    (466, "sit-identity2"),
    (467, "persistent"),
    (468, "pers-prop"),
    (469, "df-null-trivial"),
    (470, "thm-null-trivial"),
    (471, "df-the-null-sit"),
    (472, "null-triv-sc"),
    (473, "null-triv-facts"),
    (474, "cond-prop"),
    (475, "pre-comp-sit"),
    (476, "comp-sit"),
    (477, "can-sit-desc"),
    (478, "strict-sit"),
    (479, "strict-can-sit"),
    (480, "sit-lat"),
    (481, "actual"),
    (482, "act-and-not-pos"),
    (483, "actual-rem"),
    (484, "actual-s"),
    (485, "comp"),
    (486, "act-sit"),
    (487, "cons"),
    (488, "cons-remark"),
    (489, "sit-cons"),
    (490, "cons-rigid"),
    (491, "pos"),
    (492, "sit-pos"),
    (493, "pos-cons-sit"),
    (494, "sit-classical"),
    (495, "rem-pos-world"),
    (496, "world"),
    (497, "rigid-pw"),
    (498, "double-res"),
    (499, "true-w"),
    (500, "world-pos"),
    (501, "world-cons"),
    (502, "rigid-truth-at"),
    (503, "max"),
    (504, "world-max"),
    (505, "world=maxpos"),
    (506, "maxcon-rem"),
    (507, "nec-impl-p"),
    (508, "nec-equiv-nec-im"),
    (509, "world-closed-lem"),
    (510, "world-clo"),
    (511, "world-closed"),
    (512, "coherent"),
    (513, "coh-rem"),
    (514, "act-world"),
    (515, "remark-w-alpha"),
    (516, "pre-walpha"),
    (517, "w-alpha"),
    (518, "T-world"),
    (519, "truth-at-alpha"),
    (520, "alpha-world"),
    (521, "t-at-alpha-strict"),
    (522, "not-act"),
    (523, "w-alpha-part"),
    (524, "act-world2"),
    (525, "fund-lem"),
    (526, "fund"),
    (527, "nec-dia-w"),
    (528, "conj-dist-w"),
    (529, "Lew-world-con"),
    (530, "two-worlds-exist"),
    (531, "non-aw"),
    (532, "iterated-modalities"),
    (533, "world-equiv"),
    (534, "no-contradictions"),
    (535, "disj-dist-models"),
    (536, "world-skeptic"),
    (537, "tv-of-p-at-w"),
    (538, "unique-TV-w"),
    (539, "T-value-at-w"),
    (540, "TW-strict"),
    (541, "TheTrueAtW"),
    (542, "TW-rigid"),
    (543, "TW-Sigma"),
    (544, "cor-T-TV"),
    (545, "Boxp-TwT"),
    (546, "ext-at-w-F"),
    (547, "unique-ext-w"),
    (548, "ep-w-G"),
    (549, "eG-strict"),
    (550, "LawV-w"),
    (551, "rem-ext-w"),
    (552, "w-rel"),
    (553, "w-index"),
    (554, "df-rigid-rel"),
    (555, "rem-on-rigid"),
    (556, "rigid-der"),
    (557, "rigid-rel-thms"),
    (558, "w-ind-equiv"),
    (559, "rem-imp-w"),
    (560, "impwor"),
    (561, "iw-rigid"),
    (562, "iw-truth-at"),
    (563, "iw-id"),
    (564, "false-iw"),
    (565, "iw-notmc"),
    (566, "iw-p-ext"),
    (567, "iw-pext-lem"),
    (568, "iw-fund"),
    (569, "iw-ecq-no"),
    (570, "iw-ds"),
    (571, "rem-times"),
    (572, "fic-data"),
    (573, "fic-meth"),
    (574, "story"),
    (575, "story-exist"),
    (576, "story-remark"),
    (577, "stories-truth"),
    (578, "strict-char"),
    (579, "strict-pre"),
    (580, "s-en"),
    (581, "char"),
    (582, "nat-char"),
    (583, "nat-id"),
    (584, "fictional"),
    (585, "fictional-f"),
    (586, "tf-stories"),
    (587, "stories-apply1"),
    (588, "stories-apply2"),
    (589, "stories-apply3"),
    (590, "fur-con"),
    (591, "pos-fic"),
    (592, "leibniz-strands"),
    (593, "concepts"),
    (594, "con=ab"),
    (595, "concept-comp"),
    (596, "con-res-x"),
    (597, "c-id"),
    (598, "sum-pre-def"),
    (599, "sum-exists"),
    (600, "sum-def"),
    (601, "sum-lemma"),
    (602, "oplus"),
    (603, "sum-property"),
    (604, "cid-add"),
    (605, "con"),
    (606, "con-part"),
    (607, "con-id"),
    (608, "ic-add"),
    (609, "def-ded"),
    (610, "fund-leib"),
    (611, "leib-23"),
    (612, "prod-pre-def"),
    (613, "product-exists"),
    (614, "prod-def"),
    (615, "prod-lemma"),
    (616, "otimes"),
    (617, "absorption"),
    (618, "bd-lattice"),
    (619, "boolean-rem1"),
    (620, "distrib"),
    (621, "comple-df"),
    (622, "comple-exist"),
    (623, "comple-def"),
    (624, "comple-lemma"),
    (625, "comple-laws"),
    (626, "post-boole"),
    (627, "concept-sub"),
    (628, "ex-mereology"),
    (629, "part-of-c"),
    (630, "ppart-of-c"),
    (631, "ppart-ax"),
    (632, "null-concept"),
    (633, "null-facts"),
    (634, "mereo-overlap"),
    (635, "overlap-thms"),
    (636, "mer-sup"),
    (637, "underlap"),
    (638, "a-underlap"),
    (639, "dodge"),
    (640, "nnc"),
    (641, "nnc-rigid"),
    (642, "df-bottom+"),
    (643, "no-bottom"),
    (644, "df-atom+"),
    (645, "atom-part"),
    (646, "o-o"),
    (647, "nover-rem"),
    (648, "noverlap-facts"),
    (649, "newsup"),
    (650, "ndf-ex"),
    (651, "concept-of-G"),
    (652, "con-exists"),
    (653, "concept-G"),
    (654, "conG-strict"),
    (655, "conG-lemma"),
    (656, "sum3"),
    (657, "gen-inc"),
    (658, "concepts-not-properties"),
    (659, "form=con"),
    (660, "con-of-u"),
    (661, "con-u-exist"),
    (662, "concept-u"),
    (663, "Fu-cont"),
    (664, "con-u-not-strict"),
    (665, "c-uF-Fu"),
    (666, "c-uF-Fu2"),
    (667, "complete"),
    (668, "con-of-u-com"),
    (669, "restrict-concepts"),
    (670, "con-gen"),
    (671, "c-allGF-allGisF"),
    (672, "c-allGF-allGisF2"),
    (673, "fa-c-af"),
    (674, "contain-truth"),
    (675, "montague-gq"),
    (676, "con-nec"),
    (677, "no-counterpart-theory"),
    (678, "cor"),
    (679, "cor-rem"),
    (680, "real-at-facts"),
    (681, "appears-at"),
    (682, "appear-fact"),
    (683, "appear-co"),
    (684, "mirror"),
    (685, "appear-mir"),
    (686, "new-appear-fact"),
    (687, "box-appears"),
    (688, "new-real-at-fact"),
    (689, "lem-con-u"),
    (690, "ind-con"),
    (691, "concept-u-ind-con"),
    (692, "concept-u-ind-con-a"),
    (693, "ind-con-rigid"),
    (694, "ind-con-appear"),
    (695, "w-c"),
    (696, "w-c-applies"),
    (697, "ind-con-cont-c-F"),
    (698, "con-non-G"),
    (699, "con-comp"),
    (700, "compos"),
    (701, "comp-w-c"),
    (702, "compos-eq"),
    (703, "df-con-u-at-w"),
    (704, "con-u-w-exist"),
    (705, "con-u-at-w"),
    (706, "con-u-strict"),
    (707, "lem-con-u-at"),
    (708, "ind-con-iff-c-w-u"),
    (709, "lem-con-u-alpha"),
    (710, "lem-con-u-at-w"),
    (711, "con-u-at-comp"),
    (712, "rem-con-u-at-w"),
    (713, "concepts-not-properties2"),
    (714, "counterparts"),
    (715, "count-part-con"),
    (716, "count-cor"),
    (717, "con-u-at-w-count"),
    (718, "fund-thm-modal-meta"),
    (719, "fund-thm-modal-bi"),
    (720, "fund-thm-modal-strict"),
    (721, "fund-thm-mod-rem"),
    (722, "Dedekind-Peano"),
    (723, "1-1-cor"),
    (724, "1-1-cor-rem"),
    (725, "fFG"),
    (726, "eq-1-1"),
    (727, "frege-theorem"),
    (728, "why-EqE"),
    (729, "equi"),
    (730, "eq-part"),
    (731, "equi-rem"),
    (732, "equi-rem-thm"),
    (733, "empty-approx"),
    (734, "F-u"),
    (735, "eqP'"),
    (736, "P'-eq"),
    (737, "approx-cont"),
    (738, "eqE"),
    (739, "apE-eqE"),
    (740, "eq-part-act"),
    (741, "actuallyF"),
    (742, "approx-nec"),
    (743, "pre-number"),
    (744, "numbers"),
    (745, "num-tran"),
    (746, "pre-Hume"),
    (747, "num-tran-rem"),
    (748, "two-num-not"),
    (749, "num"),
    (750, "num-cont"),
    (751, "num-uniq"),
    (752, "num-def"),
    (753, "num-can"),
    (754, "numG-not-strict"),
    (755, "card"),
    (756, "natcard-nec"),
    (757, "hume"),
    (758, "hume-strict"),
    (759, "unotEu"),
    (760, "zero"),
    (761, "zero-card"),
    (762, "eq-num"),
    (763, "eq-df-num"),
    (764, "card-en"),
    (765, "0F"),
    (766, "zero="),
    (767, "hered"),
    (768, "ances-df"),
    (769, "ances"),
    (770, "anc-her"),
    (771, "rem-pre-wances"),
    (772, "df-1-1"),
    (773, "id-d-R"),
    (774, "id-R-thm"),
    (775, "w-ances-df"),
    (776, "w-ances"),
    (777, "wances-her"),
    (778, "1-1-R"),
    (779, "pre-ind"),
    (780, "pre-ind-rem"),
    (781, "pred-rem"),
    (782, "pred"),
    (783, "pred-thm"),
    (784, "pred-1-1"),
    (785, "assume-anc"),
    (786, "no-pred-0"),
    (787, "assume1"),
    (788, "nnumber"),
    (789, "0-n"),
    (790, "mod-col-num"),
    (791, "0-pred"),
    (792, "no-same-succ"),
    (793, "induction"),
    (794, "suc-num"),
    (795, "pred-num"),
    (796, "nat-card"),
    (797, "pred-func"),
    (798, "modal-axiom"),
    (799, "modal-just"),
    (800, "modal-lemma"),
    (801, "th-succ"),
    (802, "Frege's-proof"),
    (803, "non-classical"),
    (804, "def-suc"),
    (805, "suc-fact"),
    (806, "ind-gnd"),
    (807, "suc-thm"),
    (808, "numerals"),
    (809, "prec-facts"),
    (810, "num-num"),
    (811, "dig-alt"),
    (812, "rigid-restrict"),
    (813, "lt-gt"),
    (814, "lt-basic"),
    (815, "lt-conv"),
    (816, "lt-trans"),
    (817, "0lt1"),
    (818, "num-ord-lt"),
    (819, "remQuine"),
    (820, "no-num-pred"),
    (821, "dot-id-lem"),
    (822, "dot-id"),
    (823, "dot=eq="),
    (824, "integer"),
    (825, "1-pi"),
    (826, "i-prec"),
    (827, "n-n-lemma"),
    (828, "num-quant"),
    (829, "n-n"),
    (830, "num-quant-gen"),
    (831, "Functions"),
    (832, "total-D"),
    (833, "I-thm"),
    (834, "func-ex-pre"),
    (835, "func-ex"),
    (836, "func-nec"),
    (837, "fun-not-nec"),
    (838, "fcn-res-rem"),
    (839, "df-fa"),
    (840, "func-thm"),
    (841, "eq-func-nec"),
    (842, "func-rem"),
    (843, "func-obs"),
    (844, "function-rem"),
    (845, "fmaps-r"),
    (846, "fcn-from-ex"),
    (847, "fcn-from-ex2"),
    (848, "Rmap-res"),
    (849, "fcnal-from"),
    (850, "fcnl-from-ex"),
    (851, "fcnl-from-ex2"),
    (852, "fcnl-on"),
    (853, "fcnl-on-thm"),
    (854, "dom-ra"),
    (855, "df-dom"),
    (856, "fcn-from-re"),
    (857, "fcn-from"),
    (858, "fcn-sum"),
    (859, "mapping-ex"),
    (860, "dom-thm"),
    (861, "codom-thm"),
    (862, "range-thm"),
    (863, "allf-do"),
    (864, "R-gen-1-o"),
    (865, "ra-onto"),
    (866, "carProd"),
    (867, "restricted-f"),
    (868, "rf-fact"),
    (869, "rfun-exist"),
    (870, "res-fn-ex"),
    (871, "null-fn-fact"),
    (872, "res-fn-df"),
    (873, "res-fn-fact"),
    (874, "func-rest-var"),
    (875, "fcn-app-pre"),
    (876, "fcn-app-redef"),
    (877, "n-ary-op"),
    (878, "n-ary-op-rigid"),
    (879, "op-lem0"),
    (880, "con-fun"),
    (881, "proj-fun"),
    (882, "op-lem1"),
    (883, "pre-comp"),
    (884, "op-comp"),
    (885, "op-rest-var"),
    (886, "recursive"),
    (887, "recur-dig"),
    (888, "def-rel-add"),
    (889, "rec-df-add"),
    (890, "gen-recur-df"),
    (891, "gen-rec-R"),
    (892, "base-rec-thm"),
    (893, "gen-gen-rec"),
    (894, "gen-rec-thm"),
    (895, "trad-recurs-dfs"),
    (896, "prim-gen-recur"),
    (897, "minimize"),
    (898, "2ndPA-inter"),
    (899, "2ndPA-der"),
    (900, "multi-ord"),
    (901, "inf-card"),
    (902, "inf-card-exist"),
    (903, "df-infty"),
    (904, "infty-thms"),
    (905, "inf-just"),
    (906, "inf-set"),
    (907, "inf-set-exist")
]