matita/matita/contribs/lambdadelta/ground/arith/nat.txt

   1 "cic:/matita/arithmetics/nat/nat.ind"
   2 #
   3 "cic:/matita/arithmetics/nat/nat_ind.con"
   4 "cic:/matita/arithmetics/nat/nat_elim2.con"
   5 "cic:/matita/arithmetics/nat/injective_S.con"
   6 #
   7 "cic:/matita/arithmetics/nat/plus.con"
   8 "cic:/matita/arithmetics/nat/plus_n_O.con"
   9 "cic:/matita/arithmetics/nat/plus_n_Sm.con"
  10 "cic:/matita/arithmetics/nat/plus_O_n.con"
  11 "cic:/matita/arithmetics/nat/commutative_plus.con"
  12 "cic:/matita/arithmetics/nat/associative_plus.con"
  13 "cic:/matita/arithmetics/nat/plus_plus_comm_23.con"
  14 "cic:/matita/arithmetics/nat/assoc_plus1.con"
  15 "cic:/matita/arithmetics/nat/injective_plus_l.con"
  16 "cic:/matita/arithmetics/nat/injective_plus_r.con"
  17 "cic:/matita/arithmetics/nat/nat_ind_plus.con"
  18 #
  19 "cic:/matita/arithmetics/nat/le.ind"
  20 "cic:/matita/arithmetics/nat/le_ind.con"
  21 "cic:/matita/arithmetics/nat/le_n_Sn.con"
  22 "cic:/matita/arithmetics/nat/le_O_n.con"
  23 "cic:/matita/arithmetics/nat/le_S_S.con"
  24 "cic:/matita/arithmetics/nat/le_or_ge.con"
  25 "cic:/matita/arithmetics/nat/le_S_S_to_le.con"
  26 "cic:/matita/arithmetics/nat/le_n_O_to_eq.con"
  27 "cic:/matita/arithmetics/nat/le_to_le_to_eq.con"
  28 "cic:/matita/arithmetics/nat/transitive_le.con"
  29 "cic:/matita/arithmetics/nat/decidable_le.con"
  30 %
  31 "cic:/matita/arithmetics/nat/monotonic_le_plus_l.con"
  32 "cic:/matita/arithmetics/nat/monotonic_le_plus_r.con"
  33 "cic:/matita/arithmetics/nat/le_plus_n_r.con"
  34 "cic:/matita/arithmetics/nat/le_plus_n.con"
  35 "cic:/matita/arithmetics/nat/le_plus_b.con"
  36 "cic:/matita/arithmetics/nat/le_plus_a.con"
  37 "cic:/matita/arithmetics/nat/le_plus.con"
  38 "cic:/matita/arithmetics/nat/plus_le_0.con"
  39 "cic:/matita/arithmetics/nat/le_plus_to_le_r.con"
  40 "cic:/matita/arithmetics/nat/le_plus_to_le.con"
  41 #
  42 "cic:/matita/arithmetics/nat/lt.con"
  43 "cic:/matita/arithmetics/nat/lt_O_S.con"
  44 "cic:/matita/arithmetics/nat/le_to_or_lt_eq.con"
  45 "cic:/matita/arithmetics/nat/eq_or_gt.con"
  46 "cic:/matita/arithmetics/nat/lt_or_ge.con"
  47 "cic:/matita/arithmetics/nat/not_le_to_lt.con"
  48 "cic:/matita/arithmetics/nat/lt_to_le_to_lt.con"
  49 "cic:/matita/arithmetics/nat/le_to_lt_to_lt.con"
  50 "cic:/matita/arithmetics/nat/lt_to_not_le.con"
  51 "cic:/matita/arithmetics/nat/lt_to_not_eq.con"
  52 "cic:/matita/arithmetics/nat/lt_to_le.con"
  53 "cic:/matita/arithmetics/nat/ltn_to_ltO.con"
  54 "cic:/matita/arithmetics/nat/transitive_lt.con"
  55 "cic:/matita/arithmetics/nat/nat_elim1.con"
  56 "cic:/matita/arithmetics/nat/f_ind.con"
  57 "cic:/matita/arithmetics/nat/f2_ind.con"
  58 "cic:/matita/arithmetics/nat/f3_ind.con"
  59
  60 ####################################
  61
  62 "cic:/matita/arithmetics/nat/lt_plus_Sn_r.con"
  63 "cic:/matita/arithmetics/nat/lt_plus_to_lt_l.con"
  64 "cic:/matita/arithmetics/nat/monotonic_lt_plus_l.con"
  65 "cic:/matita/arithmetics/nat/monotonic_lt_plus_r.con"
  66
  67 "cic:/matita/arithmetics/nat/le_pred_n.con"
  68 "cic:/matita/arithmetics/nat/pred.con"
  69 "cic:/matita/arithmetics/nat/pred_Sn.con"
  70 "cic:/matita/arithmetics/nat/S_pred.con"
  71 "cic:/matita/arithmetics/nat/monotonic_pred.con"
  72
  73 "cic:/matita/arithmetics/nat/discr_minus_x_xy.con"
  74 "cic:/matita/arithmetics/nat/discr_plus_xy_minus_xz.con"
  75 "cic:/matita/arithmetics/nat/eq_minus_O.con"
  76 "cic:/matita/arithmetics/nat/eq_minus_S_pred.con"
  77 "cic:/matita/arithmetics/nat/inv_eq_minus_O.con"
  78 "cic:/matita/arithmetics/nat/le_minus_to_plus.con"
  79 "cic:/matita/arithmetics/nat/le_minus_to_plus_r.con"
  80 "cic:/matita/arithmetics/nat/le_plus_minus_m_m.con"
  81 "cic:/matita/arithmetics/nat/le_plus_to_minus.con"
  82 "cic:/matita/arithmetics/nat/le_plus_to_minus_r.con"
  83 "cic:/matita/arithmetics/nat/lt_minus_to_plus.con"
  84 "cic:/matita/arithmetics/nat/lt_minus_to_plus_r.con"
  85 "cic:/matita/arithmetics/nat/lt_plus_to_minus.con"
  86 "cic:/matita/arithmetics/nat/lt_plus_to_minus_r.con"
  87 "cic:/matita/arithmetics/nat/minus.con"
  88 "cic:/matita/arithmetics/nat/minus_le.con"
  89 "cic:/matita/arithmetics/nat/minus_le_minus_minus_comm.con"
  90 "cic:/matita/arithmetics/nat/minus_minus_associative.con"
  91 "cic:/matita/arithmetics/nat/minus_minus_comm.con"
  92 "cic:/matita/arithmetics/nat/minus_minus.con"
  93 "cic:/matita/arithmetics/nat/minus_minus_m_m.con"
  94 "cic:/matita/arithmetics/nat/minus_n_n.con"
  95 "cic:/matita/arithmetics/nat/minus_n_O.con"
  96 "cic:/matita/arithmetics/nat/minus_O_n.con"
  97 "cic:/matita/arithmetics/nat/minus_plus.con"
  98 "cic:/matita/arithmetics/nat/minus_plus_m_m.con"
  99 "cic:/matita/arithmetics/nat/minus_plus_plus_l.con"
 100 "cic:/matita/arithmetics/nat/minus_pred_pred.con"
 101 "cic:/matita/arithmetics/nat/minus_Sn_m.con"
 102 "cic:/matita/arithmetics/nat/minus_Sn_n.con"
 103 "cic:/matita/arithmetics/nat/minus_S_S.con"
 104 "cic:/matita/arithmetics/nat/monotonic_le_minus_l.con"
 105 "cic:/matita/arithmetics/nat/monotonic_le_minus_r.con"
 106 "cic:/matita/arithmetics/nat/monotonic_lt_minus_l.con"
 107 "cic:/matita/arithmetics/nat/plus_minus_associative.con"
 108 "cic:/matita/arithmetics/nat/plus_minus.con"
 109 "cic:/matita/arithmetics/nat/plus_minus_m_m.con"
 110 "cic:/matita/arithmetics/nat/plus_minus_plus_plus_l.con"
 111 "cic:/matita/arithmetics/nat/plus_to_minus.con"
 112 "cic:/matita/arithmetics/nat/le_inv_plus_l.con"
 113 "cic:/matita/arithmetics/nat/lt_inv_plus_l.con"
 114
 115 "cic:/matita/arithmetics/nat/to_max.con"
 116 "cic:/matita/arithmetics/nat/commutative_max.con"
 117 "cic:/matita/arithmetics/nat/leb.con"
 118 "cic:/matita/arithmetics/nat/leb_elim.con"
 119 "cic:/matita/arithmetics/nat/le_maxl.con"
 120 "cic:/matita/arithmetics/nat/le_maxr.con"
 121 "cic:/matita/arithmetics/nat/le_to_leb_true.con"
 122 "cic:/matita/arithmetics/nat/max.con"
 123 "cic:/matita/arithmetics/nat/not_le_to_leb_false.con"
 124
 125 "cic:/matita/arithmetics/nat/nat_discr.con"
 126 "cic:/matita/arithmetics/nat/times.con"
 127 "cic:/matita/arithmetics/nat/times_n_1.con"
 128 "cic:/matita/arithmetics/nat/times_Sn_m.con"