X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Farith%2Fnat.txt;h=6d8387ad5c3d918e0fb56e26bcecc1993b6c0ed3;hb=19b0a814861157ba05f23877d5cd94059f52c2e8;hp=915a45dbfa2363190f3d6e466aceba866c53be19;hpb=68e028d053806177e218ee1a5f8778d3011bef83;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt index 915a45dbf..6d8387ad5 100644 --- a/matita/matita/contribs/lambdadelta/ground/arith/nat.txt +++ b/matita/matita/contribs/lambdadelta/ground/arith/nat.txt @@ -1,137 +1,8 @@ -"cic:/matita/arithmetics/nat/nat.ind" -# -"cic:/matita/arithmetics/nat/nat_ind.con" -"cic:/matita/arithmetics/nat/nat_elim2.con" -"cic:/matita/arithmetics/nat/injective_S.con" -# -"cic:/matita/arithmetics/nat/plus.con" -"cic:/matita/arithmetics/nat/plus_n_O.con" -"cic:/matita/arithmetics/nat/plus_n_Sm.con" -"cic:/matita/arithmetics/nat/plus_O_n.con" -"cic:/matita/arithmetics/nat/commutative_plus.con" -"cic:/matita/arithmetics/nat/associative_plus.con" -"cic:/matita/arithmetics/nat/plus_plus_comm_23.con" -"cic:/matita/arithmetics/nat/assoc_plus1.con" -"cic:/matita/arithmetics/nat/injective_plus_l.con" -"cic:/matita/arithmetics/nat/injective_plus_r.con" -"cic:/matita/arithmetics/nat/nat_ind_plus.con" -# -"cic:/matita/arithmetics/nat/le.ind" -"cic:/matita/arithmetics/nat/le_ind.con" -"cic:/matita/arithmetics/nat/le_n_Sn.con" -"cic:/matita/arithmetics/nat/le_O_n.con" -"cic:/matita/arithmetics/nat/le_S_S.con" -"cic:/matita/arithmetics/nat/le_or_ge.con" -"cic:/matita/arithmetics/nat/le_S_S_to_le.con" -"cic:/matita/arithmetics/nat/le_n_O_to_eq.con" -"cic:/matita/arithmetics/nat/le_to_le_to_eq.con" -"cic:/matita/arithmetics/nat/transitive_le.con" -"cic:/matita/arithmetics/nat/decidable_le.con" -% -"cic:/matita/arithmetics/nat/monotonic_le_plus_l.con" -"cic:/matita/arithmetics/nat/monotonic_le_plus_r.con" -"cic:/matita/arithmetics/nat/le_plus_n_r.con" -"cic:/matita/arithmetics/nat/le_plus_n.con" -"cic:/matita/arithmetics/nat/le_plus_b.con" -"cic:/matita/arithmetics/nat/le_plus_a.con" -"cic:/matita/arithmetics/nat/le_plus.con" -"cic:/matita/arithmetics/nat/plus_le_0.con" -"cic:/matita/arithmetics/nat/le_plus_to_le_r.con" -"cic:/matita/arithmetics/nat/le_plus_to_le.con" -# -"cic:/matita/arithmetics/nat/lt.con" -"cic:/matita/arithmetics/nat/lt_O_S.con" -"cic:/matita/arithmetics/nat/le_to_or_lt_eq.con" -"cic:/matita/arithmetics/nat/eq_or_gt.con" -"cic:/matita/arithmetics/nat/lt_or_ge.con" -"cic:/matita/arithmetics/nat/not_le_to_lt.con" -"cic:/matita/arithmetics/nat/lt_to_le_to_lt.con" -"cic:/matita/arithmetics/nat/le_to_lt_to_lt.con" -"cic:/matita/arithmetics/nat/lt_to_not_le.con" -"cic:/matita/arithmetics/nat/lt_to_not_eq.con" -"cic:/matita/arithmetics/nat/lt_to_le.con" -"cic:/matita/arithmetics/nat/ltn_to_ltO.con" -"cic:/matita/arithmetics/nat/transitive_lt.con" -"cic:/matita/arithmetics/nat/nat_elim1.con" -"cic:/matita/arithmetics/nat/f_ind.con" -"cic:/matita/arithmetics/nat/f2_ind.con" -"cic:/matita/arithmetics/nat/f3_ind.con" -# -"cic:/matita/arithmetics/nat/monotonic_lt_plus_l.con" -"cic:/matita/arithmetics/nat/monotonic_lt_plus_r.con" -"cic:/matita/arithmetics/nat/lt_plus_Sn_r.con" -"cic:/matita/arithmetics/nat/lt_plus_to_lt_l.con" -# -"cic:/matita/arithmetics/nat/pred.con" -# -"cic:/matita/arithmetics/nat/pred_Sn.con" -# -"cic:/matita/arithmetics/nat/le_pred_n.con" -"cic:/matita/arithmetics/nat/monotonic_pred.con" -# -"cic:/matita/arithmetics/nat/S_pred.con" -# -"cic:/matita/arithmetics/nat/minus.con" -"cic:/matita/arithmetics/nat/minus_n_O.con" -"cic:/matita/arithmetics/nat/eq_minus_S_pred.con" -"cic:/matita/arithmetics/nat/minus_O_n.con" -"cic:/matita/arithmetics/nat/minus_S_S.con" -"cic:/matita/arithmetics/nat/minus_n_n.con" -"cic:/matita/arithmetics/nat/minus_Sn_n.con" -"cic:/matita/arithmetics/nat/minus_minus_comm.con" -# -"cic:/matita/arithmetics/nat/minus_plus_m_m.con" -"cic:/matita/arithmetics/nat/minus_plus.con" -"cic:/matita/arithmetics/nat/minus_plus_plus_l.con" -"cic:/matita/arithmetics/nat/plus_minus_plus_plus_l.con" -"cic:/matita/arithmetics/nat/plus_to_minus.con" -"cic:/matita/arithmetics/nat/discr_plus_xy_minus_xz.con" -"cic:/matita/arithmetics/nat/discr_minus_x_xy.con" -# -"cic:/matita/arithmetics/nat/minus_le.con" -"cic:/matita/arithmetics/nat/inv_eq_minus_O.con" -"cic:/matita/arithmetics/nat/monotonic_le_minus_l.con" -"cic:/matita/arithmetics/nat/monotonic_le_minus_r.con" -"cic:/matita/arithmetics/nat/eq_minus_O.con" -"cic:/matita/arithmetics/nat/minus_Sn_m.con" -"cic:/matita/arithmetics/nat/minus_minus_m_m.con" -# -"cic:/matita/arithmetics/nat/le_plus_minus_m_m.con" -"cic:/matita/arithmetics/nat/le_plus_to_minus.con" -"cic:/matita/arithmetics/nat/le_plus_to_minus_r.con" -"cic:/matita/arithmetics/nat/le_inv_plus_l.con" -"cic:/matita/arithmetics/nat/plus_minus_m_m.con" -"cic:/matita/arithmetics/nat/le_minus_to_plus.con" -"cic:/matita/arithmetics/nat/le_minus_to_plus_r.con" -"cic:/matita/arithmetics/nat/plus_minus.con" -"cic:/matita/arithmetics/nat/plus_minus_associative.con" -"cic:/matita/arithmetics/nat/minus_minus_associative.con" -"cic:/matita/arithmetics/nat/minus_minus.con" -"cic:/matita/arithmetics/nat/minus_le_minus_minus_comm.con" -# -"cic:/matita/arithmetics/nat/minus_pred_pred.con" -"cic:/matita/arithmetics/nat/monotonic_lt_minus_l.con" -# -"cic:/matita/arithmetics/nat/lt_plus_to_minus.con" -"cic:/matita/arithmetics/nat/lt_plus_to_minus_r.con" -"cic:/matita/arithmetics/nat/lt_inv_plus_l.con" -"cic:/matita/arithmetics/nat/lt_minus_to_plus.con" -"cic:/matita/arithmetics/nat/lt_minus_to_plus_r.con" -# -"cic:/matita/arithmetics/nat/max.con" -"cic:/matita/arithmetics/nat/commutative_max.con" - -#################################### - -"cic:/matita/arithmetics/nat/to_max.con" -"cic:/matita/arithmetics/nat/leb.con" -"cic:/matita/arithmetics/nat/leb_elim.con" -"cic:/matita/arithmetics/nat/le_maxl.con" -"cic:/matita/arithmetics/nat/le_maxr.con" -"cic:/matita/arithmetics/nat/le_to_leb_true.con" -"cic:/matita/arithmetics/nat/not_le_to_leb_false.con" - "cic:/matita/arithmetics/nat/nat_discr.con" "cic:/matita/arithmetics/nat/times.con" "cic:/matita/arithmetics/nat/times_n_1.con" "cic:/matita/arithmetics/nat/times_Sn_m.con" +"cic:/matita/arithmetics/nat/leb.con" +"cic:/matita/arithmetics/nat/leb_elim.con" +"cic:/matita/arithmetics/nat/le_to_leb_true.con" +"cic:/matita/arithmetics/nat/not_le_to_leb_false.con"