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 C/props chead_ctail
  51 C/props clt_thead (ctail)
  52 C/props c_tail_ind
  53 csuba/arity csuba_arity
  54 csuba/arity csuba_arity_rev
  55 csuba/arity arity_appls_appl
  56 csuba/clear csuba_clear_conf
  57 csuba/clear csuba_clear_trans
  58 csuba/drop csuba_drop_abbr
  59 csuba/drop csuba_drop_abst
  60 csuba/drop csuba_drop_abst_rev
  61 csuba/drop csuba_drop_abbr_rev
  62 csuba/fwd csuba_gen_abbr
  63 csuba/fwd csuba_gen_void
  64 csuba/fwd csuba_gen_abst
  65 csuba/fwd csuba_gen_flat
  66 csuba/fwd csuba_gen_bind
  67 csuba/fwd csuba_gen_abst_rev
  68 csuba/fwd csuba_gen_void_rev
  69 csuba/fwd csuba_gen_abbr_rev
  70 csuba/fwd csuba_gen_flat_rev
  71 csuba/fwd csuba_gen_bind_rev
  72 csuba/getl csuba_getl_abbr
  73 csuba/getl csuba_getl_abst
  74 csuba/getl csuba_getl_abst_rev
  75 csuba/getl csuba_getl_abbr_rev
  76 csuba/props csuba_refl
  77 csubc/arity csubc_arity_conf
  78 csubc/arity csubc_arity_trans
  79 csubc/csuba csubc_csuba
  80 csubc/drop1 drop1_csubc_trans
  81 csubc/drop drop_csubc_trans
  82 csubt/clear csubt_clear_conf
  83 csubt/csuba csubt_csuba
  84 csubt/drop csubt_drop_flat
  85 csubt/drop csubt_drop_abbr
  86 csubt/drop csubt_drop_abst
  87 csubt/fwd csubt_gen_abbr
  88 csubt/fwd csubt_gen_abst
  89 csubt/fwd csubt_gen_flat
  90 csubt/fwd csubt_gen_bind
  91 csubt/getl csubt_getl_abbr
  92 csubt/getl csubt_getl_abst
  93 csubt/pc3 csubt_pr2
  94 csubt/pc3 csubt_pc3
  95 csubt/props csubt_refl
  96 csubt/ty3 csubt_ty3
  97 csubt/ty3 csubt_ty3_ld
  98 csubv/clear csubv_clear_conf
  99 csubv/clear csubv_clear_conf_void
 100 csubv/drop csubv_drop_conf
 101 csubv/getl csubv_getl_conf
 102 csubv/getl csubv_getl_conf_void
 103 csubv/props csubv_bind_same
 104 csubv/props csubv_refl
 105 drop1/props drop1_cons_tail
 106 drop/props drop_ctail
 107 ex0/props aplus_gz_le
 108 ex0/props aplus_gz_ge
 109 ex0/props next_plus_gz
 110 ex0/props leqz_leq
 111 ex0/props leq_leqz
 112 ex1/props ex1__leq_sort_SS
 113 ex1/props ex1_arity
 114 ex1/props ex1_ty3
 115 ex2/props ex2_nf2
 116 ex2/props ex2_arity
 117 fsubst0/fwd fsubst0_gen_base
 118 leq/asucc asucc_repl
 119 leq/asucc asucc_inj
 120 leq/asucc leq_asucc
 121 leq/asucc leq_ahead_asucc_false
 122 leq/asucc leq_asucc_false
 123 leq/fwd leq_gen_sort1
 124 leq/fwd leq_gen_head1
 125 leq/fwd leq_gen_sort2
 126 leq/fwd leq_gen_head2
 127 leq/props ahead_inj_snd
 128 leq/props leq_refl
 129 leq/props leq_eq
 130 leq/props leq_sym
 131 leq/props leq_trans
 132 leq/props leq_ahead_false_1
 133 leq/props leq_ahead_false_2
 134 lift1/fwd lift1_cons_tail
 135
 136 # check #############################################################
 137
 138 lift1/fwd lifts1_flat
 139 lift1/fwd lifts1_nil
 140 lift1/fwd lifts1_cons
 141 lift1/props lift1_free
 142 lift/props thead_x_lift_y_y
 143 lift/props lifts_tapp
 144
 145 # waiting ####################################################################
 146
 147 lift/props lifts_inj
 148 llt/props lweight_repl
 149 llt/props llt_repl
 150 llt/props llt_trans
 151 llt/props llt_head_sx
 152 llt/props llt_head_dx
 153 llt/props llt_wf__q_ind
 154 llt/props llt_wf_ind
 155 next_plus/props next_plus_assoc
 156 next_plus/props next_plus_next
 157 next_plus/props next_plus_lt
 158 nf2/arity arity_nf2_inv_all
 159 nf2/dec nf2_dec
 160 nf2/fwd nf2_gen_lref
 161 nf2/fwd nf2_gen_abst
 162 nf2/fwd nf2_gen_cast
 163 nf2/fwd nf2_gen_beta
 164 nf2/fwd nf2_gen_flat
 165 nf2/fwd nf2_gen__nf2_gen_aux
 166 nf2/fwd nf2_gen_abbr
 167 nf2/fwd nf2_gen_void
 168 nf2/iso nf2_iso_appls_lref
 169 nf2/lift1 nf2_lift1
 170 nf2/pr3 nf2_pr3_unfold
 171 nf2/pr3 nf2_pr3_confluence
 172 nf2/props nf2_sort
 173 nf2/props nf2_csort_lref
 174 nf2/props nf2_abst
 175 nf2/props nf2_abst_shift
 176 nf2/props nfs2_tapp
 177 nf2/props nf2_appls_lref
 178 nf2/props nf2_appl_lref
 179 nf2/props nf2_lref_abst
 180 nf2/props nf2_lift
 181 pc1/props pc1_pr0_r
 182 pc1/props pc1_pr0_x
 183 pc1/props pc1_refl
 184 pc1/props pc1_pr0_u
 185 pc1/props pc1_s
 186 pc1/props pc1_head_1
 187 pc1/props pc1_head_2
 188 pc1/props pc1_t
 189 pc1/props pc1_pr0_u2
 190 pc1/props pc1_head
 191 pc3/dec pc3_dec
 192 pc3/dec pc3_abst_dec
 193 pc3/fsubst0 pc3_pr2_fsubst0
 194 pc3/fsubst0 pc3_pr2_fsubst0_back
 195 pc3/fsubst0 pc3_fsubst0
 196 pc3/fwd pc3_gen_sort
 197 pc3/fwd pc3_gen_abst
 198 pc3/fwd pc3_gen_abst_shift
 199 pc3/fwd pc3_gen_lift
 200 pc3/fwd pc3_gen_not_abst
 201 pc3/fwd pc3_gen_lift_abst
 202 pc3/fwd pc3_gen_sort_abst
 203 pc3/left pc3_ind_left__pc3_left_pr3
 204 pc3/left pc3_ind_left__pc3_left_trans
 205 pc3/left pc3_ind_left__pc3_left_sym
 206 pc3/left pc3_ind_left__pc3_left_pc3
 207 pc3/left pc3_ind_left__pc3_pc3_left
 208 pc3/left pc3_ind_left
 209 pc3/nf2 pc3_nf2
 210 pc3/nf2 pc3_nf2_unfold
 211 pc3/pc1 pc3_pc1
 212 pc3/props clear_pc3_trans
 213 pc3/props pc3_pr2_r
 214 pc3/props pc3_pr2_x
 215 pc3/props pc3_pr3_r
 216 pc3/props pc3_pr3_x
 217 pc3/props pc3_pr3_t
 218 pc3/props pc3_refl
 219 pc3/props pc3_s
 220 pc3/props pc3_thin_dx
 221 pc3/props pc3_head_1
 222 pc3/props pc3_head_2
 223 pc3/props pc3_pr2_u
 224 pc3/props pc3_t
 225 pc3/props pc3_pr2_u2
 226 pc3/props pc3_pr3_conf
 227 pc3/props pc3_head_12
 228 pc3/props pc3_head_21
 229 pc3/props pc3_pr0_pr2_t
 230 pc3/props pc3_pr2_pr2_t
 231 pc3/props pc3_pr2_pr3_t
 232 pc3/props pc3_pr3_pc3_t
 233 pc3/props pc3_lift
 234 pc3/props pc3_eta
 235 pc3/subst1 pc3_gen_cabbr
 236 pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
 237 pc3/wcpr0 pc3_wcpr0_t
 238 pc3/wcpr0 pc3_wcpr0
 239 pr0/fwd pr0_gen_void
 240
 241 # check #############################################################
 242
 243 pr0/dec nf0_dec
 244 pr0/subst1 pr0_subst1_back
 245 pr0/subst1 pr0_subst1_fwd
 246 pr1/pr1 pr1_strip
 247 pr1/pr1 pr1_confluence
 248 pr1/props pr1_pr0
 249 pr1/props pr1_t
 250 pr1/props pr1_head_1
 251 pr1/props pr1_head_2
 252 pr1/props pr1_comp
 253 pr1/props pr1_eta
 254 pr2/clen pr2_gen_ctail
 255 pr2/fwd pr2_gen_void
 256 pr2/props pr2_ctail
 257 pr2/subst1 pr2_gen_cabbr
 258 pr3/fwd pr3_gen_sort
 259 pr3/fwd pr3_gen_abst
 260 pr3/fwd pr3_gen_cast
 261 pr3/fwd pr3_gen_lift
 262 pr3/fwd pr3_gen_lref
 263 pr3/fwd pr3_gen_void
 264 pr3/fwd pr3_gen_abbr
 265 pr3/fwd pr3_gen_appl
 266 pr3/fwd pr3_gen_bind
 267 pr3/iso pr3_iso_appls_abbr
 268 pr3/iso pr3_iso_appls_cast
 269 pr3/iso pr3_iso_appl_bind
 270 pr3/iso pr3_iso_appls_appl_bind
 271 pr3/iso pr3_iso_appls_bind
 272 pr3/iso pr3_iso_beta
 273 pr3/iso pr3_iso_appls_beta
 274 pr3/pr1 pr3_pr1
 275 pr3/pr3 pr3_strip
 276 pr3/pr3 pr3_confluence
 277 pr3/props clear_pr3_trans
 278 pr3/props pr3_pr2
 279 pr3/props pr3_t
 280 pr3/props pr3_thin_dx
 281 pr3/props pr3_head_1
 282 pr3/props pr3_head_2
 283 pr3/props pr3_head_21
 284 pr3/props pr3_head_12
 285 pr3/props pr3_cflat
 286 pr3/props pr3_flat
 287 pr3/props pr3_pr0_pr2_t
 288 pr3/props pr3_pr2_pr2_t
 289 pr3/props pr3_pr2_pr3_t
 290 pr3/props pr3_pr3_pr3_t
 291 pr3/props pr3_lift
 292 pr3/props pr3_eta
 293 pr3/subst1 pr3_subst1
 294 pr3/subst1 pr3_gen_cabbr
 295 pr3/wcpr0 pr3_wcpr0_t
 296 sc3/arity sc3_arity_csubc
 297 sc3/arity sc3_arity
 298 sc3/props sc3_arity_gen
 299 sc3/props sc3_repl
 300 sc3/props sc3_lift
 301 sc3/props sc3_lift1
 302 sc3/props sc3_abbr
 303 sc3/props sc3_cast
 304 sc3/props sc3_props__sc3_sn3_abst
 305 sc3/props sc3_sn3
 306 sc3/props sc3_abst
 307 sc3/props sc3_bind
 308 sc3/props sc3_appl
 309 sn3/fwd sn3_gen_bind
 310 sn3/fwd sn3_gen_flat
 311 sn3/fwd sn3_gen_head
 312 sn3/fwd sn3_gen_cflat
 313 sn3/fwd sn3_gen_lift
 314 sn3/lift1 sns3_lifts1
 315 sn3/nf2 sn3_nf2
 316 sn3/nf2 nf2_sn3
 317 sn3/props sn3_pr3_trans
 318 sn3/props sn3_pr2_intro
 319 sn3/props sn3_cast
 320 sn3/props sn3_cflat
 321 sn3/props sn3_shift
 322 sn3/props sn3_change
 323 sn3/props sn3_gen_def
 324 sn3/props sn3_cdelta
 325 sn3/props sn3_cpr3_trans
 326 sn3/props sn3_bind
 327 sn3/props sn3_beta
 328 sn3/props sn3_appl_lref
 329 sn3/props sn3_appl_abbr
 330 sn3/props sn3_appl_cast
 331 sn3/props sn3_appl_bind
 332 sn3/props sn3_appl_appl
 333 sn3/props sn3_appl_beta
 334 sn3/props sn3_appl_appls
 335 sn3/props sn3_appls_lref
 336 sn3/props sn3_appls_cast
 337 sn3/props sn3_appls_bind
 338 sn3/props sn3_appls_beta
 339 sn3/props sn3_lift
 340 sn3/props sn3_abbr
 341 sn3/props sn3_appls_abbr
 342 sn3/props sns3_lifts
 343 sty0/fwd sty0_gen_sort
 344 sty0/fwd sty0_gen_lref
 345 sty0/fwd sty0_gen_bind
 346 sty0/fwd sty0_gen_appl
 347 sty0/fwd sty0_gen_cast
 348 sty0/props sty0_lift
 349 sty0/props sty0_correct
 350 sty1/cnt sty1_cnt
 351 sty1/props sty1_trans
 352 sty1/props sty1_bind
 353 sty1/props sty1_appl
 354 sty1/props sty1_lift
 355 sty1/props sty1_correct
 356 sty1/props sty1_abbr
 357 sty1/props sty1_cast2
 358 subst/fwd subst_sort
 359 subst/fwd subst_lref_lt
 360 subst/fwd subst_lref_eq
 361 subst/fwd subst_lref_gt
 362 subst/fwd subst_head
 363 subst/props subst_lift_SO
 364 subst/props subst_subst0
 365 T/dec binder_dec
 366 T/dec abst_dec
 367 tlist/props tslt_wf__q_ind
 368 tlist/props tslt_wf_ind
 369 tlist/props theads_tapp
 370 tlist/props tcons_tapp_ex
 371 tlist/props tlist_ind_rev
 372 ty3/arity ty3_arity
 373 ty3/arity_props ty3_predicative
 374 ty3/arity_props ty3_repellent
 375 ty3/arity_props ty3_acyclic
 376 ty3/arity_props ty3_sn3
 377 ty3/dec ty3_inference
 378 ty3/fsubst0 ty3_fsubst0
 379 ty3/fsubst0 ty3_csubst0
 380 ty3/fsubst0 ty3_subst0
 381 ty3/fwd ty3_gen_sort
 382 ty3/fwd ty3_gen_lref
 383 ty3/fwd ty3_gen_bind
 384 ty3/fwd ty3_gen_appl
 385 ty3/fwd ty3_gen_cast
 386 ty3/fwd tys3_gen_nil
 387 ty3/fwd tys3_gen_cons
 388 ty3/fwd_nf2 ty3_gen_appl_nf2
 389 ty3/fwd_nf2 ty3_inv_lref_nf2_pc3
 390 ty3/fwd_nf2 ty3_inv_lref_nf2
 391 ty3/fwd_nf2 ty3_inv_appls_lref_nf2
 392 ty3/fwd_nf2 ty3_inv_lref_lref_nf2
 393 ty3/nf2 ty3_nf2_inv_abst_premise_csort
 394 ty3/nf2 ty3_nf2_inv_all
 395 ty3/nf2 ty3_nf2_inv_sort
 396 ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux
 397 ty3/nf2 ty3_nf2_inv_abst
 398 ty3/pr3 ty3_sred_wcpr0_pr0
 399 ty3/pr3 ty3_sred_pr0
 400 ty3/pr3 ty3_sred_pr1
 401 ty3/pr3 ty3_sred_pr2
 402 ty3/pr3 ty3_sred_pr3
 403 ty3/pr3_props ty3_cred_pr2
 404 ty3/pr3_props ty3_cred_pr3
 405 ty3/pr3_props ty3_gen_lift
 406 ty3/pr3_props ty3_tred
 407 ty3/pr3_props ty3_sconv_pc3
 408 ty3/pr3_props ty3_sred_back
 409 ty3/pr3_props ty3_sconv
 410 ty3/props ty3_lift
 411 ty3/props ty3_correct
 412 ty3/props ty3_unique
 413 ty3/props ty3_gen_abst_abst
 414 ty3/props ty3_typecheck
 415 ty3/props ty3_getl_subst0
 416 ty3/sty0 ty3_sty0
 417 ty3/subst1 ty3_gen_cabbr
 418 ty3/subst1 ty3_gen_cvoid
 419 wf3/clear wf3_clear_conf
 420 wf3/clear clear_wf3_trans
 421 wf3/fwd wf3_gen_sort1
 422 wf3/fwd wf3_gen_bind1
 423 wf3/fwd wf3_gen_flat1
 424 wf3/fwd wf3_gen_head2
 425 wf3/getl wf3_getl_conf
 426 wf3/getl getl_wf3_trans
 427 wf3/props wf3_mono
 428 wf3/props wf3_total
 429 wf3/props ty3_shift1
 430 wf3/props wf3_idem
 431 wf3/props wf3_ty3
 432 wf3/ty3 wf3_pr2_conf
 433 wf3/ty3 wf3_pr3_conf
 434 wf3/ty3 wf3_pc3_conf
 435 wf3/ty3 wf3_ty3_conf
 436
 437 # check ######################################################################