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