matita/matita/contribs/lambdadelta/static_2/names.txt

   1 "aaa"
   2 "aaa_aaa_inv_appl"
   3 "aaa_aaa_inv_cast"
   4 "aaa_abbr"
   5 "aaa_abst"
   6 "aaa_appl"
   7 "aaa_cast"
   8 "aaa_dec"
   9 "aaa_feqx_conf"
  10 "aaa_fqu_conf"
  11 "aaa_fqup_conf"
  12 "aaa_fquq_conf"
  13 "aaa_fqus_conf"
  14 "aaa_inv_abbr"
  15 "aaa_inv_abbr_aux"
  16 "aaa_inv_abst"
  17 "aaa_inv_abst_aux"
  18 "aaa_inv_appl"
  19 "aaa_inv_appl_aux"
  20 "aaa_inv_cast"
  21 "aaa_inv_cast_aux"
  22 "aaa_inv_gref"
  23 "aaa_inv_gref_aux"
  24 "aaa_inv_lifts"
  25 "aaa_inv_lref"
  26 "aaa_inv_lref_aux"
  27 "aaa_inv_lref_drops"
  28 "aaa_inv_sort"
  29 "aaa_inv_sort_aux"
  30 "aaa_inv_zero"
  31 "aaa_inv_zero_aux"
  32 "aaa_lifts"
  33 "aaa_lref"
  34 "aaa_lref_drops"
  35 "aaa_mono"
  36 "aaa_pair_inv_lref"
  37 "aaa_sort"
  38 "aaa_teqx_conf_reqx"
  39 "aaa_zero"
  40 "aarity"
  41 "AAtom"
  42 "Abbr"
  43 "Abst"
  44 "abst_dec"
  45 "ac"
  46 "ac_eq"
  47 "ac_eq_props"
  48 "ac_le"
  49 "acle"
  50 "acle_eq_le"
  51 "acle_eq_monotonic_le"
  52 "acle_le_eq"
  53 "acle_le_monotonic_le"
  54 "acle_omega"
  55 "acle_one"
  56 "ac_le_props"
  57 "acle_refl"
  58 "acle_trans"
  59 "ac_props"
  60 "acr"
  61 "acr_aaa"
  62 "acr_aaa_csubc_lifts"
  63 "acr_abst"
  64 "acr_gcr"
  65 "acr_lifts"
  66 "ac_top"
  67 "ac_top_props"
  68 "APair"
  69 "append"
  70 "append_assoc"
  71 "append_atom"
  72 "append_atom_sn"
  73 "append_bind"
  74 "append_inj_dx"
  75 "append_inj_length_dx"
  76 "append_inj_length_sn"
  77 "append_inj_sn"
  78 "append_inv_atom3_sn"
  79 "append_inv_bind3_sn"
  80 "append_inv_pair_dx"
  81 "append_inv_refl_dx"
  82 "append_length"
  83 "append_shift"
  84 "Appl"
  85 "applv"
  86 "applv_cons"
  87 "applv_nil"
  88 "applv_simple"
  89 "apply_top"
  90 "bind"
  91 "bind1"
  92 "bind2"
  93 "Bind2"
  94 "BPair"
  95 "BUnit"
  96 "bw"
  97 "bw_pos"
  98 "candidate"
  99 "Cast"
 100 "cdeq"
 101 "cdeq_ext"
 102 "ceq"
 103 "ceq_ext"
 104 "ceq_ext_inv_eq"
 105 "ceq_ext_refl"
 106 "ceq_ext_trans"
 107 "ceq_inv_lift_sn"
 108 "ceq_lift_sn"
 109 "cext2"
 110 "cext2_co"
 111 "cext2_d_liftable2_sn"
 112 "cext2_sym"
 113 "cfull"
 114 "cfull_dec"
 115 "cfull_lift_sn"
 116 "cfun"
 117 "co_dedropable_sn"
 118 "co_dedropable_sn_CTC"
 119 "co_dedropable_sn_ltc"
 120 "co_dropable_dx"
 121 "co_dropable_dx_CTC"
 122 "co_dropable_dx_ltc"
 123 "co_dropable_sn"
 124 "co_dropable_sn_CTC"
 125 "co_dropable_sn_ltc"
 126 "CP0"
 127 "CP1"
 128 "CP2"
 129 "CP3"
 130 "d1_liftable_liftable_all"
 131 "d2_deliftable_sn_CTC"
 132 "d2_deliftable_sn_ltc"
 133 "d2_liftable_sn_CTC"
 134 "d2_liftable_sn_ltc"
 135 "d_appendable_sn"
 136 "d_deliftable1"
 137 "d_deliftable1_isuni"
 138 "d_deliftable2_bi"
 139 "d_deliftable2_sn"
 140 "d_deliftable2_sn_bi"
 141 "dedropable_sn"
 142 "dedropable_sn_CTC"
 143 "deg_inv_prec"
 144 "deg_inv_pred"
 145 "deg_iter"
 146 "deg_next_SO"
 147 "deg_O"
 148 "deg_SO"
 149 "deg_SO_gt"
 150 "deg_SO_inv_succ"
 151 "deg_SO_inv_succ_aux"
 152 "deg_SO_refl"
 153 "deg_SO_succ"
 154 "deg_SO_zero"
 155 "deliftable2_bi"
 156 "deliftable2_dx"
 157 "deliftable2_sn"
 158 "deliftable2_sn_bi"
 159 "deliftable2_sn_dx"
 160 "destruct_apair_apair_aux"
 161 "destruct_lbind_lbind_aux"
 162 "destruct_sort_sort_aux"
 163 "destruct_tatom_tatom_aux"
 164 "destruct_tpair_tpair_aux"
 165 "discr_apair_xy_x"
 166 "discr_apair_xy_y"
 167 "discr_lbind_x_xy"
 168 "discr_lbind_xy_x"
 169 "discr_tpair_xy_x"
 170 "discr_tpair_xy_y"
 171 "d_liftable1"
 172 "d_liftable1_all"
 173 "d_liftable1_isuni"
 174 "d_liftable2_bi"
 175 "d_liftable2_sn"
 176 "d_liftable2_sn_bi"
 177 "dropable_dx"
 178 "dropable_dx_CTC"
 179 "dropable_sn"
 180 "dropable_sn_CTC"
 181 "drops"
 182 "drops_after_fwd_drop2"
 183 "drops_atom"
 184 "drops_atom2_sex_conf"
 185 "drops_atom_F"
 186 "drops_bind2_fwd_rfw"
 187 "drops_conf"
 188 "drops_conf_div"
 189 "drops_conf_div_bind_isuni"
 190 "drops_conf_div_fcla"
 191 "drops_conf_div_isuni"
 192 "drops_conf_skip1"
 193 "drops_drop"
 194 "drops_eq_repl_back"
 195 "drops_eq_repl_fwd"
 196 "drops_F"
 197 "drops_fcla_fwd"
 198 "drops_fcla_fwd_le2"
 199 "drops_fcla_fwd_lt2"
 200 "drops_fcla_fwd_lt4"
 201 "drops_F_uni"
 202 "drops_fwd_drop2"
 203 "drops_fwd_drop2_aux"
 204 "drops_fwd_fcla"
 205 "drops_fwd_fcla_le2"
 206 "drops_fwd_fcla_lt2"
 207 "drops_fwd_isfin"
 208 "drops_fwd_isid"
 209 "drops_fwd_length_eq1"
 210 "drops_fwd_length_eq2"
 211 "drops_fwd_length_le4"
 212 "drops_fwd_lw"
 213 "drops_fwd_lw_lt"
 214 "drops_gen"
 215 "drops_inv_atom1"
 216 "drops_inv_atom1_aux"
 217 "drops_inv_atom2"
 218 "drops_inv_bind1_isuni"
 219 "drops_inv_bind2_isuni"
 220 "drops_inv_bind2_isuni_next"
 221 "drops_inv_drop1"
 222 "drops_inv_drop1_aux"
 223 "drops_inv_F"
 224 "drops_inv_gen"
 225 "drops_inv_isuni"
 226 "drops_inv_length_eq"
 227 "drops_inv_skip1"
 228 "drops_inv_skip1_aux"
 229 "drops_inv_skip2"
 230 "drops_inv_skip2_aux"
 231 "drops_inv_succ"
 232 "drops_inv_TF"
 233 "drops_inv_TF_aux"
 234 "drops_inv_uni"
 235 "drops_inv_x_bind_xy"
 236 "drops_isuni_ex"
 237 "drops_isuni_fwd_drop2"
 238 "drops_ldec_dec"
 239 "drops_lsubc_trans"
 240 "drops_mono"
 241 "drops_refl"
 242 "drops_seq_trans_next"
 243 "drops_sex_trans_next"
 244 "drops_sex_trans_push"
 245 "drops_skip"
 246 "drops_split_div"
 247 "drops_split_trans"
 248 "drops_split_trans_bind2"
 249 "drops_TF"
 250 "drops_tls_at"
 251 "drops_trans"
 252 "drops_trans_skip2"
 253 "eq_aarity_dec"
 254 "eq_bind1_dec"
 255 "eq_bind2_dec"
 256 "eq_bind_dec"
 257 "eq_false_inv_tpair_dx"
 258 "eq_false_inv_tpair_sn"
 259 "eq_flat2_dec"
 260 "eq_genv_dec"
 261 "eq_item0_dec"
 262 "eq_item2_dec"
 263 "eq_lenv_dec"
 264 "eq_term_dec"
 265 "ext2"
 266 "ext2_dec"
 267 "ext2_inv_pair"
 268 "ext2_inv_pair_dx"
 269 "ext2_inv_pair_dx_aux"
 270 "ext2_inv_pair_sn"
 271 "ext2_inv_pair_sn_aux"
 272 "ext2_inv_tc"
 273 "ext2_inv_unit"
 274 "ext2_inv_unit_dx"
 275 "ext2_inv_unit_dx_aux"
 276 "ext2_inv_unit_sn"
 277 "ext2_inv_unit_sn_aux"
 278 "ext2_pair"
 279 "ext2_refl"
 280 "ext2_sym"
 281 "ext2_tc"
 282 "ext2_tc_inj"
 283 "ext2_tc_pair"
 284 "ext2_tc_step"
 285 "ext2_trans"
 286 "ext2_unit"
 287 "f_dedropable_sn"
 288 "f_dropable_dx"
 289 "f_dropable_sn"
 290 "feqx"
 291 "feqx_canc_dx"
 292 "feqx_canc_sn"
 293 "feqx_fqus_trans"
 294 "feqx_intro_dx"
 295 "feqx_intro_sn"
 296 "feqx_inv_gen_dx"
 297 "feqx_inv_gen_sn"
 298 "feqx_refl"
 299 "feqx_sym"
 300 "feqx_tneqx_repl_dx"
 301 "feqx_trans"
 302 "flat2"
 303 "Flat2"
 304 "fold"
 305 "fold_atom"
 306 "fold_pair"
 307 "fold_unit"
 308 "fqu"
 309 "fqu_bind_dx"
 310 "fqu_clear"
 311 "fqu_drop"
 312 "fqu_flat_dx"
 313 "fqu_fqup"
 314 "fqu_fquq"
 315 "fqu_fwd_fw"
 316 "fqu_fwd_length_lref1"
 317 "fqu_fwd_length_lref1_aux"
 318 "fqu_gref"
 319 "fqu_inv_atom1"
 320 "fqu_inv_bind1"
 321 "fqu_inv_bind1_aux"
 322 "fqu_inv_bind1_true"
 323 "fqu_inv_flat1"
 324 "fqu_inv_flat1_aux"
 325 "fqu_inv_gref1"
 326 "fqu_inv_gref1_aux"
 327 "fqu_inv_gref1_bind"
 328 "fqu_inv_lref1"
 329 "fqu_inv_lref1_aux"
 330 "fqu_inv_lref1_bind"
 331 "fqu_inv_sort1"
 332 "fqu_inv_sort1_aux"
 333 "fqu_inv_sort1_bind"
 334 "fqu_inv_teqx"
 335 "fqu_inv_teqx_aux"
 336 "fqu_inv_zero1_pair"
 337 "fqu_lref_O"
 338 "fqu_lref_S"
 339 "fqup"
 340 "fqu_pair_sn"
 341 "fqup_bind_dx"
 342 "fqup_bind_dx_flat_dx"
 343 "fqup_clear"
 344 "fqup_drops_strap1"
 345 "fqup_drops_succ"
 346 "fqup_flat_dx"
 347 "fqup_flat_dx_bind_dx"
 348 "fqup_flat_dx_pair_sn"
 349 "fqup_fqus"
 350 "fqup_fqus_trans"
 351 "fqup_fwd_fw"
 352 "fqup_ind"
 353 "fqup_ind_dx"
 354 "fqup_inv_step_sn"
 355 "fqup_lref"
 356 "fqup_pair_sn"
 357 "fqup_strap1"
 358 "fqup_strap2"
 359 "fqup_trans"
 360 "fqup_wf_ind"
 361 "fqup_wf_ind_eq"
 362 "fqup_zeta"
 363 "fquq"
 364 "fquq_fqus"
 365 "fquq_fwd_fw"
 366 "fquq_fwd_length_lref1"
 367 "fquq_refl"
 368 "fqus"
 369 "fqus_drops"
 370 "fqus_fqup_trans"
 371 "fqus_fwd_fw"
 372 "fqus_ind"
 373 "fqus_ind_dx"
 374 "fqus_inv_atom1"
 375 "fqus_inv_bind1"
 376 "fqus_inv_bind1_true"
 377 "fqus_inv_flat1"
 378 "fqus_inv_fqup"
 379 "fqus_inv_fqu_sn"
 380 "fqus_inv_gref1"
 381 "fqus_inv_gref1_bind"
 382 "fqus_inv_lref1"
 383 "fqus_inv_lref1_bind"
 384 "fqus_inv_refl_atom3"
 385 "fqus_inv_sort1"
 386 "fqus_inv_sort1_bind"
 387 "fqus_inv_zero1_pair"
 388 "fqu_sort"
 389 "fqus_refl"
 390 "fqus_strap1"
 391 "fqus_strap1_fqu"
 392 "fqus_strap2"
 393 "fqus_strap2_fqu"
 394 "fqus_trans"
 395 "fqu_teqx_conf"
 396 "fqu_wf_ind"
 397 "frees"
 398 "frees_append_void"
 399 "frees_atom"
 400 "frees_atom_drops"
 401 "frees_bind"
 402 "frees_bind_void"
 403 "frees_eq_repl_back"
 404 "frees_eq_repl_fwd"
 405 "frees_flat"
 406 "frees_fwd_coafter"
 407 "frees_fwd_isfin"
 408 "frees_gref"
 409 "frees_ind_void"
 410 "frees_inv_append_void"
 411 "frees_inv_append_void_aux"
 412 "frees_inv_atom"
 413 "frees_inv_atom_aux"
 414 "frees_inv_bind"
 415 "frees_inv_bind_aux"
 416 "frees_inv_bind_void"
 417 "frees_inv_drops_next"
 418 "frees_inv_flat"
 419 "frees_inv_flat_aux"
 420 "frees_inv_gref"
 421 "frees_inv_gref_aux"
 422 "frees_inv_lifts"
 423 "frees_inv_lifts_ex"
 424 "frees_inv_lifts_SO"
 425 "frees_inv_lref"
 426 "frees_inv_lref_aux"
 427 "frees_inv_lref_drops"
 428 "frees_inv_pair"
 429 "frees_inv_pair_aux"
 430 "frees_inv_sort"
 431 "frees_inv_sort_aux"
 432 "frees_inv_unit"
 433 "frees_inv_unit_aux"
 434 "frees_lifts"
 435 "frees_lifts_SO"
 436 "frees_lref"
 437 "frees_lref_push"
 438 "frees_lref_pushs"
 439 "frees_mono"
 440 "frees_pair"
 441 "frees_pair_drops"
 442 "frees_req_conf"
 443 "frees_reqx_conf"
 444 "frees_sex_conf"
 445 "frees_sort"
 446 "frees_teqx_conf"
 447 "frees_teqx_conf_reqx"
 448 "frees_total"
 449 "frees_unit"
 450 "frees_unit_drops"
 451 "fsge_rex_trans"
 452 "fsle"
 453 "fsle_bind"
 454 "fsle_bind_dx_dx"
 455 "fsle_bind_dx_sn"
 456 "fsle_bind_eq"
 457 "fsle_bind_sn_ge"
 458 "fsle_flat"
 459 "fsle_flat_dx_dx"
 460 "fsle_flat_dx_sn"
 461 "fsle_flat_sn"
 462 "fsle_frees_trans"
 463 "fsle_frees_trans_eq"
 464 "fsle_fwd_pair_sn"
 465 "fsle_gref"
 466 "fsle_gref_bi"
 467 "fsle_inv_frees_eq"
 468 "fsle_inv_lifts_sn"
 469 "fsle_lifts_dx"
 470 "fsle_lifts_sn"
 471 "fsle_lifts_SO"
 472 "fsle_lifts_SO_sn"
 473 "fsle_pair_bi"
 474 "fsle_refl"
 475 "fsle_shift"
 476 "fsle_sort"
 477 "fsle_sort_bi"
 478 "fsle_trans_dx"
 479 "fsle_trans_rc"
 480 "fsle_trans_sn"
 481 "fsle_unit_bi"
 482 "f_transitive_next"
 483 "fw"
 484 "fw_clear"
 485 "fw_lpair_sn"
 486 "fw_shift"
 487 "fw_tpair_dx"
 488 "fw_tpair_sn"
 489 "GAtom"
 490 "gcp"
 491 "gcp2_all"
 492 "gcr"
 493 "gcr_aaa"
 494 "genv"
 495 "glength"
 496 "GPair"
 497 "GRef"
 498 "gw"
 499 "gw_pair"
 500 "is_apear_dec"
 501 "is_lifts_dec"
 502 "item0"
 503 "item2"
 504 "LAtom"
 505 "LBind"
 506 "length"
 507 "length_atom"
 508 "length_bind"
 509 "length_inv_succ_dx"
 510 "length_inv_succ_dx_ltail"
 511 "length_inv_succ_sn"
 512 "length_inv_succ_sn_ltail"
 513 "length_inv_zero_dx"
 514 "length_inv_zero_sn"
 515 "lenv"
 516 "lenv_case_tail"
 517 "lenv_ind_tail"
 518 "lex"
 519 "lex_atom"
 520 "lex_bind"
 521 "lex_bind_refl_dx"
 522 "lex_co"
 523 "lex_conf"
 524 "lex_confluent"
 525 "lex_CTC"
 526 "lex_CTC_ind_dx"
 527 "lex_CTC_ind_sn"
 528 "lex_CTC_inj"
 529 "lex_CTC_step_dx"
 530 "lex_CTC_step_sn"
 531 "lex_dropable_dx"
 532 "lex_dropable_sn"
 533 "lex_drops_conf_pair"
 534 "lex_drops_trans_pair"
 535 "lex_fwd_length"
 536 "lex_ind"
 537 "lex_inv_atom_dx"
 538 "lex_inv_atom_sn"
 539 "lex_inv_bind_dx"
 540 "lex_inv_bind_sn"
 541 "lex_inv_CTC"
 542 "lex_inv_pair"
 543 "lex_inv_pair_dx"
 544 "lex_inv_pair_sn"
 545 "lex_inv_unit_dx"
 546 "lex_inv_unit_sn"
 547 "lex_liftable_dedropable_sn"
 548 "lex_pair"
 549 "lex_refl"
 550 "lex_trans"
 551 "lex_transitive"
 552 "lex_unit"
 553 "liftable2_bi"
 554 "liftable2_dx"
 555 "liftable2_sn"
 556 "liftable2_sn_bi"
 557 "liftable2_sn_dx"
 558 "lifts"
 559 "lifts_applv"
 560 "liftsb"
 561 "liftsb_conf"
 562 "liftsb_div3"
 563 "liftsb_eq_repl_back"
 564 "liftsb_fwd_bw"
 565 "liftsb_fwd_isid"
 566 "lifts_bind"
 567 "liftsb_inj"
 568 "liftsb_inv_pair_dx"
 569 "liftsb_inv_pair_sn"
 570 "liftsb_inv_unit_dx"
 571 "liftsb_inv_unit_sn"
 572 "liftsb_mono"
 573 "liftsb_refl"
 574 "liftsb_split_trans"
 575 "liftsb_total"
 576 "liftsb_trans"
 577 "lifts_conf"
 578 "lifts_div3"
 579 "lifts_div4"
 580 "lifts_div4_one"
 581 "lifts_eq_repl_back"
 582 "lifts_eq_repl_fwd"
 583 "lifts_flat"
 584 "lifts_fwd_isid"
 585 "lifts_fwd_pair1"
 586 "lifts_fwd_pair2"
 587 "lifts_fwd_tw"
 588 "lifts_gref"
 589 "lifts_inj"
 590 "lifts_inv_applv1"
 591 "lifts_inv_applv2"
 592 "lifts_inv_atom1"
 593 "lifts_inv_atom2"
 594 "lifts_inv_bind1"
 595 "lifts_inv_bind1_aux"
 596 "lifts_inv_bind2"
 597 "lifts_inv_bind2_aux"
 598 "lifts_inv_flat1"
 599 "lifts_inv_flat1_aux"
 600 "lifts_inv_flat2"
 601 "lifts_inv_flat2_aux"
 602 "lifts_inv_gref1"
 603 "lifts_inv_gref1_aux"
 604 "lifts_inv_gref2"
 605 "lifts_inv_gref2_aux"
 606 "lifts_inv_lref1"
 607 "lifts_inv_lref1_aux"
 608 "lifts_inv_lref1_uni"
 609 "lifts_inv_lref2"
 610 "lifts_inv_lref2_aux"
 611 "lifts_inv_lref2_uni"
 612 "lifts_inv_lref2_uni_ge"
 613 "lifts_inv_lref2_uni_lt"
 614 "lifts_inv_pair_xy_x"
 615 "lifts_inv_pair_xy_y"
 616 "lifts_inv_push_succ_sn"
 617 "lifts_inv_push_zero_sn"
 618 "lifts_inv_sort1"
 619 "lifts_inv_sort1_aux"
 620 "lifts_inv_sort2"
 621 "lifts_inv_sort2_aux"
 622 "lifts_lref"
 623 "lifts_lref_ge"
 624 "lifts_lref_ge_minus"
 625 "lifts_lref_lt"
 626 "lifts_lref_uni"
 627 "lifts_mono"
 628 "lifts_push_lref"
 629 "lifts_push_zero"
 630 "lifts_refl"
 631 "lifts_simple_dx"
 632 "lifts_simple_sn"
 633 "lifts_sort"
 634 "lifts_split_div"
 635 "lifts_split_trans"
 636 "lifts_total"
 637 "lifts_trans"
 638 "lifts_trans4_one"
 639 "lifts_trans_uni"
 640 "lifts_uni"
 641 "liftsv"
 642 "liftsv_cons"
 643 "liftsv_inj"
 644 "liftsv_inv_cons1"
 645 "liftsv_inv_cons1_aux"
 646 "liftsv_inv_cons2"
 647 "liftsv_inv_cons2_aux"
 648 "liftsv_inv_nil1"
 649 "liftsv_inv_nil1_aux"
 650 "liftsv_inv_nil2"
 651 "liftsv_inv_nil2_aux"
 652 "liftsv_mono"
 653 "liftsv_nil"
 654 "liftsv_split_trans"
 655 "liftsv_total"
 656 "liftsv_trans"
 657 "LRef"
 658 "lsuba"
 659 "lsuba_aaa_conf"
 660 "lsuba_aaa_trans"
 661 "lsuba_atom"
 662 "lsuba_beta"
 663 "lsuba_bind"
 664 "lsuba_drops_conf_isuni"
 665 "lsuba_drops_trans_isuni"
 666 "lsuba_fwd_lsubr"
 667 "lsuba_inv_atom1"
 668 "lsuba_inv_atom1_aux"
 669 "lsuba_inv_atom2"
 670 "lsuba_inv_atom2_aux"
 671 "lsuba_inv_bind1"
 672 "lsuba_inv_bind1_aux"
 673 "lsuba_inv_bind2"
 674 "lsuba_inv_bind2_aux"
 675 "lsuba_lsubc"
 676 "lsuba_refl"
 677 "lsuba_trans"
 678 "lsubc"
 679 "lsubc_atom"
 680 "lsubc_beta"
 681 "lsubc_bind"
 682 "lsubc_drops_trans_isuni"
 683 "lsubc_fwd_lsubr"
 684 "lsubc_inv_atom1"
 685 "lsubc_inv_atom1_aux"
 686 "lsubc_inv_atom2"
 687 "lsubc_inv_atom2_aux"
 688 "lsubc_inv_bind1"
 689 "lsubc_inv_bind1_aux"
 690 "lsubc_inv_bind2"
 691 "lsubc_inv_bind2_aux"
 692 "lsubc_refl"
 693 "lsubf"
 694 "lsubf_atom"
 695 "lsubf_beta"
 696 "lsubf_beta_tl_dx"
 697 "lsubf_bind"
 698 "lsubf_bind_tl_dx"
 699 "lsubf_eq_repl_back1"
 700 "lsubf_eq_repl_back2"
 701 "lsubf_eq_repl_fwd1"
 702 "lsubf_eq_repl_fwd2"
 703 "lsubf_frees_trans"
 704 "lsubf_fwd_bind_tl"
 705 "lsubf_fwd_isid_dx"
 706 "lsubf_fwd_isid_sn"
 707 "lsubf_fwd_lsubr_isdiv"
 708 "lsubf_fwd_sle"
 709 "lsubf_inv_atom"
 710 "lsubf_inv_atom1"
 711 "lsubf_inv_atom1_aux"
 712 "lsubf_inv_atom2"
 713 "lsubf_inv_atom2_aux"
 714 "lsubf_inv_beta_sn"
 715 "lsubf_inv_bind_sn"
 716 "lsubf_inv_pair1"
 717 "lsubf_inv_pair1_aux"
 718 "lsubf_inv_pair2"
 719 "lsubf_inv_pair2_aux"
 720 "lsubf_inv_push1"
 721 "lsubf_inv_push1_aux"
 722 "lsubf_inv_push2"
 723 "lsubf_inv_push2_aux"
 724 "lsubf_inv_push_sn"
 725 "lsubf_inv_refl"
 726 "lsubf_inv_sor_dx"
 727 "lsubf_inv_unit1"
 728 "lsubf_inv_unit1_aux"
 729 "lsubf_inv_unit2"
 730 "lsubf_inv_unit2_aux"
 731 "lsubf_inv_unit_sn"
 732 "lsubf_push"
 733 "lsubf_refl"
 734 "lsubf_refl_eq"
 735 "lsubf_sor"
 736 "lsubf_unit"
 737 "lsubr"
 738 "lsubr_atom"
 739 "lsubr_beta"
 740 "lsubr_bind"
 741 "lsubr_fwd_bind1"
 742 "lsubr_fwd_bind2"
 743 "lsubr_fwd_drops2_abbr"
 744 "lsubr_fwd_drops2_bind"
 745 "lsubr_fwd_length"
 746 "lsubr_inv_abbr2"
 747 "lsubr_inv_abst1"
 748 "lsubr_inv_abst2"
 749 "lsubr_inv_atom1"
 750 "lsubr_inv_atom1_aux"
 751 "lsubr_inv_atom2"
 752 "lsubr_inv_atom2_aux"
 753 "lsubr_inv_bind1"
 754 "lsubr_inv_bind1_aux"
 755 "lsubr_inv_bind2"
 756 "lsubr_inv_bind2_aux"
 757 "lsubr_inv_pair2"
 758 "lsubr_inv_unit1"
 759 "lsubr_inv_unit2"
 760 "lsubr_lsubf"
 761 "lsubr_lsubf_isid"
 762 "lsubr_refl"
 763 "lsubr_trans"
 764 "lsubr_unit"
 765 "ltail_length"
 766 "lveq"
 767 "lveq_atom"
 768 "lveq_bind"
 769 "lveq_fwd_abst_bind_length_le"
 770 "lveq_fwd_bind_abst_length_le"
 771 "lveq_fwd_gen"
 772 "lveq_fwd_length"
 773 "lveq_fwd_length_eq"
 774 "lveq_fwd_length_le_dx"
 775 "lveq_fwd_length_le_sn"
 776 "lveq_fwd_length_minus"
 777 "lveq_fwd_length_plus"
 778 "lveq_fwd_pair_dx"
 779 "lveq_fwd_pair_sn"
 780 "lveq_inj"
 781 "lveq_inj_length"
 782 "lveq_inj_void_dx_le"
 783 "lveq_inj_void_sn_ge"
 784 "lveq_inv_atom_atom"
 785 "lveq_inv_atom_bind"
 786 "lveq_inv_bind"
 787 "lveq_inv_bind_atom"
 788 "lveq_inv_bind_O"
 789 "lveq_inv_pair_pair"
 790 "lveq_inv_succ"
 791 "lveq_inv_succ_aux"
 792 "lveq_inv_succ_dx"
 793 "lveq_inv_succ_sn"
 794 "lveq_inv_succ_sn_aux"
 795 "lveq_inv_void_dx_length"
 796 "lveq_inv_void_sn_length"
 797 "lveq_inv_void_succ_dx"
 798 "lveq_inv_void_succ_sn"
 799 "lveq_inv_zero"
 800 "lveq_inv_zero_aux"
 801 "lveq_length_eq"
 802 "lveq_length_fwd_dx"
 803 "lveq_length_fwd_sn"
 804 "lveq_refl"
 805 "lveq_sym"
 806 "lveq_void_dx"
 807 "lveq_void_sn"
 808 "lw"
 809 "lw_bind"
 810 "mk_ac"
 811 "mk_ac_props"
 812 "mk_gcp"
 813 "mk_gcr"
 814 "mk_sd"
 815 "mk_sd_props"
 816 "mk_sh"
 817 "mk_sh_acyclic"
 818 "mk_sh_decidable"
 819 "mk_sh_lt"
 820 "nexts_le"
 821 "nexts_lt"
 822 "nf"
 823 "R_confluent2_rex"
 824 "req"
 825 "req_feqx_trans"
 826 "req_fsle_comp"
 827 "req_fwd_rex"
 828 "req_inv_bind"
 829 "req_inv_flat"
 830 "req_inv_lifts_bi"
 831 "req_inv_lref_bind_dx"
 832 "req_inv_lref_bind_sn"
 833 "req_inv_zero_pair_dx"
 834 "req_inv_zero_pair_sn"
 835 "req_refl"
 836 "req_reqx"
 837 "req_reqx_trans"
 838 "req_rex_trans"
 839 "req_transitive"
 840 "reqx"
 841 "reqx_atom"
 842 "reqx_bind"
 843 "reqx_bind_repl_dx"
 844 "reqx_bind_void"
 845 "reqx_canc_dx"
 846 "reqx_canc_sn"
 847 "reqx_dec"
 848 "reqx_flat"
 849 "reqx_fqup_trans"
 850 "reqx_fquq_trans"
 851 "reqx_fqus_trans"
 852 "reqx_fqu_trans"
 853 "reqx_fsge_comp"
 854 "reqx_fwd_bind_dx"
 855 "reqx_fwd_bind_dx_void"
 856 "reqx_fwd_dx"
 857 "reqx_fwd_flat_dx"
 858 "reqx_fwd_length"
 859 "reqx_fwd_pair_sn"
 860 "reqx_fwd_zero_pair"
 861 "reqx_gref"
 862 "reqx_gref_length"
 863 "reqx_inv_atom_dx"
 864 "reqx_inv_atom_sn"
 865 "reqx_inv_bind"
 866 "reqx_inv_bind_void"
 867 "reqx_inv_flat"
 868 "reqx_inv_lifts_bi"
 869 "reqx_inv_lifts_dx"
 870 "reqx_inv_lifts_sn"
 871 "reqx_inv_lref"
 872 "reqx_inv_lref_bind_dx"
 873 "reqx_inv_lref_bind_sn"
 874 "reqx_inv_lref_pair_bi"
 875 "reqx_inv_lref_pair_dx"
 876 "reqx_inv_lref_pair_sn"
 877 "reqx_inv_zero"
 878 "reqx_inv_zero_pair_dx"
 879 "reqx_inv_zero_pair_sn"
 880 "reqx_lifts_bi"
 881 "reqx_lifts_sn"
 882 "reqx_lref"
 883 "reqx_pair"
 884 "reqx_pair_refl"
 885 "reqx_refl"
 886 "reqx_repl"
 887 "reqx_rneqx_trans"
 888 "reqx_sort"
 889 "reqx_sort_length"
 890 "reqx_sym"
 891 "reqx_trans"
 892 "reqx_unit"
 893 "reqx_unit_length"
 894 "rex"
 895 "rex_atom"
 896 "rex_bind"
 897 "rex_bind_dx_split"
 898 "rex_bind_dx_split_void"
 899 "rex_bind_repl_dx"
 900 "rex_bind_void"
 901 "rex_co"
 902 "rex_conf"
 903 "rex_confluent"
 904 "rex_dec"
 905 "rex_dropable_dx"
 906 "rex_dropable_sn"
 907 "rex_flat"
 908 "rex_flat_dx_split"
 909 "rex_fsge_compatible"
 910 "rex_fsle_compatible"
 911 "rex_fwd_bind_dx"
 912 "rex_fwd_bind_dx_void"
 913 "rex_fwd_dx"
 914 "rex_fwd_flat_dx"
 915 "rex_fwd_length"
 916 "rex_fwd_pair_sn"
 917 "rex_fwd_zero_pair"
 918 "rex_gref"
 919 "rex_gref_length"
 920 "rex_inv_atom_dx"
 921 "rex_inv_atom_sn"
 922 "rex_inv_bind"
 923 "rex_inv_bind_void"
 924 "rex_inv_flat"
 925 "rex_inv_frees"
 926 "rex_inv_gref"
 927 "rex_inv_gref_bind_dx"
 928 "rex_inv_gref_bind_sn"
 929 "rex_inv_lex_req"
 930 "rex_inv_lifts_bi"
 931 "rex_inv_lref"
 932 "rex_inv_lref_bind_dx"
 933 "rex_inv_lref_bind_sn"
 934 "rex_inv_lref_pair_bi"
 935 "rex_inv_lref_pair_dx"
 936 "rex_inv_lref_pair_sn"
 937 "rex_inv_lref_unit_dx"
 938 "rex_inv_lref_unit_sn"
 939 "rex_inv_sort"
 940 "rex_inv_sort_bind_dx"
 941 "rex_inv_sort_bind_sn"
 942 "rex_inv_zero"
 943 "rex_inv_zero_length"
 944 "rex_inv_zero_pair_dx"
 945 "rex_inv_zero_pair_sn"
 946 "rex_inv_zero_unit_dx"
 947 "rex_inv_zero_unit_sn"
 948 "rex_isid"
 949 "rex_lex"
 950 "rex_liftable_dedropable_sn"
 951 "rex_lifts_bi"
 952 "rex_lref"
 953 "rex_pair"
 954 "rex_pair_refl"
 955 "rex_pair_sn_split"
 956 "rex_refl"
 957 "rexs"
 958 "rexs_atom"
 959 "rexs_co"
 960 "rexs_fwd_bind_dx"
 961 "rexs_fwd_bind_dx_void"
 962 "rexs_fwd_flat_dx"
 963 "rexs_fwd_length"
 964 "rexs_fwd_pair_sn"
 965 "rexs_gref"
 966 "rexs_ind_dx"
 967 "rexs_ind_sn"
 968 "rexs_inv_atom_dx"
 969 "rexs_inv_atom_sn"
 970 "rexs_inv_bind"
 971 "rexs_inv_bind_void"
 972 "rexs_inv_flat"
 973 "rexs_inv_gref"
 974 "rexs_inv_gref_bind_dx"
 975 "rexs_inv_gref_bind_sn"
 976 "rexs_inv_lex_req"
 977 "rexs_inv_sort"
 978 "rexs_inv_sort_bind_dx"
 979 "rexs_inv_sort_bind_sn"
 980 "rexs_lex"
 981 "rexs_lex_req"
 982 "rexs_lref"
 983 "rex_sort"
 984 "rex_sort_length"
 985 "rexs_pair"
 986 "rexs_pair_refl"
 987 "rexs_refl"
 988 "rexs_sort"
 989 "rexs_step_dx"
 990 "rexs_step_sn"
 991 "rexs_sym"
 992 "rexs_tc"
 993 "rexs_trans"
 994 "rexs_unit"
 995 "rex_sym"
 996 "rex_trans_fsle"
 997 "rex_transitive"
 998 "rex_trans_next"
 999 "rex_unit"
