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/clear csubc_clear_conf
  80 csubc/csuba csubc_csuba
  81 csubc/drop1 drop1_csubc_trans
  82 csubc/drop1 csubc_drop1_conf_rev
  83 csubc/drop csubc_drop_conf_O
  84 csubc/drop drop_csubc_trans
  85 csubc/drop csubc_drop_conf_rev
  86 csubc/fwd csubc_gen_sort_l
  87 csubc/fwd csubc_gen_head_l
  88 csubc/fwd csubc_gen_sort_r
  89 csubc/fwd csubc_gen_head_r
  90 csubc/getl csubc_getl_conf
  91 csubc/props csubc_refl
  92 csubt/clear csubt_clear_conf
  93 csubt/csuba csubt_csuba
  94 csubt/drop csubt_drop_flat
  95 csubt/drop csubt_drop_abbr
  96 csubt/drop csubt_drop_abst
  97 csubt/fwd csubt_gen_abbr
  98 csubt/fwd csubt_gen_abst
  99 csubt/fwd csubt_gen_flat
 100 csubt/fwd csubt_gen_bind
 101 csubt/getl csubt_getl_abbr
 102 csubt/getl csubt_getl_abst
 103 csubt/pc3 csubt_pr2
 104 csubt/pc3 csubt_pc3
 105 csubt/props csubt_refl
 106 csubt/ty3 csubt_ty3
 107 csubt/ty3 csubt_ty3_ld
 108 csubv/clear csubv_clear_conf
 109 csubv/clear csubv_clear_conf_void
 110 csubv/drop csubv_drop_conf
 111 csubv/getl csubv_getl_conf
 112 csubv/getl csubv_getl_conf_void
 113 csubv/props csubv_bind_same
 114 csubv/props csubv_refl
 115 drop1/fwd drop1_gen_pnil
 116 drop1/fwd drop1_gen_pcons
 117 drop1/getl drop1_getl_trans
 118 drop1/props drop1_skip_bind
 119 drop1/props drop1_cons_tail
 120 drop1/props drop1_trans
 121 drop/props drop_ctail
 122 ex0/props aplus_gz_le
 123 ex0/props aplus_gz_ge
 124 ex0/props next_plus_gz
 125 ex0/props leqz_leq
 126 ex0/props leq_leqz
 127 ex1/props ex1__leq_sort_SS
 128 ex1/props ex1_arity
 129 ex1/props ex1_ty3
 130 ex2/props ex2_nf2
 131 ex2/props ex2_arity
 132 fsubst0/fwd fsubst0_gen_base
 133 leq/asucc asucc_repl
 134 leq/asucc asucc_inj
 135 leq/asucc leq_asucc
 136 leq/asucc leq_ahead_asucc_false
 137 leq/asucc leq_asucc_false
 138 leq/fwd leq_gen_sort1
 139 leq/fwd leq_gen_head1
 140 leq/fwd leq_gen_sort2
 141 leq/fwd leq_gen_head2
 142 leq/props ahead_inj_snd
 143 leq/props leq_refl
 144 leq/props leq_eq
 145 leq/props leq_sym
 146 leq/props leq_trans
 147 leq/props leq_ahead_false_1
 148 leq/props leq_ahead_false_2
 149 lift1/fwd lift1_sort
 150 lift1/fwd lift1_lref
 151 lift1/fwd lift1_bind
 152 lift1/fwd lift1_flat
 153 lift1/fwd lift1_cons_tail
 154 lift1/fwd lifts1_flat
 155 lift1/fwd lifts1_nil
 156 lift1/fwd lifts1_cons
 157 lift1/props lift1_lift1
 158 lift1/props lift1_xhg
 159 lift1/props lifts1_xhg
 160 lift1/props lift1_free
 161 lift/props thead_x_lift_y_y
 162 lift/props lifts_tapp
 163 lift/props lifts_inj
 164 llt/props lweight_repl
 165 llt/props llt_repl
 166 llt/props llt_trans
 167 llt/props llt_head_sx
 168 llt/props llt_head_dx
 169 llt/props llt_wf__q_ind
 170 llt/props llt_wf_ind
 171 next_plus/props next_plus_assoc
 172 next_plus/props next_plus_next
 173 next_plus/props next_plus_lt
 174 nf2/arity arity_nf2_inv_all
 175 nf2/dec nf2_dec
 176 nf2/fwd nf2_gen_lref
 177 nf2/fwd nf2_gen_abst
 178 nf2/fwd nf2_gen_cast
 179 nf2/fwd nf2_gen_beta
 180 nf2/fwd nf2_gen_flat
 181 nf2/fwd nf2_gen__nf2_gen_aux
 182 nf2/fwd nf2_gen_abbr
 183 nf2/fwd nf2_gen_void
 184 nf2/iso nf2_iso_appls_lref
 185 nf2/lift1 nf2_lift1
 186 nf2/pr3 nf2_pr3_unfold
 187 nf2/pr3 nf2_pr3_confluence
 188 nf2/props nf2_sort
 189 nf2/props nf2_csort_lref
 190 nf2/props nf2_abst
 191 nf2/props nf2_abst_shift
 192 nf2/props nfs2_tapp
 193 nf2/props nf2_appls_lref
 194 nf2/props nf2_appl_lref
 195 nf2/props nf2_lref_abst
 196 nf2/props nf2_lift
 197 pc1/props pc1_pr0_r
 198 pc1/props pc1_pr0_x
 199 pc1/props pc1_refl
 200 pc1/props pc1_pr0_u
 201 pc1/props pc1_s
 202 pc1/props pc1_head_1
 203 pc1/props pc1_head_2
 204 pc1/props pc1_t
 205 pc1/props pc1_pr0_u2
 206 pc1/props pc1_head
 207 pc3/dec pc3_dec
 208 pc3/dec pc3_abst_dec
 209 pc3/fsubst0 pc3_pr2_fsubst0
 210 pc3/fsubst0 pc3_pr2_fsubst0_back
 211 pc3/fsubst0 pc3_fsubst0
 212 pc3/fwd pc3_gen_sort
 213 pc3/fwd pc3_gen_abst
 214 pc3/fwd pc3_gen_abst_shift
 215 pc3/fwd pc3_gen_lift
 216 pc3/fwd pc3_gen_not_abst
 217 pc3/fwd pc3_gen_lift_abst
 218 pc3/fwd pc3_gen_sort_abst
 219 pc3/left pc3_ind_left__pc3_left_pr3
 220 pc3/left pc3_ind_left__pc3_left_trans
 221 pc3/left pc3_ind_left__pc3_left_sym
 222 pc3/left pc3_ind_left__pc3_left_pc3
 223 pc3/left pc3_ind_left__pc3_pc3_left
 224 pc3/left pc3_ind_left
 225 pc3/nf2 pc3_nf2
 226 pc3/nf2 pc3_nf2_unfold
 227 pc3/pc1 pc3_pc1
 228 pc3/props clear_pc3_trans
 229 pc3/props pc3_pr2_r
 230 pc3/props pc3_pr2_x
 231 pc3/props pc3_pr3_r
 232 pc3/props pc3_pr3_x
 233 pc3/props pc3_pr3_t
 234 pc3/props pc3_refl
 235 pc3/props pc3_s
 236 pc3/props pc3_thin_dx
 237 pc3/props pc3_head_1
 238 pc3/props pc3_head_2
 239 pc3/props pc3_pr2_u
 240 pc3/props pc3_t
 241 pc3/props pc3_pr2_u2
 242 pc3/props pc3_pr3_conf
 243 pc3/props pc3_head_12
 244 pc3/props pc3_head_21
 245 pc3/props pc3_pr0_pr2_t
 246 pc3/props pc3_pr2_pr2_t
 247 pc3/props pc3_pr2_pr3_t
 248 pc3/props pc3_pr3_pc3_t
 249 pc3/props pc3_lift
 250 pc3/props pc3_eta
 251 pc3/subst1 pc3_gen_cabbr
 252 pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
 253 pc3/wcpr0 pc3_wcpr0_t
 254 pc3/wcpr0 pc3_wcpr0
 255 pr0/fwd pr0_gen_void
 256 pr0/dec nf0_dec
 257 pr0/subst1 pr0_subst1_back
 258 pr0/subst1 pr0_subst1_fwd
 259 pr1/pr1 pr1_strip
 260 pr1/pr1 pr1_confluence
 261 pr1/props pr1_pr0
 262 pr1/props pr1_t
 263 pr1/props pr1_head_1
 264 pr1/props pr1_head_2
 265 pr1/props pr1_comp
 266 pr1/props pr1_eta
 267 pr2/clen pr2_gen_ctail
 268
 269 # check ######################################################################
 270
 271 pr2/clen pr2_gen_cbind
 272 pr2/clen pr2_gen_cflat
 273 pr2/fwd pr2_gen_sort
 274 pr2/fwd pr2_gen_lref
 275 pr2/fwd pr2_gen_abst
 276 pr2/fwd pr2_gen_cast
 277 pr2/fwd pr2_gen_csort
 278 pr2/fwd pr2_gen_appl
 279 pr2/fwd pr2_gen_abbr
 280 pr2/fwd pr2_gen_void
 281 pr2/fwd pr2_gen_lift
 282 pr2/pr2 pr2_confluence__pr2_free_free
 283 pr2/pr2 pr2_confluence__pr2_free_delta
 284 pr2/pr2 pr2_confluence__pr2_delta_delta
 285 pr2/pr2 pr2_confluence
 286 pr2/props pr2_thin_dx
 287 pr2/props pr2_head_1
 288 pr2/props pr2_head_2
 289 pr2/props clear_pr2_trans
 290 pr2/props pr2_cflat
 291 pr2/props pr2_ctail
 292 pr2/props pr2_change
 293 pr2/props pr2_lift
 294 pr2/subst1 pr2_delta1
 295 pr2/subst1 pr2_subst1
 296 pr2/subst1 pr2_gen_cabbr
 297 pr3/fwd pr3_gen_sort
 298 pr3/fwd pr3_gen_abst
 299 pr3/fwd pr3_gen_cast
 300 pr3/fwd pr3_gen_lift
 301 pr3/fwd pr3_gen_lref
 302 pr3/fwd pr3_gen_void
 303 pr3/fwd pr3_gen_abbr
 304 pr3/fwd pr3_gen_appl
 305 pr3/fwd pr3_gen_bind
 306 pr3/iso pr3_iso_appls_abbr
 307 pr3/iso pr3_iso_appls_cast
 308 pr3/iso pr3_iso_appl_bind
 309 pr3/iso pr3_iso_appls_appl_bind
 310 pr3/iso pr3_iso_appls_bind
 311 pr3/iso pr3_iso_beta
 312 pr3/iso pr3_iso_appls_beta
 313 pr3/pr1 pr3_pr1
 314 pr3/pr3 pr3_strip
 315 pr3/pr3 pr3_confluence
 316 pr3/props clear_pr3_trans
 317 pr3/props pr3_pr2
 318 pr3/props pr3_t
 319 pr3/props pr3_thin_dx
 320 pr3/props pr3_head_1
 321 pr3/props pr3_head_2
 322 pr3/props pr3_head_21
 323 pr3/props pr3_head_12
 324 pr3/props pr3_cflat
 325 pr3/props pr3_flat
 326 pr3/props pr3_pr0_pr2_t
 327 pr3/props pr3_pr2_pr2_t
 328 pr3/props pr3_pr2_pr3_t
 329 pr3/props pr3_pr3_pr3_t
 330 pr3/props pr3_lift
 331 pr3/props pr3_eta
 332 pr3/subst1 pr3_subst1
 333 pr3/subst1 pr3_gen_cabbr
 334 pr3/wcpr0 pr3_wcpr0_t
 335 sc3/arity sc3_arity_csubc
 336 sc3/arity sc3_arity
 337 sc3/props sc3_arity_gen
 338 sc3/props sc3_repl
 339 sc3/props sc3_lift
 340 sc3/props sc3_lift1
 341 sc3/props sc3_abbr
 342 sc3/props sc3_cast
 343 sc3/props sc3_props__sc3_sn3_abst
 344 sc3/props sc3_sn3
 345 sc3/props sc3_abst
 346 sc3/props sc3_bind
 347 sc3/props sc3_appl
 348 sn3/fwd sn3_gen_bind
 349 sn3/fwd sn3_gen_flat
 350 sn3/fwd sn3_gen_head
 351 sn3/fwd sn3_gen_cflat
 352 sn3/fwd sn3_gen_lift
 353 sn3/lift1 sns3_lifts1
 354 sn3/nf2 sn3_nf2
 355 sn3/nf2 nf2_sn3
 356 sn3/props sn3_pr3_trans
 357 sn3/props sn3_pr2_intro
 358 sn3/props sn3_cast
 359 sn3/props sn3_cflat
 360 sn3/props sn3_shift
 361 sn3/props sn3_change
 362 sn3/props sn3_gen_def
 363 sn3/props sn3_cdelta
 364 sn3/props sn3_cpr3_trans
 365 sn3/props sn3_bind
 366 sn3/props sn3_beta
 367 sn3/props sn3_appl_lref
 368 sn3/props sn3_appl_abbr
 369 sn3/props sn3_appl_cast
 370 sn3/props sn3_appl_bind
 371 sn3/props sn3_appl_appl
 372 sn3/props sn3_appl_beta
 373 sn3/props sn3_appl_appls
 374 sn3/props sn3_appls_lref
 375 sn3/props sn3_appls_cast
 376 sn3/props sn3_appls_bind
 377 sn3/props sn3_appls_beta
 378 sn3/props sn3_lift
 379 sn3/props sn3_abbr
 380 sn3/props sn3_appls_abbr
 381 sn3/props sns3_lifts
 382 sty0/fwd sty0_gen_sort
 383 sty0/fwd sty0_gen_lref
 384 sty0/fwd sty0_gen_bind
 385 sty0/fwd sty0_gen_appl
 386 sty0/fwd sty0_gen_cast
 387 sty0/props sty0_lift
 388 sty0/props sty0_correct
 389 sty1/cnt sty1_cnt
 390 sty1/props sty1_trans
 391 sty1/props sty1_bind
 392 sty1/props sty1_appl
 393 sty1/props sty1_lift
 394 sty1/props sty1_correct
 395 sty1/props sty1_abbr
 396 sty1/props sty1_cast2
 397 subst0/dec dnf_dec2
 398 subst0/dec dnf_dec
 399 subst1/fwd subst1_gen_lift_ge
 400 subst1/fwd subst1_gen_lift_lt
 401 subst1/fwd subst1_gen_lift_eq
 402 subst1/props subst1_lift_ge
 403 subst1/props subst1_lift_lt
 404 subst1/props subst1_ex
 405 subst1/props subst1_lift_S
 406 subst1/subst1 subst1_subst1
 407 subst1/subst1 subst1_subst1_back
 408 subst1/subst1 subst1_trans
 409 subst1/subst1 subst1_confluence_lift
 410 subst/fwd subst_sort
 411 subst/fwd subst_lref_lt
 412 subst/fwd subst_lref_eq
 413 subst/fwd subst_lref_gt
 414 subst/fwd subst_head
 415 subst/props subst_lift_SO
 416 subst/props subst_subst0
 417 T/dec terms_props__bind_dec
 418 T/dec bind_dec_not
 419 T/dec terms_props__flat_dec
 420 T/dec terms_props__kind_dec
 421 T/dec term_dec
 422 T/dec binder_dec
 423 T/dec abst_dec
 424 tlist/props tslt_wf__q_ind
 425 tlist/props tslt_wf_ind
 426 tlist/props theads_tapp
 427 tlist/props tcons_tapp_ex
 428 tlist/props tlist_ind_rev
 429 T/props not_abbr_abst
 430 T/props not_void_abst
 431 T/props not_abbr_void
 432 T/props not_abst_void
 433 T/props thead_x_y_y
 434 T/props tweight_lt
 435 ty3/arity ty3_arity
 436 ty3/arity_props ty3_predicative
 437 ty3/arity_props ty3_repellent
 438 ty3/arity_props ty3_acyclic
 439 ty3/arity_props ty3_sn3
 440 ty3/dec ty3_inference
 441 ty3/fsubst0 ty3_fsubst0
 442 ty3/fsubst0 ty3_csubst0
 443 ty3/fsubst0 ty3_subst0
 444 ty3/fwd ty3_gen_sort
 445 ty3/fwd ty3_gen_lref
 446 ty3/fwd ty3_gen_bind
 447 ty3/fwd ty3_gen_appl
 448 ty3/fwd ty3_gen_cast
 449 ty3/fwd tys3_gen_nil
 450 ty3/fwd tys3_gen_cons
 451 ty3/fwd_nf2 ty3_gen_appl_nf2
 452 ty3/fwd_nf2 ty3_inv_lref_nf2_pc3
 453 ty3/fwd_nf2 ty3_inv_lref_nf2
 454 ty3/fwd_nf2 ty3_inv_appls_lref_nf2
 455 ty3/fwd_nf2 ty3_inv_lref_lref_nf2
 456 ty3/nf2 ty3_nf2_inv_abst_premise_csort
 457 ty3/nf2 ty3_nf2_inv_all
 458 ty3/nf2 ty3_nf2_inv_sort
 459 ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux
 460 ty3/nf2 ty3_nf2_inv_abst
 461 ty3/pr3 ty3_sred_wcpr0_pr0
 462 ty3/pr3 ty3_sred_pr0
 463 ty3/pr3 ty3_sred_pr1
 464 ty3/pr3 ty3_sred_pr2
 465 ty3/pr3 ty3_sred_pr3
 466 ty3/pr3_props ty3_cred_pr2
 467 ty3/pr3_props ty3_cred_pr3
 468 ty3/pr3_props ty3_gen_lift
 469 ty3/pr3_props ty3_tred
 470 ty3/pr3_props ty3_sconv_pc3
 471 ty3/pr3_props ty3_sred_back
 472 ty3/pr3_props ty3_sconv
 473 ty3/props ty3_lift
 474 ty3/props ty3_correct
 475 ty3/props ty3_unique
 476 ty3/props ty3_gen_abst_abst
 477 ty3/props ty3_typecheck
 478 ty3/props ty3_getl_subst0
 479 ty3/sty0 ty3_sty0
 480 ty3/subst1 ty3_gen_cabbr
 481 ty3/subst1 ty3_gen_cvoid
 482 wf3/clear wf3_clear_conf
 483 wf3/clear clear_wf3_trans
 484 wf3/fwd wf3_gen_sort1
 485 wf3/fwd wf3_gen_bind1
 486 wf3/fwd wf3_gen_flat1
 487 wf3/fwd wf3_gen_head2
 488 wf3/getl wf3_getl_conf
 489 wf3/getl getl_wf3_trans
 490 wf3/props wf3_mono
 491 wf3/props wf3_total
 492 wf3/props ty3_shift1
 493 wf3/props wf3_idem
 494 wf3/props wf3_ty3
 495 wf3/ty3 wf3_pr2_conf
 496 wf3/ty3 wf3_pr3_conf
 497 wf3/ty3 wf3_pc3_conf
 498 wf3/ty3 wf3_ty3_conf