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") ]