X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2Falluris.txt;h=0d49a6a7425a76edabbad17f91dfb6a623516729;hb=a03741c70a531bdfcc97eddca21e30eb3cd82073;hp=10afda9d9c2abc8d92d9016c828c34eadc889712;hpb=c622da7bd4b14f5953424e09f32c14f74d681a3f;p=helm.git diff --git a/helm/software/components/ng_kernel/alluris.txt b/helm/software/components/ng_kernel/alluris.txt index 10afda9d9..0d49a6a74 100644 --- a/helm/software/components/ng_kernel/alluris.txt +++ b/helm/software/components/ng_kernel/alluris.txt @@ -1,761 +1,573 @@ -cic:/matita/tests/absurd/stupid.con -cic:/matita/tests/apply2/test.con -cic:/matita/tests/apply/a.con -cic:/matita/tests/apply/b.con -cic:/matita/tests/apply/c.con -cic:/matita/tests/apply/d.con -cic:/matita/tests/applys/foo.con -cic:/matita/tests/applys/prova2.con -cic:/matita/tests/applys/prova.con -cic:/matita/tests/assumption/stupid.con -cic:/matita/tests/bad_induction/absurd.con -cic:/matita/tests/bad_induction/bad_ind.con -cic:/matita/tests/bool/bool507.con -cic:/matita/tests/change/stupid.con -cic:/matita/tests/change/t.con -cic:/matita/tests/clearbody/stupid.con -cic:/matita/tests/clear/stupid.con -cic:/matita/tests/coercions/a.con -cic:/matita/tests/coercions/c1.con -cic:/matita/tests/coercions/c2.con -cic:/matita/tests/coercions/c3.con -cic:/matita/tests/coercions/c4.con -cic:/matita/tests/coercions/church.con -cic:/matita/tests/coercions_contravariant/A1.con -cic:/matita/tests/coercions_contravariant/A.con -cic:/matita/tests/coercions_contravariant/B1.con -cic:/matita/tests/coercions_contravariant/B.con -cic:/matita/tests/coercions_contravariant/c.con -cic:/matita/tests/coercions_contravariant/d.con -cic:/matita/tests/coercions_contravariant/f.con -cic:/matita/tests/coercions_contravariant/foo1_1.con -cic:/matita/tests/coercions_contravariant/foo2.con -cic:/matita/tests/coercions_contravariant/foo3.con -cic:/matita/tests/coercions_contravariant/foo4.con -cic:/matita/tests/coercions_contravariant/foo.con -cic:/matita/tests/coercions_contravariant/g.con -cic:/matita/tests/coercions_contravariant/h.con -cic:/matita/tests/coercions_dependent/c.con -cic:/matita/tests/coercions_dependent/vec.ind -cic:/matita/tests/coercions_dependent/vec_ind.con -cic:/matita/tests/coercions_dependent/vec_inv.con -cic:/matita/tests/coercions_dependent/veclen.con -cic:/matita/tests/coercions_dependent/vec_rec.con -cic:/matita/tests/coercions_dependent/vec_rect.con -cic:/matita/tests/coercions_dependent/xxx.con -cic:/matita/tests/coercions/double1.con -cic:/matita/tests/coercions/double2.con -cic:/matita/tests/coercions/double.con -cic:/matita/tests/coercions/empty.ind -cic:/matita/tests/coercions/empty_ind.con -cic:/matita/tests/coercions/empty_rec.con -cic:/matita/tests/coercions/empty_rect.con -cic:/matita/tests/coercions/f.con -cic:/matita/tests/coercions/foo01.con -cic:/matita/tests/coercions/foo0.con -cic:/matita/tests/coercions/foo.con -cic:/matita/tests/coercions/fst.con -cic:/matita/tests/coercions/i2pos.con -cic:/matita/tests/coercions/if.con -cic:/matita/tests/coercions/initial.ind -cic:/matita/tests/coercions/initial_ind.con -cic:/matita/tests/coercions/initial_rec.con -cic:/matita/tests/coercions/initial_rect.con -cic:/matita/tests/coercions/int.ind -cic:/matita/tests/coercions/int_ind.con -cic:/matita/tests/coercions/int_OF_initial.con -cic:/matita/tests/coercions/int_OF_pos.con -cic:/matita/tests/coercions/int_rec.con -cic:/matita/tests/coercions/int_rect.con -cic:/matita/tests/coercions/ith.con -cic:/matita/tests/coercions/listn2function.con -cic:/matita/tests/coercions/listn.ind -cic:/matita/tests/coercions/listn_ind.con -cic:/matita/tests/coercions/listn_inv.con -cic:/matita/tests/coercions/listn_rec.con -cic:/matita/tests/coercions/listn_rect.con -cic:/matita/tests/coercions/map.con -cic:/matita/tests/coercions/mapmult.con -cic:/matita/tests/coercions/nat2int.con -cic:/matita/tests/coercions/natlist2map.con -cic:/matita/tests/coercions/nat_OF_initial.con -cic:/matita/tests/coercions_nonuniform/A.con -cic:/matita/tests/coercions_nonuniform/B.con -cic:/matita/tests/coercions_nonuniform/B_OF_A.con -cic:/matita/tests/coercions_nonuniform/c1.con -cic:/matita/tests/coercions_nonuniform/c2.con -cic:/matita/tests/coercions_nonuniform/C.con -cic:/matita/tests/coercions_nonuniform/C_OF_A.con -cic:/matita/tests/coercions_nonuniform/C_OF_B.con -cic:/matita/tests/coercions_nonuniform/f1.con -cic:/matita/tests/coercions_nonuniform/f.con -cic:/matita/tests/coercions_nonuniform/g.con -cic:/matita/tests/coercions_nonuniform/k.con -cic:/matita/tests/coercions_nonuniform/test.con -cic:/matita/tests/coercions_open/AB.con -cic:/matita/tests/coercions_open/A.con -cic:/matita/tests/coercions_open/A_OF_A.con -cic:/matita/tests/coercions_open/B.con -cic:/matita/tests/coercions_open/B_OF_A.con -cic:/matita/tests/coercions_open/B_OF_B.con -cic:/matita/tests/coercions_open/daemon.con -cic:/matita/tests/coercions_open/eatA.con -cic:/matita/tests/coercions_open/eatB.con -cic:/matita/tests/coercions_open/jmcAB.con -cic:/matita/tests/coercions_open/jmcBA.con -cic:/matita/tests/coercions_open/xx.con -cic:/matita/tests/coercions/pos2nat.con -cic:/matita/tests/coercions/pos2nat'.con -cic:/matita/tests/coercions/pos.ind -cic:/matita/tests/coercions/pos_ind.con -cic:/matita/tests/coercions/pos_rec.con -cic:/matita/tests/coercions/pos_rect.con -cic:/matita/tests/coercions_propagation/eject.con -cic:/matita/tests/coercions_propagation/ejectN.con -cic:/matita/tests/coercions_propagation/f1.con -cic:/matita/tests/coercions_propagation/f.con -cic:/matita/tests/coercions_propagation/F.con -cic:/matita/tests/coercions_propagation/inject.con -cic:/matita/tests/coercions_propagation/injectN.con -cic:/matita/tests/coercions_propagation/NN.ind -cic:/matita/tests/coercions_propagation/NN_ind.con -cic:/matita/tests/coercions_propagation/NN_inv.con -cic:/matita/tests/coercions_propagation/NN_OF_NN.con -cic:/matita/tests/coercions_propagation/NN_rec.con -cic:/matita/tests/coercions_propagation/NN_rect.con -cic:/matita/tests/coercions_propagation/PN.con -cic:/matita/tests/coercions_propagation/sigma.ind -cic:/matita/tests/coercions_propagation/sigma_ind.con -cic:/matita/tests/coercions_propagation/sigma_OF_NN.con -cic:/matita/tests/coercions_propagation/sigma_OF_sigma1.con -cic:/matita/tests/coercions_propagation/sigma_OF_sigma.con -cic:/matita/tests/coercions_propagation/sigma_rec.con -cic:/matita/tests/coercions_propagation/sigma_rect.con -cic:/matita/tests/coercions_propagation/test2.con -cic:/matita/tests/coercions_propagation/test3.con -cic:/matita/tests/coercions_propagation/test4.con -cic:/matita/tests/coercions_propagation/test51_byhand.con -cic:/matita/tests/coercions_propagation/test51.con -cic:/matita/tests/coercions_propagation/test522.con -cic:/matita/tests/coercions_propagation/test5.con -cic:/matita/tests/coercions_propagation/test.con -cic:/matita/tests/coercions_russell/bind.con -cic:/matita/tests/coercions_russell/eject.con -cic:/matita/tests/coercions_russell/eject_opt.con -cic:/matita/tests/coercions_russell/f.con -cic:/matita/tests/coercions_russell/find_spec.con -cic:/matita/tests/coercions_russell/hd.con -cic:/matita/tests/coercions_russell/inject.con -cic:/matita/tests/coercions_russell/inject_opt.con -cic:/matita/tests/coercions_russell/list_OF_list.con -cic:/matita/tests/coercions_russell/mem_x_to_ex_l1_l2.con -cic:/matita/tests/coercions_russell/nat_return.con -cic:/matita/tests/coercions_russell/option_OF_nat.con -cic:/matita/tests/coercions_russell/option_OF_option.con -cic:/matita/tests/coercions_russell/raise_exn.con -cic:/matita/tests/coercions_russell/sigma_find_spec.con -cic:/matita/tests/coercions_russell/sigma.ind -cic:/matita/tests/coercions_russell/sigma_ind.con -cic:/matita/tests/coercions_russell/sigma_OF_list.con -cic:/matita/tests/coercions_russell/sigma_OF_nat1.con -cic:/matita/tests/coercions_russell/sigma_OF_nat.con -cic:/matita/tests/coercions_russell/sigma_OF_option.con -cic:/matita/tests/coercions_russell/sigma_OF_sigma1.con -cic:/matita/tests/coercions_russell/sigma_OF_sigma.con -cic:/matita/tests/coercions_russell/sigma_rec.con -cic:/matita/tests/coercions_russell/sigma_rect.con -cic:/matita/tests/coercions_russell/tl2.con -cic:/matita/tests/coercions_russell/tl.con -cic:/matita/tests/coercions_russell/try_with.con -cic:/matita/tests/coercions/T0.con -cic:/matita/tests/coercions/T1.con -cic:/matita/tests/coercions/T1_OF_T0.con -cic:/matita/tests/coercions/T2.con -cic:/matita/tests/coercions/T2_OF_T0.con -cic:/matita/tests/coercions/T3.con -cic:/matita/tests/coercions/T3_OF_T01.con -cic:/matita/tests/coercions/T3_OF_T0.con -cic:/matita/tests/coercions/T3_OF_T1.con -cic:/matita/tests/coercions/T3_OF_T2.con -cic:/matita/tests/comments/a.con -cic:/matita/tests/compose/an_1.con -cic:/matita/tests/constructor/stupid.con -cic:/matita/tests/continuationals/branch.con -cic:/matita/tests/continuationals/dot.con -cic:/matita/tests/continuationals/dot_slice.con -cic:/matita/tests/continuationals/focus.con -cic:/matita/tests/continuationals/pos.con -cic:/matita/tests/continuationals/semicolon.con -cic:/matita/tests/continuationals/skip.con -cic:/matita/tests/continuationals/skip_focus.con -cic:/matita/tests/contradiction/stupid.con -cic:/matita/tests/cut/stupid.con -cic:/matita/tests/decl/easy15.con -cic:/matita/tests/decl/easy2.con -cic:/matita/tests/decl/easy3.con -cic:/matita/tests/decl/easy45.con -cic:/matita/tests/decl/easy4.con -cic:/matita/tests/decl/easy5.con -cic:/matita/tests/decl/easy6.con -cic:/matita/tests/decl/easy.con -cic:/matita/tests/decl/size.con -cic:/matita/tests/decl/tree.ind -cic:/matita/tests/decl/tree_ind.con -cic:/matita/tests/decl/tree_rec.con -cic:/matita/tests/decl/tree_rect.con -cic:/matita/tests/decompose/ex_falso_quodlibet.con -cic:/matita/tests/decompose/MyFalse.con -cic:/matita/tests/decompose/stupid.con -cic:/matita/tests/dependent_type_inference/foo.con -cic:/matita/tests/elim/foo.con -cic:/matita/tests/elim/serious.con -cic:/matita/tests/elim/stupidtype.ind -cic:/matita/tests/elim/stupidtype_ind.con -cic:/matita/tests/elim/stupidtype_rec.con -cic:/matita/tests/elim/stupidtype_rect.con -cic:/matita/tests/elim/sum.ind -cic:/matita/tests/elim/sum_ind.con -cic:/matita/tests/elim/sum_inv.con -cic:/matita/tests/elim/sum_rec.con -cic:/matita/tests/elim/sum_rect.con -cic:/matita/tests/elim/t.con -cic:/matita/tests/elim/t'.con -cic:/matita/tests/fguidi/eq_gen_S_O_cc.con -cic:/matita/tests/fguidi/eq_gen_S_O.con -cic:/matita/tests/fguidi/eq_gen_S_S_cc.con -cic:/matita/tests/fguidi/eq_gen_S_S.con -cic:/matita/tests/fguidi/is_S.con -cic:/matita/tests/fguidi/le_gen_S_S_cc.con -cic:/matita/tests/fguidi/le_gen_S_S.con -cic:/matita/tests/fguidi/le_gen_S_x_aux.con -cic:/matita/tests/fguidi/le_gen_S_x_cc.con -cic:/matita/tests/fguidi/le_gen_S_x.con -cic:/matita/tests/fguidi/le_gen_x_O_aux.con -cic:/matita/tests/fguidi/le_gen_x_O_cc.con -cic:/matita/tests/fguidi/le_gen_x_O.con -cic:/matita/tests/fguidi/le.ind -cic:/matita/tests/fguidi/le_ind.con -cic:/matita/tests/fguidi/le_inv.con -cic:/matita/tests/fguidi/le_refl.con -cic:/matita/tests/fguidi/pred.con -cic:/matita/tests/first/eq.ind -cic:/matita/tests/first/eq_ind.con -cic:/matita/tests/first/list.ind -cic:/matita/tests/first/list_ind.con -cic:/matita/tests/first/list_len.con -cic:/matita/tests/first/list_rec.con -cic:/matita/tests/first/list_rect.con -cic:/matita/tests/first/nat.ind -cic:/matita/tests/first/nat_ind.con -cic:/matita/tests/first/nat_rec.con -cic:/matita/tests/first/nat_rect.con -cic:/matita/tests/first/stupid.con -cic:/matita/tests/fix_betareduction/a.con -cic:/matita/tests/fold/t.con -cic:/matita/tests/generalize/t.con -cic:/matita/tests/generalize/test2.con -cic:/matita/tests/hard_refine/prove_add_multiply.con -cic:/matita/tests/injection/injection_test0.con -cic:/matita/tests/injection/injection_test1.con -cic:/matita/tests/injection/injection_test2.con -cic:/matita/tests/injection/injection_test4.con -cic:/matita/tests/injection/t0.ind -cic:/matita/tests/injection/t0_ind.con -cic:/matita/tests/injection/t0_rec.con -cic:/matita/tests/injection/t0_rect.con -cic:/matita/tests/injection/t.ind -cic:/matita/tests/injection/t_ind.con -cic:/matita/tests/injection/t_inv.con -cic:/matita/tests/injection/t_rec.con -cic:/matita/tests/injection/t_rect.con -cic:/matita/tests/injection/tt.ind -cic:/matita/tests/injection/tt_ind.con -cic:/matita/tests/injection/tt_inv.con -cic:/matita/tests/injection/tt_rec.con -cic:/matita/tests/injection/tt_rect.con -cic:/matita/tests/injection/ttree.ind -cic:/matita/tests/injection/ttree_ind.con -cic:/matita/tests/injection/ttree_inv.con -cic:/matita/tests/injection/ttree_rec.con -cic:/matita/tests/injection/ttree_rect.con -cic:/matita/tests/inversion2/ledx.ind -cic:/matita/tests/inversion2/ledx_ind.con -cic:/matita/tests/inversion2/ledx_inv.con -cic:/matita/tests/inversion2/le.ind -cic:/matita/tests/inversion2/le_ind.con -cic:/matita/tests/inversion2/le_inv2.con -cic:/matita/tests/inversion2/le_inv.con -cic:/matita/tests/inversion2/nat.ind -cic:/matita/tests/inversion2/nat_ind.con -cic:/matita/tests/inversion2/nat_rec.con -cic:/matita/tests/inversion2/nat_rect.con -cic:/matita/tests/inversion2/test_inversion.con -cic:/matita/tests/inversion/sum.ind -cic:/matita/tests/inversion/sum_ind.con -cic:/matita/tests/inversion/sum_inv.con -cic:/matita/tests/inversion/sum_rec.con -cic:/matita/tests/inversion/sum_rect.con -cic:/matita/tests/inversion/t1.con -cic:/matita/tests/inversion/t.con -cic:/matita/tests/letrecand/dispari2.con -cic:/matita/tests/letrecand/dispari.con -cic:/matita/tests/letrecand/pari2.con -cic:/matita/tests/letrecand/pari.con -cic:/matita/tests/letrecand/test_dispari2.con -cic:/matita/tests/letrecand/test_dispari.con -cic:/matita/tests/letrecand/test_pari2.con -cic:/matita/tests/letrecand/test_pari.con -cic:/matita/tests/letrec/plus.con -cic:/matita/tests/match_inference/empty2nat.con -cic:/matita/tests/match_inference/empty.ind -cic:/matita/tests/match_inference/empty_ind.con -cic:/matita/tests/match_inference/empty_rec.con -cic:/matita/tests/match_inference/empty_rect.con -cic:/matita/tests/match_inference/fst.con -cic:/matita/tests/match_inference/le.ind -cic:/matita/tests/match_inference/le_ind.con -cic:/matita/tests/match_inference/nat.ind -cic:/matita/tests/match_inference/nat_ind.con -cic:/matita/tests/match_inference/nat_rec.con -cic:/matita/tests/match_inference/nat_rect.con -cic:/matita/tests/match_inference/pos2nat.con -cic:/matita/tests/match_inference/pos.ind -cic:/matita/tests/match_inference/pos_ind.con -cic:/matita/tests/match_inference/pos_rec.con -cic:/matita/tests/match_inference/pos_rect.con -cic:/matita/tests/match_inference/Prod.ind -cic:/matita/tests/match_inference/Prod_ind.con -cic:/matita/tests/match_inference/Prod_rec.con -cic:/matita/tests/match_inference/Prod_rect.con -cic:/matita/tests/match_inference/r.con -cic:/matita/tests/match_inference/True.ind -cic:/matita/tests/match_inference/True_ind.con -cic:/matita/tests/match_inference/True_rec.con -cic:/matita/tests/match_inference/True_rect.con -cic:/matita/tests/metasenv_ordering/th10.con -cic:/matita/tests/metasenv_ordering/th11.con -cic:/matita/tests/metasenv_ordering/th1.con -cic:/matita/tests/metasenv_ordering/th2.con -cic:/matita/tests/metasenv_ordering/th3.con -cic:/matita/tests/metasenv_ordering/th4.con -cic:/matita/tests/metasenv_ordering/th5.con -cic:/matita/tests/metasenv_ordering/th6.con -cic:/matita/tests/metasenv_ordering/th7.con -cic:/matita/tests/metasenv_ordering/th8.con -cic:/matita/tests/metasenv_ordering/th9.con -cic:/matita/tests/multiple_inheritance/C.con -cic:/matita/tests/multiple_inheritance/conv_test.con -cic:/matita/tests/multiple_inheritance/f.con -cic:/matita/tests/multiple_inheritance/K.con -cic:/matita/tests/multiple_inheritance/mult.con -cic:/matita/tests/multiple_inheritance/mult_idempotent.con -cic:/matita/tests/multiple_inheritance/plus.con -cic:/matita/tests/multiple_inheritance/plus_idempotent.con -cic:/matita/tests/multiple_inheritance/r1.con -cic:/matita/tests/multiple_inheritance/R1.ind -cic:/matita/tests/multiple_inheritance/R1_ind.con -cic:/matita/tests/multiple_inheritance/R1_rec.con -cic:/matita/tests/multiple_inheritance/R1_rect.con -cic:/matita/tests/multiple_inheritance/r2_.con -cic:/matita/tests/multiple_inheritance/r2.con -cic:/matita/tests/multiple_inheritance/R2.ind -cic:/matita/tests/multiple_inheritance/R2_ind.con -cic:/matita/tests/multiple_inheritance/R2_rec.con -cic:/matita/tests/multiple_inheritance/R2_rect.con -cic:/matita/tests/multiple_inheritance/R.ind -cic:/matita/tests/multiple_inheritance/R_ind.con -cic:/matita/tests/multiple_inheritance/R_rec.con -cic:/matita/tests/multiple_inheritance/R_rect.con -cic:/matita/tests/multiple_inheritance/test.con -cic:/matita/tests/multiple_inheritance/Type_OF_R.con -cic:/matita/tests/multiple_inheritance/with_.con -cic:/matita/tests/mysql_escaping/a'.con -cic:/matita/tests/naiveparamod/prova1.con -cic:/matita/tests/naiveparamod/prova2.con -cic:/matita/tests/naiveparamod/TT.ind -cic:/matita/tests/naiveparamod/TT_ind.con -cic:/matita/tests/naiveparamod/TT_rec.con -cic:/matita/tests/naiveparamod/TT_rect.con -cic:/matita/tests/overred/c.con -cic:/matita/tests/overred/daemon.con -cic:/matita/tests/overred/find_a_coercion_from_T2_for_a_term_in_T3.con -cic:/matita/tests/overred/T1.con -cic:/matita/tests/overred/T2.con -cic:/matita/tests/overred/t3.con -cic:/matita/tests/overred/T3.con -cic:/matita/tests/overred/x.con -cic:/matita/tests/overred/X.con -cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r.con -cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r'.con -cic:/matita/tests/paramodulation/BOO075-1/eq_elim_r''.con -cic:/matita/tests/paramodulation/BOO075-1/eq_f1.con -cic:/matita/tests/paramodulation/BOO075-1/eq_f.con -cic:/matita/tests/paramodulation/BOO075-1/eq.ind -cic:/matita/tests/paramodulation/BOO075-1/eq_ind.con -cic:/matita/tests/paramodulation/BOO075-1/eq_rec.con -cic:/matita/tests/paramodulation/BOO075-1/eq_rect.con -cic:/matita/tests/paramodulation/BOO075-1/ex.ind -cic:/matita/tests/paramodulation/BOO075-1/ex_ind.con -cic:/matita/tests/paramodulation/BOO075-1/prove_meredith_2_basis_1.con -cic:/matita/tests/paramodulation/BOO075-1/sym_eq.con -cic:/matita/tests/paramodulation/BOO075-1/trans_eq.con -cic:/matita/tests/paramodulation/boolean_algebra/bool5.con -cic:/matita/tests/paramodulation/boolean_algebra/bool_algebra.con -cic:/matita/tests/paramodulation/group/GRP049.con -cic:/matita/tests/paramodulation/group/GRP049_simple.con -cic:/matita/tests/paramodulation/group/self.con -cic:/matita/tests/paramodulation/para1.con -cic:/matita/tests/paramodulation/para2.con -cic:/matita/tests/pullback/L.ind -cic:/matita/tests/pullback/L_ind.con -cic:/matita/tests/pullback/L_OF_R1.con -cic:/matita/tests/pullback/L_rec.con -cic:/matita/tests/pullback/L_rect.con -cic:/matita/tests/pullback/L_to_T.con -cic:/matita/tests/pullback/P1.ind -cic:/matita/tests/pullback/P1_ind.con -cic:/matita/tests/pullback/P1_rec.con -cic:/matita/tests/pullback/P1_rect.con -cic:/matita/tests/pullback/P1_to_L.con -cic:/matita/tests/pullback/P1_to_P1.con -cic:/matita/tests/pullback/P1_to_R1.con -cic:/matita/tests/pullback/P2.ind -cic:/matita/tests/pullback/P2_ind.con -cic:/matita/tests/pullback/P2_OF_P1.con -cic:/matita/tests/pullback/P2_rec.con -cic:/matita/tests/pullback/P2_rect.con -cic:/matita/tests/pullback/P2_to_L.con -cic:/matita/tests/pullback/P2_to_R.con -cic:/matita/tests/pullback/R1.ind -cic:/matita/tests/pullback/R1_ind.con -cic:/matita/tests/pullback/R1_rec.con -cic:/matita/tests/pullback/R1_rect.con -cic:/matita/tests/pullback/R1_to_P2.con -cic:/matita/tests/pullback/R1_to_R.con -cic:/matita/tests/pullback/R.ind -cic:/matita/tests/pullback/R_ind.con -cic:/matita/tests/pullback/R_OF_P1.con -cic:/matita/tests/pullback/R_rec.con -cic:/matita/tests/pullback/R_rect.con -cic:/matita/tests/pullback/R_to_T.con -cic:/matita/tests/pullback/T.ind -cic:/matita/tests/pullback/T_ind.con -cic:/matita/tests/pullback/T_OF_P1.con -cic:/matita/tests/pullback/T_OF_P2.con -cic:/matita/tests/pullback/T_OF_R1.con -cic:/matita/tests/pullback/T_rec.con -cic:/matita/tests/pullback/T_rect.con -cic:/matita/tests/record/a.con -cic:/matita/tests/record/b.con -cic:/matita/tests/record/c.con -cic:/matita/tests/record/d.con -cic:/matita/tests/record/e.con -cic:/matita/tests/record/empty.ind -cic:/matita/tests/record/empty_ind.con -cic:/matita/tests/record/empty_rec.con -cic:/matita/tests/record/empty_rect.con -cic:/matita/tests/record/f.con -cic:/matita/tests/record/mario.con -cic:/matita/tests/record/paperino.ind -cic:/matita/tests/record/paperino_ind.con -cic:/matita/tests/record/piero.con -cic:/matita/tests/record/pippo.ind -cic:/matita/tests/record/pippo_ind.con -cic:/matita/tests/record/pippo_rec.con -cic:/matita/tests/record/pippo_rect.con -cic:/matita/tests/record/pluto.ind -cic:/matita/tests/record/pluto_ind.con -cic:/matita/tests/record/pluto_rec.con -cic:/matita/tests/record/pluto_rect.con -cic:/matita/tests/record/t.ind -cic:/matita/tests/record/t_ind.con -cic:/matita/tests/record/t_rec.con -cic:/matita/tests/record/t_rect.con -cic:/matita/tests/record/True.ind -cic:/matita/tests/record/True_ind.con -cic:/matita/tests/record/True_rec.con -cic:/matita/tests/record/True_rect.con -cic:/matita/tests/replace/t2.con -cic:/matita/tests/replace/t.con -cic:/matita/tests/rewrite/a.con -cic:/matita/tests/rewrite/foo.con -cic:/matita/tests/rewrite/t.con -cic:/matita/tests/rewrite/test_rewrite_in_hyp2.con -cic:/matita/tests/rewrite/test_rewrite_in_hyp.con -cic:/matita/tests/rewrite/test_rewrite_under_pi.con -cic:/matita/tests/second/ultrastupid.con -cic:/matita/tests/simpl/R.con -cic:/matita/tests/simpl/t.con -cic:/matita/tests/simpl/X.con -cic:/matita/tests/tacticals/myand.ind -cic:/matita/tests/tacticals/myand_ind.con -cic:/matita/tests/tacticals/myand_rec.con -cic:/matita/tests/tacticals/myand_rect.con -cic:/matita/tests/tacticals/prova2.con -cic:/matita/tests/tacticals/prova3.con -cic:/matita/tests/tacticals/prova4.con -cic:/matita/tests/tacticals/prova6.con -cic:/matita/tests/tacticals/prova.con -cic:/matita/tests/test2/a.con -cic:/matita/tests/test3/a.con -cic:/matita/tests/test3/b.con -cic:/matita/tests/test4/a.con -cic:/matita/tests/third/iperstupid.con -cic:/matita/tests/tinycals/prova1.con -cic:/matita/tests/tinycals/prova2.con -cic:/matita/tests/tinycals/prova.con -cic:/matita/tests/TPTP/Veloci/BOO001-1.p/prove_inverse_is_self_cancelling.con -cic:/matita/tests/TPTP/Veloci/BOO003-2.p/prove_a_times_a_is_a.con -cic:/matita/tests/TPTP/Veloci/BOO003-4.p/prove_a_times_a_is_a.con -cic:/matita/tests/TPTP/Veloci/BOO004-2.p/prove_a_plus_a_is_a.con -cic:/matita/tests/TPTP/Veloci/BOO004-4.p/prove_a_plus_a_is_a.con -cic:/matita/tests/TPTP/Veloci/BOO005-2.p/prove_a_plus_1_is_a.con -cic:/matita/tests/TPTP/Veloci/BOO005-4.p/prove_a_plus_1_is_a.con -cic:/matita/tests/TPTP/Veloci/BOO006-2.p/prove_right_identity.con -cic:/matita/tests/TPTP/Veloci/BOO006-4.p/prove_right_identity.con -cic:/matita/tests/TPTP/Veloci/BOO009-2.p/prove_operation.con -cic:/matita/tests/TPTP/Veloci/BOO009-4.p/prove_operation.con -cic:/matita/tests/TPTP/Veloci/BOO010-2.p/prove_a_plus_ab_is_a.con -cic:/matita/tests/TPTP/Veloci/BOO010-4.p/prove_a_plus_ab_is_a.con -cic:/matita/tests/TPTP/Veloci/BOO011-2.p/prove_inverse_of_1_is_0.con -cic:/matita/tests/TPTP/Veloci/BOO011-4.p/prove_inverse_of_1_is_0.con -cic:/matita/tests/TPTP/Veloci/BOO012-2.p/prove_inverse_is_an_involution.con -cic:/matita/tests/TPTP/Veloci/BOO012-4.p/prove_inverse_is_an_involution.con -cic:/matita/tests/TPTP/Veloci/BOO013-2.p/prove_b_is_a.con -cic:/matita/tests/TPTP/Veloci/BOO013-4.p/prove_a_inverse_is_b.con -cic:/matita/tests/TPTP/Veloci/BOO016-2.p/prove_sum.con -cic:/matita/tests/TPTP/Veloci/BOO017-2.p/prove_sum.con -cic:/matita/tests/TPTP/Veloci/BOO018-4.p/prove_inverse_of_1_is_0.con -cic:/matita/tests/TPTP/Veloci/BOO034-1.p/prove_single_axiom.con -cic:/matita/tests/TPTP/Veloci/BOO069-1.p/prove_tba_axioms_3.con -cic:/matita/tests/TPTP/Veloci/BOO071-1.p/prove_tba_axioms_5.con -cic:/matita/tests/TPTP/Veloci/BOO075-1.p/prove_meredith_2_basis_1.con -cic:/matita/tests/TPTP/Veloci/COL004-3.p/prove_u_combinator.con -cic:/matita/tests/TPTP/Veloci/COL007-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL008-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL010-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL012-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL013-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL014-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL015-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL016-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL017-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL018-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL021-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL022-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL024-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL025-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL045-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL048-1.p/prove_fixed_point.con -cic:/matita/tests/TPTP/Veloci/COL050-1.p/prove_all_fond_of_another.con -cic:/matita/tests/TPTP/Veloci/COL058-2.p/prove_the_bird_exists.con -cic:/matita/tests/TPTP/Veloci/COL058-3.p/prove_the_bird_exists.con -cic:/matita/tests/TPTP/Veloci/COL060-2.p/prove_q_combinator.con -cic:/matita/tests/TPTP/Veloci/COL060-3.p/prove_q_combinator.con -cic:/matita/tests/TPTP/Veloci/COL061-2.p/prove_q1_combinator.con -cic:/matita/tests/TPTP/Veloci/COL061-3.p/prove_q1_combinator.con -cic:/matita/tests/TPTP/Veloci/COL062-2.p/prove_c_combinator.con -cic:/matita/tests/TPTP/Veloci/COL062-3.p/prove_c_combinator.con -cic:/matita/tests/TPTP/Veloci/COL063-2.p/prove_f_combinator.con -cic:/matita/tests/TPTP/Veloci/COL063-3.p/prove_f_combinator.con -cic:/matita/tests/TPTP/Veloci/COL063-4.p/prove_f_combinator.con -cic:/matita/tests/TPTP/Veloci/COL063-5.p/prove_f_combinator.con -cic:/matita/tests/TPTP/Veloci/COL063-6.p/prove_f_combinator.con -cic:/matita/tests/TPTP/Veloci/COL064-2.p/prove_v_combinator.con -cic:/matita/tests/TPTP/Veloci/COL064-3.p/prove_v_combinator.con -cic:/matita/tests/TPTP/Veloci/COL064-4.p/prove_v_combinator.con -cic:/matita/tests/TPTP/Veloci/COL064-5.p/prove_v_combinator.con -cic:/matita/tests/TPTP/Veloci/COL064-6.p/prove_v_combinator.con -cic:/matita/tests/TPTP/Veloci/COL064-7.p/prove_v_combinator.con -cic:/matita/tests/TPTP/Veloci/COL064-8.p/prove_v_combinator.con -cic:/matita/tests/TPTP/Veloci/COL064-9.p/prove_v_combinator.con -cic:/matita/tests/TPTP/Veloci/GRP001-2.p/prove_b_times_a_is_c.con -cic:/matita/tests/TPTP/Veloci/GRP001-4.p/prove_b_times_a_is_c.con -cic:/matita/tests/TPTP/Veloci/GRP010-4.p/prove_b_times_c_is_e.con -cic:/matita/tests/TPTP/Veloci/GRP011-4.p/prove_left_cancellation.con -cic:/matita/tests/TPTP/Veloci/GRP012-4.p/prove_inverse_of_product_is_product_of_inverses.con -cic:/matita/tests/TPTP/Veloci/GRP022-2.p/prove_inverse_of_inverse_is_original.con -cic:/matita/tests/TPTP/Veloci/GRP023-2.p/prove_inverse_of_id_is_id.con -cic:/matita/tests/TPTP/Veloci/GRP115-1.p/prove_order3.con -cic:/matita/tests/TPTP/Veloci/GRP116-1.p/prove_order3.con -cic:/matita/tests/TPTP/Veloci/GRP117-1.p/prove_order3.con -cic:/matita/tests/TPTP/Veloci/GRP118-1.p/prove_order3.con -cic:/matita/tests/TPTP/Veloci/GRP136-1.p/prove_ax_antisyma.con -cic:/matita/tests/TPTP/Veloci/GRP137-1.p/prove_ax_antisymb.con -cic:/matita/tests/TPTP/Veloci/GRP139-1.p/prove_ax_glb1b.con -cic:/matita/tests/TPTP/Veloci/GRP141-1.p/prove_ax_glb1d.con -cic:/matita/tests/TPTP/Veloci/GRP142-1.p/prove_ax_glb2a.con -cic:/matita/tests/TPTP/Veloci/GRP143-1.p/prove_ax_glb2b.con -cic:/matita/tests/TPTP/Veloci/GRP144-1.p/prove_ax_glb3a.con -cic:/matita/tests/TPTP/Veloci/GRP145-1.p/prove_ax_glb3b.con -cic:/matita/tests/TPTP/Veloci/GRP146-1.p/prove_ax_lub1a.con -cic:/matita/tests/TPTP/Veloci/GRP149-1.p/prove_ax_lub1d.con -cic:/matita/tests/TPTP/Veloci/GRP150-1.p/prove_ax_lub2a.con -cic:/matita/tests/TPTP/Veloci/GRP151-1.p/prove_ax_lub2b.con -cic:/matita/tests/TPTP/Veloci/GRP152-1.p/prove_ax_lub3a.con -cic:/matita/tests/TPTP/Veloci/GRP153-1.p/prove_ax_lub3b.con -cic:/matita/tests/TPTP/Veloci/GRP154-1.p/prove_ax_mono1a.con -cic:/matita/tests/TPTP/Veloci/GRP155-1.p/prove_ax_mono1b.con -cic:/matita/tests/TPTP/Veloci/GRP156-1.p/prove_ax_mono1c.con -cic:/matita/tests/TPTP/Veloci/GRP157-1.p/prove_ax_mono2a.con -cic:/matita/tests/TPTP/Veloci/GRP158-1.p/prove_ax_mono2b.con -cic:/matita/tests/TPTP/Veloci/GRP159-1.p/prove_ax_mono2c.con -cic:/matita/tests/TPTP/Veloci/GRP160-1.p/prove_ax_refla.con -cic:/matita/tests/TPTP/Veloci/GRP161-1.p/prove_ax_reflb.con -cic:/matita/tests/TPTP/Veloci/GRP162-1.p/prove_ax_transa.con -cic:/matita/tests/TPTP/Veloci/GRP163-1.p/prove_ax_transb.con -cic:/matita/tests/TPTP/Veloci/GRP168-1.p/prove_p01a.con -cic:/matita/tests/TPTP/Veloci/GRP168-2.p/prove_p01b.con -cic:/matita/tests/TPTP/Veloci/GRP173-1.p/prove_p05a.con -cic:/matita/tests/TPTP/Veloci/GRP174-1.p/prove_p05b.con -cic:/matita/tests/TPTP/Veloci/GRP176-1.p/prove_p07.con -cic:/matita/tests/TPTP/Veloci/GRP176-2.p/prove_p07.con -cic:/matita/tests/TPTP/Veloci/GRP182-1.p/prove_p17a.con -cic:/matita/tests/TPTP/Veloci/GRP182-2.p/prove_p17a.con -cic:/matita/tests/TPTP/Veloci/GRP182-3.p/prove_p17b.con -cic:/matita/tests/TPTP/Veloci/GRP182-4.p/prove_p17b.con -cic:/matita/tests/TPTP/Veloci/GRP186-3.p/prove_p23x.con -cic:/matita/tests/TPTP/Veloci/GRP186-4.p/prove_p23x.con -cic:/matita/tests/TPTP/Veloci/GRP188-1.p/prove_p38a.con -cic:/matita/tests/TPTP/Veloci/GRP188-2.p/prove_p38a.con -cic:/matita/tests/TPTP/Veloci/GRP189-1.p/prove_p38b.con -cic:/matita/tests/TPTP/Veloci/GRP189-2.p/prove_p38b.con -cic:/matita/tests/TPTP/Veloci/GRP192-1.p/prove_p40a.con -cic:/matita/tests/TPTP/Veloci/GRP206-1.p/prove_moufang1.con -cic:/matita/tests/TPTP/Veloci/GRP454-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP455-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP456-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP457-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP458-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP459-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP460-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP463-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP467-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP481-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP484-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP485-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP486-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP487-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP488-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP490-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP491-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP492-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP493-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP494-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP495-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP496-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP497-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP498-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP509-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP510-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP511-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP512-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP513-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP514-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP515-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP516-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP517-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP518-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP520-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP541-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP542-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP543-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP544-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP545-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP546-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP547-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP548-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP549-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP550-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP551-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP552-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP556-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP558-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP560-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP561-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP562-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP564-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP565-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP566-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP567-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP568-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP569-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP570-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP572-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP573-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP574-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP576-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP577-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP578-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP580-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP581-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP582-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP583-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP584-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP586-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP588-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP590-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP592-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP595-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP596-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP597-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP598-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP599-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP600-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP602-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP603-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP604-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP605-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP606-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP608-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP612-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/GRP613-1.p/prove_these_axioms_1.con -cic:/matita/tests/TPTP/Veloci/GRP614-1.p/prove_these_axioms_2.con -cic:/matita/tests/TPTP/Veloci/GRP615-1.p/prove_these_axioms_3.con -cic:/matita/tests/TPTP/Veloci/GRP616-1.p/prove_these_axioms_4.con -cic:/matita/tests/TPTP/Veloci/LAT008-1.p/prove_absorbtion_dual.con -cic:/matita/tests/TPTP/Veloci/LAT033-1.p/idempotence_of_join.con -cic:/matita/tests/TPTP/Veloci/LAT034-1.p/idempotence_of_meet.con -cic:/matita/tests/TPTP/Veloci/LAT039-1.p/rhs.con -cic:/matita/tests/TPTP/Veloci/LAT039-2.p/rhs.con -cic:/matita/tests/TPTP/Veloci/LAT040-1.p/rhs.con -cic:/matita/tests/TPTP/Veloci/LAT045-1.p/prove_orthomodular_law.con -cic:/matita/tests/TPTP/Veloci/LCL110-2.p/prove_mv_24.con -cic:/matita/tests/TPTP/Veloci/LCL112-2.p/prove_mv_29.con -cic:/matita/tests/TPTP/Veloci/LCL113-2.p/prove_mv_33.con -cic:/matita/tests/TPTP/Veloci/LCL114-2.p/prove_mv_36.con -cic:/matita/tests/TPTP/Veloci/LCL115-2.p/prove_mv_39.con -cic:/matita/tests/TPTP/Veloci/LCL132-1.p/prove_wajsberg_lemma.con -cic:/matita/tests/TPTP/Veloci/LCL133-1.p/prove_wajsberg_lemma.con -cic:/matita/tests/TPTP/Veloci/LCL134-1.p/prove_wajsberg_lemma.con -cic:/matita/tests/TPTP/Veloci/LCL135-1.p/prove_wajsberg_lemma.con -cic:/matita/tests/TPTP/Veloci/LCL139-1.p/prove_wajsberg_lemma.con -cic:/matita/tests/TPTP/Veloci/LCL140-1.p/prove_wajsberg_lemma.con -cic:/matita/tests/TPTP/Veloci/LCL141-1.p/prove_wajsberg_lemma.con -cic:/matita/tests/TPTP/Veloci/LCL153-1.p/prove_alternative_wajsberg_axiom.con -cic:/matita/tests/TPTP/Veloci/LCL154-1.p/prove_alternative_wajsberg_axiom.con -cic:/matita/tests/TPTP/Veloci/LCL155-1.p/prove_alternative_wajsberg_axiom.con -cic:/matita/tests/TPTP/Veloci/LCL156-1.p/prove_alternative_wajsberg_axiom.con -cic:/matita/tests/TPTP/Veloci/LCL157-1.p/prove_alternative_wajsberg_axiom.con -cic:/matita/tests/TPTP/Veloci/LCL158-1.p/prove_alternative_wajsberg_axiom.con -cic:/matita/tests/TPTP/Veloci/LCL161-1.p/prove_wajsberg_axiom.con -cic:/matita/tests/TPTP/Veloci/LCL164-1.p/prove_wajsberg_axiom.con -cic:/matita/tests/TPTP/Veloci/LDA001-1.p/prove_equation.con -cic:/matita/tests/TPTP/Veloci/LDA007-3.p/prove_equation.con -cic:/matita/tests/TPTP/Veloci/RNG007-4.p/prove_inverse.con -cic:/matita/tests/TPTP/Veloci/RNG008-4.p/prove_commutativity.con -cic:/matita/tests/TPTP/Veloci/RNG011-5.p/prove_equality.con -cic:/matita/tests/TPTP/Veloci/RNG023-6.p/prove_left_alternative.con -cic:/matita/tests/TPTP/Veloci/RNG023-7.p/prove_left_alternative.con -cic:/matita/tests/TPTP/Veloci/RNG024-6.p/prove_right_alternative.con -cic:/matita/tests/TPTP/Veloci/RNG024-7.p/prove_right_alternative.con -cic:/matita/tests/TPTP/Veloci/ROB002-1.p/prove_huntingtons_axiom.con -cic:/matita/tests/TPTP/Veloci/ROB009-1.p/prove_result.con -cic:/matita/tests/TPTP/Veloci/ROB010-1.p/prove_result.con -cic:/matita/tests/TPTP/Veloci/ROB013-1.p/prove_result.con -cic:/matita/tests/TPTP/Veloci/ROB030-1.p/prove_absorption_within_negation.con -cic:/matita/tests/TPTP/Veloci/SYN083-1.p/prove_this.con -cic:/matita/tests/unfold/lem.con -cic:/matita/tests/unfold/myplus.con -cic:/matita/tests/unfold/t.con -cic:/matita/tests/unfold/trivial.con +cic:/CoRN/algebra/Basics/well_founded_ltof.con +cic:/CoRN/algebra/Basics/well_founded_induction_type.con +cic:/CoRN/algebra/Basics/well_founded.con +cic:/CoRN/algebra/Basics/surj_not.con +cic:/CoRN/algebra/Basics/surj_lt_subproof.con +cic:/CoRN/algebra/Basics/surj_lt.con +cic:/CoRN/algebra/Basics/surj_le_subproof.con +cic:/CoRN/algebra/Basics/surj_le.con +cic:/CoRN/algebra/Basics/surj_eq_subproof.con +cic:/CoRN/algebra/Basics/surj_eq.con +cic:/CoRN/algebra/Basics/proper_caseZ_diff_subproof0.con +cic:/CoRN/algebra/Basics/proper_caseZ_diff_subproof.con +cic:/CoRN/algebra/Basics/proper_caseZ_diff.con +cic:/CoRN/algebra/Basics/pred_succ_Z_ind.con +cic:/CoRN/algebra/Basics/power.con +cic:/CoRN/algebra/Basics/p_is_some_anti_convert.con +cic:/CoRN/algebra/Basics/not_r_sumbool_rec.con +cic:/CoRN/algebra/Basics/not_l_sumbool_rec.con +cic:/CoRN/algebra/Basics/nats_Z_ind.con +cic:/CoRN/algebra/Basics/nat_fac_gtzero.con +cic:/CoRN/algebra/Basics/minus4_subproof1.con +cic:/CoRN/algebra/Basics/minus4_subproof0.con +cic:/CoRN/algebra/Basics/minus4_subproof.con +cic:/CoRN/algebra/Basics/minus4.con +cic:/CoRN/algebra/Basics/minus3_subproof1.con +cic:/CoRN/algebra/Basics/minus3_subproof0.con +cic:/CoRN/algebra/Basics/minus3_subproof.con +cic:/CoRN/algebra/Basics/minus3.con +cic:/CoRN/algebra/Basics/min_convert_is_NEG.con +cic:/CoRN/algebra/Basics/ltof.con +cic:/CoRN/algebra/Basics/lt_z_two.con +cic:/CoRN/algebra/Basics/lt_wf_rect.con +cic:/CoRN/algebra/Basics/lt_mult_right.con +cic:/CoRN/algebra/Basics/lt_lt_minus_subproof.con +cic:/CoRN/algebra/Basics/lt_lt_minus.con +cic:/CoRN/algebra/Basics/lt_le_dec.con +cic:/CoRN/algebra/Basics/lt_O_positive_to_nat.con +cic:/CoRN/algebra/Basics/le_pred.con +cic:/CoRN/algebra/Basics/le_mult_right.con +cic:/CoRN/algebra/Basics/inject_nat_convert.con +cic:/CoRN/algebra/Basics/induction_ltof2T.con +cic:/CoRN/algebra/Basics/fac.con +cic:/CoRN/algebra/Basics/diff_Z_ind_subproof.con +cic:/CoRN/algebra/Basics/diff_Z_ind.con +cic:/CoRN/algebra/Basics/convert_is_POS.con +cic:/CoRN/algebra/Basics/caseZ_diff_Pos.con +cic:/CoRN/algebra/Basics/caseZ_diff_O.con +cic:/CoRN/algebra/Basics/caseZ_diff_Neg.con +cic:/CoRN/algebra/Basics/caseZ_diff.con +cic:/CoRN/algebra/Basics/anti_convert_pred_convert.con +cic:/CoRN/algebra/Basics/Zodd_Zeven_min1.con +cic:/CoRN/algebra/Basics/Zmult_minus_distr_r.con +cic:/CoRN/algebra/Basics/Zmult_absorb.con +cic:/CoRN/algebra/Basics/Zlt_reg_mult_l.con +cic:/CoRN/algebra/Basics/Zlt_opp.con +cic:/CoRN/algebra/Basics/Zlt_conv_mult_l.con +cic:/CoRN/algebra/Basics/Zgt_not_eq.con +cic:/CoRN/algebra/Basics/Z_to_nat_correct.con +cic:/CoRN/algebra/Basics/Z_to_nat.con +cic:/CoRN/algebra/Basics/Z_exh.con +cic:/CoRN/algebra/Basics/POS_anti_convert.con +cic:/CoRN/algebra/Basics/NEG_anti_convert.con +cic:/CoRN/algebra/Basics/Acc_iter.con +cic:/CoRN/algebra/Basics/Acc_inv.con +cic:/CoRN/algebra/Basics/Acc_ind.con +cic:/CoRN/algebra/Basics/Acc.ind +cic:/CoRN/algebra/CAbGroups/zmult_zero.con +cic:/CoRN/algebra/CAbGroups/zmult_wd.con +cic:/CoRN/algebra/CAbGroups/zmult_plus.con +cic:/CoRN/algebra/CAbGroups/zmult_plus'.con +cic:/CoRN/algebra/CAbGroups/zmult_one.con +cic:/CoRN/algebra/CAbGroups/zmult_mult.con +cic:/CoRN/algebra/CAbGroups/zmult_min_one.con +cic:/CoRN/algebra/CAbGroups/zmult_char_subproof1.con +cic:/CoRN/algebra/CAbGroups/zmult_char_subproof0.con +cic:/CoRN/algebra/CAbGroups/zmult_char_subproof.con +cic:/CoRN/algebra/CAbGroups/zmult_char.con +cic:/CoRN/algebra/CAbGroups/zmult_Zero.con +cic:/CoRN/algebra/CAbGroups/zmult.con +cic:/CoRN/algebra/CAbGroups/plus_runit.con +cic:/CoRN/algebra/CAbGroups/plus_rext.con +cic:/CoRN/algebra/CAbGroups/plus_is_fun.con +cic:/CoRN/algebra/CAbGroups/plus_fun.con +cic:/CoRN/algebra/CAbGroups/plus_cancel_ap_lft.con +cic:/CoRN/algebra/CAbGroups/op_lft_resp_ap.con +cic:/CoRN/algebra/CAbGroups/nmult_wd.con +cic:/CoRN/algebra/CAbGroups/nmult_plus.con +cic:/CoRN/algebra/CAbGroups/nmult_plus'.con +cic:/CoRN/algebra/CAbGroups/nmult_one.con +cic:/CoRN/algebra/CAbGroups/nmult_mult.con +cic:/CoRN/algebra/CAbGroups/nmult_inv.con +cic:/CoRN/algebra/CAbGroups/nmult_Zero.con +cic:/CoRN/algebra/CAbGroups/nmult.con +cic:/CoRN/algebra/CAbGroups/minus_plus.con +cic:/CoRN/algebra/CAbGroups/isabgrp_scrr.con +cic:/CoRN/algebra/CAbGroups/is_CAbGroup.con +cic:/CoRN/algebra/CAbGroups/inv_inv'.con +cic:/CoRN/algebra/CAbGroups/cag_proof.con +cic:/CoRN/algebra/CAbGroups/cag_op_inv.con +cic:/CoRN/algebra/CAbGroups/cag_crr.con +cic:/CoRN/algebra/CAbGroups/cag_commutes_unfolded.con +cic:/CoRN/algebra/CAbGroups/cag_commutes.con +cic:/CoRN/algebra/CAbGroups/cag_ap_cancel_lft.con +cic:/CoRN/algebra/CAbGroups/assoc_1.con +cic:/CoRN/algebra/CAbGroups/CAbGroup_rect.con +cic:/CoRN/algebra/CAbGroups/CAbGroup_rec.con +cic:/CoRN/algebra/CAbGroups/CAbGroup_is_CAbGroup.con +cic:/CoRN/algebra/CAbGroups/CAbGroup_ind.con +cic:/CoRN/algebra/CAbGroups/CAbGroup.ind +cic:/CoRN/algebra/CAbGroups/Build_SubCAbGroup.con +cic:/CoRN/algebra/CAbGroups/Build_CSemiGroup'.con +cic:/CoRN/algebra/CAbGroups/Build_CMonoid'.con +cic:/CoRN/algebra/CAbGroups/Build_CGroup'.con +cic:/CoRN/algebra/CAbGroups/Build_CAbGroup'.con +cic:/CoRN/algebra/CAbMonoids/isabgrp_scrr.con +cic:/CoRN/algebra/CAbMonoids/is_CAbMonoid.con +cic:/CoRN/algebra/CAbMonoids/cam_proof.con +cic:/CoRN/algebra/CAbMonoids/cam_crr.con +cic:/CoRN/algebra/CAbMonoids/cam_commutes_unfolded.con +cic:/CoRN/algebra/CAbMonoids/cam_commutes.con +cic:/CoRN/algebra/CAbMonoids/CAbMonoid_rect.con +cic:/CoRN/algebra/CAbMonoids/CAbMonoid_rec.con +cic:/CoRN/algebra/CAbMonoids/CAbMonoid_is_CAbMonoid.con +cic:/CoRN/algebra/CAbMonoids/CAbMonoid_ind.con +cic:/CoRN/algebra/CAbMonoids/CAbMonoid.ind +cic:/CoRN/algebra/CAbMonoids/Build_SubCAbMonoid.con +cic:/CoRN/algebra/CHomomorphism_Theorems/tau_surj.con +cic:/CoRN/algebra/CHomomorphism_Theorems/tau_strext.con +cic:/CoRN/algebra/CHomomorphism_Theorems/tau_is_fun.con +cic:/CoRN/algebra/CHomomorphism_Theorems/tau.con +cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_strext.con +cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_is_fun.con +cic:/CoRN/algebra/CHomomorphism_Theorems/sigst_inj.con +cic:/CoRN/algebra/CHomomorphism_Theorems/sigst.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cswdpredR.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cswdpred.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cspredR.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cspred.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cs_is_comod.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cs_is_coideal.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cs_as_comod.con +cic:/CoRN/algebra/CHomomorphism_Theorems/cs_as_coideal.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_surj.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_strext.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau_is_fun.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rtau.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_strext.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_is_fun.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst_inj.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Rsigst.con +cic:/CoRN/algebra/CHomomorphism_Theorems/RingHomTheorem.con +cic:/CoRN/algebra/CHomomorphism_Theorems/RdivCsR.con +cic:/CoRN/algebra/CHomomorphism_Theorems/ModHomTheorem.con +cic:/CoRN/algebra/CHomomorphism_Theorems/CsR.con +cic:/CoRN/algebra/CHomomorphism_Theorems/Cs.con +cic:/CoRN/algebra/CHomomorphism_Theorems/AdivCs.con +cic:/CoRN/algebra/CIdeals/is_ideal_rect.con +cic:/CoRN/algebra/CIdeals/is_ideal_rec.con +cic:/CoRN/algebra/CIdeals/is_ideal_ind.con +cic:/CoRN/algebra/CIdeals/is_ideal.ind +cic:/CoRN/algebra/CIdeals/is_coideal_rect.con +cic:/CoRN/algebra/CIdeals/is_coideal_rec.con +cic:/CoRN/algebra/CIdeals/is_coideal_ind.con +cic:/CoRN/algebra/CIdeals/is_coideal.ind +cic:/CoRN/algebra/CIdeals/idprpl.con +cic:/CoRN/algebra/CIdeals/idproof.con +cic:/CoRN/algebra/CIdeals/idpred.con +cic:/CoRN/algebra/CIdeals/ideal_rect.con +cic:/CoRN/algebra/CIdeals/ideal_rec.con +cic:/CoRN/algebra/CIdeals/ideal_is_ideal.con +cic:/CoRN/algebra/CIdeals/ideal_ind.con +cic:/CoRN/algebra/CIdeals/ideal_as_CSetoid.con +cic:/CoRN/algebra/CIdeals/ideal.ind +cic:/CoRN/algebra/CIdeals/idax.con +cic:/CoRN/algebra/CIdeals/coideal_wd.con +cic:/CoRN/algebra/CIdeals/coideal_rect.con +cic:/CoRN/algebra/CIdeals/coideal_rec.con +cic:/CoRN/algebra/CIdeals/coideal_plus.con +cic:/CoRN/algebra/CIdeals/coideal_nonzero.con +cic:/CoRN/algebra/CIdeals/coideal_nontriv.con +cic:/CoRN/algebra/CIdeals/coideal_mult.con +cic:/CoRN/algebra/CIdeals/coideal_is_coideal.con +cic:/CoRN/algebra/CIdeals/coideal_ind.con +cic:/CoRN/algebra/CIdeals/coideal_as_CSetoid.con +cic:/CoRN/algebra/CIdeals/coideal_apzero.con +cic:/CoRN/algebra/CIdeals/coideal.ind +cic:/CoRN/algebra/CIdeals/ciproof.con +cic:/CoRN/algebra/CIdeals/cipred.con +cic:/CoRN/algebra/CIdeals/ciplus.con +cic:/CoRN/algebra/CIdeals/cinontriv.con +cic:/CoRN/algebra/CIdeals/cimult.con +cic:/CoRN/algebra/CIdeals/ciapzero.con +cic:/CoRN/algebra/CLogic/weird_mon_covers.con +cic:/CoRN/algebra/CLogic/to_Codd_even.con +cic:/CoRN/algebra/CLogic/to_Codd.con +cic:/CoRN/algebra/CLogic/to_Ceven.con +cic:/CoRN/algebra/CLogic/toCle.con +cic:/CoRN/algebra/CLogic/toCProp_rect.con +cic:/CoRN/algebra/CLogic/toCProp_rec.con +cic:/CoRN/algebra/CLogic/toCProp_lt.con +cic:/CoRN/algebra/CLogic/toCProp_ind.con +cic:/CoRN/algebra/CLogic/toCProp_e.con +cic:/CoRN/algebra/CLogic/toCProp_Zlt.con +cic:/CoRN/algebra/CLogic/toCProp.ind +cic:/CoRN/algebra/CLogic/str_finite_or_elim.con +cic:/CoRN/algebra/CLogic/sig2T_rect.con +cic:/CoRN/algebra/CLogic/sig2T_rec.con +cic:/CoRN/algebra/CLogic/sig2T_ind.con +cic:/CoRN/algebra/CLogic/sig2T.ind +cic:/CoRN/algebra/CLogic/proj2b_sig2T.con +cic:/CoRN/algebra/CLogic/proj2a_sig2T.con +cic:/CoRN/algebra/CLogic/proj2_sigT.con +cic:/CoRN/algebra/CLogic/proj1_sigT.con +cic:/CoRN/algebra/CLogic/proj1_sig2T.con +cic:/CoRN/algebra/CLogic/pred_lt.con +cic:/CoRN/algebra/CLogic/plus_pred_pred_plus.con +cic:/CoRN/algebra/CLogic/plus_eq_one_imp_eq_zero.con +cic:/CoRN/algebra/CLogic/odd_induction.con +cic:/CoRN/algebra/CLogic/odd_ind.con +cic:/CoRN/algebra/CLogic/odd_double_ind.con +cic:/CoRN/algebra/CLogic/not_r_sum_rec.con +cic:/CoRN/algebra/CLogic/not_r_cor_rect.con +cic:/CoRN/algebra/CLogic/not_not_lt.con +cic:/CoRN/algebra/CLogic/not_l_sum_rec.con +cic:/CoRN/algebra/CLogic/not_l_cor_rect.con +cic:/CoRN/algebra/CLogic/nat_nat_pos.con +cic:/CoRN/algebra/CLogic/nat_mon_imp_mon'.con +cic:/CoRN/algebra/CLogic/nat_mon_imp_inj.con +cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon_le.con +cic:/CoRN/algebra/CLogic/nat_local_mon_imp_mon.con +cic:/CoRN/algebra/CLogic/nat_less_n_pred.con +cic:/CoRN/algebra/CLogic/nat_less_n_pred'.con +cic:/CoRN/algebra/CLogic/nat_complete_double_induction.con +cic:/CoRN/algebra/CLogic/nat_complete_double_ind.con +cic:/CoRN/algebra/CLogic/my_Cle_ind.con +cic:/CoRN/algebra/CLogic/mon_fun_covers.con +cic:/CoRN/algebra/CLogic/member_app.con +cic:/CoRN/algebra/CLogic/member.con +cic:/CoRN/algebra/CLogic/lt_pred'.con +cic:/CoRN/algebra/CLogic/lt_8.con +cic:/CoRN/algebra/CLogic/lt_5.con +cic:/CoRN/algebra/CLogic/lt_10.con +cic:/CoRN/algebra/CLogic/le_2.con +cic:/CoRN/algebra/CLogic/le_1.con +cic:/CoRN/algebra/CLogic/kseq_prop.con +cic:/CoRN/algebra/CLogic/four_induction.con +cic:/CoRN/algebra/CLogic/four_ind.con +cic:/CoRN/algebra/CLogic/finite_or_elim.con +cic:/CoRN/algebra/CLogic/even_plus_n_n.con +cic:/CoRN/algebra/CLogic/even_or_odd_plus_gt.con +cic:/CoRN/algebra/CLogic/even_or_odd_plus.con +cic:/CoRN/algebra/CLogic/even_induction.con +cic:/CoRN/algebra/CLogic/even_ind.con +cic:/CoRN/algebra/CLogic/choice.con +cic:/CoRN/algebra/CLogic/absolu_2.con +cic:/CoRN/algebra/CLogic/absolu_1.con +cic:/CoRN/algebra/CLogic/Zsgn_5.con +cic:/CoRN/algebra/CLogic/Zsgn_4.con +cic:/CoRN/algebra/CLogic/Zsgn_3.con +cic:/CoRN/algebra/CLogic/Zsgn_2.con +cic:/CoRN/algebra/CLogic/Zsgn_1.con +cic:/CoRN/algebra/CLogic/Zmult_Sm_Sn.con +cic:/CoRN/algebra/CLogic/Zlts.con +cic:/CoRN/algebra/CLogic/Zgt_mult_reg_absorb_l.con +cic:/CoRN/algebra/CLogic/Zgt_mult_conv_absorb_l.con +cic:/CoRN/algebra/CLogic/ZL9.con +cic:/CoRN/algebra/CLogic/ZL4'.con +cic:/CoRN/algebra/CLogic/Ttransitive.con +cic:/CoRN/algebra/CLogic/Tsymmetric.con +cic:/CoRN/algebra/CLogic/Trelation.con +cic:/CoRN/algebra/CLogic/Treflexive.con +cic:/CoRN/algebra/CLogic/Tequiv.con +cic:/CoRN/algebra/CLogic/S_predn.con +cic:/CoRN/algebra/CLogic/Not.con +cic:/CoRN/algebra/CLogic/Iff_trans.con +cic:/CoRN/algebra/CLogic/Iff_sym.con +cic:/CoRN/algebra/CLogic/Iff_right.con +cic:/CoRN/algebra/CLogic/Iff_refl.con +cic:/CoRN/algebra/CLogic/Iff_left.con +cic:/CoRN/algebra/CLogic/Iff_imp_imp.con +cic:/CoRN/algebra/CLogic/Iff.con +cic:/CoRN/algebra/CLogic/Ctransitive.con +cic:/CoRN/algebra/CLogic/Csymmetric.con +cic:/CoRN/algebra/CLogic/Crelation.con +cic:/CoRN/algebra/CLogic/Creflexive.con +cic:/CoRN/algebra/CLogic/Cpred_succ_Z_ind.con +cic:/CoRN/algebra/CLogic/Codd_to.con +cic:/CoRN/algebra/CLogic/Codd_rect.con +cic:/CoRN/algebra/CLogic/Codd_rec.con +cic:/CoRN/algebra/CLogic/Codd_ind.con +cic:/CoRN/algebra/CLogic/Codd_even_to.con +cic:/CoRN/algebra/CLogic/Codd.ind +cic:/CoRN/algebra/CLogic/Cnats_Z_ind.con +cic:/CoRN/algebra/CLogic/Cnat_total_order.con +cic:/CoRN/algebra/CLogic/Cnat_double_ind.con +cic:/CoRN/algebra/CLogic/Clt_to.con +cic:/CoRN/algebra/CLogic/Clt_le_weak.con +cic:/CoRN/algebra/CLogic/Clt.con +cic:/CoRN/algebra/CLogic/Cle_to.con +cic:/CoRN/algebra/CLogic/Cle_rect.con +cic:/CoRN/algebra/CLogic/Cle_rec.con +cic:/CoRN/algebra/CLogic/Cle_n_S.con +cic:/CoRN/algebra/CLogic/Cle_le_S_eq.con +cic:/CoRN/algebra/CLogic/Cle_ind.con +cic:/CoRN/algebra/CLogic/Cle.ind +cic:/CoRN/algebra/CLogic/Ceven_to.con +cic:/CoRN/algebra/CLogic/Ceven_rect.con +cic:/CoRN/algebra/CLogic/Ceven_rec.con +cic:/CoRN/algebra/CLogic/Ceven_ind.con +cic:/CoRN/algebra/CLogic/Cequiv.con +cic:/CoRN/algebra/CLogic/Cdiff_Z_ind_subproof.con +cic:/CoRN/algebra/CLogic/Cdiff_Z_ind.con +cic:/CoRN/algebra/CLogic/Cdecidable.con +cic:/CoRN/algebra/CLogic/CdeMorgan_ex_all.con +cic:/CoRN/algebra/CLogic/Ccontrapos'.con +cic:/CoRN/algebra/CLogic/CZlt_to.con +cic:/CoRN/algebra/CLogic/CZ_exh.con +cic:/CoRN/algebra/CLogic/CTrue_rect.con +cic:/CoRN/algebra/CLogic/CTrue_rec.con +cic:/CoRN/algebra/CLogic/CTrue_ind.con +cic:/CoRN/algebra/CLogic/CTrue.ind +cic:/CoRN/algebra/CLogic/CProp.con +cic:/CoRN/algebra/CLogic/COr_rect.con +cic:/CoRN/algebra/CLogic/COr_rec.con +cic:/CoRN/algebra/CLogic/COr_ind.con +cic:/CoRN/algebra/CLogic/COr.ind +cic:/CoRN/algebra/CLogic/CNot_Not_or.con +cic:/CoRN/algebra/CLogic/CNot.con +cic:/CoRN/algebra/CLogic/CFalse_rect.con +cic:/CoRN/algebra/CLogic/CFalse_rec.con +cic:/CoRN/algebra/CLogic/CFalse_ind.con +cic:/CoRN/algebra/CLogic/CFalse.ind +cic:/CoRN/algebra/CLogic/CAnd_rect.con +cic:/CoRN/algebra/CLogic/CAnd_rec.con +cic:/CoRN/algebra/CLogic/CAnd_proj2.con +cic:/CoRN/algebra/CLogic/CAnd_proj1.con +cic:/CoRN/algebra/CLogic/CAnd_ind.con +cic:/CoRN/algebra/CLogic/CAnd.ind +cic:/CoRN/algebra/CModule_Homomorphisms/mh_strext.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_zero.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_unit.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_plus.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_mult.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_pres_minus.con +cic:/CoRN/algebra/CModule_Homomorphisms/mh_apzero.con +cic:/CoRN/algebra/CModule_Homomorphisms/hommap.con +cic:/CoRN/algebra/CModule_Homomorphisms/hom3.con +cic:/CoRN/algebra/CModule_Homomorphisms/hom2.con +cic:/CoRN/algebra/CModule_Homomorphisms/hom1.con +cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_unit.con +cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_plus.con +cic:/CoRN/algebra/CModule_Homomorphisms/fun_pres_mult.con +cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_rect.con +cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_rec.con +cic:/CoRN/algebra/CModule_Homomorphisms/ModHom_ind.con +cic:/CoRN/algebra/CModule_Homomorphisms/ModHom.ind +cic:/CoRN/algebra/CModules/submod_rect.con +cic:/CoRN/algebra/CModules/submod_rec.con +cic:/CoRN/algebra/CModules/submod_is_submod.con +cic:/CoRN/algebra/CModules/submod_ind.con +cic:/CoRN/algebra/CModules/submod_as_CSetoid.con +cic:/CoRN/algebra/CModules/submod.ind +cic:/CoRN/algebra/CModules/smzero.con +cic:/CoRN/algebra/CModules/smproof.con +cic:/CoRN/algebra/CModules/smpred.con +cic:/CoRN/algebra/CModules/smplus.con +cic:/CoRN/algebra/CModules/smmult.con +cic:/CoRN/algebra/CModules/rm_proof.con +cic:/CoRN/algebra/CModules/rm_pl2.con +cic:/CoRN/algebra/CModules/rm_pl1.con +cic:/CoRN/algebra/CModules/rm_one.con +cic:/CoRN/algebra/CModules/rm_mult.con +cic:/CoRN/algebra/CModules/rm_mu.con +cic:/CoRN/algebra/CModules/rm_crr.con +cic:/CoRN/algebra/CModules/mu_zerox.con +cic:/CoRN/algebra/CModules/mu_strext.con +cic:/CoRN/algebra/CModules/mu_plus2.con +cic:/CoRN/algebra/CModules/mu_plus1.con +cic:/CoRN/algebra/CModules/mu_one.con +cic:/CoRN/algebra/CModules/mu_mult.con +cic:/CoRN/algebra/CModules/mu_minusonex.con +cic:/CoRN/algebra/CModules/mu_minusax.con +cic:/CoRN/algebra/CModules/mu_azero.con +cic:/CoRN/algebra/CModules/mu_axap0_xap0.con +cic:/CoRN/algebra/CModules/mu_axap0_aap0.con +cic:/CoRN/algebra/CModules/mu_aminusx.con +cic:/CoRN/algebra/CModules/mu0help2.con +cic:/CoRN/algebra/CModules/mu0help.con +cic:/CoRN/algebra/CModules/is_submod_rect.con +cic:/CoRN/algebra/CModules/is_submod_rec.con +cic:/CoRN/algebra/CModules/is_submod_ind.con +cic:/CoRN/algebra/CModules/is_submod.ind +cic:/CoRN/algebra/CModules/is_comod_rect.con +cic:/CoRN/algebra/CModules/is_comod_rec.con +cic:/CoRN/algebra/CModules/is_comod_ind.con +cic:/CoRN/algebra/CModules/is_comod.ind +cic:/CoRN/algebra/CModules/is_RModule_rect.con +cic:/CoRN/algebra/CModules/is_RModule_rec.con +cic:/CoRN/algebra/CModules/is_RModule_ind.con +cic:/CoRN/algebra/CModules/is_RModule.ind +cic:/CoRN/algebra/CModules/comod_wd.con +cic:/CoRN/algebra/CModules/comod_rect.con +cic:/CoRN/algebra/CModules/comod_rec.con +cic:/CoRN/algebra/CModules/comod_plus.con +cic:/CoRN/algebra/CModules/comod_nonzero.con +cic:/CoRN/algebra/CModules/comod_mult.con +cic:/CoRN/algebra/CModules/comod_is_comod.con +cic:/CoRN/algebra/CModules/comod_ind.con +cic:/CoRN/algebra/CModules/comod_as_CSetoid.con +cic:/CoRN/algebra/CModules/comod_apzero.con +cic:/CoRN/algebra/CModules/comod.ind +cic:/CoRN/algebra/CModules/cmproof.con +cic:/CoRN/algebra/CModules/cmpred.con +cic:/CoRN/algebra/CModules/cmplus.con +cic:/CoRN/algebra/CModules/cmmult.con +cic:/CoRN/algebra/CModules/cmapzero.con +cic:/CoRN/algebra/CModules/R_is_RModule.con +cic:/CoRN/algebra/CModules/R_as_RModule.con +cic:/CoRN/algebra/CModules/RModule_rect.con +cic:/CoRN/algebra/CModules/RModule_rec.con +cic:/CoRN/algebra/CModules/RModule_is_RModule.con +cic:/CoRN/algebra/CModules/RModule_ind.con +cic:/CoRN/algebra/CModules/RModule.ind +cic:/matita/dama/bishop_set/le_le_eq.con +cic:/matita/dama/bishop_set/le_antisymmetric.con +cic:/matita/dama/bishop_set/eq_trans_.con +cic:/matita/dama/bishop_set/eq_sym_.con +cic:/matita/dama/bishop_set/eq_sym.con +cic:/matita/dama/bishop_set/eq_reflexive.con +cic:/matita/dama/bishop_set/eq.con +cic:/matita/dama/bishop_set/bs_symmetric.con +cic:/matita/dama/bishop_set/bs_cotransitive.con +cic:/matita/dama/bishop_set/bs_coreflexive.con +cic:/matita/dama/bishop_set/bs_carr.con +cic:/matita/dama/bishop_set/bs_apart.con +cic:/matita/dama/bishop_set/bishop_set_rect.con +cic:/matita/dama/bishop_set/bishop_set_rec.con +cic:/matita/dama/bishop_set/bishop_set_of_ordered_set.con +cic:/matita/dama/bishop_set/bishop_set_ind.con +cic:/matita/dama/bishop_set/bishop_set.ind +cic:/matita/dama/bishop_set_rewrite/le_rewr.con +cic:/matita/dama/bishop_set_rewrite/le_rewl.con +cic:/matita/dama/bishop_set_rewrite/exc_rewr.con +cic:/matita/dama/bishop_set_rewrite/exc_rewl.con +cic:/matita/dama/bishop_set_rewrite/eq_trans.con +cic:/matita/dama/bishop_set_rewrite/ap_rewr.con +cic:/matita/dama/bishop_set_rewrite/ap_rewl.con +cic:/matita/dama/cprop_connectives/transitive.con +cic:/matita/dama/cprop_connectives/symmetric.con +cic:/matita/dama/cprop_connectives/reflexive.con +cic:/matita/dama/cprop_connectives/exT_rect.con +cic:/matita/dama/cprop_connectives/exT_rec.con +cic:/matita/dama/cprop_connectives/exT_ind.con +cic:/matita/dama/cprop_connectives/exT.ind +cic:/matita/dama/cprop_connectives/cotransitive.con +cic:/matita/dama/cprop_connectives/coreflexive.con +cic:/matita/dama/cprop_connectives/antisymmetric.con +cic:/matita/dama/cprop_connectives/Or_rect.con +cic:/matita/dama/cprop_connectives/Or_rec.con +cic:/matita/dama/cprop_connectives/Or_ind.con +cic:/matita/dama/cprop_connectives/Or.ind +cic:/matita/dama/cprop_connectives/Not.con +cic:/matita/dama/cprop_connectives/False_rect.con +cic:/matita/dama/cprop_connectives/False_rec.con +cic:/matita/dama/cprop_connectives/False_ind.con +cic:/matita/dama/cprop_connectives/False.ind +cic:/matita/dama/cprop_connectives/And_rect.con +cic:/matita/dama/cprop_connectives/And_rec.con +cic:/matita/dama/cprop_connectives/And_ind.con +cic:/matita/dama/cprop_connectives/And.ind +cic:/matita/dama/ordered_set/os_excess.con +cic:/matita/dama/ordered_set/os_cotransitive.con +cic:/matita/dama/ordered_set/os_coreflexive.con +cic:/matita/dama/ordered_set/os_carr.con +cic:/matita/dama/ordered_set/ordered_set_rect.con +cic:/matita/dama/ordered_set/ordered_set_rec.con +cic:/matita/dama/ordered_set/ordered_set_ind.con +cic:/matita/dama/ordered_set/ordered_set.ind +cic:/matita/dama/ordered_set/le_transitive.con +cic:/matita/dama/ordered_set/le_reflexive.con +cic:/matita/dama/ordered_set/le.con +cic:/matita/dama/ordered_set/exc_le_variance.con +cic:/matita/dama/sequence/sequence.con +cic:/matita/dama/sequence/fun_of_sequence.con +cic:/matita/dama/supremum/upper_bound.con +cic:/matita/dama/supremum/uniq_supremum.con +cic:/matita/dama/supremum/strong_sup.con +cic:/matita/dama/supremum/increasing.con +cic:/matita/higher_order_defs/functions/symmetric2.con +cic:/matita/higher_order_defs/functions/symmetric.con +cic:/matita/higher_order_defs/functions/surjective.con +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