]> matita.cs.unibo.it Git - helm.git/blob - components/tactics/hashtbl_equiv.ml
unified: some theorems on Lift started
[helm.git] / components / tactics / hashtbl_equiv.ml
1 (* Copyright (C) 2000-2002, HELM Team.
2  * 
3  * This file is part of HELM, an Hypertextual, Electronic
4  * Library of Mathematics, developed at the Computer Science
5  * Department, University of Bologna, Italy.
6  * 
7  * HELM is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  * 
12  * HELM is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with HELM; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 (*********************************************************************)
27 (*                                                                   *)
28 (*                           PROJECT HELM                            *)
29 (*                                                                   *)
30 (*                          Andrea Asperti                           *)
31 (*                            8/09/2004                              *)
32 (*                                                                   *)
33 (*                                                                   *)
34 (*********************************************************************)
35
36 (* $Id$ *)
37
38 (* the file contains an hash table of objects of the library
39    equivalent to some object in the standard subset; it is
40    mostly used to filter useless cases in auto *)
41
42
43 let equivalent_objects =
44 (* finte costanti; i.e. costanti senza corpo *)
45 [UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack0.con"(*,"finte costanti"*);
46  UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/Ac10.con"(*,"finte costanti"*);
47  UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/Ack2.con"(*,"finte costanti"*)
48  ]@
49 (* inutili mostri *)
50 [UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/Resg0.con"(*,"useless monster"*);
51  UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/Resg1.con"(*,"useless monster"*);
52  UriManager.uri_of_string "cic:/Rocq/DEMOS/Demo_AutoRewrite/ResAck0.con"(*,"useless monster"*)
53  ]@
54 (* istanze *)
55    (UriManager.uri_of_string "cic:/Coq/Init/Peano/eq_S.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal.con"*))::
56 [
57 UriManager.uri_of_string "cic:/Paris/ZF/src/useful/lem_iff_sym.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/iff_sym.con"*);
58 UriManager.uri_of_string "cic:/Lyon/AUTOMATA/Ensf_types/False_imp_P.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/False_ind.con"*);
59 UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/plus_O_r.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_r.con"*);
60 UriManager.uri_of_string "cic:/Coq/Reals/Rfunctions/sum_f_R0_triangle.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/PartSum/Rabs_triang_gen.con"*);
61 UriManager.uri_of_string "cic:/Sophia-Antipolis/Bertrand/Misc/eq_plus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_reg_l.con"*);
62 UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_not_and.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/or_not_and.con"*);
63 UriManager.uri_of_string "cic:/Rocq/DEMOS/Sorting/diff_true_false.con"(*,UriManager.uri_of_string "cic:/Coq/Bool/Bool/diff_true_false.con"*);
64 UriManager.uri_of_string "cic:/CoRN/metrics/CMetricSpaces/nz.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Max/le_max_l.con"*);
65 UriManager.uri_of_string "cic:/Coq/Logic/Decidable/not_or.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/not_or_and.con"*);
66 UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_not_equal.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_not_eq.con"*);
67 UriManager.uri_of_string "cic:/Coq/Reals/R_sqrt/sqrt_sqrt.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/R_sqrt/sqrt_def.con"*);
68 UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/eps2_Rgt_R0_subproof.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/eps2_Rgt_R0.con"*);
69 UriManager.uri_of_string "cic:/Coq/Logic/Eqdep_dec/eqT2eq.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con"*);
70 UriManager.uri_of_string "cic:/Coq/Reals/R_sqr/Rsqr_eq_0.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rsqr_0_uniq.con"*);
71 UriManager.uri_of_string "cic:/Rocq/THREE_GAP/Nat_compl/en_plus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_r.con"*);
72 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zabs_10.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zabs/Zabs_pos.con"*);
73 UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof0.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof.con"*);
74 UriManager.uri_of_string "cic:/Coq/Arith/Le/le_refl.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/le.ind#xpointer(1/1/1)"*); 
75 UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/le_n_n.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Le/le_refl.con"*);
76 UriManager.uri_of_string "cic:/Coq/ZArith/auxiliary/Zred_factor1.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zplus_diag_eq_mult_2.con"*);
77 UriManager.uri_of_string "cic:/Coq/Relations/Newman/caseRxy.con"(*,UriManager.uri_of_string "cic:/Coq/Relations/Newman/Ind_proof.con"*);
78 UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/S_plus_r.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/plus_n_Sm.con"*);
79 UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/Zmult_ab0a0b0.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zmult_integral.con"*);
80 UriManager.uri_of_string "cic:/Sophia-Antipolis/Algebra/Z_group/ax8.con"(*,UriManager.uri_of_string "cic:/Coq/NArith/BinPos/ZC2.con"*);
81 UriManager.uri_of_string "cic:/Sophia-Antipolis/Algebra/Z_group/Zlt_reg_l.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zplus_lt_compat_l.con"*);
82 UriManager.uri_of_string "cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/mult_neutr.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_1_l.con"*);
83 UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rlt_0_1.con"*);
84 UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Classic.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/NNPP.con"*);
85 UriManager.uri_of_string "cic:/Coq/Reals/R_sqr/Rsqr_pos_lt.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rlt_0_sqr.con"*);
86 UriManager.uri_of_string "cic:/Rocq/THREE_GAP/Nat_compl/lt_minus2.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con"*);
87 UriManager.uri_of_string "cic:/Coq/Reals/Rtrigo_def/sin_antisym.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rtrigo/sin_neg.con"*);
88 UriManager.uri_of_string "cic:/Sophia-Antipolis/Functions_in_ZFC/Functions_in_ZFC/false_implies_everything.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/False_ind.con"*);
89 UriManager.uri_of_string "cic:/Coq/ring/Setoid_ring_normalize/index_eq_prop.con"(*,UriManager.uri_of_string "cic:/Coq/ring/Ring_normalize/index_eq_prop.con"*);
90 UriManager.uri_of_string "cic:/CoRN/algebra/Basics/le_pred.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Le/le_pred.con"*);
91 UriManager.uri_of_string "cic:/Lannion/continuations/FOUnify_cps/nat_complements/le_S_eqP.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Compare/le_le_S_eq.con"*);
92 UriManager.uri_of_string "cic:/Coq/Sorting/Permutation/permut_right.con"(*,UriManager.uri_of_string "cic:/Coq/Sorting/Permutation/permut_cons.con"*);
93 UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/Zlt_mult_l.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zmult_lt_compat_l.con"*);
94 UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rplus_lt_0_compat.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/DiscrR/Rplus_lt_pos.con"*);
95 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zpower_1_subproof.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zmult_1_r.con"*);
96 UriManager.uri_of_string "cic:/CoRN/fta/KeyLemma/lem_1c.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Minus/le_minus.con"*);
97 UriManager.uri_of_string "cic:/Coq/omega/OmegaLemmas/OMEGA20.con"(*,UriManager.uri_of_string "cic:/Coq/omega/OmegaLemmas/OMEGA17.con"*);
98 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/pair_2.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Datatypes/injective_projections.con"*);
99 UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/Rlt_eps4_eps_subproof.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rlimit/Rlt_eps2_eps_subproof.con"*);
100 UriManager.uri_of_string "cic:/CoRN/algebra/Basics/le_mult_right.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_le_compat_r.con"*);
101 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zle_lt_plus_plus.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zplus_le_lt_compat.con"*);
102 UriManager.uri_of_string "cic:/Rocq/ARITH/Chinese/Nat_complements/lt_minus2.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con"*);
103 UriManager.uri_of_string "cic:/Rocq/THREE_GAP/Nat_compl/not_gt_le.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Compare_dec/not_gt.con"*);
104 UriManager.uri_of_string "cic:/Rocq/ARITH/Chinese/Nat_complements/mult_commut.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_comm.con"*);
105 UriManager.uri_of_string "cic:/CoRN/algebra/Basics/lt_mult_right.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_lt_compat_r.con"*);
106 UriManager.uri_of_string "cic:/Rocq/ARITH/Chinese/Nat_complements/mult_neutr.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_1_l.con"*);
107 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zabs_neg.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zabs/Zabs_non_eq.con"*);
108 UriManager.uri_of_string "cic:/Lyon/FIRING-SQUAD/bib/plus_S.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/plus_Sn_m.con"*);
109 UriManager.uri_of_string "cic:/Nijmegen/QArith/Qhomographic_Qpositive_to_Qpositive/one_non_negative.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zle_0_1.con"*);
110 UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rle_0_1.con"*);
111 UriManager.uri_of_string "cic:/Coq/Logic/Diaconescu/proof_irrel.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/proof_irrelevance.con"*);
112 UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_equal.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con"*);
113 UriManager.uri_of_string "cic:/Coq/IntMap/Mapiter/pair_sp.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Datatypes/surjective_pairing.con"*);
114 UriManager.uri_of_string "cic:/Coq/Logic/ProofIrrelevance/proof_irrelevance_cci.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/proof_irrelevance.con"*);
115 UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_or_not.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/not_and_or.con"*);
116 UriManager.uri_of_string "cic:/CoRN/model/structures/Zsec/Zplus_wd0.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zplus_eq_compat.con"*);
117 UriManager.uri_of_string "cic:/Coq/ZArith/auxiliary/Zred_factor6.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zplus_0_r_reverse.con"*);
118 UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/S_inj.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/eq_add_S.con"*);
119 UriManager.uri_of_string "cic:/Coq/ZArith/Wf_Z/Z_of_nat_complete.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/IZN.con"*);
120 UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Commutative_orb.con"(*,UriManager.uri_of_string "cic:/Coq/Bool/Bool/orb_comm.con"*);
121 UriManager.uri_of_string "cic:/Coq/Reals/PartSum/plus_sum.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Cauchy_prod/sum_plus.con"*);
122 UriManager.uri_of_string "cic:/Nijmegen/QArith/Qpositive/minus_le.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Minus/le_minus.con"*);
123 UriManager.uri_of_string "cic:/Lyon/FIRING-SQUAD/bib/plus_zero.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_r.con"*);
124 UriManager.uri_of_string "cic:/Sophia-Antipolis/Cours-de-Coq/ex1_auto/not_not_converse.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/NNPP.con"*);
125 UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/deMorgan_and_not.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/not_or_and.con"*);
126 UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/Commutative_andb.con"(*,UriManager.uri_of_string "cic:/Coq/Bool/Bool/andb_comm.con"*);
127 UriManager.uri_of_string "cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/lt_minus2.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/ArithProp/lt_minus_O_lt.con"*);
128 UriManager.uri_of_string "cic:/Suresnes/BDD/canonicite/Prelude0/Morgan_and_not.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/not_or_and.con"*);
129 UriManager.uri_of_string "cic:/Coq/Logic/ClassicalFacts/TrueP.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/ClassicalFacts/FalseP.con"*);
130 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zminus_eq.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zminus_eq.con"*);
131 UriManager.uri_of_string "cic:/Sophia-Antipolis/Cours-de-Coq/ex1/not_not_converse.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/NNPP.con"*);
132 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/pair_1.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Datatypes/surjective_pairing.con"*);
133 UriManager.uri_of_string "cic:/Orsay/Maths/divide/Zabs_ind.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zabs/Zabs_ind.con"*);
134 UriManager.uri_of_string "cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zmult_minus_distr_l.con"*);
135 UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Req_le.con"*);
136 UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/Sn_eq_Sm_n_eq_m.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/eq_add_S.con"*);
137 UriManager.uri_of_string "cic:/Coq/Init/Logic/trans_equal.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con"*);
138 UriManager.uri_of_string "cic:/Coq/omega/OmegaLemmas/OMEGA2.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con"*);
139 UriManager.uri_of_string "cic:/Sophia-Antipolis/Bertrand/Raux/P_Rmin.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rpower/P_Rmin.con"*);
140 UriManager.uri_of_string "cic:/Sophia-Antipolis/MATHS/Z/Nat_complements/mult_commut.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_comm.con"*);
141 UriManager.uri_of_string "cic:/Sophia-Antipolis/Huffman/Aux/le_minus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Minus/le_minus.con"*);
142 UriManager.uri_of_string "cic:/Coq/Init/Peano/plus_O_n.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_l.con"*);
143 UriManager.uri_of_string "cic:/Coq/Logic/Berardi/inv2.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Berardi/AC.con"*);
144 UriManager.uri_of_string "cic:/Coq/Reals/SeqProp/not_Rlt.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Rnot_lt_ge.con"*);
145 UriManager.uri_of_string "cic:/Nancy/FOUnify/nat_complements/le_S_eqP.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Compare/le_le_S_eq.con"*);
146 UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/le_mult_l.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_le_compat_r.con"*);
147 UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/natZ/isnat_mult.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zmult_le_0_compat.con"*);
148 UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/RIneq/Req_le_sym.con"*);
149 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zabs_mult.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zabs/Zabs_Zmult.con"*);
150 UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/plus_n_O.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_r.con"*);
151 UriManager.uri_of_string "cic:/Suresnes/BDD/rauzy/algorithme1/Prelude_BDT/excluded_middle.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/classic.con"*);
152 UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/le_mult_mult.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_le_compat.con"*);
153 UriManager.uri_of_string "cic:/Coq/Bool/Bool/Is_true_eq_true2.con"(*,UriManager.uri_of_string "cic:/Coq/Bool/Bool/Is_true_eq_left.con"*);
154 UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/natZ/isnat_plus.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zplus_le_0_compat.con"*);
155 UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/lt_plus_plus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_lt_compat.con"*);
156 UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/le_mult_r.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Mult/mult_le_compat_l.con"*);
157 UriManager.uri_of_string "cic:/Sophia-Antipolis/Functions_in_ZFC/Functions_in_ZFC/excluded_middle.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/NNPP.con"*);
158 UriManager.uri_of_string "cic:/Sophia-Antipolis/Algebra/Z_group/ax3.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zgt_pos_0.con"*);
159 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zabs_plus.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zabs/Zabs_triangle.con"*);
160 UriManager.uri_of_string "cic:/Sophia-Antipolis/Buchberger/Buch/Sdep.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Datatypes/prod_ind.con"*);
161 UriManager.uri_of_string "cic:/Coq/Reals/PartSum/Rsum_abs.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/PartSum/Rabs_triang_gen.con"*);
162 UriManager.uri_of_string "cic:/Cachan/SMC/mu/minus_n_m_le_n.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Minus/le_minus.con"*);
163 UriManager.uri_of_string "cic:/Marseille/GC/lib_arith/lib_S_pred/eqnm_eqSnSm.con"(*,UriManager.uri_of_string "cic:/Coq/Init/Peano/eq_S.con"*);
164 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zpower_1_subproof_subproof.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/BinInt/Zmult_1_r.con"*);
165 UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/predminus1.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Minus/pred_of_minus.con"*);
166 UriManager.uri_of_string "cic:/Sophia-Antipolis/Bertrand/Raux/Rpower_pow.con"(*,UriManager.uri_of_string "cic:/Coq/Reals/Rpower/Rpower_pow.con"*);
167 UriManager.uri_of_string "cic:/Lyon/FIRING-SQUAD/bib/lt_plus_plus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_lt_compat.con"*);
168 UriManager.uri_of_string "cic:/Eindhoven/POCKLINGTON/lemmas/Zlt_neq.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zlt_not_eq.con"*);
169 UriManager.uri_of_string "cic:/Coq/Arith/Lt/nat_total_order.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Compare_dec/not_eq.con"*);
170 UriManager.uri_of_string "cic:/Rocq/TreeAutomata/bases/plus_O_l.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_0_r.con"*);
171 UriManager.uri_of_string "cic:/Coq/Logic/ClassicalFacts/boolP.ind#xpointer(1/1/2)"(*,UriManager.uri_of_string "cic:/Coq/Logic/ClassicalFacts/boolP.ind#xpointer(1/1/1)"*);
172 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zmult_pos_pos.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zmult_lt_O_compat.con"*);
173 UriManager.uri_of_string "cic:/Nijmegen/QArith/Zaux/Zlt_plus_plus.con"(*,UriManager.uri_of_string "cic:/Coq/ZArith/Zorder/Zplus_lt_compat.con"*);
174 UriManager.uri_of_string "cic:/Coq/Logic/Diaconescu/pred_ext_and_rel_choice_imp_EM.con"(*,UriManager.uri_of_string "cic:/Coq/Logic/Classical_Prop/classic.con"*);
175 UriManager.uri_of_string "cic:/Sophia-Antipolis/Rsa/MiscRsa/eq_plus.con"(*,UriManager.uri_of_string "cic:/Coq/Arith/Plus/plus_reg_l.con"*)
176 ]
177 ;;
178
179 let equiv_table = Hashtbl.create 503
180 ;;
181
182 let _ = List.iter (fun a -> Hashtbl.add equiv_table a "") equivalent_objects
183 ;; 
184
185 let not_a_duplicate u =
186   try
187     ignore(Hashtbl.find equiv_table u); false
188   with
189     Not_found -> true
190 ;;