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