definition
- sttfa:natural__dest__def/type_0.def
- sttfa:natural__dest__def/type_1.def
- sttfa:natural__dest__def/type_2.def
- sttfa:natural__dest__def/term_0.def
- sttfa:natural__dest__def/Number_2ENatural_2Enatural.def
- sttfa:natural__dest__def/type_3.def
- sttfa:natural__dest__def/type_4.def
- sttfa:natural__dest__def/type_5.def
- sttfa:natural__dest__def/term_1.def
- sttfa:natural__dest__def/type_6.def
- sttfa:natural__dest__def/type_7.def
- sttfa:natural__dest__def/type_8.def
- sttfa:natural__dest__def/term_2.def
- sttfa:natural__dest__def/Data_2EPair_2E_2A.def
- sttfa:natural__dest__def/type_9.def
- sttfa:natural__dest__def/type_10.def
- sttfa:natural__dest__def/type_11.def
- sttfa:natural__dest__def/type_12.def
- sttfa:natural__dest__def/type_13.def
- sttfa:natural__dest__def/term_3.def
- sttfa:natural__dest__def/type_14.def
- sttfa:natural__dest__def/type_15.def
- sttfa:natural__dest__def/term_4.def
- sttfa:natural__dest__def/term_5.def
- sttfa:natural__dest__def/term_6.def
- sttfa:natural__dest__def/term_7.def
- sttfa:natural__dest__def/HOLLight_2ENUMERAL.def
- sttfa:natural__dest__def/term_8.def
- sttfa:natural__dest__def/Number_2ENatural_2Ezero.def
- sttfa:natural__dest__def/term_9.def
- sttfa:natural__dest__def/term_10.def
- sttfa:natural__dest__def/term_11.def
- sttfa:natural__dest__def/term_12.def
- sttfa:natural__dest__def/term_13.def
- sttfa:natural__dest__def/term_14.def
- sttfa:natural__dest__def/type_16.def
- sttfa:natural__dest__def/term_15.def
- sttfa:natural__dest__def/Number_2ENatural_2Esuc.def
- sttfa:natural__dest__def/term_16.def
- sttfa:natural__dest__def/term_17.def
- sttfa:natural__dest__def/term_18.def
- sttfa:natural__dest__def/term_19.def
- sttfa:natural__dest__def/term_20.def
- sttfa:natural__dest__def/term_21.def
- sttfa:natural__dest__def/term_22.def
- sttfa:natural__dest__def/term_23.def
- sttfa:natural__dest__def/term_24.def
- sttfa:natural__dest__def/term_25.def
- sttfa:natural__dest__def/term_26.def
- sttfa:natural__dest__def/term_27.def
- sttfa:natural__dest__def/term_28.def
- sttfa:natural__dest__def/type_17.def
- sttfa:natural__dest__def/type_18.def
- sttfa:natural__dest__def/Data_2EPair_2E_2C.def
- sttfa:natural__dest__def/term_29.def
- sttfa:natural__dest__def/Number_2ENatural_2Ebit0.def
- sttfa:natural__dest__def/term_30.def
- sttfa:natural__dest__def/Number_2ENatural_2Ebit1.def
- sttfa:natural__dest__def/term_31.def
- sttfa:natural__dest__def/term_32.def
- sttfa:natural__dest__def/term_33.def
- sttfa:natural__dest__def/term_34.def
- sttfa:natural__dest__def/term_35.def
- sttfa:natural__dest__def/term_36.def
- sttfa:natural__dest__def/term_37.def
- sttfa:natural__dest__def/term_38.def
- sttfa:natural__dest__def/term_39.def
- sttfa:natural__dest__def/term_40.def
- sttfa:natural__dest__def/type_19.def
- sttfa:natural__dest__def/type_20.def
- sttfa:natural__dest__def/term_41.def
- sttfa:natural__dest__def/term_42.def
- sttfa:natural__dest__def/term_43.def
- sttfa:natural__dest__def/term_44.def
- sttfa:natural__dest__def/term_45.def
- sttfa:natural__dest__def/term_46.def
- sttfa:natural__dest__def/term_47.def
- sttfa:natural__dest__def/term_48.def
- sttfa:natural__dest__def/term_49.def
- sttfa:natural__dest__def/term_50.def
- sttfa:natural__dest__def/term_51.def
- sttfa:natural__dest__def/term_52.def
- sttfa:natural__dest__def/term_53.def
- sttfa:natural__dest__def/term_54.def
- sttfa:natural__dest__def/term_55.def
- sttfa:natural__dest__def/Number_2ENatural_2Epre.def
- sttfa:natural__dest__def/term_56.def
- sttfa:natural__dest__def/term_57.def
- sttfa:natural__dest__def/term_58.def
- sttfa:natural__dest__def/term_59.def
- sttfa:natural__dest__def/term_60.def
- sttfa:natural__dest__def/type_21.def
- sttfa:natural__dest__def/type_22.def
- sttfa:natural__dest__def/type_23.def
- sttfa:natural__dest__def/type_24.def
- sttfa:natural__dest__def/type_25.def
- sttfa:natural__dest__def/term_61.def
- sttfa:natural__dest__def/term_62.def
- sttfa:natural__dest__def/term_63.def
- sttfa:natural__dest__def/term_64.def
- sttfa:natural__dest__def/type_26.def
- sttfa:natural__dest__def/term_65.def
- sttfa:natural__dest__def/term_66.def
- sttfa:natural__dest__def/term_67.def
- sttfa:natural__dest__def/term_68.def
- sttfa:natural__dest__def/term_69.def
- sttfa:natural__dest__def/term_70.def
- sttfa:natural__dest__def/term_71.def
- sttfa:natural__dest__def/term_72.def
- sttfa:natural__dest__def/term_73.def
- sttfa:natural__dest__def/term_74.def
- sttfa:natural__dest__def/term_75.def
- sttfa:natural__dest__def/type_27.def
- sttfa:natural__dest__def/term_76.def
- sttfa:natural__dest__def/term_77.def
- sttfa:natural__dest__def/term_78.def
- sttfa:natural__dest__def/term_79.def
- sttfa:natural__dest__def/term_80.def
- sttfa:natural__dest__def/term_81.def
- sttfa:natural__dest__def/term_82.def
- sttfa:natural__dest__def/term_83.def
- sttfa:natural__dest__def/term_84.def
- sttfa:natural__dest__def/term_85.def
- sttfa:natural__dest__def/term_86.def
- sttfa:natural__dest__def/term_87.def
- sttfa:natural__dest__def/term_88.def
- sttfa:natural__dest__def/term_89.def
- sttfa:natural__dest__def/term_90.def
- sttfa:natural__dest__def/term_91.def
- sttfa:natural__dest__def/type_28.def
- sttfa:natural__dest__def/term_92.def
- sttfa:natural__dest__def/term_93.def
- sttfa:natural__dest__def/type_29.def
- sttfa:natural__dest__def/term_94.def
- sttfa:natural__dest__def/type_30.def
- sttfa:natural__dest__def/type_31.def
- sttfa:natural__dest__def/type_32.def
- sttfa:natural__dest__def/term_95.def
- sttfa:natural__dest__def/type_33.def
- sttfa:natural__dest__def/term_96.def
- sttfa:natural__dest__def/term_97.def
- sttfa:natural__dest__def/term_98.def
- sttfa:natural__dest__def/term_99.def
- sttfa:natural__dest__def/term_100.def
- sttfa:natural__dest__def/term_101.def
- sttfa:natural__dest__def/term_102.def
- sttfa:natural__dest__def/term_103.def
- sttfa:natural__dest__def/term_104.def
- sttfa:natural__dest__def/term_105.def
- sttfa:natural__dest__def/type_34.def
- sttfa:natural__dest__def/type_35.def
- sttfa:natural__dest__def/type_36.def
- sttfa:natural__dest__def/term_106.def
- sttfa:natural__dest__def/term_107.def
- sttfa:natural__dest__def/term_108.def
- sttfa:natural__dest__def/term_109.def
- sttfa:natural__dest__def/term_110.def
- sttfa:natural__dest__def/term_111.def
- sttfa:natural__dest__def/term_112.def
- sttfa:natural__dest__def/term_113.def
- sttfa:natural__dest__def/term_114.def
- sttfa:natural__dest__def/term_115.def
- sttfa:natural__dest__def/term_116.def
- sttfa:natural__dest__def/term_117.def
- sttfa:natural__dest__def/term_118.def
- sttfa:natural__dest__def/term_119.def
- sttfa:natural__dest__def/term_120.def
- sttfa:natural__dest__def/term_121.def
- sttfa:natural__dest__def/term_122.def
- sttfa:natural__dest__def/term_123.def
- sttfa:natural__dest__def/term_124.def
- sttfa:natural__dest__def/term_125.def
- sttfa:natural__dest__def/term_126.def
- sttfa:natural__dest__def/term_127.def
- sttfa:natural__dest__def/term_128.def
- sttfa:natural__dest__def/term_129.def
- sttfa:natural__dest__def/term_130.def
- sttfa:natural__dest__def/term_131.def
- sttfa:natural__dest__def/type_37.def
- sttfa:natural__dest__def/type_38.def
- sttfa:natural__dest__def/term_132.def
- sttfa:natural__dest__def/term_133.def
- sttfa:natural__dest__def/term_134.def
- sttfa:natural__dest__def/term_135.def
- sttfa:natural__dest__def/term_136.def
- sttfa:natural__dest__def/term_137.def
- sttfa:natural__dest__def/term_138.def
- sttfa:natural__dest__def/term_139.def
- sttfa:natural__dest__def/term_140.def
- sttfa:natural__dest__def/term_141.def
- sttfa:natural__dest__def/term_142.def
- sttfa:natural__dest__def/term_143.def
- sttfa:natural__dest__def/term_144.def
- sttfa:natural__dest__def/term_145.def
- sttfa:natural__dest__def/term_146.def
- sttfa:natural__dest__def/type_39.def
- sttfa:natural__dest__def/type_40.def
- sttfa:natural__dest__def/type_41.def
- sttfa:natural__dest__def/term_147.def
- sttfa:natural__dest__def/term_148.def
- sttfa:natural__dest__def/type_42.def
- sttfa:natural__dest__def/type_43.def
- sttfa:natural__dest__def/term_149.def
- sttfa:natural__dest__def/type_44.def
- sttfa:natural__dest__def/type_45.def
- sttfa:natural__dest__def/term_150.def
- sttfa:natural__dest__def/type_46.def
- sttfa:natural__dest__def/term_151.def
- sttfa:natural__dest__def/term_152.def
- sttfa:natural__dest__def/term_153.def
- sttfa:natural__dest__def/term_154.def
- sttfa:natural__dest__def/term_155.def
- sttfa:natural__dest__def/term_156.def
- sttfa:natural__dest__def/term_157.def
- sttfa:natural__dest__def/term_158.def
- sttfa:natural__dest__def/term_159.def
- sttfa:natural__dest__def/term_160.def
- sttfa:natural__dest__def/term_161.def
- sttfa:natural__dest__def/term_162.def
- sttfa:natural__dest__def/term_163.def
- sttfa:natural__dest__def/term_164.def
- sttfa:natural__dest__def/term_165.def
- sttfa:natural__dest__def/term_166.def
- sttfa:natural__dest__def/term_167.def
- sttfa:natural__dest__def/term_168.def
- sttfa:natural__dest__def/term_169.def
- sttfa:natural__dest__def/term_170.def
- sttfa:natural__dest__def/term_171.def
- sttfa:natural__dest__def/term_172.def
- sttfa:natural__dest__def/term_173.def
- sttfa:natural__dest__def/term_174.def
- sttfa:natural__dest__def/term_175.def
- sttfa:natural__dest__def/term_176.def
- sttfa:natural__dest__def/term_177.def
- sttfa:natural__dest__def/term_178.def
- sttfa:natural__dest__def/term_179.def
- sttfa:natural__dest__def/term_180.def
- sttfa:natural__dest__def/term_181.def
- sttfa:natural__dest__def/term_182.def
theorem
- sttfa:natural__dest__def/thm_0.thm
- sttfa:natural__dest__def/thm_1.thm
- sttfa:natural__dest__def/thm_2.thm
- sttfa:natural__dest__def/thm_3.thm
- sttfa:natural__dest__def/thm_4.thm
- sttfa:natural__dest__def/thm_5.thm
- sttfa:natural__dest__def/thm_6.thm
- sttfa:natural__dest__def/thm_7.thm
- sttfa:natural__dest__def/thm_8.thm
- sttfa:natural__dest__def/thm_9.thm
- sttfa:natural__dest__def/thm_10.thm
- sttfa:natural__dest__def/thm_11.thm
- sttfa:natural__dest__def/thm_12.thm
- sttfa:natural__dest__def/thm_13.thm
- sttfa:natural__dest__def/thm_14.thm
- sttfa:natural__dest__def/thm_15.thm
- sttfa:natural__dest__def/thm_16.thm
- sttfa:natural__dest__def/thm_17.thm
- sttfa:natural__dest__def/thm_18.thm
- sttfa:natural__dest__def/thm_19.thm
- sttfa:natural__dest__def/thm_20.thm
- sttfa:natural__dest__def/thm_21.thm
- sttfa:natural__dest__def/thm_22.thm
- sttfa:natural__dest__def/thm_23.thm
- sttfa:natural__dest__def/thm_24.thm
- sttfa:natural__dest__def/thm_25.thm
- sttfa:natural__dest__def/thm_26.thm
- sttfa:natural__dest__def/thm_27.thm
- sttfa:natural__dest__def/thm_28.thm
- sttfa:natural__dest__def/EXISTS_THM.thm
- sttfa:natural__dest__def/thm_30.thm
- sttfa:natural__dest__def/thm_31.thm
- sttfa:natural__dest__def/thm_32.thm
- sttfa:natural__dest__def/thm_33.thm
- sttfa:natural__dest__def/thm_34.thm
- sttfa:natural__dest__def/thm_35.thm
- sttfa:natural__dest__def/thm_36.thm
- sttfa:natural__dest__def/thm_37.thm
- sttfa:natural__dest__def/thm_38.thm
- sttfa:natural__dest__def/thm_39.thm
- sttfa:natural__dest__def/thm_40.thm
- sttfa:natural__dest__def/thm_41.thm
- sttfa:natural__dest__def/thm_42.thm
- sttfa:natural__dest__def/thm_43.thm
- sttfa:natural__dest__def/thm_44.thm
- sttfa:natural__dest__def/thm_45.thm
- sttfa:natural__dest__def/thm_46.thm
- sttfa:natural__dest__def/thm_47.thm
- sttfa:natural__dest__def/thm_48.thm
- sttfa:natural__dest__def/thm_49.thm
- sttfa:natural__dest__def/thm_50.thm
- sttfa:natural__dest__def/thm_51.thm
- sttfa:natural__dest__def/thm_52.thm
- sttfa:natural__dest__def/thm_53.thm
- sttfa:natural__dest__def/thm_54.thm
- sttfa:natural__dest__def/thm_55.thm
- sttfa:natural__dest__def/thm_56.thm
- sttfa:natural__dest__def/thm_57.thm
- sttfa:natural__dest__def/thm_58.thm
- sttfa:natural__dest__def/thm_59.thm
- sttfa:natural__dest__def/thm_60.thm
- sttfa:natural__dest__def/thm_61.thm
- sttfa:natural__dest__def/SKOLEM_THM.thm
- sttfa:natural__dest__def/thm_63.thm
- sttfa:natural__dest__def/thm_64.thm
- sttfa:natural__dest__def/thm_65.thm
- sttfa:natural__dest__def/thm_66.thm
- sttfa:natural__dest__def/thm_67.thm
- sttfa:natural__dest__def/thm_68.thm
- sttfa:natural__dest__def/thm_69.thm
- sttfa:natural__dest__def/thm_70.thm
- sttfa:natural__dest__def/thm_71.thm
- sttfa:natural__dest__def/thm_72.thm
- sttfa:natural__dest__def/thm_73.thm
- sttfa:natural__dest__def/thm_74.thm
- sttfa:natural__dest__def/thm_75.thm
- sttfa:natural__dest__def/thm_76.thm
- sttfa:natural__dest__def/thm_77.thm
- sttfa:natural__dest__def/thm_78.thm
- sttfa:natural__dest__def/thm_79.thm
- sttfa:natural__dest__def/num_RECURSION.thm
- sttfa:natural__dest__def/thm_81.thm
- sttfa:natural__dest__def/thm_82.thm
- sttfa:natural__dest__def/thm_83.thm
- sttfa:natural__dest__def/thm_84.thm
- sttfa:natural__dest__def/thm_85.thm
- sttfa:natural__dest__def/thm_86.thm
- sttfa:natural__dest__def/thm_87.thm
- sttfa:natural__dest__def/thm_88.thm
- sttfa:natural__dest__def/thm_89.thm
- sttfa:natural__dest__def/thm_90.thm
- sttfa:natural__dest__def/thm_91.thm
- sttfa:natural__dest__def/thm_92.thm
- sttfa:natural__dest__def/thm_93.thm
- sttfa:natural__dest__def/thm_94.thm
- sttfa:natural__dest__def/thm_95.thm
- sttfa:natural__dest__def/thm_96.thm
- sttfa:natural__dest__def/thm_97.thm
- sttfa:natural__dest__def/thm_98.thm
- sttfa:natural__dest__def/thm_99.thm
- sttfa:natural__dest__def/thm_100.thm
- sttfa:natural__dest__def/thm_101.thm
- sttfa:natural__dest__def/thm_102.thm
- sttfa:natural__dest__def/PRE.thm