Appl case in is_really_smaller fixed as in the old kernel

[helm.git] / helm / software / components / ng_kernel / alluris.txt

diff --git a/helm/software/components/ng_kernel/alluris.txt b/helm/software/components/ng_kernel/alluris.txt
index 01add230a494b285682291dac39a78810233da67..444ee8e6071ac01cc1b0513fa26d95675e07276b 100644 (file)
--- a/helm/software/components/ng_kernel/alluris.txt
+++ b/helm/software/components/ng_kernel/alluris.txt
@@ -1,3 +1,79 @@
+cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con
+cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con
+cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/app_strext.con
+cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con
+cic:/matita/algebra/CoRN/SetoidFun/appA.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con
+cic:/matita/algebra/CoRN/SetoidFun/UR.con
+cic:/matita/algebra/CoRN/SetoidFun/UQ.con
+cic:/matita/algebra/CoRN/SetoidFun/UP.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind
+cic:/matita/algebra/CoRN/SetoidFun/Tapp.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con
+cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind
+cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con
+cic:/matita/algebra/CoRN/SetoidFun/Inv.con
+cic:/matita/algebra/CoRN/SetoidFun/Fid.con
+cic:/matita/algebra/CoRN/SetoidFun/Fconst.con
+cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con
+cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con
+cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind
+cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con
+cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind
+cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con
+cic:/matita/algebra/CoRN/SetoidFun/BR.con
+cic:/matita/algebra/CoRN/SetoidFun/BQ.con
+cic:/matita/algebra/CoRN/SetoidFun/BP.con
+cic:/matita/algebra/CoRN/SetoidFun/Astar.con
+cic:/matita/demo/realisability/correct2.con
+cic:/matita/demo/realisability/correct.con
+cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con
+cic:/matita/demo/realisability/type_OF_SP.con
+cic:/matita/demo/realisability/true_impl_realized.con
+cic:/matita/demo/realisability/sigma_rect.con
+cic:/matita/demo/realisability/sigma_rec.con
+cic:/matita/demo/realisability/sigma_ind.con
+cic:/matita/demo/realisability/sigma.ind
+cic:/matita/demo/realisability/realized.con
+cic:/matita/demo/realisability/pi2.con
+cic:/matita/demo/realisability/pi1.con
+cic:/matita/demo/realisability/modr.con
+cic:/matita/demo/realisability/id_axiom.con
+cic:/matita/demo/realisability/extraction.con
+cic:/matita/demo/realisability/elim_abs.con
+cic:/matita/demo/realisability/cut.con
+cic:/matita/demo/realisability/and_i.con
+cic:/matita/demo/realisability/SP_rect.con
+cic:/matita/demo/realisability/SP_rec.con
+cic:/matita/demo/realisability/SP_ind.con
+cic:/matita/demo/realisability/SP.ind
+cic:/matita/demo/realisability/Prop_OF_SP.con
 cic:/matita/Q/Qaxioms/symmetric_Qtimes.con
 cic:/matita/Q/Qaxioms/symmetric_Qplus.con
 cic:/matita/Q/Qaxioms/sigma_Q.con
@@ -1548,8 +1624,6 @@ cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_rec.con
 cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_is_CSemiGroup.con
 cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup_ind.con
 cic:/matita/algebra/CoRN/SemiGroups/CSemiGroup.ind
-cic:/matita/algebra/CoRN/SemiGroups/Astar_is_CSemiGroup.con
-cic:/matita/algebra/CoRN/SemiGroups/Astar_as_CSemiGroup.con
 cic:/matita/algebra/CoRN/SetoidFun/total_eq_part.con
 cic:/matita/algebra/CoRN/SetoidFun/ta_apfun.con
 cic:/matita/algebra/CoRN/SetoidFun/sym_apfun.con
