1 # new ########################################################################
4 r_arith2 r_arith3 r_arith4 r_arith5 r_arith6 r_arith7
6 cle_r cle_head cle_trans_head cle_flt_trans
10 # waiting ####################################################################
12 aplus/props aplus_reg_r
13 aplus/props aplus_assoc
14 aplus/props aplus_asucc
15 aplus/props aplus_sort_O_S_simpl
16 aplus/props aplus_sort_S_S_simpl
17 aplus/props aplus_asort_O_simpl
18 aplus/props aplus_asort_le_simpl
19 aplus/props aplus_asort_simpl
20 aplus/props aplus_ahead_simpl
21 aplus/props aplus_asucc_false
23 aprem/fwd aprem_gen_sort
24 aprem/fwd aprem_gen_head_O
25 aprem/fwd aprem_gen_head_S
26 aprem/props aprem_repl
27 aprem/props aprem_asucc
28 arity/aprem arity_aprem
29 arity/cimp arity_cimp_conf
30 arity/fwd arity_gen_sort
31 arity/fwd arity_gen_lref
32 arity/fwd arity_gen_bind
33 arity/fwd arity_gen_abst
34 arity/fwd arity_gen_appl
35 arity/fwd arity_gen_cast
36 arity/fwd arity_gen_appls
37 arity/fwd arity_gen_lift
38 arity/lift1 arity_lift1
39 arity/pr3 arity_sred_wcpr0_pr0
40 arity/pr3 arity_sred_wcpr0_pr1
41 arity/pr3 arity_sred_pr2
42 arity/pr3 arity_sred_pr3
44 arity/props arity_lift
45 arity/props arity_mono
46 arity/props arity_repellent
47 arity/props arity_appls_cast
48 arity/props arity_appls_abbr
49 arity/props arity_appls_bind
50 arity/subst0 arity_gen_cvoid_subst0
51 arity/subst0 arity_gen_cvoid
52 arity/subst0 arity_fsubst0
53 arity/subst0 arity_subst0
54 asucc/fwd asucc_gen_sort
55 asucc/fwd asucc_gen_head
59 csuba/arity csuba_arity
60 csuba/arity csuba_arity_rev
61 csuba/arity arity_appls_appl
62 csuba/clear csuba_clear_conf
63 csuba/clear csuba_clear_trans
64 csuba/drop csuba_drop_abbr
65 csuba/drop csuba_drop_abst
66 csuba/drop csuba_drop_abst_rev
67 csuba/drop csuba_drop_abbr_rev
68 csuba/fwd csuba_gen_abbr
69 csuba/fwd csuba_gen_void
70 csuba/fwd csuba_gen_abst
71 csuba/fwd csuba_gen_flat
72 csuba/fwd csuba_gen_bind
73 csuba/fwd csuba_gen_abst_rev
74 csuba/fwd csuba_gen_void_rev
75 csuba/fwd csuba_gen_abbr_rev
76 csuba/fwd csuba_gen_flat_rev
77 csuba/fwd csuba_gen_bind_rev
78 csuba/getl csuba_getl_abbr
79 csuba/getl csuba_getl_abst
80 csuba/getl csuba_getl_abst_rev
81 csuba/getl csuba_getl_abbr_rev
82 csuba/props csuba_refl
84 csubc/arity csubc_arity_conf
85 csubc/arity csubc_arity_trans
86 csubc/drop1 drop1_csubc_trans
87 csubc/drop drop_csubc_trans
89 csubt/csuba csubt_csuba
90 csubt/fwd csubt_gen_abbr
91 csubt/fwd csubt_gen_abst
93 csubv/clear csubv_clear_conf
94 csubv/clear csubv_clear_conf_void
95 csubv/drop csubv_drop_conf
96 csubv/getl csubv_getl_conf
97 csubv/getl csubv_getl_conf_void
98 csubv/props csubv_bind_same
99 csubv/props csubv_refl
100 drop1/props drop1_cons_tail
101 ex0/props aplus_gz_le
102 ex0/props aplus_gz_ge
103 ex0/props next_plus_gz
106 ex1/props ex1__leq_sort_SS
114 leq/asucc leq_ahead_asucc_false
115 leq/asucc leq_asucc_false
116 leq/fwd leq_gen_sort1
117 leq/fwd leq_gen_head1
118 leq/fwd leq_gen_sort2
119 leq/fwd leq_gen_head2
120 leq/props ahead_inj_snd
125 leq/props leq_ahead_false_1
126 leq/props leq_ahead_false_2
127 lift1/fwd lift1_cons_tail
128 lift/props lifts_tapp
129 llt/props lweight_repl
132 llt/props llt_head_sx
133 llt/props llt_head_dx
134 llt/props llt_wf__q_ind
136 next_plus/props next_plus_assoc
137 next_plus/props next_plus_next
138 next_plus/props next_plus_lt
139 nf2/arity arity_nf2_inv_all
145 nf2/fwd nf2_gen__nf2_gen_aux
149 nf2/props nf2_appls_lref
163 pc3/fwd pc3_gen_not_abst
164 pc3/fwd pc3_gen_lift_abst
166 pc3/nf2 pc3_nf2_unfold
168 pc3/props pc3_pr2_pr2_t
169 pc3/props pc3_pr2_pr3_t
170 pc3/props pc3_pr3_pc3_t
184 subst/fwd subst_lref_lt
185 subst/fwd subst_lref_eq
186 subst/fwd subst_lref_gt
188 subst/props subst_lift_SO
189 subst/props subst_subst0
192 tlist/props tslt_wf__q_ind
193 tlist/props tslt_wf_ind
194 tlist/props theads_tapp
195 tlist/props tcons_tapp_ex
196 tlist/props tlist_ind_rev
198 ty3/arity_props ty3_predicative
199 ty3/arity_props ty3_repellent
200 ty3/arity_props ty3_acyclic
201 ty3/dec ty3_inference
203 ty3/fwd tys3_gen_cons
204 ty3/fwd_nf2 ty3_gen_appl_nf2
205 ty3/fwd_nf2 ty3_inv_lref_nf2_pc3
206 ty3/fwd_nf2 ty3_inv_lref_nf2
207 ty3/fwd_nf2 ty3_inv_appls_lref_nf2
208 ty3/fwd_nf2 ty3_inv_lref_lref_nf2
209 ty3/nf2 ty3_nf2_inv_abst_premise_csort
210 ty3/nf2 ty3_nf2_inv_all
211 ty3/nf2 ty3_nf2_inv_sort
212 ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux
213 ty3/nf2 ty3_nf2_inv_abst
214 ty3/pr3 ty3_sred_wcpr0_pr0
219 ty3/pr3_props ty3_cred_pr2
220 ty3/pr3_props ty3_cred_pr3
221 ty3/pr3_props ty3_gen_lift
222 ty3/pr3_props ty3_tred
223 ty3/pr3_props ty3_sconv_pc3
224 ty3/pr3_props ty3_sred_back
225 ty3/pr3_props ty3_sconv
226 ty3/props ty3_gen_abst_abst
228 ty3/subst1 ty3_gen_cvoid
230 wf3/clear wf3_clear_conf
231 wf3/clear clear_wf3_trans
232 wf3/fwd wf3_gen_sort1
233 wf3/fwd wf3_gen_bind1
234 wf3/fwd wf3_gen_flat1
235 wf3/fwd wf3_gen_head2
236 wf3/getl wf3_getl_conf
237 wf3/getl getl_wf3_trans
248 # check ######################################################################