]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambda_delta/Basic_2/Basic_1.txt
theory of ltpss completed!
[helm.git] / 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/fwd pr2_gen_void
272 pr2/props pr2_ctail
273
274
275 # waiting ####################################################################
276
277 pr3/fwd pr3_gen_sort
278 pr3/fwd pr3_gen_abst
279 pr3/fwd pr3_gen_cast
280 pr3/fwd pr3_gen_lift
281 pr3/fwd pr3_gen_lref
282 pr3/fwd pr3_gen_void
283 pr3/fwd pr3_gen_abbr
284 pr3/fwd pr3_gen_appl
285 pr3/fwd pr3_gen_bind
286 pr3/iso pr3_iso_appls_abbr
287 pr3/iso pr3_iso_appls_cast
288 pr3/iso pr3_iso_appl_bind
289 pr3/iso pr3_iso_appls_appl_bind
290 pr3/iso pr3_iso_appls_bind
291 pr3/iso pr3_iso_beta
292 pr3/iso pr3_iso_appls_beta
293 pr3/pr1 pr3_pr1
294 pr3/pr3 pr3_strip
295 pr3/pr3 pr3_confluence
296 pr3/props clear_pr3_trans
297 pr3/props pr3_pr2
298 pr3/props pr3_t
299 pr3/props pr3_thin_dx
300 pr3/props pr3_head_1
301 pr3/props pr3_head_2
302 pr3/props pr3_head_21
303 pr3/props pr3_head_12
304 pr3/props pr3_cflat
305 pr3/props pr3_flat
306 pr3/props pr3_pr0_pr2_t
307 pr3/props pr3_pr2_pr2_t
308 pr3/props pr3_pr2_pr3_t
309 pr3/props pr3_pr3_pr3_t
310 pr3/props pr3_lift
311 pr3/props pr3_eta
312 pr3/subst1 pr3_subst1
313 pr3/subst1 pr3_gen_cabbr
314 pr3/wcpr0 pr3_wcpr0_t
315 sc3/arity sc3_arity_csubc
316 sc3/arity sc3_arity
317 sc3/props sc3_arity_gen
318 sc3/props sc3_repl
319 sc3/props sc3_lift
320 sc3/props sc3_lift1
321 sc3/props sc3_abbr
322 sc3/props sc3_cast
323 sc3/props sc3_props__sc3_sn3_abst
324 sc3/props sc3_sn3
325 sc3/props sc3_abst
326 sc3/props sc3_bind
327 sc3/props sc3_appl
328 sn3/fwd sn3_gen_bind
329 sn3/fwd sn3_gen_flat
330 sn3/fwd sn3_gen_head
331 sn3/fwd sn3_gen_cflat
332 sn3/fwd sn3_gen_lift
333 sn3/lift1 sns3_lifts1
334 sn3/nf2 sn3_nf2
335 sn3/nf2 nf2_sn3
336 sn3/props sn3_pr3_trans
337 sn3/props sn3_pr2_intro
338 sn3/props sn3_cast
339 sn3/props sn3_cflat
340 sn3/props sn3_shift
341 sn3/props sn3_change
342 sn3/props sn3_gen_def
343 sn3/props sn3_cdelta
344 sn3/props sn3_cpr3_trans
345 sn3/props sn3_bind
346 sn3/props sn3_beta
347 sn3/props sn3_appl_lref
348 sn3/props sn3_appl_abbr
349 sn3/props sn3_appl_cast
350 sn3/props sn3_appl_bind
351 sn3/props sn3_appl_appl
352 sn3/props sn3_appl_beta
353 sn3/props sn3_appl_appls
354 sn3/props sn3_appls_lref
355 sn3/props sn3_appls_cast
356 sn3/props sn3_appls_bind
357 sn3/props sn3_appls_beta
358 sn3/props sn3_lift
359 sn3/props sn3_abbr
360 sn3/props sn3_appls_abbr
361 sn3/props sns3_lifts
362 sty0/fwd sty0_gen_sort
363 sty0/fwd sty0_gen_lref
364 sty0/fwd sty0_gen_bind
365 sty0/fwd sty0_gen_appl
366 sty0/fwd sty0_gen_cast
367 sty0/props sty0_lift
368 sty0/props sty0_correct
369 sty1/cnt sty1_cnt
370 sty1/props sty1_trans
371 sty1/props sty1_bind
372 sty1/props sty1_appl
373 sty1/props sty1_lift
374 sty1/props sty1_correct
375 sty1/props sty1_abbr
376 sty1/props sty1_cast2
377 subst0/dec dnf_dec2
378 subst0/dec dnf_dec
379 subst1/props subst1_ex
380 subst/fwd subst_sort
381 subst/fwd subst_lref_lt
382 subst/fwd subst_lref_eq
383 subst/fwd subst_lref_gt
384 subst/fwd subst_head
385 subst/props subst_lift_SO
386 subst/props subst_subst0
387 T/dec terms_props__bind_dec
388 T/dec bind_dec_not
389 T/dec terms_props__flat_dec
390 T/dec terms_props__kind_dec
391 T/dec term_dec
392 T/dec binder_dec
393 T/dec abst_dec
394 tlist/props tslt_wf__q_ind
395 tlist/props tslt_wf_ind
396 tlist/props theads_tapp
397 tlist/props tcons_tapp_ex
398 tlist/props tlist_ind_rev
399 T/props not_abbr_abst
400 T/props not_void_abst
401 T/props not_abbr_void
402 T/props not_abst_void
403 T/props thead_x_y_y
404 T/props tweight_lt
405 ty3/arity ty3_arity
406 ty3/arity_props ty3_predicative
407 ty3/arity_props ty3_repellent
408 ty3/arity_props ty3_acyclic
409 ty3/arity_props ty3_sn3
410 ty3/dec ty3_inference
411 ty3/fsubst0 ty3_fsubst0
412 ty3/fsubst0 ty3_csubst0
413 ty3/fsubst0 ty3_subst0
414 ty3/fwd ty3_gen_sort
415 ty3/fwd ty3_gen_lref
416 ty3/fwd ty3_gen_bind
417 ty3/fwd ty3_gen_appl
418 ty3/fwd ty3_gen_cast
419 ty3/fwd tys3_gen_nil
420 ty3/fwd tys3_gen_cons
421 ty3/fwd_nf2 ty3_gen_appl_nf2
422 ty3/fwd_nf2 ty3_inv_lref_nf2_pc3
423 ty3/fwd_nf2 ty3_inv_lref_nf2
424 ty3/fwd_nf2 ty3_inv_appls_lref_nf2
425 ty3/fwd_nf2 ty3_inv_lref_lref_nf2
426 ty3/nf2 ty3_nf2_inv_abst_premise_csort
427 ty3/nf2 ty3_nf2_inv_all
428 ty3/nf2 ty3_nf2_inv_sort
429 ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux
430 ty3/nf2 ty3_nf2_inv_abst
431 ty3/pr3 ty3_sred_wcpr0_pr0
432 ty3/pr3 ty3_sred_pr0
433 ty3/pr3 ty3_sred_pr1
434 ty3/pr3 ty3_sred_pr2
435 ty3/pr3 ty3_sred_pr3
436 ty3/pr3_props ty3_cred_pr2
437 ty3/pr3_props ty3_cred_pr3
438 ty3/pr3_props ty3_gen_lift
439 ty3/pr3_props ty3_tred
440 ty3/pr3_props ty3_sconv_pc3
441 ty3/pr3_props ty3_sred_back
442 ty3/pr3_props ty3_sconv
443 ty3/props ty3_lift
444 ty3/props ty3_correct
445 ty3/props ty3_unique
446 ty3/props ty3_gen_abst_abst
447 ty3/props ty3_typecheck
448 ty3/props ty3_getl_subst0
449 ty3/sty0 ty3_sty0
450 ty3/subst1 ty3_gen_cabbr
451 ty3/subst1 ty3_gen_cvoid
452 wf3/clear wf3_clear_conf
453 wf3/clear clear_wf3_trans
454 wf3/fwd wf3_gen_sort1
455 wf3/fwd wf3_gen_bind1
456 wf3/fwd wf3_gen_flat1
457 wf3/fwd wf3_gen_head2
458 wf3/getl wf3_getl_conf
459 wf3/getl getl_wf3_trans
460 wf3/props wf3_mono
461 wf3/props wf3_total
462 wf3/props ty3_shift1
463 wf3/props wf3_idem
464 wf3/props wf3_ty3
465 wf3/ty3 wf3_pr2_conf
466 wf3/ty3 wf3_pr3_conf
467 wf3/ty3 wf3_pc3_conf
468 wf3/ty3 wf3_ty3_conf