@@ -1588,8 +1662,6 @@ cic:/matita/algebra/CoRN/SetoidFun/injective.con
 cic:/matita/algebra/CoRN/SetoidFun/inj2.con
 cic:/matita/algebra/CoRN/SetoidFun/inj1.con
 cic:/matita/algebra/CoRN/SetoidFun/id_is_bij.con
-cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_is_CSetoid.con
-cic:/matita/algebra/CoRN/SetoidFun/free_csetoid_as_csetoid.con
 cic:/matita/algebra/CoRN/SetoidFun/extension_wd.con
 cic:/matita/algebra/CoRN/SetoidFun/extend.con
 cic:/matita/algebra/CoRN/SetoidFun/ext2_a.con
@@ -1626,56 +1698,6 @@ cic:/matita/algebra/CoRN/SetoidFun/bin_part_function_comp_dom_wd.con
 cic:/matita/algebra/CoRN/SetoidFun/bijective.con
 cic:/matita/algebra/CoRN/SetoidFun/bdom_wd.con
 cic:/matita/algebra/CoRN/SetoidFun/assoc_comp.con
-cic:/matita/algebra/CoRN/SetoidFun/app_strext.con
-cic:/matita/algebra/CoRN/SetoidFun/app_as_csb_fun.con
-cic:/matita/algebra/CoRN/SetoidFun/appA.con
-cic:/matita/algebra/CoRN/SetoidFun/ap_fun.con
-cic:/matita/algebra/CoRN/SetoidFun/ap_fm_tight.con
-cic:/matita/algebra/CoRN/SetoidFun/ap_fm_symmetric.con
-cic:/matita/algebra/CoRN/SetoidFun/ap_fm_irreflexive.con
-cic:/matita/algebra/CoRN/SetoidFun/ap_fm_cotransitive.con
-cic:/matita/algebra/CoRN/SetoidFun/UR.con
-cic:/matita/algebra/CoRN/SetoidFun/UQ.con
-cic:/matita/algebra/CoRN/SetoidFun/UP.con
-cic:/matita/algebra/CoRN/SetoidFun/Tlist_rect.con
-cic:/matita/algebra/CoRN/SetoidFun/Tlist_rec.con
-cic:/matita/algebra/CoRN/SetoidFun/Tlist_ind.con
-cic:/matita/algebra/CoRN/SetoidFun/Tlist.ind
-cic:/matita/algebra/CoRN/SetoidFun/Tapp.con
-cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom1.con
-cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_pfdom.con
-cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom1.con
-cic:/matita/algebra/CoRN/SetoidFun/Prop_OF_bpfdom.con
-cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rect.con
-cic:/matita/algebra/CoRN/SetoidFun/PartFunct_rec.con
-cic:/matita/algebra/CoRN/SetoidFun/PartFunct_ind.con
-cic:/matita/algebra/CoRN/SetoidFun/PartFunct.ind
-cic:/matita/algebra/CoRN/SetoidFun/Inv_bij.con
-cic:/matita/algebra/CoRN/SetoidFun/Inv.con
-cic:/matita/algebra/CoRN/SetoidFun/Fid.con
-cic:/matita/algebra/CoRN/SetoidFun/Fconst.con
-cic:/matita/algebra/CoRN/SetoidFun/Fcomp.con
-cic:/matita/algebra/CoRN/SetoidFun/FS_is_CSetoid.con
-cic:/matita/algebra/CoRN/SetoidFun/FS_as_CSetoid.con
-cic:/matita/algebra/CoRN/SetoidFun/Dir_bij.con
-cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rect.con
-cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_rec.con
-cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun_ind.con
-cic:/matita/algebra/CoRN/SetoidFun/CSetoid_bijective_fun.ind
-cic:/matita/algebra/CoRN/SetoidFun/CSap_fm.con
-cic:/matita/algebra/CoRN/SetoidFun/CAnd_rect.con
-cic:/matita/algebra/CoRN/SetoidFun/CAnd_rec.con
-cic:/matita/algebra/CoRN/SetoidFun/CAnd_ind.con
-cic:/matita/algebra/CoRN/SetoidFun/CAnd.ind
-cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rect.con
-cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_rec.con
-cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct_ind.con
-cic:/matita/algebra/CoRN/SetoidFun/BinPartFunct.ind
-cic:/matita/algebra/CoRN/SetoidFun/BinFcomp.con
-cic:/matita/algebra/CoRN/SetoidFun/BR.con
-cic:/matita/algebra/CoRN/SetoidFun/BQ.con
-cic:/matita/algebra/CoRN/SetoidFun/BP.con
-cic:/matita/algebra/CoRN/SetoidFun/Astar.con
 cic:/matita/algebra/CoRN/SetoidInc/included_trans.con
 cic:/matita/algebra/CoRN/SetoidInc/included_refl.con
 cic:/matita/algebra/CoRN/SetoidInc/included_extend.con
