X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fnames.txt;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fstatic_2%2Fnames.txt;h=6af48b1ca3b1964e59794a726afa98207fbb3dde;hb=076439def28e649ec384fae038ed021dadd5f75c;hp=0000000000000000000000000000000000000000;hpb=d2545ffd201b1aa49887313791386add78fa8603;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/static_2/names.txt b/matita/matita/contribs/lambdadelta/static_2/names.txt
new file mode 100644
index 000000000..6af48b1ca
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/static_2/names.txt
@@ -0,0 +1,1276 @@
+aaa
+aaa_aaa_inv_appl
+aaa_aaa_inv_cast
+aaa_abbr
+aaa_abst
+aaa_appl
+aaa_cast
+aaa_dec
+aaa_feqx_conf
+aaa_fqu_conf
+aaa_fqup_conf
+aaa_fquq_conf
+aaa_fqus_conf
+aaa_inv_abbr
+aaa_inv_abbr_aux
+aaa_inv_abst
+aaa_inv_abst_aux
+aaa_inv_appl
+aaa_inv_appl_aux
+aaa_inv_cast
+aaa_inv_cast_aux
+aaa_inv_gref
+aaa_inv_gref_aux
+aaa_inv_lifts
+aaa_inv_lref
+aaa_inv_lref_aux
+aaa_inv_lref_drops
+aaa_inv_sort
+aaa_inv_sort_aux
+aaa_inv_zero
+aaa_inv_zero_aux
+aaa_lifts
+aaa_lref
+aaa_lref_drops
+aaa_mono
+aaa_pair_inv_lref
+aaa_sort
+aaa_teqx_conf_reqx
+aaa_zero
+aarity
+AAtom
+Abbr
+Abst
+abst_dec
+ac
+ac_eq
+ac_eq_props
+ac_le
+acle
+acle_eq_le
+acle_eq_monotonic_le
+acle_le_eq
+acle_le_monotonic_le
+acle_omega
+acle_one
+ac_le_props
+acle_refl
+acle_trans
+ac_props
+acr
+acr_aaa
+acr_aaa_csubc_lifts
+acr_abst
+acr_gcr
+acr_lifts
+ac_top
+ac_top_props
+APair
+append
+append_assoc
+append_atom
+append_atom_sn
+append_bind
+append_inj_dx
+append_inj_length_dx
+append_inj_length_sn
+append_inj_sn
+append_inv_atom3_sn
+append_inv_bind3_sn
+append_inv_pair_dx
+append_inv_refl_dx
+append_length
+append_shift
+Appl
+applv
+applv_cons
+applv_nil
+applv_simple
+apply_top
+bind
+bind1
+bind2
+Bind2
+BPair
+BUnit
+bw
+bw_pos
+candidate
+Cast
+cdeq
+cdeq_ext
+ceq
+ceq_ext
+ceq_ext_inv_eq
+ceq_ext_refl
+ceq_ext_trans
+ceq_inv_lift_sn
+ceq_lift_sn
+cext2
+cext2_co
+cext2_d_liftable2_sn
+cext2_sym
+cfull
+cfull_dec
+cfull_lift_sn
+cfun
+co_dedropable_sn
+co_dedropable_sn_CTC
+co_dedropable_sn_ltc
+co_dropable_dx
+co_dropable_dx_CTC
+co_dropable_dx_ltc
+co_dropable_sn
+co_dropable_sn_CTC
+co_dropable_sn_ltc
+CP0
+CP1
+CP2
+CP3
+d1_liftable_liftable_all
+d2_deliftable_sn_CTC
+d2_deliftable_sn_ltc
+d2_liftable_sn_CTC
+d2_liftable_sn_ltc
+d_appendable_sn
+d_deliftable1
+d_deliftable1_isuni
+d_deliftable2_bi
+d_deliftable2_sn
+d_deliftable2_sn_bi
+dedropable_sn
+dedropable_sn_CTC
+deg_inv_prec
+deg_inv_pred
+deg_iter
+deg_next_SO
+deg_O
+deg_SO
+deg_SO_gt
+deg_SO_inv_succ
+deg_SO_inv_succ_aux
+deg_SO_refl
+deg_SO_succ
+deg_SO_zero
+deliftable2_bi
+deliftable2_dx
+deliftable2_sn
+deliftable2_sn_bi
+deliftable2_sn_dx
+destruct_apair_apair_aux
+destruct_lbind_lbind_aux
+destruct_sort_sort_aux
+destruct_tatom_tatom_aux
+destruct_tpair_tpair_aux
+discr_apair_xy_x
+discr_apair_xy_y
+discr_lbind_x_xy
+discr_lbind_xy_x
+discr_tpair_xy_x
+discr_tpair_xy_y
+d_liftable1
+d_liftable1_all
+d_liftable1_isuni
+d_liftable2_bi
+d_liftable2_sn
+d_liftable2_sn_bi
+dropable_dx
+dropable_dx_CTC
+dropable_sn
+dropable_sn_CTC
+drops
+drops_after_fwd_drop2
+drops_atom
+drops_atom2_sex_conf
+drops_atom_F
+drops_bind2_fwd_rfw
+drops_conf
+drops_conf_div
+drops_conf_div_bind_isuni
+drops_conf_div_fcla
+drops_conf_div_isuni
+drops_conf_skip1
+drops_drop
+drops_eq_repl_back
+drops_eq_repl_fwd
+drops_F
+drops_fcla_fwd
+drops_fcla_fwd_le2
+drops_fcla_fwd_lt2
+drops_fcla_fwd_lt4
+drops_F_uni
+drops_fwd_drop2
+drops_fwd_drop2_aux
+drops_fwd_fcla
+drops_fwd_fcla_le2
+drops_fwd_fcla_lt2
+drops_fwd_isfin
+drops_fwd_isid
+drops_fwd_length_eq1
+drops_fwd_length_eq2
+drops_fwd_length_le4
+drops_fwd_lw
+drops_fwd_lw_lt
+drops_gen
+drops_inv_atom1
+drops_inv_atom1_aux
+drops_inv_atom2
+drops_inv_bind1_isuni
+drops_inv_bind2_isuni
+drops_inv_bind2_isuni_next
+drops_inv_drop1
+drops_inv_drop1_aux
+drops_inv_F
+drops_inv_gen
+drops_inv_isuni
+drops_inv_length_eq
+drops_inv_skip1
+drops_inv_skip1_aux
+drops_inv_skip2
+drops_inv_skip2_aux
+drops_inv_succ
+drops_inv_TF
+drops_inv_TF_aux
+drops_inv_uni
+drops_inv_x_bind_xy
+drops_isuni_ex
+drops_isuni_fwd_drop2
+drops_ldec_dec
+drops_lsubc_trans
+drops_mono
+drops_refl
+drops_seq_trans_next
+drops_sex_trans_next
+drops_sex_trans_push
+drops_skip
+drops_split_div
+drops_split_trans
+drops_split_trans_bind2
+drops_TF
+drops_tls_at
+drops_trans
+drops_trans_skip2
+eq_aarity_dec
+eq_bind1_dec
+eq_bind2_dec
+eq_bind_dec
+eq_false_inv_tpair_dx
+eq_false_inv_tpair_sn
+eq_flat2_dec
+eq_genv_dec
+eq_item0_dec
+eq_item2_dec
+eq_lenv_dec
+eq_term_dec
+ext2
+ext2_dec
+ext2_inv_pair
+ext2_inv_pair_dx
+ext2_inv_pair_dx_aux
+ext2_inv_pair_sn
+ext2_inv_pair_sn_aux
+ext2_inv_tc
+ext2_inv_unit
+ext2_inv_unit_dx
+ext2_inv_unit_dx_aux
+ext2_inv_unit_sn
+ext2_inv_unit_sn_aux
+ext2_pair
+ext2_refl
+ext2_sym
+ext2_tc
+ext2_tc_inj
+ext2_tc_pair
+ext2_tc_step
+ext2_trans
+ext2_unit
+f_dedropable_sn
+f_dropable_dx
+f_dropable_sn
+feqx
+feqx_canc_dx
+feqx_canc_sn
+feqx_fqus_trans
+feqx_intro_dx
+feqx_intro_sn
+feqx_inv_gen_dx
+feqx_inv_gen_sn
+feqx_refl
+feqx_sym
+feqx_tneqx_repl_dx
+feqx_trans
+flat2
+Flat2
+fold
+fold_atom
+fold_pair
+fold_unit
+fqu
+fqu_bind_dx
+fqu_clear
+fqu_drop
+fqu_flat_dx
+fqu_fqup
+fqu_fquq
+fqu_fwd_fw
+fqu_fwd_length_lref1
+fqu_fwd_length_lref1_aux
+fqu_gref
+fqu_inv_atom1
+fqu_inv_bind1
+fqu_inv_bind1_aux
+fqu_inv_bind1_true
+fqu_inv_flat1
+fqu_inv_flat1_aux
+fqu_inv_gref1
+fqu_inv_gref1_aux
+fqu_inv_gref1_bind
+fqu_inv_lref1
+fqu_inv_lref1_aux
+fqu_inv_lref1_bind
+fqu_inv_sort1
+fqu_inv_sort1_aux
+fqu_inv_sort1_bind
+fqu_inv_teqx
+fqu_inv_teqx_aux
+fqu_inv_zero1_pair
+fqu_lref_O
+fqu_lref_S
+fqup
+fqu_pair_sn
+fqup_bind_dx
+fqup_bind_dx_flat_dx
+fqup_clear
+fqup_drops_strap1
+fqup_drops_succ
+fqup_flat_dx
+fqup_flat_dx_bind_dx
+fqup_flat_dx_pair_sn
+fqup_fqus
+fqup_fqus_trans
+fqup_fwd_fw
+fqup_ind
+fqup_ind_dx
+fqup_inv_step_sn
+fqup_lref
+fqup_pair_sn
+fqup_strap1
+fqup_strap2
+fqup_trans
+fqup_wf_ind
+fqup_wf_ind_eq
+fqup_zeta
+fquq
+fquq_fqus
+fquq_fwd_fw
+fquq_fwd_length_lref1
+fquq_refl
+fqus
+fqus_drops
+fqus_fqup_trans
+fqus_fwd_fw
+fqus_ind
+fqus_ind_dx
+fqus_inv_atom1
+fqus_inv_bind1
+fqus_inv_bind1_true
+fqus_inv_flat1
+fqus_inv_fqup
+fqus_inv_fqu_sn
+fqus_inv_gref1
+fqus_inv_gref1_bind
+fqus_inv_lref1
+fqus_inv_lref1_bind
+fqus_inv_refl_atom3
+fqus_inv_sort1
+fqus_inv_sort1_bind
+fqus_inv_zero1_pair
+fqu_sort
+fqus_refl
+fqus_strap1
+fqus_strap1_fqu
+fqus_strap2
+fqus_strap2_fqu
+fqus_trans
+fqu_teqx_conf
+fqu_wf_ind
+frees
+frees_append_void
+frees_atom
+frees_atom_drops
+frees_bind
+frees_bind_void
+frees_eq_repl_back
+frees_eq_repl_fwd
+frees_flat
+frees_fwd_coafter
+frees_fwd_isfin
+frees_gref
+frees_ind_void
+frees_inv_append_void
+frees_inv_append_void_aux
+frees_inv_atom
+frees_inv_atom_aux
+frees_inv_bind
+frees_inv_bind_aux
+frees_inv_bind_void
+frees_inv_drops_next
+frees_inv_flat
+frees_inv_flat_aux
+frees_inv_gref
+frees_inv_gref_aux
+frees_inv_lifts
+frees_inv_lifts_ex
+frees_inv_lifts_SO
+frees_inv_lref
+frees_inv_lref_aux
+frees_inv_lref_drops
+frees_inv_pair
+frees_inv_pair_aux
+frees_inv_sort
+frees_inv_sort_aux
+frees_inv_unit
+frees_inv_unit_aux
+frees_lifts
+frees_lifts_SO
+frees_lref
+frees_lref_push
+frees_lref_pushs
+frees_mono
+frees_pair
+frees_pair_drops
+frees_req_conf
+frees_reqx_conf
+frees_sex_conf
+frees_sort
+frees_teqx_conf
+frees_teqx_conf_reqx
+frees_total
+frees_unit
+frees_unit_drops
+fsge_rex_trans
+fsle
+fsle_bind
+fsle_bind_dx_dx
+fsle_bind_dx_sn
+fsle_bind_eq
+fsle_bind_sn_ge
+fsle_flat
+fsle_flat_dx_dx
+fsle_flat_dx_sn
+fsle_flat_sn
+fsle_frees_trans
+fsle_frees_trans_eq
+fsle_fwd_pair_sn
+fsle_gref
+fsle_gref_bi
+fsle_inv_frees_eq
+fsle_inv_lifts_sn
+fsle_lifts_dx
+fsle_lifts_sn
+fsle_lifts_SO
+fsle_lifts_SO_sn
+fsle_pair_bi
+fsle_refl
+fsle_shift
+fsle_sort
+fsle_sort_bi
+fsle_trans_dx
+fsle_trans_rc
+fsle_trans_sn
+fsle_unit_bi
+f_transitive_next
+fw
+fw_clear
+fw_lpair_sn
+fw_shift
+fw_tpair_dx
+fw_tpair_sn
+GAtom
+gcp
+gcp2_all
+gcr
+gcr_aaa
+genv
+glength
+GPair
+GRef
+gw
+gw_pair
+is_apear_dec
+is_lifts_dec
+item0
+item2
+LAtom
+LBind
+length
+length_atom
+length_bind
+length_inv_succ_dx
+length_inv_succ_dx_ltail
+length_inv_succ_sn
+length_inv_succ_sn_ltail
+length_inv_zero_dx
+length_inv_zero_sn
+lenv
+lenv_case_tail
+lenv_ind_tail
+lex
+lex_atom
+lex_bind
+lex_bind_refl_dx
+lex_co
+lex_conf
+lex_confluent
+lex_CTC
+lex_CTC_ind_dx
+lex_CTC_ind_sn
+lex_CTC_inj
+lex_CTC_step_dx
+lex_CTC_step_sn
+lex_dropable_dx
+lex_dropable_sn
+lex_drops_conf_pair
+lex_drops_trans_pair
+lex_fwd_length
+lex_ind
+lex_inv_atom_dx
+lex_inv_atom_sn
+lex_inv_bind_dx
+lex_inv_bind_sn
+lex_inv_CTC
+lex_inv_pair
+lex_inv_pair_dx
+lex_inv_pair_sn
+lex_inv_unit_dx
+lex_inv_unit_sn
+lex_liftable_dedropable_sn
+lex_pair
+lex_refl
+lex_trans
+lex_transitive
+lex_unit
+liftable2_bi
+liftable2_dx
+liftable2_sn
+liftable2_sn_bi
+liftable2_sn_dx
+lifts
+lifts_applv
+liftsb
+liftsb_conf
+liftsb_div3
+liftsb_eq_repl_back
+liftsb_fwd_bw
+liftsb_fwd_isid
+lifts_bind
+liftsb_inj
+liftsb_inv_pair_dx
+liftsb_inv_pair_sn
+liftsb_inv_unit_dx
+liftsb_inv_unit_sn
+liftsb_mono
+liftsb_refl
+liftsb_split_trans
+liftsb_total
+liftsb_trans
+lifts_conf
+lifts_div3
+lifts_div4
+lifts_div4_one
+lifts_eq_repl_back
+lifts_eq_repl_fwd
+lifts_flat
+lifts_fwd_isid
+lifts_fwd_pair1
+lifts_fwd_pair2
+lifts_fwd_tw
+lifts_gref
+lifts_inj
+lifts_inv_applv1
+lifts_inv_applv2
+lifts_inv_atom1
+lifts_inv_atom2
+lifts_inv_bind1
+lifts_inv_bind1_aux
+lifts_inv_bind2
+lifts_inv_bind2_aux
+lifts_inv_flat1
+lifts_inv_flat1_aux
+lifts_inv_flat2
+lifts_inv_flat2_aux
+lifts_inv_gref1
+lifts_inv_gref1_aux
+lifts_inv_gref2
+lifts_inv_gref2_aux
+lifts_inv_lref1
+lifts_inv_lref1_aux
+lifts_inv_lref1_uni
+lifts_inv_lref2
+lifts_inv_lref2_aux
+lifts_inv_lref2_uni
+lifts_inv_lref2_uni_ge
+lifts_inv_lref2_uni_lt
+lifts_inv_pair_xy_x
+lifts_inv_pair_xy_y
+lifts_inv_push_succ_sn
+lifts_inv_push_zero_sn
+lifts_inv_sort1
+lifts_inv_sort1_aux
+lifts_inv_sort2
+lifts_inv_sort2_aux
+lifts_lref
+lifts_lref_ge
+lifts_lref_ge_minus
+lifts_lref_lt
+lifts_lref_uni
+lifts_mono
+lifts_push_lref
+lifts_push_zero
+lifts_refl
+lifts_simple_dx
+lifts_simple_sn
+lifts_sort
+lifts_split_div
+lifts_split_trans
+lifts_total
+lifts_trans
+lifts_trans4_one
+lifts_trans_uni
+lifts_uni
+liftsv
+liftsv_cons
+liftsv_inj
+liftsv_inv_cons1
+liftsv_inv_cons1_aux
+liftsv_inv_cons2
+liftsv_inv_cons2_aux
+liftsv_inv_nil1
+liftsv_inv_nil1_aux
+liftsv_inv_nil2
+liftsv_inv_nil2_aux
+liftsv_mono
+liftsv_nil
+liftsv_split_trans
+liftsv_total
+liftsv_trans
+LRef
+lsuba
+lsuba_aaa_conf
+lsuba_aaa_trans
+lsuba_atom
+lsuba_beta
+lsuba_bind
+lsuba_drops_conf_isuni
+lsuba_drops_trans_isuni
+lsuba_fwd_lsubr
+lsuba_inv_atom1
+lsuba_inv_atom1_aux
+lsuba_inv_atom2
+lsuba_inv_atom2_aux
+lsuba_inv_bind1
+lsuba_inv_bind1_aux
+lsuba_inv_bind2
+lsuba_inv_bind2_aux
+lsuba_lsubc
+lsuba_refl
+lsuba_trans
+lsubc
+lsubc_atom
+lsubc_beta
+lsubc_bind
+lsubc_drops_trans_isuni
+lsubc_fwd_lsubr
+lsubc_inv_atom1
+lsubc_inv_atom1_aux
+lsubc_inv_atom2
+lsubc_inv_atom2_aux
+lsubc_inv_bind1
+lsubc_inv_bind1_aux
+lsubc_inv_bind2
+lsubc_inv_bind2_aux
+lsubc_refl
+lsubf
+lsubf_atom
+lsubf_beta
+lsubf_beta_tl_dx
+lsubf_bind
+lsubf_bind_tl_dx
+lsubf_eq_repl_back1
+lsubf_eq_repl_back2
+lsubf_eq_repl_fwd1
+lsubf_eq_repl_fwd2
+lsubf_frees_trans
+lsubf_fwd_bind_tl
+lsubf_fwd_isid_dx
+lsubf_fwd_isid_sn
+lsubf_fwd_lsubr_isdiv
+lsubf_fwd_sle
+lsubf_inv_atom
+lsubf_inv_atom1
+lsubf_inv_atom1_aux
+lsubf_inv_atom2
+lsubf_inv_atom2_aux
+lsubf_inv_beta_sn
+lsubf_inv_bind_sn
+lsubf_inv_pair1
+lsubf_inv_pair1_aux
+lsubf_inv_pair2
+lsubf_inv_pair2_aux
+lsubf_inv_push1
+lsubf_inv_push1_aux
+lsubf_inv_push2
+lsubf_inv_push2_aux
+lsubf_inv_push_sn
+lsubf_inv_refl
+lsubf_inv_sor_dx
+lsubf_inv_unit1
+lsubf_inv_unit1_aux
+lsubf_inv_unit2
+lsubf_inv_unit2_aux
+lsubf_inv_unit_sn
+lsubf_push
+lsubf_refl
+lsubf_refl_eq
+lsubf_sor
+lsubf_unit
+lsubr
+lsubr_atom
+lsubr_beta
+lsubr_bind
+lsubr_fwd_bind1
+lsubr_fwd_bind2
+lsubr_fwd_drops2_abbr
+lsubr_fwd_drops2_bind
+lsubr_fwd_length
+lsubr_inv_abbr2
+lsubr_inv_abst1
+lsubr_inv_abst2
+lsubr_inv_atom1
+lsubr_inv_atom1_aux
+lsubr_inv_atom2
+lsubr_inv_atom2_aux
+lsubr_inv_bind1
+lsubr_inv_bind1_aux
+lsubr_inv_bind2
+lsubr_inv_bind2_aux
+lsubr_inv_pair2
+lsubr_inv_unit1
+lsubr_inv_unit2
+lsubr_lsubf
+lsubr_lsubf_isid
+lsubr_refl
+lsubr_trans
+lsubr_unit
+ltail_length
+lveq
+lveq_atom
+lveq_bind
+lveq_fwd_abst_bind_length_le
+lveq_fwd_bind_abst_length_le
+lveq_fwd_gen
+lveq_fwd_length
+lveq_fwd_length_eq
+lveq_fwd_length_le_dx
+lveq_fwd_length_le_sn
+lveq_fwd_length_minus
+lveq_fwd_length_plus
+lveq_fwd_pair_dx
+lveq_fwd_pair_sn
+lveq_inj
+lveq_inj_length
+lveq_inj_void_dx_le
+lveq_inj_void_sn_ge
+lveq_inv_atom_atom
+lveq_inv_atom_bind
+lveq_inv_bind
+lveq_inv_bind_atom
+lveq_inv_bind_O
+lveq_inv_pair_pair
+lveq_inv_succ
+lveq_inv_succ_aux
+lveq_inv_succ_dx
+lveq_inv_succ_sn
+lveq_inv_succ_sn_aux
+lveq_inv_void_dx_length
+lveq_inv_void_sn_length
+lveq_inv_void_succ_dx
+lveq_inv_void_succ_sn
+lveq_inv_zero
+lveq_inv_zero_aux
+lveq_length_eq
+lveq_length_fwd_dx
+lveq_length_fwd_sn
+lveq_refl
+lveq_sym
+lveq_void_dx
+lveq_void_sn
+lw
+lw_bind
+mk_ac
+mk_ac_props
+mk_gcp
+mk_gcr
+mk_sd
+mk_sd_props
+mk_sh
+mk_sh_acyclic
+mk_sh_decidable
+mk_sh_lt
+nexts_le
+nexts_lt
+nf
+R_confluent2_rex
+req
+req_feqx_trans
+req_fsle_comp
+req_fwd_rex
+req_inv_bind
+req_inv_flat
+req_inv_lifts_bi
+req_inv_lref_bind_dx
+req_inv_lref_bind_sn
+req_inv_zero_pair_dx
+req_inv_zero_pair_sn
+req_refl
+req_reqx
+req_reqx_trans
+req_rex_trans
+req_transitive
+reqx
+reqx_atom
+reqx_bind
+reqx_bind_repl_dx
+reqx_bind_void
+reqx_canc_dx
+reqx_canc_sn
+reqx_dec
+reqx_flat
+reqx_fqup_trans
+reqx_fquq_trans
+reqx_fqus_trans
+reqx_fqu_trans
+reqx_fsge_comp
+reqx_fwd_bind_dx
+reqx_fwd_bind_dx_void
+reqx_fwd_dx
+reqx_fwd_flat_dx
+reqx_fwd_length
+reqx_fwd_pair_sn
+reqx_fwd_zero_pair
+reqx_gref
+reqx_gref_length
+reqx_inv_atom_dx
+reqx_inv_atom_sn
+reqx_inv_bind
+reqx_inv_bind_void
+reqx_inv_flat
+reqx_inv_lifts_bi
+reqx_inv_lifts_dx
+reqx_inv_lifts_sn
+reqx_inv_lref
+reqx_inv_lref_bind_dx
+reqx_inv_lref_bind_sn
+reqx_inv_lref_pair_bi
+reqx_inv_lref_pair_dx
+reqx_inv_lref_pair_sn
+reqx_inv_zero
+reqx_inv_zero_pair_dx
+reqx_inv_zero_pair_sn
+reqx_lifts_bi
+reqx_lifts_sn
+reqx_lref
+reqx_pair
+reqx_pair_refl
+reqx_refl
+reqx_repl
+reqx_rneqx_trans
+reqx_sort
+reqx_sort_length
+reqx_sym
+reqx_trans
+reqx_unit
+reqx_unit_length
+rex
+rex_atom
+rex_bind
+rex_bind_dx_split
+rex_bind_dx_split_void
+rex_bind_repl_dx
+rex_bind_void
+rex_co
+rex_conf
+rex_confluent
+rex_dec
+rex_dropable_dx
+rex_dropable_sn
+rex_flat
+rex_flat_dx_split
+rex_fsge_compatible
+rex_fsle_compatible
+rex_fwd_bind_dx
+rex_fwd_bind_dx_void
+rex_fwd_dx
+rex_fwd_flat_dx
+rex_fwd_length
+rex_fwd_pair_sn
+rex_fwd_zero_pair
+rex_gref
+rex_gref_length
+rex_inv_atom_dx
+rex_inv_atom_sn
+rex_inv_bind
+rex_inv_bind_void
+rex_inv_flat
+rex_inv_frees
+rex_inv_gref
+rex_inv_gref_bind_dx
+rex_inv_gref_bind_sn
+rex_inv_lex_req
+rex_inv_lifts_bi
+rex_inv_lref
+rex_inv_lref_bind_dx
+rex_inv_lref_bind_sn
+rex_inv_lref_pair_bi
+rex_inv_lref_pair_dx
+rex_inv_lref_pair_sn
+rex_inv_lref_unit_dx
+rex_inv_lref_unit_sn
+rex_inv_sort
+rex_inv_sort_bind_dx
+rex_inv_sort_bind_sn
+rex_inv_zero
+rex_inv_zero_length
+rex_inv_zero_pair_dx
+rex_inv_zero_pair_sn
+rex_inv_zero_unit_dx
+rex_inv_zero_unit_sn
+rex_isid
+rex_lex
+rex_liftable_dedropable_sn
+rex_lifts_bi
+rex_lref
+rex_pair
+rex_pair_refl
+rex_pair_sn_split
+rex_refl
+rexs
+rexs_atom
+rexs_co
+rexs_fwd_bind_dx
+rexs_fwd_bind_dx_void
+rexs_fwd_flat_dx
+rexs_fwd_length
+rexs_fwd_pair_sn
+rexs_gref
+rexs_ind_dx
+rexs_ind_sn
+rexs_inv_atom_dx
+rexs_inv_atom_sn
+rexs_inv_bind
+rexs_inv_bind_void
+rexs_inv_flat
+rexs_inv_gref
+rexs_inv_gref_bind_dx
+rexs_inv_gref_bind_sn
+rexs_inv_lex_req
+rexs_inv_sort
+rexs_inv_sort_bind_dx
+rexs_inv_sort_bind_sn
+rexs_lex
+rexs_lex_req
+rexs_lref
+rex_sort
+rex_sort_length
+rexs_pair
+rexs_pair_refl
+rexs_refl
+rexs_sort
+rexs_step_dx
+rexs_step_sn
+rexs_sym
+rexs_tc
+rexs_trans
+rexs_unit
+rex_sym
+rex_trans_fsle
+rex_transitive
+rex_trans_next
+rex_unit
+rex_unit_length
+rex_unit_sn
+R_fsge_compatible
+rfw
+rfw_clear
+rfw_lpair_dx
+rfw_lpair_sn
+rfw_shift
+rfw_tpair_dx
+rfw_tpair_sn
+rneqx_inv_bind
+rneqx_inv_bind_void
+rneqx_inv_flat
+rneqx_reqx_canc_dx
+rneqx_reqx_div
+rnex_inv_bind
+rnex_inv_bind_void
+rnex_inv_flat
+R_pw_confluent2_sex
+S1
+S2
+S3
+S5
+S6
+S7
+sd
+sd_d
+sd_d_correct
+sd_d_props
+sd_d_SS
+sd_O
+sd_O_props
+sd_props
+sd_SO
+sd_SO_props
+seq
+seq_canc_dx
+seq_canc_sn
+seq_co_dedropable_sn
+seq_co_dropable_dx
+seq_co_dropable_sn
+seq_drops_conf_next
+seq_drops_trans_next
+seq_eq_repl_back
+seq_eq_repl_fwd
+seq_fwd_length
+seq_inv_atom1
+seq_inv_atom2
+seq_inv_next
+seq_inv_next1
+seq_inv_next2
+seq_inv_push
+seq_inv_push1
+seq_inv_push2
+seq_inv_tl
+seq_join
+seq_meet
+seq_refl
+seq_sym
+seq_trans
+sex
+sex_atom
+sex_canc_dx
+sex_canc_sn
+sex_co
+sex_co_dropable_dx
+sex_co_dropable_sn
+sex_co_isid
+sex_conf
+sex_dec
+sex_dropable_dx_aux
+sex_drops_conf_next
+sex_drops_conf_push
+sex_drops_trans_next
+sex_drops_trans_push
+sex_eq_repl_back
+sex_eq_repl_fwd
+sex_fwd_bind
+sex_fwd_length
+sex_inv_atom1
+sex_inv_atom1_aux
+sex_inv_atom2
+sex_inv_atom2_aux
+sex_inv_next
+sex_inv_next1
+sex_inv_next1_aux
+sex_inv_next2
+sex_inv_next2_aux
+sex_inv_push
+sex_inv_push1
+sex_inv_push1_aux
+sex_inv_push2
+sex_inv_push2_aux
+sex_inv_tc_dx
+sex_inv_tc_sn
+sex_inv_tl
+sex_join
+sex_length_cfull
+sex_length_isid
+sex_liftable_co_dedropable_bi
+sex_liftable_co_dedropable_sn
+sex_meet
+sex_next
+sex_pair_repl
+sex_push
+sex_refl
+sex_sdj
+sex_sdj_split
+sex_sle_split
+sex_sym
+sex_tc_dx
+sex_tc_inj_dx
+sex_tc_inj_sn
+sex_tc_next
+sex_tc_next_dx
+sex_tc_next_sn
+sex_tc_push
+sex_tc_push_dx
+sex_tc_push_sn
+sex_tc_refl
+sex_tc_step_dx
+sex_trans
+sex_trans_gen
+sex_trans_id_cfull
+sex_transitive
+sh
+sh_acyclic
+sh_decidable
+sh_lt
+sh_lt_acyclic
+sh_lt_dec
+sh_lt_nexts_inv_lt
+simple
+simple_atom
+simple_dec_ex
+simple_flat
+simple_inv_bind
+simple_inv_bind_aux
+simple_inv_pair
+simple_teqo_repl_dx
+simple_teqo_repl_sn
+sle_seq_trans
+sle_sex_conf
+sle_sex_trans
+Sort
+s_rs_transitive_isid
+s_rs_transitive_lex_inv_isid
+TAtom
+tc_f_dedropable_sn
+tc_f_dropable_dx
+tc_f_dropable_sn
+teqo
+teqo_canc_dx
+teqo_canc_sn
+teqo_dec
+teqo_gref
+teqo_inv_applv_bind_simple
+teqo_inv_gref1
+teqo_inv_gref1_aux
+teqo_inv_lifts_bi
+teqo_inv_lref1
+teqo_inv_lref1_aux
+teqo_inv_pair
+teqo_inv_pair1
+teqo_inv_pair1_aux
+teqo_inv_pair2
+teqo_inv_pair2_aux
+teqo_inv_sort1
+teqo_inv_sort1_aux
+teqo_lifts_bi
+teqo_lifts_dx
+teqo_lifts_sn
+teqo_lref
+teqo_pair
+teqo_refl
+teqo_sort
+teqo_sym
+teqo_trans
+teqx
+teqx_canc_dx
+teqx_canc_sn
+teqx_dec
+teqx_ext
+teqx_feqx
+teqx_fqup_trans
+teqx_fquq_trans
+teqx_fqus_trans
+teqx_fqu_trans
+teqx_fwd_atom1
+teqx_gref
+teqx_inv_gref1
+teqx_inv_gref1_aux
+teqx_inv_lifts_bi
+teqx_inv_lifts_dx
+teqx_inv_lifts_sn
+teqx_inv_lref1
+teqx_inv_lref1_aux
+teqx_inv_pair
+teqx_inv_pair1
+teqx_inv_pair1_aux
+teqx_inv_pair2
+teqx_inv_pair_xy_x
+teqx_inv_pair_xy_y
+teqx_inv_sort1
+teqx_inv_sort1_aux
+teqx_inv_sort2
+teqx_lifts_bi
+teqx_lifts_dx
+teqx_lifts_inv_pair_sn
+teqx_lifts_sn
+teqx_lref
+teqx_pair
+teqx_refl
+teqx_repl
+teqx_reqx_conf
+teqx_reqx_div
+teqx_rex_conf
+teqx_rex_div
+teqx_sort
+teqx_sym
+teqx_teqo
+teqx_tneqx_trans
+teqx_trans
+teqx_tweq
+term
+tneqx_inv_pair
+tneqx_teqx_canc_dx
+TPair
+tw
+tweq
+tweq_abbr
+tweq_abbr_neg
+tweq_abbr_pos
+tweq_abst
+tweq_appl
+tweq_canc_dx
+tweq_canc_sn
+tweq_cast
+tweq_dec
+tweq_fwd_pair_bi
+tweq_fwd_pair_sn
+tweq_gref
+tweq_inv_abbr_neg_sn
+tweq_inv_abbr_pos_bi
+tweq_inv_abbr_pos_sn
+tweq_inv_abbr_pos_x_lifts_y_y
+tweq_inv_abbr_sn
+tweq_inv_abbr_sn_aux
+tweq_inv_abst_sn
+tweq_inv_abst_sn_aux
+tweq_inv_appl_bi
+tweq_inv_appl_sn
+tweq_inv_appl_sn_aux
+tweq_inv_cast_bi
+tweq_inv_cast_sn
+tweq_inv_cast_sn_aux
+tweq_inv_cast_xy_y
+tweq_inv_gref_sn
+tweq_inv_gref_sn_aux
+tweq_inv_lifts_bi
+tweq_inv_lref_sn
+tweq_inv_lref_sn_aux
+tweq_inv_sort_sn
+tweq_inv_sort_sn_aux
+tweq_lifts_bi
+tweq_lifts_dx
+tweq_lifts_sn
+tweq_lref
+tweq_refl
+tweq_repl
+tweq_simple_trans
+tweq_sort
+tweq_sym
+tweq_trans
+tw_le_pair_dx
+tw_pos
+Void