File ‹AOT_keys.ML›
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")
]