@@ -2064,7 +2086,6 @@ cic:/matita/demo/propositional_sequent_calculus/or_of_list_permut.con
 cic:/matita/demo/propositional_sequent_calculus/or_of_list.con
 cic:/matita/demo/propositional_sequent_calculus/not_nf_inv.con
 cic:/matita/demo/propositional_sequent_calculus/not_nf_ind.con
-cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con
 cic:/matita/demo/propositional_sequent_calculus/not_nf.ind
 cic:/matita/demo/propositional_sequent_calculus/not_eq_nil_append_cons.con
 cic:/matita/demo/propositional_sequent_calculus/negate.con
@@ -2078,47 +2099,6 @@ cic:/matita/demo/propositional_sequent_calculus/eval.con
 cic:/matita/demo/propositional_sequent_calculus/eq_to_eq_mem.con
 cic:/matita/demo/propositional_sequent_calculus/eq_plus_n_m_O_to_eq_m_O.con
 cic:/matita/demo/propositional_sequent_calculus/eq_notb_notb_b_b.con
-cic:/matita/demo/propositional_sequent_calculus/eq_eval_elim_not_eval.con
-cic:/matita/demo/propositional_sequent_calculus/elim_not.con
-cic:/matita/demo/propositional_sequent_calculus/distributive_orb_andb.con
-cic:/matita/demo/propositional_sequent_calculus/distributive_andb_orb.con
-cic:/matita/demo/propositional_sequent_calculus/derive_inv.con
-cic:/matita/demo/propositional_sequent_calculus/derive_ind.con
-cic:/matita/demo/propositional_sequent_calculus/derive.ind
-cic:/matita/demo/propositional_sequent_calculus/demorgan2.con
-cic:/matita/demo/propositional_sequent_calculus/demorgan1.con
-cic:/matita/demo/propositional_sequent_calculus/daemon.con
-cic:/matita/demo/propositional_sequent_calculus/completeness_base.con
-cic:/matita/demo/propositional_sequent_calculus/associative_andb.con
-cic:/matita/demo/propositional_sequent_calculus/assoc_orb.con
-cic:/matita/demo/propositional_sequent_calculus/and_of_list_permut.con
-cic:/matita/demo/propositional_sequent_calculus/and_of_list.con
-cic:/matita/demo/propositional_sequent_calculus/Formula_rect.con
-cic:/matita/demo/propositional_sequent_calculus/Formula_rec.con
-cic:/matita/demo/propositional_sequent_calculus/Formula_ind.con
-cic:/matita/demo/propositional_sequent_calculus/Formula.ind
-cic:/matita/demo/realisability/type_OF_SP.con
-cic:/matita/demo/realisability/true_impl_realized.con
-cic:/matita/demo/realisability/sigma_rect.con
-cic:/matita/demo/realisability/sigma_rec.con
-cic:/matita/demo/realisability/sigma_ind.con
-cic:/matita/demo/realisability/sigma.ind
-cic:/matita/demo/realisability/realized.con
-cic:/matita/demo/realisability/pi2.con
-cic:/matita/demo/realisability/pi1.con
-cic:/matita/demo/realisability/modr.con
-cic:/matita/demo/realisability/id_axiom.con
-cic:/matita/demo/realisability/extraction.con
-cic:/matita/demo/realisability/elim_abs.con
-cic:/matita/demo/realisability/cut.con
-cic:/matita/demo/realisability/correct2.con
-cic:/matita/demo/realisability/correct.con
-cic:/matita/demo/realisability/and_i.con
-cic:/matita/demo/realisability/SP_rect.con
-cic:/matita/demo/realisability/SP_rec.con
-cic:/matita/demo/realisability/SP_ind.con
-cic:/matita/demo/realisability/SP.ind
-cic:/matita/demo/realisability/Prop_OF_SP.con
 cic:/matita/technicalities/setoids/variance_rect.con
 cic:/matita/technicalities/setoids/variance_rec.con
 cic:/matita/technicalities/setoids/variance_of_argument_class.con
