X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2Falluris.txt;h=0d49a6a7425a76edabbad17f91dfb6a623516729;hb=491d4b52a73ec28b4c8f28414d87d146e8caa40d;hp=5c8668c837253429412f7dbdb62f1cd05a6a7c97;hpb=c48c7e28f54e00e12755f703a8c46187be701ed2;p=helm.git diff --git a/helm/software/components/ng_kernel/alluris.txt b/helm/software/components/ng_kernel/alluris.txt index 5c8668c83..0d49a6a74 100644 --- a/helm/software/components/ng_kernel/alluris.txt +++ b/helm/software/components/ng_kernel/alluris.txt @@ -1,375 +1,491 @@ -cic:/matita/nat/compare/not_eq_to_eqb_false.con -cic:/matita/nat/compare/nat_compare_to_Prop.con -cic:/matita/nat/compare/nat_compare_pred_pred.con -cic:/matita/nat/compare/nat_compare_n_n.con -cic:/matita/nat/compare/nat_compare_n_m_m_n.con -cic:/matita/nat/compare/nat_compare_elim.con -cic:/matita/nat/compare/nat_compare_S_S.con -cic:/matita/nat/compare/nat_compare.con -cic:/matita/nat/compare/ltb_to_Prop.con -cic:/matita/nat/compare/ltb_elim.con -cic:/matita/nat/compare/ltb.con -cic:/matita/nat/compare/lt_to_leb_false.con -cic:/matita/nat/compare/leb_true_to_le.con -cic:/matita/nat/compare/leb_to_Prop.con -cic:/matita/nat/compare/leb_false_to_not_le.con -cic:/matita/nat/compare/leb_elim.con -cic:/matita/nat/compare/leb_demod3.con -cic:/matita/nat/compare/leb_demod2.con -cic:/matita/nat/compare/leb_demod1.con -cic:/matita/nat/compare/leb.con -cic:/matita/nat/compare/le_to_leb_true.con -cic:/matita/nat/compare/eqb_true_to_eq.con -cic:/matita/nat/compare/eqb_to_Prop.con -cic:/matita/nat/compare/eqb_n_n.con -cic:/matita/nat/compare/eqb_false_to_not_eq.con -cic:/matita/nat/compare/eqb_elim.con -cic:/matita/nat/compare/eqb.con -cic:/matita/nat/compare/eq_to_eqb_true.con -cic:/matita/nat/compare/compare_demod2.con -cic:/matita/nat/compare/compare_demod1.con -cic:/matita/nat/nat/pred_demod2.con -cic:/matita/nat/nat/pred_demod1.con -cic:/matita/nat/nat/pred_Sn.con -cic:/matita/nat/nat/pred.con -cic:/matita/nat/nat/not_zero.con -cic:/matita/nat/nat/not_eq_n_Sn.con -cic:/matita/nat/nat/not_eq_S.con -cic:/matita/nat/nat/not_eq_O_S.con -cic:/matita/nat/nat/nat_rect.con -cic:/matita/nat/nat/nat_rec.con -cic:/matita/nat/nat/nat_ind.con -cic:/matita/nat/nat/nat_elim2.con -cic:/matita/nat/nat/nat_case1.con -cic:/matita/nat/nat/nat_case.con -cic:/matita/nat/nat/nat.ind -cic:/matita/nat/nat/injective_S.con -cic:/matita/nat/nat/inj_S.con -cic:/matita/nat/nat/decidable_eq_nat.con -cic:/matita/nat/orders/transitive_lt.con -cic:/matita/nat/orders/transitive_le.con -cic:/matita/nat/orders/trans_lt.con -cic:/matita/nat/orders/trans_le.con -cic:/matita/nat/orders/not_lt_to_le.con -cic:/matita/nat/orders/not_le_to_lt.con -cic:/matita/nat/orders/not_le_Sn_n.con -cic:/matita/nat/orders/not_le_Sn_O.con -cic:/matita/nat/orders/not_eq_to_le_to_lt.con -cic:/matita/nat/orders/nat_elim1.con -cic:/matita/nat/orders/ltn_to_ltO.con -cic:/matita/nat/orders/lt_to_not_le.con -cic:/matita/nat/orders/lt_to_not_eq.con -cic:/matita/nat/orders/lt_to_lt_S_S.con -cic:/matita/nat/orders/lt_to_le_to_lt.con -cic:/matita/nat/orders/lt_to_le.con -cic:/matita/nat/orders/lt_pred.con -cic:/matita/nat/orders/lt_n_m_to_not_lt_m_Sn.con -cic:/matita/nat/orders/lt_S_to_lt.con -cic:/matita/nat/orders/lt_S_to_le.con -cic:/matita/nat/orders/lt_S_S_to_lt.con -cic:/matita/nat/orders/lt_SO_n_to_lt_O_pred_n.con -cic:/matita/nat/orders/lt_O_n_elim.con -cic:/matita/nat/orders/lt_O_S.con -cic:/matita/nat/orders/lt.con -cic:/matita/nat/orders/le_to_or_lt_eq.con -cic:/matita/nat/orders/le_to_not_lt.con -cic:/matita/nat/orders/le_to_lt_to_lt.con -cic:/matita/nat/orders/le_to_le_to_eq.con -cic:/matita/nat/orders/le_to_le_pred.con -cic:/matita/nat/orders/le_pred_to_le.con -cic:/matita/nat/orders/le_pred_n.con -cic:/matita/nat/orders/le_n_m_to_lt_m_Sn_to_eq_n_m.con -cic:/matita/nat/orders/le_n_fn.con -cic:/matita/nat/orders/le_n_Sn.con -cic:/matita/nat/orders/le_n_Sm_elim.con -cic:/matita/nat/orders/le_n_O_to_eq.con -cic:/matita/nat/orders/le_n_O_elim.con -cic:/matita/nat/orders/le_inv.con -cic:/matita/nat/orders/le_ind.con -cic:/matita/nat/orders/le_S_S_to_le.con -cic:/matita/nat/orders/le_S_S.con -cic:/matita/nat/orders/le_O_n.con -cic:/matita/nat/orders/leS_to_not_zero.con -cic:/matita/nat/orders/le.ind -cic:/matita/nat/orders/increasing_to_monotonic.con -cic:/matita/nat/orders/increasing_to_le2.con -cic:/matita/nat/orders/increasing_to_le.con -cic:/matita/nat/orders/increasing.con -cic:/matita/nat/orders/gt.con -cic:/matita/nat/orders/ge.con -cic:/matita/nat/orders/eq_to_not_lt.con -cic:/matita/nat/orders/decidable_lt.con -cic:/matita/nat/orders/decidable_le.con -cic:/matita/nat/orders/antisymmetric_le.con -cic:/matita/nat/orders/antisym_le.con -cic:/matita/nat/orders/S_pred.con -cic:/matita/nat/orders/Not_lt_n_n.con -cic:/matita/nat/plus/sym_plus.con -cic:/matita/nat/plus/plus_n_Sm.con -cic:/matita/nat/plus/plus_n_SO.con -cic:/matita/nat/plus/plus_n_O.con -cic:/matita/nat/plus/plus_demod4.con -cic:/matita/nat/plus/plus_demod3.con -cic:/matita/nat/plus/plus_demod2.con -cic:/matita/nat/plus/plus_demod1.con -cic:/matita/nat/plus/plus.con -cic:/matita/nat/plus/injective_plus_r.con -cic:/matita/nat/plus/injective_plus_l.con -cic:/matita/nat/plus/inj_plus_r.con -cic:/matita/nat/plus/inj_plus_l.con -cic:/matita/nat/plus/associative_plus.con -cic:/matita/nat/plus/assoc_plus.con -cic:/matita/nat/times/times_n_Sm.con -cic:/matita/nat/times/times_n_SO.con -cic:/matita/nat/times/times_n_O.con -cic:/matita/nat/times/times_demod6.con -cic:/matita/nat/times/times_demod4.con -cic:/matita/nat/times/times_demod2.con -cic:/matita/nat/times/times_demod1.con -cic:/matita/nat/times/times_SSO_n.con -cic:/matita/nat/times/times_SSO.con -cic:/matita/nat/times/times_O_to_O.con -cic:/matita/nat/times/times.con -cic:/matita/nat/times/symmetric_times.con -cic:/matita/nat/times/sym_times.con -cic:/matita/nat/times/or_eq_eq_S.con -cic:/matita/nat/times/distributive_times_plus.con -cic:/matita/nat/times/distr_times_plus.con -cic:/matita/nat/times/associative_times.con -cic:/matita/nat/times/assoc_times.con -cic:/matita/Z/z/pos_n_eq_S_n.con -cic:/matita/Z/z/not_eq_pos_neg.con -cic:/matita/Z/z/not_eq_OZ_pos.con -cic:/matita/Z/z/not_eq_OZ_neg.con -cic:/matita/Z/z/neg_Z_of_nat.con -cic:/matita/Z/z/injective_pos.con -cic:/matita/Z/z/injective_neg.con -cic:/matita/Z/z/inj_pos.con -cic:/matita/Z/z/inj_neg.con -cic:/matita/Z/z/decidable_eq_Z.con -cic:/matita/Z/z/abs.con -cic:/matita/Z/z/Zsucc_Zpred.con -cic:/matita/Z/z/Zsucc.con -cic:/matita/Z/z/Zpred_Zsucc.con -cic:/matita/Z/z/Zpred.con -cic:/matita/Z/z/Z_rect.con -cic:/matita/Z/z/Z_rec.con -cic:/matita/Z/z/Z_of_nat.con -cic:/matita/Z/z/Z_ind.con -cic:/matita/Z/z/Z.ind -cic:/matita/Z/z/OZ_test_to_Prop.con -cic:/matita/Z/z/OZ_test.con -cic:/matita/algebra/monoids/premonoid.con -cic:/matita/algebra/monoids/monoid_properties.con -cic:/matita/algebra/monoids/magma.con -cic:/matita/algebra/monoids/is_semi_group.con -cic:/matita/algebra/monoids/is_right_inverse.con -cic:/matita/algebra/monoids/is_left_inverse_to_is_right_inverse_to_eq.con -cic:/matita/algebra/monoids/is_left_inverse.con -cic:/matita/algebra/monoids/isSemiGroup_OF_Monoid.con -cic:/matita/algebra/monoids/isMonoid_rect.con -cic:/matita/algebra/monoids/isMonoid_rec.con -cic:/matita/algebra/monoids/isMonoid_ind.con -cic:/matita/algebra/monoids/isMonoid.ind -cic:/matita/algebra/monoids/e_is_right_unit.con -cic:/matita/algebra/monoids/e_is_left_unit.con -cic:/matita/algebra/monoids/e.con -cic:/matita/algebra/monoids/Type_OF_PreMonoid.con -cic:/matita/algebra/monoids/Type_OF_Monoid.con -cic:/matita/algebra/monoids/PreMonoid_rect.con -cic:/matita/algebra/monoids/PreMonoid_rec.con -cic:/matita/algebra/monoids/PreMonoid_ind.con -cic:/matita/algebra/monoids/PreMonoid.ind -cic:/matita/algebra/monoids/Monoid_rect.con -cic:/matita/algebra/monoids/Monoid_rec.con -cic:/matita/algebra/monoids/Monoid_ind.con -cic:/matita/algebra/monoids/Monoid.ind -cic:/matita/algebra/monoids/Magma_OF_Monoid.con -cic:/matita/algebra/semigroups/semigroup_properties.con -cic:/matita/algebra/semigroups/op_associative.con -cic:/matita/algebra/semigroups/op.con -cic:/matita/algebra/semigroups/magma.con -cic:/matita/algebra/semigroups/is_right_unit.con -cic:/matita/algebra/semigroups/is_left_unit_to_is_right_unit_to_eq.con -cic:/matita/algebra/semigroups/is_left_unit.con -cic:/matita/algebra/semigroups/isSemiGroup_rect.con -cic:/matita/algebra/semigroups/isSemiGroup_rec.con -cic:/matita/algebra/semigroups/isSemiGroup_ind.con -cic:/matita/algebra/semigroups/isSemiGroup.ind -cic:/matita/algebra/semigroups/carrier.con -cic:/matita/algebra/semigroups/Type_OF_SemiGroup.con -cic:/matita/algebra/semigroups/SemiGroup_rect.con -cic:/matita/algebra/semigroups/SemiGroup_rec.con -cic:/matita/algebra/semigroups/SemiGroup_ind.con -cic:/matita/algebra/semigroups/SemiGroup.ind -cic:/matita/algebra/semigroups/Magma_rect.con -cic:/matita/algebra/semigroups/Magma_rec.con -cic:/matita/algebra/semigroups/Magma_ind.con -cic:/matita/algebra/semigroups/Magma.ind -cic:/matita/datatypes/bool/true_to_true_to_andb_true.con -cic:/matita/datatypes/bool/orb_sym.con -cic:/matita/datatypes/bool/orb_elim.con -cic:/matita/datatypes/bool/orb.con -cic:/matita/datatypes/bool/notb_notb.con -cic:/matita/datatypes/bool/notb_elim.con -cic:/matita/datatypes/bool/notb.con -cic:/matita/datatypes/bool/not_eq_true_false.con -cic:/matita/datatypes/bool/injective_notb.con -cic:/matita/datatypes/bool/if_then_else.con -cic:/matita/datatypes/bool/bool_to_decidable_eq.con -cic:/matita/datatypes/bool/bool_rect.con -cic:/matita/datatypes/bool/bool_rec.con -cic:/matita/datatypes/bool/bool_ind.con -cic:/matita/datatypes/bool/bool_elim.con -cic:/matita/datatypes/bool/bool.ind -cic:/matita/datatypes/bool/andb_true_true_r.con -cic:/matita/datatypes/bool/andb_true_true.con -cic:/matita/datatypes/bool/andb_sym.con -cic:/matita/datatypes/bool/andb_elim.con -cic:/matita/datatypes/bool/andb_assoc.con -cic:/matita/datatypes/bool/andb.con -cic:/matita/datatypes/bool/and_true.con -cic:/matita/datatypes/bool/P_x_to_P_x_to_eq.con -cic:/matita/datatypes/compare/compare_rect.con -cic:/matita/datatypes/compare/compare_rec.con -cic:/matita/datatypes/compare/compare_invert.con -cic:/matita/datatypes/compare/compare_ind.con -cic:/matita/datatypes/compare/compare.ind -cic:/matita/datatypes/constructors/void_rect.con -cic:/matita/datatypes/constructors/void_rec.con -cic:/matita/datatypes/constructors/void_ind.con -cic:/matita/datatypes/constructors/void.ind -cic:/matita/datatypes/constructors/unit_rect.con -cic:/matita/datatypes/constructors/unit_rec.con -cic:/matita/datatypes/constructors/unit_ind.con -cic:/matita/datatypes/constructors/unit.ind -cic:/matita/datatypes/constructors/snd.con -cic:/matita/datatypes/constructors/option_rect.con -cic:/matita/datatypes/constructors/option_rec.con -cic:/matita/datatypes/constructors/option_ind.con -cic:/matita/datatypes/constructors/option.ind -cic:/matita/datatypes/constructors/fst.con -cic:/matita/datatypes/constructors/eq_pair_fst_snd.con -cic:/matita/datatypes/constructors/Sum_rect.con -cic:/matita/datatypes/constructors/Sum_rec.con -cic:/matita/datatypes/constructors/Sum_ind.con -cic:/matita/datatypes/constructors/Sum.ind -cic:/matita/datatypes/constructors/Prod_rect.con -cic:/matita/datatypes/constructors/Prod_rec.con -cic:/matita/datatypes/constructors/Prod_ind.con -cic:/matita/datatypes/constructors/Prod.ind -cic:/matita/decidable_kit/decidable/reflect_rect.con -cic:/matita/decidable_kit/decidable/reflect_rec.con -cic:/matita/decidable_kit/decidable/reflect_inv.con -cic:/matita/decidable_kit/decidable/reflect_ind.con -cic:/matita/decidable_kit/decidable/reflect.ind -cic:/matita/decidable_kit/decidable/prove_reflect.con -cic:/matita/decidable_kit/decidable/p2bT.con -cic:/matita/decidable_kit/decidable/p2bF.con -cic:/matita/decidable_kit/decidable/orbP.con -cic:/matita/decidable_kit/decidable/orbC.con -cic:/matita/decidable_kit/decidable/orb.con -cic:/matita/decidable_kit/decidable/negbP.con -cic:/matita/decidable_kit/decidable/negb.con -cic:/matita/decidable_kit/decidable/ltb_refl.con -cic:/matita/decidable_kit/decidable/ltb_n_Sm.con -cic:/matita/decidable_kit/decidable/ltbW.con -cic:/matita/decidable_kit/decidable/ltbP.con -cic:/matita/decidable_kit/decidable/ltb.con -cic:/matita/decidable_kit/decidable/ltW.con -cic:/matita/decidable_kit/decidable/ltS.con -cic:/matita/decidable_kit/decidable/ltS'.con -cic:/matita/decidable_kit/decidable/leb_refl.con -cic:/matita/decidable_kit/decidable/leb_eqb.con -cic:/matita/decidable_kit/decidable/lebW.con -cic:/matita/decidable_kit/decidable/lebP.con -cic:/matita/decidable_kit/decidable/idP.con -cic:/matita/decidable_kit/decidable/eq_to_bool.con -cic:/matita/decidable_kit/decidable/congr_S.con -cic:/matita/decidable_kit/decidable/bool_to_eq.con -cic:/matita/decidable_kit/decidable/b2pT.con -cic:/matita/decidable_kit/decidable/b2pF.con -cic:/matita/decidable_kit/decidable/andbPF.con -cic:/matita/decidable_kit/decidable/andbP.con -cic:/matita/decidable_kit/decidable/andb.con -cic:/matita/decidable_kit/eqtype/test_canonical_option_eqType.con -cic:/matita/decidable_kit/eqtype/sval.con -cic:/matita/decidable_kit/eqtype/sub_eqType.con -cic:/matita/decidable_kit/eqtype/sprop.con -cic:/matita/decidable_kit/eqtype/sort_OF_nat.con -cic:/matita/decidable_kit/eqtype/sort_OF_bool.con -cic:/matita/decidable_kit/eqtype/sort.con -cic:/matita/decidable_kit/eqtype/sigma_rect.con -cic:/matita/decidable_kit/eqtype/sigma_rec.con -cic:/matita/decidable_kit/eqtype/sigma_ind.con -cic:/matita/decidable_kit/eqtype/sigma_eq_dec.con -cic:/matita/decidable_kit/eqtype/sigma.ind -cic:/matita/decidable_kit/eqtype/option_eqType.con -cic:/matita/decidable_kit/eqtype/option_canonical_eqType.con -cic:/matita/decidable_kit/eqtype/ocmpP.con -cic:/matita/decidable_kit/eqtype/ocmp.con -cic:/matita/decidable_kit/eqtype/nat_eqType.con -cic:/matita/decidable_kit/eqtype/nat_canonical_eqType.con -cic:/matita/decidable_kit/eqtype/in_sub_rect.con -cic:/matita/decidable_kit/eqtype/in_sub_rec.con -cic:/matita/decidable_kit/eqtype/in_sub_inv.con -cic:/matita/decidable_kit/eqtype/in_sub_ind.con -cic:/matita/decidable_kit/eqtype/in_sub_eq.con -cic:/matita/decidable_kit/eqtype/in_sub.ind -cic:/matita/decidable_kit/eqtype/if_p.con -cic:/matita/decidable_kit/eqtype/eqbP.con -cic:/matita/decidable_kit/eqtype/eq_compatible.con -cic:/matita/decidable_kit/eqtype/eqType_rect.con -cic:/matita/decidable_kit/eqtype/eqType_rec.con -cic:/matita/decidable_kit/eqtype/eqType_ind.con -cic:/matita/decidable_kit/eqtype/eqType_decidable.con -cic:/matita/decidable_kit/eqtype/eqType.ind -cic:/matita/decidable_kit/eqtype/eqP.con -cic:/matita/decidable_kit/eqtype/cmp_refl.con -cic:/matita/decidable_kit/eqtype/cmpP.con -cic:/matita/decidable_kit/eqtype/cmpC.con -cic:/matita/decidable_kit/eqtype/cmp.con -cic:/matita/decidable_kit/eqtype/bool_eqType.con -cic:/matita/decidable_kit/eqtype/bool_canonical_eqType.con -cic:/matita/decidable_kit/eqtype/bcmpP.con -cic:/matita/decidable_kit/eqtype/bcmp.con -cic:/matita/decidable_kit/list_aux/mem.con -cic:/matita/decidable_kit/list_aux/list_eqType.con -cic:/matita/decidable_kit/list_aux/lcmp_length.con -cic:/matita/decidable_kit/list_aux/lcmpP.con -cic:/matita/decidable_kit/list_aux/lcmp.con -cic:/matita/decidable_kit/list_aux/count.con -cic:/matita/decidable_kit/streicher/stepH.con -cic:/matita/decidable_kit/streicher/step.con -cic:/matita/decidable_kit/streicher/pirrel.con -cic:/matita/decidable_kit/streicher/nu_k.con -cic:/matita/decidable_kit/streicher/nu_inv.con -cic:/matita/decidable_kit/streicher/nu.con -cic:/matita/decidable_kit/streicher/decT.con -cic:/matita/decidable_kit/streicher/cancel_nu_nu_inv.con -cic:/matita/decidable_kit/streicher/cancel.con -cic:/matita/demo/realisability/type_OF_SP.con -cic:/matita/demo/realisability/true_impl_realized.con -cic:/matita/demo/realisability/sigma_rect.con -cic:/matita/demo/realisability/sigma_rec.con -cic:/matita/demo/realisability/sigma_ind.con -cic:/matita/demo/realisability/sigma.ind -cic:/matita/demo/realisability/realized.con -cic:/matita/demo/realisability/pi2.con -cic:/matita/demo/realisability/pi1.con -cic:/matita/demo/realisability/modr.con -cic:/matita/demo/realisability/id_axiom.con -cic:/matita/demo/realisability/extraction.con -cic:/matita/demo/realisability/elim_abs.con -cic:/matita/demo/realisability/cut.con -cic:/matita/demo/realisability/correct2.con -cic:/matita/demo/realisability/correct.con -cic:/matita/demo/realisability/and_i.con -cic:/matita/demo/realisability/SP_rect.con -cic:/matita/demo/realisability/SP_rec.con -cic:/matita/demo/realisability/SP_ind.con -cic:/matita/demo/realisability/SP.ind -cic:/matita/demo/realisability/Prop_OF_SP.con +cic:/CoRN/algebra/Basics/well_founded_ltof.con +cic:/CoRN/algebra/Basics/well_founded_induction_type.con +cic:/CoRN/algebra/Basics/well_founded.con +cic:/CoRN/algebra/Basics/surj_not.con +cic:/CoRN/algebra/Basics/surj_lt_subproof.con +cic:/CoRN/algebra/Basics/surj_lt.con +cic:/CoRN/algebra/Basics/surj_le_subproof.con +cic:/CoRN/algebra/Basics/surj_le.con +cic:/CoRN/algebra/Basics/surj_eq_subproof.con +cic:/CoRN/algebra/Basics/surj_eq.con +cic:/CoRN/algebra/Basics/proper_caseZ_diff_subproof0.con +cic:/CoRN/algebra/Basics/proper_caseZ_diff_subproof.con +cic:/CoRN/algebra/Basics/proper_caseZ_diff.con +cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con +cic:/CoRN/algebra/Basics/power.con +cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con +cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con +cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con +cic:/CoRN/algebra/Basics/nats_Z_ind.con +cic:/CoRN/algebra/Basics/nat_fac_gtzero.con +cic:/CoRN/algebra/Basics/minus4_subproof1.con +cic:/CoRN/algebra/Basics/minus4_subproof0.con +cic:/CoRN/algebra/Basics/minus4_subproof.con +cic:/CoRN/algebra/Basics/minus4.con +cic:/CoRN/algebra/Basics/minus3_subproof1.con +cic:/CoRN/algebra/Basics/minus3_subproof0.con +cic:/CoRN/algebra/Basics/minus3_subproof.con +cic:/CoRN/algebra/Basics/minus3.con +cic:/CoRN/algebra/Basics/min_convert_is_NEG.con +cic:/CoRN/algebra/Basics/ltof.con +cic:/CoRN/algebra/Basics/lt_z_two.con +cic:/CoRN/algebra/Basics/lt_wf_rect.con +cic:/CoRN/algebra/Basics/lt_mult_right.con +cic:/CoRN/algebra/Basics/lt_lt_minus_subproof.con +cic:/CoRN/algebra/Basics/lt_lt_minus.con +cic:/CoRN/algebra/Basics/lt_le_dec.con +cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con +cic:/CoRN/algebra/Basics/le_pred.con +cic:/CoRN/algebra/Basics/le_mult_right.con +cic:/CoRN/algebra/Basics/inject_nat_convert.con +cic:/CoRN/algebra/Basics/induction_ltof2T.con +cic:/CoRN/algebra/Basics/fac.con +cic:/CoRN/algebra/Basics/diff_Z_ind_subproof.con +cic:/CoRN/algebra/Basics/diff_Z_ind.con +cic:/CoRN/algebra/Basics/convert_is_POS.con +cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con +cic:/CoRN/algebra/Basics/caseZ_diff_O.con +cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con +cic:/CoRN/algebra/Basics/caseZ_diff.con +cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con +cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con +cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con +cic:/CoRN/algebra/Basics/Zmult_absorb.con +cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con +cic:/CoRN/algebra/Basics/Zlt_opp.con +cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con +cic:/CoRN/algebra/Basics/Zgt_not_eq.con +cic:/CoRN/algebra/Basics/Z_to_nat_correct.con +cic:/CoRN/algebra/Basics/Z_to_nat.con +cic:/CoRN/algebra/Basics/Z_exh.con +cic:/CoRN/algebra/Basics/POS_anti_convert.con +cic:/CoRN/algebra/Basics/NEG_anti_convert.con +cic:/CoRN/algebra/Basics/Acc_iter.con +cic:/CoRN/algebra/Basics/Acc_inv.con +cic:/CoRN/algebra/Basics/Acc_ind.con +cic:/CoRN/algebra/Basics/Acc.ind +cic:/CoRN/algebra/CAbGroups/zmult_zero.con +cic:/CoRN/algebra/CAbGroups/zmult_wd.con +cic:/CoRN/algebra/CAbGroups/zmult_plus.con +cic:/CoRN/algebra/CAbGroups/zmult_plus'.con +cic:/CoRN/algebra/CAbGroups/zmult_one.con +cic:/CoRN/algebra/CAbGroups/zmult_mult.con +cic:/CoRN/algebra/CAbGroups/zmult_min_one.con +cic:/CoRN/algebra/CAbGroups/zmult_char_subproof1.con +cic:/CoRN/algebra/CAbGroups/zmult_char_subproof0.con +cic:/CoRN/algebra/CAbGroups/zmult_char_subproof.con +cic:/CoRN/algebra/CAbGroups/zmult_char.con +cic:/CoRN/algebra/CAbGroups/zmult_Zero.con +cic:/CoRN/algebra/CAbGroups/zmult.con +cic:/CoRN/algebra/CAbGroups/plus_runit.con +cic:/CoRN/algebra/CAbGroups/plus_rext.con +cic:/CoRN/algebra/CAbGroups/plus_is_fun.con +cic:/CoRN/algebra/CAbGroups/plus_fun.con +cic:/CoRN/algebra/CAbGroups/plus_cancel_ap_lft.con +cic:/CoRN/algebra/CAbGroups/op_lft_resp_ap.con +cic:/CoRN/algebra/CAbGroups/nmult_wd.con +cic:/CoRN/algebra/CAbGroups/nmult_plus.con +cic:/CoRN/algebra/CAbGroups/nmult_plus'.con +cic:/CoRN/algebra/CAbGroups/nmult_one.con +cic:/CoRN/algebra/CAbGroups/nmult_mult.con +cic:/CoRN/algebra/CAbGroups/nmult_inv.con +cic:/CoRN/algebra/CAbGroups/nmult_Zero.con +cic:/CoRN/algebra/CAbGroups/nmult.con +cic:/CoRN/algebra/CAbGroups/minus_plus.con +cic:/CoRN/algebra/CAbGroups/isabgrp_scrr.con +cic:/CoRN/algebra/CAbGroups/is_CAbGroup.con +cic:/CoRN/algebra/CAbGroups/inv_inv'.con +cic:/CoRN/algebra/CAbGroups/cag_proof.con +cic:/CoRN/algebra/CAbGroups/cag_op_inv.con +cic:/CoRN/algebra/CAbGroups/cag_crr.con +cic:/CoRN/algebra/CAbGroups/cag_commutes_unfolded.con +cic:/CoRN/algebra/CAbGroups/cag_commutes.con +cic:/CoRN/algebra/CAbGroups/cag_ap_cancel_lft.con +cic:/CoRN/algebra/CAbGroups/assoc_1.con +cic:/CoRN/algebra/CAbGroups/CAbGroup_rect.con +cic:/CoRN/algebra/CAbGroups/CAbGroup_rec.con +cic:/CoRN/algebra/CAbGroups/CAbGroup_is_CAbGroup.con +cic:/CoRN/algebra/CAbGroups/CAbGroup_ind.con +cic:/CoRN/algebra/CAbGroups/CAbGroup.ind +cic:/CoRN/algebra/CAbGroups/Build_SubCAbGroup.con +cic:/CoRN/algebra/CAbGroups/Build_CSemiGroup'.con +cic:/CoRN/algebra/CAbGroups/Build_CMonoid'.con +cic:/CoRN/algebra/CAbGroups/Build_CGroup'.con +cic:/CoRN/algebra/CAbGroups/Build_CAbGroup'.con +cic:/CoRN/algebra/CAbMonoids/isabgrp_scrr.con +cic:/CoRN/algebra/CAbMonoids/is_CAbMonoid.con +cic:/CoRN/algebra/CAbMonoids/cam_proof.con +cic:/CoRN/algebra/CAbMonoids/cam_crr.con +cic:/CoRN/algebra/CAbMonoids/cam_commutes_unfolded.con +cic:/CoRN/algebra/CAbMonoids/cam_commutes.con +cic:/CoRN/algebra/CAbMonoids/CAbMonoid_rect.con +cic:/CoRN/algebra/CAbMonoids/CAbMonoid_rec.con +cic:/CoRN/algebra/CAbMonoids/CAbMonoid_is_CAbMonoid.con +cic:/CoRN/algebra/CAbMonoids/CAbMonoid_ind.con +cic:/CoRN/algebra/CAbMonoids/CAbMonoid.ind +cic:/CoRN/algebra/CAbMonoids/Build_SubCAbMonoid.con +cic:/CoRN/algebra/CHomomorphism_Theorems/tau_surj.con +cic:/CoRN/algebra/CHomomorphism_Theorems/tau_strext.con +cic:/CoRN/algebra/CHomomorphism_Theorems/tau_is_fun.con +cic:/CoRN/algebra/CHomomorphism_Theorems/tau.con +cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_strext.con +cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_is_fun.con +cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_inj.con +cic:/CoRN/algebra/CHomomorphism_Theorems/sigst.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cswdpredR.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cswdpred.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cspredR.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cspred.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cs_is_comod.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cs_is_coideal.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cs_as_comod.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cs_as_coideal.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_surj.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_strext.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_is_fun.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_strext.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_is_fun.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_inj.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst.con +cic:/CoRN/algebra/CHomomorphism_Theorems/RingHomTheorem.con +cic:/CoRN/algebra/CHomomorphism_Theorems/RdivCsR.con +cic:/CoRN/algebra/CHomomorphism_Theorems/ModHomTheorem.con +cic:/CoRN/algebra/CHomomorphism_Theorems/CsR.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Cs.con +cic:/CoRN/algebra/CHomomorphism_Theorems/AdivCs.con +cic:/CoRN/algebra/CIdeals/is_ideal_rect.con +cic:/CoRN/algebra/CIdeals/is_ideal_rec.con +cic:/CoRN/algebra/CIdeals/is_ideal_ind.con +cic:/CoRN/algebra/CIdeals/is_ideal.ind +cic:/CoRN/algebra/CIdeals/is_coideal_rect.con +cic:/CoRN/algebra/CIdeals/is_coideal_rec.con +cic:/CoRN/algebra/CIdeals/is_coideal_ind.con +cic:/CoRN/algebra/CIdeals/is_coideal.ind +cic:/CoRN/algebra/CIdeals/idprpl.con +cic:/CoRN/algebra/CIdeals/idproof.con +cic:/CoRN/algebra/CIdeals/idpred.con +cic:/CoRN/algebra/CIdeals/ideal_rect.con +cic:/CoRN/algebra/CIdeals/ideal_rec.con +cic:/CoRN/algebra/CIdeals/ideal_is_ideal.con +cic:/CoRN/algebra/CIdeals/ideal_ind.con +cic:/CoRN/algebra/CIdeals/ideal_as_CSetoid.con +cic:/CoRN/algebra/CIdeals/ideal.ind +cic:/CoRN/algebra/CIdeals/idax.con +cic:/CoRN/algebra/CIdeals/coideal_wd.con +cic:/CoRN/algebra/CIdeals/coideal_rect.con +cic:/CoRN/algebra/CIdeals/coideal_rec.con +cic:/CoRN/algebra/CIdeals/coideal_plus.con +cic:/CoRN/algebra/CIdeals/coideal_nonzero.con +cic:/CoRN/algebra/CIdeals/coideal_nontriv.con +cic:/CoRN/algebra/CIdeals/coideal_mult.con +cic:/CoRN/algebra/CIdeals/coideal_is_coideal.con +cic:/CoRN/algebra/CIdeals/coideal_ind.con +cic:/CoRN/algebra/CIdeals/coideal_as_CSetoid.con +cic:/CoRN/algebra/CIdeals/coideal_apzero.con +cic:/CoRN/algebra/CIdeals/coideal.ind +cic:/CoRN/algebra/CIdeals/ciproof.con +cic:/CoRN/algebra/CIdeals/cipred.con +cic:/CoRN/algebra/CIdeals/ciplus.con +cic:/CoRN/algebra/CIdeals/cinontriv.con +cic:/CoRN/algebra/CIdeals/cimult.con +cic:/CoRN/algebra/CIdeals/ciapzero.con +cic:/CoRN/algebra/CLogic/weird_mon_covers.con +cic:/CoRN/algebra/CLogic/to_Codd_even.con +cic:/CoRN/algebra/CLogic/to_Codd.con +cic:/CoRN/algebra/CLogic/to_Ceven.con +cic:/CoRN/algebra/CLogic/toCle.con +cic:/CoRN/algebra/CLogic/toCProp_rect.con +cic:/CoRN/algebra/CLogic/toCProp_rec.con +cic:/CoRN/algebra/CLogic/toCProp_lt.con +cic:/CoRN/algebra/CLogic/toCProp_ind.con +cic:/CoRN/algebra/CLogic/toCProp_e.con +cic:/CoRN/algebra/CLogic/toCProp_Zlt.con +cic:/CoRN/algebra/CLogic/toCProp.ind +cic:/CoRN/algebra/CLogic/str_finite_or_elim.con +cic:/CoRN/algebra/CLogic/sig2T_rect.con +cic:/CoRN/algebra/CLogic/sig2T_rec.con +cic:/CoRN/algebra/CLogic/sig2T_ind.con +cic:/CoRN/algebra/CLogic/sig2T.ind +cic:/CoRN/algebra/CLogic/proj2b_sig2T.con +cic:/CoRN/algebra/CLogic/proj2a_sig2T.con +cic:/CoRN/algebra/CLogic/proj2_sigT.con +cic:/CoRN/algebra/CLogic/proj1_sigT.con +cic:/CoRN/algebra/CLogic/proj1_sig2T.con +cic:/CoRN/algebra/CLogic/pred_lt.con +cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con +cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con +cic:/CoRN/algebra/CLogic/odd_induction.con +cic:/CoRN/algebra/CLogic/odd_ind.con +cic:/CoRN/algebra/CLogic/odd_double_ind.con +cic:/CoRN/algebra/CLogic/not_r_sum_rec.con +cic:/CoRN/algebra/CLogic/not_r_cor_rect.con +cic:/CoRN/algebra/CLogic/not_not_lt.con +cic:/CoRN/algebra/CLogic/not_l_sum_rec.con +cic:/CoRN/algebra/CLogic/not_l_cor_rect.con +cic:/CoRN/algebra/CLogic/nat_nat_pos.con +cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con +cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con +cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con +cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con +cic:/CoRN/algebra/CLogic/nat_less_n_pred.con +cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con +cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con +cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con +cic:/CoRN/algebra/CLogic/my_Cle_ind.con +cic:/CoRN/algebra/CLogic/mon_fun_covers.con +cic:/CoRN/algebra/CLogic/member_app.con +cic:/CoRN/algebra/CLogic/member.con +cic:/CoRN/algebra/CLogic/lt_pred'.con +cic:/CoRN/algebra/CLogic/lt_8.con +cic:/CoRN/algebra/CLogic/lt_5.con +cic:/CoRN/algebra/CLogic/lt_10.con +cic:/CoRN/algebra/CLogic/le_2.con +cic:/CoRN/algebra/CLogic/le_1.con +cic:/CoRN/algebra/CLogic/kseq_prop.con +cic:/CoRN/algebra/CLogic/four_induction.con +cic:/CoRN/algebra/CLogic/four_ind.con +cic:/CoRN/algebra/CLogic/finite_or_elim.con +cic:/CoRN/algebra/CLogic/even_plus_n_n.con +cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con +cic:/CoRN/algebra/CLogic/even_or_odd_plus.con +cic:/CoRN/algebra/CLogic/even_induction.con +cic:/CoRN/algebra/CLogic/even_ind.con +cic:/CoRN/algebra/CLogic/choice.con +cic:/CoRN/algebra/CLogic/absolu_2.con +cic:/CoRN/algebra/CLogic/absolu_1.con +cic:/CoRN/algebra/CLogic/Zsgn_5.con +cic:/CoRN/algebra/CLogic/Zsgn_4.con +cic:/CoRN/algebra/CLogic/Zsgn_3.con +cic:/CoRN/algebra/CLogic/Zsgn_2.con +cic:/CoRN/algebra/CLogic/Zsgn_1.con +cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con +cic:/CoRN/algebra/CLogic/Zlts.con +cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con +cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con +cic:/CoRN/algebra/CLogic/ZL9.con +cic:/CoRN/algebra/CLogic/ZL4'.con +cic:/CoRN/algebra/CLogic/Ttransitive.con +cic:/CoRN/algebra/CLogic/Tsymmetric.con +cic:/CoRN/algebra/CLogic/Trelation.con +cic:/CoRN/algebra/CLogic/Treflexive.con +cic:/CoRN/algebra/CLogic/Tequiv.con +cic:/CoRN/algebra/CLogic/S_predn.con +cic:/CoRN/algebra/CLogic/Not.con +cic:/CoRN/algebra/CLogic/Iff_trans.con +cic:/CoRN/algebra/CLogic/Iff_sym.con +cic:/CoRN/algebra/CLogic/Iff_right.con +cic:/CoRN/algebra/CLogic/Iff_refl.con +cic:/CoRN/algebra/CLogic/Iff_left.con +cic:/CoRN/algebra/CLogic/Iff_imp_imp.con +cic:/CoRN/algebra/CLogic/Iff.con +cic:/CoRN/algebra/CLogic/Ctransitive.con +cic:/CoRN/algebra/CLogic/Csymmetric.con +cic:/CoRN/algebra/CLogic/Crelation.con +cic:/CoRN/algebra/CLogic/Creflexive.con +cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con +cic:/CoRN/algebra/CLogic/Codd_to.con +cic:/CoRN/algebra/CLogic/Codd_rect.con +cic:/CoRN/algebra/CLogic/Codd_rec.con +cic:/CoRN/algebra/CLogic/Codd_ind.con +cic:/CoRN/algebra/CLogic/Codd_even_to.con +cic:/CoRN/algebra/CLogic/Codd.ind +cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con +cic:/CoRN/algebra/CLogic/Cnat_total_order.con +cic:/CoRN/algebra/CLogic/Cnat_double_ind.con +cic:/CoRN/algebra/CLogic/Clt_to.con +cic:/CoRN/algebra/CLogic/Clt_le_weak.con +cic:/CoRN/algebra/CLogic/Clt.con +cic:/CoRN/algebra/CLogic/Cle_to.con +cic:/CoRN/algebra/CLogic/Cle_rect.con +cic:/CoRN/algebra/CLogic/Cle_rec.con +cic:/CoRN/algebra/CLogic/Cle_n_S.con +cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con +cic:/CoRN/algebra/CLogic/Cle_ind.con +cic:/CoRN/algebra/CLogic/Cle.ind +cic:/CoRN/algebra/CLogic/Ceven_to.con +cic:/CoRN/algebra/CLogic/Ceven_rect.con +cic:/CoRN/algebra/CLogic/Ceven_rec.con +cic:/CoRN/algebra/CLogic/Ceven_ind.con +cic:/CoRN/algebra/CLogic/Cequiv.con +cic:/CoRN/algebra/CLogic/Cdiff_Z_ind_subproof.con +cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con +cic:/CoRN/algebra/CLogic/Cdecidable.con +cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con +cic:/CoRN/algebra/CLogic/Ccontrapos'.con +cic:/CoRN/algebra/CLogic/CZlt_to.con +cic:/CoRN/algebra/CLogic/CZ_exh.con +cic:/CoRN/algebra/CLogic/CTrue_rect.con +cic:/CoRN/algebra/CLogic/CTrue_rec.con +cic:/CoRN/algebra/CLogic/CTrue_ind.con +cic:/CoRN/algebra/CLogic/CTrue.ind +cic:/CoRN/algebra/CLogic/CProp.con +cic:/CoRN/algebra/CLogic/COr_rect.con +cic:/CoRN/algebra/CLogic/COr_rec.con +cic:/CoRN/algebra/CLogic/COr_ind.con +cic:/CoRN/algebra/CLogic/COr.ind +cic:/CoRN/algebra/CLogic/CNot_Not_or.con +cic:/CoRN/algebra/CLogic/CNot.con +cic:/CoRN/algebra/CLogic/CFalse_rect.con +cic:/CoRN/algebra/CLogic/CFalse_rec.con +cic:/CoRN/algebra/CLogic/CFalse_ind.con +cic:/CoRN/algebra/CLogic/CFalse.ind +cic:/CoRN/algebra/CLogic/CAnd_rect.con +cic:/CoRN/algebra/CLogic/CAnd_rec.con +cic:/CoRN/algebra/CLogic/CAnd_proj2.con +cic:/CoRN/algebra/CLogic/CAnd_proj1.con +cic:/CoRN/algebra/CLogic/CAnd_ind.con +cic:/CoRN/algebra/CLogic/CAnd.ind +cic:/CoRN/algebra/CModule_Homomorphisms/mh_strext.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_zero.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_unit.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_plus.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_mult.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_minus.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_apzero.con +cic:/CoRN/algebra/CModule_Homomorphisms/hommap.con +cic:/CoRN/algebra/CModule_Homomorphisms/hom3.con +cic:/CoRN/algebra/CModule_Homomorphisms/hom2.con +cic:/CoRN/algebra/CModule_Homomorphisms/hom1.con +cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_unit.con +cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_plus.con +cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_mult.con +cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_rect.con +cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_rec.con +cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_ind.con +cic:/CoRN/algebra/CModule_Homomorphisms/ModHom.ind +cic:/CoRN/algebra/CModules/submod_rect.con +cic:/CoRN/algebra/CModules/submod_rec.con +cic:/CoRN/algebra/CModules/submod_is_submod.con +cic:/CoRN/algebra/CModules/submod_ind.con +cic:/CoRN/algebra/CModules/submod_as_CSetoid.con +cic:/CoRN/algebra/CModules/submod.ind +cic:/CoRN/algebra/CModules/smzero.con +cic:/CoRN/algebra/CModules/smproof.con +cic:/CoRN/algebra/CModules/smpred.con +cic:/CoRN/algebra/CModules/smplus.con +cic:/CoRN/algebra/CModules/smmult.con +cic:/CoRN/algebra/CModules/rm_proof.con +cic:/CoRN/algebra/CModules/rm_pl2.con +cic:/CoRN/algebra/CModules/rm_pl1.con +cic:/CoRN/algebra/CModules/rm_one.con +cic:/CoRN/algebra/CModules/rm_mult.con +cic:/CoRN/algebra/CModules/rm_mu.con +cic:/CoRN/algebra/CModules/rm_crr.con +cic:/CoRN/algebra/CModules/mu_zerox.con +cic:/CoRN/algebra/CModules/mu_strext.con +cic:/CoRN/algebra/CModules/mu_plus2.con +cic:/CoRN/algebra/CModules/mu_plus1.con +cic:/CoRN/algebra/CModules/mu_one.con +cic:/CoRN/algebra/CModules/mu_mult.con +cic:/CoRN/algebra/CModules/mu_minusonex.con +cic:/CoRN/algebra/CModules/mu_minusax.con +cic:/CoRN/algebra/CModules/mu_azero.con +cic:/CoRN/algebra/CModules/mu_axap0_xap0.con +cic:/CoRN/algebra/CModules/mu_axap0_aap0.con +cic:/CoRN/algebra/CModules/mu_aminusx.con +cic:/CoRN/algebra/CModules/mu0help2.con +cic:/CoRN/algebra/CModules/mu0help.con +cic:/CoRN/algebra/CModules/is_submod_rect.con +cic:/CoRN/algebra/CModules/is_submod_rec.con +cic:/CoRN/algebra/CModules/is_submod_ind.con +cic:/CoRN/algebra/CModules/is_submod.ind +cic:/CoRN/algebra/CModules/is_comod_rect.con +cic:/CoRN/algebra/CModules/is_comod_rec.con +cic:/CoRN/algebra/CModules/is_comod_ind.con +cic:/CoRN/algebra/CModules/is_comod.ind +cic:/CoRN/algebra/CModules/is_RModule_rect.con +cic:/CoRN/algebra/CModules/is_RModule_rec.con +cic:/CoRN/algebra/CModules/is_RModule_ind.con +cic:/CoRN/algebra/CModules/is_RModule.ind +cic:/CoRN/algebra/CModules/comod_wd.con +cic:/CoRN/algebra/CModules/comod_rect.con +cic:/CoRN/algebra/CModules/comod_rec.con +cic:/CoRN/algebra/CModules/comod_plus.con +cic:/CoRN/algebra/CModules/comod_nonzero.con +cic:/CoRN/algebra/CModules/comod_mult.con +cic:/CoRN/algebra/CModules/comod_is_comod.con +cic:/CoRN/algebra/CModules/comod_ind.con +cic:/CoRN/algebra/CModules/comod_as_CSetoid.con +cic:/CoRN/algebra/CModules/comod_apzero.con +cic:/CoRN/algebra/CModules/comod.ind +cic:/CoRN/algebra/CModules/cmproof.con +cic:/CoRN/algebra/CModules/cmpred.con +cic:/CoRN/algebra/CModules/cmplus.con +cic:/CoRN/algebra/CModules/cmmult.con +cic:/CoRN/algebra/CModules/cmapzero.con +cic:/CoRN/algebra/CModules/R_is_RModule.con +cic:/CoRN/algebra/CModules/R_as_RModule.con +cic:/CoRN/algebra/CModules/RModule_rect.con +cic:/CoRN/algebra/CModules/RModule_rec.con +cic:/CoRN/algebra/CModules/RModule_is_RModule.con +cic:/CoRN/algebra/CModules/RModule_ind.con +cic:/CoRN/algebra/CModules/RModule.ind +cic:/matita/dama/bishop_set/le_le_eq.con +cic:/matita/dama/bishop_set/le_antisymmetric.con +cic:/matita/dama/bishop_set/eq_trans_.con +cic:/matita/dama/bishop_set/eq_sym_.con +cic:/matita/dama/bishop_set/eq_sym.con +cic:/matita/dama/bishop_set/eq_reflexive.con +cic:/matita/dama/bishop_set/eq.con +cic:/matita/dama/bishop_set/bs_symmetric.con +cic:/matita/dama/bishop_set/bs_cotransitive.con +cic:/matita/dama/bishop_set/bs_coreflexive.con +cic:/matita/dama/bishop_set/bs_carr.con +cic:/matita/dama/bishop_set/bs_apart.con +cic:/matita/dama/bishop_set/bishop_set_rect.con +cic:/matita/dama/bishop_set/bishop_set_rec.con +cic:/matita/dama/bishop_set/bishop_set_of_ordered_set.con +cic:/matita/dama/bishop_set/bishop_set_ind.con +cic:/matita/dama/bishop_set/bishop_set.ind +cic:/matita/dama/bishop_set_rewrite/le_rewr.con +cic:/matita/dama/bishop_set_rewrite/le_rewl.con +cic:/matita/dama/bishop_set_rewrite/exc_rewr.con +cic:/matita/dama/bishop_set_rewrite/exc_rewl.con +cic:/matita/dama/bishop_set_rewrite/eq_trans.con +cic:/matita/dama/bishop_set_rewrite/ap_rewr.con +cic:/matita/dama/bishop_set_rewrite/ap_rewl.con +cic:/matita/dama/cprop_connectives/transitive.con +cic:/matita/dama/cprop_connectives/symmetric.con +cic:/matita/dama/cprop_connectives/reflexive.con +cic:/matita/dama/cprop_connectives/exT_rect.con +cic:/matita/dama/cprop_connectives/exT_rec.con +cic:/matita/dama/cprop_connectives/exT_ind.con +cic:/matita/dama/cprop_connectives/exT.ind +cic:/matita/dama/cprop_connectives/cotransitive.con +cic:/matita/dama/cprop_connectives/coreflexive.con +cic:/matita/dama/cprop_connectives/antisymmetric.con +cic:/matita/dama/cprop_connectives/Or_rect.con +cic:/matita/dama/cprop_connectives/Or_rec.con +cic:/matita/dama/cprop_connectives/Or_ind.con +cic:/matita/dama/cprop_connectives/Or.ind +cic:/matita/dama/cprop_connectives/Not.con +cic:/matita/dama/cprop_connectives/False_rect.con +cic:/matita/dama/cprop_connectives/False_rec.con +cic:/matita/dama/cprop_connectives/False_ind.con +cic:/matita/dama/cprop_connectives/False.ind +cic:/matita/dama/cprop_connectives/And_rect.con +cic:/matita/dama/cprop_connectives/And_rec.con +cic:/matita/dama/cprop_connectives/And_ind.con +cic:/matita/dama/cprop_connectives/And.ind +cic:/matita/dama/ordered_set/os_excess.con +cic:/matita/dama/ordered_set/os_cotransitive.con +cic:/matita/dama/ordered_set/os_coreflexive.con +cic:/matita/dama/ordered_set/os_carr.con +cic:/matita/dama/ordered_set/ordered_set_rect.con +cic:/matita/dama/ordered_set/ordered_set_rec.con +cic:/matita/dama/ordered_set/ordered_set_ind.con +cic:/matita/dama/ordered_set/ordered_set.ind +cic:/matita/dama/ordered_set/le_transitive.con +cic:/matita/dama/ordered_set/le_reflexive.con +cic:/matita/dama/ordered_set/le.con +cic:/matita/dama/ordered_set/exc_le_variance.con +cic:/matita/dama/sequence/sequence.con +cic:/matita/dama/sequence/fun_of_sequence.con +cic:/matita/dama/supremum/upper_bound.con +cic:/matita/dama/supremum/uniq_supremum.con +cic:/matita/dama/supremum/strong_sup.con +cic:/matita/dama/supremum/increasing.con cic:/matita/higher_order_defs/functions/symmetric2.con cic:/matita/higher_order_defs/functions/symmetric.con cic:/matita/higher_order_defs/functions/surjective.con @@ -380,7 +496,6 @@ cic:/matita/higher_order_defs/functions/distributive2.con cic:/matita/higher_order_defs/functions/distributive.con cic:/matita/higher_order_defs/functions/compose.con cic:/matita/higher_order_defs/functions/associative.con -cic:/matita/higher_order_defs/ordering/antisymmetric.con cic:/matita/higher_order_defs/relations/transitive.con cic:/matita/higher_order_defs/relations/tight_apart.con cic:/matita/higher_order_defs/relations/symmetric.con @@ -389,55 +504,6 @@ cic:/matita/higher_order_defs/relations/reflexive.con cic:/matita/higher_order_defs/relations/irreflexive.con cic:/matita/higher_order_defs/relations/cotransitive.con cic:/matita/higher_order_defs/relations/antisymmetric.con -cic:/matita/list/list/x3.con -cic:/matita/list/list/x2.con -cic:/matita/list/list/x1.con -cic:/matita/list/list/tmp.con -cic:/matita/list/list/tail_demod2.con -cic:/matita/list/list/tail_demod1.con -cic:/matita/list/list/tail.con -cic:/matita/list/list/permutation_inv.con -cic:/matita/list/list/permutation_ind.con -cic:/matita/list/list/permutation.ind -cic:/matita/list/list/permut1_inv.con -cic:/matita/list/list/permut1_ind.con -cic:/matita/list/list/nth.con -cic:/matita/list/list/nil_cons.con -cic:/matita/list/list/map_foldr2.con -cic:/matita/list/list/map_foldr1.con -cic:/matita/list/list/map_demod2.con -cic:/matita/list/list/map_demod1.con -cic:/matita/list/list/map.con -cic:/matita/list/list/list_rect.con -cic:/matita/list/list/list_rec.con -cic:/matita/list/list/list_ind2.con -cic:/matita/list/list/list_ind.con -cic:/matita/list/list/list.ind -cic:/matita/list/list/length.con -cic:/matita/list/list/len_demod2.con -cic:/matita/list/list/len_demod1.con -cic:/matita/list/list/le_length_filter.con -cic:/matita/list/list/iota_demod2.con -cic:/matita/list/list/iota_demod1.con -cic:/matita/list/list/iota.con -cic:/matita/list/list/id_list.con -cic:/matita/list/list/foldr.con -cic:/matita/list/list/filter_demod2.con -cic:/matita/list/list/filter_demod1.con -cic:/matita/list/list/filter.con -cic:/matita/list/list/eq_map.con -cic:/matita/list/list/cons_append_commute.con -cic:/matita/list/list/associative_append.con -cic:/matita/list/list/append_nil.con -cic:/matita/list/list/append_demod2.con -cic:/matita/list/list/append_demod1.con -cic:/matita/list/list/append_cons.con -cic:/matita/list/list/append.con -cic:/matita/logic/coimplication/iff_trans.con -cic:/matita/logic/coimplication/iff_sym.con -cic:/matita/logic/coimplication/iff_refl.con -cic:/matita/logic/coimplication/iff_intro.con -cic:/matita/logic/coimplication/Iff.con cic:/matita/logic/connectives/proj2.con cic:/matita/logic/connectives/proj1.con cic:/matita/logic/connectives/iff.con @@ -463,9 +529,6 @@ cic:/matita/logic/connectives/And_rect.con cic:/matita/logic/connectives/And_rec.con cic:/matita/logic/connectives/And_ind.con cic:/matita/logic/connectives/And.ind -cic:/matita/logic/connectives2/transitive_iff.con -cic:/matita/logic/connectives2/symmetric_iff.con -cic:/matita/logic/connectives2/reflexive_iff.con cic:/matita/logic/equality/transitive_eq.con cic:/matita/logic/equality/trans_sym_eq.con cic:/matita/logic/equality/trans_eq.con @@ -492,88 +555,19 @@ cic:/matita/logic/equality/eq_OF_eq1.con cic:/matita/logic/equality/eq_OF_eq.con cic:/matita/logic/equality/eq.ind cic:/matita/logic/equality/comp.con -cic:/matita/technicalities/setoids/variance_rect.con -cic:/matita/technicalities/setoids/variance_rec.con -cic:/matita/technicalities/setoids/variance_of_argument_class.con -cic:/matita/technicalities/setoids/variance_ind.con -cic:/matita/technicalities/setoids/variance.ind -cic:/matita/technicalities/setoids/rewrite_direction_rect.con -cic:/matita/technicalities/setoids/rewrite_direction_rec.con -cic:/matita/technicalities/setoids/rewrite_direction_ind.con -cic:/matita/technicalities/setoids/rewrite_direction.ind -cic:/matita/technicalities/setoids/relation_of_relation_class.con -cic:/matita/technicalities/setoids/relation_of_product_of_arguments.con -cic:/matita/technicalities/setoids/relation_of_areflexive_relation_class.con -cic:/matita/technicalities/setoids/relation_class_of_reflexive_relation_class.con -cic:/matita/technicalities/setoids/relation_class_of_argument_class.con -cic:/matita/technicalities/setoids/relation_class_of_areflexive_relation_class.con -cic:/matita/technicalities/setoids/product_of_arguments.con -cic:/matita/technicalities/setoids/opposite_direction_idempotent.con -cic:/matita/technicalities/setoids/opposite_direction.con -cic:/matita/technicalities/setoids/nelistT_rect.con -cic:/matita/technicalities/setoids/nelistT_rec.con -cic:/matita/technicalities/setoids/nelistT_ind.con -cic:/matita/technicalities/setoids/nelistT.ind -cic:/matita/technicalities/setoids/morphism_theory_of_predicate.con -cic:/matita/technicalities/setoids/morphism_theory_of_function.con -cic:/matita/technicalities/setoids/make_compatibility_goal_aux.con -cic:/matita/technicalities/setoids/make_compatibility_goal.con -cic:/matita/technicalities/setoids/list_of_Leibniz_of_list_of_types.con -cic:/matita/technicalities/setoids/interp_relation_class_list.con -cic:/matita/technicalities/setoids/interp.con -cic:/matita/technicalities/setoids/impl_trans.con -cic:/matita/technicalities/setoids/impl_refl.con -cic:/matita/technicalities/setoids/impl.con -cic:/matita/technicalities/setoids/get_rewrite_direction.con -cic:/matita/technicalities/setoids/function_type_of_morphism_signature.con -cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_reflexive_transitive_relation.con -cic:/matita/technicalities/setoids/equality_morphism_of_symmetric_areflexive_transitive_relation.con -cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_reflexive_transitive_relation.con -cic:/matita/technicalities/setoids/equality_morphism_of_asymmetric_areflexive_transitive_relation.con -cic:/matita/technicalities/setoids/directed_relation_of_relation_class.con -cic:/matita/technicalities/setoids/directed_relation_of_argument_class.con -cic:/matita/technicalities/setoids/check_if_variance_is_respected_inv.con -cic:/matita/technicalities/setoids/check_if_variance_is_respected_ind.con -cic:/matita/technicalities/setoids/check_if_variance_is_respected.ind -cic:/matita/technicalities/setoids/carrier_of_relation_class.con -cic:/matita/technicalities/setoids/carrier_of_reflexive_relation_class.con -cic:/matita/technicalities/setoids/carrier_of_areflexive_relation_class.con -cic:/matita/technicalities/setoids/apply_morphism_compatibility_Right2Left.con -cic:/matita/technicalities/setoids/apply_morphism_compatibility_Left2Right.con -cic:/matita/technicalities/setoids/apply_morphism.con -cic:/matita/technicalities/setoids/about_carrier_of_relation_class_and_relation_class_of_argument_class.con -cic:/matita/technicalities/setoids/X_Relation_Class_rect.con -cic:/matita/technicalities/setoids/X_Relation_Class_rec.con -cic:/matita/technicalities/setoids/X_Relation_Class_ind.con -cic:/matita/technicalities/setoids/X_Relation_Class.ind -cic:/matita/technicalities/setoids/Relation_Class.con -cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rect.con -cic:/matita/technicalities/setoids/Reflexive_Relation_Class_rec.con -cic:/matita/technicalities/setoids/Reflexive_Relation_Class_ind.con -cic:/matita/technicalities/setoids/Reflexive_Relation_Class.ind -cic:/matita/technicalities/setoids/Morphism_Theory_rect.con -cic:/matita/technicalities/setoids/Morphism_Theory_rec.con -cic:/matita/technicalities/setoids/Morphism_Theory_ind.con -cic:/matita/technicalities/setoids/Morphism_Theory.ind -cic:/matita/technicalities/setoids/Morphism_Context_rect2.con -cic:/matita/technicalities/setoids/Morphism_Context_rect.con -cic:/matita/technicalities/setoids/Morphism_Context_rec.con -cic:/matita/technicalities/setoids/Morphism_Context_inv.con -cic:/matita/technicalities/setoids/Morphism_Context_ind.con -cic:/matita/technicalities/setoids/Morphism_Context_List_rect2.con -cic:/matita/technicalities/setoids/Morphism_Context_List_rect.con -cic:/matita/technicalities/setoids/Morphism_Context_List_rec.con -cic:/matita/technicalities/setoids/Morphism_Context_List_inv.con -cic:/matita/technicalities/setoids/Morphism_Context_List_ind.con -cic:/matita/technicalities/setoids/Morphism_Context.ind -cic:/matita/technicalities/setoids/Impl_Relation_Class.con -cic:/matita/technicalities/setoids/Iff_Relation_Class.con -cic:/matita/technicalities/setoids/Function.con -cic:/matita/technicalities/setoids/Compat.con -cic:/matita/technicalities/setoids/Arguments.con -cic:/matita/technicalities/setoids/Argument_Class.con -cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rect.con -cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rec.con -cic:/matita/technicalities/setoids/Areflexive_Relation_Class_ind.con -cic:/matita/technicalities/setoids/Areflexive_Relation_Class.ind -cic:/matita/tests/XXX.ind +cic:/matita/nat/nat/pred_Sn.con +cic:/matita/nat/nat/pred.con +cic:/matita/nat/nat/not_zero.con +cic:/matita/nat/nat/not_eq_n_Sn.con +cic:/matita/nat/nat/not_eq_S.con +cic:/matita/nat/nat/not_eq_O_S.con +cic:/matita/nat/nat/nat_rect.con +cic:/matita/nat/nat/nat_rec.con +cic:/matita/nat/nat/nat_ind.con +cic:/matita/nat/nat/nat_elim2.con +cic:/matita/nat/nat/nat_case1.con +cic:/matita/nat/nat/nat_case.con +cic:/matita/nat/nat/nat.ind +cic:/matita/nat/nat/injective_S.con +cic:/matita/nat/nat/inj_S.con +cic:/matita/nat/nat/decidable_eq_nat.con