matita/matita/contribs/lambdadelta/basic_2/basic_1.txt

   1 # new ########################################################################
   2
   3 s_le_gen s_lt_gen
   4 r_arith2 r_arith3 r_arith4 r_arith5 r_arith6 r_arith7
   5 tle tle_r
   6 cle_r cle_head cle_trans_head cle_flt_trans
   7 lift_tle lift_free_sym
   8 subst0_gen_lift_rev_ge
   9
  10 # waiting ####################################################################
  11
  12 aplus/props aplus_reg_r
  13 aplus/props aplus_assoc
  14 aplus/props aplus_asucc
  15 aplus/props aplus_sort_O_S_simpl
  16 aplus/props aplus_sort_S_S_simpl
  17 aplus/props aplus_asort_O_simpl
  18 aplus/props aplus_asort_le_simpl
  19 aplus/props aplus_asort_simpl
  20 aplus/props aplus_ahead_simpl
  21 aplus/props aplus_asucc_false
  22 aplus/props aplus_inj
  23 aprem/fwd aprem_gen_sort
  24 aprem/fwd aprem_gen_head_O
  25 aprem/fwd aprem_gen_head_S
  26 aprem/props aprem_repl
  27 aprem/props aprem_asucc
  28 arity/aprem arity_aprem
  29 arity/cimp arity_cimp_conf
  30 arity/fwd arity_gen_sort
  31 arity/fwd arity_gen_lref
  32 arity/fwd arity_gen_bind
  33 arity/fwd arity_gen_abst
  34 arity/fwd arity_gen_appl
  35 arity/fwd arity_gen_cast
  36 arity/fwd arity_gen_appls
  37 arity/fwd arity_gen_lift
  38 arity/lift1 arity_lift1
  39 arity/pr3 arity_sred_wcpr0_pr0
  40 arity/pr3 arity_sred_wcpr0_pr1
  41 arity/pr3 arity_sred_pr2
  42 arity/pr3 arity_sred_pr3
  43 arity/props node_inh
  44 arity/props arity_lift
  45 arity/props arity_mono
  46 arity/props arity_repellent
  47 arity/props arity_appls_cast
  48 arity/props arity_appls_abbr
  49 arity/props arity_appls_bind
  50 arity/subst0 arity_gen_cvoid_subst0
  51 arity/subst0 arity_gen_cvoid
  52 arity/subst0 arity_fsubst0
  53 arity/subst0 arity_subst0
  54 asucc/fwd asucc_gen_sort
  55 asucc/fwd asucc_gen_head
  56
  57 cnt/props cnt_lift
  58
  59 csuba/arity csuba_arity
  60 csuba/arity csuba_arity_rev
  61 csuba/arity arity_appls_appl
  62 csuba/clear csuba_clear_conf
  63 csuba/clear csuba_clear_trans
  64 csuba/drop csuba_drop_abbr
  65 csuba/drop csuba_drop_abst
  66 csuba/drop csuba_drop_abst_rev
  67 csuba/drop csuba_drop_abbr_rev
  68 csuba/fwd csuba_gen_abbr
  69 csuba/fwd csuba_gen_void
  70 csuba/fwd csuba_gen_abst
  71 csuba/fwd csuba_gen_flat
  72 csuba/fwd csuba_gen_bind
  73 csuba/fwd csuba_gen_abst_rev
  74 csuba/fwd csuba_gen_void_rev
  75 csuba/fwd csuba_gen_abbr_rev
  76 csuba/fwd csuba_gen_flat_rev
  77 csuba/fwd csuba_gen_bind_rev
  78 csuba/getl csuba_getl_abbr
  79 csuba/getl csuba_getl_abst
  80 csuba/getl csuba_getl_abst_rev
  81 csuba/getl csuba_getl_abbr_rev
  82 csuba/props csuba_refl
  83
  84 csubc/arity csubc_arity_conf
  85 csubc/arity csubc_arity_trans
  86 csubc/drop1 drop1_csubc_trans
  87 csubc/drop drop_csubc_trans
  88
  89 csubt/csuba csubt_csuba
  90 csubt/fwd csubt_gen_abbr
  91 csubt/fwd csubt_gen_abst
  92
  93 csubv/clear csubv_clear_conf
  94 csubv/clear csubv_clear_conf_void
  95 csubv/drop csubv_drop_conf
  96 csubv/getl csubv_getl_conf
  97 csubv/getl csubv_getl_conf_void
  98 csubv/props csubv_bind_same
  99 csubv/props csubv_refl
 100 drop1/props drop1_cons_tail
 101 ex0/props aplus_gz_le
 102 ex0/props aplus_gz_ge
 103 ex0/props next_plus_gz
 104 ex0/props leqz_leq
 105 ex0/props leq_leqz
 106 ex1/props ex1__leq_sort_SS
 107 ex1/props ex1_arity
 108 ex1/props ex1_ty3
 109 ex2/props ex2_nf2
 110 ex2/props ex2_arity
 111 leq/asucc asucc_repl
 112 leq/asucc asucc_inj
 113 leq/asucc leq_asucc
 114 leq/asucc leq_ahead_asucc_false
 115 leq/asucc leq_asucc_false
 116 leq/fwd leq_gen_sort1
 117 leq/fwd leq_gen_head1
 118 leq/fwd leq_gen_sort2
 119 leq/fwd leq_gen_head2
 120 leq/props ahead_inj_snd
 121 leq/props leq_refl
 122 leq/props leq_eq
 123 leq/props leq_sym
 124 leq/props leq_trans
 125 leq/props leq_ahead_false_1
 126 leq/props leq_ahead_false_2
 127 lift1/fwd lift1_cons_tail
 128 lift/props lifts_tapp
 129 llt/props lweight_repl
 130 llt/props llt_repl
 131 llt/props llt_trans
 132 llt/props llt_head_sx
 133 llt/props llt_head_dx
 134 llt/props llt_wf__q_ind
 135 llt/props llt_wf_ind
 136 next_plus/props next_plus_assoc
 137 next_plus/props next_plus_next
 138 next_plus/props next_plus_lt
 139 nf2/arity arity_nf2_inv_all
 140 nf2/fwd nf2_gen_lref
 141 nf2/fwd nf2_gen_abst
 142 nf2/fwd nf2_gen_cast
 143 nf2/fwd nf2_gen_beta
 144 nf2/fwd nf2_gen_flat
 145 nf2/fwd nf2_gen__nf2_gen_aux
 146 nf2/fwd nf2_gen_abbr
 147 nf2/fwd nf2_gen_void
 148 nf2/props nfs2_tapp
 149 nf2/props nf2_appls_lref
 150 pc1/props pc1_pr0_r
 151 pc1/props pc1_pr0_x
 152 pc1/props pc1_refl
 153 pc1/props pc1_pr0_u
 154 pc1/props pc1_s
 155 pc1/props pc1_head_1
 156 pc1/props pc1_head_2
 157 pc1/props pc1_t
 158 pc1/props pc1_pr0_u2
 159 pc1/props pc1_head
 160
 161 pc3/dec pc3_dec
 162 pc3/dec pc3_abst_dec
 163 pc3/fwd pc3_gen_not_abst
 164 pc3/fwd pc3_gen_lift_abst
 165 pc3/nf2 pc3_nf2
 166 pc3/nf2 pc3_nf2_unfold
 167 pc3/pc1 pc3_pc1
 168 pc3/props pc3_pr2_pr2_t
 169 pc3/props pc3_pr2_pr3_t
 170 pc3/props pc3_pr3_pc3_t
 171 pc3/props pc3_eta
 172
 173 pr0/fwd pr0_gen_void
 174 pr0/dec nf0_dec
 175
 176 pr1/props pr1_eta
 177
 178 pr2/fwd pr2_gen_void
 179 pr3/fwd pr3_gen_void
 180 pr3/props pr3_eta
 181 sn3/props sns3_lifts
 182 sty1/cnt sty1_cnt
 183 subst/fwd subst_sort
 184 subst/fwd subst_lref_lt
 185 subst/fwd subst_lref_eq
 186 subst/fwd subst_lref_gt
 187 subst/fwd subst_head
 188 subst/props subst_lift_SO
 189 subst/props subst_subst0
 190 T/dec binder_dec
 191 T/dec abst_dec
 192 tlist/props tslt_wf__q_ind
 193 tlist/props tslt_wf_ind
 194 tlist/props theads_tapp
 195 tlist/props tcons_tapp_ex
 196 tlist/props tlist_ind_rev
 197 ty3/arity ty3_arity
 198 ty3/arity_props ty3_predicative
 199 ty3/arity_props ty3_repellent
 200 ty3/arity_props ty3_acyclic
 201 ty3/dec ty3_inference
 202 ty3/fwd tys3_gen_nil
 203 ty3/fwd tys3_gen_cons
 204 ty3/fwd_nf2 ty3_gen_appl_nf2
 205 ty3/fwd_nf2 ty3_inv_lref_nf2_pc3
 206 ty3/fwd_nf2 ty3_inv_lref_nf2
 207 ty3/fwd_nf2 ty3_inv_appls_lref_nf2
 208 ty3/fwd_nf2 ty3_inv_lref_lref_nf2
 209 ty3/nf2 ty3_nf2_inv_abst_premise_csort
 210 ty3/nf2 ty3_nf2_inv_all
 211 ty3/nf2 ty3_nf2_inv_sort
 212 ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux
 213 ty3/nf2 ty3_nf2_inv_abst
 214 ty3/pr3 ty3_sred_wcpr0_pr0
 215 ty3/pr3 ty3_sred_pr0
 216 ty3/pr3 ty3_sred_pr1
 217 ty3/pr3 ty3_sred_pr2
 218 ty3/pr3 ty3_sred_pr3
 219 ty3/pr3_props ty3_cred_pr2
 220 ty3/pr3_props ty3_cred_pr3
 221 ty3/pr3_props ty3_gen_lift
 222 ty3/pr3_props ty3_tred
 223 ty3/pr3_props ty3_sconv_pc3
 224 ty3/pr3_props ty3_sred_back
 225 ty3/pr3_props ty3_sconv
 226 ty3/props ty3_gen_abst_abst
 227 ty3/sty0 ty3_sty0
 228 ty3/subst1 ty3_gen_cvoid
 229
 230 wf3/clear wf3_clear_conf
 231 wf3/clear clear_wf3_trans
 232 wf3/fwd wf3_gen_sort1
 233 wf3/fwd wf3_gen_bind1
 234 wf3/fwd wf3_gen_flat1
 235 wf3/fwd wf3_gen_head2
 236 wf3/getl wf3_getl_conf
 237 wf3/getl getl_wf3_trans
 238 wf3/props wf3_mono
 239 wf3/props wf3_total
 240 wf3/props ty3_shift1
 241 wf3/props wf3_idem
 242 wf3/props wf3_ty3
 243 wf3/ty3 wf3_pr2_conf
 244 wf3/ty3 wf3_pr3_conf
 245 wf3/ty3 wf3_pc3_conf
 246 wf3/ty3 wf3_ty3_conf
 247
 248 # check ######################################################################
 249