# waiting #################################################################### aplus/props aplus_reg_r aplus/props aplus_assoc aplus/props aplus_asucc aplus/props aplus_sort_O_S_simpl aplus/props aplus_sort_S_S_simpl aplus/props aplus_asort_O_simpl aplus/props aplus_asort_le_simpl aplus/props aplus_asort_simpl aplus/props aplus_ahead_simpl aplus/props aplus_asucc_false aplus/props aplus_inj aprem/fwd aprem_gen_sort aprem/fwd aprem_gen_head_O aprem/fwd aprem_gen_head_S aprem/props aprem_repl aprem/props aprem_asucc arity/aprem arity_aprem arity/cimp arity_cimp_conf arity/fwd arity_gen_sort arity/fwd arity_gen_lref arity/fwd arity_gen_bind arity/fwd arity_gen_abst arity/fwd arity_gen_appl arity/fwd arity_gen_cast arity/fwd arity_gen_appls arity/fwd arity_gen_lift arity/lift1 arity_lift1 arity/pr3 arity_sred_wcpr0_pr0 arity/pr3 arity_sred_wcpr0_pr1 arity/pr3 arity_sred_pr2 arity/pr3 arity_sred_pr3 arity/props node_inh arity/props arity_lift arity/props arity_mono arity/props arity_repellent arity/props arity_appls_cast arity/props arity_appls_abbr arity/props arity_appls_bind arity/subst0 arity_gen_cvoid_subst0 arity/subst0 arity_gen_cvoid arity/subst0 arity_fsubst0 arity/subst0 arity_subst0 asucc/fwd asucc_gen_sort asucc/fwd asucc_gen_head cnt/props cnt_lift C/props clt_wf__q_ind C/props clt_wf_ind csuba/arity csuba_arity csuba/arity csuba_arity_rev csuba/arity arity_appls_appl csuba/clear csuba_clear_conf csuba/clear csuba_clear_trans csuba/drop csuba_drop_abbr csuba/drop csuba_drop_abst csuba/drop csuba_drop_abst_rev csuba/drop csuba_drop_abbr_rev csuba/fwd csuba_gen_abbr csuba/fwd csuba_gen_void csuba/fwd csuba_gen_abst csuba/fwd csuba_gen_flat csuba/fwd csuba_gen_bind csuba/fwd csuba_gen_abst_rev csuba/fwd csuba_gen_void_rev csuba/fwd csuba_gen_abbr_rev csuba/fwd csuba_gen_flat_rev csuba/fwd csuba_gen_bind_rev csuba/getl csuba_getl_abbr csuba/getl csuba_getl_abst csuba/getl csuba_getl_abst_rev csuba/getl csuba_getl_abbr_rev csuba/props csuba_refl csubc/arity csubc_arity_conf csubc/arity csubc_arity_trans csubc/csuba csubc_csuba csubc/drop1 drop1_csubc_trans csubc/drop drop_csubc_trans csubt/clear csubt_clear_conf csubt/csuba csubt_csuba csubt/drop csubt_drop_flat csubt/drop csubt_drop_abbr csubt/drop csubt_drop_abst csubt/fwd csubt_gen_abbr csubt/fwd csubt_gen_abst csubt/fwd csubt_gen_flat csubt/fwd csubt_gen_bind csubt/getl csubt_getl_abbr csubt/getl csubt_getl_abst csubt/pc3 csubt_pr2 csubt/pc3 csubt_pc3 csubt/props csubt_refl csubt/ty3 csubt_ty3 csubt/ty3 csubt_ty3_ld csubv/clear csubv_clear_conf csubv/clear csubv_clear_conf_void csubv/drop csubv_drop_conf csubv/getl csubv_getl_conf csubv/getl csubv_getl_conf_void csubv/props csubv_bind_same csubv/props csubv_refl drop1/props drop1_cons_tail ex0/props aplus_gz_le ex0/props aplus_gz_ge ex0/props next_plus_gz ex0/props leqz_leq ex0/props leq_leqz ex1/props ex1__leq_sort_SS ex1/props ex1_arity ex1/props ex1_ty3 ex2/props ex2_nf2 ex2/props ex2_arity fsubst0/fwd fsubst0_gen_base leq/asucc asucc_repl leq/asucc asucc_inj leq/asucc leq_asucc leq/asucc leq_ahead_asucc_false leq/asucc leq_asucc_false leq/fwd leq_gen_sort1 leq/fwd leq_gen_head1 leq/fwd leq_gen_sort2 leq/fwd leq_gen_head2 leq/props ahead_inj_snd leq/props leq_refl leq/props leq_eq leq/props leq_sym leq/props leq_trans leq/props leq_ahead_false_1 leq/props leq_ahead_false_2 lift1/fwd lift1_cons_tail lift1/fwd lifts1_nil lift1/fwd lifts1_cons lift/props thead_x_lift_y_y lift/props lifts_tapp lift/props lifts_inj llt/props lweight_repl llt/props llt_repl llt/props llt_trans llt/props llt_head_sx llt/props llt_head_dx llt/props llt_wf__q_ind llt/props llt_wf_ind next_plus/props next_plus_assoc next_plus/props next_plus_next next_plus/props next_plus_lt nf2/arity arity_nf2_inv_all nf2/fwd nf2_gen_lref nf2/fwd nf2_gen_abst nf2/fwd nf2_gen_cast nf2/fwd nf2_gen_beta nf2/fwd nf2_gen_flat nf2/fwd nf2_gen__nf2_gen_aux nf2/fwd nf2_gen_abbr nf2/fwd nf2_gen_void nf2/props nfs2_tapp nf2/props nf2_appls_lref pc1/props pc1_pr0_r pc1/props pc1_pr0_x pc1/props pc1_refl pc1/props pc1_pr0_u pc1/props pc1_s pc1/props pc1_head_1 pc1/props pc1_head_2 pc1/props pc1_t pc1/props pc1_pr0_u2 pc1/props pc1_head pc3/dec pc3_dec pc3/dec pc3_abst_dec pc3/fsubst0 pc3_pr2_fsubst0 pc3/fsubst0 pc3_pr2_fsubst0_back pc3/fsubst0 pc3_fsubst0 pc3/fwd pc3_gen_not_abst pc3/fwd pc3_gen_lift_abst pc3/nf2 pc3_nf2 pc3/nf2 pc3_nf2_unfold pc3/pc1 pc3_pc1 pc3/props pc3_pr0_pr2_t pc3/props pc3_pr2_pr2_t pc3/props pc3_pr2_pr3_t pc3/props pc3_pr3_pc3_t pc3/props pc3_eta pc3/subst1 pc3_gen_cabbr pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux pc3/wcpr0 pc3_wcpr0_t pc3/wcpr0 pc3_wcpr0 pr0/fwd pr0_gen_void pr0/dec nf0_dec pr0/subst1 pr0_subst1_back pr0/subst1 pr0_subst1_fwd pr1/pr1 pr1_strip pr1/pr1 pr1_confluence pr1/props pr1_pr0 pr1/props pr1_t pr1/props pr1_head_1 pr1/props pr1_head_2 pr1/props pr1_comp pr1/props pr1_eta pr2/fwd pr2_gen_void pr2/subst1 pr2_gen_cabbr pr3/fwd pr3_gen_void pr3/pr1 pr3_pr1 pr3/props pr3_eta pr3/subst1 pr3_gen_cabbr sn3/props sns3_lifts sty0/fwd sty0_gen_sort sty0/fwd sty0_gen_lref sty0/fwd sty0_gen_bind sty0/fwd sty0_gen_appl sty0/fwd sty0_gen_cast sty0/props sty0_lift sty0/props sty0_correct sty1/cnt sty1_cnt sty1/props sty1_trans sty1/props sty1_bind sty1/props sty1_appl sty1/props sty1_lift sty1/props sty1_correct sty1/props sty1_abbr sty1/props sty1_cast2 subst/fwd subst_sort subst/fwd subst_lref_lt subst/fwd subst_lref_eq subst/fwd subst_lref_gt subst/fwd subst_head subst/props subst_lift_SO subst/props subst_subst0 T/dec binder_dec T/dec abst_dec tlist/props tslt_wf__q_ind tlist/props tslt_wf_ind tlist/props theads_tapp tlist/props tcons_tapp_ex tlist/props tlist_ind_rev ty3/arity ty3_arity ty3/arity_props ty3_predicative ty3/arity_props ty3_repellent ty3/arity_props ty3_acyclic ty3/arity_props ty3_sn3 ty3/dec ty3_inference ty3/fsubst0 ty3_fsubst0 ty3/fsubst0 ty3_csubst0 ty3/fsubst0 ty3_subst0 ty3/fwd ty3_gen_sort ty3/fwd ty3_gen_lref ty3/fwd ty3_gen_bind ty3/fwd ty3_gen_appl ty3/fwd ty3_gen_cast ty3/fwd tys3_gen_nil ty3/fwd tys3_gen_cons ty3/fwd_nf2 ty3_gen_appl_nf2 ty3/fwd_nf2 ty3_inv_lref_nf2_pc3 ty3/fwd_nf2 ty3_inv_lref_nf2 ty3/fwd_nf2 ty3_inv_appls_lref_nf2 ty3/fwd_nf2 ty3_inv_lref_lref_nf2 ty3/nf2 ty3_nf2_inv_abst_premise_csort ty3/nf2 ty3_nf2_inv_all ty3/nf2 ty3_nf2_inv_sort ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux ty3/nf2 ty3_nf2_inv_abst ty3/pr3 ty3_sred_wcpr0_pr0 ty3/pr3 ty3_sred_pr0 ty3/pr3 ty3_sred_pr1 ty3/pr3 ty3_sred_pr2 ty3/pr3 ty3_sred_pr3 ty3/pr3_props ty3_cred_pr2 ty3/pr3_props ty3_cred_pr3 ty3/pr3_props ty3_gen_lift ty3/pr3_props ty3_tred ty3/pr3_props ty3_sconv_pc3 ty3/pr3_props ty3_sred_back ty3/pr3_props ty3_sconv ty3/props ty3_lift ty3/props ty3_correct ty3/props ty3_unique ty3/props ty3_gen_abst_abst ty3/props ty3_typecheck ty3/props ty3_getl_subst0 ty3/sty0 ty3_sty0 ty3/subst1 ty3_gen_cabbr ty3/subst1 ty3_gen_cvoid wf3/clear wf3_clear_conf wf3/clear clear_wf3_trans wf3/fwd wf3_gen_sort1 wf3/fwd wf3_gen_bind1 wf3/fwd wf3_gen_flat1 wf3/fwd wf3_gen_head2 wf3/getl wf3_getl_conf wf3/getl getl_wf3_trans wf3/props wf3_mono wf3/props wf3_total wf3/props ty3_shift1 wf3/props wf3_idem wf3/props wf3_ty3 wf3/ty3 wf3_pr2_conf wf3/ty3 wf3_pr3_conf wf3/ty3 wf3_pc3_conf wf3/ty3 wf3_ty3_conf # check ######################################################################