components/ng_kernel/alluris.txt

   1 cic:/matita/Q/Qaxioms/symmetric_Qtimes.con
   2 cic:/matita/Q/Qaxioms/symmetric_Qplus.con
   3 cic:/matita/Q/Qaxioms/sigma_Q.con
   4 cic:/matita/Q/Qaxioms/num.con
   5 cic:/matita/Q/Qaxioms/frac_num_denom.con
   6 cic:/matita/Q/Qaxioms/frac_n.con
   7 cic:/matita/Q/Qaxioms/frac_Qopp.con
   8 cic:/matita/Q/Qaxioms/frac_Qinv2.con
   9 cic:/matita/Q/Qaxioms/frac_Qinv1.con
  10 cic:/matita/Q/Qaxioms/frac_O.con
  11 cic:/matita/Q/Qaxioms/frac.con
  12 cic:/matita/Q/Qaxioms/distributive_Qtimes_Qplus.con
  13 cic:/matita/Q/Qaxioms/denom.con
  14 cic:/matita/Q/Qaxioms/associative_Qtimes.con
  15 cic:/matita/Q/Qaxioms/associative_Qplus.con
  16 cic:/matita/Q/Qaxioms/Qtimes_frac.con
  17 cic:/matita/Q/Qaxioms/Qtimes_Qinv.con
  18 cic:/matita/Q/Qaxioms/Qtimes_Q1.con
  19 cic:/matita/Q/Qaxioms/Qtimes.con
  20 cic:/matita/Q/Qaxioms/Qplus_frac.con
  21 cic:/matita/Q/Qaxioms/Qplus_Qopp.con
  22 cic:/matita/Q/Qaxioms/Qplus_QO.con
  23 cic:/matita/Q/Qaxioms/Qplus.con
  24 cic:/matita/Q/Qaxioms/Qopp.con
  25 cic:/matita/Q/Qaxioms/Qlt_fracr.con
  26 cic:/matita/Q/Qaxioms/Qlt_fracl.con
  27 cic:/matita/Q/Qaxioms/Qlt.con
  28 cic:/matita/Q/Qaxioms/Qinv.con
  29 cic:/matita/Q/Qaxioms/QO.con
  30 cic:/matita/Q/Qaxioms/Q1.con
  31 cic:/matita/Q/Qaxioms/Q.con
  32 cic:/matita/Q/q/symmetric_rtimes.con
  33 cic:/matita/Q/q/symmetric2_ftimes.con
  34 cic:/matita/Q/q/rtimes_rinv.con
  35 cic:/matita/Q/q/rtimes.con
  36 cic:/matita/Q/q/rinv.con
  37 cic:/matita/Q/q/ratio_rect.con
  38 cic:/matita/Q/q/ratio_rec.con
  39 cic:/matita/Q/q/ratio_ind.con
  40 cic:/matita/Q/q/ratio.ind
  41 cic:/matita/Q/q/not_eq_pp_nn.con
  42 cic:/matita/Q/q/not_eq_pp_cons.con
  43 cic:/matita/Q/q/not_eq_nn_cons.con
  44 cic:/matita/Q/q/injective_pp.con
  45 cic:/matita/Q/q/injective_nn.con
  46 cic:/matita/Q/q/ftl.con
  47 cic:/matita/Q/q/ftimes_finv.con
  48 cic:/matita/Q/q/ftimes.con
  49 cic:/matita/Q/q/fraction_rect.con
  50 cic:/matita/Q/q/fraction_rec.con
  51 cic:/matita/Q/q/fraction_ind.con
  52 cic:/matita/Q/q/fraction_elim2.con
  53 cic:/matita/Q/q/fraction.ind
  54 cic:/matita/Q/q/finv.con
  55 cic:/matita/Q/q/fhd.con
  56 cic:/matita/Q/q/eqfb_to_Prop.con
  57 cic:/matita/Q/q/eqfb.con
  58 cic:/matita/Q/q/eq_cons_to_eq2.con
  59 cic:/matita/Q/q/eq_cons_to_eq1.con
  60 cic:/matita/Q/q/decidable_eq_fraction.con
  61 cic:/matita/Q/q/aux.con
  62 cic:/matita/Q/q/Z_to_ratio.con
  63 cic:/matita/Q/q/Qtimes.con
  64 cic:/matita/Q/q/Q_rect.con
  65 cic:/matita/Q/q/Q_rec.con
  66 cic:/matita/Q/q/Q_ind.con
  67 cic:/matita/Q/q/Q.ind
  68 cic:/matita/Z/compare/eqZb_to_Prop.con
  69 cic:/matita/Z/compare/eqZb_elim.con
  70 cic:/matita/Z/compare/eqZb.con
  71 cic:/matita/Z/compare/Z_compare_to_Prop.con
  72 cic:/matita/Z/compare/Z_compare.con
  73 cic:/matita/Z/dirichlet_product/sigma_p_OZ.con
  74 cic:/matita/Z/dirichlet_product/is_one_OZ.con
  75 cic:/matita/Z/dirichlet_product/is_one.con
  76 cic:/matita/Z/dirichlet_product/dirichlet_product_one_r.con
  77 cic:/matita/Z/dirichlet_product/dirichlet_product_one_l.con
  78 cic:/matita/Z/dirichlet_product/dirichlet_product_is_one_r.con
  79 cic:/matita/Z/dirichlet_product/dirichlet_product_is_one_l.con
  80 cic:/matita/Z/dirichlet_product/dirichlet_product.con
  81 cic:/matita/Z/dirichlet_product/commutative_dirichlet_product.con
  82 cic:/matita/Z/dirichlet_product/associative_dirichlet_product.con
  83 cic:/matita/Z/inversion/sigma_div_moebius.con
  84 cic:/matita/Z/inversion/sigma_div.con
  85 cic:/matita/Z/inversion/inversion.con
  86 cic:/matita/Z/moebius/sigma_p_moebius1.con
  87 cic:/matita/Z/moebius/sigma_p_moebius.con
  88 cic:/matita/Z/moebius/p_ord_SSq_r_to_moebius.con
  89 cic:/matita/Z/moebius/p_ord_SO_r_to_moebius1.con
  90 cic:/matita/Z/moebius/p_ord_SO_r_to_moebius.con
  91 cic:/matita/Z/moebius/p_ord_SO_SO_to_moebius.con
  92 cic:/matita/Z/moebius/not_divides_to_eq_moebius_aux.con
  93 cic:/matita/Z/moebius/moebius_exp.con
  94 cic:/matita/Z/moebius/moebius_aux_SO.con
  95 cic:/matita/Z/moebius/moebius_aux.con
  96 cic:/matita/Z/moebius/moebius.con
  97 cic:/matita/Z/moebius/eq_moebius_moebius_aux.con
  98 cic:/matita/Z/orders/transitive_Zlt.con
  99 cic:/matita/Z/orders/transitive_Zle.con
 100 cic:/matita/Z/orders/trans_Zlt.con
 101 cic:/matita/Z/orders/trans_Zle.con
 102 cic:/matita/Z/orders/lt_to_Zlt_pos_pos.con
 103 cic:/matita/Z/orders/lt_to_Zlt_neg_neg.con
 104 cic:/matita/Z/orders/irreflexive_Zlt.con
 105 cic:/matita/Z/orders/irrefl_Zlt.con
 106 cic:/matita/Z/orders/Zlt_to_Zle.con
 107 cic:/matita/Z/orders/Zlt_pos_pos_to_lt.con
 108 cic:/matita/Z/orders/Zlt_neg_neg_to_lt.con
 109 cic:/matita/Z/orders/Zlt.con
 110 cic:/matita/Z/orders/Zle.con
 111 cic:/matita/Z/plus/sym_Zplus.con
 112 cic:/matita/Z/plus/injective_Zplus_r.con
 113 cic:/matita/Z/plus/injective_Zplus_l.con
 114 cic:/matita/Z/plus/eq_OZ_Zopp_OZ.con
 115 cic:/matita/Z/plus/associative_Zplus.con
 116 cic:/matita/Z/plus/assoc_Zplus.con
 117 cic:/matita/Z/plus/Zsucc_Zplus_pos_O.con
 118 cic:/matita/Z/plus/Zpred_Zplus_neg_O.con
 119 cic:/matita/Z/plus/Zplus_z_OZ.con
 120 cic:/matita/Z/plus/Zplus_pos_pos.con
 121 cic:/matita/Z/plus/Zplus_pos_neg.con
 122 cic:/matita/Z/plus/Zplus_neg_pos.con
 123 cic:/matita/Z/plus/Zplus_neg_neg.con
 124 cic:/matita/Z/plus/Zplus_Zsucc_pos_pos.con
 125 cic:/matita/Z/plus/Zplus_Zsucc_pos_neg.con
 126 cic:/matita/Z/plus/Zplus_Zsucc_neg_pos.con
 127 cic:/matita/Z/plus/Zplus_Zsucc_neg_neg.con
 128 cic:/matita/Z/plus/Zplus_Zsucc_Zpred.con
 129 cic:/matita/Z/plus/Zplus_Zsucc.con
 130 cic:/matita/Z/plus/Zplus_Zpred.con
 131 cic:/matita/Z/plus/Zplus_Zopp.con
 132 cic:/matita/Z/plus/Zplus.con
 133 cic:/matita/Z/plus/Zopp_Zplus.con
 134 cic:/matita/Z/plus/Zopp_Zopp.con
 135 cic:/matita/Z/plus/Zopp.con
 136 cic:/matita/Z/plus/Zminus.con
 137 cic:/matita/Z/sigma_p/true_to_sigma_p_Sn.con
 138 cic:/matita/Z/sigma_p/symmetricZPlus.con
 139 cic:/matita/Z/sigma_p/sigma_p_plus.con
 140 cic:/matita/Z/sigma_p/sigma_p_knm.con
 141 cic:/matita/Z/sigma_p/sigma_p_gi.con
 142 cic:/matita/Z/sigma_p/sigma_p_false.con
 143 cic:/matita/Z/sigma_p/sigma_p_divides_b.con
 144 cic:/matita/Z/sigma_p/sigma_p2_eq.con
 145 cic:/matita/Z/sigma_p/sigma_p2.con
 146 cic:/matita/Z/sigma_p/sigma_p2'.con
 147 cic:/matita/Z/sigma_p/sigma_p.con
 148 cic:/matita/Z/sigma_p/false_to_sigma_p_Sn.con
 149 cic:/matita/Z/sigma_p/false_to_eq_sigma_p.con
 150 cic:/matita/Z/sigma_p/eq_sigma_p_gh.con
 151 cic:/matita/Z/sigma_p/eq_sigma_p1.con
 152 cic:/matita/Z/sigma_p/eq_sigma_p.con
 153 cic:/matita/Z/sigma_p/divides_exp_to_lt_ord.con
 154 cic:/matita/Z/sigma_p/divides_exp_to_divides_ord_rem.con
 155 cic:/matita/Z/sigma_p/Ztimes_sigma_pr.con
 156 cic:/matita/Z/sigma_p/Ztimes_sigma_pl.con
 157 cic:/matita/Z/times/times_minus1.con
 158 cic:/matita/Z/times/symmetric_Ztimes.con
 159 cic:/matita/Z/times/sym_Ztimes.con
 160 cic:/matita/Z/times/distributive_Ztimes_Zplus.con
 161 cic:/matita/Z/times/distributive2_Ztimes_pos_Zplus.con
 162 cic:/matita/Z/times/distributive2_Ztimes_neg_Zplus.con
 163 cic:/matita/Z/times/distr_Ztimes_Zplus_pos.con
 164 cic:/matita/Z/times/distr_Ztimes_Zplus_neg.con
 165 cic:/matita/Z/times/distr_Ztimes_Zplus.con
 166 cic:/matita/Z/times/associative_Ztimes.con
 167 cic:/matita/Z/times/assoc_Ztimes.con
 168 cic:/matita/Z/times/Ztimes_z_OZ.con
 169 cic:/matita/Z/times/Ztimes_neg_Zopp.con
 170 cic:/matita/Z/times/Ztimes_Zplus_pos_pos_neg.con
 171 cic:/matita/Z/times/Ztimes_Zplus_pos_neg_pos.con
 172 cic:/matita/Z/times/Ztimes_Zone_r.con
 173 cic:/matita/Z/times/Ztimes_Zone_l.con
 174 cic:/matita/Z/times/Ztimes.con
 175 cic:/matita/Z/times/Zone.con
 176 cic:/matita/Z/z/pos_n_eq_S_n.con
 177 cic:/matita/Z/z/not_eq_pos_neg.con
 178 cic:/matita/Z/z/not_eq_OZ_pos.con
 179 cic:/matita/Z/z/not_eq_OZ_neg.con
 180 cic:/matita/Z/z/neg_Z_of_nat.con
 181 cic:/matita/Z/z/injective_pos.con
 182 cic:/matita/Z/z/injective_neg.con
 183 cic:/matita/Z/z/inj_pos.con
 184 cic:/matita/Z/z/inj_neg.con
 185 cic:/matita/Z/z/decidable_eq_Z.con
 186 cic:/matita/Z/z/abs.con
 187 cic:/matita/Z/z/Zsucc_Zpred.con
 188 cic:/matita/Z/z/Zsucc.con
 189 cic:/matita/Z/z/Zpred_Zsucc.con
 190 cic:/matita/Z/z/Zpred.con
 191 cic:/matita/Z/z/Z_rect.con
 192 cic:/matita/Z/z/Z_rec.con
 193 cic:/matita/Z/z/Z_of_nat.con
 194 cic:/matita/Z/z/Z_ind.con
 195 cic:/matita/Z/z/Z.ind
 196 cic:/matita/Z/z/OZ_test_to_Prop.con
 197 cic:/matita/Z/z/OZ_test.con
 198 cic:/matita/algebra/CoRN/SemiGroups/subcrr.con
 199 cic:/matita/algebra/CoRN/SemiGroups/plus_assoc_unfolded.con
 200 cic:/matita/algebra/CoRN/SemiGroups/plus_assoc.con
 201 cic:/matita/algebra/CoRN/SemiGroups/part_function_plus_strext.con
 202 cic:/matita/algebra/CoRN/SemiGroups/morphism_of_CSemiGroups.con
 203 cic:/matita/algebra/CoRN/SemiGroups/mk_SubCSemiGroup.con
 204 cic:/matita/algebra/CoRN/SemiGroups/is_unit.con
 205 cic:/matita/algebra/CoRN/SemiGroups/is_rht_unit.con
 206 cic:/matita/algebra/CoRN/SemiGroups/is_lft_unit.con
 207 cic:/matita/algebra/CoRN/SemiGroups/is_CSemiGroup.con
 208 cic:/matita/algebra/CoRN/SemiGroups/included_FPlus.con
 209 cic:/matita/algebra/CoRN/SemiGroups/included_FPlus'.con
 210 cic:/matita/algebra/CoRN/SemiGroups/included_FPlus''.con
 211 cic:/matita/algebra/CoRN/SemiGroups/dprod_strext.con
 212 cic:/matita/algebra/CoRN/SemiGroups/dprod_as_csb_fun.con
 213 cic:/matita/algebra/CoRN/SemiGroups/dprod.con
 214 cic:/matita/algebra/CoRN/SemiGroups/direct_product_is_CSemiGroup.con
 215 cic:/matita/algebra/CoRN/SemiGroups/direct_product_as_CSemiGroup.con
 216 cic:/matita/algebra/CoRN/SemiGroups/csg_proof.con
 217 cic:/matita/algebra/CoRN/SemiGroups/csg_op.con
 218 cic:/matita/algebra/CoRN/SemiGroups/csg_crr.con
 219 cic:/matita/algebra/CoRN/SemiGroups/cs_unique_unit.con
 220 cic:/matita/algebra/CoRN/SemiGroups/Type_OF_CSemiGroup.con
 221 cic:/matita/algebra/CoRN/SemiGroups/NQ.con
 222 cic:/matita/algebra/CoRN/SemiGroups/NP.con
 223 cic:/matita/algebra/CoRN/SemiGroups/FunClass_2_OF_CSemiGroup.con
 224 cic:/matita/algebra/CoRN/SemiGroups/Fplus.con
 225 cic:/matita/algebra/CoRN/SemiGroups/FS_is_CSemiGroup.con
 226 cic:/matita/algebra/CoRN/SemiGroups/FS_as_CSemiGroup.con
 227 cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_rect.con
 228 cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_rec.con
 229 cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_is_CSemiGroup.con
 230 cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_ind.con
 231 cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup.ind
 232 cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con
 233 cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con
 234 cic:/matita/algebra/CoRN/SetoidFun/total_eq_part.con
 235 cic:/matita/algebra/CoRN/SetoidFun/ta_apfun.con
 236 cic:/matita/algebra/CoRN/SetoidFun/sym_apfun.con
 237 cic:/matita/algebra/CoRN/SetoidFun/surjective.con
 238 cic:/matita/algebra/CoRN/SetoidFun/sigT_rect.con
 239 cic:/matita/algebra/CoRN/SetoidFun/sigT_rec.con
 240 cic:/matita/algebra/CoRN/SetoidFun/sigT_ind.con
 241 cic:/matita/algebra/CoRN/SetoidFun/sigT.ind
 242 cic:/matita/algebra/CoRN/SetoidFun/projected_bin_fun.con
 243 cic:/matita/algebra/CoRN/SetoidFun/proj_bin_fun.con
 244 cic:/matita/algebra/CoRN/SetoidFun/projT2m.con
 245 cic:/matita/algebra/CoRN/SetoidFun/projT1.con
 246 cic:/matita/algebra/CoRN/SetoidFun/proj2_sigTm.con
 247 cic:/matita/algebra/CoRN/SetoidFun/proj1_sigT.con
 248 cic:/matita/algebra/CoRN/SetoidFun/prj2.con
 249 cic:/matita/algebra/CoRN/SetoidFun/prj1.con
 250 cic:/matita/algebra/CoRN/SetoidFun/pfwdef.con
 251 cic:/matita/algebra/CoRN/SetoidFun/pfstrx.con
 252 cic:/matita/algebra/CoRN/SetoidFun/pfpfun.con
 253 cic:/matita/algebra/CoRN/SetoidFun/pfdom.con
 254 cic:/matita/algebra/CoRN/SetoidFun/part_function_comp_strext.con
 255 cic:/matita/algebra/CoRN/SetoidFun/part_function_comp_dom_wd.con
 256 cic:/matita/algebra/CoRN/SetoidFun/opOnFun.con
 257 cic:/matita/algebra/CoRN/SetoidFun/n_ary_operation.con
 258 cic:/matita/algebra/CoRN/SetoidFun/mycor.con
 259 cic:/matita/algebra/CoRN/SetoidFun/is_nullary_operation.con
 260 cic:/matita/algebra/CoRN/SetoidFun/irrefl_apfun.con
 261 cic:/matita/algebra/CoRN/SetoidFun/invfun.con
 262 cic:/matita/algebra/CoRN/SetoidFun/inverse.con
 263 cic:/matita/algebra/CoRN/SetoidFun/inv_strext.con
 264 cic:/matita/algebra/CoRN/SetoidFun/inv2.con
 265 cic:/matita/algebra/CoRN/SetoidFun/inv1.con
 266 cic:/matita/algebra/CoRN/SetoidFun/injective_weak.con
 267 cic:/matita/algebra/CoRN/SetoidFun/injective_imp_injective_weak.con
 268 cic:/matita/algebra/CoRN/SetoidFun/injective.con
 269 cic:/matita/algebra/CoRN/SetoidFun/inj2.con
 270 cic:/matita/algebra/CoRN/SetoidFun/inj1.con
 271 cic:/matita/algebra/CoRN/SetoidFun/id_is_bij.con
 272 cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con
 273 cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con
 274 cic:/matita/algebra/CoRN/SetoidFun/extension_wd.con
 275 cic:/matita/algebra/CoRN/SetoidFun/extend.con
 276 cic:/matita/algebra/CoRN/SetoidFun/ext2_a.con
 277 cic:/matita/algebra/CoRN/SetoidFun/ext2.con
 278 cic:/matita/algebra/CoRN/SetoidFun/ext1.con
 279 cic:/matita/algebra/CoRN/SetoidFun/eq_to_ap_to_ap.con
 280 cic:/matita/algebra/CoRN/SetoidFun/eq_fun.con
 281 cic:/matita/algebra/CoRN/SetoidFun/eq_fm.con
 282 cic:/matita/algebra/CoRN/SetoidFun/empty_word.con
 283 cic:/matita/algebra/CoRN/SetoidFun/dom_wd.con
 284 cic:/matita/algebra/CoRN/SetoidFun/disj_wd.con
 285 cic:/matita/algebra/CoRN/SetoidFun/disj.con
 286 cic:/matita/algebra/CoRN/SetoidFun/direct.con
 287 cic:/matita/algebra/CoRN/SetoidFun/cs_binproj1.con
 288 cic:/matita/algebra/CoRN/SetoidFun/cotrans_apfun.con
 289 cic:/matita/algebra/CoRN/SetoidFun/conj_wd.con
 290 cic:/matita/algebra/CoRN/SetoidFun/conjP.con
 291 cic:/matita/algebra/CoRN/SetoidFun/compose_CSetoid_un_bin_fun.con
 292 cic:/matita/algebra/CoRN/SetoidFun/compose_CSetoid_fun.con
 293 cic:/matita/algebra/CoRN/SetoidFun/compose_CSetoid_bin_un_fun.con
 294 cic:/matita/algebra/CoRN/SetoidFun/compose_CSetoid_bin_fun.con
 295 cic:/matita/algebra/CoRN/SetoidFun/comp_resp_bij.con
 296 cic:/matita/algebra/CoRN/SetoidFun/comp_as_bin_op.con
 297 cic:/matita/algebra/CoRN/SetoidFun/comp.con
 298 cic:/matita/algebra/CoRN/SetoidFun/bpfwdef.con
 299 cic:/matita/algebra/CoRN/SetoidFun/bpfstrx.con
 300 cic:/matita/algebra/CoRN/SetoidFun/bpfpfun.con
 301 cic:/matita/algebra/CoRN/SetoidFun/bpfdom.con
 302 cic:/matita/algebra/CoRN/SetoidFun/block.con
 303 cic:/matita/algebra/CoRN/SetoidFun/binproj1_strext.con
 304 cic:/matita/algebra/CoRN/SetoidFun/binproj1.con
 305 cic:/matita/algebra/CoRN/SetoidFun/bin_part_function_comp_strext.con
 306 cic:/matita/algebra/CoRN/SetoidFun/bin_part_function_comp_dom_wd.con
 307 cic:/matita/algebra/CoRN/SetoidFun/bijective.con
 308 cic:/matita/algebra/CoRN/SetoidFun/bdom_wd.con
 309 cic:/matita/algebra/CoRN/SetoidFun/assoc_comp.con
 310 cic:/matita/algebra/CoRN/SetoidFun/app_strext.con
 311 cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con
 312 cic:/matita/algebra/CoRN/SetoidFun/appA.con
 313 cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con
 314 cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con
 315 cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con
 316 cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con
 317 cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con
 318 cic:/matita/algebra/CoRN/SetoidFun/UR.con
 319 cic:/matita/algebra/CoRN/SetoidFun/UQ.con
 320 cic:/matita/algebra/CoRN/SetoidFun/UP.con
 321 cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con
 322 cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con
 323 cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con
 324 cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind
 325 cic:/matita/algebra/CoRN/SetoidFun/Tapp.con
 326 cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con
 327 cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con
 328 cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con
 329 cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con
 330 cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con
 331 cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con
 332 cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con
 333 cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind
 334 cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con
 335 cic:/matita/algebra/CoRN/SetoidFun/Inv.con
 336 cic:/matita/algebra/CoRN/SetoidFun/Fid.con
 337 cic:/matita/algebra/CoRN/SetoidFun/Fconst.con
 338 cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con
 339 cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con
 340 cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con
 341 cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con
 342 cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con
 343 cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con
 344 cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con
 345 cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind
 346 cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con
 347 cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con
 348 cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con
 349 cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con
 350 cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind
 351 cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con
 352 cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con
 353 cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con
 354 cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind
 355 cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con
 356 cic:/matita/algebra/CoRN/SetoidFun/BR.con
 357 cic:/matita/algebra/CoRN/SetoidFun/BQ.con
 358 cic:/matita/algebra/CoRN/SetoidFun/BP.con
 359 cic:/matita/algebra/CoRN/SetoidFun/Astar.con
 360 cic:/matita/algebra/CoRN/SetoidInc/included_trans.con
 361 cic:/matita/algebra/CoRN/SetoidInc/included_refl.con
 362 cic:/matita/algebra/CoRN/SetoidInc/included_extend.con
 363 cic:/matita/algebra/CoRN/SetoidInc/included_conj_rht.con
 364 cic:/matita/algebra/CoRN/SetoidInc/included_conj_lft.con
 365 cic:/matita/algebra/CoRN/SetoidInc/included_conj.con
 366 cic:/matita/algebra/CoRN/SetoidInc/included_conj'.con
 367 cic:/matita/algebra/CoRN/SetoidInc/included_conj''.con
 368 cic:/matita/algebra/CoRN/SetoidInc/included_FComp.con
 369 cic:/matita/algebra/CoRN/SetoidInc/included_FComp'.con
 370 cic:/matita/algebra/CoRN/SetoidInc/included.con
 371 cic:/matita/algebra/CoRN/Setoids/wdp_well_def.con
 372 cic:/matita/algebra/CoRN/Setoids/wdp_pred.con
 373 cic:/matita/algebra/CoRN/Setoids/wd_pred_rect.con
 374 cic:/matita/algebra/CoRN/Setoids/wd_pred_rec.con
 375 cic:/matita/algebra/CoRN/Setoids/wd_pred_ind.con
 376 cic:/matita/algebra/CoRN/Setoids/wd_pred.ind
 377 cic:/matita/algebra/CoRN/Setoids/un_op_wd_unfolded.con
 378 cic:/matita/algebra/CoRN/Setoids/un_op_wd.con
 379 cic:/matita/algebra/CoRN/Setoids/un_op_strext_unfolded.con
 380 cic:/matita/algebra/CoRN/Setoids/un_op_strext.con
 381 cic:/matita/algebra/CoRN/Setoids/un_op_pres_pred.con
 382 cic:/matita/algebra/CoRN/Setoids/un_op_fun.con
 383 cic:/matita/algebra/CoRN/Setoids/subcsetoid_is_CSetoid.con
 384 cic:/matita/algebra/CoRN/Setoids/subcsetoid_equiv.con
 385 cic:/matita/algebra/CoRN/Setoids/subcsetoid_eq.con
 386 cic:/matita/algebra/CoRN/Setoids/subcsetoid_crr_rect.con
 387 cic:/matita/algebra/CoRN/Setoids/subcsetoid_crr_rec.con
 388 cic:/matita/algebra/CoRN/Setoids/subcsetoid_crr_ind.con
 389 cic:/matita/algebra/CoRN/Setoids/subcsetoid_crr.ind
 390 cic:/matita/algebra/CoRN/Setoids/subcsetoid_ap.con
 391 cic:/matita/algebra/CoRN/Setoids/scs_prf.con
 392 cic:/matita/algebra/CoRN/Setoids/scs_elem.con
 393 cic:/matita/algebra/CoRN/Setoids/restrict_relation.con
 394 cic:/matita/algebra/CoRN/Setoids/restr_un_op_wd.con
 395 cic:/matita/algebra/CoRN/Setoids/restr_un_op_strext.con
 396 cic:/matita/algebra/CoRN/Setoids/restr_un_op.con
 397 cic:/matita/algebra/CoRN/Setoids/restr_f_assoc.con
 398 cic:/matita/algebra/CoRN/Setoids/restr_bin_op_well_def.con
 399 cic:/matita/algebra/CoRN/Setoids/restr_bin_op_strext.con
 400 cic:/matita/algebra/CoRN/Setoids/restr_bin_op.con
 401 cic:/matita/algebra/CoRN/Setoids/rel_wdr.con
 402 cic:/matita/algebra/CoRN/Setoids/rel_wdl.con
 403 cic:/matita/algebra/CoRN/Setoids/rel_strextarg_imp_strext.con
 404 cic:/matita/algebra/CoRN/Setoids/rel_strext_rht.con
 405 cic:/matita/algebra/CoRN/Setoids/rel_strext_lft.con
 406 cic:/matita/algebra/CoRN/Setoids/rel_strext_imp_rhtarg.con
 407 cic:/matita/algebra/CoRN/Setoids/rel_strext_imp_lftarg.con
 408 cic:/matita/algebra/CoRN/Setoids/rel_strext.con
 409 cic:/matita/algebra/CoRN/Setoids/proper_caseZ_diff_CS.con
 410 cic:/matita/algebra/CoRN/Setoids/prodcsetoid_is_CSetoid.con
 411 cic:/matita/algebra/CoRN/Setoids/prod_eq.con
 412 cic:/matita/algebra/CoRN/Setoids/prod_ap.con
 413 cic:/matita/algebra/CoRN/Setoids/pred_wd.con
 414 cic:/matita/algebra/CoRN/Setoids/pred_strong_ext.con
 415 cic:/matita/algebra/CoRN/Setoids/outer_op_well_def.con
 416 cic:/matita/algebra/CoRN/Setoids/outer_op_strext.con
 417 cic:/matita/algebra/CoRN/Setoids/outer_op_bin_fun.con
 418 cic:/matita/algebra/CoRN/Setoids/notnot_ap_imp_neq.con
 419 cic:/matita/algebra/CoRN/Setoids/not_neq_imp_eq.con
 420 cic:/matita/algebra/CoRN/Setoids/not_ap_imp_eq.con
 421 cic:/matita/algebra/CoRN/Setoids/neq_imp_notnot_ap.con
 422 cic:/matita/algebra/CoRN/Setoids/nat_less_n_fun.con
 423 cic:/matita/algebra/CoRN/Setoids/nat_less_n_fun'.con
 424 cic:/matita/algebra/CoRN/Setoids/mk_SubCSetoid_un_op.con
 425 cic:/matita/algebra/CoRN/Setoids/mk_SubCSetoid_bin_op.con
 426 cic:/matita/algebra/CoRN/Setoids/mk_SubCSetoid.con
 427 cic:/matita/algebra/CoRN/Setoids/mk_CSetoid_un_op.con
 428 cic:/matita/algebra/CoRN/Setoids/mk_CSetoid_outer_op.con
 429 cic:/matita/algebra/CoRN/Setoids/mk_CSetoid_bin_op.con
 430 cic:/matita/algebra/CoRN/Setoids/is_CSetoid_rect.con
 431 cic:/matita/algebra/CoRN/Setoids/is_CSetoid_rec.con
 432 cic:/matita/algebra/CoRN/Setoids/is_CSetoid_ind.con
 433 cic:/matita/algebra/CoRN/Setoids/is_CSetoid.ind
 434 cic:/matita/algebra/CoRN/Setoids/id_un_op.con
 435 cic:/matita/algebra/CoRN/Setoids/id_strext.con
 436 cic:/matita/algebra/CoRN/Setoids/id_pres_eq.con
 437 cic:/matita/algebra/CoRN/Setoids/fun_wd.con
 438 cic:/matita/algebra/CoRN/Setoids/fun_strext_imp_wd.con
 439 cic:/matita/algebra/CoRN/Setoids/fun_strext.con
 440 cic:/matita/algebra/CoRN/Setoids/ex_unq.con
 441 cic:/matita/algebra/CoRN/Setoids/equiv.con
 442 cic:/matita/algebra/CoRN/Setoids/eq_wdl.con
 443 cic:/matita/algebra/CoRN/Setoids/eq_transitive_unfolded.con
 444 cic:/matita/algebra/CoRN/Setoids/eq_transitive.con
 445 cic:/matita/algebra/CoRN/Setoids/eq_symmetric_unfolded.con
 446 cic:/matita/algebra/CoRN/Setoids/eq_symmetric.con
 447 cic:/matita/algebra/CoRN/Setoids/eq_reflexive_unfolded.con
 448 cic:/matita/algebra/CoRN/Setoids/eq_reflexive.con
 449 cic:/matita/algebra/CoRN/Setoids/eq_imp_not_neq.con
 450 cic:/matita/algebra/CoRN/Setoids/eq_imp_not_ap.con
 451 cic:/matita/algebra/CoRN/Setoids/csp_wd.con
 452 cic:/matita/algebra/CoRN/Setoids/csp_strext.con
 453 cic:/matita/algebra/CoRN/Setoids/csp_pred.con
 454 cic:/matita/algebra/CoRN/Setoids/csoo_wd_unfolded.con
 455 cic:/matita/algebra/CoRN/Setoids/csoo_wd.con
 456 cic:/matita/algebra/CoRN/Setoids/csoo_strext.con
 457 cic:/matita/algebra/CoRN/Setoids/csf_wd_unfolded.con
 458 cic:/matita/algebra/CoRN/Setoids/csf_wd.con
 459 cic:/matita/algebra/CoRN/Setoids/csf_strext_unfolded.con
 460 cic:/matita/algebra/CoRN/Setoids/csf_strext.con
 461 cic:/matita/algebra/CoRN/Setoids/csf_fun.con
 462 cic:/matita/algebra/CoRN/Setoids/csbf_wd_unfolded.con
 463 cic:/matita/algebra/CoRN/Setoids/csbf_wd.con
 464 cic:/matita/algebra/CoRN/Setoids/csbf_strext.con
 465 cic:/matita/algebra/CoRN/Setoids/csbf_fun.con
 466 cic:/matita/algebra/CoRN/Setoids/cs_un_op_strext.con
 467 cic:/matita/algebra/CoRN/Setoids/cs_proof.con
 468 cic:/matita/algebra/CoRN/Setoids/cs_neq.con
 469 cic:/matita/algebra/CoRN/Setoids/cs_eq.con
 470 cic:/matita/algebra/CoRN/Setoids/cs_crr.con
 471 cic:/matita/algebra/CoRN/Setoids/cs_bin_op_wd.con
 472 cic:/matita/algebra/CoRN/Setoids/cs_bin_op_strext.con
 473 cic:/matita/algebra/CoRN/Setoids/cs_ap.con
 474 cic:/matita/algebra/CoRN/Setoids/commutes.con
 475 cic:/matita/algebra/CoRN/Setoids/caseZ_diff.con
 476 cic:/matita/algebra/CoRN/Setoids/bin_op_wd_unfolded.con
 477 cic:/matita/algebra/CoRN/Setoids/bin_op_wd.con
 478 cic:/matita/algebra/CoRN/Setoids/bin_op_strext_unfolded.con
 479 cic:/matita/algebra/CoRN/Setoids/bin_op_strext.con
 480 cic:/matita/algebra/CoRN/Setoids/bin_op_pres_pred.con
 481 cic:/matita/algebra/CoRN/Setoids/bin_op_is_wd_un_op_rht.con
 482 cic:/matita/algebra/CoRN/Setoids/bin_op_is_wd_un_op_lft.con
 483 cic:/matita/algebra/CoRN/Setoids/bin_op_is_strext_un_op_rht.con
 484 cic:/matita/algebra/CoRN/Setoids/bin_op_is_strext_un_op_lft.con
 485 cic:/matita/algebra/CoRN/Setoids/bin_op_bin_fun.con
 486 cic:/matita/algebra/CoRN/Setoids/bin_op2un_op_rht.con
 487 cic:/matita/algebra/CoRN/Setoids/bin_op2un_op_lft.con
 488 cic:/matita/algebra/CoRN/Setoids/bin_fun_wd.con
 489 cic:/matita/algebra/CoRN/Setoids/bin_fun_strext_imp_wd.con
 490 cic:/matita/algebra/CoRN/Setoids/bin_fun_strext.con
 491 cic:/matita/algebra/CoRN/Setoids/ax_ap_tight.con
 492 cic:/matita/algebra/CoRN/Setoids/ax_ap_symmetric.con
 493 cic:/matita/algebra/CoRN/Setoids/ax_ap_irreflexive.con
 494 cic:/matita/algebra/CoRN/Setoids/ax_ap_cotransitive.con
 495 cic:/matita/algebra/CoRN/Setoids/ap_tight.con
 496 cic:/matita/algebra/CoRN/Setoids/ap_symmetric_unfolded.con
 497 cic:/matita/algebra/CoRN/Setoids/ap_symmetric.con
 498 cic:/matita/algebra/CoRN/Setoids/ap_irreflexive_unfolded.con
 499 cic:/matita/algebra/CoRN/Setoids/ap_irreflexive.con
 500 cic:/matita/algebra/CoRN/Setoids/ap_imp_neq.con
 501 cic:/matita/algebra/CoRN/Setoids/ap_cotransitive_unfolded.con
 502 cic:/matita/algebra/CoRN/Setoids/ap_cotransitive.con
 503 cic:/matita/algebra/CoRN/Setoids/Zminus_S_S.con
 504 cic:/matita/algebra/CoRN/Setoids/Prop_OF_subcsetoid_crr1.con
 505 cic:/matita/algebra/CoRN/Setoids/Prop_OF_subcsetoid_crr.con
 506 cic:/matita/algebra/CoRN/Setoids/ProdCSetoid.con
 507 cic:/matita/algebra/CoRN/Setoids/FunClass_2_OF_CSetoid_outer_op.con
 508 cic:/matita/algebra/CoRN/Setoids/FunClass_2_OF_CSetoid_bin_op.con
 509 cic:/matita/algebra/CoRN/Setoids/Const_CSetoid_fun.con
 510 cic:/matita/algebra/CoRN/Setoids/CSetoid_un_op.con
 511 cic:/matita/algebra/CoRN/Setoids/CSetoid_rect.con
 512 cic:/matita/algebra/CoRN/Setoids/CSetoid_rec.con
 513 cic:/matita/algebra/CoRN/Setoids/CSetoid_predicate_rect.con
 514 cic:/matita/algebra/CoRN/Setoids/CSetoid_predicate_rec.con
 515 cic:/matita/algebra/CoRN/Setoids/CSetoid_predicate_ind.con
 516 cic:/matita/algebra/CoRN/Setoids/CSetoid_predicate.ind
 517 cic:/matita/algebra/CoRN/Setoids/CSetoid_outer_op.con
 518 cic:/matita/algebra/CoRN/Setoids/CSetoid_is_CSetoid.con
 519 cic:/matita/algebra/CoRN/Setoids/CSetoid_ind.con
 520 cic:/matita/algebra/CoRN/Setoids/CSetoid_fun_rect.con
 521 cic:/matita/algebra/CoRN/Setoids/CSetoid_fun_rec.con
 522 cic:/matita/algebra/CoRN/Setoids/CSetoid_fun_ind.con
 523 cic:/matita/algebra/CoRN/Setoids/CSetoid_fun.ind
 524 cic:/matita/algebra/CoRN/Setoids/CSetoid_bin_op.con
 525 cic:/matita/algebra/CoRN/Setoids/CSetoid_bin_fun_rect.con
 526 cic:/matita/algebra/CoRN/Setoids/CSetoid_bin_fun_rec.con
 527 cic:/matita/algebra/CoRN/Setoids/CSetoid_bin_fun_ind.con
 528 cic:/matita/algebra/CoRN/Setoids/CSetoid_bin_fun.ind
 529 cic:/matita/algebra/CoRN/Setoids/CSetoid.ind
 530 cic:/matita/algebra/CoRN/Setoids/CSassociative.con
 531 cic:/matita/algebra/finite_groups/semigroup.con
 532 cic:/matita/algebra/finite_groups/repr_index_of.con
 533 cic:/matita/algebra/finite_groups/repr.con
 534 cic:/matita/algebra/finite_groups/pigeonhole.con
 535 cic:/matita/algebra/finite_groups/order.con
 536 cic:/matita/algebra/finite_groups/is_finite_enumerable.con
 537 cic:/matita/algebra/finite_groups/isSemiGroup_OF_finite_enumerable_SemiGroup.con
 538 cic:/matita/algebra/finite_groups/index_of_sur.con
 539 cic:/matita/algebra/finite_groups/index_of_repr.con
 540 cic:/matita/algebra/finite_groups/index_of.con
 541 cic:/matita/algebra/finite_groups/finite_enumerable_rect.con
 542 cic:/matita/algebra/finite_groups/finite_enumerable_rec.con
 543 cic:/matita/algebra/finite_groups/finite_enumerable_ind.con
 544 cic:/matita/algebra/finite_groups/finite_enumerable_SemiGroup_to_left_cancellable_to_right_cancellable_to_isMonoid.con
 545 cic:/matita/algebra/finite_groups/finite_enumerable_SemiGroup_rect.con
 546 cic:/matita/algebra/finite_groups/finite_enumerable_SemiGroup_rec.con
 547 cic:/matita/algebra/finite_groups/finite_enumerable_SemiGroup_ind.con
 548 cic:/matita/algebra/finite_groups/finite_enumerable_SemiGroup.ind
 549 cic:/matita/algebra/finite_groups/finite_enumerable.ind
 550 cic:/matita/algebra/finite_groups/Type_OF_finite_enumerable_SemiGroup.con
 551 cic:/matita/algebra/finite_groups/Magma_OF_finite_enumerable_SemiGroup.con
 552 cic:/matita/algebra/groups/subgrp.con
 553 cic:/matita/algebra/groups/subgroup_rect.con
 554 cic:/matita/algebra/groups/subgroup_rec.con
 555 cic:/matita/algebra/groups/subgroup_ind.con
 556 cic:/matita/algebra/groups/subgroup.ind
 557 cic:/matita/algebra/groups/right_cancellable.con
 558 cic:/matita/algebra/groups/premonoid.con
 559 cic:/matita/algebra/groups/pregroup.con
 560 cic:/matita/algebra/groups/ns_subgroup.con
 561 cic:/matita/algebra/groups/normal_subgroup_rect.con
 562 cic:/matita/algebra/groups/normal_subgroup_rec.con
 563 cic:/matita/algebra/groups/normal_subgroup_ind.con
 564 cic:/matita/algebra/groups/normal_subgroup.ind
 565 cic:/matita/algebra/groups/normal.con
 566 cic:/matita/algebra/groups/morphism_to_eq_f_1_1.con
 567 cic:/matita/algebra/groups/morphism_rect.con
 568 cic:/matita/algebra/groups/morphism_rec.con
 569 cic:/matita/algebra/groups/morphism_ind.con
 570 cic:/matita/algebra/groups/morphism_OF_subgroup.con
 571 cic:/matita/algebra/groups/morphism_OF_normal_subgroup.con
 572 cic:/matita/algebra/groups/morphism.ind
 573 cic:/matita/algebra/groups/morphism.con
 574 cic:/matita/algebra/groups/monomorphism_rect.con
 575 cic:/matita/algebra/groups/monomorphism_rec.con
 576 cic:/matita/algebra/groups/monomorphism_ind.con
 577 cic:/matita/algebra/groups/monomorphism_OF_normal_subgroup.con
 578 cic:/matita/algebra/groups/monomorphism.ind
 579 cic:/matita/algebra/groups/member_of_subgroup_op_inv_x_y_to_left_coset_eq.con
 580 cic:/matita/algebra/groups/member_of_subgroup.con
 581 cic:/matita/algebra/groups/member_of_left_coset.con
 582 cic:/matita/algebra/groups/left_coset_rect.con
 583 cic:/matita/algebra/groups/left_coset_rec.con
 584 cic:/matita/algebra/groups/left_coset_ind.con
 585 cic:/matita/algebra/groups/left_coset_eq.con
 586 cic:/matita/algebra/groups/left_coset_disjoint.con
 587 cic:/matita/algebra/groups/left_coset.ind
 588 cic:/matita/algebra/groups/left_cancellable.con
 589 cic:/matita/algebra/groups/is_monoid.con
 590 cic:/matita/algebra/groups/isSemiGroup_OF_subgroup.con
 591 cic:/matita/algebra/groups/isSemiGroup_OF_normal_subgroup.con
 592 cic:/matita/algebra/groups/isSemiGroup_OF_isGroup.con
 593 cic:/matita/algebra/groups/isSemiGroup_OF_Group.con
 594 cic:/matita/algebra/groups/isMonoid_OF_subgroup.con
 595 cic:/matita/algebra/groups/isMonoid_OF_normal_subgroup.con
 596 cic:/matita/algebra/groups/isMonoid_OF_Group.con
 597 cic:/matita/algebra/groups/isGroup_rect.con
 598 cic:/matita/algebra/groups/isGroup_rec.con
 599 cic:/matita/algebra/groups/isGroup_ind.con
 600 cic:/matita/algebra/groups/isGroup_OF_subgroup.con
 601 cic:/matita/algebra/groups/isGroup_OF_normal_subgroup.con
 602 cic:/matita/algebra/groups/isGroup.ind
 603 cic:/matita/algebra/groups/inv_is_right_inverse.con
 604 cic:/matita/algebra/groups/inv_is_left_inverse.con
 605 cic:/matita/algebra/groups/inv.con
 606 cic:/matita/algebra/groups/injective.con
 607 cic:/matita/algebra/groups/in_x_mk_left_coset_x_H.con
 608 cic:/matita/algebra/groups/image.con
 609 cic:/matita/algebra/groups/group_properties.con
 610 cic:/matita/algebra/groups/group.con
 611 cic:/matita/algebra/groups/f_morph.con
 612 cic:/matita/algebra/groups/eq_opxy_z_to_eq_y_opinvxz.con
 613 cic:/matita/algebra/groups/eq_opxy_z_to_eq_x_opzinvy.con
 614 cic:/matita/algebra/groups/eq_opxy_e_to_eq_x_invy.con
 615 cic:/matita/algebra/groups/eq_opxy_e_to_eq_invx_y.con
 616 cic:/matita/algebra/groups/eq_op_x_y_op_z_y_to_eq.con
 617 cic:/matita/algebra/groups/eq_op_x_y_op_x_z_to_eq.con
 618 cic:/matita/algebra/groups/eq_inv_op_x_y_op_inv_y_inv_x.con
 619 cic:/matita/algebra/groups/eq_inv_inv_x_x.con
 620 cic:/matita/algebra/groups/eq_image_inv_inv_image.con
 621 cic:/matita/algebra/groups/embed.con
 622 cic:/matita/algebra/groups/element.con
 623 cic:/matita/algebra/groups/Type_OF_subgroup.con
 624 cic:/matita/algebra/groups/Type_OF_normal_subgroup.con
 625 cic:/matita/algebra/groups/Type_OF_PreGroup.con
 626 cic:/matita/algebra/groups/Type_OF_Group.con
 627 cic:/matita/algebra/groups/PreMonoid_OF_subgroup.con
 628 cic:/matita/algebra/groups/PreMonoid_OF_normal_subgroup.con
 629 cic:/matita/algebra/groups/PreMonoid_OF_Group.con
 630 cic:/matita/algebra/groups/PreGroup_rect.con
 631 cic:/matita/algebra/groups/PreGroup_rec.con
 632 cic:/matita/algebra/groups/PreGroup_ind.con
 633 cic:/matita/algebra/groups/PreGroup_OF_subgroup.con
 634 cic:/matita/algebra/groups/PreGroup_OF_normal_subgroup.con
 635 cic:/matita/algebra/groups/PreGroup.ind
 636 cic:/matita/algebra/groups/Not_member_of_subgroup_to_left_coset_disjoint.con
 637 cic:/matita/algebra/groups/Magma_OF_subgroup.con
 638 cic:/matita/algebra/groups/Magma_OF_normal_subgroup.con
 639 cic:/matita/algebra/groups/Magma_OF_PreGroup.con
 640 cic:/matita/algebra/groups/Magma_OF_Group.con
 641 cic:/matita/algebra/groups/Group_rect.con
 642 cic:/matita/algebra/groups/Group_rec.con
 643 cic:/matita/algebra/groups/Group_ind.con
 644 cic:/matita/algebra/groups/Group_OF_normal_subgroup.con
 645 cic:/matita/algebra/groups/Group.ind
 646 cic:/matita/algebra/monoids/premonoid.con
 647 cic:/matita/algebra/monoids/monoid_properties.con
 648 cic:/matita/algebra/monoids/magma.con
 649 cic:/matita/algebra/monoids/is_semi_group.con
 650 cic:/matita/algebra/monoids/is_right_inverse.con
 651 cic:/matita/algebra/monoids/is_left_inverse_to_is_right_inverse_to_eq.con
 652 cic:/matita/algebra/monoids/is_left_inverse.con
 653 cic:/matita/algebra/monoids/isSemiGroup_OF_Monoid.con
 654 cic:/matita/algebra/monoids/isMonoid_rect.con
 655 cic:/matita/algebra/monoids/isMonoid_rec.con
 656 cic:/matita/algebra/monoids/isMonoid_ind.con
 657 cic:/matita/algebra/monoids/isMonoid.ind
 658 cic:/matita/algebra/monoids/e_is_right_unit.con
 659 cic:/matita/algebra/monoids/e_is_left_unit.con
 660 cic:/matita/algebra/monoids/e.con
 661 cic:/matita/algebra/monoids/Type_OF_PreMonoid.con
 662 cic:/matita/algebra/monoids/Type_OF_Monoid.con
 663 cic:/matita/algebra/monoids/PreMonoid_rect.con
 664 cic:/matita/algebra/monoids/PreMonoid_rec.con
 665 cic:/matita/algebra/monoids/PreMonoid_ind.con
 666 cic:/matita/algebra/monoids/PreMonoid.ind
 667 cic:/matita/algebra/monoids/Monoid_rect.con
 668 cic:/matita/algebra/monoids/Monoid_rec.con
 669 cic:/matita/algebra/monoids/Monoid_ind.con
 670 cic:/matita/algebra/monoids/Monoid.ind
 671 cic:/matita/algebra/monoids/Magma_OF_Monoid.con
 672 cic:/matita/algebra/semigroups/semigroup_properties.con
 673 cic:/matita/algebra/semigroups/op_associative.con
 674 cic:/matita/algebra/semigroups/op.con
 675 cic:/matita/algebra/semigroups/magma.con
 676 cic:/matita/algebra/semigroups/is_right_unit.con
 677 cic:/matita/algebra/semigroups/is_left_unit_to_is_right_unit_to_eq.con
 678 cic:/matita/algebra/semigroups/is_left_unit.con
 679 cic:/matita/algebra/semigroups/isSemiGroup_rect.con
 680 cic:/matita/algebra/semigroups/isSemiGroup_rec.con
 681 cic:/matita/algebra/semigroups/isSemiGroup_ind.con
 682 cic:/matita/algebra/semigroups/isSemiGroup.ind
 683 cic:/matita/algebra/semigroups/carrier.con
 684 cic:/matita/algebra/semigroups/Type_OF_SemiGroup.con
 685 cic:/matita/algebra/semigroups/SemiGroup_rect.con
 686 cic:/matita/algebra/semigroups/SemiGroup_rec.con
 687 cic:/matita/algebra/semigroups/SemiGroup_ind.con
 688 cic:/matita/algebra/semigroups/SemiGroup.ind
 689 cic:/matita/algebra/semigroups/Magma_rect.con
 690 cic:/matita/algebra/semigroups/Magma_rec.con
 691 cic:/matita/algebra/semigroups/Magma_ind.con
 692 cic:/matita/algebra/semigroups/Magma.ind
 693 cic:/matita/datatypes/bool/true_to_true_to_andb_true.con
 694 cic:/matita/datatypes/bool/orb_sym.con
 695 cic:/matita/datatypes/bool/orb_elim.con
 696 cic:/matita/datatypes/bool/orb.con
 697 cic:/matita/datatypes/bool/notb_notb.con
 698 cic:/matita/datatypes/bool/notb_elim.con
 699 cic:/matita/datatypes/bool/notb.con
 700 cic:/matita/datatypes/bool/not_eq_true_false.con
 701 cic:/matita/datatypes/bool/injective_notb.con
 702 cic:/matita/datatypes/bool/if_then_else.con
 703 cic:/matita/datatypes/bool/bool_to_decidable_eq.con
 704 cic:/matita/datatypes/bool/bool_rect.con
 705 cic:/matita/datatypes/bool/bool_rec.con
 706 cic:/matita/datatypes/bool/bool_ind.con
 707 cic:/matita/datatypes/bool/bool_elim.con
 708 cic:/matita/datatypes/bool/bool.ind
 709 cic:/matita/datatypes/bool/andb_true_true_r.con
 710 cic:/matita/datatypes/bool/andb_true_true.con
 711 cic:/matita/datatypes/bool/andb_sym.con
 712 cic:/matita/datatypes/bool/andb_elim.con
 713 cic:/matita/datatypes/bool/andb_assoc.con
 714 cic:/matita/datatypes/bool/andb.con
 715 cic:/matita/datatypes/bool/and_true.con
 716 cic:/matita/datatypes/bool/P_x_to_P_x_to_eq.con
 717 cic:/matita/datatypes/compare/compare_rect.con
 718 cic:/matita/datatypes/compare/compare_rec.con
 719 cic:/matita/datatypes/compare/compare_invert.con
 720 cic:/matita/datatypes/compare/compare_ind.con
 721 cic:/matita/datatypes/compare/compare.ind
 722 cic:/matita/datatypes/constructors/void_rect.con
 723 cic:/matita/datatypes/constructors/void_rec.con
 724 cic:/matita/datatypes/constructors/void_ind.con
 725 cic:/matita/datatypes/constructors/void.ind
 726 cic:/matita/datatypes/constructors/unit_rect.con
 727 cic:/matita/datatypes/constructors/unit_rec.con
 728 cic:/matita/datatypes/constructors/unit_ind.con
 729 cic:/matita/datatypes/constructors/unit.ind
 730 cic:/matita/datatypes/constructors/snd.con
 731 cic:/matita/datatypes/constructors/option_rect.con
 732 cic:/matita/datatypes/constructors/option_rec.con
 733 cic:/matita/datatypes/constructors/option_ind.con
 734 cic:/matita/datatypes/constructors/option.ind
 735 cic:/matita/datatypes/constructors/fst.con
 736 cic:/matita/datatypes/constructors/eq_pair_fst_snd.con
 737 cic:/matita/datatypes/constructors/Sum_rect.con
 738 cic:/matita/datatypes/constructors/Sum_rec.con
 739 cic:/matita/datatypes/constructors/Sum_ind.con
 740 cic:/matita/datatypes/constructors/Sum.ind
 741 cic:/matita/datatypes/constructors/Prod_rect.con
 742 cic:/matita/datatypes/constructors/Prod_rec.con
 743 cic:/matita/datatypes/constructors/Prod_ind.con
 744 cic:/matita/datatypes/constructors/Prod.ind
 745 cic:/matita/decidable_kit/decidable/reflect_rect.con
 746 cic:/matita/decidable_kit/decidable/reflect_rec.con
 747 cic:/matita/decidable_kit/decidable/reflect_inv.con
 748 cic:/matita/decidable_kit/decidable/reflect_ind.con
 749 cic:/matita/decidable_kit/decidable/reflect.ind
 750 cic:/matita/decidable_kit/decidable/prove_reflect.con
 751 cic:/matita/decidable_kit/decidable/p2bT.con
 752 cic:/matita/decidable_kit/decidable/p2bF.con
 753 cic:/matita/decidable_kit/decidable/orbP.con
 754 cic:/matita/decidable_kit/decidable/orbC.con
 755 cic:/matita/decidable_kit/decidable/orb.con
 756 cic:/matita/decidable_kit/decidable/negbP.con
 757 cic:/matita/decidable_kit/decidable/negb.con
 758 cic:/matita/decidable_kit/decidable/ltb_refl.con
 759 cic:/matita/decidable_kit/decidable/ltb_n_Sm.con
 760 cic:/matita/decidable_kit/decidable/ltbW.con
 761 cic:/matita/decidable_kit/decidable/ltbP.con
 762 cic:/matita/decidable_kit/decidable/ltb.con
 763 cic:/matita/decidable_kit/decidable/ltW.con
 764 cic:/matita/decidable_kit/decidable/ltS.con
 765 cic:/matita/decidable_kit/decidable/ltS'.con
 766 cic:/matita/decidable_kit/decidable/leb_refl.con
 767 cic:/matita/decidable_kit/decidable/leb_eqb.con
 768 cic:/matita/decidable_kit/decidable/lebW.con
 769 cic:/matita/decidable_kit/decidable/lebP.con
 770 cic:/matita/decidable_kit/decidable/idP.con
 771 cic:/matita/decidable_kit/decidable/eq_to_bool.con
 772 cic:/matita/decidable_kit/decidable/congr_S.con
 773 cic:/matita/decidable_kit/decidable/bool_to_eq.con
 774 cic:/matita/decidable_kit/decidable/b2pT.con
 775 cic:/matita/decidable_kit/decidable/b2pF.con
 776 cic:/matita/decidable_kit/decidable/andbPF.con
 777 cic:/matita/decidable_kit/decidable/andbP.con
 778 cic:/matita/decidable_kit/decidable/andb.con
 779 cic:/matita/decidable_kit/eqtype/test_canonical_option_eqType.con
 780 cic:/matita/decidable_kit/eqtype/sval.con
 781 cic:/matita/decidable_kit/eqtype/sub_eqType.con
 782 cic:/matita/decidable_kit/eqtype/sprop.con
 783 cic:/matita/decidable_kit/eqtype/sort_OF_nat.con
 784 cic:/matita/decidable_kit/eqtype/sort_OF_bool.con
 785 cic:/matita/decidable_kit/eqtype/sort.con
 786 cic:/matita/decidable_kit/eqtype/sigma_rect.con
 787 cic:/matita/decidable_kit/eqtype/sigma_rec.con
 788 cic:/matita/decidable_kit/eqtype/sigma_ind.con
 789 cic:/matita/decidable_kit/eqtype/sigma_eq_dec.con
 790 cic:/matita/decidable_kit/eqtype/sigma.ind
 791 cic:/matita/decidable_kit/eqtype/option_eqType.con
 792 cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con
 793 cic:/matita/decidable_kit/eqtype/ocmpP.con
 794 cic:/matita/decidable_kit/eqtype/ocmp.con
 795 cic:/matita/decidable_kit/eqtype/nat_eqType.con
 796 cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con
 797 cic:/matita/decidable_kit/eqtype/in_sub_rect.con
 798 cic:/matita/decidable_kit/eqtype/in_sub_rec.con
 799 cic:/matita/decidable_kit/eqtype/in_sub_inv.con
 800 cic:/matita/decidable_kit/eqtype/in_sub_ind.con
 801 cic:/matita/decidable_kit/eqtype/in_sub_eq.con
 802 cic:/matita/decidable_kit/eqtype/in_sub.ind
 803 cic:/matita/decidable_kit/eqtype/if_p.con
 804 cic:/matita/decidable_kit/eqtype/eqbP.con
 805 cic:/matita/decidable_kit/eqtype/eq_compatible.con
 806 cic:/matita/decidable_kit/eqtype/eqType_rect.con
 807 cic:/matita/decidable_kit/eqtype/eqType_rec.con
 808 cic:/matita/decidable_kit/eqtype/eqType_ind.con
 809 cic:/matita/decidable_kit/eqtype/eqType_decidable.con
 810 cic:/matita/decidable_kit/eqtype/eqType.ind
 811 cic:/matita/decidable_kit/eqtype/eqP.con
 812 cic:/matita/decidable_kit/eqtype/cmp_refl.con
 813 cic:/matita/decidable_kit/eqtype/cmpP.con
 814 cic:/matita/decidable_kit/eqtype/cmpC.con
 815 cic:/matita/decidable_kit/eqtype/cmp.con
 816 cic:/matita/decidable_kit/eqtype/bool_eqType.con
 817 cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con
 818 cic:/matita/decidable_kit/eqtype/bcmpP.con
 819 cic:/matita/decidable_kit/eqtype/bcmp.con
 820 cic:/matita/decidable_kit/fgraph/uniq_infgraphseq.con
 821 cic:/matita/decidable_kit/fgraph/setA.con
 822 cic:/matita/decidable_kit/fgraph/orb_refl.con
 823 cic:/matita/decidable_kit/fgraph/multss.con
 824 cic:/matita/decidable_kit/fgraph/multes.con
 825 cic:/matita/decidable_kit/fgraph/mkpermr.con
 826 cic:/matita/decidable_kit/fgraph/mem_multss.con
 827 cic:/matita/decidable_kit/fgraph/mem_multes.con
 828 cic:/matita/decidable_kit/fgraph/mem_mkpermr_size.con
 829 cic:/matita/decidable_kit/fgraph/mem_infgraphseq.con
 830 cic:/matita/decidable_kit/fgraph/mem_concat.con
 831 cic:/matita/decidable_kit/fgraph/iter.con
 832 cic:/matita/decidable_kit/fgraph/infgraphseq.con
 833 cic:/matita/decidable_kit/fgraph/infgraph_spec_rect.con
 834 cic:/matita/decidable_kit/fgraph/infgraph_spec_rec.con
 835 cic:/matita/decidable_kit/fgraph/infgraph_spec_inv.con
 836 cic:/matita/decidable_kit/fgraph/infgraph_spec_ind.con
 837 cic:/matita/decidable_kit/fgraph/infgraph_spec.ind
 838 cic:/matita/decidable_kit/fgraph/infgraphP.con
 839 cic:/matita/decidable_kit/fgraph/infgraph.con
 840 cic:/matita/decidable_kit/fgraph/fval_eqE.con
 841 cic:/matita/decidable_kit/fgraph/fval.con
 842 cic:/matita/decidable_kit/fgraph/fproof.con
 843 cic:/matita/decidable_kit/fgraph/fgraph_eqType.con
 844 cic:/matita/decidable_kit/fgraph/fgraph_eqP.con
 845 cic:/matita/decidable_kit/fgraph/fgraph_default.con
 846 cic:/matita/decidable_kit/fgraph/fgraphType_rect.con
 847 cic:/matita/decidable_kit/fgraph/fgraphType_rec.con
 848 cic:/matita/decidable_kit/fgraph/fgraphType_ind.con
 849 cic:/matita/decidable_kit/fgraph/fgraphType.ind
 850 cic:/matita/decidable_kit/fgraph/count_setA.con
 851 cic:/matita/decidable_kit/fintype/uniq_tail.con
 852 cic:/matita/decidable_kit/fintype/uniq_mem.con
 853 cic:/matita/decidable_kit/fintype/uniq_fintype_enum.con
 854 cic:/matita/decidable_kit/fintype/uniqP.con
 855 cic:/matita/decidable_kit/fintype/uniq.con
 856 cic:/matita/decidable_kit/fintype/sub_finType.con
 857 cic:/matita/decidable_kit/fintype/sub_enumP.con
 858 cic:/matita/decidable_kit/fintype/segment_finType.con
 859 cic:/matita/decidable_kit/fintype/segment_enum.con
 860 cic:/matita/decidable_kit/fintype/segment.con
 861 cic:/matita/decidable_kit/fintype/mem_finType.con
 862 cic:/matita/decidable_kit/fintype/mem_filter.con
 863 cic:/matita/decidable_kit/fintype/is_some.con
 864 cic:/matita/decidable_kit/fintype/iota_ltb.con
 865 cic:/matita/decidable_kit/fintype/fsort.con
 866 cic:/matita/decidable_kit/fintype/finType_rect.con
 867 cic:/matita/decidable_kit/fintype/finType_rec.con
 868 cic:/matita/decidable_kit/fintype/finType_ind.con
 869 cic:/matita/decidable_kit/fintype/finType.ind
 870 cic:/matita/decidable_kit/fintype/filter.con
 871 cic:/matita/decidable_kit/fintype/enum_uniq.con
 872 cic:/matita/decidable_kit/fintype/enum.con
 873 cic:/matita/decidable_kit/fintype/count_O_mem.con
 874 cic:/matita/decidable_kit/fintype/count_O.con
 875 cic:/matita/decidable_kit/fintype/andbC.con
 876 cic:/matita/decidable_kit/fintype/andbA.con
 877 cic:/matita/decidable_kit/fintype/Type_OF_finType.con
 878 cic:/matita/decidable_kit/list_aux/mem.con
 879 cic:/matita/decidable_kit/list_aux/list_eqType.con
 880 cic:/matita/decidable_kit/list_aux/lcmp_length.con
 881 cic:/matita/decidable_kit/list_aux/lcmpP.con
 882 cic:/matita/decidable_kit/list_aux/lcmp.con
 883 cic:/matita/decidable_kit/list_aux/count.con
 884 cic:/matita/decidable_kit/streicher/stepH.con
 885 cic:/matita/decidable_kit/streicher/step.con
 886 cic:/matita/decidable_kit/streicher/pirrel.con
 887 cic:/matita/decidable_kit/streicher/nu_k.con
 888 cic:/matita/decidable_kit/streicher/nu_inv.con
 889 cic:/matita/decidable_kit/streicher/nu.con
 890 cic:/matita/decidable_kit/streicher/decT.con
 891 cic:/matita/decidable_kit/streicher/cancel_nu_nu_inv.con
 892 cic:/matita/decidable_kit/streicher/cancel.con
 893 cic:/matita/demo/power_derivative/monomio_product.con
 894 cic:/matita/demo/power_derivative/monomio.con
 895 cic:/matita/demo/power_derivative/inj.con
 896 cic:/matita/demo/power_derivative/f_eq_extensional.con
 897 cic:/matita/demo/power_derivative/derivative_x1.con
 898 cic:/matita/demo/power_derivative/derivative_x0.con
 899 cic:/matita/demo/power_derivative/derivative_power.con
 900 cic:/matita/demo/power_derivative/derivative_power'.con
 901 cic:/matita/demo/power_derivative/derivative_mult.con
 902 cic:/matita/demo/power_derivative/derivative.con
 903 cic:/matita/demo/power_derivative/costante_sum.con
 904 cic:/matita/demo/power_derivative/costante.con
 905 cic:/matita/demo/power_derivative/Rpower.con
 906 cic:/matita/demo/power_derivative/Rplus_comm.con
 907 cic:/matita/demo/power_derivative/Rplus_assoc.con
 908 cic:/matita/demo/power_derivative/Rplus_Rzero_x.con
 909 cic:/matita/demo/power_derivative/Rplus.con
 910 cic:/matita/demo/power_derivative/Rmult_comm.con
 911 cic:/matita/demo/power_derivative/Rmult_assoc.con
 912 cic:/matita/demo/power_derivative/Rmult_Rzero_x.con
 913 cic:/matita/demo/power_derivative/Rmult_Rplus_distr.con
 914 cic:/matita/demo/power_derivative/Rmult_Rone_x.con
 915 cic:/matita/demo/power_derivative/Rmult.con
 916 cic:/matita/demo/power_derivative/R1.con
 917 cic:/matita/demo/power_derivative/R0.con
 918 cic:/matita/demo/power_derivative/R.con
 919 cic:/matita/demo/power_derivative/Fplus.con
 920 cic:/matita/demo/power_derivative/Fmult_zero_f.con
 921 cic:/matita/demo/power_derivative/Fmult_one_f.con
 922 cic:/matita/demo/power_derivative/Fmult_commutative.con
 923 cic:/matita/demo/power_derivative/Fmult_associative.con
 924 cic:/matita/demo/power_derivative/Fmult_Fplus_distr.con
 925 cic:/matita/demo/power_derivative/Fmult.con
 926 cic:/matita/demo/propositional_sequent_calculus/weakeningR.con
 927 cic:/matita/demo/propositional_sequent_calculus/transitiveb_same_atom.con
 928 cic:/matita/demo/propositional_sequent_calculus/transitiveb.con
 929 cic:/matita/demo/propositional_sequent_calculus/symmetricb_same_atom.con
 930 cic:/matita/demo/propositional_sequent_calculus/symmetricb_eqb.con
 931 cic:/matita/demo/propositional_sequent_calculus/symmetricb.con
 932 cic:/matita/demo/propositional_sequent_calculus/symm_orb.con
 933 cic:/matita/demo/propositional_sequent_calculus/symm_andb.con
 934 cic:/matita/demo/propositional_sequent_calculus/soundness.con
 935 cic:/matita/demo/propositional_sequent_calculus/sizel_0_no_axiom_is_tautology.con
 936 cic:/matita/demo/propositional_sequent_calculus/sizel.con
 937 cic:/matita/demo/propositional_sequent_calculus/size_of_sequent.con
 938 cic:/matita/demo/propositional_sequent_calculus/size.con
 939 cic:/matita/demo/propositional_sequent_calculus/sequent.con
 940 cic:/matita/demo/propositional_sequent_calculus/same_atom_to_exists.con
 941 cic:/matita/demo/propositional_sequent_calculus/same_atom_to_eq.con
 942 cic:/matita/demo/propositional_sequent_calculus/same_atom.con
 943 cic:/matita/demo/propositional_sequent_calculus/orb_not_b_b.con
 944 cic:/matita/demo/propositional_sequent_calculus/or_of_list_permut.con
 945 cic:/matita/demo/propositional_sequent_calculus/or_of_list.con
 946 cic:/matita/demo/propositional_sequent_calculus/not_nf_inv.con
 947 cic:/matita/demo/propositional_sequent_calculus/not_nf_ind.con
 948 cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con
 949 cic:/matita/demo/propositional_sequent_calculus/not_nf.ind
 950 cic:/matita/demo/propositional_sequent_calculus/not_eq_nil_append_cons.con
 951 cic:/matita/demo/propositional_sequent_calculus/negate.con
 952 cic:/matita/demo/propositional_sequent_calculus/mem_to_exists_l1_l2.con
 953 cic:/matita/demo/propositional_sequent_calculus/mem_same_atom_to_exists.con
 954 cic:/matita/demo/propositional_sequent_calculus/look_for_axiom.con
 955 cic:/matita/demo/propositional_sequent_calculus/is_tautology.con
 956 cic:/matita/demo/propositional_sequent_calculus/interp.con
 957 cic:/matita/demo/propositional_sequent_calculus/formula_of_sequent.con
 958 cic:/matita/demo/propositional_sequent_calculus/eval.con
 959 cic:/matita/demo/propositional_sequent_calculus/eq_to_eq_mem.con
 960 cic:/matita/demo/propositional_sequent_calculus/eq_plus_n_m_O_to_eq_m_O.con
 961 cic:/matita/demo/propositional_sequent_calculus/eq_notb_notb_b_b.con
 962 cic:/matita/demo/propositional_sequent_calculus/eq_eval_elim_not_eval.con
 963 cic:/matita/demo/propositional_sequent_calculus/elim_not.con
 964 cic:/matita/demo/propositional_sequent_calculus/distributive_orb_andb.con
 965 cic:/matita/demo/propositional_sequent_calculus/distributive_andb_orb.con
 966 cic:/matita/demo/propositional_sequent_calculus/derive_inv.con
 967 cic:/matita/demo/propositional_sequent_calculus/derive_ind.con
 968 cic:/matita/demo/propositional_sequent_calculus/derive.ind
 969 cic:/matita/demo/propositional_sequent_calculus/demorgan2.con
 970 cic:/matita/demo/propositional_sequent_calculus/demorgan1.con
 971 cic:/matita/demo/propositional_sequent_calculus/daemon.con
 972 cic:/matita/demo/propositional_sequent_calculus/completeness_base.con
 973 cic:/matita/demo/propositional_sequent_calculus/associative_andb.con
 974 cic:/matita/demo/propositional_sequent_calculus/assoc_orb.con
 975 cic:/matita/demo/propositional_sequent_calculus/and_of_list_permut.con
 976 cic:/matita/demo/propositional_sequent_calculus/and_of_list.con
 977 cic:/matita/demo/propositional_sequent_calculus/Formula_rect.con
 978 cic:/matita/demo/propositional_sequent_calculus/Formula_rec.con
 979 cic:/matita/demo/propositional_sequent_calculus/Formula_ind.con
 980 cic:/matita/demo/propositional_sequent_calculus/Formula.ind
 981 cic:/matita/demo/realisability/type_OF_SP.con
 982 cic:/matita/demo/realisability/true_impl_realized.con
 983 cic:/matita/demo/realisability/sigma_rect.con
 984 cic:/matita/demo/realisability/sigma_rec.con
 985 cic:/matita/demo/realisability/sigma_ind.con
 986 cic:/matita/demo/realisability/sigma.ind
 987 cic:/matita/demo/realisability/realized.con
 988 cic:/matita/demo/realisability/pi2.con
 989 cic:/matita/demo/realisability/pi1.con
 990 cic:/matita/demo/realisability/modr.con
 991 cic:/matita/demo/realisability/id_axiom.con
 992 cic:/matita/demo/realisability/extraction.con
 993 cic:/matita/demo/realisability/elim_abs.con
 994 cic:/matita/demo/realisability/cut.con
 995 cic:/matita/demo/realisability/correct2.con
 996 cic:/matita/demo/realisability/correct.con
 997 cic:/matita/demo/realisability/and_i.con
 998 cic:/matita/demo/realisability/SP_rect.con
 999 cic:/matita/demo/realisability/SP_rec.con
