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