val AOT_items = [ (7, "chapLanguage"), (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"), (79, "fn-functional-term"), (12, "term-same-type"), (13, "identity-sym-remark"), (14, "substitutions"), (15, "substitutable"), (16, "alphabetic-variants"), (17, "two-defs"), (85, "fn-defs"), (86, "fn-exp-sub"), (87, "fn-exp-sub2"), (18, "conventions"), (19, "conventions3"), (20, "existence"), (21, "studied-amb"), (92, "fnQuinecorner"), (22, "oa"), (23, "identity"), (94, "fn-prf-oa"), (24, "=-infix"), (25, "lang-conc-rem"), (26, "alpha-bet-rem"), (27, "identity-pre"), (102, "fn-prov-false"), (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"), (109, "fn-preview-pf"), (36, "p-identity-rem"), (37, "p-identity2-rem"), (112, "fnRigEnc"), (8, "chapAxioms"), (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"), (120, "fn-lam-sub-term"), (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"), (9, "chapTheorems"), (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"), (132, "fn-s-wRN"), (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"), (137, "fn-cond-df"), (76, "ded-thm-cor"), (139, "fn-var-der"), (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"), (144, "fnOppZal2011"), (106, "exist-nec"), (107, "t=t-proper"), (108, "id-rel-nec-equiv"), (109, "df-equiv-id"), (110, "rule=E"), (146, "fn-type-only"), (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"), (151, "fn-log-act-rl"), (135, "RA"), (136, "meta-rule"), (153, "fn-just-RA"), (155, "fn-ruleRA-alt"), (156, "fn-act-two"), (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, "property-facts"), (207, "thm-cont-propos"), (208, "thm-noncont-propos"), (209, "no-cnac"), (210, "pos-not-pna"), (211, "basic-prop"), (212, "proposition-facts"), (213, "cont-tf"), (214, "cont-true-cont"), (215, "q0cf"), (216, "q0cf-rem"), (217, "cont-tf-thm"), (218, "rem-conting"), (219, "property-facts1"), (220, "eq-not-nec"), (221, "eqnotnec"), (222, "oa-contingent"), (223, "df-cont-nec"), (224, "cont-nec-fact1"), (225, "cont-nec-fact2"), (226, "sixteen"), (227, "o-objects-exist"), (228, "partition"), (229, "=E-definiens"), (230, "=E"), (231, "=E-infix"), (232, "haecceity-expanded"), (233, "=E-simple"), (234, "id-nec3"), (235, "non-=E"), (236, "thm-neg=E"), (237, "id-nec4"), (238, "id-act2"), (239, "ord=Eequiv"), (240, "ord-=E="), (241, "ind-nec"), (242, "ord=E"), (243, "ord=E2"), (244, "ordnecfail"), (245, "ab-obey"), (246, "encoders-are-abstract"), (247, "denote="), (248, "denote=rem"), (249, "A-obj-ex"), (250, "A-objects!"), (251, "obj-oth"), (252, "A-descriptions"), (253, "can-ind"), (254, "thm-can-terms2"), (255, "can-ab2"), (256, "desc-encode"), (257, "abstraction-contingent"), (173, "fn-form-mode"), (258, "desc-nec-encode"), (259, "Box-desc-encode"), (260, "strict-can"), (261, "box-phi-a"), (262, "strict-can-rem2"), (263, "df-null-uni"), (264, "null-uni-uniq"), (265, "df-null-uni-terms"), (266, "null-uni-facts"), (267, "null-uni-rmk2"), (268, "aclassical"), (269, "aclassical2"), (177, "fnAczel-mod"), (270, "kirchner-thm-rem"), (271, "kirchner-thm"), (272, "kirchner-thm-cor"), (273, "discern-obj"), (274, "disc-obj-rem"), (275, "prop-prop1"), (276, "prop-prop2"), (277, "prop-indis"), (278, "prop-in-thm"), (279, "prop-in-f"), (280, "prop-prop-nec"), (281, "enc-prop-nec"), (282, "def-omit"), (185, "fn-delta-down"), (283, "t-dfs"), (284, "df-fragile-axiom"), (10, "chapLogicalObjects"), (285, "tvalues-remark"), (286, "tv-p"), (287, "tv-p-rem"), (288, "p-has-!tv"), (289, "TV-lem1"), (290, "T-value"), (291, "TV-lem2"), (292, "two-T"), (293, "uni-tv"), (294, "the-tv-p"), (295, "prop-enc"), (296, "tv-id"), (297, "not-can-thm"), (298, "t-prov-can"), (299, "T-lem"), (300, "ab-T"), (301, "TVp-TV"), (302, "the-true"), (197, "fn-sol-circ-p"), (303, "T-T-value"), (304, "valueof-facts"), (305, "q-True"), (306, "exten-p"), (307, "extof-e"), (308, "ext-p-tv"), (309, "set-remark"), (310, "tv-v-class"), (311, "naive-logical"), (312, "exten-property"), (313, "exten-remark"), (314, "pre-LawV"), (315, "unique-ext-of"), (316, "membership"), (317, "mem-exem"), (318, "fund-thm-class"), (319, "non-well-found"), (320, "mat-eq-cont1"), (321, "in-no-col"), (322, "the-extG"), (323, "no-imprac"), (324, "extG-id"), (325, "mat-eq-cont2"), (326, "eG-not-sc"), (327, "ext-features"), (328, "lawV"), (329, "Frege-notation"), (330, "Frege-lawV"), (331, "no-lawV-pred"), (212, "fn-var-bin-subt"), (332, "frege-members"), (333, "mem-exem-cor"), (334, "extG-class"), (335, "eG-not-sc-rem"), (336, "res-var"), (337, "res-var-bound"), (216, "fn-ex-res"), (338, "res-var-df"), (218, "fn-free-res-var-def"), (339, "res-var-term"), (340, "res-var-bound-reas"), (228, "fn-res-var-qucom"), (231, "fnA-all-com"), (341, "res-var-free"), (234, "fn-conj-int"), (342, "res-var-empty"), (343, "extensionality"), (344, "df-null"), (345, "null"), (346, "null-symbol"), (347, "null-exists"), (348, "df-universall"), (349, "universal-class"), (350, "df-unions"), (351, "unions"), (352, "unions2"), (353, "unions3"), (354, "unions-df"), (355, "unions-prin"), (356, "df-complements"), (357, "complements"), (358, "complements2"), (359, "df-intersections"), (360, "intersections"), (361, "intersections2"), (362, "intersect-df"), (363, "int-mem"), (364, "cond-set-comprehension"), (365, "res-meta"), (366, "set-comp-df"), (367, "t-defs4"), (368, "class-ab-prin"), (369, "class-ab-id"), (370, "separation"), (371, "separation2"), (372, "separation-ab"), (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"), (246, "fn-line-not-rigid"), (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"), (11, "chapForms"), (420, "form-remark"), (251, "fn-geach-note"), (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"), (12, "chapWorlds"), (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, "actual"), (492, "act-and-not-pos"), (493, "actual-rem"), (494, "actual-s"), (495, "comp"), (496, "act-sit"), (497, "cons"), (498, "cons-remark"), (499, "sit-cons"), (500, "cons-rigid"), (501, "pos"), (502, "sit-pos"), (503, "incomp-sit"), (504, "incomp-cons"), (505, "routley-star"), (506, "routley-star-rem"), (507, "hype"), (508, "routley-star-hype"), (509, "rem-pos-world"), (510, "sit-classical"), (284, "fntypeproviso"), (286, "fnPhi-not-p"), (511, "world"), (512, "rigid-pw"), (513, "double-res"), (514, "true-w"), (515, "world-identity"), (516, "world-pos"), (517, "world-cons"), (518, "rigid-truth-at"), (519, "max"), (520, "world-max"), (521, "world=maxpos"), (522, "maxcon-rem"), (523, "w-star-w"), (524, "nec-impl-p"), (525, "nec-equiv-nec-im"), (526, "world-closed-lem"), (527, "world-clo"), (528, "world-closed"), (529, "coherent"), (530, "coh-rem"), (531, "act-world"), (532, "remark-w-alpha"), (533, "pre-walpha"), (534, "w-alpha"), (535, "T-world"), (536, "truth-at-alpha"), (537, "alpha-world"), (538, "t-at-alpha-strict"), (539, "not-act"), (540, "w-alpha-part"), (541, "act-world2"), (542, "fund-lem"), (543, "fund"), (544, "nec-dia-w"), (545, "conj-dist-w"), (546, "Lew-world-con"), (291, "fn-proof-conj-dist-w-8"), (547, "two-worlds-exist"), (548, "non-aw"), (549, "Kaplan-axiom"), (550, "iterated-modalities"), (551, "world-equiv"), (552, "no-contradictions"), (553, "disj-dist-models"), (554, "world-skeptic"), (555, "tv-at-w-of-p"), (556, "unique-TV-w"), (557, "T-value-at-w"), (558, "TW-strict"), (559, "TheTrueAtW"), (560, "TW-rigid"), (561, "cor-T-TV"), (562, "Boxp-TwT"), (563, "ext-at-w-F"), (564, "unique-ext-w"), (565, "ep-w-G"), (566, "eG-strict"), (567, "LawV-w"), (568, "rem-ext-w"), (569, "w-rel"), (299, "fn-rel-w"), (570, "w-index"), (571, "df-rigid-rel"), (572, "rem-on-rigid"), (573, "rigid-der"), (302, "fn-rel-w2"), (574, "rigid-rel-thms"), (575, "w-ind-equiv"), (576, "rem-imp-w"), (577, "impwor"), (578, "iw-rigid"), (579, "iw-truth-at"), (580, "iw-id"), (581, "false-iw"), (582, "iw-notmc"), (583, "iw-p-ext"), (584, "iw-pext-lem"), (585, "iw-fund"), (586, "iw-ecq-no"), (309, "fn-iw-correct"), (587, "iw-ds"), (588, "rem-times"), (589, "tense-simple"), (590, "fic-data"), (591, "fic-meth"), (592, "story"), (593, "story-exist"), (594, "story-remark"), (595, "stories-truth"), (596, "strict-char"), (324, "fn-exp-pow"), (597, "s-en"), (598, "char"), (599, "nat-char"), (600, "nat-id"), (325, "fn-fic-ind"), (601, "fictional"), (602, "fictional-f"), (603, "fict-ab"), (604, "tf-stories"), (605, "stories-apply1"), (606, "stories-apply2"), (607, "stories-apply3"), (608, "fur-con"), (609, "pos-fic1"), (610, "pos-fic2"), (13, "chapConcepts"), (611, "leibniz-strands"), (612, "concepts"), (613, "con=ab"), (614, "concept-comp"), (615, "con-res-x"), (616, "c-id"), (617, "sum-pre-def"), (618, "sum-exists"), (619, "sum-def"), (620, "sum-lemma"), (621, "oplus"), (622, "sum-property"), (623, "cid-add"), (624, "con"), (625, "con-part"), (333, "fn-df-isin"), (626, "con-id"), (627, "ic-add"), (628, "def-ded"), (629, "fund-leib"), (630, "leib-23"), (631, "prod-pre-def"), (632, "product-exists"), (633, "prod-def"), (634, "prod-lemma"), (635, "otimes"), (636, "absorption"), (637, "bd-lattice"), (638, "boolean-rem1"), (639, "distrib"), (640, "comple-df"), (641, "comple-exist"), (642, "comple-def"), (643, "comple-lemma"), (644, "comple-laws"), (645, "post-boole"), (646, "concept-sub"), (647, "ex-mereology"), (648, "part-of-c"), (649, "ppart-of-c"), (650, "ppart-ax"), (651, "null-concept"), (652, "null-facts"), (653, "mereo-overlap"), (654, "overlap-thms"), (655, "mer-sup"), (656, "underlap"), (657, "a-underlap"), (340, "fn-underlap"), (658, "dodge"), (659, "nnc"), (660, "nnc-rigid"), (661, "df-bottom+"), (662, "no-bottom"), (663, "df-atom+"), (664, "atom-part"), (665, "o-o"), (666, "nover-rem"), (667, "noverlap-facts"), (668, "newsup"), (669, "ndf-ex"), (670, "concept-of-G"), (671, "con-exists"), (672, "concept-G"), (673, "form=con"), (674, "conG-strict"), (675, "conG-lemma"), (676, "sum3"), (677, "gen-inc"), (678, "concepts-not-properties"), (343, "fn-c-R-c-P"), (679, "restrict-concepts"), (680, "con-of-u"), (681, "con-u-exist"), (344, "fnConOfU"), (682, "concept-u"), (683, "Fu-cont"), (684, "con-u-not-strict"), (685, "c-uF-Fu"), (686, "c-uF-Fu2"), (687, "complete"), (688, "con-of-u-com"), (689, "con-gen"), (690, "c-allGF-allGisF"), (691, "c-allGF-allGisF2"), (692, "fa-c-af"), (693, "contain-truth"), (694, "montague-gq"), (695, "con-nec"), (696, "no-counterpart-theory"), (697, "cor"), (698, "cor-rem"), (699, "real-at-facts"), (700, "appears-at"), (701, "appear-fact"), (702, "appear-co"), (703, "mirror"), (704, "appear-mir"), (705, "new-appear-fact"), (706, "box-appears"), (707, "new-real-at-fact"), (708, "lem-con-u"), (709, "ind-con"), (710, "concept-u-ind-con"), (711, "concept-u-ind-con-a"), (712, "ind-con-rigid"), (713, "ind-con-appear"), (714, "w-c"), (715, "w-c-applies"), (716, "ind-con-cont-c-F"), (717, "con-non-G"), (718, "con-comp"), (719, "compos"), (720, "comp-w-c"), (721, "compos-eq"), (722, "counterparts"), (723, "count-part-con"), (724, "count-cor"), (725, "df-con-u-at-w"), (726, "con-u-w-exist"), (727, "con-u-at-w"), (728, "con-u-strict"), (729, "lem-con-u-at"), (730, "ind-con-iff-c-w-u"), (731, "lem-con-u-alpha"), (732, "lem-con-u-at-w"), (733, "con-u-at-comp"), (734, "rem-con-u-at-w"), (735, "concepts-not-properties2"), (736, "fund-thm-modal-meta"), (737, "fund-thm-modal-bi"), (738, "fund-thm-modal-strict"), (739, "fund-thm-mod-rem"), (14, "chapNumbers"), (740, "Dedekind-Peano"), (741, "1-1-cor"), (742, "1-1-cor-rem"), (743, "fFG"), (360, "fn-maps"), (744, "eq-1-1"), (745, "frege-theorem"), (362, "fn-1893df"), (746, "why-EqE"), (747, "equi"), (748, "eq-part"), (749, "equi-rem"), (750, "equi-rem-thm"), (751, "empty-approx"), (752, "F-u"), (753, "eqP'"), (754, "P'-eq"), (755, "approx-cont"), (756, "eqE"), (757, "apE-eqE"), (758, "eq-part-act"), (759, "actuallyF"), (760, "approx-nec"), (761, "pre-number"), (762, "numbers"), (763, "num"), (764, "num-tran"), (765, "pre-Hume"), (766, "num-tran2"), (767, "num-tran-rem"), (768, "two-num-not"), (769, "num-cont"), (770, "num-uniq"), (771, "num-def"), (772, "num-can"), (773, "numG-not-strict"), (774, "eq-num"), (775, "hume-strict"), (776, "hume"), (777, "card"), (778, "eq-df-num"), (779, "natcard-nec"), (780, "card-en"), (781, "unotEu"), (782, "zero"), (783, "zero-card"), (784, "0F"), (785, "zero="), (786, "hered"), (787, "ances-df"), (788, "ances"), (789, "anc-her"), (790, "rem-pre-wances"), (791, "df-rel-dis"), (792, "rem-rigid-D"), (793, "w-ances-df"), (794, "w-ances"), (795, "wances-her"), (796, "1-1-R"), (797, "pre-ind"), (798, "pre-ind-rem"), (799, "pred-rem"), (800, "pred"), (801, "pred-thm"), (802, "pred-1-1"), (803, "pred-rel-disc"), (804, "assume-anc"), (805, "no-pred-0"), (806, "assume1"), (807, "nnumber"), (808, "0-n"), (809, "mod-col-num"), (810, "0-pred"), (811, "no-same-succ"), (812, "induction"), (813, "nat-card"), (814, "suc-num"), (815, "pred-num"), (816, "pred-func"), (817, "th-succ-lem"), (818, "th-succ"), (819, "Freges-proof"), (820, "non-classical"), (821, "def-suc"), (822, "suc-fact"), (823, "ind-gnd"), (824, "suc-thm"), (825, "numerals"), (826, "prec-facts"), (827, "num-num"), (828, "dig-alt"), (829, "rigid-restrict"), (830, "lt-gt"), (831, "lt-basic"), (832, "lt-conv"), (833, "lt-trans"), (834, "0lt1"), (835, "num-le"), (836, "num-ord-lt"), (837, "remQuine"), (838, "no-num-pred"), (839, "dot-id"), (840, "dot=eq="), (841, "integer"), (842, "1-pi"), (843, "i-prec"), (844, "n-n-lemma"), (845, "num-quant"), (846, "n-n"), (847, "num-quant-gen"), (848, "Functions"), (849, "total-D"), (850, "I-thm"), (851, "func-ex-pre"), (852, "func-ex"), (853, "func-nec"), (854, "fun-not-nec"), (855, "fcn-res-rem"), (856, "df-fa"), (857, "func-thm"), (858, "eq-func-nec"), (859, "func-rem"), (860, "func-obs"), (861, "function-rem"), (862, "fmaps-r"), (863, "fcn-from-ex"), (864, "fcn-from-ex2"), (865, "Rmap-res"), (866, "fcnal-from"), (867, "fcnl-from-ex"), (868, "fcnl-from-ex2"), (869, "fcnl-on"), (870, "fcnl-on-thm"), (871, "dom-ra"), (872, "df-dom"), (873, "fcn-from-re"), (874, "fcn-from"), (875, "fcn-sum"), (876, "mapping-ex"), (877, "dom-thm"), (878, "codom-thm"), (879, "range-thm"), (880, "allf-do"), (881, "R-gen-1-o"), (882, "ra-onto"), (883, "carProd"), (884, "restricted-f"), (885, "rf-fact"), (886, "rfun-exist"), (887, "res-fn-ex"), (888, "null-fn-fact"), (889, "res-fn-df"), (890, "res-fn-fact"), (891, "func-rest-var"), (892, "fcn-app-pre"), (893, "fcn-app-redef"), (894, "n-ary-op"), (895, "n-ary-op-rigid"), (896, "op-lem0"), (897, "con-fun"), (898, "proj-fun"), (899, "op-lem1"), (900, "pre-comp"), (901, "op-comp"), (902, "op-rest-var"), (903, "recursive"), (904, "recur-dig"), (905, "def-rel-add"), (906, "rec-df-add"), (907, "gen-recur-df"), (908, "gen-rec-R"), (909, "base-rec-thm"), (910, "gen-gen-rec"), (911, "gen-rec-thm"), (912, "trad-recurs-dfs"), (913, "prim-gen-recur"), (914, "minimize"), (915, "2ndPA-inter"), (916, "2ndPA-der"), (917, "inf-card"), (918, "inf-card-exist"), (919, "df-infty"), (920, "infty-thms"), (921, "inf-just"), (922, "inf-set"), (923, "inf-set-exist") ]