1000 cic:/matita/demo/realisability/SP_ind.con
1001 cic:/matita/demo/realisability/SP.ind
1002 cic:/matita/demo/realisability/Prop_OF_SP.con
1003 cic:/matita/higher_order_defs/functions/symmetric2.con
1004 cic:/matita/higher_order_defs/functions/symmetric.con
1005 cic:/matita/higher_order_defs/functions/surjective.con
1006 cic:/matita/higher_order_defs/functions/monotonic.con
1007 cic:/matita/higher_order_defs/functions/injective.con
1008 cic:/matita/higher_order_defs/functions/eq_f_g_h.con
1009 cic:/matita/higher_order_defs/functions/distributive2.con
1010 cic:/matita/higher_order_defs/functions/distributive.con
1011 cic:/matita/higher_order_defs/functions/compose.con
1012 cic:/matita/higher_order_defs/functions/associative.con
1013 cic:/matita/higher_order_defs/ordering/antisymmetric.con
1014 cic:/matita/higher_order_defs/relations/transitive.con
1015 cic:/matita/higher_order_defs/relations/tight_apart.con
1016 cic:/matita/higher_order_defs/relations/symmetric.con
1017 cic:/matita/higher_order_defs/relations/relation.con
1018 cic:/matita/higher_order_defs/relations/reflexive.con
1019 cic:/matita/higher_order_defs/relations/irreflexive.con
1020 cic:/matita/higher_order_defs/relations/cotransitive.con
1021 cic:/matita/higher_order_defs/relations/antisymmetric.con
1022 cic:/matita/list/in/not_in_list_nil.con
1023 cic:/matita/list/in/mem_true_to_in_list.con
1024 cic:/matita/list/in/mem.con
1025 cic:/matita/list/in/incl_A_A.con
1026 cic:/matita/list/in/incl.con
1027 cic:/matita/list/in/in_list_to_mem_true.con
1028 cic:/matita/list/in/in_list_to_in_list_append_r.con
1029 cic:/matita/list/in/in_list_to_in_list_append_l.con
1030 cic:/matita/list/in/in_list_tail.con
1031 cic:/matita/list/in/in_list_singleton_to_eq.con
1032 cic:/matita/list/in/in_list_inv.con
1033 cic:/matita/list/in/in_list_ind.con
1034 cic:/matita/list/in/in_list_filter_to_p_true.con
1035 cic:/matita/list/in/in_list_filter_r.con
1036 cic:/matita/list/in/in_list_filter.con
1037 cic:/matita/list/in/in_list_cons_case.con
1038 cic:/matita/list/in/in_list_append_to_or_in_list.con
1039 cic:/matita/list/in/in_list.ind
1040 cic:/matita/list/list/x3.con
1041 cic:/matita/list/list/x2.con
1042 cic:/matita/list/list/x1.con
1043 cic:/matita/list/list/tmp.con
1044 cic:/matita/list/list/tail.con
1045 cic:/matita/list/list/permutation_inv.con
1046 cic:/matita/list/list/permutation_ind.con
1047 cic:/matita/list/list/permutation.ind
1048 cic:/matita/list/list/permut1_inv.con
1049 cic:/matita/list/list/permut1_ind.con
1050 cic:/matita/list/list/nth.con
1051 cic:/matita/list/list/nil_cons.con
1052 cic:/matita/list/list/map.con
1053 cic:/matita/list/list/list_rect.con
1054 cic:/matita/list/list/list_rec.con
1055 cic:/matita/list/list/list_ind2.con
1056 cic:/matita/list/list/list_ind.con
1057 cic:/matita/list/list/list.ind
1058 cic:/matita/list/list/length.con
1059 cic:/matita/list/list/le_length_filter.con
1060 cic:/matita/list/list/iota.con
1061 cic:/matita/list/list/id_list.con
1062 cic:/matita/list/list/foldr.con
1063 cic:/matita/list/list/filter.con
1064 cic:/matita/list/list/eq_map.con
1065 cic:/matita/list/list/cons_append_commute.con
1066 cic:/matita/list/list/associative_append.con
1067 cic:/matita/list/list/append_nil.con
1068 cic:/matita/list/list/append_cons.con
1069 cic:/matita/list/list/append.con
1070 cic:/matita/list/sort/sorted_to_minimum.con
1071 cic:/matita/list/sort/sorted_to_eq_sorted_b_true.con
1072 cic:/matita/list/sort/sorted_inv.con
1073 cic:/matita/list/sort/sorted_ind.con
1074 cic:/matita/list/sort/sorted_cons_to_sorted.con
1075 cic:/matita/list/sort/sorted.ind
1076 cic:/matita/list/sort/ordered_injective.con
1077 cic:/matita/list/sort/ordered.con
1078 cic:/matita/list/sort/insertionsort_sorted.con
1079 cic:/matita/list/sort/insertionsort.con
1080 cic:/matita/list/sort/insert_sorted.con
1081 cic:/matita/list/sort/insert_ind.con
1082 cic:/matita/list/sort/insert.con
1083 cic:/matita/logic/coimplication/iff_trans.con
1084 cic:/matita/logic/coimplication/iff_sym.con
1085 cic:/matita/logic/coimplication/iff_refl.con
1086 cic:/matita/logic/coimplication/iff_intro.con
1087 cic:/matita/logic/coimplication/Iff.con
1088 cic:/matita/logic/connectives/proj2.con
1089 cic:/matita/logic/connectives/proj1.con
1090 cic:/matita/logic/connectives/iff.con
1091 cic:/matita/logic/connectives/ex_ind.con
1092 cic:/matita/logic/connectives/ex2_ind.con
1093 cic:/matita/logic/connectives/ex2.ind
1094 cic:/matita/logic/connectives/ex.ind
1095 cic:/matita/logic/connectives/decidable.con
1096 cic:/matita/logic/connectives/absurd.con
1097 cic:/matita/logic/connectives/True_rect.con
1098 cic:/matita/logic/connectives/True_rec.con
1099 cic:/matita/logic/connectives/True_ind.con
1100 cic:/matita/logic/connectives/True.ind
1101 cic:/matita/logic/connectives/Or_ind.con
1102 cic:/matita/logic/connectives/Or_ind'.con
1103 cic:/matita/logic/connectives/Or.ind
1104 cic:/matita/logic/connectives/Not.con
1105 cic:/matita/logic/connectives/False_rect.con
1106 cic:/matita/logic/connectives/False_rec.con
1107 cic:/matita/logic/connectives/False_ind.con
1108 cic:/matita/logic/connectives/False.ind
1109 cic:/matita/logic/connectives/And_rect.con
1110 cic:/matita/logic/connectives/And_rec.con
1111 cic:/matita/logic/connectives/And_ind.con
1112 cic:/matita/logic/connectives/And.ind
1113 cic:/matita/logic/connectives2/transitive_iff.con
1114 cic:/matita/logic/connectives2/symmetric_iff.con
1115 cic:/matita/logic/connectives2/reflexive_iff.con
1116 cic:/matita/logic/equality/transitive_eq.con
1117 cic:/matita/logic/equality/trans_sym_eq.con
1118 cic:/matita/logic/equality/trans_eq.con
1119 cic:/matita/logic/equality/symmetric_eq.con
1120 cic:/matita/logic/equality/sym_eq.con
1121 cic:/matita/logic/equality/reflexive_eq.con
1122 cic:/matita/logic/equality/nu_left_inv.con
1123 cic:/matita/logic/equality/nu_inv.con
1124 cic:/matita/logic/equality/nu_constant.con
1125 cic:/matita/logic/equality/nu.con
1126 cic:/matita/logic/equality/eq_to_eq_to_eq_p_q.con
1127 cic:/matita/logic/equality/eq_rect.con
1128 cic:/matita/logic/equality/eq_rect'.con
1129 cic:/matita/logic/equality/eq_rec.con
1130 cic:/matita/logic/equality/eq_ind.con
1131 cic:/matita/logic/equality/eq_f2.con
1132 cic:/matita/logic/equality/eq_f.con
1133 cic:/matita/logic/equality/eq_f'.con
1134 cic:/matita/logic/equality/eq_elim_r.con
1135 cic:/matita/logic/equality/eq_elim_r'.con
1136 cic:/matita/logic/equality/eq_elim_r''.con
1137 cic:/matita/logic/equality/eq_OF_eq2.con
1138 cic:/matita/logic/equality/eq_OF_eq1.con
1139 cic:/matita/logic/equality/eq_OF_eq.con
1140 cic:/matita/logic/equality/eq.ind
1141 cic:/matita/logic/equality/comp.con
1142 cic:/matita/nat/bertrand/tech3.con
1143 cic:/matita/nat/bertrand/tech1.con
1144 cic:/matita/nat/bertrand/tech.con
1145 cic:/matita/nat/bertrand/sorted_lt.con
1146 cic:/matita/nat/bertrand/sorted_list_n_aux.con
1147 cic:/matita/nat/bertrand/sorted_gt.con
1148 cic:/matita/nat/bertrand/sieve_sound2.con
1149 cic:/matita/nat/bertrand/sieve_sound1.con
1150 cic:/matita/nat/bertrand/sieve_sorted.con
1151 cic:/matita/nat/bertrand/sieve_prime.con
1152 cic:/matita/nat/bertrand/sieve_aux.con
1153 cic:/matita/nat/bertrand/sieve.con
1154 cic:/matita/nat/bertrand/not_not_bertrand_to_bertrand1.con
1155 cic:/matita/nat/bertrand/not_not_bertrand_to_bertrand.con
1156 cic:/matita/nat/bertrand/not_bertrand_to_le_B.con
1157 cic:/matita/nat/bertrand/not_bertrand_to_le2.con
1158 cic:/matita/nat/bertrand/not_bertrand_to_le1.con
1159 cic:/matita/nat/bertrand/not_bertrand.con
1160 cic:/matita/nat/bertrand/min_prim.con
1161 cic:/matita/nat/bertrand/lt_to_div_O.con
1162 cic:/matita/nat/bertrand/lt_div_to_times.con
1163 cic:/matita/nat/bertrand/lt_div_S_div.con
1164 cic:/matita/nat/bertrand/lprim.con
1165 cic:/matita/nat/bertrand/list_of_primes_to_bertrand.con
1166 cic:/matita/nat/bertrand/list_of_primes.con
1167 cic:/matita/nat/bertrand/list_n_aux.con
1168 cic:/matita/nat/bertrand/list_n.con
1169 cic:/matita/nat/bertrand/list_divides.con
1170 cic:/matita/nat/bertrand/le_to_bertrand2.con
1171 cic:/matita/nat/bertrand/le_to_bertrand.con
1172 cic:/matita/nat/bertrand/le_times_div_m_m.con
1173 cic:/matita/nat/bertrand/le_list_n_r.con
1174 cic:/matita/nat/bertrand/le_list_n_aux_r.con
1175 cic:/matita/nat/bertrand/le_list_n_aux_k_k.con
1176 cic:/matita/nat/bertrand/le_list_n_aux.con
1177 cic:/matita/nat/bertrand/le_list_n.con
1178 cic:/matita/nat/bertrand/le_length_list_n.con
1179 cic:/matita/nat/bertrand/le_k.con
1180 cic:/matita/nat/bertrand/le_SSO_list_n.con
1181 cic:/matita/nat/bertrand/le_B_split2_exp.con
1182 cic:/matita/nat/bertrand/le_B_split1_teta.con
1183 cic:/matita/nat/bertrand/k1.con
1184 cic:/matita/nat/bertrand/k.con
1185 cic:/matita/nat/bertrand/in_list_sieve_to_prime.con
1186 cic:/matita/nat/bertrand/in_list_sieve_to_leq.con
1187 cic:/matita/nat/bertrand/in_list_SSO_list_n.con
1188 cic:/matita/nat/bertrand/exp_plus_SSO.con
1189 cic:/matita/nat/bertrand/eq_B_B1.con
1190 cic:/matita/nat/bertrand/eq_B1_times_B_split1_B_split2.con
1191 cic:/matita/nat/bertrand/divides_to_prime_divides.con
1192 cic:/matita/nat/bertrand/checker_sound.con
1193 cic:/matita/nat/bertrand/checker_cons.con
1194 cic:/matita/nat/bertrand/checker.con
1195 cic:/matita/nat/bertrand/check_list2.con
1196 cic:/matita/nat/bertrand/check_list1.con
1197 cic:/matita/nat/bertrand/check_list.con
1198 cic:/matita/nat/bertrand/bertrand_n.con
1199 cic:/matita/nat/bertrand/bertrand.con
1200 cic:/matita/nat/bertrand/B_split2.con
1201 cic:/matita/nat/bertrand/B_split1.con
1202 cic:/matita/nat/bertrand/B1.con
1203 cic:/matita/nat/binomial/lt_O_bc.con
1204 cic:/matita/nat/binomial/fact_minus.con
1205 cic:/matita/nat/binomial/exp_plus_sigma_p.con
1206 cic:/matita/nat/binomial/exp_Sn_SSO.con
1207 cic:/matita/nat/binomial/exp_S_sigma_p.con
1208 cic:/matita/nat/binomial/bc_n_n.con
1209 cic:/matita/nat/binomial/bc_n_O.con
1210 cic:/matita/nat/binomial/bc2.con
1211 cic:/matita/nat/binomial/bc1.con
1212 cic:/matita/nat/binomial/bc.con
1213 cic:/matita/nat/chebyshev/times_SSO_pred.con
1214 cic:/matita/nat/chebyshev/sigma_p_divides_b1.con
1215 cic:/matita/nat/chebyshev/sigma_p_divides_b.con
1216 cic:/matita/nat/chebyshev/prim.con
1217 cic:/matita/nat/chebyshev/pi_p_primeb_divides_b.con
1218 cic:/matita/nat/chebyshev/pi_p_primeb5.con
1219 cic:/matita/nat/chebyshev/pi_p_primeb4.con
1220 cic:/matita/nat/chebyshev/pi_p_primeb1.con
1221 cic:/matita/nat/chebyshev/pi_p_primeb.con
1222 cic:/matita/nat/chebyshev/not_prime_times_SSO.con
1223 cic:/matita/nat/chebyshev/monotonic_A.con
1224 cic:/matita/nat/chebyshev/lt_max_to_pi_p_primeb.con
1225 cic:/matita/nat/chebyshev/lt_SSSSO_to_le_B_exp.con
1226 cic:/matita/nat/chebyshev/lt_SSSSO_to_le_A_exp.con
1227 cic:/matita/nat/chebyshev/lt_SO_to_le_exp_B.con
1228 cic:/matita/nat/chebyshev/lt_SO_to_le_B_exp.con
1229 cic:/matita/nat/chebyshev/le_primr.con
1230 cic:/matita/nat/chebyshev/le_priml1.con
1231 cic:/matita/nat/chebyshev/le_priml.con
1232 cic:/matita/nat/chebyshev/le_prim_n3.con
1233 cic:/matita/nat/chebyshev/le_prim_n2.con
1234 cic:/matita/nat/chebyshev/le_prim_n1.con
1235 cic:/matita/nat/chebyshev/le_prim_n.con
1236 cic:/matita/nat/chebyshev/le_prim_log.con
1237 cic:/matita/nat/chebyshev/le_pred.con
1238 cic:/matita/nat/chebyshev/le_ord_log.con
1239 cic:/matita/nat/chebyshev/le_n_SSSSSSSSO_to_le_A_exp.con
1240 cic:/matita/nat/chebyshev/le_fact_A.con
1241 cic:/matita/nat/chebyshev/le_exp_primr.con
1242 cic:/matita/nat/chebyshev/le_exp_priml.con
1243 cic:/matita/nat/chebyshev/le_exp_prim4l.con
1244 cic:/matita/nat/chebyshev/le_exp_B.con
1245 cic:/matita/nat/chebyshev/le_S_times_SSO.con
1246 cic:/matita/nat/chebyshev/le_B_exp.con
1247 cic:/matita/nat/chebyshev/le_B_A4.con
1248 cic:/matita/nat/chebyshev/le_B_A.con
1249 cic:/matita/nat/chebyshev/le_Al1.con
1250 cic:/matita/nat/chebyshev/le_Al.con
1251 cic:/matita/nat/chebyshev/le_A_exp5.con
1252 cic:/matita/nat/chebyshev/le_A_exp4.con
1253 cic:/matita/nat/chebyshev/le_A_exp1.con
1254 cic:/matita/nat/chebyshev/le_A_exp.con
1255 cic:/matita/nat/chebyshev/le_A_BA1.con
1256 cic:/matita/nat/chebyshev/le_A_BA.con
1257 cic:/matita/nat/chebyshev/leA_r2.con
1258 cic:/matita/nat/chebyshev/leA_prim.con
1259 cic:/matita/nat/chebyshev/fact_pi_p3.con
1260 cic:/matita/nat/chebyshev/fact_pi_p2.con
1261 cic:/matita/nat/chebyshev/fact_pi_p.con
1262 cic:/matita/nat/chebyshev/exp_fact_SSO.con
1263 cic:/matita/nat/chebyshev/eq_sigma_pi_SO_n.con
1264 cic:/matita/nat/chebyshev/eq_sigma_p_div.con
1265 cic:/matita/nat/chebyshev/eq_prim_prim_pred.con
1266 cic:/matita/nat/chebyshev/eq_pi_p_primeb_divides_b.con
1267 cic:/matita/nat/chebyshev/eq_ord_sigma_p.con
1268 cic:/matita/nat/chebyshev/eq_fact_pi_p.con
1269 cic:/matita/nat/chebyshev/eq_fact_B.con
1270 cic:/matita/nat/chebyshev/eq_A_SSO_n.con
1271 cic:/matita/nat/chebyshev/eq_A_A'.con
1272 cic:/matita/nat/chebyshev/B_SSSSSSSSO.con
1273 cic:/matita/nat/chebyshev/B_SSSSSSSO.con
1274 cic:/matita/nat/chebyshev/B_SSSSSSO.con
1275 cic:/matita/nat/chebyshev/B_SSSSSO.con
1276 cic:/matita/nat/chebyshev/B_SSSSO.con
1277 cic:/matita/nat/chebyshev/B_SSSO.con
1278 cic:/matita/nat/chebyshev/B.con
1279 cic:/matita/nat/chebyshev/A_SSSSO.con
1280 cic:/matita/nat/chebyshev/A_SSSO.con
1281 cic:/matita/nat/chebyshev/A_SSO.con
1282 cic:/matita/nat/chebyshev/A_SO.con
1283 cic:/matita/nat/chebyshev/A.con
1284 cic:/matita/nat/chebyshev/A'.con
1285 cic:/matita/nat/chebyshev_teta/teta_pred.con
1286 cic:/matita/nat/chebyshev_teta/teta_pi_p_teta.con
1287 cic:/matita/nat/chebyshev_teta/teta.con
1288 cic:/matita/nat/chebyshev_teta/prime_to_divides_M.con
1289 cic:/matita/nat/chebyshev_teta/lt_O_to_le_teta_exp_teta.con
1290 cic:/matita/nat/chebyshev_teta/lt_O_teta.con
1291 cic:/matita/nat/chebyshev_teta/lt_M.con
1292 cic:/matita/nat/chebyshev_teta/le_teta_M_teta.con
1293 cic:/matita/nat/chebyshev_teta/le_teta.con
1294 cic:/matita/nat/chebyshev_teta/divides_pi_p_M1.con
1295 cic:/matita/nat/chebyshev_teta/divides_pi_p_M.con
1296 cic:/matita/nat/chebyshev_teta/divides_fact_to_le.con
1297 cic:/matita/nat/chebyshev_teta/divides_fact_to_divides.con
1298 cic:/matita/nat/chebyshev_teta/div_teta_teta.con
1299 cic:/matita/nat/chebyshev_teta/M.con
1300 cic:/matita/nat/chebyshev_thm/theta_pi.con
1301 cic:/matita/nat/chebyshev_thm/log_pi_p.con
1302 cic:/matita/nat/chebyshev_thm/le_log_C2_sigma_p.con
1303 cic:/matita/nat/chebyshev_thm/jj.con
1304 cic:/matita/nat/chebyshev_thm/daemon.con
1305 cic:/matita/nat/chebyshev_thm/asdasd.con
1306 cic:/matita/nat/chebyshev_thm/C2.con
1307 cic:/matita/nat/chebyshev_thm/C1.con
1308 cic:/matita/nat/chebyshev_thm/C.con
1309 cic:/matita/nat/chinese_reminder/mod_cr_pair.con
1310 cic:/matita/nat/chinese_reminder/cr_pair4.con
1311 cic:/matita/nat/chinese_reminder/cr_pair3.con
1312 cic:/matita/nat/chinese_reminder/cr_pair2.con
1313 cic:/matita/nat/chinese_reminder/cr_pair1.con
1314 cic:/matita/nat/chinese_reminder/cr_pair.con
1315 cic:/matita/nat/chinese_reminder/and_congruent_congruent_lt.con
1316 cic:/matita/nat/chinese_reminder/and_congruent_congruent.con
1317 cic:/matita/nat/compare/not_eq_to_eqb_false.con
1318 cic:/matita/nat/compare/nat_compare_to_Prop.con
1319 cic:/matita/nat/compare/nat_compare_pred_pred.con
1320 cic:/matita/nat/compare/nat_compare_n_n.con
1321 cic:/matita/nat/compare/nat_compare_n_m_m_n.con
1322 cic:/matita/nat/compare/nat_compare_elim.con
1323 cic:/matita/nat/compare/nat_compare_S_S.con
1324 cic:/matita/nat/compare/nat_compare.con
1325 cic:/matita/nat/compare/ltb_to_Prop.con
1326 cic:/matita/nat/compare/ltb_elim.con
1327 cic:/matita/nat/compare/ltb.con
1328 cic:/matita/nat/compare/lt_to_leb_false.con
1329 cic:/matita/nat/compare/leb_true_to_le.con
1330 cic:/matita/nat/compare/leb_to_Prop.con
1331 cic:/matita/nat/compare/leb_false_to_not_le.con
1332 cic:/matita/nat/compare/leb_elim.con
1333 cic:/matita/nat/compare/leb.con
1334 cic:/matita/nat/compare/le_to_leb_true.con
1335 cic:/matita/nat/compare/eqb_true_to_eq.con
1336 cic:/matita/nat/compare/eqb_to_Prop.con
1337 cic:/matita/nat/compare/eqb_n_n.con
1338 cic:/matita/nat/compare/eqb_false_to_not_eq.con
1339 cic:/matita/nat/compare/eqb_elim.con
1340 cic:/matita/nat/compare/eqb.con
1341 cic:/matita/nat/compare/eq_to_eqb_true.con
1342 cic:/matita/nat/congruence/transitive_congruent.con
1343 cic:/matita/nat/congruence/mod_times_mod.con
1344 cic:/matita/nat/congruence/mod_times.con
1345 cic:/matita/nat/congruence/mod_mod.con
1346 cic:/matita/nat/congruence/le_to_mod.con
1347 cic:/matita/nat/congruence/eq_times_plus_to_congruent.con
1348 cic:/matita/nat/congruence/divides_to_congruent.con
1349 cic:/matita/nat/congruence/congruent_to_divides.con
1350 cic:/matita/nat/congruence/congruent_times.con
1351 cic:/matita/nat/congruence/congruent_pi.con
1352 cic:/matita/nat/congruence/congruent_n_n.con
1353 cic:/matita/nat/congruence/congruent_n_mod_times.con
1354 cic:/matita/nat/congruence/congruent_n_mod_n.con
1355 cic:/matita/nat/congruence/congruent.con
1356 cic:/matita/nat/congruence/S_mod.con
1357 cic:/matita/nat/count/sigma_times.con
1358 cic:/matita/nat/count/sigma_plus1.con
1359 cic:/matita/nat/count/sigma_plus.con
1360 cic:/matita/nat/count/sigma_f_g.con
1361 cic:/matita/nat/count/eq_sigma_sigma1.con
1362 cic:/matita/nat/count/eq_sigma_sigma.con
1363 cic:/matita/nat/count/count_times.con
1364 cic:/matita/nat/count/count.con
1365 cic:/matita/nat/count/bool_to_nat_andb.con
1366 cic:/matita/nat/count/bool_to_nat.con
1367 cic:/matita/nat/div_and_mod/or_div_mod.con
1368 cic:/matita/nat/div_and_mod/n_divides_aux.con
1369 cic:/matita/nat/div_and_mod/n_divides.con
1370 cic:/matita/nat/div_and_mod/mod_plus_times.con
1371 cic:/matita/nat/div_and_mod/mod_n_n.con
1372 cic:/matita/nat/div_and_mod/mod_aux.con
1373 cic:/matita/nat/div_and_mod/mod_SO.con
1374 cic:/matita/nat/div_and_mod/mod_S.con
1375 cic:/matita/nat/div_and_mod/mod_O_n.con
1376 cic:/matita/nat/div_and_mod/mod.con
1377 cic:/matita/nat/div_and_mod/lt_to_eq_mod.con
1378 cic:/matita/nat/div_and_mod/lt_mod_m_m.con
1379 cic:/matita/nat/div_and_mod/lt_O_to_injective_times_r.con
1380 cic:/matita/nat/div_and_mod/lt_O_to_injective_times_l.con
1381 cic:/matita/nat/div_and_mod/lt_O_to_div_times.con
1382 cic:/matita/nat/div_and_mod/le_mod_aux_m_m.con
1383 cic:/matita/nat/div_and_mod/injective_times_r.con
1384 cic:/matita/nat/div_and_mod/injective_times_l.con
1385 cic:/matita/nat/div_and_mod/inj_times_r1.con
1386 cic:/matita/nat/div_and_mod/inj_times_r.con
1387 cic:/matita/nat/div_and_mod/inj_times_l1.con
1388 cic:/matita/nat/div_and_mod/inj_times_l.con
1389 cic:/matita/nat/div_and_mod/eq_times_div_minus_mod.con
1390 cic:/matita/nat/div_and_mod/eq_div_O.con
1391 cic:/matita/nat/div_and_mod/div_times.con
1392 cic:/matita/nat/div_and_mod/div_plus_times.con
1393 cic:/matita/nat/div_and_mod/div_n_n.con
1394 cic:/matita/nat/div_and_mod/div_mod_spec_to_not_eq_O.con
1395 cic:/matita/nat/div_and_mod/div_mod_spec_to_eq2.con
1396 cic:/matita/nat/div_and_mod/div_mod_spec_to_eq.con
1397 cic:/matita/nat/div_and_mod/div_mod_spec_times.con
1398 cic:/matita/nat/div_and_mod/div_mod_spec_rect.con
1399 cic:/matita/nat/div_and_mod/div_mod_spec_rec.con
1400 cic:/matita/nat/div_and_mod/div_mod_spec_ind.con
1401 cic:/matita/nat/div_and_mod/div_mod_spec_div_mod.con
1402 cic:/matita/nat/div_and_mod/div_mod_spec.ind
1403 cic:/matita/nat/div_and_mod/div_mod.con
1404 cic:/matita/nat/div_and_mod/div_aux_mod_aux.con
1405 cic:/matita/nat/div_and_mod/div_aux.con
1406 cic:/matita/nat/div_and_mod/div_SO.con
1407 cic:/matita/nat/div_and_mod/div.con
1408 cic:/matita/nat/div_and_mod_diseq/monotonic_div.con
1409 cic:/matita/nat/div_and_mod_diseq/lt_times_to_lt_div.con
1410 cic:/matita/nat/div_and_mod_diseq/lt_times_to_lt.con
1411 cic:/matita/nat/div_and_mod_diseq/lt_m_nm.con
1412 cic:/matita/nat/div_and_mod_diseq/lt_div_S.con
1413 cic:/matita/nat/div_and_mod_diseq/lt_div.con
1414 cic:/matita/nat/div_and_mod_diseq/le_times_to_le_div2.con
1415 cic:/matita/nat/div_and_mod_diseq/le_times_to_le_div.con
1416 cic:/matita/nat/div_and_mod_diseq/le_times_div_div_times.con
1417 cic:/matita/nat/div_and_mod_diseq/le_plus_mod.con
1418 cic:/matita/nat/div_and_mod_diseq/le_plus_div.con
1419 cic:/matita/nat/div_and_mod_diseq/le_div_times_m.con
1420 cic:/matita/nat/div_and_mod_diseq/le_div_times_Sm.con
1421 cic:/matita/nat/div_and_mod_diseq/le_div_plus_S.con
1422 cic:/matita/nat/div_and_mod_diseq/le_div_S_S_div.con
1423 cic:/matita/nat/div_and_mod_diseq/le_div.con
1424 cic:/matita/nat/euler_theorem/totient_card_aux.con
1425 cic:/matita/nat/euler_theorem/totient_card.con
1426 cic:/matita/nat/euler_theorem/permut_p_mod.con
1427 cic:/matita/nat/euler_theorem/gcd_pi_p.con
1428 cic:/matita/nat/euler_theorem/congruent_map_iter_p_times.con
1429 cic:/matita/nat/euler_theorem/congruent_exp_totient_SO.con
1430 cic:/matita/nat/euler_theorem/card_Sn.con
1431 cic:/matita/nat/exp/times_exp.con
1432 cic:/matita/nat/exp/monotonic_exp1.con
1433 cic:/matita/nat/exp/lt_m_exp_nm.con
1434 cic:/matita/nat/exp/lt_exp_to_lt1.con
1435 cic:/matita/nat/exp/lt_exp_to_lt.con
1436 cic:/matita/nat/exp/lt_exp1.con
1437 cic:/matita/nat/exp/lt_exp.con
1438 cic:/matita/nat/exp/lt_O_exp.con
1439 cic:/matita/nat/exp/le_exp_to_le1.con
1440 cic:/matita/nat/exp/le_exp_to_le.con
1441 cic:/matita/nat/exp/le_exp.con
1442 cic:/matita/nat/exp/injective_exp_r.con
1443 cic:/matita/nat/exp/inj_exp_r.con
1444 cic:/matita/nat/exp/exp_to_eq_O.con
1445 cic:/matita/nat/exp/exp_plus_times.con
1446 cic:/matita/nat/exp/exp_n_SO.con
1447 cic:/matita/nat/exp/exp_n_O.con
1448 cic:/matita/nat/exp/exp_exp_times.con
1449 cic:/matita/nat/exp/exp_SSO.con
1450 cic:/matita/nat/exp/exp_SO_n.con
1451 cic:/matita/nat/exp/exp.con
1452 cic:/matita/nat/factorial/lt_n_fact_n.con
1453 cic:/matita/nat/factorial/le_n_fact_n.con
1454 cic:/matita/nat/factorial/le_SSO_fact.con
1455 cic:/matita/nat/factorial/le_SO_fact.con
1456 cic:/matita/nat/factorial/fact.con
1457 cic:/matita/nat/factorial2/lt_SSSSO_to_fact.con
1458 cic:/matita/nat/factorial2/lt_O_to_fact1.con
1459 cic:/matita/nat/factorial2/lt_O_fact.con
1460 cic:/matita/nat/factorial2/le_fact_10.con
1461 cic:/matita/nat/factorial2/factS.con
1462 cic:/matita/nat/factorial2/fact3.con
1463 cic:/matita/nat/factorial2/fact2.con
1464 cic:/matita/nat/factorial2/fact1.con
1465 cic:/matita/nat/factorial2/exp_S.con
1466 cic:/matita/nat/factorial2/ab_times_cd.con
1467 cic:/matita/nat/factorization/p_ord_to_lt_max_prime_factor1.con
1468 cic:/matita/nat/factorization/p_ord_to_lt_max_prime_factor.con
1469 cic:/matita/nat/factorization/not_eq_nf_last_nf_cons.con
1470 cic:/matita/nat/factorization/not_eq_nf_cons_O_nf_cons.con
1471 cic:/matita/nat/factorization/not_divides_defactorize_aux.con
1472 cic:/matita/nat/factorization/nat_fact_rect.con
1473 cic:/matita/nat/factorization/nat_fact_rec.con
1474 cic:/matita/nat/factorization/nat_fact_ind.con
1475 cic:/matita/nat/factorization/nat_fact_all_rect.con
1476 cic:/matita/nat/factorization/nat_fact_all_rec.con
1477 cic:/matita/nat/factorization/nat_fact_all_ind.con
1478 cic:/matita/nat/factorization/nat_fact_all.ind
1479 cic:/matita/nat/factorization/nat_fact.ind
1480 cic:/matita/nat/factorization/max_prime_factor_to_not_p_ord_O.con
1481 cic:/matita/nat/factorization/max_prime_factor.con
1482 cic:/matita/nat/factorization/max_p_exponent.con
1483 cic:/matita/nat/factorization/max_p.con
1484 cic:/matita/nat/factorization/lt_max_prime_factor_to_not_divides.con
1485 cic:/matita/nat/factorization/lt_SO_max_prime.con
1486 cic:/matita/nat/factorization/lt_SO_defactorize_aux.con
1487 cic:/matita/nat/factorization/lt_O_defactorize_aux.con
1488 cic:/matita/nat/factorization/injective_defactorize_aux.con
1489 cic:/matita/nat/factorization/injective_defactorize.con
1490 cic:/matita/nat/factorization/factorize_defactorize.con
1491 cic:/matita/nat/factorization/factorize_aux.con
1492 cic:/matita/nat/factorization/factorize.con
1493 cic:/matita/nat/factorization/eq_p_max.con
1494 cic:/matita/nat/factorization/eq_defactorize_aux_to_eq.con
1495 cic:/matita/nat/factorization/divides_to_max_prime_factor1.con
1496 cic:/matita/nat/factorization/divides_to_max_prime_factor.con
1497 cic:/matita/nat/factorization/divides_max_prime_factor_n.con
1498 cic:/matita/nat/factorization/divides_max_p_defactorize.con
1499 cic:/matita/nat/factorization/defactorize_factorize.con
1500 cic:/matita/nat/factorization/defactorize_aux_factorize_aux.con
1501 cic:/matita/nat/factorization/defactorize_aux.con
1502 cic:/matita/nat/factorization/defactorize.con
1503 cic:/matita/nat/fermat_little_theorem/prime_to_not_divides_fact.con
1504 cic:/matita/nat/fermat_little_theorem/permut_mod.con
1505 cic:/matita/nat/fermat_little_theorem/permut_S_mod.con
1506 cic:/matita/nat/fermat_little_theorem/congruent_exp_pred_SO.con
1507 cic:/matita/nat/gcd/symmetric_gcd.con
1508 cic:/matita/nat/gcd/sym_gcd.con
1509 cic:/matita/nat/gcd/prime_to_gcd_SO.con
1510 cic:/matita/nat/gcd/lt_O_gcd.con
1511 cic:/matita/nat/gcd/le_gcd_times.con
1512 cic:/matita/nat/gcd/gcd_times_SO_to_gcd_SO.con
1513 cic:/matita/nat/gcd/gcd_n_times_nm.con
1514 cic:/matita/nat/gcd/gcd_n_n.con
1515 cic:/matita/nat/gcd/gcd_mod.con
1516 cic:/matita/nat/gcd/gcd_aux.con
1517 cic:/matita/nat/gcd/gcd_SO_to_lt_n.con
1518 cic:/matita/nat/gcd/gcd_SO_to_lt_O.con
1519 cic:/matita/nat/gcd/gcd_SO_to_divides_times_to_divides.con
1520 cic:/matita/nat/gcd/gcd_SO_n.con
1521 cic:/matita/nat/gcd/gcd_O_to_eq_O.con
1522 cic:/matita/nat/gcd/gcd_O_n.con
1523 cic:/matita/nat/gcd/gcd.con
1524 cic:/matita/nat/gcd/eq_minus_gcd_aux.con
1525 cic:/matita/nat/gcd/eq_minus_gcd.con
1526 cic:/matita/nat/gcd/eq_gcd_times_SO.con
1527 cic:/matita/nat/gcd/eq_gcd_SO_to_not_divides.con
1528 cic:/matita/nat/gcd/divides_to_divides_times.con
1529 cic:/matita/nat/gcd/divides_times_to_divides.con
1530 cic:/matita/nat/gcd/divides_times_gcd_aux.con
1531 cic:/matita/nat/gcd/divides_mod_to_divides.con
1532 cic:/matita/nat/gcd/divides_mod_gcd.con
1533 cic:/matita/nat/gcd/divides_mod.con
1534 cic:/matita/nat/gcd/divides_gcd_nm.con
1535 cic:/matita/nat/gcd/divides_gcd_n.con
1536 cic:/matita/nat/gcd/divides_gcd_mod.con
1537 cic:/matita/nat/gcd/divides_gcd_m.con
1538 cic:/matita/nat/gcd/divides_gcd_aux_mn.con
1539 cic:/matita/nat/gcd/divides_gcd_aux.con
1540 cic:/matita/nat/gcd/divides_exp_to_eq.con
1541 cic:/matita/nat/gcd/divides_exp_to_divides.con
1542 cic:/matita/nat/gcd/divides_d_times_gcd.con
1543 cic:/matita/nat/gcd/divides_d_gcd.con
1544 cic:/matita/nat/gcd_properties1/gcd_plus_times_gcd.con
1545 cic:/matita/nat/gcd_properties1/gcd_SO_to_eq_gcd_times_times_gcd_gcd.con
1546 cic:/matita/nat/gcd_properties1/gcd_SO_to_divides_to_divides_to_divides_times.con
1547 cic:/matita/nat/gcd_properties1/gcd1.con
1548 cic:/matita/nat/gcd_properties1/eq_gcd_times_times_times_gcd.con
1549 cic:/matita/nat/gcd_properties1/eq_gcd_gcd_minus.con
1550 cic:/matita/nat/gcd_properties1/eq_gcd_div_div_div_gcd.con
1551 cic:/matita/nat/gcd_properties1/divides_times_to_divides_div_gcd.con
1552 cic:/matita/nat/gcd_properties1/associative_nat_gcd.con
1553 cic:/matita/nat/generic_iter_p/true_to_iter_p_gen_Sn.con
1554 cic:/matita/nat/generic_iter_p/p_ord_times.con
1555 cic:/matita/nat/generic_iter_p/or_false_eq_baseA_to_eq_iter_p_gen.con
1556 cic:/matita/nat/generic_iter_p/mod_p_ord_times.con
1557 cic:/matita/nat/generic_iter_p/lt_times_to_lt_O.con
1558 cic:/matita/nat/generic_iter_p/iter_p_gen_plusA.con
1559 cic:/matita/nat/generic_iter_p/iter_p_gen_knm.con
1560 cic:/matita/nat/generic_iter_p/iter_p_gen_iter_p_gen.con
1561 cic:/matita/nat/generic_iter_p/iter_p_gen_gi.con
1562 cic:/matita/nat/generic_iter_p/iter_p_gen_false.con
1563 cic:/matita/nat/generic_iter_p/iter_p_gen_divides.con
1564 cic:/matita/nat/generic_iter_p/iter_p_gen_2_eq.con
1565 cic:/matita/nat/generic_iter_p/iter_p_gen2.con
1566 cic:/matita/nat/generic_iter_p/iter_p_gen2'.con
1567 cic:/matita/nat/generic_iter_p/iter_p_gen.con
1568 cic:/matita/nat/generic_iter_p/false_to_iter_p_gen_Sn.con
1569 cic:/matita/nat/generic_iter_p/false_to_eq_iter_p_gen.con
1570 cic:/matita/nat/generic_iter_p/eq_p_ord_times.con
1571 cic:/matita/nat/generic_iter_p/eq_iter_p_gen_pred.con
1572 cic:/matita/nat/generic_iter_p/eq_iter_p_gen_gh.con
1573 cic:/matita/nat/generic_iter_p/eq_iter_p_gen1.con
1574 cic:/matita/nat/generic_iter_p/eq_iter_p_gen.con
1575 cic:/matita/nat/generic_iter_p/div_p_ord_times.con
1576 cic:/matita/nat/generic_iter_p/distributive_times_plus_iter_p_gen.con
1577 cic:/matita/nat/iteration2/true_to_sigma_p_Sn.con
1578 cic:/matita/nat/iteration2/symmetricIntPlus.con
1579 cic:/matita/nat/iteration2/sigma_p_true.con
1580 cic:/matita/nat/iteration2/sigma_p_times.con
1581 cic:/matita/nat/iteration2/sigma_p_sigma_p.con
1582 cic:/matita/nat/iteration2/sigma_p_plus_1.con
1583 cic:/matita/nat/iteration2/sigma_p_plus.con
1584 cic:/matita/nat/iteration2/sigma_p_knm.con
1585 cic:/matita/nat/iteration2/sigma_p_gi.con
1586 cic:/matita/nat/iteration2/sigma_p_false.con
1587 cic:/matita/nat/iteration2/sigma_p_divides.con
1588 cic:/matita/nat/iteration2/sigma_p2_eq.con
1589 cic:/matita/nat/iteration2/sigma_p2.con
1590 cic:/matita/nat/iteration2/sigma_p2'.con
1591 cic:/matita/nat/iteration2/sigma_p.con
1592 cic:/matita/nat/iteration2/sigma_P_SO_to_sigma_p_true.con
1593 cic:/matita/nat/iteration2/or_false_to_eq_sigma_p.con
1594 cic:/matita/nat/iteration2/lt_sigma_p.con
1595 cic:/matita/nat/iteration2/le_sigma_p1.con
1596 cic:/matita/nat/iteration2/le_sigma_p.con
1597 cic:/matita/nat/iteration2/false_to_sigma_p_Sn.con
1598 cic:/matita/nat/iteration2/false_to_eq_sigma_p.con
1599 cic:/matita/nat/iteration2/eq_sigma_p_sigma_p_times2.con
1600 cic:/matita/nat/iteration2/eq_sigma_p_sigma_p_times1.con
1601 cic:/matita/nat/iteration2/eq_sigma_p_pred.con
1602 cic:/matita/nat/iteration2/eq_sigma_p_gh.con
1603 cic:/matita/nat/iteration2/eq_sigma_p1.con
1604 cic:/matita/nat/iteration2/eq_sigma_p.con
1605 cic:/matita/nat/iteration2/eq_map_iter_i_sigma_p_alwaysTrue.con
1606 cic:/matita/nat/iteration2/distributive_times_plus_sigma_p.con
1607 cic:/matita/nat/iteration2/bool_to_nat_to_eq_sigma_p.con
1608 cic:/matita/nat/le_arith/monotonic_le_times_r.con
1609 cic:/matita/nat/le_arith/monotonic_le_times_l.con
1610 cic:/matita/nat/le_arith/monotonic_le_plus_r.con
1611 cic:/matita/nat/le_arith/monotonic_le_plus_l.con
1612 cic:/matita/nat/le_arith/le_times_to_le.con
1613 cic:/matita/nat/le_arith/le_times_r.con
1614 cic:/matita/nat/le_arith/le_times_n.con
1615 cic:/matita/nat/le_arith/le_times_l.con
1616 cic:/matita/nat/le_arith/le_times.con
1617 cic:/matita/nat/le_arith/le_plus_to_le.con
1618 cic:/matita/nat/le_arith/le_plus_r.con
1619 cic:/matita/nat/le_arith/le_plus_n_r.con
1620 cic:/matita/nat/le_arith/le_plus_n.con
1621 cic:/matita/nat/le_arith/le_plus_l.con
1622 cic:/matita/nat/le_arith/le_plus.con
1623 cic:/matita/nat/le_arith/le_S_times_SSO.con
1624 cic:/matita/nat/le_arith/eq_plus_to_le.con
1625 cic:/matita/nat/le_arith/O_lt_const_to_le_times_const.con
1626 cic:/matita/nat/log/lt_to_log_O.con
1627 cic:/matita/nat/log/lt_log_n_n.con
1628 cic:/matita/nat/log/lt_exp_log.con
1629 cic:/matita/nat/log/lt_O_log.con
1630 cic:/matita/nat/log/log_times_l.con
1631 cic:/matita/nat/log/log_times1.con
1632 cic:/matita/nat/log/log_times.con
1633 cic:/matita/nat/log/log_n_n.con
1634 cic:/matita/nat/log/log_i_SSOn.con
1635 cic:/matita/nat/log/log_exp2.con
1636 cic:/matita/nat/log/log_exp1.con
1637 cic:/matita/nat/log/log_exp.con
1638 cic:/matita/nat/log/log_div.con
1639 cic:/matita/nat/log/log_SO.con
1640 cic:/matita/nat/log/log.con
1641 cic:/matita/nat/log/le_log_plus.con
1642 cic:/matita/nat/log/le_log_n_n.con
1643 cic:/matita/nat/log/le_log.con
1644 cic:/matita/nat/log/le_exp_log.con
1645 cic:/matita/nat/log/exp_n_O.con
1646 cic:/matita/nat/log/eq_log_exp.con
1647 cic:/matita/nat/lt_arith/times_mod.con
1648 cic:/matita/nat/lt_arith/nat_compare_times_l.con
1649 cic:/matita/nat/lt_arith/monotonic_to_injective.con
1650 cic:/matita/nat/lt_arith/monotonic_lt_times_variant.con
1651 cic:/matita/nat/lt_arith/monotonic_lt_times_r.con
1652 cic:/matita/nat/lt_arith/monotonic_lt_times_l.con
1653 cic:/matita/nat/lt_arith/monotonic_lt_plus_r.con
1654 cic:/matita/nat/lt_arith/monotonic_lt_plus_l.con
1655 cic:/matita/nat/lt_arith/lt_to_lt_to_eq_div_div_times_times.con
1656 cic:/matita/nat/lt_arith/lt_to_le_to_lt_times.con
1657 cic:/matita/nat/lt_arith/lt_to_le_times_to_lt_S_to_div.con
1658 cic:/matita/nat/lt_arith/lt_to_div_to_and_le_times_lt_S.con
1659 cic:/matita/nat/lt_arith/lt_times_to_lt_r.con
1660 cic:/matita/nat/lt_arith/lt_times_to_lt_l.con
1661 cic:/matita/nat/lt_arith/lt_times_to_lt_O.con
1662 cic:/matita/nat/lt_arith/lt_times_r1.con
1663 cic:/matita/nat/lt_arith/lt_times_r.con
1664 cic:/matita/nat/lt_arith/lt_times_plus_times.con
1665 cic:/matita/nat/lt_arith/lt_times_n_to_lt_r.con
1666 cic:/matita/nat/lt_arith/lt_times_n_to_lt.con
1667 cic:/matita/nat/lt_arith/lt_times_l1.con
1668 cic:/matita/nat/lt_arith/lt_times_l.con
1669 cic:/matita/nat/lt_arith/lt_times_eq_O.con
1670 cic:/matita/nat/lt_arith/lt_times.con
1671 cic:/matita/nat/lt_arith/lt_plus_to_lt_r.con
1672 cic:/matita/nat/lt_arith/lt_plus_to_lt_l.con
1673 cic:/matita/nat/lt_arith/lt_plus_r.con
1674 cic:/matita/nat/lt_arith/lt_plus_l.con
1675 cic:/matita/nat/lt_arith/lt_plus.con
1676 cic:/matita/nat/lt_arith/lt_div_n_m_n.con
1677 cic:/matita/nat/lt_arith/lt_O_times_S_S.con
1678 cic:/matita/nat/lt_arith/le_to_lt_to_plus_lt.con
1679 cic:/matita/nat/lt_arith/increasing_to_injective.con
1680 cic:/matita/nat/lt_arith/eq_mod_O_to_lt_O_div.con
1681 cic:/matita/nat/lt_arith/eq_div_div_div_times.con
1682 cic:/matita/nat/lt_arith/eq_div_div_div_div.con
1683 cic:/matita/nat/lt_arith/SSO_mod.con
1684 cic:/matita/nat/lt_arith/O_lt_times_to_O_lt.con
1685 cic:/matita/nat/map_iter_p/pi_p_S.con
1686 cic:/matita/nat/map_iter_p/pi_p.con
1687 cic:/matita/nat/map_iter_p/permut_p_transpose.con
1688 cic:/matita/nat/map_iter_p/permut_p_compose.con
1689 cic:/matita/nat/map_iter_p/permut_p_S_to_permut_p.con
1690 cic:/matita/nat/map_iter_p/permut_p_O.con
1691 cic:/matita/nat/map_iter_p/permut_p.con
1692 cic:/matita/nat/map_iter_p/map_iter_p_S_true.con
1693 cic:/matita/nat/map_iter_p/map_iter_p_S_false.con
1694 cic:/matita/nat/map_iter_p/map_iter_p_O.con
1695 cic:/matita/nat/map_iter_p/map_iter_p.con
1696 cic:/matita/nat/map_iter_p/lt_O_pi_p.con
1697 cic:/matita/nat/map_iter_p/extentional_eq_n_to_permut_p.con
1698 cic:/matita/nat/map_iter_p/extentional_eq_n.con
1699 cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose3.con
1700 cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose2.con
1701 cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose1.con
1702 cic:/matita/nat/map_iter_p/eq_map_iter_p_transpose.con
1703 cic:/matita/nat/map_iter_p/eq_map_iter_p_permut.con
1704 cic:/matita/nat/map_iter_p/eq_map_iter_p_k.con
1705 cic:/matita/nat/map_iter_p/eq_map_iter_p_a.con
1706 cic:/matita/nat/map_iter_p/eq_map_iter_p.con
1707 cic:/matita/nat/map_iter_p/decidable_n2.con
1708 cic:/matita/nat/map_iter_p/decidable_n1.con
1709 cic:/matita/nat/map_iter_p/decidable_n.con
1710 cic:/matita/nat/map_iter_p/count_card1.con
1711 cic:/matita/nat/map_iter_p/count_card.con
1712 cic:/matita/nat/map_iter_p/card.con
1713 cic:/matita/nat/map_iter_p/a_times_pi_p.con
1714 cic:/matita/nat/minimization/min_aux_S.con
1715 cic:/matita/nat/minimization/min_aux_O_f.con
1716 cic:/matita/nat/minimization/min_aux.con
1717 cic:/matita/nat/minimization/min_O_f.con
1718 cic:/matita/nat/minimization/min.con
1719 cic:/matita/nat/minimization/max_spec_to_max.con
1720 cic:/matita/nat/minimization/max_spec.con
1721 cic:/matita/nat/minimization/max_f_g.con
1722 cic:/matita/nat/minimization/max_S_max.con
1723 cic:/matita/nat/minimization/max_O_f.con
1724 cic:/matita/nat/minimization/max_O.con
1725 cic:/matita/nat/minimization/max.con
1726 cic:/matita/nat/minimization/lt_min_aux_to_false.con
1727 cic:/matita/nat/minimization/lt_max_to_false.con
1728 cic:/matita/nat/minimization/le_to_le_max.con
1729 cic:/matita/nat/minimization/le_min_aux_r.con
1730 cic:/matita/nat/minimization/le_min_aux.con
1731 cic:/matita/nat/minimization/le_max_n.con
1732 cic:/matita/nat/minimization/le_max_f_max_g.con
1733 cic:/matita/nat/minimization/false_to_lt_max.con
1734 cic:/matita/nat/minimization/f_min_aux_true.con
1735 cic:/matita/nat/minimization/f_max_true.con
1736 cic:/matita/nat/minimization/f_m_to_le_max.con
1737 cic:/matita/nat/minimization/f_false_to_le_max.con
1738 cic:/matita/nat/minimization/exists_max_forall_false.con
1739 cic:/matita/nat/minimization/exists_forall_le.con
1740 cic:/matita/nat/minus/plus_to_minus.con
1741 cic:/matita/nat/minus/plus_minus_m_m.con
1742 cic:/matita/nat/minus/plus_minus.con
1743 cic:/matita/nat/minus/monotonic_le_minus_r.con
1744 cic:/matita/nat/minus/minus_to_plus.con
1745 cic:/matita/nat/minus/minus_pred_pred.con
1746 cic:/matita/nat/minus/minus_plus_m_m.con
1747 cic:/matita/nat/minus/minus_n_n.con
1748 cic:/matita/nat/minus/minus_n_O.con
1749 cic:/matita/nat/minus/minus_m_minus_mn.con
1750 cic:/matita/nat/minus/minus_le_S_minus_S.con
1751 cic:/matita/nat/minus/minus_le_O_to_le.con
1752 cic:/matita/nat/minus/minus_Sn_n.con
1753 cic:/matita/nat/minus/minus_Sn_m.con
1754 cic:/matita/nat/minus/minus_S_S.con
1755 cic:/matita/nat/minus/minus.con
1756 cic:/matita/nat/minus/lt_to_lt_O_minus.con
1757 cic:/matita/nat/minus/lt_plus_to_lt_minus.con
1758 cic:/matita/nat/minus/lt_minus_to_plus.con
1759 cic:/matita/nat/minus/lt_minus_to_lt_plus.con
1760 cic:/matita/nat/minus/lt_minus_r.con
1761 cic:/matita/nat/minus/lt_minus_m.con
1762 cic:/matita/nat/minus/lt_minus_l.con
1763 cic:/matita/nat/minus/lt_minus_S_n_to_le_minus_n.con
1764 cic:/matita/nat/minus/lt_O_minus_to_lt.con
1765 cic:/matita/nat/minus/le_plus_to_minus_r.con
1766 cic:/matita/nat/minus/le_plus_to_minus.con
1767 cic:/matita/nat/minus/le_minus_to_plus.con
1768 cic:/matita/nat/minus/le_minus_m.con
1769 cic:/matita/nat/minus/le_SO_minus.con
1770 cic:/matita/nat/minus/eq_plus_minus_minus_minus.con
1771 cic:/matita/nat/minus/eq_minus_plus_plus_minus.con
1772 cic:/matita/nat/minus/eq_minus_n_m_O.con
1773 cic:/matita/nat/minus/eq_minus_minus_minus_plus.con
1774 cic:/matita/nat/minus/eq_minus_S_pred.con
1775 cic:/matita/nat/minus/distributive_times_minus.con
1776 cic:/matita/nat/minus/distr_times_minus.con
1777 cic:/matita/nat/nat/pred_Sn.con
1778 cic:/matita/nat/nat/pred.con
1779 cic:/matita/nat/nat/not_zero.con
1780 cic:/matita/nat/nat/not_eq_n_Sn.con
1781 cic:/matita/nat/nat/not_eq_S.con
1782 cic:/matita/nat/nat/not_eq_O_S.con
1783 cic:/matita/nat/nat/nat_rect.con
1784 cic:/matita/nat/nat/nat_rec.con
1785 cic:/matita/nat/nat/nat_ind.con
1786 cic:/matita/nat/nat/nat_elim2.con
1787 cic:/matita/nat/nat/nat_case1.con
1788 cic:/matita/nat/nat/nat_case.con
1789 cic:/matita/nat/nat/nat.ind
1790 cic:/matita/nat/nat/injective_S.con
1791 cic:/matita/nat/nat/inj_S.con
1792 cic:/matita/nat/nat/decidable_eq_nat.con
1793 cic:/matita/nat/neper/sigma_p_log_div2.con
1794 cic:/matita/nat/neper/sigma_p_log_div1.con
1795 cic:/matita/nat/neper/sigma_p_log_div.con
1796 cic:/matita/nat/neper/sigma_p_div_exp.con
1797 cic:/matita/nat/neper/neper_sigma_p3.con
1798 cic:/matita/nat/neper/neper_sigma_p2.con
1799 cic:/matita/nat/neper/neper_sigma_p1.con
1800 cic:/matita/nat/neper/neper_monotonic.con
1801 cic:/matita/nat/neper/lt_exp_sigma_p_exp.con
1802 cic:/matita/nat/neper/lt_exp_Sn_n_SSSO.con
1803 cic:/matita/nat/neper/lt_exp_Sn_m_SSSO.con
1804 cic:/matita/nat/neper/lt_SO_to_lt_exp_Sn_n_SSSO.con
1805 cic:/matita/nat/neper/le_sigma_p_div_log_div_pred_log.con
1806 cic:/matita/nat/neper/le_log_exp_fact_sigma_p.con
1807 cic:/matita/nat/neper/le_log_exp_Sn_log_exp_n.con
1808 cic:/matita/nat/neper/le_log_div_sigma_p.con
1809 cic:/matita/nat/neper/le_fact_exp1.con
1810 cic:/matita/nat/neper/le_fact_exp.con
1811 cic:/matita/nat/neper/le_exp_sigma_p_exp.con
1812 cic:/matita/nat/neper/le_exp_div.con
1813 cic:/matita/nat/neper/le_exp_SSO_fact.con
1814 cic:/matita/nat/neper/le_SSO_neper.con
1815 cic:/matita/nat/neper/le_SSO_exp_neper.con
1816 cic:/matita/nat/neper/eq_fact_pi_p.con
1817 cic:/matita/nat/neper/eq_exp_pi_p.con
1818 cic:/matita/nat/neper/divides_times_to_eq.con
1819 cic:/matita/nat/neper/divides_times_to_divides_div.con
1820 cic:/matita/nat/neper/divides_sigma_p_to_eq.con
1821 cic:/matita/nat/neper/divides_pi_p_to_eq.con
1822 cic:/matita/nat/neper/divides_pi_p.con
1823 cic:/matita/nat/neper/divides_fact_fact.con
1824 cic:/matita/nat/nth_prime/smallest_factor_fact.con
1825 cic:/matita/nat/nth_prime/prime_to_nth_prime.con
1826 cic:/matita/nat/nth_prime/prime_nth_prime.con
1827 cic:/matita/nat/nth_prime/nth_prime.con
1828 cic:/matita/nat/nth_prime/lt_nth_prime_to_not_prime.con
1829 cic:/matita/nat/nth_prime/lt_nth_prime_n_nth_prime_Sn.con
1830 cic:/matita/nat/nth_prime/lt_n_nth_prime_n.con
1831 cic:/matita/nat/nth_prime/lt_SO_nth_prime_n.con
1832 cic:/matita/nat/nth_prime/lt_O_nth_prime_n.con
1833 cic:/matita/nat/nth_prime/injective_nth_prime.con
1834 cic:/matita/nat/nth_prime/increasing_nth_prime.con
1835 cic:/matita/nat/nth_prime/ex_prime.con
1836 cic:/matita/nat/nth_prime/ex_m_le_n_nth_prime_m.con
1837 cic:/matita/nat/o/lt_times_SSO_n_exp_SSO_n.con
1838 cic:/matita/nat/o/lt_exp_n_SSO_exp_SSO_n.con
1839 cic:/matita/nat/o/le_times_n_exp.con
1840 cic:/matita/nat/o/le_times_exp_n_SSO_exp_SSO_n.con
1841 cic:/matita/nat/o/le_times_SSO_n_exp_SSO_n.con
1842 cic:/matita/nat/o/le_exp_n_SSO_exp_SSO_n1.con
1843 cic:/matita/nat/o/le_exp_n_SSO_exp_SSO_n.con
1844 cic:/matita/nat/ord/p_ord_to_not_eq_O.con
1845 cic:/matita/nat/ord/p_ord_to_exp1.con
1846 cic:/matita/nat/ord/p_ord_times.con
1847 cic:/matita/nat/ord/p_ord_p.con
1848 cic:/matita/nat/ord/p_ord_inv.con
1849 cic:/matita/nat/ord/p_ord_exp1.con
1850 cic:/matita/nat/ord/p_ord_exp.con
1851 cic:/matita/nat/ord/p_ord_aux_to_not_mod_O.con
1852 cic:/matita/nat/ord/p_ord_aux_to_exp.con
1853 cic:/matita/nat/ord/p_ord_aux_to_Prop1.con
1854 cic:/matita/nat/ord/p_ord_aux_to_Prop.con
1855 cic:/matita/nat/ord/p_ord_aux.con
1856 cic:/matita/nat/ord/p_ord_O_to_not_divides.con
1857 cic:/matita/nat/ord/p_ord.con
1858 cic:/matita/nat/ord/ord_times.con
1859 cic:/matita/nat/ord/ord_rem.con
1860 cic:/matita/nat/ord/ord_ord_rem.con
1861 cic:/matita/nat/ord/ord_exp.con
1862 cic:/matita/nat/ord/ord_O_to_not_divides.con
1863 cic:/matita/nat/ord/ord.con
1864 cic:/matita/nat/ord/not_ord_O_to_divides.con
1865 cic:/matita/nat/ord/not_divides_to_p_ord_O.con
1866 cic:/matita/nat/ord/not_divides_to_ord_O.con
1867 cic:/matita/nat/ord/not_divides_ord_rem.con
1868 cic:/matita/nat/ord/mod_p_ord_inv.con
1869 cic:/matita/nat/ord/lt_ord_rem.con
1870 cic:/matita/nat/ord/lt_O_ord_rem.con
1871 cic:/matita/nat/ord/fst_p_ord_times.con
1872 cic:/matita/nat/ord/exp_ord.con
1873 cic:/matita/nat/ord/eq_p_ord_inv.con
1874 cic:/matita/nat/ord/divides_to_p_ord.con
1875 cic:/matita/nat/ord/divides_to_ord.con
1876 cic:/matita/nat/ord/divides_to_not_ord_O.con
1877 cic:/matita/nat/ord/divides_to_le_ord.con
1878 cic:/matita/nat/ord/divides_to_divides_ord_rem.con
1879 cic:/matita/nat/ord/divides_ord_rem.con
1880 cic:/matita/nat/ord/div_p_ord_inv.con
1881 cic:/matita/nat/orders/transitive_lt.con
1882 cic:/matita/nat/orders/transitive_le.con
1883 cic:/matita/nat/orders/trans_lt.con
1884 cic:/matita/nat/orders/trans_le.con
1885 cic:/matita/nat/orders/not_lt_to_le.con
1886 cic:/matita/nat/orders/not_le_to_lt.con
1887 cic:/matita/nat/orders/not_le_Sn_n.con
1888 cic:/matita/nat/orders/not_le_Sn_O.con
1889 cic:/matita/nat/orders/not_eq_to_le_to_lt.con
1890 cic:/matita/nat/orders/nat_elim1.con
1891 cic:/matita/nat/orders/ltn_to_ltO.con
1892 cic:/matita/nat/orders/lt_to_not_le.con
1893 cic:/matita/nat/orders/lt_to_not_eq.con
1894 cic:/matita/nat/orders/lt_to_lt_S_S.con
1895 cic:/matita/nat/orders/lt_to_le_to_lt.con
1896 cic:/matita/nat/orders/lt_to_le.con
1897 cic:/matita/nat/orders/lt_pred.con
1898 cic:/matita/nat/orders/lt_n_m_to_not_lt_m_Sn.con
1899 cic:/matita/nat/orders/lt_S_to_lt.con
1900 cic:/matita/nat/orders/lt_S_to_le.con
1901 cic:/matita/nat/orders/lt_S_S_to_lt.con
1902 cic:/matita/nat/orders/lt_SO_n_to_lt_O_pred_n.con
1903 cic:/matita/nat/orders/lt_O_n_elim.con
1904 cic:/matita/nat/orders/lt_O_S.con
1905 cic:/matita/nat/orders/lt.con
1906 cic:/matita/nat/orders/le_to_or_lt_eq.con
1907 cic:/matita/nat/orders/le_to_not_lt.con
1908 cic:/matita/nat/orders/le_to_lt_to_lt.con
1909 cic:/matita/nat/orders/le_to_le_to_eq.con
1910 cic:/matita/nat/orders/le_to_le_pred.con
1911 cic:/matita/nat/orders/le_pred_to_le.con
1912 cic:/matita/nat/orders/le_pred_n.con
1913 cic:/matita/nat/orders/le_n_m_to_lt_m_Sn_to_eq_n_m.con
1914 cic:/matita/nat/orders/le_n_fn.con
1915 cic:/matita/nat/orders/le_n_Sn.con
1916 cic:/matita/nat/orders/le_n_Sm_elim.con
1917 cic:/matita/nat/orders/le_n_O_to_eq.con
1918 cic:/matita/nat/orders/le_n_O_elim.con
1919 cic:/matita/nat/orders/le_inv.con
1920 cic:/matita/nat/orders/le_ind.con
1921 cic:/matita/nat/orders/le_S_S_to_le.con
1922 cic:/matita/nat/orders/le_S_S.con
1923 cic:/matita/nat/orders/le_O_n.con
1924 cic:/matita/nat/orders/leS_to_not_zero.con
1925 cic:/matita/nat/orders/le.ind
1926 cic:/matita/nat/orders/increasing_to_monotonic.con
1927 cic:/matita/nat/orders/increasing_to_le2.con
1928 cic:/matita/nat/orders/increasing_to_le.con
1929 cic:/matita/nat/orders/increasing.con
1930 cic:/matita/nat/orders/gt.con
1931 cic:/matita/nat/orders/ge.con
1932 cic:/matita/nat/orders/eq_to_not_lt.con
1933 cic:/matita/nat/orders/decidable_lt.con
1934 cic:/matita/nat/orders/decidable_le.con
1935 cic:/matita/nat/orders/antisymmetric_le.con
1936 cic:/matita/nat/orders/antisym_le.con
1937 cic:/matita/nat/orders/S_pred.con
1938 cic:/matita/nat/orders/Not_lt_n_n.con
1939 cic:/matita/nat/permutation/transpose_transpose.con
1940 cic:/matita/nat/permutation/transpose_i_j_j_i.con
1941 cic:/matita/nat/permutation/transpose_i_j_j.con
1942 cic:/matita/nat/permutation/transpose_i_j_i.con
1943 cic:/matita/nat/permutation/transpose_i_i.con
1944 cic:/matita/nat/permutation/transpose.con
1945 cic:/matita/nat/permutation/permut_transpose_r.con
1946 cic:/matita/nat/permutation/permut_transpose_l.con
1947 cic:/matita/nat/permutation/permut_transpose.con
1948 cic:/matita/nat/permutation/permut_to_eq_map_iter_i.con
1949 cic:/matita/nat/permutation/permut_to_bijn.con
1950 cic:/matita/nat/permutation/permut_n_to_le.con
1951 cic:/matita/nat/permutation/permut_n_to_eq_n.con
1952 cic:/matita/nat/permutation/permut_invert_permut.con
1953 cic:/matita/nat/permutation/permut_fg.con
1954 cic:/matita/nat/permutation/permut_S_to_permut_transpose.con
1955 cic:/matita/nat/permutation/permut_S_to_permut.con
1956 cic:/matita/nat/permutation/permut_O_to_eq_O.con
1957 cic:/matita/nat/permutation/permut.con
1958 cic:/matita/nat/permutation/map_iter_i.con
1959 cic:/matita/nat/permutation/invert_permut_f.con
1960 cic:/matita/nat/permutation/invert_permut.con
1961 cic:/matita/nat/permutation/injn_Sn_n.con
1962 cic:/matita/nat/permutation/injn.con
1963 cic:/matita/nat/permutation/injective_transpose.con
1964 cic:/matita/nat/permutation/injective_to_injn.con
1965 cic:/matita/nat/permutation/injective_invert_permut.con
1966 cic:/matita/nat/permutation/inj_transpose.con
1967 cic:/matita/nat/permutation/f_invert_permut.con
1968 cic:/matita/nat/permutation/eq_transpose.con
1969 cic:/matita/nat/permutation/eq_to_bijn.con
1970 cic:/matita/nat/permutation/eq_map_iter_i_transpose_l.con
1971 cic:/matita/nat/permutation/eq_map_iter_i_transpose_i_Si.con
1972 cic:/matita/nat/permutation/eq_map_iter_i_transpose2.con
1973 cic:/matita/nat/permutation/eq_map_iter_i_transpose1.con
1974 cic:/matita/nat/permutation/eq_map_iter_i_transpose.con
1975 cic:/matita/nat/permutation/eq_map_iter_i_sigma.con
1976 cic:/matita/nat/permutation/eq_map_iter_i_pi.con
1977 cic:/matita/nat/permutation/eq_map_iter_i_fact.con
1978 cic:/matita/nat/permutation/eq_map_iter_i.con
1979 cic:/matita/nat/permutation/bijn_transpose_r.con
1980 cic:/matita/nat/permutation/bijn_transpose_l.con
1981 cic:/matita/nat/permutation/bijn_transpose.con
1982 cic:/matita/nat/permutation/bijn_n_Sn.con
1983 cic:/matita/nat/permutation/bijn_fg.con
1984 cic:/matita/nat/permutation/bijn_Sn_n.con
1985 cic:/matita/nat/permutation/bijn.con
1986 cic:/matita/nat/pi_p/true_to_pi_p_Sn.con
1987 cic:/matita/nat/pi_p/times_pi_p.con
1988 cic:/matita/nat/pi_p/pi_p_times.con
1989 cic:/matita/nat/pi_p/pi_p_pi_p1.con
1990 cic:/matita/nat/pi_p/pi_p_pi_p.con
1991 cic:/matita/nat/pi_p/pi_p_knm.con
1992 cic:/matita/nat/pi_p/pi_p_gi.con
1993 cic:/matita/nat/pi_p/pi_p_false.con
1994 cic:/matita/nat/pi_p/pi_p_SO.con
1995 cic:/matita/nat/pi_p/pi_p2.con
1996 cic:/matita/nat/pi_p/pi_p2'.con
1997 cic:/matita/nat/pi_p/pi_p.con
1998 cic:/matita/nat/pi_p/or_false_eq_SO_to_eq_pi_p.con
1999 cic:/matita/nat/pi_p/le_pi_p.con
2000 cic:/matita/nat/pi_p/false_to_pi_p_Sn.con
2001 cic:/matita/nat/pi_p/false_to_eq_pi_p.con
2002 cic:/matita/nat/pi_p/exp_times_pi_p.con
2003 cic:/matita/nat/pi_p/exp_sigma_p1.con
2004 cic:/matita/nat/pi_p/exp_sigma_p.con
2005 cic:/matita/nat/pi_p/exp_pi_p.con
2006 cic:/matita/nat/pi_p/eq_pi_p_gh.con
2007 cic:/matita/nat/pi_p/eq_pi_p1.con
2008 cic:/matita/nat/pi_p/eq_pi_p.con
2009 cic:/matita/nat/plus/sym_plus.con
2010 cic:/matita/nat/plus/plus_n_Sm.con
2011 cic:/matita/nat/plus/plus_n_SO.con
2012 cic:/matita/nat/plus/plus_n_O.con
2013 cic:/matita/nat/plus/plus.con
2014 cic:/matita/nat/plus/injective_plus_r.con
2015 cic:/matita/nat/plus/injective_plus_l.con
2016 cic:/matita/nat/plus/inj_plus_r.con
2017 cic:/matita/nat/plus/inj_plus_l.con
2018 cic:/matita/nat/plus/associative_plus.con
2019 cic:/matita/nat/plus/assoc_plus.con
2020 cic:/matita/nat/primes/transitive_divides.con
2021 cic:/matita/nat/primes/trans_divides.con
2022 cic:/matita/nat/primes/smallest_factor.con
2023 cic:/matita/nat/primes/reflexive_divides.con
2024 cic:/matita/nat/primes/primeb_true_to_prime.con
2025 cic:/matita/nat/primes/primeb_to_Prop.con
2026 cic:/matita/nat/primes/primeb_false_to_not_prime.con
2027 cic:/matita/nat/primes/primeb.con
2028 cic:/matita/nat/primes/prime_to_smallest_factor.con
2029 cic:/matita/nat/primes/prime_to_primeb_true.con
2030 cic:/matita/nat/primes/prime_to_lt_SO.con
2031 cic:/matita/nat/primes/prime_to_lt_O.con
2032 cic:/matita/nat/primes/prime_smallest_factor_n.con
2033 cic:/matita/nat/primes/prime.con
2034 cic:/matita/nat/primes/or_div_mod1.con
2035 cic:/matita/nat/primes/not_prime_to_primeb_false.con
2036 cic:/matita/nat/primes/not_prime_SO.con
2037 cic:/matita/nat/primes/not_prime_O.con
2038 cic:/matita/nat/primes/not_divides_to_divides_b_false.con
2039 cic:/matita/nat/primes/not_divides_S_fact.con
2040 cic:/matita/nat/primes/mod_S_fact.con
2041 cic:/matita/nat/primes/mod_O_to_divides.con
2042 cic:/matita/nat/primes/lt_smallest_factor_to_not_divides.con
2043 cic:/matita/nat/primes/lt_SO_smallest_factor.con
2044 cic:/matita/nat/primes/lt_O_smallest_factor.con
2045 cic:/matita/nat/primes/le_smallest_factor_n.con
2046 cic:/matita/nat/primes/eq_mod_to_divides.con
2047 cic:/matita/nat/primes/eq_div_plus.con
2048 cic:/matita/nat/primes/divides_to_mod_O.con
2049 cic:/matita/nat/primes/divides_to_lt_O.con
2050 cic:/matita/nat/primes/divides_to_le.con
2051 cic:/matita/nat/primes/divides_to_eq_times_div_div_times.con
2052 cic:/matita/nat/primes/divides_to_divides_b_true1.con
2053 cic:/matita/nat/primes/divides_to_divides_b_true.con
2054 cic:/matita/nat/primes/divides_to_div_mod_spec.con
2055 cic:/matita/nat/primes/divides_to_div.con
2056 cic:/matita/nat/primes/divides_times.con
2057 cic:/matita/nat/primes/divides_smallest_factor_n.con
2058 cic:/matita/nat/primes/divides_plus.con
2059 cic:/matita/nat/primes/divides_n_n.con
2060 cic:/matita/nat/primes/divides_n_O.con
2061 cic:/matita/nat/primes/divides_minus.con
2062 cic:/matita/nat/primes/divides_ind.con
2063 cic:/matita/nat/primes/divides_fact.con
2064 cic:/matita/nat/primes/divides_f_pi_f.con
2065 cic:/matita/nat/primes/divides_div.con
2066 cic:/matita/nat/primes/divides_b_true_to_lt_O.con
2067 cic:/matita/nat/primes/divides_b_true_to_divides1.con
2068 cic:/matita/nat/primes/divides_b_true_to_divides.con
2069 cic:/matita/nat/primes/divides_b_to_Prop.con
2070 cic:/matita/nat/primes/divides_b_false_to_not_divides1.con
2071 cic:/matita/nat/primes/divides_b_false_to_not_divides.con
2072 cic:/matita/nat/primes/divides_b_div_true.con
2073 cic:/matita/nat/primes/divides_b.con
2074 cic:/matita/nat/primes/divides_SO_n.con
2075 cic:/matita/nat/primes/divides.ind
2076 cic:/matita/nat/primes/div_mod_spec_to_divides.con
2077 cic:/matita/nat/primes/div_div.con
2078 cic:/matita/nat/primes/decidable_prime.con
2079 cic:/matita/nat/primes/decidable_divides.con
2080 cic:/matita/nat/primes/antisymmetric_divides.con
2081 cic:/matita/nat/relevant_equations/times_plus_plus.con
2082 cic:/matita/nat/relevant_equations/times_plus_l.con
2083 cic:/matita/nat/relevant_equations/times_minus_l.con
2084 cic:/matita/nat/relevant_equations/eq_pred_to_eq.con
2085 cic:/matita/nat/sigma_and_pi/sigma.con
2086 cic:/matita/nat/sigma_and_pi/pi.con
2087 cic:/matita/nat/sigma_and_pi/exp_pi_l.con
2088 cic:/matita/nat/sigma_and_pi/eq_sigma.con
2089 cic:/matita/nat/sigma_and_pi/eq_pi.con
2090 cic:/matita/nat/sigma_and_pi/eq_fact_pi.con
2091 cic:/matita/nat/sqrt/sqrt.con
2092 cic:/matita/nat/sqrt/monotonic_sqrt.con
2093 cic:/matita/nat/sqrt/lt_sqrt_to_le_times_l.con
2094 cic:/matita/nat/sqrt/lt_sqrt_n.con
2095 cic:/matita/nat/sqrt/lt_sqrt.con
2096 cic:/matita/nat/sqrt/leq_sqrt_n.con
2097 cic:/matita/nat/sqrt/le_sqrt_to_le_times_r.con
2098 cic:/matita/nat/sqrt/le_sqrt_to_le_times_l.con
2099 cic:/matita/nat/sqrt/le_sqrt_nl.con
2100 cic:/matita/nat/sqrt/le_sqrt_n_n.con
2101 cic:/matita/nat/sqrt/le_sqrt_n1.con
2102 cic:/matita/nat/sqrt/le_sqrt_log_n.con
2103 cic:/matita/nat/sqrt/eq_sqrt.con
2104 cic:/matita/nat/times/times_n_Sm.con
2105 cic:/matita/nat/times/times_n_SO.con
2106 cic:/matita/nat/times/times_n_O.con
2107 cic:/matita/nat/times/times_SSO_n.con
2108 cic:/matita/nat/times/times_SSO.con
2109 cic:/matita/nat/times/times_O_to_O.con
2110 cic:/matita/nat/times/times.con
2111 cic:/matita/nat/times/symmetric_times.con
2112 cic:/matita/nat/times/sym_times.con
2113 cic:/matita/nat/times/or_eq_eq_S.con
2114 cic:/matita/nat/times/distributive_times_plus.con
2115 cic:/matita/nat/times/distr_times_plus.con
2116 cic:/matita/nat/times/associative_times.con
2117 cic:/matita/nat/times/assoc_times.con
2118 cic:/matita/nat/totient/totient_times.con
2119 cic:/matita/nat/totient/totient.con
2120 cic:/matita/nat/totient1/sigma_p_Sn_divides_b_totient_n.con
2121 cic:/matita/nat/totient1/lt_O_to_divides_to_lt_O_div.con
2122 cic:/matita/technicalities/setoids/variance_rect.con
2123 cic:/matita/technicalities/setoids/variance_rec.con
2124 cic:/matita/technicalities/setoids/variance_of_argument_class.con
2125 cic:/matita/technicalities/setoids/variance_ind.con
2126 cic:/matita/technicalities/setoids/variance.ind
2127 cic:/matita/technicalities/setoids/rewrite_direction_rect.con
2128 cic:/matita/technicalities/setoids/rewrite_direction_rec.con
2129 cic:/matita/technicalities/setoids/rewrite_direction_ind.con
2130 cic:/matita/technicalities/setoids/rewrite_direction.ind
2131 cic:/matita/technicalities/setoids/relation_of_relation_class.con
2132 cic:/matita/technicalities/setoids/relation_of_product_of_arguments.con
2133 cic:/matita/technicalities/setoids/relation_of_areflexive_relation_class.con
2134 cic:/matita/technicalities/setoids/relation_class_of_reflexive_relation_class.con
2135 cic:/matita/technicalities/setoids/relation_class_of_argument_class.con
2136 cic:/matita/technicalities/setoids/relation_class_of_areflexive_relation_class.con
2137 cic:/matita/technicalities/setoids/product_of_arguments.con
2138 cic:/matita/technicalities/setoids/opposite_direction_idempotent.con
2139 cic:/matita/technicalities/setoids/opposite_direction.con
2140 cic:/matita/technicalities/setoids/nelistT_rect.con
2141 cic:/matita/technicalities/setoids/nelistT_rec.con
2142 cic:/matita/technicalities/setoids/nelistT_ind.con
2143 cic:/matita/technicalities/setoids/nelistT.ind
2144 cic:/matita/technicalities/setoids/morphism_theory_of_predicate.con
2145 cic:/matita/technicalities/setoids/morphism_theory_of_function.con
2146 cic:/matita/technicalities/setoids/make_compatibility_goal_aux.con
2147 cic:/matita/technicalities/setoids/make_compatibility_goal.con
2148 cic:/matita/technicalities/setoids/list_of_Leibniz_of_list_of_types.con
2149 cic:/matita/technicalities/setoids/interp_relation_class_list.con
2150 cic:/matita/technicalities/setoids/interp.con
2151 cic:/matita/technicalities/setoids/impl_trans.con
2152 cic:/matita/technicalities/setoids/impl_refl.con
2153 cic:/matita/technicalities/setoids/impl.con
2154 cic:/matita/technicalities/setoids/get_rewrite_direction.con
2155 cic:/matita/technicalities/setoids/function_type_of_morphism_signature.con
2156 cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_reflexive_transitive_relation.con
2157 cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_areflexive_transitive_relation.con
2158 cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_reflexive_transitive_relation.con
2159 cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_areflexive_transitive_relation.con
2160 cic:/matita/technicalities/setoids/directed_relation_of_relation_class.con
2161 cic:/matita/technicalities/setoids/directed_relation_of_argument_class.con
2162 cic:/matita/technicalities/setoids/check_if_variance_is_respected_inv.con
2163 cic:/matita/technicalities/setoids/check_if_variance_is_respected_ind.con
2164 cic:/matita/technicalities/setoids/check_if_variance_is_respected.ind
2165 cic:/matita/technicalities/setoids/carrier_of_relation_class.con
2166 cic:/matita/technicalities/setoids/carrier_of_reflexive_relation_class.con
2167 cic:/matita/technicalities/setoids/carrier_of_areflexive_relation_class.con
2168 cic:/matita/technicalities/setoids/apply_morphism_compatibility_Right2Left.con
2169 cic:/matita/technicalities/setoids/apply_morphism_compatibility_Left2Right.con
2170 cic:/matita/technicalities/setoids/apply_morphism.con
2171 cic:/matita/technicalities/setoids/about_carrier_of_relation_class_and_relation_class_of_argument_class.con
2172 cic:/matita/technicalities/setoids/X_Relation_Class_rect.con
2173 cic:/matita/technicalities/setoids/X_Relation_Class_rec.con
2174 cic:/matita/technicalities/setoids/X_Relation_Class_ind.con
2175 cic:/matita/technicalities/setoids/X_Relation_Class.ind
2176 cic:/matita/technicalities/setoids/Relation_Class.con
2177 cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rect.con
2178 cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rec.con
2179 cic:/matita/technicalities/setoids/Reflexive_Relation_Class_ind.con
2180 cic:/matita/technicalities/setoids/Reflexive_Relation_Class.ind
2181 cic:/matita/technicalities/setoids/Morphism_Theory_rect.con
2182 cic:/matita/technicalities/setoids/Morphism_Theory_rec.con
2183 cic:/matita/technicalities/setoids/Morphism_Theory_ind.con
2184 cic:/matita/technicalities/setoids/Morphism_Theory.ind
2185 cic:/matita/technicalities/setoids/Morphism_Context_rect2.con
2186 cic:/matita/technicalities/setoids/Morphism_Context_rect.con
2187 cic:/matita/technicalities/setoids/Morphism_Context_rec.con
2188 cic:/matita/technicalities/setoids/Morphism_Context_inv.con
2189 cic:/matita/technicalities/setoids/Morphism_Context_ind.con
2190 cic:/matita/technicalities/setoids/Morphism_Context_List_rect2.con
2191 cic:/matita/technicalities/setoids/Morphism_Context_List_rect.con
2192 cic:/matita/technicalities/setoids/Morphism_Context_List_rec.con
2193 cic:/matita/technicalities/setoids/Morphism_Context_List_inv.con
2194 cic:/matita/technicalities/setoids/Morphism_Context_List_ind.con
2195 cic:/matita/technicalities/setoids/Morphism_Context.ind
2196 cic:/matita/technicalities/setoids/Impl_Relation_Class.con
2197 cic:/matita/technicalities/setoids/Iff_Relation_Class.con
2198 cic:/matita/technicalities/setoids/Function.con
2199 cic:/matita/technicalities/setoids/Compat.con
2200 cic:/matita/technicalities/setoids/Arguments.con
2201 cic:/matita/technicalities/setoids/Argument_Class.con
2202 cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rect.con
2203 cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rec.con
2204 cic:/matita/technicalities/setoids/Areflexive_Relation_Class_ind.con
2205 cic:/matita/technicalities/setoids/Areflexive_Relation_Class.ind