From a3b43762ca9cfb746933dcd991bfc363b5fdd9b7 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Mon, 9 Jun 2008 16:02:24 +0000 Subject: [PATCH] more proof irrelevance --- .../software/components/ng_kernel/alluris.txt | 2973 +++++++++++++---- helm/software/components/ng_kernel/check.ml | 12 +- .../components/ng_kernel/nCicReduction.ml | 2 +- .../components/ng_kernel/nCicReduction.mli | 2 +- .../components/ng_kernel/nCicTypeChecker.ml | 79 +- .../components/ng_kernel/oCic2NCic.ml | 6 +- helm/software/components/ng_kernel/test.ma | 34 +- 7 files changed, 2498 insertions(+), 610 deletions(-) diff --git a/helm/software/components/ng_kernel/alluris.txt b/helm/software/components/ng_kernel/alluris.txt index 0d49a6a74..bfd76a2af 100644 --- a/helm/software/components/ng_kernel/alluris.txt +++ b/helm/software/components/ng_kernel/alluris.txt @@ -1,573 +1,2400 @@ -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 -cic:/matita/higher_order_defs/functions/monotonic.con -cic:/matita/higher_order_defs/functions/injective.con -cic:/matita/higher_order_defs/functions/eq_f_g_h.con -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/relations/transitive.con -cic:/matita/higher_order_defs/relations/tight_apart.con -cic:/matita/higher_order_defs/relations/symmetric.con -cic:/matita/higher_order_defs/relations/relation.con -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/logic/connectives/proj2.con -cic:/matita/logic/connectives/proj1.con -cic:/matita/logic/connectives/iff.con -cic:/matita/logic/connectives/ex_ind.con -cic:/matita/logic/connectives/ex2_ind.con -cic:/matita/logic/connectives/ex2.ind -cic:/matita/logic/connectives/ex.ind -cic:/matita/logic/connectives/decidable.con -cic:/matita/logic/connectives/absurd.con -cic:/matita/logic/connectives/True_rect.con -cic:/matita/logic/connectives/True_rec.con -cic:/matita/logic/connectives/True_ind.con -cic:/matita/logic/connectives/True.ind -cic:/matita/logic/connectives/Or_ind.con -cic:/matita/logic/connectives/Or_ind'.con -cic:/matita/logic/connectives/Or.ind -cic:/matita/logic/connectives/Not.con -cic:/matita/logic/connectives/False_rect.con -cic:/matita/logic/connectives/False_rec.con -cic:/matita/logic/connectives/False_ind.con -cic:/matita/logic/connectives/False.ind -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/equality/transitive_eq.con -cic:/matita/logic/equality/trans_sym_eq.con -cic:/matita/logic/equality/trans_eq.con -cic:/matita/logic/equality/symmetric_eq.con -cic:/matita/logic/equality/sym_eq.con -cic:/matita/logic/equality/reflexive_eq.con -cic:/matita/logic/equality/nu_left_inv.con -cic:/matita/logic/equality/nu_inv.con -cic:/matita/logic/equality/nu_constant.con -cic:/matita/logic/equality/nu.con -cic:/matita/logic/equality/eq_to_eq_to_eq_p_q.con -cic:/matita/logic/equality/eq_rect.con -cic:/matita/logic/equality/eq_rect'.con -cic:/matita/logic/equality/eq_rec.con -cic:/matita/logic/equality/eq_ind.con -cic:/matita/logic/equality/eq_f2.con -cic:/matita/logic/equality/eq_f.con -cic:/matita/logic/equality/eq_f'.con -cic:/matita/logic/equality/eq_elim_r.con -cic:/matita/logic/equality/eq_elim_r'.con -cic:/matita/logic/equality/eq_elim_r''.con -cic:/matita/logic/equality/eq_OF_eq2.con -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/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:/BellLabs/lazyPCF/OpSem/environments/cfgenv.con +cic:/BellLabs/lazyPCF/OpSem/environments/cfgexp.con +cic:/BellLabs/lazyPCF/OpSem/environments/config.ind +cic:/BellLabs/lazyPCF/OpSem/environments/config_ind.con +cic:/BellLabs/lazyPCF/OpSem/environments/config_rec.con +cic:/BellLabs/lazyPCF/OpSem/environments/config_rect.con +cic:/BellLabs/lazyPCF/OpSem/environments/mapsto.con +cic:/BellLabs/lazyPCF/OpSem/environments/member.con +cic:/BellLabs/lazyPCF/OpSem/environments/OS_Dom.con +cic:/BellLabs/lazyPCF/OpSem/environments/OS_Dom_ty.con +cic:/BellLabs/lazyPCF/OpSem/environments/OS_env.con +cic:/BellLabs/lazyPCF/OpSem/environments/TE_Dom.con +cic:/BellLabs/lazyPCF/OpSem/environments/ty_env.con +cic:/BellLabs/lazyPCF/OpSem/environments/VT.con +cic:/BellLabs/lazyPCF/OpSem/environments/VTT.con +cic:/BellLabs/lazyPCF/OpSem/freevars/fv.con +cic:/BellLabs/lazyPCF/OpSem/freevars/FV_fv.con +cic:/BellLabs/lazyPCF/OpSem/freevars/FV.ind +cic:/BellLabs/lazyPCF/OpSem/freevars/FV_ind.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_abs.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_appl.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_clos.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_cond.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_fff.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_fix.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_is_o.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_o.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_prd.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_succ.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_ttt.con +cic:/BellLabs/lazyPCF/OpSem/freevars/inv_FV_var.con +cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_abs.con +cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_appl.con +cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_clos.con +cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_cond.con +cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_fix.con +cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_is_o.con +cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_prd.con +cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_succ.con +cic:/BellLabs/lazyPCF/OpSem/freevars/notFV_var.con +cic:/BellLabs/lazyPCF/OpSem/OSrules/Ap.ind +cic:/BellLabs/lazyPCF/OpSem/OSrules/Ap_ind.con +cic:/BellLabs/lazyPCF/OpSem/OSrules/ApNewVar.con +cic:/BellLabs/lazyPCF/OpSem/OSrules/OScons.con +cic:/BellLabs/lazyPCF/OpSem/OSrules/OSred.ind +cic:/BellLabs/lazyPCF/OpSem/OSrules/OSred_ind.con +cic:/BellLabs/lazyPCF/OpSem/rename/rename.ind +cic:/BellLabs/lazyPCF/OpSem/rename/rename_ind.con +cic:/BellLabs/lazyPCF/OpSem/rename/RenNotFree.con +cic:/BellLabs/lazyPCF/OpSem/syntax/tm.ind +cic:/BellLabs/lazyPCF/OpSem/syntax/tm_ind.con +cic:/BellLabs/lazyPCF/OpSem/syntax/tm_rec.con +cic:/BellLabs/lazyPCF/OpSem/syntax/tm_rect.con +cic:/BellLabs/lazyPCF/OpSem/syntax/ty.ind +cic:/BellLabs/lazyPCF/OpSem/syntax/ty_ind.con +cic:/BellLabs/lazyPCF/OpSem/syntax/ty_rec.con +cic:/BellLabs/lazyPCF/OpSem/syntax/ty_rect.con +cic:/BellLabs/lazyPCF/OpSem/syntax/vari.ind +cic:/BellLabs/lazyPCF/OpSem/syntax/vari_ind.con +cic:/BellLabs/lazyPCF/OpSem/syntax/vari_rec.con +cic:/BellLabs/lazyPCF/OpSem/syntax/vari_rect.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_abs.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_appl.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_clos.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_cond.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_fff.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_fix.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_is_o.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_o.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_prd.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_succ.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_ttt.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/inv_TC_var.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/tc.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/TC.ind +cic:/BellLabs/lazyPCF/OpSem/typecheck/TC_ind.con +cic:/BellLabs/lazyPCF/OpSem/typecheck/TC_tc.con +cic:/BellLabs/lazyPCF/OpSem/utils/AABC_ABC.con +cic:/BellLabs/lazyPCF/OpSem/utils/bool_not_arr.con +cic:/BellLabs/lazyPCF/OpSem/utils/F_If.con +cic:/BellLabs/lazyPCF/OpSem/utils/IfA_IfAIfA.con +cic:/BellLabs/lazyPCF/OpSem/utils/If_F.con +cic:/BellLabs/lazyPCF/OpSem/utils/If_T.con +cic:/BellLabs/lazyPCF/OpSem/utils/is_arr.con +cic:/BellLabs/lazyPCF/OpSem/utils/is_bool.con +cic:/BellLabs/lazyPCF/OpSem/utils/is_nat.con +cic:/BellLabs/lazyPCF/OpSem/utils/nat_not_arr.con +cic:/BellLabs/lazyPCF/OpSem/utils/nat_not_bool.con +cic:/BellLabs/lazyPCF/OpSem/utils/Rand_ty.con +cic:/BellLabs/lazyPCF/OpSem/utils/Rator_ty.con +cic:/BellLabs/lazyPCF/OpSem/utils/subty_eq.con +cic:/BellLabs/lazyPCF/OpSem/utils/T_If.con +cic:/BellLabs/lazyPCF/OpSem/utils/valu.con +cic:/BellLabs/lazyPCF/OpSem/utils/vari_nat.con +cic:/BellLabs/lazyPCF/OpSem/utils/Xmidnat.con +cic:/BellLabs/lazyPCF/OpSem/utils/Xmidvar.con +cic:/BellLabs/lazyPCF/SubjRed/ApTypes/ren_case1.con +cic:/BellLabs/lazyPCF/SubjRed/ApTypes/ren_case2.con +cic:/BellLabs/lazyPCF/SubjRed/ApTypes/ren_var1.con +cic:/BellLabs/lazyPCF/SubjRed/ApTypes/ren_var2.con +cic:/BellLabs/lazyPCF/SubjRed/ApTypes/TEp_Ap.con +cic:/BellLabs/lazyPCF/SubjRed/ApTypes/TEp_RenExp.con +cic:/BellLabs/lazyPCF/SubjRed/ApTypes/TEp_RenExpGen.con +cic:/BellLabs/lazyPCF/SubjRed/envprops/dom_pres.con +cic:/BellLabs/lazyPCF/SubjRed/envprops/TCHet_FVeinDomH.con +cic:/BellLabs/lazyPCF/SubjRed/envprops/TEDomDomty_OSDom.con +cic:/BellLabs/lazyPCF/SubjRed/envprops/vtinH_vinDomH.con +cic:/BellLabs/lazyPCF/SubjRed/mapsto/Mp_eqExt.con +cic:/BellLabs/lazyPCF/SubjRed/mapsto/Mp_inv_eqExt.con +cic:/BellLabs/lazyPCF/SubjRed/mapsto/Mp_inv_nfvExt.con +cic:/BellLabs/lazyPCF/SubjRed/mapsto/Mp_nfvExt.con +cic:/BellLabs/lazyPCF/SubjRed/mapsto/Mp_swap.con +cic:/BellLabs/lazyPCF/SubjRed/NF/F.ind +cic:/BellLabs/lazyPCF/SubjRed/NF/F_ind.con +cic:/BellLabs/lazyPCF/SubjRed/NF/inv_NF_Sno.con +cic:/BellLabs/lazyPCF/SubjRed/NF/inv_Sno_s.con +cic:/BellLabs/lazyPCF/SubjRed/NF/NF.ind +cic:/BellLabs/lazyPCF/SubjRed/NF/NF_ind.con +cic:/BellLabs/lazyPCF/SubjRed/NF/NFsucc.con +cic:/BellLabs/lazyPCF/SubjRed/NFprops/Fe_not_bool.con +cic:/BellLabs/lazyPCF/SubjRed/NFprops/Fe_not_nat.con +cic:/BellLabs/lazyPCF/SubjRed/NFprops/NFebool_TF.con +cic:/BellLabs/lazyPCF/SubjRed/NFprops/NFe_Fe.con +cic:/BellLabs/lazyPCF/SubjRed/NFprops/NFenat_Snoe.con +cic:/BellLabs/lazyPCF/SubjRed/NFprops/Snoe_notFVe.con +cic:/BellLabs/lazyPCF/SubjRed/NF/Sno.ind +cic:/BellLabs/lazyPCF/SubjRed/NF/Sno_ind.con +cic:/BellLabs/lazyPCF/SubjRed/NF/SnoSucc.con +cic:/BellLabs/lazyPCF/SubjRed/subjrnf/NormalForms.con +cic:/BellLabs/lazyPCF/SubjRed/subjrnf/subjr_NF.con +cic:/BellLabs/lazyPCF/SubjRed/subjrnf/subjr_red.con +cic:/BellLabs/lazyPCF/SubjRed/TypeThms/TEp_eqExt.con +cic:/BellLabs/lazyPCF/SubjRed/TypeThms/TEp_inv_eqExt.con +cic:/BellLabs/lazyPCF/SubjRed/TypeThms/TEp_inv_nfvExt.con +cic:/BellLabs/lazyPCF/SubjRed/TypeThms/TEp_nfvExt.con +cic:/BellLabs/lazyPCF/SubjRed/TypeThms/TEp_swap.con +cic:/BellLabs/lazyPCF/SubjRed/valid/inv_valid_cons.con +cic:/BellLabs/lazyPCF/SubjRed/valid/valid_c.con +cic:/BellLabs/lazyPCF/SubjRed/valid/valid_config.ind +cic:/BellLabs/lazyPCF/SubjRed/valid/valid_config_ind.con +cic:/BellLabs/lazyPCF/SubjRed/valid/valid_env.ind +cic:/BellLabs/lazyPCF/SubjRed/valid/valid_env_ind.con +cic:/Cachan/SMC/alloc/BDDalloc_BDD_OK.con +cic:/Cachan/SMC/alloc/BDDalloc.con +cic:/Cachan/SMC/alloc/BDDallocGet.con +cic:/Cachan/SMC/alloc/BDDalloc_keeps_cnt_OK.con +cic:/Cachan/SMC/alloc/BDDalloc_keeps_config_OK.con +cic:/Cachan/SMC/alloc/BDDalloc_keeps_free_list_OK.con +cic:/Cachan/SMC/alloc/BDDalloc_keeps_neg_memo_OK.con +cic:/Cachan/SMC/alloc/BDDalloc_keeps_or_memo_OK.con +cic:/Cachan/SMC/alloc/BDDalloc_keeps_sharing_OK.con +cic:/Cachan/SMC/alloc/BDDalloc_keeps_state_OK.con +cic:/Cachan/SMC/alloc/BDDalloc_keeps_univ_memo_OK.con +cic:/Cachan/SMC/alloc/BDDalloc_lemma_1.con +cic:/Cachan/SMC/alloc/BDDalloc_lemma_2.con +cic:/Cachan/SMC/alloc/BDDalloc_lemma_3.con +cic:/Cachan/SMC/alloc/BDDalloc_lemma_4.con +cic:/Cachan/SMC/alloc/BDDalloc_lemma_5.con +cic:/Cachan/SMC/alloc/BDDalloc_negm_same.con +cic:/Cachan/SMC/alloc/BDDalloc_node_OK.con +cic:/Cachan/SMC/alloc/BDDalloc_one.con +cic:/Cachan/SMC/alloc/BDDalloc_orm_same.con +cic:/Cachan/SMC/alloc/BDDalloc_preserves_nodes.con +cic:/Cachan/SMC/alloc/BDDalloc_preserves_used_nodes.con +cic:/Cachan/SMC/alloc/BDDalloc_um_same.con +cic:/Cachan/SMC/alloc/BDDalloc_zero.con +cic:/Cachan/SMC/alloc/BDD_OK_l.con +cic:/Cachan/SMC/alloc/BDD_OK_r.con +cic:/Cachan/SMC/alloc/BDDsharing_OK_1.con +cic:/Cachan/SMC/alloc/new_cfg_nodes_preserved.con +cic:/Cachan/SMC/alloc/new_cfg_OK.con +cic:/Cachan/SMC/alloc/new_l_OK.con +cic:/Cachan/SMC/alloc/new_r_OK.con +cic:/Cachan/SMC/alloc/new_xl_lt_x.con +cic:/Cachan/SMC/alloc/new_xr_lt_x.con +cic:/Cachan/SMC/alloc/no_dup_new.con +cic:/Cachan/SMC/bool_fun/augment.con +cic:/Cachan/SMC/bool_fun/bool_expr.ind +cic:/Cachan/SMC/bool_fun/bool_expr_ind.con +cic:/Cachan/SMC/bool_fun/bool_expr_rec.con +cic:/Cachan/SMC/bool_fun/bool_expr_rect.con +cic:/Cachan/SMC/bool_fun/bool_fun_and_comm.con +cic:/Cachan/SMC/bool_fun/bool_fun_and.con +cic:/Cachan/SMC/bool_fun/bool_fun_and_idempotent.con +cic:/Cachan/SMC/bool_fun/bool_fun_and_lemma.con +cic:/Cachan/SMC/bool_fun/bool_fun_and_orthogonal.con +cic:/Cachan/SMC/bool_fun/bool_fun_and_preserves_eq.con +cic:/Cachan/SMC/bool_fun/bool_fun.con +cic:/Cachan/SMC/bool_fun/bool_fun_eq.con +cic:/Cachan/SMC/bool_fun/bool_fun_eq_independent.con +cic:/Cachan/SMC/bool_fun/bool_fun_eq_neg_eq.con +cic:/Cachan/SMC/bool_fun/bool_fun_eq_refl.con +cic:/Cachan/SMC/bool_fun/bool_fun_eq_sym.con +cic:/Cachan/SMC/bool_fun/bool_fun_eq_trans.con +cic:/Cachan/SMC/bool_fun/bool_fun_ex.con +cic:/Cachan/SMC/bool_fun/bool_fun_ex_lemma.con +cic:/Cachan/SMC/bool_fun/bool_fun_ex_preserves_eq.con +cic:/Cachan/SMC/bool_fun/bool_fun_ext.con +cic:/Cachan/SMC/bool_fun/bool_fun_ext_if.con +cic:/Cachan/SMC/bool_fun/bool_fun_ext_one.con +cic:/Cachan/SMC/bool_fun/bool_fun_ext_zero.con +cic:/Cachan/SMC/bool_fun/bool_fun_forall.con +cic:/Cachan/SMC/bool_fun/bool_fun_forall_if_egal.con +cic:/Cachan/SMC/bool_fun/bool_fun_forall_independent.con +cic:/Cachan/SMC/bool_fun/bool_fun_forall_one.con +cic:/Cachan/SMC/bool_fun/bool_fun_forall_orthogonal.con +cic:/Cachan/SMC/bool_fun/bool_fun_forall_preserves_eq.con +cic:/Cachan/SMC/bool_fun/bool_fun_forall_zero.con +cic:/Cachan/SMC/bool_fun/bool_fun_if.con +cic:/Cachan/SMC/bool_fun/bool_fun_if_eq_1.con +cic:/Cachan/SMC/bool_fun/bool_fun_if_eq_2.con +cic:/Cachan/SMC/bool_fun/bool_fun_iff.con +cic:/Cachan/SMC/bool_fun/bool_fun_iff_lemma.con +cic:/Cachan/SMC/bool_fun/bool_fun_iff_preserves_eq.con +cic:/Cachan/SMC/bool_fun/bool_fun_if_preserves_eq.con +cic:/Cachan/SMC/bool_fun/bool_fun_if_restrict.con +cic:/Cachan/SMC/bool_fun/bool_fun_if_restrict_false.con +cic:/Cachan/SMC/bool_fun/bool_fun_if_restrict_false_independent.con +cic:/Cachan/SMC/bool_fun/bool_fun_if_restrict_true.con +cic:/Cachan/SMC/bool_fun/bool_fun_if_restrict_true_independent.con +cic:/Cachan/SMC/bool_fun/bool_fun_impl.con +cic:/Cachan/SMC/bool_fun/bool_fun_impl_lemma.con +cic:/Cachan/SMC/bool_fun/bool_fun_impl_preserves_eq.con +cic:/Cachan/SMC/bool_fun/bool_fun_independent.con +cic:/Cachan/SMC/bool_fun/bool_fun_independent_if.con +cic:/Cachan/SMC/bool_fun/bool_fun_independent_one.con +cic:/Cachan/SMC/bool_fun/bool_fun_independent_zero.con +cic:/Cachan/SMC/bool_fun/bool_fun_neg.con +cic:/Cachan/SMC/bool_fun/bool_fun_neg_one.con +cic:/Cachan/SMC/bool_fun/bool_fun_neg_orthogonal.con +cic:/Cachan/SMC/bool_fun/bool_fun_neg_preserves_eq.con +cic:/Cachan/SMC/bool_fun/bool_fun_neg_zero.con +cic:/Cachan/SMC/bool_fun/bool_fun_of_bool_expr.con +cic:/Cachan/SMC/bool_fun/bool_fun_one.con +cic:/Cachan/SMC/bool_fun/bool_fun_or_comm.con +cic:/Cachan/SMC/bool_fun/bool_fun_or.con +cic:/Cachan/SMC/bool_fun/bool_fun_or_one.con +cic:/Cachan/SMC/bool_fun/bool_fun_or_orthogonal.con +cic:/Cachan/SMC/bool_fun/bool_fun_or_orthogonal_left.con +cic:/Cachan/SMC/bool_fun/bool_fun_or_orthogonal_right.con +cic:/Cachan/SMC/bool_fun/bool_fun_or_preserves_eq.con +cic:/Cachan/SMC/bool_fun/bool_fun_or_zero.con +cic:/Cachan/SMC/bool_fun/bool_fun_restrict.con +cic:/Cachan/SMC/bool_fun/bool_fun_restrict_one.con +cic:/Cachan/SMC/bool_fun/bool_fun_restrict_preserves_eq.con +cic:/Cachan/SMC/bool_fun/bool_fun_restrict_zero.con +cic:/Cachan/SMC/bool_fun/bool_fun_var.con +cic:/Cachan/SMC/bool_fun/bool_fun_var_lemma.con +cic:/Cachan/SMC/bool_fun/bool_fun_zero.con +cic:/Cachan/SMC/bool_fun/var_env.con +cic:/Cachan/SMC/config/BDDbounded.ind +cic:/Cachan/SMC/config/BDDbounded_ind.con +cic:/Cachan/SMC/config/BDDbounded_lemma.con +cic:/Cachan/SMC/config/BDDbounded_node_OK.con +cic:/Cachan/SMC/config/BDDconfig.con +cic:/Cachan/SMC/config/BDDconfig_OK.con +cic:/Cachan/SMC/config/BDDfree_list.con +cic:/Cachan/SMC/config/BDDfree_list_OK.con +cic:/Cachan/SMC/config/BDDneg_memo.con +cic:/Cachan/SMC/config/BDDneg_memo_OK.con +cic:/Cachan/SMC/config/BDDneg_memo_put.con +cic:/Cachan/SMC/config/BDDnegm_put_nodes_preserved.con +cic:/Cachan/SMC/config/BDDnegm_put_OK.con +cic:/Cachan/SMC/config/BDD_OK.con +cic:/Cachan/SMC/config/BDD_OK_node_OK.con +cic:/Cachan/SMC/config/BDDone.con +cic:/Cachan/SMC/config/BDDone_preserved.con +cic:/Cachan/SMC/config/BDDor_memo.con +cic:/Cachan/SMC/config/BDDor_memo_OK.con +cic:/Cachan/SMC/config/BDDor_memo_put.con +cic:/Cachan/SMC/config/BDDorm_put_nodes_preserved.con +cic:/Cachan/SMC/config/BDDorm_put_OK.con +cic:/Cachan/SMC/config/BDDsharing_map.con +cic:/Cachan/SMC/config/BDDsharing_OK.con +cic:/Cachan/SMC/config/BDDstate.con +cic:/Cachan/SMC/config/BDDstate_OK.con +cic:/Cachan/SMC/config/BDDum_put_nodes_preserved.con +cic:/Cachan/SMC/config/BDDum_put_OK.con +cic:/Cachan/SMC/config/BDDunique_1.con +cic:/Cachan/SMC/config/BDDunique.con +cic:/Cachan/SMC/config/BDDuniv_memo.con +cic:/Cachan/SMC/config/BDDuniv_memo_OK.con +cic:/Cachan/SMC/config/BDDuniv_memo_put.con +cic:/Cachan/SMC/config/BDDvar_independent_1.con +cic:/Cachan/SMC/config/BDDvar_independent_bs.con +cic:/Cachan/SMC/config/BDDvar_independent_high.con +cic:/Cachan/SMC/config/BDDvar_independent_low.con +cic:/Cachan/SMC/config/BDDzero.con +cic:/Cachan/SMC/config/BDDzero_preserved.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_1_change_bound.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_1.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_1_ext.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_bs.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_ext.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_high.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_int.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_low.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_one.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_bs_zero.con +cic:/Cachan/SMC/config/bool_fun_of_BDD.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_int.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_one.con +cic:/Cachan/SMC/config/bool_fun_of_BDD_zero.con +cic:/Cachan/SMC/config/bs_node_height.con +cic:/Cachan/SMC/config/bs_node_height_left.con +cic:/Cachan/SMC/config/bs_node_height_left_le.con +cic:/Cachan/SMC/config/bs_node_height_right.con +cic:/Cachan/SMC/config/bs_node_height_right_le.con +cic:/Cachan/SMC/config/bs_of_cfg.con +cic:/Cachan/SMC/config/bs_of_cfg_OK.con +cic:/Cachan/SMC/config/cfg_comp.con +cic:/Cachan/SMC/config/cnt_of_cfg.con +cic:/Cachan/SMC/config/cnt_of_cfg_OK.con +cic:/Cachan/SMC/config/cnt_OK.con +cic:/Cachan/SMC/config/config_node_OK.con +cic:/Cachan/SMC/config/config_OK_one.con +cic:/Cachan/SMC/config/config_OK_zero.con +cic:/Cachan/SMC/config/cons_OK_list_OK.con +cic:/Cachan/SMC/config/fl_of_cfg.con +cic:/Cachan/SMC/config/fl_of_cfg_OK.con +cic:/Cachan/SMC/config/gc_OK.con +cic:/Cachan/SMC/config/high_bounded.con +cic:/Cachan/SMC/config/high_OK.con +cic:/Cachan/SMC/config/high_used_bs.con +cic:/Cachan/SMC/config/high_used'_bs.con +cic:/Cachan/SMC/config/high_used.con +cic:/Cachan/SMC/config/high_used'.con +cic:/Cachan/SMC/config/increase_bound.con +cic:/Cachan/SMC/config/initBDDconfig.con +cic:/Cachan/SMC/config/initBDDconfig_OK.con +cic:/Cachan/SMC/config/initBDDfree_list.con +cic:/Cachan/SMC/config/initBDDfree_list_OK.con +cic:/Cachan/SMC/config/initBDDneg_memo.con +cic:/Cachan/SMC/config/initBDDneg_memo_OK.con +cic:/Cachan/SMC/config/initBDDor_memo.con +cic:/Cachan/SMC/config/initBDDor_memo_OK.con +cic:/Cachan/SMC/config/initBDDsharing_map.con +cic:/Cachan/SMC/config/initBDDsharing_map_OK.con +cic:/Cachan/SMC/config/initBDDstate.con +cic:/Cachan/SMC/config/initBDDstate_OK.con +cic:/Cachan/SMC/config/initBDDuniv_memo.con +cic:/Cachan/SMC/config/initBDDuniv_memo_OK.con +cic:/Cachan/SMC/config/internal_node_lemma.con +cic:/Cachan/SMC/config/int_node_gt_1.con +cic:/Cachan/SMC/config/int_node_lt_cnt.con +cic:/Cachan/SMC/config/low_bounded.con +cic:/Cachan/SMC/config/low_high_neq.con +cic:/Cachan/SMC/config/low_OK.con +cic:/Cachan/SMC/config/low_used_bs.con +cic:/Cachan/SMC/config/low_used'_bs.con +cic:/Cachan/SMC/config/low_used.con +cic:/Cachan/SMC/config/low_used'.con +cic:/Cachan/SMC/config/negm_of_cfg.con +cic:/Cachan/SMC/config/negm_of_cfg_OK.con +cic:/Cachan/SMC/config/node_height.con +cic:/Cachan/SMC/config/node_height_one.con +cic:/Cachan/SMC/config/node_height_zero.con +cic:/Cachan/SMC/config/node_OK_BDD_OK.con +cic:/Cachan/SMC/config/node_OK.con +cic:/Cachan/SMC/config/node_OK_list_OK_bs.con +cic:/Cachan/SMC/config/node_OK_list_OK.con +cic:/Cachan/SMC/config/node_preserved_bs_bool_fun_1.con +cic:/Cachan/SMC/config/node_preserved_bs_bool_fun.con +cic:/Cachan/SMC/config/node_preserved_bs.con +cic:/Cachan/SMC/config/node_preserved_bs_node_height_eq.con +cic:/Cachan/SMC/config/node_preserved_bs_reachable_1.con +cic:/Cachan/SMC/config/node_preserved_bs_reachable.con +cic:/Cachan/SMC/config/node_preserved_bs_trans.con +cic:/Cachan/SMC/config/node_preserved.con +cic:/Cachan/SMC/config/node_preserved_node_height_eq.con +cic:/Cachan/SMC/config/node_preserved_OK_bs.con +cic:/Cachan/SMC/config/nodes_preserved_bool_fun.con +cic:/Cachan/SMC/config/nodes_preserved_bounded.con +cic:/Cachan/SMC/config/nodes_preserved_bs_bool_fun_1.con +cic:/Cachan/SMC/config/nodes_preserved_bs_bool_fun.con +cic:/Cachan/SMC/config/nodes_preserved_bs.con +cic:/Cachan/SMC/config/nodes_preserved_bs_node_height_eq.con +cic:/Cachan/SMC/config/nodes_preserved_bs_node_OK.con +cic:/Cachan/SMC/config/nodes_preserved_bs_refl.con +cic:/Cachan/SMC/config/nodes_preserved_bs_trans.con +cic:/Cachan/SMC/config/nodes_preserved.con +cic:/Cachan/SMC/config/nodes_preserved_config_node_OK.con +cic:/Cachan/SMC/config/nodes_preserved_neg_memo_OK.con +cic:/Cachan/SMC/config/nodes_preserved_node_height_eq.con +cic:/Cachan/SMC/config/nodes_preserved_or_memo_OK.con +cic:/Cachan/SMC/config/nodes_preserved_refl.con +cic:/Cachan/SMC/config/nodes_preserved_trans.con +cic:/Cachan/SMC/config/nodes_preserved_um_OK.con +cic:/Cachan/SMC/config/nodes_preserved_used_nodes_preserved.con +cic:/Cachan/SMC/config/nodes_reachableBDDone.con +cic:/Cachan/SMC/config/nodes_reachableBDDzero.con +cic:/Cachan/SMC/config/nodes_reachable.ind +cic:/Cachan/SMC/config/nodes_reachable_ind.con +cic:/Cachan/SMC/config/nodes_reachable_lemma_1.con +cic:/Cachan/SMC/config/nodes_reachable_trans.con +cic:/Cachan/SMC/config/no_duplicate_node.con +cic:/Cachan/SMC/config/no_new_node_bs.con +cic:/Cachan/SMC/config/no_new_node.con +cic:/Cachan/SMC/config/not_zero_is_one.con +cic:/Cachan/SMC/config/one_OK.con +cic:/Cachan/SMC/config/orm_of_cfg.con +cic:/Cachan/SMC/config/orm_of_cfg_OK.con +cic:/Cachan/SMC/config/reachable_node_OK_1.con +cic:/Cachan/SMC/config/reachable_node_OK.con +cic:/Cachan/SMC/config/share_of_cfg.con +cic:/Cachan/SMC/config/share_of_cfg_OK.con +cic:/Cachan/SMC/config/um_of_cfg.con +cic:/Cachan/SMC/config/um_of_cfg_OK.con +cic:/Cachan/SMC/config/used_list_OK_bs.con +cic:/Cachan/SMC/config/used_list_OK.con +cic:/Cachan/SMC/config/used_node_bs.con +cic:/Cachan/SMC/config/used_node'_bs.con +cic:/Cachan/SMC/config/used_node.con +cic:/Cachan/SMC/config/used_node'.con +cic:/Cachan/SMC/config/used_node_cons_node_ul.con +cic:/Cachan/SMC/config/used_node_cons_node'_ul.con +cic:/Cachan/SMC/config/used_node'_cons_node_ul.con +cic:/Cachan/SMC/config/used_node'_cons_node'_ul.con +cic:/Cachan/SMC/config/used_node_OK_bs.con +cic:/Cachan/SMC/config/used_node'_OK_bs.con +cic:/Cachan/SMC/config/used_node_OK.con +cic:/Cachan/SMC/config/used_node'_OK.con +cic:/Cachan/SMC/config/used_nodes_preserved_bool_fun.con +cic:/Cachan/SMC/config/used_nodes_preserved'_bool_fun.con +cic:/Cachan/SMC/config/used_nodes_preserved_bs_bool_fun.con +cic:/Cachan/SMC/config/used_nodes_preserved'_bs_bool_fun.con +cic:/Cachan/SMC/config/used_nodes_preserved_bs.con +cic:/Cachan/SMC/config/used_nodes_preserved_bs_cons.con +cic:/Cachan/SMC/config/used_nodes_preserved.con +cic:/Cachan/SMC/config/used_nodes_preserved_cons.con +cic:/Cachan/SMC/config/used_nodes_preserved_list_OK_bs.con +cic:/Cachan/SMC/config/used_nodes_preserved_list_OK.con +cic:/Cachan/SMC/config/used_nodes_preserved_node_height_eq.con +cic:/Cachan/SMC/config/used_nodes_preserved'_node_height_eq.con +cic:/Cachan/SMC/config/used_nodes_preserved_node_OK.con +cic:/Cachan/SMC/config/used_nodes_preserved_node_OK'.con +cic:/Cachan/SMC/config/used_nodes_preserved_preserved_bs.con +cic:/Cachan/SMC/config/used_nodes_preserved_preserved'_bs.con +cic:/Cachan/SMC/config/used_nodes_preserved_refl.con +cic:/Cachan/SMC/config/used_nodes_preserved_trans.con +cic:/Cachan/SMC/config/used_nodes_preserved_used_node.con +cic:/Cachan/SMC/config/used_nodes_preserved_used_node'.con +cic:/Cachan/SMC/config/used_node'_used_node_bs.con +cic:/Cachan/SMC/config/used'_one.con +cic:/Cachan/SMC/config/used'_zero.con +cic:/Cachan/SMC/config/zero_OK.con +cic:/Cachan/SMC/gc/add_used_nodes_1.con +cic:/Cachan/SMC/gc/add_used_nodes_1_lemma_1.con +cic:/Cachan/SMC/gc/add_used_nodes_1_lemma_2.con +cic:/Cachan/SMC/gc/add_used_nodes.con +cic:/Cachan/SMC/gc/add_used_nodes_lemma_1.con +cic:/Cachan/SMC/gc/add_used_nodes_lemma_2.con +cic:/Cachan/SMC/gc/clean'1_1.con +cic:/Cachan/SMC/gc/clean'1_1_lemma.con +cic:/Cachan/SMC/gc/clean'1.con +cic:/Cachan/SMC/gc/clean1.con +cic:/Cachan/SMC/gc/clean'1_lemma.con +cic:/Cachan/SMC/gc/clean1_lemma.con +cic:/Cachan/SMC/gc/clean'2_1.con +cic:/Cachan/SMC/gc/clean2_1.con +cic:/Cachan/SMC/gc/clean'2_1_lemma.con +cic:/Cachan/SMC/gc/clean2_1_lemma.con +cic:/Cachan/SMC/gc/clean'2.con +cic:/Cachan/SMC/gc/clean2.con +cic:/Cachan/SMC/gc/clean'2_lemma.con +cic:/Cachan/SMC/gc/clean2_lemma.con +cic:/Cachan/SMC/gc/clean3_1.con +cic:/Cachan/SMC/gc/clean3_1_lemma.con +cic:/Cachan/SMC/gc/clean3.con +cic:/Cachan/SMC/gc/clean3_lemma.con +cic:/Cachan/SMC/gc/dummy_mark.ind +cic:/Cachan/SMC/gc/dummy_mark_ind.con +cic:/Cachan/SMC/gc/dummy_mark_rec.con +cic:/Cachan/SMC/gc/dummy_mark_rect.con +cic:/Cachan/SMC/gc/gc_0.con +cic:/Cachan/SMC/gc/gc_0_OK.con +cic:/Cachan/SMC/gc/gc_inf.con +cic:/Cachan/SMC/gc/gc_inf_OK.con +cic:/Cachan/SMC/gc/gc_x.con +cic:/Cachan/SMC/gc/gc_x_OK.con +cic:/Cachan/SMC/gc/gc_x_opt.con +cic:/Cachan/SMC/gc/gc_x_opt_OK.con +cic:/Cachan/SMC/gc/is_nil.con +cic:/Cachan/SMC/gc/mark.con +cic:/Cachan/SMC/gc/mark_lemma_1.con +cic:/Cachan/SMC/gc/mark_lemma_2.con +cic:/Cachan/SMC/gc/mark_lemma_3.con +cic:/Cachan/SMC/gc/new_bsBDDbounded_1.con +cic:/Cachan/SMC/gc/new_bs_BDDhigh.con +cic:/Cachan/SMC/gc/new_bs_BDDlow.con +cic:/Cachan/SMC/gc/new_bs.con +cic:/Cachan/SMC/gc/new_bs_lemma_1.con +cic:/Cachan/SMC/gc/new_bs_lemma_2.con +cic:/Cachan/SMC/gc/new_bs_OK.con +cic:/Cachan/SMC/gc/new_bs_one.con +cic:/Cachan/SMC/gc/new_bs_used_nodes_preserved.con +cic:/Cachan/SMC/gc/new_bs_zero.con +cic:/Cachan/SMC/gc/new_cfg_OK.con +cic:/Cachan/SMC/gc/new_cnt_OK.con +cic:/Cachan/SMC/gc/new_fl.con +cic:/Cachan/SMC/gc/new_fl_OK.con +cic:/Cachan/SMC/gc/new_negm_OK.con +cic:/Cachan/SMC/gc/new_orm_OK.con +cic:/Cachan/SMC/gc/new_share_OK.con +cic:/Cachan/SMC/gc/new_univm_OK.con +cic:/Cachan/SMC/gc/no_new_node_new_bs.con +cic:/Cachan/SMC/gc/set_closed.con +cic:/Cachan/SMC/gc/used_node_bs_1.con +cic:/Cachan/SMC/gc/used_node_bs_1_preserved.con +cic:/Cachan/SMC/make/BDDmake_bool_fun.con +cic:/Cachan/SMC/make/BDDmake.con +cic:/Cachan/SMC/make/BDDmake_keeps_config_OK.con +cic:/Cachan/SMC/make/BDDmake_node_height_eq_1.con +cic:/Cachan/SMC/make/BDDmake_node_height_eq.con +cic:/Cachan/SMC/make/BDDmake_node_height_le.con +cic:/Cachan/SMC/make/BDDmake_node_OK.con +cic:/Cachan/SMC/make/BDDmake_preserves_used_nodes.con +cic:/Cachan/SMC/make/no_dup.con +cic:/Cachan/SMC/misc/ad_gt_1_lemma.con +cic:/Cachan/SMC/misc/ad_lt_lemma.con +cic:/Cachan/SMC/misc/ad_S_compare.con +cic:/Cachan/SMC/misc/ad_S.con +cic:/Cachan/SMC/misc/ad_S_is_S.con +cic:/Cachan/SMC/misc/ad_S_le_then_neq.con +cic:/Cachan/SMC/misc/ad_S_neq_ad_z.con +cic:/Cachan/SMC/misc/andb3_lemma_1.con +cic:/Cachan/SMC/misc/andb3_lemma.con +cic:/Cachan/SMC/misc/BDDcompare_1.con +cic:/Cachan/SMC/misc/BDDcompare.con +cic:/Cachan/SMC/misc/BDDcompare_inf_sup.con +cic:/Cachan/SMC/misc/BDDcompare_lt.con +cic:/Cachan/SMC/misc/BDDcompare_sup_inf.con +cic:/Cachan/SMC/misc/BDDcompare_trans.con +cic:/Cachan/SMC/misc/BDD_EGAL_complete.con +cic:/Cachan/SMC/misc/BDD_EGAL_correct.con +cic:/Cachan/SMC/misc/BDDlt_compare.con +cic:/Cachan/SMC/misc/BDDvar.con +cic:/Cachan/SMC/misc/BDDvar_le_max_1.con +cic:/Cachan/SMC/misc/BDDvar_le_max_2.con +cic:/Cachan/SMC/misc/BDDvar_max_comm.con +cic:/Cachan/SMC/misc/BDDvar_max.con +cic:/Cachan/SMC/misc/BDDvar_max_inf.con +cic:/Cachan/SMC/misc/BDDvar_max_max.con +cic:/Cachan/SMC/misc/eq_ad_S_eq.con +cic:/Cachan/SMC/misc/list_sum.con +cic:/Cachan/SMC/misc/lt_max_1_2.con +cic:/Cachan/SMC/misc/lt_max_1.con +cic:/Cachan/SMC/misc/lt_max_2.con +cic:/Cachan/SMC/misc/lt_trans_1.con +cic:/Cachan/SMC/misc/max.con +cic:/Cachan/SMC/misc/max_x_x_eq_x.con +cic:/Cachan/SMC/misc/nat_gt_1_lemma.con +cic:/Cachan/SMC/misc/no_dup_cons_no_dup.con +cic:/Cachan/SMC/misc/no_dup_cons_no_in.con +cic:/Cachan/SMC/misc/no_dup_list.ind +cic:/Cachan/SMC/misc/no_dup_list_ind.con +cic:/Cachan/SMC/misc/no_dup_sum.con +cic:/Cachan/SMC/misc/prod_sum.con +cic:/Cachan/SMC/misc/relation_sum.con +cic:/Cachan/SMC/mu/ad_to_be_eq1.con +cic:/Cachan/SMC/mu/ad_to_be_eq.con +cic:/Cachan/SMC/mu/ad_to_be_ok.con +cic:/Cachan/SMC/mu/BDDiter2n.con +cic:/Cachan/SMC/mu/BDDiter2n_lemma1.con +cic:/Cachan/SMC/mu/BDDiter2n_lemma2.con +cic:/Cachan/SMC/mu/BDDiter_as_iter.con +cic:/Cachan/SMC/mu/BDDiter.con +cic:/Cachan/SMC/mu/BDDmu_eval.con +cic:/Cachan/SMC/mu/BDDmu_eval_ok.con +cic:/Cachan/SMC/mu/be_iter1.con +cic:/Cachan/SMC/mu/be_iter1eq2.con +cic:/Cachan/SMC/mu/be_iter1_fix_ex.con +cic:/Cachan/SMC/mu/be_iter1_inc.con +cic:/Cachan/SMC/mu/be_iter1_le_preserved.con +cic:/Cachan/SMC/mu/be_iter1_n_le.con +cic:/Cachan/SMC/mu/be_iter1_ok.con +cic:/Cachan/SMC/mu/be_iter1_plus1.con +cic:/Cachan/SMC/mu/be_iter1_plus.con +cic:/Cachan/SMC/mu/be_iter1_preserves_eq.con +cic:/Cachan/SMC/mu/be_iter2.con +cic:/Cachan/SMC/mu/be_iter2n_0.con +cic:/Cachan/SMC/mu/be_iter2n_2n.con +cic:/Cachan/SMC/mu/be_iter2n.con +cic:/Cachan/SMC/mu/be_iter2n_eq_preserved_1.con +cic:/Cachan/SMC/mu/be_iter2n_eq_preserved_2.con +cic:/Cachan/SMC/mu/be_iter2n_eq_preserved.con +cic:/Cachan/SMC/mu/be_iter2n_false.con +cic:/Cachan/SMC/mu/be_iter2n_is_lfp_be.con +cic:/Cachan/SMC/mu/be_iter2n_le_preserved.con +cic:/Cachan/SMC/mu/be_iter2n_prop_preserved.con +cic:/Cachan/SMC/mu/be_iter2n_true.con +cic:/Cachan/SMC/mu/be_iter.con +cic:/Cachan/SMC/mu/be_iter_eq_1.con +cic:/Cachan/SMC/mu/be_iter_eq_preserved_1.con +cic:/Cachan/SMC/mu/be_iter_eq_preserved.con +cic:/Cachan/SMC/mu/be_iter_is_lfp_be.con +cic:/Cachan/SMC/mu/be_iter_le_preserved.con +cic:/Cachan/SMC/mu/be_iter_prop_preserved.con +cic:/Cachan/SMC/mu/be_le1.con +cic:/Cachan/SMC/mu/be_le1_le.con +cic:/Cachan/SMC/mu/be_le_ens_inc.con +cic:/Cachan/SMC/mu/be_le_le1.con +cic:/Cachan/SMC/mu/be_le_zero.con +cic:/Cachan/SMC/mu/beq_complete.con +cic:/Cachan/SMC/mu/beq_correct.con +cic:/Cachan/SMC/mu/beq_Eq_true.con +cic:/Cachan/SMC/mu/be_to_be_inc.con +cic:/Cachan/SMC/mu/bool_expr_to_var_env''_card.con +cic:/Cachan/SMC/mu/bool_expr_to_var_env''.con +cic:/Cachan/SMC/mu/bool_expr_to_var_env''_finite.con +cic:/Cachan/SMC/mu/Brel_env.con +cic:/Cachan/SMC/mu/Btrans_env.con +cic:/Cachan/SMC/mu/card_Evar_env''LSU_lemma.con +cic:/Cachan/SMC/mu/card_imagef1'lemma.con +cic:/Cachan/SMC/mu/card_imagef1'orf2'lemma.con +cic:/Cachan/SMC/mu/card_imagef2'lemma.con +cic:/Cachan/SMC/mu/cardinal_Union.con +cic:/Cachan/SMC/mu/cfgnode_eq.con +cic:/Cachan/SMC/mu/cfg_re_bre_ok.con +cic:/Cachan/SMC/mu/cfg_re_bre_ok_put.con +cic:/Cachan/SMC/mu/cfg_te_bte_ok.con +cic:/Cachan/SMC/mu/cfg_ul_bre_cons_ok.con +cic:/Cachan/SMC/mu/cfg_ul_bre_ok.con +cic:/Cachan/SMC/mu/cfg_ul_bre_ok_put.con +cic:/Cachan/SMC/mu/cfg_ul_bte_cons_ok.con +cic:/Cachan/SMC/mu/cfg_ul_bte_ok.con +cic:/Cachan/SMC/mu/cfg_ul_re_bre_ok_preserved.con +cic:/Cachan/SMC/mu/cfg_ul_te_bte_ok_preserved.con +cic:/Cachan/SMC/mu/decreasing_be_seq_1.con +cic:/Cachan/SMC/mu/decreasing_be_seq.con +cic:/Cachan/SMC/mu/decreasing_ens_seq.con +cic:/Cachan/SMC/mu/decreasing_seq.con +cic:/Cachan/SMC/mu/Eenv''_var''card.con +cic:/Cachan/SMC/mu/Eenv''_var''finite.con +cic:/Cachan/SMC/mu/Eenv_var''LU_card.con +cic:/Cachan/SMC/mu/Eenv_var''LU_finite.con +cic:/Cachan/SMC/mu/empty_map_card.con +cic:/Cachan/SMC/mu/eval_be_independent.con +cic:/Cachan/SMC/mu/Evar_env'.con +cic:/Cachan/SMC/mu/Evar_env''.con +cic:/Cachan/SMC/mu/Evar_env''LSU.con +cic:/Cachan/SMC/mu/Evar_env'LSU.con +cic:/Cachan/SMC/mu/Evar_env''LSU_finite.con +cic:/Cachan/SMC/mu/Evar_env''LSULU.con +cic:/Cachan/SMC/mu/Evar_env''LU.con +cic:/Cachan/SMC/mu/Evar_env'LU.con +cic:/Cachan/SMC/mu/Evar_env''ntoSn.con +cic:/Cachan/SMC/mu/Evar_env'ntoSn.con +cic:/Cachan/SMC/mu/Evar_env''ntoSn_lemma.con +cic:/Cachan/SMC/mu/Evar_env'ntoSn_lemma.con +cic:/Cachan/SMC/mu/f1.con +cic:/Cachan/SMC/mu/f1'.con +cic:/Cachan/SMC/mu/f2.con +cic:/Cachan/SMC/mu/f2'.con +cic:/Cachan/SMC/mu/f_bre_ok.con +cic:/Cachan/SMC/mu/f_bte_ok.con +cic:/Cachan/SMC/mu/f_ok.ind +cic:/Cachan/SMC/mu/f_ok_ind.con +cic:/Cachan/SMC/mu/fp.con +cic:/Cachan/SMC/mu/f_P_even.ind +cic:/Cachan/SMC/mu/f_P_even_ind.con +cic:/Cachan/SMC/mu/imagef1.con +cic:/Cachan/SMC/mu/imagef1'.con +cic:/Cachan/SMC/mu/imagef1'finite.con +cic:/Cachan/SMC/mu/imagef1lemma'.con +cic:/Cachan/SMC/mu/imagef1'orf2'.con +cic:/Cachan/SMC/mu/imagef1orf2.con +cic:/Cachan/SMC/mu/imagef1'orf2'finite.con +cic:/Cachan/SMC/mu/imagef1'orf2'lemma.con +cic:/Cachan/SMC/mu/imagef2.con +cic:/Cachan/SMC/mu/imagef2'.con +cic:/Cachan/SMC/mu/imagef2'finite.con +cic:/Cachan/SMC/mu/imagef2lemma'.con +cic:/Cachan/SMC/mu/incl_eq.con +cic:/Cachan/SMC/mu/increasing_be_seq_1.con +cic:/Cachan/SMC/mu/increasing_seq.con +cic:/Cachan/SMC/mu/iter2n.con +cic:/Cachan/SMC/mu/iter.con +cic:/Cachan/SMC/mu/le_minus_le.con +cic:/Cachan/SMC/mu/le_minus_minus.con +cic:/Cachan/SMC/mu/lfp_be.con +cic:/Cachan/SMC/mu/lfp_be_lfp.con +cic:/Cachan/SMC/mu/lfp.con +cic:/Cachan/SMC/mu/lt_mn_minus.con +cic:/Cachan/SMC/mu/lx'N.con +cic:/Cachan/SMC/mu/lxN.con +cic:/Cachan/SMC/mu/M0inEvar_env''.con +cic:/Cachan/SMC/mu/Map_eq_complete.con +cic:/Cachan/SMC/mu/Map_eq.con +cic:/Cachan/SMC/mu/Map_eq_correct.con +cic:/Cachan/SMC/mu/Map_eq_dec.con +cic:/Cachan/SMC/mu/mf_be_ok.con +cic:/Cachan/SMC/mu/mf.con +cic:/Cachan/SMC/mu/mf_fix_ex.con +cic:/Cachan/SMC/mu/mf_inc.con +cic:/Cachan/SMC/mu/mf_lfp.con +cic:/Cachan/SMC/mu/mf_preserves_eq.con +cic:/Cachan/SMC/mu/mfs.con +cic:/Cachan/SMC/mu/minus_n_m_le_n.con +cic:/Cachan/SMC/mu/minusUL0_var_lu.con +cic:/Cachan/SMC/mu/mu_all_bre_ok.con +cic:/Cachan/SMC/mu/mu_all_bte_ok.con +cic:/Cachan/SMC/mu/mu_all_eval_lu.con +cic:/Cachan/SMC/mu/mu_and_bre_ok.con +cic:/Cachan/SMC/mu/mu_and_bte_ok.con +cic:/Cachan/SMC/mu/mu_ap_ok_inv.con +cic:/Cachan/SMC/mu/mu_eval.con +cic:/Cachan/SMC/mu/mu_eval_lemma1.con +cic:/Cachan/SMC/mu/mu_eval_lemma2.con +cic:/Cachan/SMC/mu/mu_eval_mu_is_lfp.con +cic:/Cachan/SMC/mu/mu_ex_bre_ok.con +cic:/Cachan/SMC/mu/mu_ex_bte_ok.con +cic:/Cachan/SMC/mu/mu_ex_eval_lu.con +cic:/Cachan/SMC/mu/mu_form_ap_ok.ind +cic:/Cachan/SMC/mu/mu_form_ap_ok_ind.con +cic:/Cachan/SMC/mu/mu_form.ind +cic:/Cachan/SMC/mu/mu_form_ind.con +cic:/Cachan/SMC/mu/mu_form_rec.con +cic:/Cachan/SMC/mu/mu_form_rect.con +cic:/Cachan/SMC/mu/mu_iff_bre_ok.con +cic:/Cachan/SMC/mu/mu_iff_bte_ok.con +cic:/Cachan/SMC/mu/mu_impl_bre_ok.con +cic:/Cachan/SMC/mu/mu_impl_bte_ok.con +cic:/Cachan/SMC/mu/mu_mu_bre_ok.con +cic:/Cachan/SMC/mu/mu_or_bre_ok.con +cic:/Cachan/SMC/mu/mu_or_bte_ok.con +cic:/Cachan/SMC/mu/mu_rel_free.con +cic:/Cachan/SMC/mu/mu_t_free.con +cic:/Cachan/SMC/mu/nat_lu.con +cic:/Cachan/SMC/mu/nat_lu_var_lu.con +cic:/Cachan/SMC/munew/be_dash.con +cic:/Cachan/SMC/munew/bool_fun_of_be_ext1.con +cic:/Cachan/SMC/munew/dash_be_ok.con +cic:/Cachan/SMC/munew/dash_renf.con +cic:/Cachan/SMC/munew/eval_dash_lemma1.con +cic:/Cachan/SMC/munew/exl_semantics.con +cic:/Cachan/SMC/munew/forall_lemma1.con +cic:/Cachan/SMC/munew/mu_all_eval_semantics1.con +cic:/Cachan/SMC/munew/mu_all_eval_semantics2.con +cic:/Cachan/SMC/munew/mu_ex_eval_semantics1.con +cic:/Cachan/SMC/munew/mu_ex_eval_semantics2.con +cic:/Cachan/SMC/munew/no_dup_lx'_1.con +cic:/Cachan/SMC/munew/renamef.con +cic:/Cachan/SMC/munew/renamef_ext.con +cic:/Cachan/SMC/munew/renamef_id.con +cic:/Cachan/SMC/munew/renamefS.con +cic:/Cachan/SMC/munew/renfnad.con +cic:/Cachan/SMC/munew/renfnat.con +cic:/Cachan/SMC/munew/replacel_lemma2.con +cic:/Cachan/SMC/munew/replacel_lemma.con +cic:/Cachan/SMC/munew/univl_semantics.con +cic:/Cachan/SMC/munew/var_env'_dash.con +cic:/Cachan/SMC/munew/var_env''_dash.con +cic:/Cachan/SMC/munew/var_env_or.con +cic:/Cachan/SMC/munew/var_env'_or.con +cic:/Cachan/SMC/mu/rel_env.con +cic:/Cachan/SMC/mu/re_put.con +cic:/Cachan/SMC/mu/re_to_be_dec.con +cic:/Cachan/SMC/mu/re_to_be_inc.con +cic:/Cachan/SMC/mu/same_set_finite.con +cic:/Cachan/SMC/mu/same_set_same_cardinal.con +cic:/Cachan/SMC/mu/seq.con +cic:/Cachan/SMC/mu/seq_eq.con +cic:/Cachan/SMC/mu/seq_inj.con +cic:/Cachan/SMC/mu/seq_surj.con +cic:/Cachan/SMC/muset/env_to_be_lemma1.con +cic:/Cachan/SMC/muset/env_to_be_lemma.con +cic:/Cachan/SMC/muset/le_minus_le1.con +cic:/Cachan/SMC/muset/muevaleqset.con +cic:/Cachan/SMC/muset/mu_form2set.con +cic:/Cachan/SMC/muset/new_t_to_rel.con +cic:/Cachan/SMC/muset/rel_1.con +cic:/Cachan/SMC/muset/relfreeeven.con +cic:/Cachan/SMC/muset/re_sre_ok.con +cic:/Cachan/SMC/muset/set_0.con +cic:/Cachan/SMC/muset/set_1.con +cic:/Cachan/SMC/muset/set_all.con +cic:/Cachan/SMC/muset/set_and.con +cic:/Cachan/SMC/muset/set_ap.con +cic:/Cachan/SMC/muset/set_ap_state_set.con +cic:/Cachan/SMC/muset/set_ex.ind +cic:/Cachan/SMC/muset/set_ex_ind.con +cic:/Cachan/SMC/muset/set_iff.con +cic:/Cachan/SMC/muset/set_impl.con +cic:/Cachan/SMC/muset/set_mu.con +cic:/Cachan/SMC/muset/set_neg.con +cic:/Cachan/SMC/muset/set_or.con +cic:/Cachan/SMC/muset/set_renv.con +cic:/Cachan/SMC/muset/set_tenv.con +cic:/Cachan/SMC/muset/sre_put.con +cic:/Cachan/SMC/muset/state_rel.con +cic:/Cachan/SMC/muset/state_set.con +cic:/Cachan/SMC/muset/te_ste_ok.con +cic:/Cachan/SMC/muset/t_to_rel1.con +cic:/Cachan/SMC/muset/t_to_rel.con +cic:/Cachan/SMC/muset/var_env'_to_env''_to_env'.con +cic:/Cachan/SMC/muset/ve''_to_be.con +cic:/Cachan/SMC/muset/ve''_to_be_ok1.con +cic:/Cachan/SMC/muset/ve''_to_be_ok2.con +cic:/Cachan/SMC/muset/ve''_to_be_ok3.con +cic:/Cachan/SMC/muset/ve''_to_be_ok.con +cic:/Cachan/SMC/mu/singleton_add_empty.con +cic:/Cachan/SMC/mu/singleton_cardinal_one.con +cic:/Cachan/SMC/mu/Splus_nm.con +cic:/Cachan/SMC/mu/trans_env.con +cic:/Cachan/SMC/mu/two_power.con +cic:/Cachan/SMC/mu/unprimed_var.con +cic:/Cachan/SMC/mu/var_env''cardinal_one.con +cic:/Cachan/SMC/mu/var_env_eq.con +cic:/Cachan/SMC/mu/var_env''le.con +cic:/Cachan/SMC/mu/var_env''le_refl.con +cic:/Cachan/SMC/mu/var_env''le_trans.con +cic:/Cachan/SMC/mu/var_env''M0.con +cic:/Cachan/SMC/mu/var_env''singleton.con +cic:/Cachan/SMC/mu/var_env'_to_env''.con +cic:/Cachan/SMC/mu/var_env'_to_env''_lemma3.con +cic:/Cachan/SMC/mu/var_env'_to_var_env''_lemma1.con +cic:/Cachan/SMC/mu/var_env'_to_var_env''_lemma2.con +cic:/Cachan/SMC/mu/var_lu.con +cic:/Cachan/SMC/mu/var_lu_nat_lu.con +cic:/Cachan/SMC/mu/zero_lt_pow.con +cic:/Cachan/SMC/myMap/eqmap_equiv.con +cic:/Cachan/SMC/myMap/F.con +cic:/Cachan/SMC/myMap/f_OK.con +cic:/Cachan/SMC/myMap/makeM2_MapDom_lemma.con +cic:/Cachan/SMC/myMap/map_app_list1.con +cic:/Cachan/SMC/myMap/map_app_list1_lemma_1.con +cic:/Cachan/SMC/myMap/map_app_list1_lemma_2.con +cic:/Cachan/SMC/myMap/map_app_list1_lemma_3.con +cic:/Cachan/SMC/myMap/map_app_list1_lemma_4.con +cic:/Cachan/SMC/myMap/MapDomRestrByApp1.con +cic:/Cachan/SMC/myMap/MapDomRestrByApp1_lemma_1.con +cic:/Cachan/SMC/myMap/MapDomRestrByApp1_lemma_2.con +cic:/Cachan/SMC/myMap/MapDomRestrByApp1_lemma_3.con +cic:/Cachan/SMC/myMap/MapDomRestrByApp1_lemma_4.con +cic:/Cachan/SMC/myMap/MapDomRestrTo_DomBy.con +cic:/Cachan/SMC/myMap/MapDomRestrTo_DomBy_lemma_1.con +cic:/Cachan/SMC/myMap/MapDomRestrTo_DomBy_lemma_2.con +cic:/Cachan/SMC/myMap/MapGet2.con +cic:/Cachan/SMC/myMap/MapGet3.con +cic:/Cachan/SMC/myMap/MapMerge_assoc.con +cic:/Cachan/SMC/myMap/MapMerge_eq.con +cic:/Cachan/SMC/myMap/MapMerge_neutral_left.con +cic:/Cachan/SMC/myMap/MapMerge_neutral_right.con +cic:/Cachan/SMC/myMap/Mapn.con +cic:/Cachan/SMC/myMap/MapPut2.con +cic:/Cachan/SMC/myMap/MapPut2_semantics.con +cic:/Cachan/SMC/myMap/MapPut3.con +cic:/Cachan/SMC/myMap/MapPut3_semantics.con +cic:/Cachan/SMC/myMap/my_alist_of_map_lemma_1.con +cic:/Cachan/SMC/myMap/my_alist_of_map_lemma_2.con +cic:/Cachan/SMC/myMap/my_alist_of_map_lemma_3.con +cic:/Cachan/SMC/myMap/my_fold_right_aapp.con +cic:/Cachan/SMC/myMap/my_fold_right_lemma.con +cic:/Cachan/SMC/myMap/myMapFold_as_fold_1.con +cic:/Cachan/SMC/myMap/myMapFold_as_fold_2.con +cic:/Cachan/SMC/myMap/myMapFold_as_fold.con +cic:/Cachan/SMC/myMap/myMapFold_lemma.con +cic:/Cachan/SMC/myMap/no_dup_alist.con +cic:/Cachan/SMC/myMap/no_dup_alist_of_Map.con +cic:/Cachan/SMC/myMap/op_eq_2.con +cic:/Cachan/SMC/neg/BDDneg_1.con +cic:/Cachan/SMC/neg/BDDneg_1_lemma.con +cic:/Cachan/SMC/op/BDDand.con +cic:/Cachan/SMC/op/BDDand_config_OK.con +cic:/Cachan/SMC/op/BDDand_is_and.con +cic:/Cachan/SMC/op/BDDand_list_OK.con +cic:/Cachan/SMC/op/BDDand_list_OK_cons.con +cic:/Cachan/SMC/op/BDDand_node_OK.con +cic:/Cachan/SMC/op/BDDand_used_nodes_preserved.con +cic:/Cachan/SMC/op/BDDand_var_le.con +cic:/Cachan/SMC/op/BDDiff.con +cic:/Cachan/SMC/op/BDDiff_config_OK.con +cic:/Cachan/SMC/op/BDDiff_is_iff.con +cic:/Cachan/SMC/op/BDDiff_list_OK.con +cic:/Cachan/SMC/op/BDDiff_list_OK_cons.con +cic:/Cachan/SMC/op/BDDiff_node_OK.con +cic:/Cachan/SMC/op/BDDiff_used_nodes_preserved.con +cic:/Cachan/SMC/op/BDDimpl.con +cic:/Cachan/SMC/op/BDDimpl_config_OK.con +cic:/Cachan/SMC/op/BDDimpl_is_impl.con +cic:/Cachan/SMC/op/BDDimpl_list_OK.con +cic:/Cachan/SMC/op/BDDimpl_list_OK_cons.con +cic:/Cachan/SMC/op/BDDimpl_node_OK.con +cic:/Cachan/SMC/op/BDDimpl_used_nodes_preserved.con +cic:/Cachan/SMC/op/BDDneg.con +cic:/Cachan/SMC/op/BDDneg_config_OK.con +cic:/Cachan/SMC/op/BDDneg_is_neg.con +cic:/Cachan/SMC/op/BDDneg_list_OK.con +cic:/Cachan/SMC/op/BDDneg_list_OK_cons.con +cic:/Cachan/SMC/op/BDDneg_node_OK.con +cic:/Cachan/SMC/op/BDDneg_used_nodes_preserved.con +cic:/Cachan/SMC/op/BDDneg_var_eq.con +cic:/Cachan/SMC/op/BDDor.con +cic:/Cachan/SMC/op/BDDor_config_OK.con +cic:/Cachan/SMC/op/BDDor_is_or.con +cic:/Cachan/SMC/op/BDDor_list_OK.con +cic:/Cachan/SMC/op/BDDor_list_OK_cons.con +cic:/Cachan/SMC/op/BDDor_node_OK.con +cic:/Cachan/SMC/op/BDDor_used_nodes_preserved.con +cic:/Cachan/SMC/op/BDDor_var_le.con +cic:/Cachan/SMC/op/BDDvar_make.con +cic:/Cachan/SMC/op/BDDvar_make_config_OK.con +cic:/Cachan/SMC/op/BDDvar_make_is_var.con +cic:/Cachan/SMC/op/BDDvar_make_list_OK.con +cic:/Cachan/SMC/op/BDDvar_make_list_OK_cons.con +cic:/Cachan/SMC/op/BDDvar_make_node_OK.con +cic:/Cachan/SMC/op/BDDvar_make_used_nodes_preserved.con +cic:/Cachan/SMC/or/BDDor_1.con +cic:/Cachan/SMC/or/BDDor_1_lemma.con +cic:/Cachan/SMC/quant/ad_list_neq.con +cic:/Cachan/SMC/quant/and_eq.con +cic:/Cachan/SMC/quant/and_le2.con +cic:/Cachan/SMC/quant/and_le.con +cic:/Cachan/SMC/quant/and_ok_inv.con +cic:/Cachan/SMC/quant/and_x_free.con +cic:/Cachan/SMC/quant/ap.con +cic:/Cachan/SMC/quant/ap'.con +cic:/Cachan/SMC/quant/ap'_eq_ap.con +cic:/Cachan/SMC/quant/ap_neq_ap'.con +cic:/Cachan/SMC/quant/BDDex.con +cic:/Cachan/SMC/quant/BDDex_config_OK.con +cic:/Cachan/SMC/quant/BDDex_is_ex.con +cic:/Cachan/SMC/quant/BDDexl.con +cic:/Cachan/SMC/quant/BDDexl_config_OK.con +cic:/Cachan/SMC/quant/BDDexl_is_exl.con +cic:/Cachan/SMC/quant/BDDex_list_OK.con +cic:/Cachan/SMC/quant/BDDex_list_OK_cons.con +cic:/Cachan/SMC/quant/BDDexl_lemma.con +cic:/Cachan/SMC/quant/BDDexl_list_OK.con +cic:/Cachan/SMC/quant/BDDexl_list_OK_cons.con +cic:/Cachan/SMC/quant/BDDexl_node_OK.con +cic:/Cachan/SMC/quant/BDDexl_used_nodes_preserved.con +cic:/Cachan/SMC/quant/BDDex_node_OK.con +cic:/Cachan/SMC/quant/BDDex_used_nodes_preserved.con +cic:/Cachan/SMC/quant/BDDmu_all.con +cic:/Cachan/SMC/quant/BDDmu_all_config_OK.con +cic:/Cachan/SMC/quant/BDDmu_all_is_mu_all.con +cic:/Cachan/SMC/quant/BDDmu_all_lemma.con +cic:/Cachan/SMC/quant/BDDmu_all_list_OK.con +cic:/Cachan/SMC/quant/BDDmu_all_list_OK_cons.con +cic:/Cachan/SMC/quant/BDDmu_all_node_OK.con +cic:/Cachan/SMC/quant/BDDmu_all_used_nodes_preserved.con +cic:/Cachan/SMC/quant/BDDmu_ex.con +cic:/Cachan/SMC/quant/BDDmu_ex_config_OK.con +cic:/Cachan/SMC/quant/BDDmu_ex_is_mu_ex.con +cic:/Cachan/SMC/quant/BDDmu_ex_lemma.con +cic:/Cachan/SMC/quant/BDDmu_ex_list_OK.con +cic:/Cachan/SMC/quant/BDDmu_ex_list_OK_cons.con +cic:/Cachan/SMC/quant/BDDmu_ex_node_OK.con +cic:/Cachan/SMC/quant/BDDmu_ex_used_nodes_preserved.con +cic:/Cachan/SMC/quant/BDDreplace.con +cic:/Cachan/SMC/quant/BDDreplace_config_OK.con +cic:/Cachan/SMC/quant/BDDreplace_is_replace.con +cic:/Cachan/SMC/quant/BDDreplacel.con +cic:/Cachan/SMC/quant/BDDreplacel_config_OK.con +cic:/Cachan/SMC/quant/BDDreplacel_is_replacel.con +cic:/Cachan/SMC/quant/BDDreplace_list_OK.con +cic:/Cachan/SMC/quant/BDDreplace_list_OK_cons.con +cic:/Cachan/SMC/quant/BDDreplacel_lemma.con +cic:/Cachan/SMC/quant/BDDreplacel_list_OK.con +cic:/Cachan/SMC/quant/BDDreplacel_list_OK_cons.con +cic:/Cachan/SMC/quant/BDDreplacel_node_OK.con +cic:/Cachan/SMC/quant/BDDreplacel_used_nodes_preserved.con +cic:/Cachan/SMC/quant/BDDreplace_node_OK.con +cic:/Cachan/SMC/quant/BDDreplace_used_nodes_preserved.con +cic:/Cachan/SMC/quant/BDDsubst.con +cic:/Cachan/SMC/quant/BDDsubst_config_OK.con +cic:/Cachan/SMC/quant/BDDsubst_is_subst1.con +cic:/Cachan/SMC/quant/BDDsubst_is_subst.con +cic:/Cachan/SMC/quant/BDDsubst_lemma.con +cic:/Cachan/SMC/quant/BDDsubst_list_OK.con +cic:/Cachan/SMC/quant/BDDsubst_list_OK_cons.con +cic:/Cachan/SMC/quant/BDDsubst_node_OK.con +cic:/Cachan/SMC/quant/BDDsubst_used_nodes_preserved.con +cic:/Cachan/SMC/quant/BDDuniv.con +cic:/Cachan/SMC/quant/BDDuniv_config_OK.con +cic:/Cachan/SMC/quant/BDDuniv_is_univ.con +cic:/Cachan/SMC/quant/BDDunivl.con +cic:/Cachan/SMC/quant/BDDunivl_config_OK.con +cic:/Cachan/SMC/quant/BDDuniv_list_OK.con +cic:/Cachan/SMC/quant/BDDuniv_list_OK_cons.con +cic:/Cachan/SMC/quant/BDDunivl_is_univl.con +cic:/Cachan/SMC/quant/BDDunivl_lemma.con +cic:/Cachan/SMC/quant/BDDunivl_list_OK.con +cic:/Cachan/SMC/quant/BDDunivl_list_OK_cons.con +cic:/Cachan/SMC/quant/BDDunivl_node_OK.con +cic:/Cachan/SMC/quant/BDDunivl_used_nodes_preserved.con +cic:/Cachan/SMC/quant/BDDuniv_node_OK.con +cic:/Cachan/SMC/quant/BDDuniv_used_nodes_preserved.con +cic:/Cachan/SMC/quant/BDDuniv_var_le.con +cic:/Cachan/SMC/quant/be_eq.con +cic:/Cachan/SMC/quant/be_eq_dec_complete.con +cic:/Cachan/SMC/quant/be_eq_dec.con +cic:/Cachan/SMC/quant/be_eq_dec_correct.con +cic:/Cachan/SMC/quant/be_eq_dec_eq.con +cic:/Cachan/SMC/quant/be_eq_eq_dec.con +cic:/Cachan/SMC/quant/be_eq_le.con +cic:/Cachan/SMC/quant/be_eq_refl.con +cic:/Cachan/SMC/quant/be_eq_sym.con +cic:/Cachan/SMC/quant/be_eq_trans.con +cic:/Cachan/SMC/quant/be_ex.con +cic:/Cachan/SMC/quant/be_le2.con +cic:/Cachan/SMC/quant/be_le2_le.con +cic:/Cachan/SMC/quant/be_le_antisym.con +cic:/Cachan/SMC/quant/be_le.con +cic:/Cachan/SMC/quant/be_le_le2.con +cic:/Cachan/SMC/quant/be_le_not_1.con +cic:/Cachan/SMC/quant/be_le_refl.con +cic:/Cachan/SMC/quant/be_le_trans.con +cic:/Cachan/SMC/quant/be_ok_be_x_free.con +cic:/Cachan/SMC/quant/be_ok.ind +cic:/Cachan/SMC/quant/be_ok_ind.con +cic:/Cachan/SMC/quant/be_x_free_be_ok.con +cic:/Cachan/SMC/quant/be_x_free.con +cic:/Cachan/SMC/quant/bool_fun_and_ext.con +cic:/Cachan/SMC/quant/bool_fun_exl.con +cic:/Cachan/SMC/quant/bool_fun_exl_preserves_eq.con +cic:/Cachan/SMC/quant/bool_fun_iff_ext.con +cic:/Cachan/SMC/quant/bool_fun_impl_ext.con +cic:/Cachan/SMC/quant/bool_fun_mu_all.con +cic:/Cachan/SMC/quant/bool_fun_mu_all_preserves_eq.con +cic:/Cachan/SMC/quant/bool_fun_mu_ex.con +cic:/Cachan/SMC/quant/bool_fun_mu_ex_preserves_eq.con +cic:/Cachan/SMC/quant/bool_fun_neg_ext.con +cic:/Cachan/SMC/quant/bool_fun_of_be_ext.con +cic:/Cachan/SMC/quant/bool_fun_or_ext.con +cic:/Cachan/SMC/quant/bool_fun_replace.con +cic:/Cachan/SMC/quant/bool_fun_replacel.con +cic:/Cachan/SMC/quant/bool_fun_replacel_preserves_eq.con +cic:/Cachan/SMC/quant/bool_fun_replace_preserves_eq.con +cic:/Cachan/SMC/quant/bool_fun_restrict1.con +cic:/Cachan/SMC/quant/bool_fun_restrict1_eq_restrict.con +cic:/Cachan/SMC/quant/bool_fun_restrict_eq_subst.con +cic:/Cachan/SMC/quant/bool_fun_subst1.con +cic:/Cachan/SMC/quant/bool_fun_subst1_eq_subst.con +cic:/Cachan/SMC/quant/bool_fun_subst.con +cic:/Cachan/SMC/quant/bool_fun_subst_preserves_eq.con +cic:/Cachan/SMC/quant/bool_fun_univl.con +cic:/Cachan/SMC/quant/bool_fun_univl_preserves_eq.con +cic:/Cachan/SMC/quant/bool_fun_var_ext.con +cic:/Cachan/SMC/quant/bool_to_be.con +cic:/Cachan/SMC/quant/bool_to_be_to_bf.con +cic:/Cachan/SMC/quant/bool_to_bf.con +cic:/Cachan/SMC/quant/eq_neg_eq.con +cic:/Cachan/SMC/quant/eval_be'.con +cic:/Cachan/SMC/quant/exl.con +cic:/Cachan/SMC/quant/ex_le2.con +cic:/Cachan/SMC/quant/exl_le2.con +cic:/Cachan/SMC/quant/exl_OK.con +cic:/Cachan/SMC/quant/exl_x_free.con +cic:/Cachan/SMC/quant/ex_OK.con +cic:/Cachan/SMC/quant/ex_x_free.con +cic:/Cachan/SMC/quant/forall_.con +cic:/Cachan/SMC/quant/forall_OK.con +cic:/Cachan/SMC/quant/iff_eq.con +cic:/Cachan/SMC/quant/iff_ok_inv.con +cic:/Cachan/SMC/quant/impl_eq.con +cic:/Cachan/SMC/quant/impl_le2.con +cic:/Cachan/SMC/quant/impl_le.con +cic:/Cachan/SMC/quant/impl_ok_inv.con +cic:/Cachan/SMC/quant/impl_x_free.con +cic:/Cachan/SMC/quant/in_lx'_1.con +cic:/Cachan/SMC/quant/in_lx'_1_conv.con +cic:/Cachan/SMC/quant/in_lx'.con +cic:/Cachan/SMC/quant/length_lx_1_eq_lx'_1.con +cic:/Cachan/SMC/quant/length_lx_eq_lx'.con +cic:/Cachan/SMC/quant/lt_O_n_lx'_1.con +cic:/Cachan/SMC/quant/lx_1.con +cic:/Cachan/SMC/quant/lx'_1.con +cic:/Cachan/SMC/quant/lx_1_neg_lx'_1.con +cic:/Cachan/SMC/quant/lx.con +cic:/Cachan/SMC/quant/lx'.con +cic:/Cachan/SMC/quant/lx_neq_lx'.con +cic:/Cachan/SMC/quant/mu_all_eq.con +cic:/Cachan/SMC/quant/mu_all_eval.con +cic:/Cachan/SMC/quant/mu_all_eval_ok.con +cic:/Cachan/SMC/quant/mu_all_le2.con +cic:/Cachan/SMC/quant/mu_all_le.con +cic:/Cachan/SMC/quant/mu_all_x_free.con +cic:/Cachan/SMC/quant/mu_ex_eq.con +cic:/Cachan/SMC/quant/mu_ex_eval.con +cic:/Cachan/SMC/quant/mu_ex_eval_ok.con +cic:/Cachan/SMC/quant/mu_ex_le2.con +cic:/Cachan/SMC/quant/mu_ex_le.con +cic:/Cachan/SMC/quant/mu_ex_x_free.con +cic:/Cachan/SMC/quant/neg_eq_eq.con +cic:/Cachan/SMC/quant/neg_ok_inv.con +cic:/Cachan/SMC/quant/or_eq.con +cic:/Cachan/SMC/quant/or_le2.con +cic:/Cachan/SMC/quant/or_le.con +cic:/Cachan/SMC/quant/or_ok_inv.con +cic:/Cachan/SMC/quant/replace.con +cic:/Cachan/SMC/quant/replacel.con +cic:/Cachan/SMC/quant/replace_le2.con +cic:/Cachan/SMC/quant/replacel_le2.con +cic:/Cachan/SMC/quant/replacel_OK.con +cic:/Cachan/SMC/quant/replacel_x_free.con +cic:/Cachan/SMC/quant/replace_OK.con +cic:/Cachan/SMC/quant/replace_x_free.con +cic:/Cachan/SMC/quant/restrict.con +cic:/Cachan/SMC/quant/restrict_OK.con +cic:/Cachan/SMC/quant/restrict_x_free.con +cic:/Cachan/SMC/quant/subst.con +cic:/Cachan/SMC/quant/subst_le2.con +cic:/Cachan/SMC/quant/subst_ok.con +cic:/Cachan/SMC/quant/subst_x_free.con +cic:/Cachan/SMC/quant/univl.con +cic:/Cachan/SMC/quant/univ_le2.con +cic:/Cachan/SMC/quant/univl_le2.con +cic:/Cachan/SMC/quant/univl_OK.con +cic:/Cachan/SMC/quant/univl_x_free.con +cic:/Cachan/SMC/quant/univ_x_free.con +cic:/Cachan/SMC/quant/var_env'.con +cic:/Cachan/SMC/quant/var_env''.con +cic:/Cachan/SMC/quant/var_env_to_env'.con +cic:/Cachan/SMC/quant/var_env'_to_env.con +cic:/Cachan/SMC/quant/var_env''_to_env.con +cic:/Cachan/SMC/quant/var_env''_to_env'.con +cic:/Cachan/SMC/quant/var_ok_inv.con +cic:/Cachan/SMC/tauto/BDDof_bool_expr.con +cic:/Cachan/SMC/tauto/BDDof_bool_expr_correct.con +cic:/Cachan/SMC/tauto/init_list_OK.con +cic:/Cachan/SMC/tauto/is_tauto.con +cic:/Cachan/SMC/tauto/is_tauto_lemma.con +cic:/Cachan/SMC/univ/BDDuniv_1.con +cic:/Cachan/SMC/univ/BDDuniv_1_lemma.con +cic:/Coq/Arith/Between/bet_eq.con +cic:/Coq/Arith/Between/between.ind +cic:/Coq/Arith/Between/between_ind.con +cic:/Coq/Arith/Between/between_in_int.con +cic:/Coq/Arith/Between/between_le.con +cic:/Coq/Arith/Between/between_not_exists.con +cic:/Coq/Arith/Between/between_or_exists.con +cic:/Coq/Arith/Between/between_restr.con +cic:/Coq/Arith/Between/between_Sk_l.con +cic:/Coq/Arith/Between/event_O.con +cic:/Coq/Arith/Between/eventually.con +cic:/Coq/Arith/Between/exists_between.ind +cic:/Coq/Arith/Between/exists_between_ind.con +cic:/Coq/Arith/Between/exists_in_int.con +cic:/Coq/Arith/Between/exists_le_S.con +cic:/Coq/Arith/Between/exists_lt.con +cic:/Coq/Arith/Between/exists_S_le.con +cic:/Coq/Arith/Between/in_int_between.con +cic:/Coq/Arith/Between/in_int.con +cic:/Coq/Arith/Between/in_int_exists.con +cic:/Coq/Arith/Between/in_int_intro.con +cic:/Coq/Arith/Between/in_int_lt.con +cic:/Coq/Arith/Between/in_int_p_Sq.con +cic:/Coq/Arith/Between/in_int_S.con +cic:/Coq/Arith/Between/in_int_Sp_q.con +cic:/Coq/Arith/Between/nth_le.con +cic:/Coq/Arith/Between/P_nth.ind +cic:/Coq/Arith/Between/P_nth_ind.con +cic:/Coq/Arith/Bool_nat/lt_ge_dec.con +cic:/Coq/Arith/Bool_nat/nat_eq_bool.con +cic:/Coq/Arith/Bool_nat/nat_ge_lt_bool.con +cic:/Coq/Arith/Bool_nat/nat_gt_le_bool.con +cic:/Coq/Arith/Bool_nat/nat_le_gt_bool.con +cic:/Coq/Arith/Bool_nat/nat_lt_ge_bool.con +cic:/Coq/Arith/Bool_nat/nat_noteq_bool.con +cic:/Coq/Arith/Bool_nat/notzerop_bool.con +cic:/Coq/Arith/Bool_nat/notzerop.con +cic:/Coq/Arith/Bool_nat/zerop_bool.con +cic:/Coq/Arith/Compare_dec/dec_ge.con +cic:/Coq/Arith/Compare_dec/dec_gt.con +cic:/Coq/Arith/Compare_dec/dec_le.con +cic:/Coq/Arith/Compare_dec/dec_lt.con +cic:/Coq/Arith/Compare_dec/gt_eq_gt_dec.con +cic:/Coq/Arith/Compare_dec/le_ge_dec.con +cic:/Coq/Arith/Compare_dec/le_gt_dec.con +cic:/Coq/Arith/Compare_dec/le_le_S_dec.con +cic:/Coq/Arith/Compare_dec/le_lt_dec.con +cic:/Coq/Arith/Compare_dec/le_lt_eq_dec.con +cic:/Coq/Arith/Compare_dec/lt_eq_lt_dec.con +cic:/Coq/Arith/Compare_dec/not_eq.con +cic:/Coq/Arith/Compare_dec/not_ge.con +cic:/Coq/Arith/Compare_dec/not_gt.con +cic:/Coq/Arith/Compare_dec/not_le.con +cic:/Coq/Arith/Compare_dec/not_lt.con +cic:/Coq/Arith/Compare_dec/zerop.con +cic:/Coq/Arith/Compare/discrete_nat.con +cic:/Coq/Arith/Compare/le_dec.con +cic:/Coq/Arith/Compare/le_decide.con +cic:/Coq/Arith/Compare/le_le_S_eq.con +cic:/Coq/Arith/Compare/le_or_le_S.con +cic:/Coq/Arith/Compare/lt_or_eq.con +cic:/Coq/Arith/Compare/Pcompare.con +cic:/Coq/Arith/Div2/div2.con +cic:/Coq/Arith/Div2/div2_even.con +cic:/Coq/Arith/Div2/div2_odd.con +cic:/Coq/Arith/Div2/double.con +cic:/Coq/Arith/Div2/double_even.con +cic:/Coq/Arith/Div2/double_odd.con +cic:/Coq/Arith/Div2/double_plus.con +cic:/Coq/Arith/Div2/double_S.con +cic:/Coq/Arith/Div2/even_2n.con +cic:/Coq/Arith/Div2/even_div2.con +cic:/Coq/Arith/Div2/even_double.con +cic:/Coq/Arith/Div2/even_odd_div2.con +cic:/Coq/Arith/Div2/even_odd_double.con +cic:/Coq/Arith/Div2/ind_0_1_SS.con +cic:/Coq/Arith/Div2/lt_div2.con +cic:/Coq/Arith/Div2/odd_div2.con +cic:/Coq/Arith/Div2/odd_double.con +cic:/Coq/Arith/Div2/odd_S2n.con +cic:/Coq/Arith/EqNat/beq_nat.con +cic:/Coq/Arith/EqNat/beq_nat_eq.con +cic:/Coq/Arith/EqNat/beq_nat_refl.con +cic:/Coq/Arith/EqNat/eq_eq_nat.con +cic:/Coq/Arith/EqNat/eq_nat.con +cic:/Coq/Arith/EqNat/eq_nat_decide.con +cic:/Coq/Arith/EqNat/eq_nat_elim.con +cic:/Coq/Arith/EqNat/eq_nat_eq.con +cic:/Coq/Arith/EqNat/eq_nat_refl.con +cic:/Coq/Arith/Euclid/diveucl.ind +cic:/Coq/Arith/Euclid/diveucl_ind.con +cic:/Coq/Arith/Euclid/diveucl_rec.con +cic:/Coq/Arith/Euclid/diveucl_rect.con +cic:/Coq/Arith/Euclid/eucl_dev.con +cic:/Coq/Arith/Euclid/modulo.con +cic:/Coq/Arith/Euclid/quotient.con +cic:/Coq/Arith/Even/even_even_plus.con +cic:/Coq/Arith/Even/even.ind +cic:/Coq/Arith/Even/even_ind.con +cic:/Coq/Arith/Even/even_mult_aux.con +cic:/Coq/Arith/Even/even_mult_inv_l.con +cic:/Coq/Arith/Even/even_mult_inv_r.con +cic:/Coq/Arith/Even/even_mult_l.con +cic:/Coq/Arith/Even/even_mult_r.con +cic:/Coq/Arith/Even/even_odd_dec.con +cic:/Coq/Arith/Even/even_or_odd.con +cic:/Coq/Arith/Even/even_plus_aux.con +cic:/Coq/Arith/Even/even_plus_even_inv_l.con +cic:/Coq/Arith/Even/even_plus_even_inv_r.con +cic:/Coq/Arith/Even/even_plus_odd_inv_l.con +cic:/Coq/Arith/Even/even_plus_odd_inv_r.con +cic:/Coq/Arith/Even/not_even_and_odd.con +cic:/Coq/Arith/Even/odd_even_plus.con +cic:/Coq/Arith/Even/odd_ind.con +cic:/Coq/Arith/Even/odd_mult.con +cic:/Coq/Arith/Even/odd_mult_inv_l.con +cic:/Coq/Arith/Even/odd_mult_inv_r.con +cic:/Coq/Arith/Even/odd_plus_even_inv_l.con +cic:/Coq/Arith/Even/odd_plus_even_inv_r.con +cic:/Coq/Arith/Even/odd_plus_l.con +cic:/Coq/Arith/Even/odd_plus_odd_inv_l.con +cic:/Coq/Arith/Even/odd_plus_odd_inv_r.con +cic:/Coq/Arith/Even/odd_plus_r.con +cic:/Coq/Arith/Factorial/fact.con +cic:/Coq/Arith/Factorial/fact_le.con +cic:/Coq/Arith/Factorial/fact_neq_0.con +cic:/Coq/Arith/Factorial/lt_O_fact.con +cic:/Coq/Arith/Gt/gt_asym.con +cic:/Coq/Arith/Gt/gt_irrefl.con +cic:/Coq/Arith/Gt/gt_le_S.con +cic:/Coq/Arith/Gt/gt_le_trans.con +cic:/Coq/Arith/Gt/gt_not_le.con +cic:/Coq/Arith/Gt/gt_n_S.con +cic:/Coq/Arith/Gt/gt_O_eq.con +cic:/Coq/Arith/Gt/gt_pred.con +cic:/Coq/Arith/Gt/gt_S.con +cic:/Coq/Arith/Gt/gt_S_le.con +cic:/Coq/Arith/Gt/gt_S_n.con +cic:/Coq/Arith/Gt/gt_Sn_n.con +cic:/Coq/Arith/Gt/gt_Sn_O.con +cic:/Coq/Arith/Gt/gt_trans.con +cic:/Coq/Arith/Gt/gt_trans_S.con +cic:/Coq/Arith/Gt/le_gt_S.con +cic:/Coq/Arith/Gt/le_gt_trans.con +cic:/Coq/Arith/Gt/le_not_gt.con +cic:/Coq/Arith/Gt/le_S_gt.con +cic:/Coq/Arith/Gt/plus_gt_compat_l.con +cic:/Coq/Arith/Gt/plus_gt_reg_l.con +cic:/Coq/Arith/Le/le_antisym.con +cic:/Coq/Arith/Le/le_elim_rel.con +cic:/Coq/Arith/Le/le_n_O_eq.con +cic:/Coq/Arith/Le/le_n_S.con +cic:/Coq/Arith/Le/le_n_Sn.con +cic:/Coq/Arith/Le/le_O_n.con +cic:/Coq/Arith/Le/le_pred.con +cic:/Coq/Arith/Le/le_pred_n.con +cic:/Coq/Arith/Le/le_refl.con +cic:/Coq/Arith/Le/le_S_n.con +cic:/Coq/Arith/Le/le_Sn_le.con +cic:/Coq/Arith/Le/le_Sn_n.con +cic:/Coq/Arith/Le/le_Sn_O.con +cic:/Coq/Arith/Le/le_trans.con +cic:/Coq/Arith/Lt/le_lt_n_Sm.con +cic:/Coq/Arith/Lt/le_lt_or_eq.con +cic:/Coq/Arith/Lt/le_lt_trans.con +cic:/Coq/Arith/Lt/le_not_lt.con +cic:/Coq/Arith/Lt/le_or_lt.con +cic:/Coq/Arith/Lt/lt_asym.con +cic:/Coq/Arith/Lt/lt_irrefl.con +cic:/Coq/Arith/Lt/lt_le_S.con +cic:/Coq/Arith/Lt/lt_le_trans.con +cic:/Coq/Arith/Lt/lt_le_weak.con +cic:/Coq/Arith/Lt/lt_n_O.con +cic:/Coq/Arith/Lt/lt_not_le.con +cic:/Coq/Arith/Lt/lt_n_S.con +cic:/Coq/Arith/Lt/lt_n_Sm_le.con +cic:/Coq/Arith/Lt/lt_n_Sn.con +cic:/Coq/Arith/Lt/lt_O_neq.con +cic:/Coq/Arith/Lt/lt_O_Sn.con +cic:/Coq/Arith/Lt/lt_pred.con +cic:/Coq/Arith/Lt/lt_pred_n_n.con +cic:/Coq/Arith/Lt/lt_S.con +cic:/Coq/Arith/Lt/lt_S_n.con +cic:/Coq/Arith/Lt/lt_trans.con +cic:/Coq/Arith/Lt/nat_total_order.con +cic:/Coq/Arith/Lt/neq_O_lt.con +cic:/Coq/Arith/Lt/S_pred.con +cic:/Coq/Arith/Max/le_max_l.con +cic:/Coq/Arith/Max/le_max_r.con +cic:/Coq/Arith/Max/max_case2.con +cic:/Coq/Arith/Max/max_case.con +cic:/Coq/Arith/Max/max_comm.con +cic:/Coq/Arith/Max/max.con +cic:/Coq/Arith/Max/max_dec.con +cic:/Coq/Arith/Max/max_l.con +cic:/Coq/Arith/Max/max_r.con +cic:/Coq/Arith/Max/max_SS.con +cic:/Coq/Arith/Min/le_min_l.con +cic:/Coq/Arith/Min/le_min_r.con +cic:/Coq/Arith/Min/min_case2.con +cic:/Coq/Arith/Min/min_case.con +cic:/Coq/Arith/Min/min_comm.con +cic:/Coq/Arith/Min/min.con +cic:/Coq/Arith/Min/min_dec.con +cic:/Coq/Arith/Min/min_l.con +cic:/Coq/Arith/Min/min_r.con +cic:/Coq/Arith/Min/min_SS.con +cic:/Coq/Arith/Minus/le_minus.con +cic:/Coq/Arith/Minus/le_plus_minus.con +cic:/Coq/Arith/Minus/le_plus_minus_r.con +cic:/Coq/Arith/Minus/lt_minus.con +cic:/Coq/Arith/Minus/lt_O_minus_lt.con +cic:/Coq/Arith/Minus/minus_n_n.con +cic:/Coq/Arith/Minus/minus_n_O.con +cic:/Coq/Arith/Minus/minus_plus.con +cic:/Coq/Arith/Minus/minus_plus_simpl_l_reverse.con +cic:/Coq/Arith/Minus/minus_Sn_m.con +cic:/Coq/Arith/Minus/not_le_minus_0.con +cic:/Coq/Arith/Minus/plus_minus.con +cic:/Coq/Arith/Minus/pred_of_minus.con +cic:/Coq/Arith/Mult/mult_0_l.con +cic:/Coq/Arith/Mult/mult_0_r.con +cic:/Coq/Arith/Mult/mult_1_l.con +cic:/Coq/Arith/Mult/mult_1_r.con +cic:/Coq/Arith/Mult/mult_acc_aux.con +cic:/Coq/Arith/Mult/mult_acc.con +cic:/Coq/Arith/Mult/mult_assoc.con +cic:/Coq/Arith/Mult/mult_assoc_reverse.con +cic:/Coq/Arith/Mult/mult_comm.con +cic:/Coq/Arith/Mult/mult_le_compat.con +cic:/Coq/Arith/Mult/mult_le_compat_l.con +cic:/Coq/Arith/Mult/mult_le_compat_r.con +cic:/Coq/Arith/Mult/mult_lt_compat_r.con +cic:/Coq/Arith/Mult/mult_minus_distr_r.con +cic:/Coq/Arith/Mult/mult_O_le.con +cic:/Coq/Arith/Mult/mult_plus_distr_l.con +cic:/Coq/Arith/Mult/mult_plus_distr_r.con +cic:/Coq/Arith/Mult/mult_S_le_reg_l.con +cic:/Coq/Arith/Mult/mult_S_lt_compat_l.con +cic:/Coq/Arith/Mult/mult_tail_mult.con +cic:/Coq/Arith/Mult/odd_even_lem.con +cic:/Coq/Arith/Mult/tail_mult.con +cic:/Coq/Arith/Peano_dec/dec_eq_nat.con +cic:/Coq/Arith/Peano_dec/eq_nat_dec.con +cic:/Coq/Arith/Peano_dec/O_or_S.con +cic:/Coq/Arith/Plus/le_plus_l.con +cic:/Coq/Arith/Plus/le_plus_r.con +cic:/Coq/Arith/Plus/le_plus_trans.con +cic:/Coq/Arith/Plus/lt_plus_trans.con +cic:/Coq/Arith/Plus/plus_0_l.con +cic:/Coq/Arith/Plus/plus_0_r.con +cic:/Coq/Arith/Plus/plus_acc.con +cic:/Coq/Arith/Plus/plus_assoc.con +cic:/Coq/Arith/Plus/plus_assoc_reverse.con +cic:/Coq/Arith/Plus/plus_comm.con +cic:/Coq/Arith/Plus/plus_is_O.con +cic:/Coq/Arith/Plus/plus_is_one.con +cic:/Coq/Arith/Plus/plus_le_compat.con +cic:/Coq/Arith/Plus/plus_le_compat_l.con +cic:/Coq/Arith/Plus/plus_le_compat_r.con +cic:/Coq/Arith/Plus/plus_le_lt_compat.con +cic:/Coq/Arith/Plus/plus_le_reg_l.con +cic:/Coq/Arith/Plus/plus_lt_compat.con +cic:/Coq/Arith/Plus/plus_lt_compat_l.con +cic:/Coq/Arith/Plus/plus_lt_compat_r.con +cic:/Coq/Arith/Plus/plus_lt_le_compat.con +cic:/Coq/Arith/Plus/plus_lt_reg_l.con +cic:/Coq/Arith/Plus/plus_permute_2_in_4.con +cic:/Coq/Arith/Plus/plus_permute.con +cic:/Coq/Arith/Plus/plus_reg_l.con +cic:/Coq/Arith/Plus/plus_Snm_nSm.con +cic:/Coq/Arith/Plus/plus_tail_plus.con +cic:/Coq/Arith/Plus/tail_plus.con +cic:/Coq/Arith/Wf_nat/acc_lt_rel.con +cic:/Coq/Arith/Wf_nat/gtof.con +cic:/Coq/Arith/Wf_nat/gt_wf_ind.con +cic:/Coq/Arith/Wf_nat/gt_wf_rec.con +cic:/Coq/Arith/Wf_nat/induction_gtof1.con +cic:/Coq/Arith/Wf_nat/induction_gtof2.con +cic:/Coq/Arith/Wf_nat/induction_ltof1.con +cic:/Coq/Arith/Wf_nat/induction_ltof2.con +cic:/Coq/Arith/Wf_nat/inv_lt_rel.con +cic:/Coq/Arith/Wf_nat/ltof.con +cic:/Coq/Arith/Wf_nat/lt_wf.con +cic:/Coq/Arith/Wf_nat/lt_wf_double_ind.con +cic:/Coq/Arith/Wf_nat/lt_wf_double_rec.con +cic:/Coq/Arith/Wf_nat/lt_wf_ind.con +cic:/Coq/Arith/Wf_nat/lt_wf_rec1.con +cic:/Coq/Arith/Wf_nat/lt_wf_rec.con +cic:/Coq/Arith/Wf_nat/well_founded_gtof.con +cic:/Coq/Arith/Wf_nat/well_founded_inv_lt_rel_compat.con +cic:/Coq/Arith/Wf_nat/well_founded_inv_rel_inv_lt_rel.con +cic:/Coq/Arith/Wf_nat/well_founded_lt_compat.con +cic:/Coq/Arith/Wf_nat/well_founded_ltof.con +cic:/Coq/Bool/Bool/absoption_andb.con +cic:/Coq/Bool/Bool/absoption_orb.con +cic:/Coq/Bool/Bool/andb_assoc.con +cic:/Coq/Bool/Bool/andb_b_false.con +cic:/Coq/Bool/Bool/andb_b_true.con +cic:/Coq/Bool/Bool/andb_comm.con +cic:/Coq/Bool/Bool/andb.con +cic:/Coq/Bool/Bool/andb_false_b.con +cic:/Coq/Bool/Bool/andb_false_elim.con +cic:/Coq/Bool/Bool/andb_false_intro1.con +cic:/Coq/Bool/Bool/andb_false_intro2.con +cic:/Coq/Bool/Bool/andb_neg_b.con +cic:/Coq/Bool/Bool/andb_prop2.con +cic:/Coq/Bool/Bool/andb_prop.con +cic:/Coq/Bool/Bool/andb_true_b.con +cic:/Coq/Bool/Bool/andb_true_eq.con +cic:/Coq/Bool/Bool/andb_true_intro2.con +cic:/Coq/Bool/Bool/andb_true_intro.con +cic:/Coq/Bool/Bool/bool_1.con +cic:/Coq/Bool/Bool/bool_2.con +cic:/Coq/Bool/Bool/bool_3.con +cic:/Coq/Bool/Bool/bool_4.con +cic:/Coq/Bool/Bool/bool_5.con +cic:/Coq/Bool/Bool/bool_6.con +cic:/Coq/Bool/Bool/demorgan1.con +cic:/Coq/Bool/Bool/demorgan2.con +cic:/Coq/Bool/Bool/demorgan3.con +cic:/Coq/Bool/Bool/demorgan4.con +cic:/Coq/Bool/Bool/diff_false_true.con +cic:/Coq/Bool/Bool/diff_true_false.con +cic:/Coq/Bool/Bool/eqb.con +cic:/Coq/Bool/Bool/eqb_eq.con +cic:/Coq/Bool/BoolEq/beq_eq_not_false.con +cic:/Coq/Bool/BoolEq/beq_eq_true.con +cic:/Coq/Bool/BoolEq/beq_false_not_eq.con +cic:/Coq/Bool/Bool/eqb_negb1.con +cic:/Coq/Bool/Bool/eqb_negb2.con +cic:/Coq/Bool/Bool/eqb_prop.con +cic:/Coq/Bool/Bool/eqb_refl.con +cic:/Coq/Bool/Bool/eqb_reflx.con +cic:/Coq/Bool/Bool/eqb_subst.con +cic:/Coq/Bool/BoolEq/eq_dec.con +cic:/Coq/Bool/BoolEq/exists_beq_eq.con +cic:/Coq/Bool/BoolEq/not_eq_false_beq.con +cic:/Coq/Bool/Bool/eq_true_false_abs.con +cic:/Coq/Bool/Bool/false_xorb.con +cic:/Coq/Bool/Bool/ifb.con +cic:/Coq/Bool/Bool/if_negb.con +cic:/Coq/Bool/Bool/implb.con +cic:/Coq/Bool/Bool/Is_true.con +cic:/Coq/Bool/Bool/Is_true_eq_left.con +cic:/Coq/Bool/Bool/Is_true_eq_right.con +cic:/Coq/Bool/Bool/Is_true_eq_true2.con +cic:/Coq/Bool/Bool/Is_true_eq_true.con +cic:/Coq/Bool/Bool/leb.con +cic:/Coq/Bool/Bool/negb_andb.con +cic:/Coq/Bool/Bool/negb.con +cic:/Coq/Bool/Bool/negb_elim.con +cic:/Coq/Bool/Bool/negb_intro.con +cic:/Coq/Bool/Bool/negb_orb.con +cic:/Coq/Bool/Bool/negb_sym.con +cic:/Coq/Bool/Bool/no_fixpoint_negb.con +cic:/Coq/Bool/Bool/not_false_is_true.con +cic:/Coq/Bool/Bool/not_true_is_false.con +cic:/Coq/Bool/Bool/orb_assoc.con +cic:/Coq/Bool/Bool/orb_b_false.con +cic:/Coq/Bool/Bool/orb_b_true.con +cic:/Coq/Bool/Bool/orb_comm.con +cic:/Coq/Bool/Bool/orb.con +cic:/Coq/Bool/Bool/orb_false_b.con +cic:/Coq/Bool/Bool/orb_false_elim.con +cic:/Coq/Bool/Bool/orb_false_intro.con +cic:/Coq/Bool/Bool/orb_neg_b.con +cic:/Coq/Bool/Bool/orb_prop2.con +cic:/Coq/Bool/Bool/orb_prop.con +cic:/Coq/Bool/Bool/orb_true_b.con +cic:/Coq/Bool/Bool/orb_true_elim.con +cic:/Coq/Bool/Bool/orb_true_intro.con +cic:/Coq/Bool/Bool/true_xorb.con +cic:/Coq/Bool/Bool/xorb_assoc.con +cic:/Coq/Bool/Bool/xorb_comm.con +cic:/Coq/Bool/Bool/xorb.con +cic:/Coq/Bool/Bool/xorb_eq.con +cic:/Coq/Bool/Bool/xorb_false.con +cic:/Coq/Bool/Bool/xorb_move_l_r_1.con +cic:/Coq/Bool/Bool/xorb_move_l_r_2.con +cic:/Coq/Bool/Bool/xorb_move_r_l_1.con +cic:/Coq/Bool/Bool/xorb_move_r_l_2.con +cic:/Coq/Bool/Bool/xorb_nilpotent.con +cic:/Coq/Bool/Bool/xorb_true.con +cic:/Coq/Bool/Bvector/Bcons.con +cic:/Coq/Bool/Bvector/Bhigh.con +cic:/Coq/Bool/Bvector/Blow.con +cic:/Coq/Bool/Bvector/Bneg.con +cic:/Coq/Bool/Bvector/Bnil.con +cic:/Coq/Bool/Bvector/BshiftL.con +cic:/Coq/Bool/Bvector/BshiftL_iter.con +cic:/Coq/Bool/Bvector/BshiftRa.con +cic:/Coq/Bool/Bvector/BshiftRa_iter.con +cic:/Coq/Bool/Bvector/BshiftRl.con +cic:/Coq/Bool/Bvector/BshiftRl_iter.con +cic:/Coq/Bool/Bvector/Bsign.con +cic:/Coq/Bool/Bvector/BVand.con +cic:/Coq/Bool/Bvector/Bvect_false.con +cic:/Coq/Bool/Bvector/Bvector.con +cic:/Coq/Bool/Bvector/Bvect_true.con +cic:/Coq/Bool/Bvector/BVor.con +cic:/Coq/Bool/Bvector/BVxor.con +cic:/Coq/Bool/Bvector/Vbinary.con +cic:/Coq/Bool/Bvector/Vconst.con +cic:/Coq/Bool/Bvector/vector.ind +cic:/Coq/Bool/Bvector/vector_ind.con +cic:/Coq/Bool/Bvector/vector_rec.con +cic:/Coq/Bool/Bvector/vector_rect.con +cic:/Coq/Bool/Bvector/Vextend.con +cic:/Coq/Bool/Bvector/Vhead.con +cic:/Coq/Bool/Bvector/Vlast.con +cic:/Coq/Bool/Bvector/Vshiftin.con +cic:/Coq/Bool/Bvector/Vshiftout.con +cic:/Coq/Bool/Bvector/Vshiftrepeat.con +cic:/Coq/Bool/Bvector/Vtail.con +cic:/Coq/Bool/Bvector/Vtrunc.con +cic:/Coq/Bool/Bvector/Vunary.con +cic:/Coq/Bool/DecBool/ifdec.con +cic:/Coq/Bool/DecBool/ifdec_left.con +cic:/Coq/Bool/DecBool/ifdec_right.con +cic:/Coq/Bool/IfProp/Iffalse_inv.con +cic:/Coq/Bool/IfProp/IfProp_false.con +cic:/Coq/Bool/IfProp/IfProp.ind +cic:/Coq/Bool/IfProp/IfProp_ind.con +cic:/Coq/Bool/IfProp/IfProp_or.con +cic:/Coq/Bool/IfProp/IfProp_sum.con +cic:/Coq/Bool/IfProp/IfProp_true.con +cic:/Coq/Bool/IfProp/Iftrue_inv.con +cic:/Coq/Bool/Sumbool/bool_eq_ind.con +cic:/Coq/Bool/Sumbool/bool_eq_rec.con +cic:/Coq/Bool/Sumbool/bool_of_sumbool.con +cic:/Coq/Bool/Sumbool/sumbool_and.con +cic:/Coq/Bool/Sumbool/sumbool_not.con +cic:/Coq/Bool/Sumbool/sumbool_of_bool.con +cic:/Coq/Bool/Sumbool/sumbool_or.con +cic:/Coq/Bool/Zerob/zerob.con +cic:/Coq/Bool/Zerob/zerob_false_elim.con +cic:/Coq/Bool/Zerob/zerob_false_intro.con +cic:/Coq/Bool/Zerob/zerob_true_elim.con +cic:/Coq/Bool/Zerob/zerob_true_intro.con +cic:/Coq/field/Field_Compl/appT.con +cic:/Coq/field/Field_Compl/assoc_2nd.con +cic:/Coq/field/Field_Compl/field_rel_option.ind +cic:/Coq/field/Field_Compl/field_rel_option_ind.con +cic:/Coq/field/Field_Compl/field_rel_option_rec.con +cic:/Coq/field/Field_Compl/field_rel_option_rect.con +cic:/Coq/field/Field_Compl/fstT.con +cic:/Coq/field/Field_Compl/listT.ind +cic:/Coq/field/Field_Compl/listT_ind.con +cic:/Coq/field/Field_Compl/listT_rec.con +cic:/Coq/field/Field_Compl/listT_rect.con +cic:/Coq/field/Field_Compl/mem.con +cic:/Coq/field/Field_Compl/prodT.ind +cic:/Coq/field/Field_Compl/prodT_ind.con +cic:/Coq/field/Field_Compl/prodT_rec.con +cic:/Coq/field/Field_Compl/prodT_rect.con +cic:/Coq/field/Field_Compl/sndT.con +cic:/Coq/field/Field_Theory/A.con +cic:/Coq/field/Field_Theory/Adiv.con +cic:/Coq/field/Field_Theory/Aeq.con +cic:/Coq/field/Field_Theory/Ainv.con +cic:/Coq/field/Field_Theory/AinvT_r.con +cic:/Coq/field/Field_Theory/Aminus.con +cic:/Coq/field/Field_Theory/Amult.con +cic:/Coq/field/Field_Theory/AmultT_1l.con +cic:/Coq/field/Field_Theory/AmultT_1r.con +cic:/Coq/field/Field_Theory/AmultT_AplusT_distr.con +cic:/Coq/field/Field_Theory/AmultT_assoc.con +cic:/Coq/field/Field_Theory/AmultT_Ol.con +cic:/Coq/field/Field_Theory/AmultT_Or.con +cic:/Coq/field/Field_Theory/AmultT_sym.con +cic:/Coq/field/Field_Theory/Aone.con +cic:/Coq/field/Field_Theory/Aopp.con +cic:/Coq/field/Field_Theory/Aplus.con +cic:/Coq/field/Field_Theory/AplusT_AoppT_r.con +cic:/Coq/field/Field_Theory/AplusT_assoc.con +cic:/Coq/field/Field_Theory/AplusT_Ol.con +cic:/Coq/field/Field_Theory/AplusT_sym.con +cic:/Coq/field/Field_Theory/assoc.con +cic:/Coq/field/Field_Theory/assoc_correct.con +cic:/Coq/field/Field_Theory/assoc_mult.con +cic:/Coq/field/Field_Theory/assoc_mult_correct1.con +cic:/Coq/field/Field_Theory/assoc_mult_correct.con +cic:/Coq/field/Field_Theory/assoc_plus_correct.con +cic:/Coq/field/Field_Theory/Azero.con +cic:/Coq/field/Field_Theory/distrib.con +cic:/Coq/field/Field_Theory/distrib_correct.con +cic:/Coq/field/Field_Theory/distrib_EAopp.con +cic:/Coq/field/Field_Theory/distrib_main.con +cic:/Coq/field/Field_Theory/distrib_mult_left.con +cic:/Coq/field/Field_Theory/distrib_mult_left_correct.con +cic:/Coq/field/Field_Theory/distrib_mult_right.con +cic:/Coq/field/Field_Theory/distrib_mult_right_correct.con +cic:/Coq/field/Field_Theory/eqExprA.con +cic:/Coq/field/Field_Theory/eqExprA_O.con +cic:/Coq/field/Field_Theory/eq_nat_dec.con +cic:/Coq/field/Field_Theory/ExprA.ind +cic:/Coq/field/Field_Theory/ExprA_ind.con +cic:/Coq/field/Field_Theory/ExprA_rec.con +cic:/Coq/field/Field_Theory/ExprA_rect.con +cic:/Coq/field/Field_Theory/Field_Theory.ind +cic:/Coq/field/Field_Theory/Field_Theory_ind.con +cic:/Coq/field/Field_Theory/Field_Theory_rec.con +cic:/Coq/field/Field_Theory/Field_Theory_rect.con +cic:/Coq/field/Field_Theory/interp_ExprA.con +cic:/Coq/field/Field_Theory/inverse_correct.con +cic:/Coq/field/Field_Theory/inverse_simplif.con +cic:/Coq/field/Field_Theory/merge_mult.con +cic:/Coq/field/Field_Theory/merge_mult_correct1.con +cic:/Coq/field/Field_Theory/merge_mult_correct.con +cic:/Coq/field/Field_Theory/merge_plus.con +cic:/Coq/field/Field_Theory/merge_plus_correct1.con +cic:/Coq/field/Field_Theory/merge_plus_correct.con +cic:/Coq/field/Field_Theory/monom_remove.con +cic:/Coq/field/Field_Theory/monom_remove_correct.con +cic:/Coq/field/Field_Theory/monom_simplif.con +cic:/Coq/field/Field_Theory/monom_simplif_correct.con +cic:/Coq/field/Field_Theory/monom_simplif_rem.con +cic:/Coq/field/Field_Theory/monom_simplif_rem_correct.con +cic:/Coq/field/Field_Theory/mult_eq.con +cic:/Coq/field/Field_Theory/multiply_aux.con +cic:/Coq/field/Field_Theory/multiply_aux_correct.con +cic:/Coq/field/Field_Theory/multiply.con +cic:/Coq/field/Field_Theory/multiply_correct.con +cic:/Coq/field/Field_Theory/mult_of_list.con +cic:/Coq/field/Field_Theory/r_AmultT_mult.con +cic:/Coq/field/Field_Theory/r_AplusT_plus.con +cic:/Coq/field/Field_Theory/Rmult_neq_0_reg.con +cic:/Coq/field/Field_Theory/RT.con +cic:/Coq/field/Field_Theory/Th_inv_def.con +cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con +cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con +cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con +cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con +cic:/Coq/fourier/Fourier_util/Rfourier_le.con +cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con +cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con +cic:/Coq/fourier/Fourier_util/Rfourier_lt.con +cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con +cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con +cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con +cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con +cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con +cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con +cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con +cic:/Coq/fourier/Fourier_util/Rle_not_lt.con +cic:/Coq/fourier/Fourier_util/Rle_zero_1.con +cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con +cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con +cic:/Coq/fourier/Fourier_util/Rlt_not_le.con +cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con +cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con +cic:/Coq/fourier/Fourier_util/Rnot_le_le.con +cic:/Coq/fourier/Fourier_util/Rnot_lt0.con +cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con +cic:/Coq/Init/Datatypes/bool.ind +cic:/Coq/Init/Datatypes/bool_ind.con +cic:/Coq/Init/Datatypes/bool_rec.con +cic:/Coq/Init/Datatypes/bool_rect.con +cic:/Coq/Init/Datatypes/comparison.ind +cic:/Coq/Init/Datatypes/comparison_ind.con +cic:/Coq/Init/Datatypes/comparison_rec.con +cic:/Coq/Init/Datatypes/comparison_rect.con +cic:/Coq/Init/Datatypes/CompOpp.con +cic:/Coq/Init/Datatypes/Empty_set.ind +cic:/Coq/Init/Datatypes/Empty_set_ind.con +cic:/Coq/Init/Datatypes/Empty_set_rec.con +cic:/Coq/Init/Datatypes/Empty_set_rect.con +cic:/Coq/Init/Datatypes/fst.con +cic:/Coq/Init/Datatypes/identity.ind +cic:/Coq/Init/Datatypes/identity_ind.con +cic:/Coq/Init/Datatypes/identity_rec.con +cic:/Coq/Init/Datatypes/identity_rect.con +cic:/Coq/Init/Datatypes/injective_projections.con +cic:/Coq/Init/Datatypes/nat.ind +cic:/Coq/Init/Datatypes/nat_ind.con +cic:/Coq/Init/Datatypes/nat_rec.con +cic:/Coq/Init/Datatypes/nat_rect.con +cic:/Coq/Init/Datatypes/option.ind +cic:/Coq/Init/Datatypes/option_ind.con +cic:/Coq/Init/Datatypes/option_rec.con +cic:/Coq/Init/Datatypes/option_rect.con +cic:/Coq/Init/Datatypes/prod.ind +cic:/Coq/Init/Datatypes/prod_ind.con +cic:/Coq/Init/Datatypes/prod_rec.con +cic:/Coq/Init/Datatypes/prod_rect.con +cic:/Coq/Init/Datatypes/snd.con +cic:/Coq/Init/Datatypes/sum.ind +cic:/Coq/Init/Datatypes/sum_ind.con +cic:/Coq/Init/Datatypes/sum_rec.con +cic:/Coq/Init/Datatypes/sum_rect.con +cic:/Coq/Init/Datatypes/surjective_pairing.con +cic:/Coq/Init/Datatypes/unit.ind +cic:/Coq/Init/Datatypes/unit_ind.con +cic:/Coq/Init/Datatypes/unit_rec.con +cic:/Coq/Init/Datatypes/unit_rect.con +cic:/Coq/Init/Logic/absurd.con +cic:/Coq/Init/Logic/all.con +cic:/Coq/Init/Logic/and.ind +cic:/Coq/Init/Logic/and_ind.con +cic:/Coq/Init/Logic/and_rec.con +cic:/Coq/Init/Logic/and_rect.con +cic:/Coq/Init/Logic/eq.ind +cic:/Coq/Init/Logic/eq_ind.con +cic:/Coq/Init/Logic/eq_ind_r.con +cic:/Coq/Init/Logic/eq_rec.con +cic:/Coq/Init/Logic/eq_rec_r.con +cic:/Coq/Init/Logic/eq_rect.con +cic:/Coq/Init/Logic/eq_rect_r.con +cic:/Coq/Init/Logic/ex2.ind +cic:/Coq/Init/Logic/ex2_ind.con +cic:/Coq/Init/Logic/ex.ind +cic:/Coq/Init/Logic/ex_ind.con +cic:/Coq/Init/Logic/False.ind +cic:/Coq/Init/Logic/False_ind.con +cic:/Coq/Init/Logic/False_rec.con +cic:/Coq/Init/Logic/False_rect.con +cic:/Coq/Init/Logic/f_equal2.con +cic:/Coq/Init/Logic/f_equal3.con +cic:/Coq/Init/Logic/f_equal4.con +cic:/Coq/Init/Logic/f_equal5.con +cic:/Coq/Init/Logic/f_equal.con +cic:/Coq/Init/Logic/gen.con +cic:/Coq/Init/Logic/iff.con +cic:/Coq/Init/Logic/iff_refl.con +cic:/Coq/Init/Logic/iff_sym.con +cic:/Coq/Init/Logic/iff_trans.con +cic:/Coq/Init/Logic/IF_then_else.con +cic:/Coq/Init/Logic/inst.con +cic:/Coq/Init/Logic/not.con +cic:/Coq/Init/Logic/or.ind +cic:/Coq/Init/Logic/or_ind.con +cic:/Coq/Init/Logic/proj1.con +cic:/Coq/Init/Logic/proj2.con +cic:/Coq/Init/Logic/sym_eq.con +cic:/Coq/Init/Logic/sym_equal.con +cic:/Coq/Init/Logic/sym_not_eq.con +cic:/Coq/Init/Logic/sym_not_equal.con +cic:/Coq/Init/Logic/trans_eq.con +cic:/Coq/Init/Logic/trans_equal.con +cic:/Coq/Init/Logic/True.ind +cic:/Coq/Init/Logic/True_ind.con +cic:/Coq/Init/Logic/True_rec.con +cic:/Coq/Init/Logic/True_rect.con +cic:/Coq/Init/Logic_Type/congr_id.con +cic:/Coq/Init/Logic_Type/fstT.con +cic:/Coq/Init/Logic_Type/identity_ind_r.con +cic:/Coq/Init/Logic_Type/identity_rec_r.con +cic:/Coq/Init/Logic_Type/identity_rect_r.con +cic:/Coq/Init/Logic_Type/notT.con +cic:/Coq/Init/Logic_Type/prodT_curry.con +cic:/Coq/Init/Logic_Type/prodT.ind +cic:/Coq/Init/Logic_Type/prodT_ind.con +cic:/Coq/Init/Logic_Type/prodT_rec.con +cic:/Coq/Init/Logic_Type/prodT_rect.con +cic:/Coq/Init/Logic_Type/prodT_uncurry.con +cic:/Coq/Init/Logic_Type/sndT.con +cic:/Coq/Init/Logic_Type/sym_id.con +cic:/Coq/Init/Logic_Type/sym_not_id.con +cic:/Coq/Init/Logic_Type/trans_id.con +cic:/Coq/Init/Peano/eq_add_S.con +cic:/Coq/Init/Peano/eq_S.con +cic:/Coq/Init/Peano/ge.con +cic:/Coq/Init/Peano/gt.con +cic:/Coq/Init/Peano/IsSucc.con +cic:/Coq/Init/Peano/le.ind +cic:/Coq/Init/Peano/le_ind.con +cic:/Coq/Init/Peano/lt.con +cic:/Coq/Init/Peano/minus.con +cic:/Coq/Init/Peano/mult.con +cic:/Coq/Init/Peano/mult_n_O.con +cic:/Coq/Init/Peano/mult_n_Sm.con +cic:/Coq/Init/Peano/nat_case.con +cic:/Coq/Init/Peano/nat_double_ind.con +cic:/Coq/Init/Peano/not_eq_S.con +cic:/Coq/Init/Peano/n_Sn.con +cic:/Coq/Init/Peano/O_S.con +cic:/Coq/Init/Peano/plus.con +cic:/Coq/Init/Peano/plus_n_O.con +cic:/Coq/Init/Peano/plus_n_Sm.con +cic:/Coq/Init/Peano/plus_O_n.con +cic:/Coq/Init/Peano/plus_Sn_m.con +cic:/Coq/Init/Peano/pred.con +cic:/Coq/Init/Peano/pred_Sn.con +cic:/Coq/Init/Specif/absurd_set.con +cic:/Coq/Init/Specif/bool_choice.con +cic:/Coq/Init/Specif/Choice2.con +cic:/Coq/Init/Specif/Choice.con +cic:/Coq/Init/Specif/error.con +cic:/Coq/Init/Specif/Exc.con +cic:/Coq/Init/Specif/except.con +cic:/Coq/Init/Specif/proj1_sig.con +cic:/Coq/Init/Specif/proj2_sig.con +cic:/Coq/Init/Specif/projS1.con +cic:/Coq/Init/Specif/projS2.con +cic:/Coq/Init/Specif/projT1.con +cic:/Coq/Init/Specif/projT2.con +cic:/Coq/Init/Specif/sig2.ind +cic:/Coq/Init/Specif/sig2_ind.con +cic:/Coq/Init/Specif/sig2_rec.con +cic:/Coq/Init/Specif/sig2_rect.con +cic:/Coq/Init/Specif/sig.ind +cic:/Coq/Init/Specif/sig_ind.con +cic:/Coq/Init/Specif/sig_rec.con +cic:/Coq/Init/Specif/sig_rect.con +cic:/Coq/Init/Specif/sigS2.ind +cic:/Coq/Init/Specif/sigS2_ind.con +cic:/Coq/Init/Specif/sigS2_rec.con +cic:/Coq/Init/Specif/sigS2_rect.con +cic:/Coq/Init/Specif/sigS.ind +cic:/Coq/Init/Specif/sigS_ind.con +cic:/Coq/Init/Specif/sigS_rec.con +cic:/Coq/Init/Specif/sigS_rect.con +cic:/Coq/Init/Specif/sigT.ind +cic:/Coq/Init/Specif/sigT_ind.con +cic:/Coq/Init/Specif/sigT_rec.con +cic:/Coq/Init/Specif/sigT_rect.con +cic:/Coq/Init/Specif/sumbool.ind +cic:/Coq/Init/Specif/sumbool_ind.con +cic:/Coq/Init/Specif/sumbool_rec.con +cic:/Coq/Init/Specif/sumbool_rect.con +cic:/Coq/Init/Specif/sumor.ind +cic:/Coq/Init/Specif/sumor_ind.con +cic:/Coq/Init/Specif/sumor_rec.con +cic:/Coq/Init/Specif/sumor_rect.con +cic:/Coq/Init/Specif/value.con +cic:/Coq/Init/Wf/Acc.ind +cic:/Coq/Init/Wf/Acc_ind.con +cic:/Coq/Init/Wf/Acc_inv.con +cic:/Coq/Init/Wf/Acc_inv_dep.con +cic:/Coq/Init/Wf/Acc_iter_2.con +cic:/Coq/Init/Wf/Acc_iter.con +cic:/Coq/Init/Wf/Acc_rec.con +cic:/Coq/Init/Wf/Acc_rect.con +cic:/Coq/Init/Wf/Fix.con +cic:/Coq/Init/Wf/Fix_eq.con +cic:/Coq/Init/Wf/Fix_F.con +cic:/Coq/Init/Wf/Fix_F_eq.con +cic:/Coq/Init/Wf/Fix_F_inv.con +cic:/Coq/Init/Wf/well_founded.con +cic:/Coq/Init/Wf/well_founded_ind.con +cic:/Coq/Init/Wf/well_founded_induction.con +cic:/Coq/Init/Wf/well_founded_induction_type_2.con +cic:/Coq/Init/Wf/well_founded_induction_type.con +cic:/Coq/IntMap/Adalloc/ad_alloc_opt_allocates_1.con +cic:/Coq/IntMap/Adalloc/ad_alloc_opt_allocates.con +cic:/Coq/IntMap/Adalloc/ad_alloc_opt.con +cic:/Coq/IntMap/Adalloc/ad_alloc_opt_optimal_1.con +cic:/Coq/IntMap/Adalloc/ad_alloc_opt_optimal.con +cic:/Coq/IntMap/Adalloc/ad_le_antisym.con +cic:/Coq/IntMap/Adalloc/ad_le.con +cic:/Coq/IntMap/Adalloc/ad_le_double_mono.con +cic:/Coq/IntMap/Adalloc/ad_le_double_mono_conv.con +cic:/Coq/IntMap/Adalloc/ad_le_double_plus_un_mono.con +cic:/Coq/IntMap/Adalloc/ad_le_double_plus_un_mono_conv.con +cic:/Coq/IntMap/Adalloc/ad_le_lt_trans.con +cic:/Coq/IntMap/Adalloc/ad_le_refl.con +cic:/Coq/IntMap/Adalloc/ad_le_trans.con +cic:/Coq/IntMap/Adalloc/ad_lt_double_mono.con +cic:/Coq/IntMap/Adalloc/ad_lt_double_mono_conv.con +cic:/Coq/IntMap/Adalloc/ad_lt_double_plus_un_mono.con +cic:/Coq/IntMap/Adalloc/ad_lt_double_plus_un_mono_conv.con +cic:/Coq/IntMap/Adalloc/ad_lt_le_trans.con +cic:/Coq/IntMap/Adalloc/ad_lt_le_weak.con +cic:/Coq/IntMap/Adalloc/ad_lt_trans.con +cic:/Coq/IntMap/Adalloc/ad_min_choice.con +cic:/Coq/IntMap/Adalloc/ad_min.con +cic:/Coq/IntMap/Adalloc/ad_min_le_1.con +cic:/Coq/IntMap/Adalloc/ad_min_le_2.con +cic:/Coq/IntMap/Adalloc/ad_min_le_3.con +cic:/Coq/IntMap/Adalloc/ad_min_le_4.con +cic:/Coq/IntMap/Adalloc/ad_min_le_5.con +cic:/Coq/IntMap/Adalloc/ad_min_lt_3.con +cic:/Coq/IntMap/Adalloc/ad_min_lt_4.con +cic:/Coq/IntMap/Adalloc/ad_of_nat.con +cic:/Coq/IntMap/Adalloc/ad_of_nat_of_ad.con +cic:/Coq/IntMap/Adalloc/nat_le_complete.con +cic:/Coq/IntMap/Adalloc/nat_le_complete_conv.con +cic:/Coq/IntMap/Adalloc/nat_le.con +cic:/Coq/IntMap/Adalloc/nat_le_correct.con +cic:/Coq/IntMap/Adalloc/nat_le_correct_conv.con +cic:/Coq/IntMap/Adalloc/nat_of_ad.con +cic:/Coq/IntMap/Adalloc/nat_of_ad_double.con +cic:/Coq/IntMap/Adalloc/nat_of_ad_double_plus_un.con +cic:/Coq/IntMap/Adalloc/nat_of_ad_of_nat.con +cic:/Coq/IntMap/Addec/ad_bit_0_0_not_double_plus_un.con +cic:/Coq/IntMap/Addec/ad_bit_0_1_not_double.con +cic:/Coq/IntMap/Addec/ad_bit_0_neq.con +cic:/Coq/IntMap/Addec/ad_div_bit_eq.con +cic:/Coq/IntMap/Addec/ad_div_bit_neq.con +cic:/Coq/IntMap/Addec/ad_div_eq.con +cic:/Coq/IntMap/Addec/ad_div_neq.con +cic:/Coq/IntMap/Addec/ad_double_or_double_plus_un.con +cic:/Coq/IntMap/Addec/ad_eq_1.con +cic:/Coq/IntMap/Addec/ad_eq_comm.con +cic:/Coq/IntMap/Addec/ad_eq_complete.con +cic:/Coq/IntMap/Addec/ad_eq.con +cic:/Coq/IntMap/Addec/ad_eq_correct.con +cic:/Coq/IntMap/Addec/ad_neq.con +cic:/Coq/IntMap/Addec/ad_not_div_2_not_double.con +cic:/Coq/IntMap/Addec/ad_not_div_2_not_double_plus_un.con +cic:/Coq/IntMap/Addec/ad_xor_eq_false.con +cic:/Coq/IntMap/Addec/ad_xor_eq_true.con +cic:/Coq/IntMap/Addr/ad_bit_0.con +cic:/Coq/IntMap/Addr/ad_bit_0_correct.con +cic:/Coq/IntMap/Addr/ad_bit_1.con +cic:/Coq/IntMap/Addr/ad_bit.con +cic:/Coq/IntMap/Addr/ad_div_2.con +cic:/Coq/IntMap/Addr/ad_div_2_correct.con +cic:/Coq/IntMap/Addr/ad_div_2_double.con +cic:/Coq/IntMap/Addr/ad_div_2_double_plus_un.con +cic:/Coq/IntMap/Addr/ad_double_bit_0.con +cic:/Coq/IntMap/Addr/ad_double.con +cic:/Coq/IntMap/Addr/ad_double_div_2.con +cic:/Coq/IntMap/Addr/ad_double_inj.con +cic:/Coq/IntMap/Addr/ad_double_plus_un_bit_0.con +cic:/Coq/IntMap/Addr/ad_double_plus_un.con +cic:/Coq/IntMap/Addr/ad_double_plus_un_div_2.con +cic:/Coq/IntMap/Addr/ad_double_plus_un_inj.con +cic:/Coq/IntMap/Addr/ad_faithful_1.con +cic:/Coq/IntMap/Addr/ad_faithful_2.con +cic:/Coq/IntMap/Addr/ad_faithful_3.con +cic:/Coq/IntMap/Addr/ad_faithful_4.con +cic:/Coq/IntMap/Addr/ad_faithful.con +cic:/Coq/IntMap/Addr/adf_xor_assoc.con +cic:/Coq/IntMap/Addr/adf_xor.con +cic:/Coq/IntMap/Addr/adf_xor_eq.con +cic:/Coq/IntMap/Addr/ad.ind +cic:/Coq/IntMap/Addr/ad_ind.con +cic:/Coq/IntMap/Addr/ad_neg_bit_0_1.con +cic:/Coq/IntMap/Addr/ad_neg_bit_0_2.con +cic:/Coq/IntMap/Addr/ad_neg_bit_0.con +cic:/Coq/IntMap/Addr/ad_rec.con +cic:/Coq/IntMap/Addr/ad_rect.con +cic:/Coq/IntMap/Addr/ad_same_bit_0.con +cic:/Coq/IntMap/Addr/ad_sum.con +cic:/Coq/IntMap/Addr/ad_xor_assoc.con +cic:/Coq/IntMap/Addr/ad_xor_bit_0.con +cic:/Coq/IntMap/Addr/ad_xor_comm.con +cic:/Coq/IntMap/Addr/ad_xor.con +cic:/Coq/IntMap/Addr/ad_xor_div_2.con +cic:/Coq/IntMap/Addr/ad_xor_eq.con +cic:/Coq/IntMap/Addr/ad_xor_neutral_left.con +cic:/Coq/IntMap/Addr/ad_xor_neutral_right.con +cic:/Coq/IntMap/Addr/ad_xor_nilpotent.con +cic:/Coq/IntMap/Addr/ad_xor_sem_1.con +cic:/Coq/IntMap/Addr/ad_xor_sem_2.con +cic:/Coq/IntMap/Addr/ad_xor_sem_3.con +cic:/Coq/IntMap/Addr/ad_xor_sem_4.con +cic:/Coq/IntMap/Addr/ad_xor_sem_5.con +cic:/Coq/IntMap/Addr/ad_xor_sem_6.con +cic:/Coq/IntMap/Addr/ad_xor_semantics.con +cic:/Coq/IntMap/Addr/eqf.con +cic:/Coq/IntMap/Addr/eqf_refl.con +cic:/Coq/IntMap/Addr/eqf_sym.con +cic:/Coq/IntMap/Addr/eqf_trans.con +cic:/Coq/IntMap/Addr/eqf_xor_1.con +cic:/Coq/IntMap/Addr/p_xor.con +cic:/Coq/IntMap/Adist/ad_pdist_comm.con +cic:/Coq/IntMap/Adist/ad_pdist.con +cic:/Coq/IntMap/Adist/ad_pdist_eq_1.con +cic:/Coq/IntMap/Adist/ad_pdist_eq_2.con +cic:/Coq/IntMap/Adist/ad_pdist_ultra.con +cic:/Coq/IntMap/Adist/ad_plength_1.con +cic:/Coq/IntMap/Adist/ad_plength.con +cic:/Coq/IntMap/Adist/ad_plength_first_one.con +cic:/Coq/IntMap/Adist/ad_plength_infty.con +cic:/Coq/IntMap/Adist/ad_plength_lb.con +cic:/Coq/IntMap/Adist/ad_plength_one.con +cic:/Coq/IntMap/Adist/ad_plength_ub.con +cic:/Coq/IntMap/Adist/ad_plength_ultra_1.con +cic:/Coq/IntMap/Adist/ad_plength_ultra.con +cic:/Coq/IntMap/Adist/ad_plength_zeros.con +cic:/Coq/IntMap/Adist/le_ni_le.con +cic:/Coq/IntMap/Adist/natinf.ind +cic:/Coq/IntMap/Adist/natinf_ind.con +cic:/Coq/IntMap/Adist/natinf_rec.con +cic:/Coq/IntMap/Adist/natinf_rect.con +cic:/Coq/IntMap/Adist/ni_le_antisym.con +cic:/Coq/IntMap/Adist/ni_le.con +cic:/Coq/IntMap/Adist/ni_le_le.con +cic:/Coq/IntMap/Adist/ni_le_min_1.con +cic:/Coq/IntMap/Adist/ni_le_min_2.con +cic:/Coq/IntMap/Adist/ni_le_min_induc.con +cic:/Coq/IntMap/Adist/ni_le_refl.con +cic:/Coq/IntMap/Adist/ni_le_total.con +cic:/Coq/IntMap/Adist/ni_le_trans.con +cic:/Coq/IntMap/Adist/ni_min_assoc.con +cic:/Coq/IntMap/Adist/ni_min_case.con +cic:/Coq/IntMap/Adist/ni_min_comm.con +cic:/Coq/IntMap/Adist/ni_min.con +cic:/Coq/IntMap/Adist/ni_min_idemp.con +cic:/Coq/IntMap/Adist/ni_min_inf_l.con +cic:/Coq/IntMap/Adist/ni_min_inf_r.con +cic:/Coq/IntMap/Adist/ni_min_O_l.con +cic:/Coq/IntMap/Adist/ni_min_O_r.con +cic:/Coq/IntMap/Fset/FSet.con +cic:/Coq/IntMap/Fset/FSetDelta.con +cic:/Coq/IntMap/Fset/FSetDiff.con +cic:/Coq/IntMap/Fset/FSet_Dom.con +cic:/Coq/IntMap/Fset/FSetInter.con +cic:/Coq/IntMap/Fset/FSetUnion.con +cic:/Coq/IntMap/Fset/in_dom.con +cic:/Coq/IntMap/Fset/in_dom_delta.con +cic:/Coq/IntMap/Fset/in_dom_M0.con +cic:/Coq/IntMap/Fset/in_dom_M1_1.con +cic:/Coq/IntMap/Fset/in_dom_M1_2.con +cic:/Coq/IntMap/Fset/in_dom_M1.con +cic:/Coq/IntMap/Fset/in_dom_merge.con +cic:/Coq/IntMap/Fset/in_dom_none.con +cic:/Coq/IntMap/Fset/in_dom_put_behind.con +cic:/Coq/IntMap/Fset/in_dom_put.con +cic:/Coq/IntMap/Fset/in_dom_remove.con +cic:/Coq/IntMap/Fset/in_dom_restrby.con +cic:/Coq/IntMap/Fset/in_dom_restrto.con +cic:/Coq/IntMap/Fset/in_dom_some.con +cic:/Coq/IntMap/Fset/in_FSet.con +cic:/Coq/IntMap/Fset/in_FSet_delta.con +cic:/Coq/IntMap/Fset/in_FSet_diff.con +cic:/Coq/IntMap/Fset/in_FSet_inter.con +cic:/Coq/IntMap/Fset/in_FSet_union.con +cic:/Coq/IntMap/Fset/MapDom.con +cic:/Coq/IntMap/Fset/MapDom_Dom.con +cic:/Coq/IntMap/Fset/MapDomRestrBy.con +cic:/Coq/IntMap/Fset/MapDomRestrBy_semantics.con +cic:/Coq/IntMap/Fset/MapDomRestrTo.con +cic:/Coq/IntMap/Fset/MapDomRestrTo_semantics.con +cic:/Coq/IntMap/Fset/MapDom_semantics_1.con +cic:/Coq/IntMap/Fset/MapDom_semantics_2.con +cic:/Coq/IntMap/Fset/MapDom_semantics_3.con +cic:/Coq/IntMap/Fset/MapDom_semantics_4.con +cic:/Coq/IntMap/Lsort/aapp_length.con +cic:/Coq/IntMap/Lsort/ad_bit_0_gt.con +cic:/Coq/IntMap/Lsort/ad_bit_0_less.con +cic:/Coq/IntMap/Lsort/ad_comp_double_monotonic.con +cic:/Coq/IntMap/Lsort/ad_comp_double_plus_un_monotonic.con +cic:/Coq/IntMap/Lsort/ad_comp_monotonic.con +cic:/Coq/IntMap/Lsort/ad_double_monotonic.con +cic:/Coq/IntMap/Lsort/ad_double_plus_un_monotonic.con +cic:/Coq/IntMap/Lsort/ad_ind_double.con +cic:/Coq/IntMap/Lsort/ad_less_1.con +cic:/Coq/IntMap/Lsort/ad_less.con +cic:/Coq/IntMap/Lsort/ad_less_def_1.con +cic:/Coq/IntMap/Lsort/ad_less_def_2.con +cic:/Coq/IntMap/Lsort/ad_less_def_3.con +cic:/Coq/IntMap/Lsort/ad_less_def_4.con +cic:/Coq/IntMap/Lsort/ad_less_not_refl.con +cic:/Coq/IntMap/Lsort/ad_less_total.con +cic:/Coq/IntMap/Lsort/ad_less_trans.con +cic:/Coq/IntMap/Lsort/ad_less_z.con +cic:/Coq/IntMap/Lsort/ad_monotonic.con +cic:/Coq/IntMap/Lsort/ad_rec_double.con +cic:/Coq/IntMap/Lsort/ad_z_less_1.con +cic:/Coq/IntMap/Lsort/ad_z_less_2.con +cic:/Coq/IntMap/Lsort/alist_canonical.con +cic:/Coq/IntMap/Lsort/alist_conc_sorted.con +cic:/Coq/IntMap/Lsort/alist_nth_ad_aapp_1.con +cic:/Coq/IntMap/Lsort/alist_nth_ad_aapp_2.con +cic:/Coq/IntMap/Lsort/alist_nth_ad.con +cic:/Coq/IntMap/Lsort/alist_nth_ad_semantics.con +cic:/Coq/IntMap/Lsort/alist_of_Map_nth_ad.con +cic:/Coq/IntMap/Lsort/alist_of_Map_sorts_1.con +cic:/Coq/IntMap/Lsort/alist_of_Map_sorts1.con +cic:/Coq/IntMap/Lsort/alist_of_Map_sorts2.con +cic:/Coq/IntMap/Lsort/alist_of_Map_sorts.con +cic:/Coq/IntMap/Lsort/alist_semantics_nth_ad.con +cic:/Coq/IntMap/Lsort/alist_semantics_same_tail.con +cic:/Coq/IntMap/Lsort/alist_semantics_tail.con +cic:/Coq/IntMap/Lsort/alist_sorted_1.con +cic:/Coq/IntMap/Lsort/alist_sorted_1_imp_2.con +cic:/Coq/IntMap/Lsort/alist_sorted_2.con +cic:/Coq/IntMap/Lsort/alist_sorted_2_imp.con +cic:/Coq/IntMap/Lsort/alist_sorted.con +cic:/Coq/IntMap/Lsort/alist_sorted_imp_1.con +cic:/Coq/IntMap/Lsort/alist_sorted_tail.con +cic:/Coq/IntMap/Lsort/alist_too_low.con +cic:/Coq/IntMap/Lsort/app_length.con +cic:/Coq/IntMap/Lsort/interval_split.con +cic:/Coq/IntMap/Mapaxioms/eqmap.con +cic:/Coq/IntMap/Mapaxioms/eqmap_refl.con +cic:/Coq/IntMap/Mapaxioms/eqmap_sym.con +cic:/Coq/IntMap/Mapaxioms/eqmap_trans.con +cic:/Coq/IntMap/Mapaxioms/eqm_refl.con +cic:/Coq/IntMap/Mapaxioms/eqm_sym.con +cic:/Coq/IntMap/Mapaxioms/eqm_trans.con +cic:/Coq/IntMap/Mapaxioms/FSetDelta_assoc.con +cic:/Coq/IntMap/Mapaxioms/FSet_ext.con +cic:/Coq/IntMap/Mapaxioms/FSetInter_assoc.con +cic:/Coq/IntMap/Mapaxioms/FSetInter_comm.con +cic:/Coq/IntMap/Mapaxioms/FSetInter_idempotent.con +cic:/Coq/IntMap/Mapaxioms/FSetInter_M0_s.con +cic:/Coq/IntMap/Mapaxioms/FSetInter_s_M0.con +cic:/Coq/IntMap/Mapaxioms/FSetInter_Union_l.con +cic:/Coq/IntMap/Mapaxioms/FSetInter_Union_r.con +cic:/Coq/IntMap/Mapaxioms/FSetUnion_assoc.con +cic:/Coq/IntMap/Mapaxioms/FSetUnion_comm.con +cic:/Coq/IntMap/Mapaxioms/FSetUnion_idempotent.con +cic:/Coq/IntMap/Mapaxioms/FSetUnion_Inter_l.con +cic:/Coq/IntMap/Mapaxioms/FSetUnion_Inter_r.con +cic:/Coq/IntMap/Mapaxioms/FSetUnion_M0_s.con +cic:/Coq/IntMap/Mapaxioms/FSetUnion_s_M0.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_as_DomRestrBy_2.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_as_DomRestrBy.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_as_Merge.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_empty_m_1.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_empty_m.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_ext.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_ext_l.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_ext_r.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_m_empty_1.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_m_empty.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_nilpotent.con +cic:/Coq/IntMap/Mapaxioms/MapDelta_sym.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_By_comm.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_By.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_Dom.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_empty_m_1.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_empty_m.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_ext.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_ext_l.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_ext_r.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_m_empty_1.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_m_empty.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_m_m_1.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_m_m.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_To_comm.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrBy_To.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_assoc.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_By_comm.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_By.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_Dom.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_empty_m_1.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_empty_m.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_ext.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_ext_l.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_ext_r.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_idempotent.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_m_empty_1.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_m_empty.con +cic:/Coq/IntMap/Mapaxioms/MapDomRestrTo_To_comm.con +cic:/Coq/IntMap/Mapaxioms/MapDom_Split_1.con +cic:/Coq/IntMap/Mapaxioms/MapDom_Split_2.con +cic:/Coq/IntMap/Mapaxioms/MapDom_Split_3.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_assoc.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_DomRestrBy.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_DomRestrTo.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_empty_l.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_empty_m_1.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_empty_m.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_empty_r.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_ext.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_ext_l.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_ext_r.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_idempotent.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_m_empty_1.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_m_empty.con +cic:/Coq/IntMap/Mapaxioms/MapMerge_RestrTo_l.con +cic:/Coq/IntMap/Mapaxioms/MapPut_as_Merge.con +cic:/Coq/IntMap/Mapaxioms/MapPut_behind_as_Merge.con +cic:/Coq/IntMap/Mapaxioms/MapPut_behind_ext.con +cic:/Coq/IntMap/Mapaxioms/MapPut_ext.con +cic:/Coq/IntMap/Mapaxioms/MapRemove_as_RestrBy.con +cic:/Coq/IntMap/Mapaxioms/MapRemove_ext.con +cic:/Coq/IntMap/Mapc/alist_of_Map_of_alist_c.con +cic:/Coq/IntMap/Mapcanon/M2_eqmap_1.con +cic:/Coq/IntMap/Mapcanon/M2_eqmap_2.con +cic:/Coq/IntMap/Mapcanon/makeM2_canon.con +cic:/Coq/IntMap/Mapcanon/mapcanon_exists_1.con +cic:/Coq/IntMap/Mapcanon/mapcanon_exists_2.con +cic:/Coq/IntMap/Mapcanon/mapcanon_exists.con +cic:/Coq/IntMap/Mapcanon/MapCanonicalize.con +cic:/Coq/IntMap/Mapcanon/mapcanon.ind +cic:/Coq/IntMap/Mapcanon/mapcanon_ind.con +cic:/Coq/IntMap/Mapcanon/mapcanon_M2_1.con +cic:/Coq/IntMap/Mapcanon/mapcanon_M2_2.con +cic:/Coq/IntMap/Mapcanon/mapcanon_M2.con +cic:/Coq/IntMap/Mapcanon/mapcanon_unique.con +cic:/Coq/IntMap/Mapcanon/MapCollect_canon.con +cic:/Coq/IntMap/Mapcanon/MapDelta_canon.con +cic:/Coq/IntMap/Mapcanon/MapDom_canon.con +cic:/Coq/IntMap/Mapcanon/MapDomRestrBy_canon.con +cic:/Coq/IntMap/Mapcanon/MapDomRestrTo_canon.con +cic:/Coq/IntMap/Mapcanon/MapFold_canon_1.con +cic:/Coq/IntMap/Mapcanon/MapFold_canon.con +cic:/Coq/IntMap/Mapcanon/MapMerge_canon.con +cic:/Coq/IntMap/Mapcanon/Map_of_alist_canon.con +cic:/Coq/IntMap/Mapcanon/MapPut1_canon.con +cic:/Coq/IntMap/Mapcanon/MapPut_behind_canon.con +cic:/Coq/IntMap/Mapcanon/MapPut_canon.con +cic:/Coq/IntMap/Mapcanon/MapRemove_canon.con +cic:/Coq/IntMap/Mapcanon/MapSubset_c_1.con +cic:/Coq/IntMap/Mapcanon/MapSubset_c_2.con +cic:/Coq/IntMap/Mapcard/length_as_fold_2.con +cic:/Coq/IntMap/Mapcard/length_as_fold.con +cic:/Coq/IntMap/Mapcard/MapCard_as_Fold_1.con +cic:/Coq/IntMap/Mapcard/MapCard_as_Fold.con +cic:/Coq/IntMap/Mapcard/MapCard_as_length.con +cic:/Coq/IntMap/Mapcard/MapCard_Dom.con +cic:/Coq/IntMap/Mapcard/MapCard_Dom_Put_behind.con +cic:/Coq/IntMap/Mapcard/MapCard_ext.con +cic:/Coq/IntMap/Mapcard/MapCard_is_not_O.con +cic:/Coq/IntMap/Mapcard/MapCard_is_O.con +cic:/Coq/IntMap/Mapcard/MapCard_is_one.con +cic:/Coq/IntMap/Mapcard/MapCard_is_one_unique.con +cic:/Coq/IntMap/Mapcard/MapCard_is_Sn.con +cic:/Coq/IntMap/Mapcard/MapCard_M0.con +cic:/Coq/IntMap/Mapcard/MapCard_M1.con +cic:/Coq/IntMap/Mapcard/MapCard_makeM2.con +cic:/Coq/IntMap/Mapcard/MapCard_Put_1.con +cic:/Coq/IntMap/Mapcard/MapCard_Put_1_conv.con +cic:/Coq/IntMap/Mapcard/MapCard_Put1_equals_2.con +cic:/Coq/IntMap/Mapcard/MapCard_Put_2.con +cic:/Coq/IntMap/Mapcard/MapCard_Put_2_conv.con +cic:/Coq/IntMap/Mapcard/MapCard_Put_behind_Put.con +cic:/Coq/IntMap/Mapcard/MapCard_Put_behind_sum.con +cic:/Coq/IntMap/Mapcard/MapCard_Put_lb.con +cic:/Coq/IntMap/Mapcard/MapCard_Put_sum.con +cic:/Coq/IntMap/Mapcard/MapCard_Put_ub.con +cic:/Coq/IntMap/Mapcard/MapCard_Remove_1.con +cic:/Coq/IntMap/Mapcard/MapCard_Remove_1_conv.con +cic:/Coq/IntMap/Mapcard/MapCard_Remove_2.con +cic:/Coq/IntMap/Mapcard/MapCard_Remove_2_conv.con +cic:/Coq/IntMap/Mapcard/MapCard_Remove_lb.con +cic:/Coq/IntMap/Mapcard/MapCard_Remove_sum.con +cic:/Coq/IntMap/Mapcard/MapCard_Remove_ub.con +cic:/Coq/IntMap/Mapcard/MapDomRestrBy_Card_lb.con +cic:/Coq/IntMap/Mapcard/MapDomRestrBy_Card_ub_l.con +cic:/Coq/IntMap/Mapcard/MapDomRestrTo_Card_ub_l.con +cic:/Coq/IntMap/Mapcard/MapDomRestrTo_Card_ub_r.con +cic:/Coq/IntMap/Mapcard/MapMerge_Card_disjoint.con +cic:/Coq/IntMap/Mapcard/MapMerge_Card_lb_l.con +cic:/Coq/IntMap/Mapcard/MapMerge_Card_lb_r.con +cic:/Coq/IntMap/Mapcard/MapMerge_Card_ub.con +cic:/Coq/IntMap/Mapcard/MapMerge_disjoint_Card.con +cic:/Coq/IntMap/Mapcard/MapMerge_Restr_Card.con +cic:/Coq/IntMap/Mapcard/MapSplit_Card.con +cic:/Coq/IntMap/Mapcard/MapSubset_card_eq_1.con +cic:/Coq/IntMap/Mapcard/MapSubset_card_eq.con +cic:/Coq/IntMap/Mapcard/MapSubset_Card_le.con +cic:/Coq/IntMap/Mapc/FSetDelta_assoc_c.con +cic:/Coq/IntMap/Mapc/FSet_ext_c.con +cic:/Coq/IntMap/Mapc/FSetInter_assoc_c.con +cic:/Coq/IntMap/Mapc/FSetInter_comm_c.con +cic:/Coq/IntMap/Mapc/FSetInter_idempotent.con +cic:/Coq/IntMap/Mapc/FSetInter_M0_s_c.con +cic:/Coq/IntMap/Mapc/FSetInter_s_M0_c.con +cic:/Coq/IntMap/Mapc/FSetInter_Union_l_c.con +cic:/Coq/IntMap/Mapc/FSetInter_Union_r.con +cic:/Coq/IntMap/Mapc/FSetUnion_assoc_c.con +cic:/Coq/IntMap/Mapc/FSetUnion_comm_c.con +cic:/Coq/IntMap/Mapc/FSetUnion_idempotent.con +cic:/Coq/IntMap/Mapc/FSetUnion_Inter_l_c.con +cic:/Coq/IntMap/Mapc/FSetUnion_Inter_r.con +cic:/Coq/IntMap/Mapc/FSetUnion_M0_s_c.con +cic:/Coq/IntMap/Mapc/FSetUnion_s_M0_c.con +cic:/Coq/IntMap/Mapc/FSubset_antisym_c.con +cic:/Coq/IntMap/Mapc/MapDelta_as_DomRestrBy_2_c.con +cic:/Coq/IntMap/Mapc/MapDelta_as_DomRestrBy_c.con +cic:/Coq/IntMap/Mapc/MapDelta_as_Merge_c.con +cic:/Coq/IntMap/Mapc/MapDelta_disjoint_c.con +cic:/Coq/IntMap/Mapc/MapDelta_nilpotent_c.con +cic:/Coq/IntMap/Mapc/MapDelta_sym_c.con +cic:/Coq/IntMap/Mapc/MapDisjoint_empty_c.con +cic:/Coq/IntMap/Mapc/MapDomRestrBy_By_c.con +cic:/Coq/IntMap/Mapc/MapDomRestrBy_By_comm_c.con +cic:/Coq/IntMap/Mapc/MapDomRestrBy_Dom_c.con +cic:/Coq/IntMap/Mapc/MapDomRestrBy_To_c.con +cic:/Coq/IntMap/Mapc/MapDomRestrBy_To_comm_c.con +cic:/Coq/IntMap/Mapc/MapDomRestrTo_assoc_c.con +cic:/Coq/IntMap/Mapc/MapDomRestrTo_By_c.con +cic:/Coq/IntMap/Mapc/MapDomRestrTo_By_comm_c.con +cic:/Coq/IntMap/Mapc/MapDomRestrTo_Dom_c.con +cic:/Coq/IntMap/Mapc/MapDomRestrTo_idempotent_c.con +cic:/Coq/IntMap/Mapc/MapDomRestrTo_To_comm_c.con +cic:/Coq/IntMap/Mapc/MapDom_Split_1_c.con +cic:/Coq/IntMap/Mapc/MapDom_Split_2_c.con +cic:/Coq/IntMap/Mapc/MapDom_Split_3_c.con +cic:/Coq/IntMap/Mapc/MapMerge_assoc_c.con +cic:/Coq/IntMap/Mapc/MapMerge_DomRestrBy_c.con +cic:/Coq/IntMap/Mapc/MapMerge_DomRestrTo_c.con +cic:/Coq/IntMap/Mapc/MapMerge_empty_m_c.con +cic:/Coq/IntMap/Mapc/MapMerge_idempotent_c.con +cic:/Coq/IntMap/Mapc/MapMerge_RestrTo_l_c.con +cic:/Coq/IntMap/Mapc/Map_of_alist_of_Map_c.con +cic:/Coq/IntMap/Mapc/MapPut_as_Merge_c.con +cic:/Coq/IntMap/Mapc/MapPut_behind_as_Merge_c.con +cic:/Coq/IntMap/Mapc/MapRemove_as_RestrBy_c.con +cic:/Coq/IntMap/Mapc/MapSubset_antisym_c.con +cic:/Coq/IntMap/Map/eqm.con +cic:/Coq/IntMap/Mapfold/DMerge.con +cic:/Coq/IntMap/Mapfold/in_dom_DMerge_1.con +cic:/Coq/IntMap/Mapfold/in_dom_DMerge_2.con +cic:/Coq/IntMap/Mapfold/in_dom_DMerge_3.con +cic:/Coq/IntMap/Mapfold/MapFold1_as_Fold_1.con +cic:/Coq/IntMap/Mapfold/MapFold1_as_Fold.con +cic:/Coq/IntMap/Mapfold/MapFold1_ext.con +cic:/Coq/IntMap/Mapfold/MapFold_distr_l.con +cic:/Coq/IntMap/Mapfold/MapFold_distr_r_1.con +cic:/Coq/IntMap/Mapfold/MapFold_distr_r.con +cic:/Coq/IntMap/Mapfold/MapFold_ext.con +cic:/Coq/IntMap/Mapfold/MapFold_ext_f_1.con +cic:/Coq/IntMap/Mapfold/MapFold_ext_f.con +cic:/Coq/IntMap/Mapfold/MapFold_Merge_disjoint_1.con +cic:/Coq/IntMap/Mapfold/MapFold_Merge_disjoint.con +cic:/Coq/IntMap/Mapfold/MapFold_orb_1.con +cic:/Coq/IntMap/Mapfold/MapFold_orb.con +cic:/Coq/IntMap/Mapfold/MapFold_Put_behind_disjoint_2.con +cic:/Coq/IntMap/Mapfold/MapFold_Put_behind_disjoint.con +cic:/Coq/IntMap/Mapfold/MapFold_Put_disjoint_1.con +cic:/Coq/IntMap/Mapfold/MapFold_Put_disjoint_2.con +cic:/Coq/IntMap/Mapfold/MapFold_Put_disjoint.con +cic:/Coq/IntMap/Mapiter/aapp.con +cic:/Coq/IntMap/Mapiter/acons.con +cic:/Coq/IntMap/Mapiter/ad_comp_double_inj.con +cic:/Coq/IntMap/Mapiter/ad_comp_double_plus_un_inj.con +cic:/Coq/IntMap/Mapiter/ad_inj.con +cic:/Coq/IntMap/Mapiter/alist.con +cic:/Coq/IntMap/Mapiter/alist_MapMerge_semantics.con +cic:/Coq/IntMap/Mapiter/alist_MapMerge_semantics_disjoint.con +cic:/Coq/IntMap/Mapiter/alist_of_Map.con +cic:/Coq/IntMap/Mapiter/alist_of_Map_of_alist.con +cic:/Coq/IntMap/Mapiter/alist_of_Map_semantics_1_1.con +cic:/Coq/IntMap/Mapiter/alist_of_Map_semantics_1.con +cic:/Coq/IntMap/Mapiter/alist_of_Map_semantics.con +cic:/Coq/IntMap/Mapiter/alist_semantics_app.con +cic:/Coq/IntMap/Mapiter/alist_semantics.con +cic:/Coq/IntMap/Mapiter/alist_semantics_disjoint_comm.con +cic:/Coq/IntMap/Mapiter/anil.con +cic:/Coq/IntMap/Mapiter/fold_right_aapp.con +cic:/Coq/IntMap/Mapiter/MapCollect1.con +cic:/Coq/IntMap/Mapiter/MapCollect_as_Fold.con +cic:/Coq/IntMap/Mapiter/MapCollect.con +cic:/Coq/IntMap/Mapiter/MapFold1.con +cic:/Coq/IntMap/Mapiter/MapFold1_state.con +cic:/Coq/IntMap/Mapiter/MapFold_as_fold_1.con +cic:/Coq/IntMap/Mapiter/MapFold_as_fold.con +cic:/Coq/IntMap/Mapiter/MapFold.con +cic:/Coq/IntMap/Mapiter/MapFold_empty.con +cic:/Coq/IntMap/Mapiter/MapFold_M1.con +cic:/Coq/IntMap/Mapiter/MapFold_state.con +cic:/Coq/IntMap/Mapiter/MapFold_state_stateless_1.con +cic:/Coq/IntMap/Mapiter/MapFold_state_stateless.con +cic:/Coq/IntMap/Mapiter/Map_of_alist.con +cic:/Coq/IntMap/Mapiter/Map_of_alist_of_Map.con +cic:/Coq/IntMap/Mapiter/Map_of_alist_semantics.con +cic:/Coq/IntMap/Mapiter/MapSweep1.con +cic:/Coq/IntMap/Mapiter/MapSweep2.con +cic:/Coq/IntMap/Mapiter/MapSweep.con +cic:/Coq/IntMap/Mapiter/MapSweep_semantics_1_1.con +cic:/Coq/IntMap/Mapiter/MapSweep_semantics_1.con +cic:/Coq/IntMap/Mapiter/MapSweep_semantics_2_1.con +cic:/Coq/IntMap/Mapiter/MapSweep_semantics_2_2.con +cic:/Coq/IntMap/Mapiter/MapSweep_semantics_2.con +cic:/Coq/IntMap/Mapiter/MapSweep_semantics_3_1.con +cic:/Coq/IntMap/Mapiter/MapSweep_semantics_3.con +cic:/Coq/IntMap/Mapiter/MapSweep_semantics_4_1.con +cic:/Coq/IntMap/Mapiter/MapSweep_semantics_4.con +cic:/Coq/IntMap/Mapiter/pair_sp.con +cic:/Coq/IntMap/Maplists/ad_in_elems_in_list.con +cic:/Coq/IntMap/Maplists/ad_in_list_app_1.con +cic:/Coq/IntMap/Maplists/ad_in_list_app.con +cic:/Coq/IntMap/Maplists/ad_in_list.con +cic:/Coq/IntMap/Maplists/ad_in_list_forms_circuit.con +cic:/Coq/IntMap/Maplists/ad_in_list_l.con +cic:/Coq/IntMap/Maplists/ad_in_list_of_dom_in_dom.con +cic:/Coq/IntMap/Maplists/ad_in_list_r.con +cic:/Coq/IntMap/Maplists/ad_in_list_rev.con +cic:/Coq/IntMap/Maplists/ad_list_app_length.con +cic:/Coq/IntMap/Maplists/ad_list_app_rev.con +cic:/Coq/IntMap/Maplists/ad_list_card.con +cic:/Coq/IntMap/Maplists/ad_list_Elems.con +cic:/Coq/IntMap/Maplists/ad_list_has_circuit_stutters.con +cic:/Coq/IntMap/Maplists/ad_list_not_stutters_card.con diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index 71ba8ddc2..4f99dd057 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -12,7 +12,8 @@ (* $Id$ *) let debug = true -let ignore_exc = false +let ignore_exc = true +let ignore_exc_new_typing = true let rank_all_dependencies = false let trust_environment = false @@ -185,7 +186,14 @@ let _ = (fun u -> let u= OCic2NCic.nuri_of_ouri u in indent := 0; - NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u)) + try NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u) + with + | NCicTypeChecker.AssertFailure s + | NCicTypeChecker.TypeCheckerFailure s + | NCicEnvironment.ObjectNotFound s + | NCicEnvironment.BadDependency s as e -> + prerr_endline ("######### " ^ Lazy.force s); + if not ignore_exc_new_typing then raise e) alluris; let dopo = Unix.gettimeofday () in Gc.compact (); diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index c15e75a87..20a573c5d 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -224,7 +224,7 @@ let are_convertible ?(subst=[]) get_relevance = | (C.Appl (hd1::tl1), C.Appl (hd2::tl2)) -> aux test_eq_only context hd1 hd2 && - let relevance = get_relevance ~subst context hd1 in + let relevance = get_relevance ~subst context hd1 tl1 in (try HExtlib.list_forall_default3 (fun t1 t2 b -> not b || aux test_eq_only context t1 t2) diff --git a/helm/software/components/ng_kernel/nCicReduction.mli b/helm/software/components/ng_kernel/nCicReduction.mli index 5943c9260..ebbba2543 100644 --- a/helm/software/components/ng_kernel/nCicReduction.mli +++ b/helm/software/components/ng_kernel/nCicReduction.mli @@ -19,7 +19,7 @@ val whd : val are_convertible : ?subst:NCic.substitution -> (subst:NCic.substitution -> - NCic.context -> NCic.term -> bool list) -> + NCic.context -> NCic.term -> NCic.term list -> bool list) -> NCic.context -> NCic.term -> NCic.term -> bool diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 8b8348023..5daea200c 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -1022,28 +1022,44 @@ and type_of_constant ((Ref.Ref (uri,_)) as ref) = ty | _ -> raise (AssertFailure (lazy "type_of_constant: environment/reference")) -and get_relevance ~subst context = function - | C.Const r -> +and get_relevance ~subst context te args = + match te with + | C.Const r when List.length (E.get_relevance r) >= List.length args -> let relevance = E.get_relevance r in (match r with | Ref.Ref (_,Ref.Con (_,_,lno)) -> let _,relevance = HExtlib.split_nth lno relevance in HExtlib.mk_list false lno @ relevance | _ -> relevance) - | t -> + | t -> let ty = typeof ~subst ~metasenv:[] context t in - let rec aux context = function - | C.Prod (name,so,de) -> - let sort = typeof ~subst ~metasenv:[] context so in - (match sort with - | C.Sort C.Prop -> false::(aux ((name,(C.Decl so))::context) de) - | C.Sort _ -> true::(aux ((name,(C.Decl so))::context) de) - | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf + let rec aux context ty = function + | [] -> [] + | arg::tl -> match R.whd ~subst context ty with + | C.Prod (name,so,de) -> + let sort = typeof ~subst ~metasenv:[] context so in + let new_ty = S.subst ~avoid_beta_redexes:true arg de in + (match R.whd ~subst context sort with + | C.Sort C.Prop -> + false::(aux ((name,(C.Decl so))::context) new_ty tl) + | C.Sort _ + | C.Meta _ -> true::(aux ((name,(C.Decl so))::context) de tl) + | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf "Prod: the type %s of the source of %s is not a sort" (PP.ppterm ~subst ~metasenv:[] ~context sort) (PP.ppterm ~subst ~metasenv:[] ~context so))))) - | _ -> [] - in aux context ty + | _ -> + raise + (TypeCheckerFailure + (lazy (Printf.sprintf + "Appl: %s is not a function, it cannot be applied" + (PP.ppterm ~subst ~metasenv:[] ~context + (let res = List.length tl in + let eaten = List.length args - res in + (C.Appl + (t::fst + (HExtlib.split_nth eaten args)))))))) + in aux context ty args ;; let typecheck_context ~metasenv ~subst context = @@ -1136,8 +1152,37 @@ let check_rel1_irrelevant ~metasenv ~subst context = fun _ -> ();; in aux (1, context) () *) -let check_relevance ~metasenv ~subst ~in_type relevance = fun _ -> ();; -(* let shift e (in_type, context, relevance) = +let check_relevance ~subst ~metasenv relevance ty = + let error () = + raise (TypeCheckerFailure + (lazy ("Wrong relevance declaration: " ^ + String.concat "," (List.map string_of_bool relevance)^ + "\nfor type: "^PP.ppterm ~metasenv ~subst ~context:[] ty))) + in + let rec aux context relevance ty = + match R.whd ~subst context ty with + | C.Prod (name,so,de) -> + let sort = typeof ~subst ~metasenv context so in + (match (relevance,R.whd ~subst context sort) with + | [],_ -> () + | false::tl,C.Sort C.Prop -> aux ((name,(C.Decl so))::context) tl de + | true::_,C.Sort C.Prop + | false::_,C.Sort _ + | false::_,C.Meta _ -> error () + | true::tl,C.Sort _ + | true::tl,C.Meta _ -> aux ((name,(C.Decl so))::context) tl de + | _ -> raise (TypeCheckerFailure (lazy (Printf.sprintf + "Prod: the type %s of the source of %s is not a sort" + (PP.ppterm ~subst ~metasenv ~context sort) + (PP.ppterm ~subst ~metasenv ~context so))))) + | _ -> (match relevance with + | [] -> () + | _::_ -> error ()) + in aux [] relevance ty +;; +(* old check_relevance + +let shift e (in_type, context, relevance) = assert (relevance = []); in_type, e::context, relevance in let rec aux2 (_,context,relevance as k) t = @@ -1210,11 +1255,11 @@ let typecheck_obj (uri,_height,metasenv,subst,kind) = "inferred type:\n%s\nexpected type:\n%s") (PP.ppterm ~subst ~metasenv ~context:[] ty_te) (PP.ppterm ~subst ~metasenv ~context:[] ty)))); - check_relevance ~in_type:true ~subst ~metasenv relevance ty; - check_relevance ~in_type:false ~subst ~metasenv relevance te + check_relevance ~subst ~metasenv relevance ty + (*check_relevance ~in_type:false ~subst ~metasenv relevance te*) | C.Constant (relevance,_,None,ty,_) -> ignore (typeof ~subst ~metasenv [] ty); - check_relevance ~in_type:true ~subst ~metasenv relevance ty + check_relevance ~subst ~metasenv relevance ty | C.Inductive (_, leftno, tyl, _) -> check_mutual_inductive_defs uri ~metasenv ~subst leftno tyl | C.Fixpoint (inductive,fl,_) -> diff --git a/helm/software/components/ng_kernel/oCic2NCic.ml b/helm/software/components/ng_kernel/oCic2NCic.ml index 56159ffa4..0ead3ff2f 100644 --- a/helm/software/components/ng_kernel/oCic2NCic.ml +++ b/helm/software/components/ng_kernel/oCic2NCic.ml @@ -46,10 +46,12 @@ let get_relevance ty = match CicReduction.whd context ty with Cic.Prod (n,s,t) -> not (is_proof_irrelevant context s)::aux (Some (n,Cic.Decl s)::context) t - | ty -> if is_proof_irrelevant context ty then raise InProp else [] + | _ -> [] + in aux [] ty +(* | ty -> if is_proof_irrelevant context ty then raise InProp else [] in try aux [] ty - with InProp -> [] + with InProp -> []*) ;; (* porcatissima *) diff --git a/helm/software/components/ng_kernel/test.ma b/helm/software/components/ng_kernel/test.ma index ff017315c..36a2d9f72 100644 --- a/helm/software/components/ng_kernel/test.ma +++ b/helm/software/components/ng_kernel/test.ma @@ -12,9 +12,15 @@ (* *) (**************************************************************************) -include "nat/plus.ma". +inductive nat : Set \def +| O : nat +| S : nat -> nat. + +let rec a m n := +match m with + [ O => n + | S x => S (a x n)]. -(* let rec f n := match n with [ O => O @@ -24,21 +30,21 @@ let rec f n := | S q => let rec h y := match y with - [ O => f m + g q + [ O => a (f m) (g q) | S w => h w] in h q] in g m]. -*) -let rec f n := - match n with - [ O => O - | S m => g m - ] -and g m := - match m with - [ O => O - | S n => f n - ]. \ No newline at end of file +coinductive conat : Set \def +| OO : conat +| OS : conat -> conat. + +inductive wrap : Set \def +| w : conat -> wrap +| ws : wrap -> wrap. + +let corec h (n:nat) \def +g (ws (w (h n))) +and g x \def OO. \ No newline at end of file -- 2.39.2