@@ -2129,11 +2109,11 @@ cic:/matita/technicalities/setoids/rewrite_direction_rec.con
 cic:/matita/technicalities/setoids/rewrite_direction_ind.con
 cic:/matita/technicalities/setoids/rewrite_direction.ind
 cic:/matita/technicalities/setoids/relation_of_relation_class.con
-cic:/matita/technicalities/setoids/relation_of_product_of_arguments.con
 cic:/matita/technicalities/setoids/relation_of_areflexive_relation_class.con
 cic:/matita/technicalities/setoids/relation_class_of_reflexive_relation_class.con
 cic:/matita/technicalities/setoids/relation_class_of_argument_class.con
 cic:/matita/technicalities/setoids/relation_class_of_areflexive_relation_class.con
+cic:/matita/technicalities/setoids/relation_of_product_of_arguments.con
 cic:/matita/technicalities/setoids/product_of_arguments.con
 cic:/matita/technicalities/setoids/opposite_direction_idempotent.con
 cic:/matita/technicalities/setoids/opposite_direction.con
@@ -2203,3 +2183,25 @@ cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rect.con
 cic:/matita/technicalities/setoids/Areflexive_Relation_Class_rec.con
 cic:/matita/technicalities/setoids/Areflexive_Relation_Class_ind.con
 cic:/matita/technicalities/setoids/Areflexive_Relation_Class.ind
+# # mutual fix
+# cic:/matita/demo/propositional_sequent_calculus/not_nf_elim_not.con
+# # depending on the previous
+# cic:/matita/demo/propositional_sequent_calculus/eq_eval_elim_not_eval.con
+# cic:/matita/demo/propositional_sequent_calculus/elim_not.con
+# cic:/matita/demo/propositional_sequent_calculus/distributive_orb_andb.con
+# cic:/matita/demo/propositional_sequent_calculus/distributive_andb_orb.con
+# cic:/matita/demo/propositional_sequent_calculus/derive_inv.con
+# cic:/matita/demo/propositional_sequent_calculus/derive_ind.con
+# cic:/matita/demo/propositional_sequent_calculus/derive.ind
+# cic:/matita/demo/propositional_sequent_calculus/demorgan2.con
+# cic:/matita/demo/propositional_sequent_calculus/demorgan1.con
+# cic:/matita/demo/propositional_sequent_calculus/daemon.con
+# cic:/matita/demo/propositional_sequent_calculus/completeness_base.con
+# cic:/matita/demo/propositional_sequent_calculus/associative_andb.con
+# cic:/matita/demo/propositional_sequent_calculus/assoc_orb.con
+# cic:/matita/demo/propositional_sequent_calculus/and_of_list_permut.con
+# cic:/matita/demo/propositional_sequent_calculus/and_of_list.con
+# cic:/matita/demo/propositional_sequent_calculus/Formula_rect.con
+# cic:/matita/demo/propositional_sequent_calculus/Formula_rec.con
+# cic:/matita/demo/propositional_sequent_calculus/Formula_ind.con
+# cic:/matita/demo/propositional_sequent_calculus/Formula.ind