1000 "rex_unit_length"
1001 "rex_unit_sn"
1002 "R_fsge_compatible"
1003 "rfw"
1004 "rfw_clear"
1005 "rfw_lpair_dx"
1006 "rfw_lpair_sn"
1007 "rfw_shift"
1008 "rfw_tpair_dx"
1009 "rfw_tpair_sn"
1010 "rneqx_inv_bind"
1011 "rneqx_inv_bind_void"
1012 "rneqx_inv_flat"
1013 "rneqx_reqx_canc_dx"
1014 "rneqx_reqx_div"
1015 "rnex_inv_bind"
1016 "rnex_inv_bind_void"
1017 "rnex_inv_flat"
1018 "R_pw_confluent2_sex"
1019 "S1"
1020 "S2"
1021 "S3"
1022 "S5"
1023 "S6"
1024 "S7"
1025 "sd"
1026 "sd_d"
1027 "sd_d_correct"
1028 "sd_d_props"
1029 "sd_d_SS"
1030 "sd_O"
1031 "sd_O_props"
1032 "sd_props"
1033 "sd_SO"
1034 "sd_SO_props"
1035 "seq"
1036 "seq_canc_dx"
1037 "seq_canc_sn"
1038 "seq_co_dedropable_sn"
1039 "seq_co_dropable_dx"
1040 "seq_co_dropable_sn"
1041 "seq_drops_conf_next"
1042 "seq_drops_trans_next"
1043 "seq_eq_repl_back"
1044 "seq_eq_repl_fwd"
1045 "seq_fwd_length"
1046 "seq_inv_atom1"
1047 "seq_inv_atom2"
1048 "seq_inv_next"
1049 "seq_inv_next1"
1050 "seq_inv_next2"
1051 "seq_inv_push"
1052 "seq_inv_push1"
1053 "seq_inv_push2"
1054 "seq_inv_tl"
1055 "seq_join"
1056 "seq_meet"
1057 "seq_refl"
1058 "seq_sym"
1059 "seq_trans"
1060 "sex"
1061 "sex_atom"
1062 "sex_canc_dx"
1063 "sex_canc_sn"
1064 "sex_co"
1065 "sex_co_dropable_dx"
1066 "sex_co_dropable_sn"
1067 "sex_co_isid"
1068 "sex_conf"
1069 "sex_dec"
1070 "sex_dropable_dx_aux"
1071 "sex_drops_conf_next"
1072 "sex_drops_conf_push"
1073 "sex_drops_trans_next"
1074 "sex_drops_trans_push"
1075 "sex_eq_repl_back"
1076 "sex_eq_repl_fwd"
1077 "sex_fwd_bind"
1078 "sex_fwd_length"
1079 "sex_inv_atom1"
1080 "sex_inv_atom1_aux"
1081 "sex_inv_atom2"
1082 "sex_inv_atom2_aux"
1083 "sex_inv_next"
1084 "sex_inv_next1"
1085 "sex_inv_next1_aux"
1086 "sex_inv_next2"
1087 "sex_inv_next2_aux"
1088 "sex_inv_push"
1089 "sex_inv_push1"
1090 "sex_inv_push1_aux"
1091 "sex_inv_push2"
1092 "sex_inv_push2_aux"
1093 "sex_inv_tc_dx"
1094 "sex_inv_tc_sn"
1095 "sex_inv_tl"
1096 "sex_join"
1097 "sex_length_cfull"
1098 "sex_length_isid"
1099 "sex_liftable_co_dedropable_bi"
1100 "sex_liftable_co_dedropable_sn"
1101 "sex_meet"
1102 "sex_next"
1103 "sex_pair_repl"
1104 "sex_push"
1105 "sex_refl"
1106 "sex_sdj"
1107 "sex_sdj_split"
1108 "sex_sle_split"
1109 "sex_sym"
1110 "sex_tc_dx"
1111 "sex_tc_inj_dx"
1112 "sex_tc_inj_sn"
1113 "sex_tc_next"
1114 "sex_tc_next_dx"
1115 "sex_tc_next_sn"
1116 "sex_tc_push"
1117 "sex_tc_push_dx"
1118 "sex_tc_push_sn"
1119 "sex_tc_refl"
1120 "sex_tc_step_dx"
1121 "sex_trans"
1122 "sex_trans_gen"
1123 "sex_trans_id_cfull"
1124 "sex_transitive"
1125 "sh"
1126 "sh_acyclic"
1127 "sh_decidable"
1128 "sh_lt"
1129 "sh_lt_acyclic"
1130 "sh_lt_dec"
1131 "sh_lt_nexts_inv_lt"
1132 "simple"
1133 "simple_atom"
1134 "simple_dec_ex"
1135 "simple_flat"
1136 "simple_inv_bind"
1137 "simple_inv_bind_aux"
1138 "simple_inv_pair"
1139 "simple_teqo_repl_dx"
1140 "simple_teqo_repl_sn"
1141 "sle_seq_trans"
1142 "sle_sex_conf"
1143 "sle_sex_trans"
1144 "Sort"
1145 "s_rs_transitive_isid"
1146 "s_rs_transitive_lex_inv_isid"
1147 "TAtom"
1148 "tc_f_dedropable_sn"
1149 "tc_f_dropable_dx"
1150 "tc_f_dropable_sn"
1151 "teqo"
1152 "teqo_canc_dx"
1153 "teqo_canc_sn"
1154 "teqo_dec"
1155 "teqo_gref"
1156 "teqo_inv_applv_bind_simple"
1157 "teqo_inv_gref1"
1158 "teqo_inv_gref1_aux"
1159 "teqo_inv_lifts_bi"
1160 "teqo_inv_lref1"
1161 "teqo_inv_lref1_aux"
1162 "teqo_inv_pair"
1163 "teqo_inv_pair1"
1164 "teqo_inv_pair1_aux"
1165 "teqo_inv_pair2"
1166 "teqo_inv_pair2_aux"
1167 "teqo_inv_sort1"
1168 "teqo_inv_sort1_aux"
1169 "teqo_lifts_bi"
1170 "teqo_lifts_dx"
1171 "teqo_lifts_sn"
1172 "teqo_lref"
1173 "teqo_pair"
1174 "teqo_refl"
1175 "teqo_sort"
1176 "teqo_sym"
1177 "teqo_trans"
1178 "teqx"
1179 "teqx_canc_dx"
1180 "teqx_canc_sn"
1181 "teqx_dec"
1182 "teqx_ext"
1183 "teqx_feqx"
1184 "teqx_fqup_trans"
1185 "teqx_fquq_trans"
1186 "teqx_fqus_trans"
1187 "teqx_fqu_trans"
1188 "teqx_fwd_atom1"
1189 "teqx_gref"
1190 "teqx_inv_gref1"
1191 "teqx_inv_gref1_aux"
1192 "teqx_inv_lifts_bi"
1193 "teqx_inv_lifts_dx"
1194 "teqx_inv_lifts_sn"
1195 "teqx_inv_lref1"
1196 "teqx_inv_lref1_aux"
1197 "teqx_inv_pair"
1198 "teqx_inv_pair1"
1199 "teqx_inv_pair1_aux"
1200 "teqx_inv_pair2"
1201 "teqx_inv_pair_xy_x"
1202 "teqx_inv_pair_xy_y"
1203 "teqx_inv_sort1"
1204 "teqx_inv_sort1_aux"
1205 "teqx_inv_sort2"
1206 "teqx_lifts_bi"
1207 "teqx_lifts_dx"
1208 "teqx_lifts_inv_pair_sn"
1209 "teqx_lifts_sn"
1210 "teqx_lref"
1211 "teqx_pair"
1212 "teqx_refl"
1213 "teqx_repl"
1214 "teqx_reqx_conf"
1215 "teqx_reqx_div"
1216 "teqx_rex_conf"
1217 "teqx_rex_div"
1218 "teqx_sort"
1219 "teqx_sym"
1220 "teqx_teqo"
1221 "teqx_tneqx_trans"
1222 "teqx_trans"
1223 "teqx_tweq"
1224 "term"
1225 "tneqx_inv_pair"
1226 "tneqx_teqx_canc_dx"
1227 "TPair"
1228 "tw"
1229 "tweq"
1230 "tweq_abbr"
1231 "tweq_abbr_neg"
1232 "tweq_abbr_pos"
1233 "tweq_abst"
1234 "tweq_appl"
1235 "tweq_canc_dx"
1236 "tweq_canc_sn"
1237 "tweq_cast"
1238 "tweq_dec"
1239 "tweq_fwd_pair_bi"
1240 "tweq_fwd_pair_sn"
1241 "tweq_gref"
1242 "tweq_inv_abbr_neg_sn"
1243 "tweq_inv_abbr_pos_bi"
1244 "tweq_inv_abbr_pos_sn"
1245 "tweq_inv_abbr_pos_x_lifts_y_y"
1246 "tweq_inv_abbr_sn"
1247 "tweq_inv_abbr_sn_aux"
1248 "tweq_inv_abst_sn"
1249 "tweq_inv_abst_sn_aux"
1250 "tweq_inv_appl_bi"
1251 "tweq_inv_appl_sn"
1252 "tweq_inv_appl_sn_aux"
1253 "tweq_inv_cast_bi"
1254 "tweq_inv_cast_sn"
1255 "tweq_inv_cast_sn_aux"
1256 "tweq_inv_cast_xy_y"
1257 "tweq_inv_gref_sn"
1258 "tweq_inv_gref_sn_aux"
1259 "tweq_inv_lifts_bi"
1260 "tweq_inv_lref_sn"
1261 "tweq_inv_lref_sn_aux"
1262 "tweq_inv_sort_sn"
1263 "tweq_inv_sort_sn_aux"
1264 "tweq_lifts_bi"
1265 "tweq_lifts_dx"
1266 "tweq_lifts_sn"
1267 "tweq_lref"
1268 "tweq_refl"
1269 "tweq_repl"
1270 "tweq_simple_trans"
1271 "tweq_sort"
1272 "tweq_sym"
1273 "tweq_trans"
1274 "tw_le_pair_dx"
1275 "tw_pos"
1276 "Void"