--- /dev/null
+# 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
+
+# check ######################################################################
+
+clen/getl getl_ctail_clen
+clen/getl getl_gen_tail
+cnt/props cnt_lift
+C/props clt_cong
+C/props clt_head
+C/props clt_wf__q_ind
+C/props clt_wf_ind
+C/props chead_ctail
+C/props clt_thead
+C/props c_tail_ind
+
+# waiting ####################################################################
+
+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/clear csubc_clear_conf
+csubc/csuba csubc_csuba
+csubc/drop1 drop1_csubc_trans
+csubc/drop1 csubc_drop1_conf_rev
+csubc/drop csubc_drop_conf_O
+csubc/drop drop_csubc_trans
+csubc/drop csubc_drop_conf_rev
+csubc/fwd csubc_gen_sort_l
+csubc/fwd csubc_gen_head_l
+csubc/fwd csubc_gen_sort_r
+csubc/fwd csubc_gen_head_r
+csubc/getl csubc_getl_conf
+csubc/props csubc_refl
+csubst0/clear csubst0_clear_O
+csubst0/clear csubst0_clear_O_back
+csubst0/clear csubst0_clear_S
+csubst0/clear csubst0_clear_trans
+csubst0/drop csubst0_drop_gt
+csubst0/drop csubst0_drop_gt_back
+csubst0/drop csubst0_drop_lt
+csubst0/drop csubst0_drop_eq
+csubst0/drop csubst0_drop_eq_back
+csubst0/drop csubst0_drop_lt_back
+csubst0/fwd csubst0_gen_sort
+csubst0/fwd csubst0_gen_head
+csubst0/fwd csubst0_gen_S_bind_2
+csubst0/getl csubst0_getl_ge
+csubst0/getl csubst0_getl_lt
+csubst0/getl csubst0_getl_ge_back
+csubst0/getl csubst0_getl_lt_back
+csubst0/props csubst0_snd_bind
+csubst0/props csubst0_fst_bind
+csubst0/props csubst0_both_bind
+csubst1/fwd csubst1_gen_head
+csubst1/getl csubst1_getl_ge
+csubst1/getl csubst1_getl_lt
+csubst1/getl csubst1_getl_ge_back
+csubst1/getl getl_csubst1
+csubst1/props csubst1_head
+csubst1/props csubst1_bind
+csubst1/props csubst1_flat
+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/fwd drop1_gen_pnil
+drop1/fwd drop1_gen_pcons
+drop1/getl drop1_getl_trans
+drop1/props drop1_skip_bind
+drop1/props drop1_cons_tail
+drop1/props drop1_trans
+
+drop/props drop_ctail
+
+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
+
+# check ######################################################################
+
+flt/props flt_thead_sx
+flt/props flt_thead_dx
+flt/props flt_shift
+flt/props flt_arith0
+flt/props flt_arith1
+flt/props flt_arith2
+flt/props flt_trans
+flt/props flt_wf__q_ind
+flt/props flt_wf_ind
+fsubst0/fwd fsubst0_gen_base
+getl/clear clear_getl_trans
+getl/clear getl_clear_trans
+getl/clear getl_clear_bind
+getl/clear getl_clear_conf
+getl/dec getl_dec
+getl/drop getl_drop
+getl/drop getl_drop_conf_lt
+getl/drop getl_drop_conf_ge
+getl/drop getl_conf_ge_drop
+getl/drop getl_drop_conf_rev
+getl/drop drop_getl_trans_lt
+getl/drop drop_getl_trans_le
+getl/drop drop_getl_trans_ge
+getl/drop getl_drop_trans
+getl/flt getl_flt
+getl/fwd getl_gen_all
+getl/fwd getl_gen_sort
+getl/fwd getl_gen_O
+getl/fwd getl_gen_S
+getl/fwd getl_gen_2
+getl/fwd getl_gen_flat
+getl/fwd getl_gen_bind
+getl/getl getl_conf_le
+getl/getl getl_trans
+getl/props getl_refl
+getl/props getl_head
+getl/props getl_flat
+getl/props getl_ctail
+getl/props getl_mono
+iso/fwd iso_gen_sort
+iso/fwd iso_gen_lref
+iso/fwd iso_gen_head
+iso/fwd iso_flats_lref_bind_false
+iso/fwd iso_flats_flat_bind_false
+iso/props iso_refl
+iso/props iso_trans
+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_sort
+lift1/fwd lift1_lref
+lift1/fwd lift1_bind
+lift1/fwd lift1_flat
+lift1/fwd lift1_cons_tail
+lift1/fwd lifts1_flat
+lift1/fwd lifts1_nil
+lift1/fwd lifts1_cons
+lift1/props lift1_lift1
+lift1/props lift1_xhg
+lift1/props lifts1_xhg
+lift1/props lift1_free
+lift/fwd lift_sort
+lift/fwd lift_lref_lt
+lift/fwd lift_lref_ge
+lift/fwd lift_head
+lift/fwd lift_bind
+lift/fwd lift_flat
+lift/fwd lift_gen_sort
+lift/fwd lift_gen_lref
+lift/fwd lift_gen_lref_lt
+lift/fwd lift_gen_lref_false
+lift/fwd lift_gen_lref_ge
+lift/fwd lift_gen_head
+lift/fwd lift_gen_bind
+lift/fwd lift_gen_flat
+lift/props thead_x_lift_y_y
+lift/props lift_r
+lift/props lift_lref_gt
+lift/props lifts_tapp
+lift/props lift_inj
+lift/props lift_gen_lift
+lift/props lifts_inj
+lift/props lift_free
+lift/props lift_d
+lift/tlt lift_weight_map
+lift/tlt lift_weight
+lift/tlt lift_weight_add
+lift/tlt lift_weight_add_O
+lift/tlt lift_tlt_dx
+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/dec nf2_dec
+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/iso nf2_iso_appls_lref
+nf2/lift1 nf2_lift1
+nf2/pr3 nf2_pr3_unfold
+nf2/pr3 nf2_pr3_confluence
+nf2/props nf2_sort
+nf2/props nf2_csort_lref
+nf2/props nf2_abst
+nf2/props nf2_abst_shift
+nf2/props nfs2_tapp
+nf2/props nf2_appls_lref
+nf2/props nf2_appl_lref
+nf2/props nf2_lref_abst
+nf2/props nf2_lift
+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_sort
+pc3/fwd pc3_gen_abst
+pc3/fwd pc3_gen_abst_shift
+pc3/fwd pc3_gen_lift
+pc3/fwd pc3_gen_not_abst
+pc3/fwd pc3_gen_lift_abst
+pc3/fwd pc3_gen_sort_abst
+pc3/left pc3_ind_left__pc3_left_pr3
+pc3/left pc3_ind_left__pc3_left_trans
+pc3/left pc3_ind_left__pc3_left_sym
+pc3/left pc3_ind_left__pc3_left_pc3
+pc3/left pc3_ind_left__pc3_pc3_left
+pc3/left pc3_ind_left
+pc3/nf2 pc3_nf2
+pc3/nf2 pc3_nf2_unfold
+pc3/pc1 pc3_pc1
+pc3/props clear_pc3_trans
+pc3/props pc3_pr2_r
+pc3/props pc3_pr2_x
+pc3/props pc3_pr3_r
+pc3/props pc3_pr3_x
+pc3/props pc3_pr3_t
+pc3/props pc3_refl
+pc3/props pc3_s
+pc3/props pc3_thin_dx
+pc3/props pc3_head_1
+pc3/props pc3_head_2
+pc3/props pc3_pr2_u
+pc3/props pc3_t
+pc3/props pc3_pr2_u2
+pc3/props pc3_pr3_conf
+pc3/props pc3_head_12
+pc3/props pc3_head_21
+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_lift
+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/dec nf0_dec
+pr0/fwd pr0_gen_sort
+pr0/fwd pr0_gen_lref
+pr0/fwd pr0_gen_abst
+pr0/fwd pr0_gen_appl
+pr0/fwd pr0_gen_cast
+pr0/fwd pr0_gen_abbr
+pr0/fwd pr0_gen_void
+pr0/fwd pr0_gen_lift
+pr0/pr0 pr0_confluence__pr0_cong_upsilon_refl
+pr0/pr0 pr0_confluence__pr0_cong_upsilon_cong
+pr0/pr0 pr0_confluence__pr0_cong_upsilon_delta
+pr0/pr0 pr0_confluence__pr0_cong_upsilon_zeta
+pr0/pr0 pr0_confluence__pr0_cong_delta
+pr0/pr0 pr0_confluence__pr0_upsilon_upsilon
+pr0/pr0 pr0_confluence__pr0_delta_delta
+pr0/pr0 pr0_confluence__pr0_delta_tau
+pr0/pr0 pr0_confluence
+pr0/props pr0_lift
+pr0/props pr0_subst0_back
+pr0/props pr0_subst0_fwd
+pr0/props pr0_subst0
+pr0/subst1 pr0_delta1
+pr0/subst1 pr0_subst1_back
+pr0/subst1 pr0_subst1_fwd
+pr0/subst1 pr0_subst1
+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/clen pr2_gen_ctail
+pr2/clen pr2_gen_cbind
+pr2/clen pr2_gen_cflat
+pr2/fwd pr2_gen_sort
+pr2/fwd pr2_gen_lref
+pr2/fwd pr2_gen_abst
+pr2/fwd pr2_gen_cast
+pr2/fwd pr2_gen_csort
+pr2/fwd pr2_gen_appl
+pr2/fwd pr2_gen_abbr
+pr2/fwd pr2_gen_void
+pr2/fwd pr2_gen_lift
+pr2/pr2 pr2_confluence__pr2_free_free
+pr2/pr2 pr2_confluence__pr2_free_delta
+pr2/pr2 pr2_confluence__pr2_delta_delta
+pr2/pr2 pr2_confluence
+pr2/props pr2_thin_dx
+pr2/props pr2_head_1
+pr2/props pr2_head_2
+pr2/props clear_pr2_trans
+pr2/props pr2_cflat
+pr2/props pr2_ctail
+pr2/props pr2_change
+pr2/props pr2_lift
+pr2/subst1 pr2_delta1
+pr2/subst1 pr2_subst1
+pr2/subst1 pr2_gen_cabbr
+pr3/fwd pr3_gen_sort
+pr3/fwd pr3_gen_abst
+pr3/fwd pr3_gen_cast
+pr3/fwd pr3_gen_lift
+pr3/fwd pr3_gen_lref
+pr3/fwd pr3_gen_void
+pr3/fwd pr3_gen_abbr
+pr3/fwd pr3_gen_appl
+pr3/fwd pr3_gen_bind
+pr3/iso pr3_iso_appls_abbr
+pr3/iso pr3_iso_appls_cast
+pr3/iso pr3_iso_appl_bind
+pr3/iso pr3_iso_appls_appl_bind
+pr3/iso pr3_iso_appls_bind
+pr3/iso pr3_iso_beta
+pr3/iso pr3_iso_appls_beta
+pr3/pr1 pr3_pr1
+pr3/pr3 pr3_strip
+pr3/pr3 pr3_confluence
+pr3/props clear_pr3_trans
+pr3/props pr3_pr2
+pr3/props pr3_t
+pr3/props pr3_thin_dx
+pr3/props pr3_head_1
+pr3/props pr3_head_2
+pr3/props pr3_head_21
+pr3/props pr3_head_12
+pr3/props pr3_cflat
+pr3/props pr3_flat
+pr3/props pr3_pr0_pr2_t
+pr3/props pr3_pr2_pr2_t
+pr3/props pr3_pr2_pr3_t
+pr3/props pr3_pr3_pr3_t
+pr3/props pr3_lift
+pr3/props pr3_eta
+pr3/subst1 pr3_subst1
+pr3/subst1 pr3_gen_cabbr
+pr3/wcpr0 pr3_wcpr0_t
+sc3/arity sc3_arity_csubc
+sc3/arity sc3_arity
+sc3/props sc3_arity_gen
+sc3/props sc3_repl
+sc3/props sc3_lift
+sc3/props sc3_lift1
+sc3/props sc3_abbr
+sc3/props sc3_cast
+sc3/props sc3_props__sc3_sn3_abst
+sc3/props sc3_sn3
+sc3/props sc3_abst
+sc3/props sc3_bind
+sc3/props sc3_appl
+sn3/fwd sn3_gen_bind
+sn3/fwd sn3_gen_flat
+sn3/fwd sn3_gen_head
+sn3/fwd sn3_gen_cflat
+sn3/fwd sn3_gen_lift
+sn3/lift1 sns3_lifts1
+sn3/nf2 sn3_nf2
+sn3/nf2 nf2_sn3
+sn3/props sn3_pr3_trans
+sn3/props sn3_pr2_intro
+sn3/props sn3_cast
+sn3/props sn3_cflat
+sn3/props sn3_shift
+sn3/props sn3_change
+sn3/props sn3_gen_def
+sn3/props sn3_cdelta
+sn3/props sn3_cpr3_trans
+sn3/props sn3_bind
+sn3/props sn3_beta
+sn3/props sn3_appl_lref
+sn3/props sn3_appl_abbr
+sn3/props sn3_appl_cast
+sn3/props sn3_appl_bind
+sn3/props sn3_appl_appl
+sn3/props sn3_appl_beta
+sn3/props sn3_appl_appls
+sn3/props sn3_appls_lref
+sn3/props sn3_appls_cast
+sn3/props sn3_appls_bind
+sn3/props sn3_appls_beta
+sn3/props sn3_lift
+sn3/props sn3_abbr
+sn3/props sn3_appls_abbr
+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
+subst0/dec dnf_dec2
+subst0/dec dnf_dec
+subst0/fwd subst0_gen_sort
+subst0/fwd subst0_gen_lref
+subst0/fwd subst0_gen_head
+subst0/fwd subst0_gen_lift_lt
+subst0/fwd subst0_gen_lift_false
+subst0/fwd subst0_gen_lift_ge
+subst0/props subst0_refl
+subst0/props subst0_lift_lt
+subst0/props subst0_lift_ge
+subst0/props subst0_lift_ge_S
+subst0/props subst0_lift_ge_s
+subst0/subst0 subst0_subst0
+subst0/subst0 subst0_subst0_back
+subst0/subst0 subst0_trans
+subst0/subst0 subst0_confluence_neq
+subst0/subst0 subst0_confluence_eq
+subst0/subst0 subst0_confluence_lift
+subst0/tlt subst0_weight_le
+subst0/tlt subst0_weight_lt
+subst0/tlt subst0_tlt_head
+subst0/tlt subst0_tlt
+subst1/fwd subst1_gen_sort
+subst1/fwd subst1_gen_lref
+subst1/fwd subst1_gen_head
+subst1/fwd subst1_gen_lift_lt
+subst1/fwd subst1_gen_lift_eq
+subst1/fwd subst1_gen_lift_ge
+subst1/props subst1_head
+subst1/props subst1_lift_lt
+subst1/props subst1_lift_ge
+subst1/props subst1_ex
+subst1/props subst1_lift_S
+subst1/subst1 subst1_subst1
+subst1/subst1 subst1_subst1_back
+subst1/subst1 subst1_trans
+subst1/subst1 subst1_confluence_neq
+subst1/subst1 subst1_confluence_eq
+subst1/subst1 subst1_confluence_lift
+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 terms_props__bind_dec
+T/dec bind_dec_not
+T/dec terms_props__flat_dec
+T/dec terms_props__kind_dec
+T/dec term_dec
+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
+tlt/props wadd_le
+tlt/props wadd_lt
+tlt/props wadd_O
+tlt/props weight_le
+tlt/props weight_eq
+tlt/props weight_add_O
+tlt/props weight_add_S
+tlt/props tlt_trans
+tlt/props tlt_head_sx
+tlt/props tlt_head_dx
+tlt/props tlt_wf__q_ind
+tlt/props tlt_wf_ind
+T/props not_abbr_abst
+T/props not_void_abst
+T/props not_abbr_void
+T/props not_abst_void
+T/props thead_x_y_y
+T/props tweight_lt
+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
+wcpr0/fwd wcpr0_gen_sort
+wcpr0/fwd wcpr0_gen_head
+wcpr0/getl wcpr0_drop
+wcpr0/getl wcpr0_drop_back
+wcpr0/getl wcpr0_getl
+wcpr0/getl wcpr0_getl_back
+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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic-2/grammar/cl_weight.ma".
+
+(* SHIFT OF A CLOSURE *******************************************************)
+
+let rec shift L T on L ≝ match L with
+[ LSort ⇒ T
+| LPair L I V ⇒ shift L (𝕓{I} V. T)
+].
+
+interpretation "shift (closure)" 'Append L T = (shift L T).
+
+(* Basic properties *********************************************************)
+
+lemma tw_shift: ∀L,T. #[L, T] ≤ #[L @ T].
+#L elim L //
+#K #I #V #IHL #T
+@transitive_le [3: @IHL |2: /2/ | skip ]
+qed.
+
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic-2/grammar/lenv_weight.ma".
+
+(* WEIGHT OF A CLOSURE ******************************************************)
+
+definition cw: lenv → term → ? ≝ λL,T. #[L] + #[T].
+
+interpretation "weight (closure)" 'Weight L T = (cw L T).
+
+(* Basic properties *********************************************************)
+
+lemma cw_shift: ∀K,I,V,T. #[K. 𝕓{I} V, T] < #[K, 𝕓{I} V. T].
+normalize //
+qed.
+
+axiom cw_wf_ind: ∀R:lenv→term→Prop.
+ (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → R L1 T1) → R L2 T2) →
+ ∀L,T. R L T.
* [ suggested invocation to start formal specifications with ]
*)
-include "Ground-2/ground.ma".
+include "Ground-2/list.ma".
include "Basic-2/notation.ma".
(* BINARY ITEMS *************************************************************)
coercion item2_of_bind2: ∀I:bind2.item2 ≝ Bind on _I:bind2 to item2.
coercion item2_of_flat2: ∀I:flat2.item2 ≝ Flat on _I:flat2 to item2.
+
+(* Basic-1: removed theorems 19:
+ s_S s_plus s_plus_sym s_minus minus_s_s s_le s_lt s_inj s_inc
+ s_arith0 s_arith1
+ r_S r_plus r_plus_sym r_minus r_dis s_r r_arith0 r_arith1
+*)
include "Basic-2/grammar/lenv.ma".
-(* LENGTH *******************************************************************)
+(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
-(* the length of a local environment *)
let rec length L ≝ match L with
[ LSort ⇒ 0
| LPair L _ _ ⇒ length L + 1
include "Basic-2/grammar/term_weight.ma".
include "Basic-2/grammar/lenv.ma".
-(* WEIGHTS ******************************************************************)
+(* WEIGHT OF A LOCAL ENVIRONMENT ********************************************)
-(* the weight of a local environment *)
let rec lw L ≝ match L with
[ LSort ⇒ 0
-| LPair L _ V ⇒ lw L + #V
+| LPair L _ V ⇒ lw L + #[V]
].
interpretation "weight (local environment)" 'Weight L = (lw L).
-
-(* the weight of a closure *)
-definition cw: lenv → term → ? ≝ λL,T. #L + #T.
-
-interpretation "weight (closure)" 'Weight L T = (cw L T).
-
-axiom cw_wf_ind: ∀P:lenv→term→Prop.
- (∀L2,T2. (∀L1,T1. #[L1,T1] < #[L2,T2] → P L1 T1) → P L2 T2) →
- ∀L,T. P L T.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic-2/grammar/lenv_length.ma".
+
+(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
+
+inductive leq: lenv → nat → nat → lenv → Prop ≝
+| leq_sort: ∀d,e. leq (⋆) d e (⋆)
+| leq_OO: ∀L1,L2. leq L1 0 0 L2
+| leq_eq: ∀L1,L2,I,V,e. leq L1 0 e L2 → leq (L1. 𝕓{I} V) 0 (e + 1) (L2.𝕓{I} V)
+| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
+ leq L1 d e L2 → leq (L1. 𝕓{I1} V1) (d + 1) e (L2. 𝕓{I2} V2)
+.
+
+interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2).
+
+(* Basic properties *********************************************************)
+
+lemma leq_refl: ∀d,e,L. L [d, e] ≈ L.
+#d elim d -d
+[ #e elim e -e // #e #IHe #L elim L -L /2/
+| #d #IHd #e #L elim L -L /2/
+]
+qed.
+
+lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1.
+#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/
+qed.
+
+lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d →
+ ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2.
+
+#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/
+qed.
+
+(* Basic inversion lemmas ***************************************************)
(* *)
(**************************************************************************)
-include "Ground-2/ground.ma".
+include "Ground-2/list.ma".
(* SORT HIERARCHY ***********************************************************)
interpretation "sort (term)" 'Star k = (TSort k).
-interpretation "local reference (term)" 'Weight i = (TLRef i).
+interpretation "local reference (term)" 'LRef i = (TLRef i).
interpretation "term construction (binary)" 'SItem I T1 T2 = (TPair I T1 T2).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic-2/grammar/term.ma".
+
+(* SIMPLE (NEUTRAL) TERMS ***************************************************)
+
+inductive simple: term → Prop ≝
+ | simple_sort: ∀k. simple (⋆k)
+ | simple_lref: ∀i. simple (#i)
+ | simple_flat: ∀I,V,T. simple (𝕗{I} V. T)
+.
+
+interpretation "simple (term)" 'Simple T = (simple T).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact simple_inv_bind_aux: ∀T. 𝕊[T] → ∀J,W,U. T = 𝕓{J} W. U → False.
+#T * -T
+[ #k #J #W #U #H destruct
+| #k #J #W #U #H destruct
+| #I #V #T #J #W #U #H destruct
+]
+qed.
+
+lemma simple_inv_bind: ∀I,V,T. 𝕊[𝕓{I} V. T] → False.
+/2 width=6/ qed.
include "Basic-2/grammar/term.ma".
-(* WEIGHT *******************************************************************)
+(* WEIGHT OF A TERM *********************************************************)
-(* the weight of a term *)
let rec tw T ≝ match T with
[ TSort _ ⇒ 1
| TLRef _ ⇒ 1
interpretation "weight (term)" 'Weight T = (tw T).
-axiom tw_wf_ind: ∀P:term→Prop.
- (∀T2. (∀T1. # T1 < # T2 → P T1) → P T2) →
- ∀T. P T.
+(* Basic properties *********************************************************)
+
+axiom tw_wf_ind: ∀R:term→Prop.
+ (∀T2. (∀T1. #[T1] < #[T2] → R T1) → R T2) →
+ ∀T. R T.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Basic-2/grammar/term_simple.ma".
+
+(* HOMOMORPHIC TERMS ********************************************************)
+
+inductive thom: term → term → Prop ≝
+ | thom_sort: ∀k. thom (⋆k) (⋆k)
+ | thom_lref: ∀i. thom (#i) (#i)
+ | thom_abst: ∀V1,V2,T1,T2. thom (𝕚{Abst} V1. T1) (𝕚{Abst} V2. T2)
+ | thom_appl: ∀V1,V2,T1,T2. thom T1 T2 → 𝕊[T1] → 𝕊[T2] →
+ thom (𝕚{Appl} V1. T1) (𝕚{Appl} V2. T2)
+.
+
+interpretation "homomorphic (term)" 'napart T1 T2 = (thom T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma thom_sym: ∀T1,T2. T1 ≈ T2 → T2 ≈ T1.
+#T1 #T2 #H elim H -H T1 T2 /2/
+qed.
+
+lemma thom_refl2: ∀T1,T2. T1 ≈ T2 → T2 ≈ T2.
+#T1 #T2 #H elim H -H T1 T2 /2/
+qed.
+
+lemma thom_refl1: ∀T1,T2. T1 ≈ T2 → T1 ≈ T1.
+/3/ qed.
+
+lemma simple_thom_repl_dx: ∀T1,T2. T1 ≈ T2 → 𝕊[T1] → 𝕊[T2].
+#T1 #T2 #H elim H -H T1 T2 //
+#V1 #V2 #T1 #T2 #H
+elim (simple_inv_bind … H)
+qed.
+
+lemma simple_thom_repl_sn: ∀T1,T2. T1 ≈ T2 → 𝕊[T2] → 𝕊[T1].
+/3/ qed.
+
+(* Basic inversion lemmas ***************************************************)
NAMING CONVENTIONS FOR METAVARIABLES
+A,B : arity
+C,D : candidate of reducibility
+E,F,G : reserved: future use
H : reserved: transient premise
IH : reserved: inductive premise
I,J : item
K,L : local environment
+M,N : reserved: future use
+O : reserved: standard library
+P,Q : reserved: future use
+R : generic predicate (relation)
+S : reserved: standard library
T,U,V,W: term
X,Y,Z : reserved: transient objet denoted by a capital letter
non associative with precedence 90
for @{ 'Star $k }.
-notation "hvbox( 𝕚 { I } break (term 90 T1) . break (term 90 T) )"
+notation "hvbox( # term 90 k )"
+ non associative with precedence 90
+ for @{ 'LRef $k }.
+
+notation "hvbox( 𝕚 { I } break term 90 T1 . break term 90 T )"
non associative with precedence 90
for @{ 'SItem $I $T1 $T }.
-notation "hvbox( 𝕓 { I } break (term 90 T1) . break (term 90 T) )"
+notation "hvbox( 𝕓 { I } break term 90 T1 . break term 90 T )"
non associative with precedence 90
for @{ 'SBind $I $T1 $T }.
-notation "hvbox( 𝕗 { I } break (term 90 T1) . break (term 90 T) )"
+notation "hvbox( 𝕗 { I } break term 90 T1 . break term 90 T )"
non associative with precedence 90
for @{ 'SFlat $I $T1 $T }.
-notation "hvbox( T . break 𝕓 { I } break (term 90 T1) )"
+notation "hvbox( T . break 𝕓 { I } break term 90 T1 )"
non associative with precedence 89
for @{ 'DBind $T $I $T1 }.
-(*
-notation "hvbox( | L | )"
- non associative with precedence 70
- for @{ 'Length $L }.
-*)
-notation "hvbox( # term 90 x )"
+
+notation "hvbox( # [ x ] )"
non associative with precedence 90
for @{ 'Weight $x }.
non associative with precedence 90
for @{ 'Weight $x $y }.
-(* Substitution *************************************************************)
+notation "hvbox( 𝕊 [ T ] )"
+ non associative with precedence 45
+ for @{ 'Simple $T }.
notation "hvbox( T1 break [ d , break e ] ≈ break T2 )"
non associative with precedence 45
for @{ 'Eq $T1 $d $e $T2 }.
+(* Substitution *************************************************************)
+
notation "hvbox( ↑ [ d , break e ] break T1 ≡ break T2 )"
non associative with precedence 45
for @{ 'RLift $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'PRed $T1 $T2 }.
-notation "hvbox( L ⊢ break (term 90 T1) ⇒ break T2 )"
+notation "hvbox( L ⊢ break term 90 T1 ⇒ break T2 )"
non associative with precedence 45
for @{ 'PRed $L $T1 $T2 }.
(* *)
(**************************************************************************)
+include "Basic-2/grammar/cl_shift.ma".
include "Basic-2/reduction/tpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
qed.
(* Basic inversion lemmas ***************************************************)
+
+lemma cpr_inv_lsort: ∀T1,T2. ⋆ ⊢ T1 ⇒ T2 → T1 ⇒ T2.
+#T1 #T2 * #T #HT normalize #HT2
+<(tps_inv_refl0 … HT2) -HT2 //
+qed.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cpr_shift_fwd: ∀L,T1,T2. L ⊢ T1 ⇒ T2 → L @ T1 ⇒ L @ T2.
+#L elim L -L
+[ /2/
+| normalize /3/
+].
+qed.
(* Basic inversion lemmas ***************************************************)
-lemma lcpr_inv_item1_aux: ∀L1,L2. L1 ⊢ ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
- ∃∃K2,V2. K1 ⊢ ⇒ K2 & K2 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+fact lcpr_inv_item1_aux: ∀L1,L2. L1 ⊢ ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
+ ∃∃K2,V2. K1 ⊢ ⇒ K2 & K2 ⊢ V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
#L1 #L2 * -L1 L2
[ #K1 #I #V1 #H destruct
| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
(* Basic inversion lemmas ***************************************************)
-lemma ltpr_inv_item1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
- ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
+fact ltpr_inv_item1_aux: ∀L1,L2. L1 ⇒ L2 → ∀K1,I,V1. L1 = K1. 𝕓{I} V1 →
+ ∃∃K2,V2. K1 ⇒ K2 & V1 ⇒ V2 & L2 = K2. 𝕓{I} V2.
#L1 #L2 * -L1 L2
[ #K1 #I #V1 #H destruct
| #K1 #K2 #I #V1 #V2 #HK12 #HV12 #L #J #W #H destruct - K1 I V1 /2 width=5/
(* Basic inversion lemmas ***************************************************)
-lemma tpr_inv_sort1_aux: ∀U1,U2. U1 ⇒ U2 → ∀k. U1 = ⋆k → U2 = ⋆k.
+fact tpr_inv_sort1_aux: ∀U1,U2. U1 ⇒ U2 → ∀k. U1 = ⋆k → U2 = ⋆k.
#U1 #U2 * -U1 U2
[ #k0 #k #H destruct -k0 //
| #i #k #H destruct
lemma tpr_inv_sort1: ∀k,U2. ⋆k ⇒ U2 → U2 = ⋆k.
/2/ qed.
-lemma tpr_inv_lref1_aux: ∀U1,U2. U1 ⇒ U2 → ∀i. U1 = #i → U2 = #i.
+fact tpr_inv_lref1_aux: ∀U1,U2. U1 ⇒ U2 → ∀i. U1 = #i → U2 = #i.
#U1 #U2 * -U1 U2
[ #k #i #H destruct
| #j #i #H destruct -j //
lemma tpr_inv_lref1: ∀i,U2. #i ⇒ U2 → U2 = #i.
/2/ qed.
-lemma tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
- (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
- ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
- U2 = 𝕚{I} V2. T
- )∨
- ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
+fact tpr_inv_bind1_aux: ∀U1,U2. U1 ⇒ U2 → ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
+ (∃∃V2,T2,T. V1 ⇒ V2 & T1 ⇒ T2 &
+ ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
+ U2 = 𝕚{I} V2. T
+ ) ∨
+ ∃∃T. ↑[0,1] T ≡ T1 & T ⇒ U2 & I = Abbr.
#U1 #U2 * -U1 U2
[ #k #I #V #T #H destruct
| #i #I #V #T #H destruct
elim (tpr_inv_bind1 … H) -H * /3 width=7/
qed.
-lemma tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 →
- ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
- U2 = 𝕚{Appl} V2. T2
- | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
- U0 = 𝕚{Abst} W. T1 &
- U2 = 𝕓{Abbr} V2. T2
- | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
- ↑[0,1] V2 ≡ V &
- U0 = 𝕚{Abbr} W1. T1 &
- U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2.
+fact tpr_inv_appl1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,U0. U1 = 𝕚{Appl} V1. U0 →
+ ∨∨ ∃∃V2,T2. V1 ⇒ V2 & U0 ⇒ T2 &
+ U2 = 𝕚{Appl} V2. T2
+ | ∃∃V2,W,T1,T2. V1 ⇒ V2 & T1 ⇒ T2 &
+ U0 = 𝕚{Abst} W. T1 &
+ U2 = 𝕓{Abbr} V2. T2
+ | ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
+ ↑[0,1] V2 ≡ V &
+ U0 = 𝕚{Abbr} W1. T1 &
+ U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2.
#U1 #U2 * -U1 U2
[ #k #V #T #H destruct
| #i #V #T #H destruct
U2 = 𝕚{Abbr} W2. 𝕚{Appl} V. T2.
/2/ qed.
-lemma tpr_inv_cast1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Cast} V1. T1 →
- (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2)
- ∨ T1 ⇒ U2.
+fact tpr_inv_cast1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Cast} V1. T1 →
+ (∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Cast} V2. T2)
+ ∨ T1 ⇒ U2.
#U1 #U2 * -U1 U2
[ #k #V #T #H destruct
| #i #V #T #H destruct
]
qed.
-lemma tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
- ∨∨ T1 = #i
- | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
- T1 = 𝕚{Abbr} V. T
- | ∃∃V,T. T ⇒ #i & T1 = 𝕚{Cast} V. T.
+fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
+ ∨∨ T1 = #i
+ | ∃∃V,T,T0. ↑[O,1] T0 ≡ T & T0 ⇒ #i &
+ T1 = 𝕚{Abbr} V. T
+ | ∃∃V,T. T ⇒ #i & T1 = 𝕚{Cast} V. T.
#T1 #T2 * -T1 T2
[ #k #i #H destruct
| #j #i /2/
(* Advanced inversion lemmas ************************************************)
-lemma tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 →
- ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
+fact tpr_inv_abst1_aux: ∀U1,U2. U1 ⇒ U2 → ∀V1,T1. U1 = 𝕚{Abst} V1. T1 →
+ ∃∃V2,T2. V1 ⇒ V2 & T1 ⇒ T2 & U2 = 𝕚{Abst} V2. T2.
#U1 #U2 * -U1 U2
[ #k #V #T #H destruct
| #i #V #T #H destruct
(* Confluence lemmas ********************************************************)
-lemma tpr_conf_sort_sort: ∀k. ∃∃X. ⋆k ⇒ X & ⋆k ⇒ X.
+fact tpr_conf_sort_sort: ∀k. ∃∃X. ⋆k ⇒ X & ⋆k ⇒ X.
/2/ qed.
-lemma tpr_conf_lref_lref: ∀i. ∃∃X. #i ⇒ X & #i ⇒ X.
+fact tpr_conf_lref_lref: ∀i. ∃∃X. #i ⇒ X & #i ⇒ X.
/2/ qed.
-lemma tpr_conf_flat_flat:
+fact tpr_conf_flat_flat:
∀I,V0,V1,T0,T1,V2,T2. (
- ∀X0:term. #X0 < #V0 + #T0 + 1 →
+ ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
elim (IH … HT01 … HT02) -HT01 HT02 /3 width=5/
qed.
-lemma tpr_conf_flat_beta:
+fact tpr_conf_flat_beta:
∀V0,V1,T1,V2,W0,U0,T2. (
- ∀X0:term. #X0 < #V0 + (#W0 + #U0 + 1) + 1 →
+ ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 →
∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
elim (IH … HT02 … HU01) -HT02 HU01 IH /3 width=5/
qed.
-lemma tpr_conf_flat_theta:
+fact tpr_conf_flat_theta:
∀V0,V1,T1,V2,V,W0,W2,U0,U2. (
- ∀X0:term. #X0 < #V0 + (#W0 + #U0 + 1) + 1 →
+ ∀X0:term. #[X0] < #[V0] + (#[W0] + #[U0] + 1) + 1 →
∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
]
qed.
-lemma tpr_conf_flat_cast:
+fact tpr_conf_flat_cast:
∀X2,V0,V1,T0,T1. (
- ∀X0:term. #X0 < #V0 + # T0 + 1 →
+ ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
elim (IH … HT01 … HT02) -HT01 HT02 IH /3/
qed.
-lemma tpr_conf_beta_beta:
+fact tpr_conf_beta_beta:
∀W0:term. ∀V0,V1,T0,T1,V2,T2. (
- ∀X0:term. #X0 < #V0 + (#W0 + #T0 + 1) + 1 →
+ ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 →
∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
elim (IH … HT01 … HT02) -HT01 HT02 IH /3 width=5/
qed.
-lemma tpr_conf_delta_delta:
+fact tpr_conf_delta_delta:
∀I1,V0,V1,T0,T1,TT1,V2,T2,TT2. (
- ∀X0:term. #X0 < #V0 +#T0 + 1→
+ ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
@ex2_1_intro [2,3: @tpr_delta |1: skip ] /width=10/ (**) (* /3 width=10/ is too slow *)
qed.
-lemma tpr_conf_delta_zeta:
+fact tpr_conf_delta_zeta:
∀X2,V0,V1,T0,T1,TT1,T2. (
- ∀X0:term. #X0 < #V0 +#T0 + 1→
+ ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
elim (IH … HTX2 … HTT2) -HTX2 HTT2 IH /3/
qed.
-lemma tpr_conf_theta_theta:
+fact tpr_conf_theta_theta:
∀VV1,V0,V1,W0,W1,T0,T1,V2,VV2,W2,T2. (
- ∀X0:term. #X0 < #V0 + (#W0 + #T0 + 1) + 1 →
+ ∀X0:term. #[X0] < #[V0] + (#[W0] + #[T0] + 1) + 1 →
∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
@ex2_1_intro [2,3: @tpr_bind |1:skip ] /2 width=5/ (**) (* /4 width=5/ is too slow *)
qed.
-lemma tpr_conf_zeta_zeta:
+fact tpr_conf_zeta_zeta:
∀V0:term. ∀X2,TT0,T0,T1,T2. (
- ∀X0:term. #X0 < #V0 + #TT0 + 1 →
+ ∀X0:term. #[X0] < #[V0] + #[TT0] + 1 →
∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
elim (IH … HT01 … HTX2) -HT01 HTX2 IH /2/
qed.
-lemma tpr_conf_tau_tau:
+fact tpr_conf_tau_tau:
∀V0,T0:term. ∀X2,T1. (
- ∀X0:term. #X0 < #V0 + #T0 + 1 →
+ ∀X0:term. #[X0] < #[V0] + #[T0] + 1 →
∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
(* Confluence ***************************************************************)
-lemma tpr_conf_aux:
+fact tpr_conf_aux:
∀Y0:term. (
- ∀X0:term. #X0 < #Y0 → ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
+ ∀X0:term. #[X0] < #[Y0] →
+ ∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
∀X0,X1,X2. X0 ⇒ X1 → X0 ⇒ X2 → X0 = Y0 →
(* *)
(**************************************************************************)
-include "Basic-2/substitution/leq.ma".
+include "Basic-2/grammar/leq.ma".
include "Basic-2/substitution/lift.ma".
(* DROPPING *****************************************************************)
+(* Basic-1: includes: drop_skip_bind *)
inductive drop: lenv → nat → nat → lenv → Prop ≝
| drop_sort: ∀d,e. drop (⋆) d e (⋆)
| drop_comp: ∀L1,L2,I,V. drop L1 0 0 L2 → drop (L1. 𝕓{I} V) 0 0 (L2. 𝕓{I} V)
(* Basic inversion lemmas ***************************************************)
-lemma drop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2.
+fact drop_inv_refl_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 → e = 0 → L1 = L2.
#d #e #L1 #L2 #H elim H -H d e L1 L2
[ //
| #L1 #L2 #I #V #_ #IHL12 #H1 #H2
]
qed.
+(* Basic-1: was: drop_gen_refl *)
lemma drop_inv_refl: ∀L1,L2. ↓[0, 0] L1 ≡ L2 → L1 = L2.
/2 width=5/ qed.
-lemma drop_inv_sort1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ →
- L2 = ⋆.
+fact drop_inv_sort1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → L1 = ⋆ →
+ L2 = ⋆.
#d #e #L1 #L2 * -d e L1 L2
[ //
| #L1 #L2 #I #V #_ #H destruct
]
qed.
+(* Basic-1: was: drop_gen_sort *)
lemma drop_inv_sort1: ∀d,e,L2. ↓[d, e] ⋆ ≡ L2 → L2 = ⋆.
/2 width=5/ qed.
-lemma drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 →
- ∀K,I,V. L1 = K. 𝕓{I} V →
- (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
- (0 < e ∧ ↓[d, e - 1] K ≡ L2).
+fact drop_inv_O1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → d = 0 →
+ ∀K,I,V. L1 = K. 𝕓{I} V →
+ (e = 0 ∧ L2 = K. 𝕓{I} V) ∨
+ (0 < e ∧ ↓[d, e - 1] K ≡ L2).
#d #e #L1 #L2 * -d e L1 L2
[ #d #e #_ #K #I #V #H destruct
| #L1 #L2 #I #V #HL12 #H #K #J #W #HX destruct -L1 I V
(0 < e ∧ ↓[0, e - 1] K ≡ L2).
/2/ qed.
+(* Basic-1: was: drop_gen_drop *)
lemma drop_inv_drop1: ∀e,K,I,V,L2.
↓[0, e] K. 𝕓{I} V ≡ L2 → 0 < e → ↓[0, e - 1] K ≡ L2.
#e #K #I #V #L2 #H #He
elim (lt_refl_false … He)
qed.
-lemma drop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
- ∀I,K1,V1. L1 = K1. 𝕓{I} V1 →
- ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 &
- ↑[d - 1, e] V2 ≡ V1 &
- L2 = K2. 𝕓{I} V2.
+fact drop_inv_skip1_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
+ ∀I,K1,V1. L1 = K1. 𝕓{I} V1 →
+ ∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 &
+ ↑[d - 1, e] V2 ≡ V1 &
+ L2 = K2. 𝕓{I} V2.
#d #e #L1 #L2 * -d e L1 L2
[ #d #e #_ #I #K #V #H destruct
| #L1 #L2 #I #V #_ #H elim (lt_refl_false … H)
]
qed.
+(* Basic-1: was: drop_gen_skip_l *)
lemma drop_inv_skip1: ∀d,e,I,K1,V1,L2. ↓[d, e] K1. 𝕓{I} V1 ≡ L2 → 0 < d →
∃∃K2,V2. ↓[d - 1, e] K1 ≡ K2 &
↑[d - 1, e] V2 ≡ V1 &
L2 = K2. 𝕓{I} V2.
/2/ qed.
-lemma drop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
- ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
- ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 &
- ↑[d - 1, e] V2 ≡ V1 &
- L1 = K1. 𝕓{I} V1.
+fact drop_inv_skip2_aux: ∀d,e,L1,L2. ↓[d, e] L1 ≡ L2 → 0 < d →
+ ∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
+ ∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 &
+ ↑[d - 1, e] V2 ≡ V1 &
+ L1 = K1. 𝕓{I} V1.
#d #e #L1 #L2 * -d e L1 L2
[ #d #e #_ #I #K #V #H destruct
| #L1 #L2 #I #V #_ #H elim (lt_refl_false … H)
]
qed.
+(* Basic-1: was: drop_gen_skip_r *)
lemma drop_inv_skip2: ∀d,e,I,L1,K2,V2. ↓[d, e] L1 ≡ K2. 𝕓{I} V2 → 0 < d →
∃∃K1,V1. ↓[d - 1, e] K1 ≡ K2 & ↑[d - 1, e] V2 ≡ V1 &
L1 = K1. 𝕓{I} V1.
(* Basic properties *********************************************************)
+(* Basic-1: was by definition: drop_refl *)
lemma drop_refl: ∀L. ↓[0, 0] L ≡ L.
#L elim L -L /2/
qed.
(* Basic forvard lemmas *****************************************************)
+(* Basic-1: was: drop_S *)
lemma drop_fwd_drop2: ∀L1,I2,K2,V2,e. ↓[O, e] L1 ≡ K2. 𝕓{I2} V2 →
↓[O, e + 1] L1 ≡ K2.
#L1 elim L1 -L1
]
]
qed.
+
+(* Basic-1: removed theorems 18:
+ drop_skip_flat
+ cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
+ drop_clear drop_clear_O drop_clear_S
+ clear_gen_sort clear_gen_bind clear_gen_flat clear_gen_flat_r
+ clear_gen_all clear_clear clear_mono clear_trans clear_ctail
+ clear_cle
+*)
(* Main properties **********************************************************)
+(* Basic-1: was: drop_mono *)
theorem drop_mono: ∀d,e,L,L1. ↓[d, e] L ≡ L1 →
∀L2. ↓[d, e] L ≡ L2 → L1 = L2.
#d #e #L #L1 #H elim H -H d e L L1
]
qed.
+(* Basic-1: was: drop_conf_ge *)
theorem drop_conf_ge: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 →
∀e2,L2. ↓[0, e2] L ≡ L2 → d1 + e1 ≤ e2 →
↓[0, e2 - e1] L1 ≡ L2.
]
qed.
+(* Basic-1: was: drop_conf_lt *)
theorem drop_conf_lt: ∀d1,e1,L,L1. ↓[d1, e1] L ≡ L1 →
∀e2,K2,I,V2. ↓[0, e2] L ≡ K2. 𝕓{I} V2 →
e2 < d1 → let d ≝ d1 - e2 - 1 in
]
qed.
+(* Basic-1: was: drop_trans_le *)
theorem drop_trans_le: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
∀e2,L2. ↓[0, e2] L ≡ L2 → e2 ≤ d1 →
∃∃L0. ↓[0, e2] L1 ≡ L0 & ↓[d1 - e2, e1] L0 ≡ L2.
]
qed.
+(* Basic-1: was: drop_trans_ge *)
theorem drop_trans_ge: ∀d1,e1,L1,L. ↓[d1, e1] L1 ≡ L →
∀e2,L2. ↓[0, e2] L ≡ L2 → d1 ≤ e2 → ↓[0, e1 + e2] L1 ≡ L2.
#d1 #e1 #L1 #L #H elim H -H d1 e1 L1 L
#e1 #e1 #e2 >commutative_plus /2 width=5/
qed.
+(* Basic-1: was: drop_conf_rev *)
axiom drop_div: ∀e1,L1,L. ↓[0, e1] L1 ≡ L → ∀e2,L2. ↓[0, e2] L2 ≡ L →
∃∃L0. ↓[0, e1] L0 ≡ L2 & ↓[e1, e2] L0 ≡ L1.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "Basic-2/grammar/lenv_length.ma".
-
-(* LOCAL ENVIRONMENT EQUALITY ***********************************************)
-
-inductive leq: lenv → nat → nat → lenv → Prop ≝
-| leq_sort: ∀d,e. leq (⋆) d e (⋆)
-| leq_OO: ∀L1,L2. leq L1 0 0 L2
-| leq_eq: ∀L1,L2,I,V,e. leq L1 0 e L2 → leq (L1. 𝕓{I} V) 0 (e + 1) (L2.𝕓{I} V)
-| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e.
- leq L1 d e L2 → leq (L1. 𝕓{I1} V1) (d + 1) e (L2. 𝕓{I2} V2)
-.
-
-interpretation "local environment equality" 'Eq L1 d e L2 = (leq L1 d e L2).
-
-(* Basic properties *********************************************************)
-
-lemma leq_refl: ∀d,e,L. L [d, e] ≈ L.
-#d elim d -d
-[ #e elim e -e // #e #IHe #L elim L -L /2/
-| #d #IHd #e #L elim L -L /2/
-]
-qed.
-
-lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1.
-#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/
-qed.
-
-lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d →
- ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2.
-
-#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/
-qed.
-
-(* Basic inversion lemmas ***************************************************)
(* Basic forward lemmas *****************************************************)
-lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #T1 = #T2.
+lemma tw_lift: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → #[T1] = #[T2].
#d #e #T1 #T2 #H elim H -d e T1 T2; normalize //
qed.
(* Basic inversion lemmas ***************************************************)
-lemma lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2.
+fact lift_inv_refl_aux: ∀d,e,T1,T2. ↑[d, e] T1 ≡ T2 → e = 0 → T1 = T2.
#d #e #T1 #T2 #H elim H -H d e T1 T2 /3/
qed.
lemma lift_inv_refl: ∀d,T1,T2. ↑[d, 0] T1 ≡ T2 → T1 = T2.
/2/ qed.
-lemma lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k.
+fact lift_inv_sort1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T1 = ⋆k → T2 = ⋆k.
#d #e #T1 #T2 * -d e T1 T2 //
[ #i #d #e #_ #k #H destruct
| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
lemma lift_inv_sort1: ∀d,e,T2,k. ↑[d,e] ⋆k ≡ T2 → T2 = ⋆k.
/2 width=5/ qed.
-lemma lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i →
- (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
+fact lift_inv_lref1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T1 = #i →
+ (i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
#d #e #T1 #T2 * -d e T1 T2
[ #k #d #e #i #H destruct
| #j #d #e #Hj #i #Hi destruct /3/
elim (lt_refl_false … Hdd)
qed.
-lemma lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
- ∀I,V1,U1. T1 = 𝕓{I} V1.U1 →
- ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
- T2 = 𝕓{I} V2. U2.
+fact lift_inv_bind1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+ ∀I,V1,U1. T1 = 𝕓{I} V1.U1 →
+ ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
+ T2 = 𝕓{I} V2. U2.
#d #e #T1 #T2 * -d e T1 T2
[ #k #d #e #I #V1 #U1 #H destruct
| #i #d #e #_ #I #V1 #U1 #H destruct
T2 = 𝕓{I} V2. U2.
/2/ qed.
-lemma lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
- ∀I,V1,U1. T1 = 𝕗{I} V1.U1 →
- ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
- T2 = 𝕗{I} V2. U2.
+fact lift_inv_flat1_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+ ∀I,V1,U1. T1 = 𝕗{I} V1.U1 →
+ ∃∃V2,U2. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
+ T2 = 𝕗{I} V2. U2.
#d #e #T1 #T2 * -d e T1 T2
[ #k #d #e #I #V1 #U1 #H destruct
| #i #d #e #_ #I #V1 #U1 #H destruct
T2 = 𝕗{I} V2. U2.
/2/ qed.
-lemma lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
+fact lift_inv_sort2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀k. T2 = ⋆k → T1 = ⋆k.
#d #e #T1 #T2 * -d e T1 T2 //
[ #i #d #e #_ #k #H destruct
| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
lemma lift_inv_sort2: ∀d,e,T1,k. ↑[d,e] T1 ≡ ⋆k → T1 = ⋆k.
/2 width=5/ qed.
-lemma lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i →
- (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
+fact lift_inv_lref2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 → ∀i. T2 = #i →
+ (i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
#d #e #T1 #T2 * -d e T1 T2
[ #k #d #e #i #H destruct
| #j #d #e #Hj #i #Hi destruct /3/
elim (plus_lt_false … Hdd)
qed.
-lemma lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
- ∀I,V2,U2. T2 = 𝕓{I} V2.U2 →
- ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
- T1 = 𝕓{I} V1. U1.
+fact lift_inv_bind2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+ ∀I,V2,U2. T2 = 𝕓{I} V2.U2 →
+ ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d+1,e] U1 ≡ U2 &
+ T1 = 𝕓{I} V1. U1.
#d #e #T1 #T2 * -d e T1 T2
[ #k #d #e #I #V2 #U2 #H destruct
| #i #d #e #_ #I #V2 #U2 #H destruct
T1 = 𝕓{I} V1. U1.
/2/ qed.
-lemma lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
- ∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
- ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
- T1 = 𝕗{I} V1. U1.
+fact lift_inv_flat2_aux: ∀d,e,T1,T2. ↑[d,e] T1 ≡ T2 →
+ ∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
+ ∃∃V1,U1. ↑[d,e] V1 ≡ V2 & ↑[d,e] U1 ≡ U2 &
+ T1 = 𝕗{I} V1. U1.
#d #e #T1 #T2 * -d e T1 T2
[ #k #d #e #I #V2 #U2 #H destruct
| #i #d #e #_ #I #V2 #U2 #H destruct
(* Basic inversion lemmas ***************************************************)
-lemma tps_inv_lref1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. T1 = #i →
- T2 = #i ∨
- ∃∃K,V. d ≤ i & i < d + e &
- ↓[O, i] L ≡ K. 𝕓{Abbr} V &
- ↑[O, i + 1] V ≡ T2.
+fact tps_inv_lref1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀i. T1 = #i →
+ T2 = #i ∨
+ ∃∃K,V. d ≤ i & i < d + e &
+ ↓[O, i] L ≡ K. 𝕓{Abbr} V &
+ ↑[O, i + 1] V ≡ T2.
#L #T1 #T2 #d #e * -L T1 T2 d e
[ #L #k #d #e #i #H destruct
| /2/
↑[O, i + 1] V ≡ T2.
/2/ qed.
-lemma tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
- ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
- ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 &
- L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 &
- U2 = 𝕓{I} V2. T2.
+fact tps_inv_bind1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
+ ∀I,V1,T1. U1 = 𝕓{I} V1. T1 →
+ ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 &
+ L. 𝕓{I} V1 ⊢ T1 [d + 1, e] ≫ T2 &
+ U2 = 𝕓{I} V2. T2.
#d #e #L #U1 #U2 * -d e L U1 U2
[ #L #k #d #e #I #V1 #T1 #H destruct
| #L #i #d #e #I #V1 #T1 #H destruct
U2 = 𝕓{I} V2. T2.
/2/ qed.
-lemma tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
- ∀I,V1,T1. U1 = 𝕗{I} V1. T1 →
- ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 &
- U2 = 𝕗{I} V2. T2.
+fact tps_inv_flat1_aux: ∀d,e,L,U1,U2. L ⊢ U1 [d, e] ≫ U2 →
+ ∀I,V1,T1. U1 = 𝕗{I} V1. T1 →
+ ∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 &
+ U2 = 𝕗{I} V2. T2.
#d #e #L #U1 #U2 * -d e L U1 U2
[ #L #k #d #e #I #V1 #T1 #H destruct
| #L #i #d #e #I #V1 #T1 #H destruct
∃∃V2,T2. L ⊢ V1 [d, e] ≫ V2 & L ⊢ T1 [d, e] ≫ T2 &
U2 = 𝕗{I} V2. T2.
/2/ qed.
+
+fact tps_inv_refl0_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 0 → T1 = T2.
+#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
+[ //
+| //
+| #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #H destruct -e;
+ lapply (le_to_lt_to_lt … Hdi … Hide) -Hdi Hide <plus_n_O #Hdd
+ elim (lt_refl_false … Hdd)
+| /3/
+| /3/
+]
+qed.
+
+lemma tps_inv_refl0: ∀L,T1,T2,d. L ⊢ T1 [d, 0] ≫ T2 → T1 = T2.
+/2 width=6/ qed.
(* Advanced inversion lemmas ************************************************)
-lemma tps_inv_refl1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 →
- ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
+fact tps_inv_refl1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 →
+ ∀K,V. ↓[0, d] L ≡ K. 𝕓{Abst} V → T1 = T2.
#L #T1 #T2 #d #e #H elim H -H L T1 T2 d e
[ //
| //
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "arithmetics/nat.ma".
+include "Ground-2/xoa_props.ma".
+
+(* ARITHMETICAL PROPERTIES **************************************************)
+
+lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
+#n #m <plus_n_Sm #H destruct
+qed.
+
+lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p.
+#n #m #p <plus_n_Sm #H @(lt_to_le_to_lt … H) //
+qed.
+
+lemma minus_le: ∀m,n. m - n ≤ m.
+/2/ qed.
+
+lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
+/2/ qed.
+
+lemma lt_to_le: ∀a,b. a < b → a ≤ b.
+/2/ qed.
+
+lemma lt_refl_false: ∀n. n < n → False.
+#n #H elim (lt_to_not_eq … H) -H /2/
+qed.
+
+lemma lt_zero_false: ∀n. n < 0 → False.
+#n #H elim (lt_to_not_le … H) -H /2/
+qed.
+
+lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
+#m #n elim (decidable_lt m n) /3/
+qed.
+
+lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
+#m elim m -m
+[ * /2/
+| #m #IHm * [ /2/ ]
+ #n elim (IHm n) -IHm #H
+ [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] /2/ (**) (* /3/ is slow *)
+ qed.
+
+lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
+#m #n * -n /3/
+qed.
+
+lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p.
+/2/ qed.
+
+lemma plus_lt_false: ∀m,n. m + n < m → False.
+#m #n #H1 lapply (le_plus_n_r n m) #H2
+lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
+elim (lt_refl_false … H)
+qed.
+
+lemma monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
+#p #q #n #H1 #H2
+@lt_plus_to_minus_r <plus_minus_m_m //.
+qed.
+
+lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
+/2/ qed.
+
+lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d.
+/2/ qed.
+
+lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
+// qed.
+
+lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
+#n #m #p #lepm @plus_to_minus <associative_plus
+>(commutative_plus p) <plus_minus_m_m //
+qed.
+
+lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
+#b elim b -b
+[ #c #a #H >(le_O_to_eq_O … H) -H //
+| #b #IHb #c elim c -c //
+ #c #_ #a #Hcb
+ lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
+ <plus_n_Sm normalize /2/
+]
+qed.
+
+lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
+// qed.
+
+lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
+/3/ qed.
+
+lemma le_plus_minus: ∀a,b,c. c ≤ b → a + b - c = a + (b - c).
+/2/ qed.
+
+lemma plus_minus_m_m_comm: ∀n,m. m ≤ n → n = m + (n - m).
+/2/ qed.
+
+lemma minus_plus_m_m_comm: ∀n,m. n = (m + n) - m.
+/2/ qed.
+
+lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a.
+/2/ qed.
+
+lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
+#a #b #c1 #H >minus_plus @eq_f2 /2/
+qed.
+
+lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
+#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2/
+qed.
+
+lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b.
+// qed.
+
+lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
+#x #a #b #c1 >plus_plus_comm_23 //
+qed.
+
+lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b.
+/2/ qed.
+
+lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a.
+/3/ qed.
+
+lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b.
+#a #b #c1 #H >minus_plus <minus_minus //
+qed.
+
+lemma arith_g1: ∀a,b,c1. c1 ≤ b → a - (b - c1) - c1 = a - b.
+/2/ qed.
+
+lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
+ a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
+#a1 #a2 #b #c1 #H1 #H2 <le_plus_minus_comm /2/
+qed.
+
+lemma arith_i2: ∀a,c1,c2. c1 + c2 ≤ a → c1 + c2 + (a - c1 - c2) = a.
+/2/ qed.
+
+lemma arith_z1: ∀a,b,c1. a + c1 - b - c1 = a - b.
+// qed.
+
+(* unstable *****************************************************************)
+
+lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
+/2/ qed.
+
+lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
+#j #i #e #d #H lapply (plus_le_minus … H) -H /2/
+qed.
+
+lemma arith3: ∀a1,a2,b,c1. a1 + a2 ≤ b → a1 + c1 + a2 ≤ b + c1.
+/2/ qed.
+
+lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
+/2/ qed.
+
+lemma arith5: ∀a,b1,b2,c1. c1 ≤ b1 → c1 ≤ a → a < b1 + b2 → a - c1 < b1 - c1 + b2.
+#a #b1 #b2 #c1 #H1 #H2 #H3
+<le_plus_minus_comm // @monotonic_lt_minus_l //
+qed.
+
+lemma arith8: ∀a,b. a < a + b + 1.
+// qed.
+
+lemma arith9: ∀a,b,c. c < a + (b + c + 1) + 1.
+// qed.
+
+lemma arith10: ∀a,b,c,d,e. a ≤ b → c + (a - d - e) ≤ c + (b - d - e).
+#a #b #c #d #e #H
+>minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l //
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "arithmetics/nat.ma".
-include "Ground-2/xoa_props.ma".
-
-(* ARITHMETICAL PROPERTIES **************************************************)
-
-lemma plus_S_eq_O_false: ∀n,m. n + S m = 0 → False.
-#n #m <plus_n_Sm #H destruct
-qed.
-
-lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p.
-#n #m #p <plus_n_Sm #H @(lt_to_le_to_lt … H) //
-qed.
-
-lemma minus_le: ∀m,n. m - n ≤ m.
-/2/ qed.
-
-lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
-/2/ qed.
-
-lemma lt_to_le: ∀a,b. a < b → a ≤ b.
-/2/ qed.
-
-lemma lt_refl_false: ∀n. n < n → False.
-#n #H elim (lt_to_not_eq … H) -H /2/
-qed.
-
-lemma lt_zero_false: ∀n. n < 0 → False.
-#n #H elim (lt_to_not_le … H) -H /2/
-qed.
-
-lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
-#m #n elim (decidable_lt m n) /3/
-qed.
-
-lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
-#m elim m -m
-[ * /2/
-| #m #IHm * [ /2/ ]
- #n elim (IHm n) -IHm #H
- [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] /2/ (**) (* /3/ is slow *)
- qed.
-
-lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
-#m #n * -n /3/
-qed.
-
-lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p.
-/2/ qed.
-
-lemma plus_lt_false: ∀m,n. m + n < m → False.
-#m #n #H1 lapply (le_plus_n_r n m) #H2
-lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
-elim (lt_refl_false … H)
-qed.
-
-lemma monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
-#p #q #n #H1 #H2
-@lt_plus_to_minus_r <plus_minus_m_m //.
-qed.
-
-lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
-/2/ qed.
-
-lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d.
-/2/ qed.
-
-lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
-// qed.
-
-lemma le_plus_minus_comm: ∀n,m,p. p ≤ m → m + n - p = m - p + n.
-#n #m #p #lepm @plus_to_minus <associative_plus
->(commutative_plus p) <plus_minus_m_m //
-qed.
-
-lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
-#b elim b -b
-[ #c #a #H >(le_O_to_eq_O … H) -H //
-| #b #IHb #c elim c -c //
- #c #_ #a #Hcb
- lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
- <plus_n_Sm normalize /2/
-]
-qed.
-
-lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
-// qed.
-
-lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
-/3/ qed.
-
-lemma le_plus_minus: ∀a,b,c. c ≤ b → a + b - c = a + (b - c).
-/2/ qed.
-
-lemma plus_minus_m_m_comm: ∀n,m. m ≤ n → n = m + (n - m).
-/2/ qed.
-
-theorem minus_plus_m_m_comm: ∀n,m. n = (m + n) - m.
-/2/ qed.
-
-lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a.
-/2/ qed.
-
-lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >minus_plus @eq_f2 /2/
-qed.
-
-lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
-#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2/
-qed.
-
-lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b.
-// qed.
-
-lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
-#x #a #b #c1 >plus_plus_comm_23 //
-qed.
-
-lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b.
-/2/ qed.
-
-lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a.
-/3/ qed.
-
-lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b.
-#a #b #c1 #H >minus_plus <minus_minus //
-qed.
-
-lemma arith_g1: ∀a,b,c1. c1 ≤ b → a - (b - c1) - c1 = a - b.
-/2/ qed.
-
-lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
- a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
-#a1 #a2 #b #c1 #H1 #H2 <le_plus_minus_comm /2/
-qed.
-
-lemma arith_i2: ∀a,c1,c2. c1 + c2 ≤ a → c1 + c2 + (a - c1 - c2) = a.
-/2/ qed.
-
-lemma arith_z1: ∀a,b,c1. a + c1 - b - c1 = a - b.
-// qed.
-
-(* unstable *****************************************************************)
-
-lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
-/2/ qed.
-
-lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
-#j #i #e #d #H lapply (plus_le_minus … H) -H /2/
-qed.
-
-lemma arith3: ∀a1,a2,b,c1. a1 + a2 ≤ b → a1 + c1 + a2 ≤ b + c1.
-/2/ qed.
-
-lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
-/2/ qed.
-
-lemma arith5: ∀a,b1,b2,c1. c1 ≤ b1 → c1 ≤ a → a < b1 + b2 → a - c1 < b1 - c1 + b2.
-#a #b1 #b2 #c1 #H1 #H2 #H3
-<le_plus_minus_comm // @monotonic_lt_minus_l //
-qed.
-
-lemma arith8: ∀a,b. a < a + b + 1.
-// qed.
-
-lemma arith9: ∀a,b,c. c < a + (b + c + 1) + 1.
-// qed.
-
-lemma arith10: ∀a,b,c,d,e. a ≤ b → c + (a - d - e) ≤ c + (b - d - e).
-#a #b #c #d #e #H
->minus_plus >minus_plus @monotonic_le_plus_r @monotonic_le_minus_l //
-qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "Ground-2/arith.ma".
+include "Ground-2/notation.ma".
+
+(* LISTS ********************************************************************)
+
+inductive list (A:Type[0]) : Type[0] :=
+ | nil : list A
+ | cons: A -> list A -> list A.
+
+interpretation "nil (list)" 'Nil = (nil ?).
+
+interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
+
+let rec append A (l1: list A) l2 on l1 ≝
+ match l1 with
+ [ nil ⇒ l2
+ | cons hd tl ⇒ hd :: append A tl l2
+ ].
+
+interpretation "append (list)" 'Append l1 l2 = (append ? l1 l2).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+(* Lists ********************************************************************)
+
+notation "hvbox( hd break :: tl )"
+ right associative with precedence 47
+ for @{'Cons $hd $tl}.
+
+notation "hvbox( l1 break @ l2)"
+ right associative with precedence 47
+ for @{'Append $l1 $l2 }.
CONF = Ground-2/xoa.conf.xml
TARGETS = Ground-2/xoa_natation.ma Ground-2/xoa.ma
+PACKAGES = Ground-2 Basic-2
+
all:
+# xoa ########################################################################
+
xoa: $(TARGETS)
$(TARGETS): $(CONF)
@echo " EXEC $(XOA) $(CONF)"
$(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(CONF)
-stats: MAS = $(shell find -name "*.ma")
+# stats ######################################################################
+
+stats: $(PACKAGES:%=%.stats)
-stats: CHARS = $(shell cat $(MAS) | wc -c)
+%.stats: MAS = $(shell find $* -name "*.ma")
-stats:
+%.stats: CHARS = $(shell cat $(MAS) | wc -c)
+
+%.stats:
+ @printf '\e[1;40;37m'
+ @printf '%-15s %-42s' 'Statistics for:' $*
+ @printf '\e[0m\n'
@printf '\e[1;40;35m'
@printf '%-8s %6i' Chars $(CHARS)
@printf ' %-8s %5i' Lines `cat $(MAS) | wc -l`
@printf ' %-6s %3i' Pages `echo $$(($(CHARS) / 5120))`
+ @printf ' %-10s' ''
@printf '\e[0m\n'
@printf '\e[1;40;36m'
@printf '%-8s %6i' Sources `ls $(MAS) | wc -l`
- @printf ' %-27s' ''
+ @printf ' %-40s' ''
# @printf ' %-8s %5i' Objs `ls *.vo | wc -l`
# @printf ' %-6s %3i' Files `ls *.v | wc -l`
@printf '\e[0m\n'
@printf '\e[1;40;32m'
@printf '%-8s %6i' Theorems `grep theorem $(MAS) | wc -l`
@printf ' %-8s %5i' Lemmas `grep lemma $(MAS) | wc -l`
- @printf ' %-6s %3i' Proofs `grep qed $(MAS) | wc -l`
-# @printf ' %-9s %3i' Generated `grep Derive *.v | wc -l`
+ @printf ' %-6s %3i' Facts `grep fact $(MAS) | wc -l`
+ @printf ' %-6s %3i' Proofs `grep qed $(MAS) | wc -l`
@printf '\e[0m\n'
@printf '\e[1;40;33m'
@printf '%-8s %6i' Defs `grep "definition\|let rec\|inductive\|record" $(MAS) | wc -l`
- @printf ' %-27s' ''
+ @printf ' %-40s' ''
# @printf ' %-8s %5i' Local `grep "Local" *.v | wc -l`
@printf '\e[0m\n'
@printf '\e[1;40;31m'
@printf '%-8s %6i' Axioms `grep axiom $(MAS) | wc -l`
@printf ' %-8s %5i' Comments `grep "(\*[^*]*$$" $(MAS) | wc -l`
@printf ' %-6s %3i' Marks `grep "(\*\*)" $(MAS) | wc -l`
+ @printf ' %-10s' ''
@printf '\e[0m\n'
projects / helm.git / commitdiff