matita/matita/contribs/lambda_delta/basic_2/basic_1.txt

   1 # waiting ####################################################################
   2
   3 aplus/props aplus_reg_r
   4 aplus/props aplus_assoc
   5 aplus/props aplus_asucc
   6 aplus/props aplus_sort_O_S_simpl
   7 aplus/props aplus_sort_S_S_simpl
   8 aplus/props aplus_asort_O_simpl
   9 aplus/props aplus_asort_le_simpl
  10 aplus/props aplus_asort_simpl
  11 aplus/props aplus_ahead_simpl
  12 aplus/props aplus_asucc_false
  13 aplus/props aplus_inj
  14 aprem/fwd aprem_gen_sort
  15 aprem/fwd aprem_gen_head_O
  16 aprem/fwd aprem_gen_head_S
  17 aprem/props aprem_repl
  18 aprem/props aprem_asucc
  19 arity/aprem arity_aprem
  20 arity/cimp arity_cimp_conf
  21 arity/fwd arity_gen_sort
  22 arity/fwd arity_gen_lref
  23 arity/fwd arity_gen_bind
  24 arity/fwd arity_gen_abst
  25 arity/fwd arity_gen_appl
  26 arity/fwd arity_gen_cast
  27 arity/fwd arity_gen_appls
  28 arity/fwd arity_gen_lift
  29 arity/lift1 arity_lift1
  30 arity/pr3 arity_sred_wcpr0_pr0
  31 arity/pr3 arity_sred_wcpr0_pr1
  32 arity/pr3 arity_sred_pr2
  33 arity/pr3 arity_sred_pr3
  34 arity/props node_inh
  35 arity/props arity_lift
  36 arity/props arity_mono
  37 arity/props arity_repellent
  38 arity/props arity_appls_cast
  39 arity/props arity_appls_abbr
  40 arity/props arity_appls_bind
  41 arity/subst0 arity_gen_cvoid_subst0
  42 arity/subst0 arity_gen_cvoid
  43 arity/subst0 arity_fsubst0
  44 arity/subst0 arity_subst0
  45 asucc/fwd asucc_gen_sort
  46 asucc/fwd asucc_gen_head
  47 cnt/props cnt_lift
  48 C/props clt_wf__q_ind
  49 C/props clt_wf_ind
  50 csuba/arity csuba_arity
  51 csuba/arity csuba_arity_rev
  52 csuba/arity arity_appls_appl
  53 csuba/clear csuba_clear_conf
  54 csuba/clear csuba_clear_trans
  55 csuba/drop csuba_drop_abbr
  56 csuba/drop csuba_drop_abst
  57 csuba/drop csuba_drop_abst_rev
  58 csuba/drop csuba_drop_abbr_rev
  59 csuba/fwd csuba_gen_abbr
  60 csuba/fwd csuba_gen_void
  61 csuba/fwd csuba_gen_abst
  62 csuba/fwd csuba_gen_flat
  63 csuba/fwd csuba_gen_bind
  64 csuba/fwd csuba_gen_abst_rev
  65 csuba/fwd csuba_gen_void_rev
  66 csuba/fwd csuba_gen_abbr_rev
  67 csuba/fwd csuba_gen_flat_rev
  68 csuba/fwd csuba_gen_bind_rev
  69 csuba/getl csuba_getl_abbr
  70 csuba/getl csuba_getl_abst
  71 csuba/getl csuba_getl_abst_rev
  72 csuba/getl csuba_getl_abbr_rev
  73 csuba/props csuba_refl
  74 csubc/arity csubc_arity_conf
  75 csubc/arity csubc_arity_trans
  76 csubc/csuba csubc_csuba
  77 csubc/drop1 drop1_csubc_trans
  78 csubc/drop drop_csubc_trans
  79 csubt/clear csubt_clear_conf
  80 csubt/csuba csubt_csuba
  81 csubt/drop csubt_drop_flat
  82 csubt/drop csubt_drop_abbr
  83 csubt/drop csubt_drop_abst
  84 csubt/fwd csubt_gen_abbr
  85 csubt/fwd csubt_gen_abst
  86 csubt/fwd csubt_gen_flat
  87 csubt/fwd csubt_gen_bind
  88 csubt/getl csubt_getl_abbr
  89 csubt/getl csubt_getl_abst
  90 csubt/pc3 csubt_pr2
  91 csubt/pc3 csubt_pc3
  92 csubt/props csubt_refl
  93 csubt/ty3 csubt_ty3
  94 csubt/ty3 csubt_ty3_ld
  95 csubv/clear csubv_clear_conf
  96 csubv/clear csubv_clear_conf_void
  97 csubv/drop csubv_drop_conf
  98 csubv/getl csubv_getl_conf
  99 csubv/getl csubv_getl_conf_void
 100 csubv/props csubv_bind_same
 101 csubv/props csubv_refl
 102 drop1/props drop1_cons_tail
 103 ex0/props aplus_gz_le
 104 ex0/props aplus_gz_ge
 105 ex0/props next_plus_gz
 106 ex0/props leqz_leq
 107 ex0/props leq_leqz
 108 ex1/props ex1__leq_sort_SS
 109 ex1/props ex1_arity
 110 ex1/props ex1_ty3
 111 ex2/props ex2_nf2
 112 ex2/props ex2_arity
 113 fsubst0/fwd fsubst0_gen_base
 114 leq/asucc asucc_repl
 115 leq/asucc asucc_inj
 116 leq/asucc leq_asucc
 117 leq/asucc leq_ahead_asucc_false
 118 leq/asucc leq_asucc_false
 119 leq/fwd leq_gen_sort1
 120 leq/fwd leq_gen_head1
 121 leq/fwd leq_gen_sort2
 122 leq/fwd leq_gen_head2
 123 leq/props ahead_inj_snd
 124 leq/props leq_refl
 125 leq/props leq_eq
 126 leq/props leq_sym
 127 leq/props leq_trans
 128 leq/props leq_ahead_false_1
 129 leq/props leq_ahead_false_2
 130 lift1/fwd lift1_cons_tail
 131 lift1/fwd lifts1_nil
 132 lift1/fwd lifts1_cons
 133 lift/props thead_x_lift_y_y
 134 lift/props lifts_tapp
 135 lift/props lifts_inj
 136 llt/props lweight_repl
 137 llt/props llt_repl
 138 llt/props llt_trans
 139 llt/props llt_head_sx
 140 llt/props llt_head_dx
 141 llt/props llt_wf__q_ind
 142 llt/props llt_wf_ind
 143 next_plus/props next_plus_assoc
 144 next_plus/props next_plus_next
 145 next_plus/props next_plus_lt
 146 nf2/arity arity_nf2_inv_all
 147 nf2/fwd nf2_gen_lref
 148 nf2/fwd nf2_gen_abst
 149 nf2/fwd nf2_gen_cast
 150 nf2/fwd nf2_gen_beta
 151 nf2/fwd nf2_gen_flat
 152 nf2/fwd nf2_gen__nf2_gen_aux
 153 nf2/fwd nf2_gen_abbr
 154 nf2/fwd nf2_gen_void
 155 nf2/props nfs2_tapp
 156 nf2/props nf2_appls_lref
 157 pc1/props pc1_pr0_r
 158 pc1/props pc1_pr0_x
 159 pc1/props pc1_refl
 160 pc1/props pc1_pr0_u
 161 pc1/props pc1_s
 162 pc1/props pc1_head_1
 163 pc1/props pc1_head_2
 164 pc1/props pc1_t
 165 pc1/props pc1_pr0_u2
 166 pc1/props pc1_head
 167 pc3/dec pc3_dec
 168 pc3/dec pc3_abst_dec
 169 pc3/fsubst0 pc3_pr2_fsubst0
 170 pc3/fsubst0 pc3_pr2_fsubst0_back
 171 pc3/fsubst0 pc3_fsubst0
 172 pc3/fwd pc3_gen_sort
 173 pc3/fwd pc3_gen_abst
 174 pc3/fwd pc3_gen_abst_shift
 175 pc3/fwd pc3_gen_lift
 176 pc3/fwd pc3_gen_not_abst
 177 pc3/fwd pc3_gen_lift_abst
 178 pc3/fwd pc3_gen_sort_abst
 179 pc3/left pc3_ind_left__pc3_left_pr3
 180 pc3/left pc3_ind_left__pc3_left_trans
 181 pc3/left pc3_ind_left__pc3_left_sym
 182 pc3/left pc3_ind_left__pc3_left_pc3
 183 pc3/left pc3_ind_left__pc3_pc3_left
 184 pc3/left pc3_ind_left
 185 pc3/nf2 pc3_nf2
 186 pc3/nf2 pc3_nf2_unfold
 187 pc3/pc1 pc3_pc1
 188 pc3/props pc3_pr2_r
 189 pc3/props pc3_pr2_x
 190 pc3/props pc3_pr3_r
 191 pc3/props pc3_pr3_x
 192 pc3/props pc3_pr3_t
 193 pc3/props pc3_s
 194 pc3/props pc3_thin_dx
 195 pc3/props pc3_head_1
 196 pc3/props pc3_head_2
 197 pc3/props pc3_pr2_u
 198 pc3/props pc3_t
 199 pc3/props pc3_pr2_u2
 200 pc3/props pc3_pr3_conf
 201 pc3/props pc3_head_12
 202 pc3/props pc3_head_21
 203 pc3/props pc3_pr0_pr2_t
 204 pc3/props pc3_pr2_pr2_t
 205 pc3/props pc3_pr2_pr3_t
 206 pc3/props pc3_pr3_pc3_t
 207 pc3/props pc3_lift
 208 pc3/props pc3_eta
 209 pc3/subst1 pc3_gen_cabbr
 210 pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
 211 pc3/wcpr0 pc3_wcpr0_t
 212 pc3/wcpr0 pc3_wcpr0
 213 pr0/fwd pr0_gen_void
 214 pr0/dec nf0_dec
 215 pr0/subst1 pr0_subst1_back
 216 pr0/subst1 pr0_subst1_fwd
 217 pr1/pr1 pr1_strip
 218 pr1/pr1 pr1_confluence
 219 pr1/props pr1_pr0
 220 pr1/props pr1_t
 221 pr1/props pr1_head_1
 222 pr1/props pr1_head_2
 223 pr1/props pr1_comp
 224 pr1/props pr1_eta
 225 pr2/fwd pr2_gen_void
 226 pr2/subst1 pr2_gen_cabbr
 227 pr3/fwd pr3_gen_void
 228 pr3/pr1 pr3_pr1
 229 pr3/props pr3_eta
 230 pr3/subst1 pr3_gen_cabbr
 231 sn3/props sns3_lifts
 232 sty0/fwd sty0_gen_sort
 233 sty0/fwd sty0_gen_lref
 234 sty0/fwd sty0_gen_bind
 235 sty0/fwd sty0_gen_appl
 236 sty0/fwd sty0_gen_cast
 237 sty0/props sty0_lift
 238 sty0/props sty0_correct
 239 sty1/cnt sty1_cnt
 240 sty1/props sty1_trans
 241 sty1/props sty1_bind
 242 sty1/props sty1_appl
 243 sty1/props sty1_lift
 244 sty1/props sty1_correct
 245 sty1/props sty1_abbr
 246 sty1/props sty1_cast2
 247 subst/fwd subst_sort
 248 subst/fwd subst_lref_lt
 249 subst/fwd subst_lref_eq
 250 subst/fwd subst_lref_gt
 251 subst/fwd subst_head
 252 subst/props subst_lift_SO
 253 subst/props subst_subst0
 254 T/dec binder_dec
 255 T/dec abst_dec
 256 tlist/props tslt_wf__q_ind
 257 tlist/props tslt_wf_ind
 258 tlist/props theads_tapp
 259 tlist/props tcons_tapp_ex
 260 tlist/props tlist_ind_rev
 261 ty3/arity ty3_arity
 262 ty3/arity_props ty3_predicative
 263 ty3/arity_props ty3_repellent
 264 ty3/arity_props ty3_acyclic
 265 ty3/arity_props ty3_sn3
 266 ty3/dec ty3_inference
 267 ty3/fsubst0 ty3_fsubst0
 268 ty3/fsubst0 ty3_csubst0
 269 ty3/fsubst0 ty3_subst0
 270 ty3/fwd ty3_gen_sort
 271 ty3/fwd ty3_gen_lref
 272 ty3/fwd ty3_gen_bind
 273 ty3/fwd ty3_gen_appl
 274 ty3/fwd ty3_gen_cast
 275 ty3/fwd tys3_gen_nil
 276 ty3/fwd tys3_gen_cons
 277 ty3/fwd_nf2 ty3_gen_appl_nf2
 278 ty3/fwd_nf2 ty3_inv_lref_nf2_pc3
 279 ty3/fwd_nf2 ty3_inv_lref_nf2
 280 ty3/fwd_nf2 ty3_inv_appls_lref_nf2
 281 ty3/fwd_nf2 ty3_inv_lref_lref_nf2
 282 ty3/nf2 ty3_nf2_inv_abst_premise_csort
 283 ty3/nf2 ty3_nf2_inv_all
 284 ty3/nf2 ty3_nf2_inv_sort
 285 ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux
 286 ty3/nf2 ty3_nf2_inv_abst
 287 ty3/pr3 ty3_sred_wcpr0_pr0
 288 ty3/pr3 ty3_sred_pr0
 289 ty3/pr3 ty3_sred_pr1
 290 ty3/pr3 ty3_sred_pr2
 291 ty3/pr3 ty3_sred_pr3
 292 ty3/pr3_props ty3_cred_pr2
 293 ty3/pr3_props ty3_cred_pr3
 294 ty3/pr3_props ty3_gen_lift
 295 ty3/pr3_props ty3_tred
 296 ty3/pr3_props ty3_sconv_pc3
 297 ty3/pr3_props ty3_sred_back
 298 ty3/pr3_props ty3_sconv
 299 ty3/props ty3_lift
 300 ty3/props ty3_correct
 301 ty3/props ty3_unique
 302 ty3/props ty3_gen_abst_abst
 303 ty3/props ty3_typecheck
 304 ty3/props ty3_getl_subst0
 305 ty3/sty0 ty3_sty0
 306 ty3/subst1 ty3_gen_cabbr
 307 ty3/subst1 ty3_gen_cvoid
 308 wf3/clear wf3_clear_conf
 309 wf3/clear clear_wf3_trans
 310 wf3/fwd wf3_gen_sort1
 311 wf3/fwd wf3_gen_bind1
 312 wf3/fwd wf3_gen_flat1
 313 wf3/fwd wf3_gen_head2
 314 wf3/getl wf3_getl_conf
 315 wf3/getl getl_wf3_trans
 316 wf3/props wf3_mono
 317 wf3/props wf3_total
 318 wf3/props ty3_shift1
 319 wf3/props wf3_idem
 320 wf3/props wf3_ty3
 321 wf3/ty3 wf3_pr2_conf
 322 wf3/ty3 wf3_pr3_conf
 323 wf3/ty3 wf3_pc3_conf
 324 wf3/ty3 wf3_ty3_conf
 325
 326 # check ######################################################################