- basics: some support for abstract triangular confluence (which

subject reduction is an instance of)
- predefined_virtuals: more Alt-L shortcuts
- lambda_delta: more properties on computation, some annotations,
improved Makefile

diff --git a/matita/matita/contribs/lambda_delta/Makefile b/matita/matita/contribs/lambda_delta/Makefile
index 005b69df79599c0a91365fd90d76c255eb3ca74d..71dff0f41f7f60ae70f662fb8ad4929b4e9d6063 100644 (file)
--- a/matita/matita/contribs/lambda_delta/Makefile
+++ b/matita/matita/contribs/lambda_delta/Makefile
@@ -1,9 +1,13 @@
-H       = @
-XOA_DIR = ../../../components/binaries/xoa
-XOA     = xoa.native
+H        = @
+XOA_DIR  = ../../../components/binaries/xoa
+XOA      = xoa.native
 
-CONF    = ground_2/xoa.conf.xml
-TARGETS = ground_2/xoa_natation.ma ground_2/xoa.ma
+CONF     = ground_2/xoa.conf.xml
+TARGETS  = ground_2/xoa_natation.ma ground_2/xoa.ma
+
+ORIG     = . ./orig.sh 
+
+ORIGS    = basic_2/basic_1.orig
 
 PACKAGES = ground_2 basic_2 apps_2
 
@@ -17,6 +21,12 @@ $(TARGETS): $(CONF)
        @echo "  EXEC $(XOA) $(CONF)"
        $(H)MATITA_RT_BASE_DIR=../.. $(XOA_DIR)/$(XOA) $(CONF)
 
+# orig #######################################################################
+
+orig: $(ORIGS)
+       @echo "  ORIG basic_2"
+       $(H)$(ORIG) basic_2 < $(ORIGS)
+
 # stats ######################################################################
 
 stats: $(PACKAGES:%=%.stats)

diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.orig b/matita/matita/contribs/lambda_delta/basic_2/basic_1.orig
new file mode 100644 (file)
index 0000000..0b48e94
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.orig
@@ -0,0 +1,712 @@
+aplus/props / aplus_ahead_simpl
+aplus/props / aplus_asort_le_simpl
+aplus/props / aplus_asort_O_simpl
+aplus/props / aplus_asort_simpl
+aplus/props / aplus_assoc
+aplus/props / aplus_asucc
+aplus/props / aplus_asucc_false
+aplus/props / aplus_inj
+aplus/props / aplus_reg_r
+aplus/props / aplus_sort_O_S_simpl
+aplus/props / aplus_sort_S_S_simpl
+aprem/fwd / aprem_gen_head_O
+aprem/fwd / aprem_gen_head_S
+aprem/fwd / aprem_gen_sort
+aprem/props / aprem_asucc
+aprem/props / aprem_repl
+arity/aprem / arity_aprem
+arity/cimp / arity_cimp_conf
+arity/fwd / arity_gen_abst
+arity/fwd / arity_gen_appl
+arity/fwd / arity_gen_appls
+arity/fwd / arity_gen_bind
+arity/fwd / arity_gen_cast
+arity/fwd / arity_gen_lift
+arity/fwd / arity_gen_lref
+arity/fwd / arity_gen_sort
+arity/lift1 / arity_lift1
+arity/pr3 / arity_sred_pr2
+arity/pr3 / arity_sred_pr3
+arity/pr3 / arity_sred_wcpr0_pr0
+arity/pr3 / arity_sred_wcpr0_pr1
+arity/props / arity_appls_abbr
+arity/props / arity_appls_bind
+arity/props / arity_appls_cast
+arity/props / arity_lift
+arity/props / arity_mono
+arity/props / arity_repellent
+arity/props / node_inh
+arity/subst0 / arity_fsubst0
+arity/subst0 / arity_gen_cvoid
+arity/subst0 / arity_gen_cvoid_subst0
+arity/subst0 / arity_subst0
+asucc/fwd / asucc_gen_head
+asucc/fwd / asucc_gen_sort
+cimp/props / cimp_bind
+cimp/props / cimp_flat_dx
+cimp/props / cimp_flat_sx
+cimp/props / cimp_getl_conf
+clear/drop / drop_clear
+clear/drop / drop_clear_O
+clear/drop / drop_clear_S
+clear/fwd / clear_gen_all
+clear/fwd / clear_gen_bind
+clear/fwd / clear_gen_flat
+clear/fwd / clear_gen_flat_r
+clear/fwd / clear_gen_sort
+clear/props / clear_cle
+clear/props / clear_clear
+clear/props / clear_ctail
+clear/props / clear_mono
+clear/props / clear_trans
+clen/getl / getl_ctail_clen
+clen/getl / getl_gen_tail
+cnt/props / cnt_lift
+C/props / chead_ctail
+C/props / clt_cong
+C/props / clt_head
+C/props / clt_thead
+C/props / clt_wf_ind
+C/props clt_wf q_ind
+C/props / c_tail_ind
+csuba/arity / arity_appls_appl
+csuba/arity / csuba_arity
+csuba/arity / csuba_arity_rev
+csuba/clear / csuba_clear_conf
+csuba/clear / csuba_clear_trans
+csuba/drop / csuba_drop_abbr
+csuba/drop / csuba_drop_abbr_rev
+csuba/drop / csuba_drop_abst
+csuba/drop / csuba_drop_abst_rev
+csuba/fwd / csuba_gen_abbr
+csuba/fwd / csuba_gen_abbr_rev
+csuba/fwd / csuba_gen_abst
+csuba/fwd / csuba_gen_abst_rev
+csuba/fwd / csuba_gen_bind
+csuba/fwd / csuba_gen_bind_rev
+csuba/fwd / csuba_gen_flat
+csuba/fwd / csuba_gen_flat_rev
+csuba/fwd / csuba_gen_void
+csuba/fwd / csuba_gen_void_rev
+csuba/getl / csuba_getl_abbr
+csuba/getl / csuba_getl_abbr_rev
+csuba/getl / csuba_getl_abst
+csuba/getl / csuba_getl_abst_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 / csubc_drop1_conf_rev
+csubc/drop1 / drop1_csubc_trans
+csubc/drop / csubc_drop_conf_O
+csubc/drop / csubc_drop_conf_rev
+csubc/drop / drop_csubc_trans
+csubc/fwd / csubc_gen_head_l
+csubc/fwd / csubc_gen_head_r
+csubc/fwd / csubc_gen_sort_l
+csubc/fwd / csubc_gen_sort_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_eq
+csubst0/drop / csubst0_drop_eq_back
+csubst0/drop / csubst0_drop_gt
+csubst0/drop / csubst0_drop_gt_back
+csubst0/drop / csubst0_drop_lt
+csubst0/drop / csubst0_drop_lt_back
+csubst0/fwd / csubst0_gen_head
+csubst0/fwd / csubst0_gen_S_bind_2
+csubst0/fwd / csubst0_gen_sort
+csubst0/getl / csubst0_getl_ge
+csubst0/getl / csubst0_getl_ge_back
+csubst0/getl / csubst0_getl_lt
+csubst0/getl / csubst0_getl_lt_back
+csubst0/props / csubst0_both_bind
+csubst0/props / csubst0_fst_bind
+csubst0/props / csubst0_snd_bind
+csubst1/fwd / csubst1_gen_head
+csubst1/getl / csubst1_getl_ge
+csubst1/getl / csubst1_getl_ge_back
+csubst1/getl / csubst1_getl_lt
+csubst1/getl / getl_csubst1
+csubst1/props / csubst1_bind
+csubst1/props / csubst1_flat
+csubst1/props / csubst1_head
+csubt/clear / csubt_clear_conf
+csubt/csuba / csubt_csuba
+csubt/drop / csubt_drop_abbr
+csubt/drop / csubt_drop_abst
+csubt/drop / csubt_drop_flat
+csubt/fwd / csubt_gen_abbr
+csubt/fwd / csubt_gen_abst
+csubt/fwd / csubt_gen_bind
+csubt/fwd / csubt_gen_flat
+csubt/getl / csubt_getl_abbr
+csubt/getl / csubt_getl_abst
+csubt/pc3 / csubt_pc3
+csubt/pc3 / csubt_pr2
+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_pcons
+drop1/fwd / drop1_gen_pnil
+drop1/getl / drop1_getl_trans
+drop1/props / drop1_cons_tail
+drop1/props / drop1_skip_bind
+drop1/props / drop1_trans
+drop/fwd / drop_gen_drop
+drop/fwd / drop_gen_refl
+drop/fwd / drop_gen_skip_l
+drop/fwd / drop_gen_skip_r
+drop/fwd / drop_gen_sort
+drop/props / drop_conf_ge
+drop/props / drop_conf_lt
+drop/props / drop_conf_rev
+drop/props / drop_ctail
+drop/props / drop_mono
+drop/props / drop_S
+drop/props / drop_skip_bind
+drop/props / drop_skip_flat
+drop/props / drop_trans_ge
+drop/props / drop_trans_le
+ex0/props / aplus_gz_ge
+ex0/props / aplus_gz_le
+ex0/props / leq_leqz
+ex0/props / leqz_leq
+ex0/props / next_plus_gz
+ex1/props / ex1_arity
+ex1/props ex1 leq_sort_SS
+ex1/props / ex1_ty3
+ex2/props / ex2_arity
+ex2/props / ex2_nf2
+flt/props / flt_arith0
+flt/props / flt_arith1
+flt/props / flt_arith2
+flt/props / flt_shift
+flt/props / flt_thead_dx
+flt/props / flt_thead_sx
+flt/props / flt_trans
+flt/props / flt_wf_ind
+flt/props flt_wf q_ind
+fsubst0/fwd / fsubst0_gen_base
+getl/clear / clear_getl_trans
+getl/clear / getl_clear_bind
+getl/clear / getl_clear_conf
+getl/clear / getl_clear_trans
+getl/dec / getl_dec
+getl/drop / drop_getl_trans_ge
+getl/drop / drop_getl_trans_le
+getl/drop / drop_getl_trans_lt
+getl/drop / getl_conf_ge_drop
+getl/drop / getl_drop
+getl/drop / getl_drop_conf_ge
+getl/drop / getl_drop_conf_lt
+getl/drop / getl_drop_conf_rev
+getl/drop / getl_drop_trans
+getl/flt / getl_flt
+getl/fwd / getl_gen_2
+getl/fwd / getl_gen_all
+getl/fwd / getl_gen_bind
+getl/fwd / getl_gen_flat
+getl/fwd / getl_gen_O
+getl/fwd / getl_gen_S
+getl/fwd / getl_gen_sort
+getl/getl / getl_conf_le
+getl/getl / getl_trans
+getl/props / getl_ctail
+getl/props / getl_flat
+getl/props / getl_head
+getl/props / getl_mono
+getl/props / getl_refl
+iso/fwd / iso_flats_flat_bind_false
+iso/fwd / iso_flats_lref_bind_false
+iso/fwd / iso_gen_head
+iso/fwd / iso_gen_lref
+iso/fwd / iso_gen_sort
+iso/props / iso_refl
+iso/props / iso_trans
+leq/asucc / asucc_inj
+leq/asucc / asucc_repl
+leq/asucc / leq_ahead_asucc_false
+leq/asucc / leq_asucc
+leq/asucc / leq_asucc_false
+leq/fwd / leq_gen_head1
+leq/fwd / leq_gen_head2
+leq/fwd / leq_gen_sort1
+leq/fwd / leq_gen_sort2
+leq/props / ahead_inj_snd
+leq/props / leq_ahead_false_1
+leq/props / leq_ahead_false_2
+leq/props / leq_eq
+leq/props / leq_refl
+leq/props / leq_sym
+leq/props / leq_trans
+lift1/fwd / lift1_bind
+lift1/fwd / lift1_cons_tail
+lift1/fwd / lift1_flat
+lift1/fwd / lift1_lref
+lift1/fwd / lift1_sort
+lift1/fwd / lifts1_cons
+lift1/fwd / lifts1_flat
+lift1/fwd / lifts1_nil
+lift1/props / lift1_free
+lift1/props / lift1_lift1
+lift1/props / lift1_xhg
+lift1/props / lifts1_xhg
+lift/fwd / lift_bind
+lift/fwd / lift_flat
+lift/fwd / lift_gen_bind
+lift/fwd / lift_gen_flat
+lift/fwd / lift_gen_head
+lift/fwd / lift_gen_lref
+lift/fwd / lift_gen_lref_false
+lift/fwd / lift_gen_lref_ge
+lift/fwd / lift_gen_lref_lt
+lift/fwd / lift_gen_sort
+lift/fwd / lift_head
+lift/fwd / lift_lref_ge
+lift/fwd / lift_lref_lt
+lift/fwd / lift_sort
+lift/props / lift_d
+lift/props / lift_free
+lift/props / lift_gen_lift
+lift/props / lift_inj
+lift/props / lift_lref_gt
+lift/props / lift_r
+lift/props / lifts_inj
+lift/props / lifts_tapp
+lift/props / thead_x_lift_y_y
+lift/tlt / lift_tlt_dx
+lift/tlt / lift_weight
+lift/tlt / lift_weight_add
+lift/tlt / lift_weight_add_O
+lift/tlt / lift_weight_map
+llt/props / llt_head_dx
+llt/props / llt_head_sx
+llt/props / llt_repl
+llt/props / llt_trans
+llt/props / llt_wf_ind
+llt/props llt_wf q_ind
+llt/props / lweight_repl
+next_plus/props / next_plus_assoc
+next_plus/props / next_plus_lt
+next_plus/props / next_plus_next
+nf2/arity / arity_nf2_inv_all
+nf2/dec / nf2_dec
+nf2/fwd / nf2_gen_abbr
+nf2/fwd / nf2_gen_abst
+nf2/fwd / nf2_gen_beta
+nf2/fwd / nf2_gen_cast
+nf2/fwd / nf2_gen_flat
+nf2/fwd / nf2_gen_lref
+nf2/fwd nf2_gen nf2_gen_aux
+nf2/fwd / nf2_gen_void
+nf2/iso / nf2_iso_appls_lref
+nf2/lift1 / nf2_lift1
+nf2/pr3 / nf2_pr3_confluence
+nf2/pr3 / nf2_pr3_unfold
+nf2/props / nf2_abst
+nf2/props / nf2_abst_shift
+nf2/props / nf2_appl_lref
+nf2/props / nf2_appls_lref
+nf2/props / nf2_csort_lref
+nf2/props / nf2_lift
+nf2/props / nf2_lref_abst
+nf2/props / nf2_sort
+nf2/props / nfs2_tapp
+pc1/props / pc1_head
+pc1/props / pc1_head_1
+pc1/props / pc1_head_2
+pc1/props / pc1_pr0_r
+pc1/props / pc1_pr0_u
+pc1/props / pc1_pr0_u2
+pc1/props / pc1_pr0_x
+pc1/props / pc1_refl
+pc1/props / pc1_s
+pc1/props / pc1_t
+pc3/dec / pc3_abst_dec
+pc3/dec / pc3_dec
+pc3/fsubst0 / pc3_fsubst0
+pc3/fsubst0 / pc3_pr2_fsubst0
+pc3/fsubst0 / pc3_pr2_fsubst0_back
+pc3/fwd / pc3_gen_abst
+pc3/fwd / pc3_gen_abst_shift
+pc3/fwd / pc3_gen_lift
+pc3/fwd / pc3_gen_lift_abst
+pc3/fwd / pc3_gen_not_abst
+pc3/fwd / pc3_gen_sort
+pc3/fwd / pc3_gen_sort_abst
+pc3/left / pc3_ind_left
+pc3/left pc3_ind_left pc3_left_pc3
+pc3/left pc3_ind_left pc3_left_pr3
+pc3/left pc3_ind_left pc3_left_sym
+pc3/left pc3_ind_left pc3_left_trans
+pc3/left pc3_ind_left pc3_pc3_left
+pc3/nf2 / pc3_nf2
+pc3/nf2 / pc3_nf2_unfold
+pc3/pc1 / pc3_pc1
+pc3/props / clear_pc3_trans
+pc3/props / pc3_eta
+pc3/props / pc3_head_1
+pc3/props / pc3_head_12
+pc3/props / pc3_head_2
+pc3/props / pc3_head_21
+pc3/props / pc3_lift
+pc3/props / pc3_pr0_pr2_t
+pc3/props / pc3_pr2_pr2_t
+pc3/props / pc3_pr2_pr3_t
+pc3/props / pc3_pr2_r
+pc3/props / pc3_pr2_u
+pc3/props / pc3_pr2_u2
+pc3/props / pc3_pr2_x
+pc3/props / pc3_pr3_conf
+pc3/props / pc3_pr3_pc3_t
+pc3/props / pc3_pr3_r
+pc3/props / pc3_pr3_t
+pc3/props / pc3_pr3_x
+pc3/props / pc3_refl
+pc3/props / pc3_s
+pc3/props / pc3_t
+pc3/props / pc3_thin_dx
+pc3/subst1 / pc3_gen_cabbr
+pc3/wcpr0 / pc3_wcpr0
+pc3/wcpr0 pc3_wcpr0 pc3_wcpr0_t_aux
+pc3/wcpr0 / pc3_wcpr0_t
+pr0/dec / nf0_dec
+pr0/fwd / pr0_gen_abbr
+pr0/fwd / pr0_gen_abst
+pr0/fwd / pr0_gen_appl
+pr0/fwd / pr0_gen_cast
+pr0/fwd / pr0_gen_lift
+pr0/fwd / pr0_gen_lref
+pr0/fwd / pr0_gen_sort
+pr0/fwd / pr0_gen_void
+pr0/pr0 / pr0_confluence
+pr0/pr0 pr0_confluence pr0_cong_delta
+pr0/pr0 pr0_confluence pr0_cong_upsilon_cong
+pr0/pr0 pr0_confluence pr0_cong_upsilon_delta
+pr0/pr0 pr0_confluence pr0_cong_upsilon_refl
+pr0/pr0 pr0_confluence pr0_cong_upsilon_zeta
+pr0/pr0 pr0_confluence pr0_delta_delta
+pr0/pr0 pr0_confluence pr0_delta_tau
+pr0/pr0 pr0_confluence pr0_upsilon_upsilon
+pr0/props / pr0_lift
+pr0/props / pr0_subst0
+pr0/props / pr0_subst0_back
+pr0/props / pr0_subst0_fwd
+pr0/subst1 / pr0_delta1
+pr0/subst1 / pr0_subst1
+pr0/subst1 / pr0_subst1_back
+pr0/subst1 / pr0_subst1_fwd
+pr1/pr1 / pr1_confluence
+pr1/pr1 / pr1_strip
+pr1/props / pr1_comp
+pr1/props / pr1_eta
+pr1/props / pr1_head_1
+pr1/props / pr1_head_2
+pr1/props / pr1_pr0
+pr1/props / pr1_t
+pr2/clen / pr2_gen_cbind
+pr2/clen / pr2_gen_cflat
+pr2/clen / pr2_gen_ctail
+pr2/fwd / pr2_gen_abbr
+pr2/fwd / pr2_gen_abst
+pr2/fwd / pr2_gen_appl
+pr2/fwd / pr2_gen_cast
+pr2/fwd / pr2_gen_csort
+pr2/fwd / pr2_gen_lift
+pr2/fwd / pr2_gen_lref
+pr2/fwd / pr2_gen_sort
+pr2/fwd / pr2_gen_void
+pr2/pr2 / pr2_confluence
+pr2/pr2 pr2_confluence pr2_delta_delta
+pr2/pr2 pr2_confluence pr2_free_delta
+pr2/pr2 pr2_confluence pr2_free_free
+pr2/props / clear_pr2_trans
+pr2/props / pr2_cflat
+pr2/props / pr2_change
+pr2/props / pr2_ctail
+pr2/props / pr2_head_1
+pr2/props / pr2_head_2
+pr2/props / pr2_lift
+pr2/props / pr2_thin_dx
+pr2/subst1 / pr2_delta1
+pr2/subst1 / pr2_gen_cabbr
+pr2/subst1 / pr2_subst1
+pr3/fwd / pr3_gen_abbr
+pr3/fwd / pr3_gen_abst
+pr3/fwd / pr3_gen_appl
+pr3/fwd / pr3_gen_bind
+pr3/fwd / pr3_gen_cast
+pr3/fwd / pr3_gen_lift
+pr3/fwd / pr3_gen_lref
+pr3/fwd / pr3_gen_sort
+pr3/fwd / pr3_gen_void
+pr3/iso / pr3_iso_appl_bind
+pr3/iso / pr3_iso_appls_abbr
+pr3/iso / pr3_iso_appls_appl_bind
+pr3/iso / pr3_iso_appls_beta
+pr3/iso / pr3_iso_appls_bind
+pr3/iso / pr3_iso_appls_cast
+pr3/iso / pr3_iso_beta
+pr3/pr1 / pr3_pr1
+pr3/pr3 / pr3_confluence
+pr3/pr3 / pr3_strip
+pr3/props / clear_pr3_trans
+pr3/props / pr3_cflat
+pr3/props / pr3_eta
+pr3/props / pr3_flat
+pr3/props / pr3_head_1
+pr3/props / pr3_head_12
+pr3/props / pr3_head_2
+pr3/props / pr3_head_21
+pr3/props / pr3_lift
+pr3/props / pr3_pr0_pr2_t
+pr3/props / pr3_pr2
+pr3/props / pr3_pr2_pr2_t
+pr3/props / pr3_pr2_pr3_t
+pr3/props / pr3_pr3_pr3_t
+pr3/props / pr3_t
+pr3/props / pr3_thin_dx
+pr3/subst1 / pr3_gen_cabbr
+pr3/subst1 / pr3_subst1
+pr3/wcpr0 / pr3_wcpr0_t
+r/props / r_arith0
+r/props / r_arith1
+r/props / r_dis
+r/props / r_minus
+r/props / r_plus
+r/props / r_plus_sym
+r/props / r_S
+r/props / s_r
+sc3/arity / sc3_arity
+sc3/arity / sc3_arity_csubc
+sc3/props / sc3_abbr
+sc3/props / sc3_abst
+sc3/props / sc3_appl
+sc3/props / sc3_arity_gen
+sc3/props / sc3_bind
+sc3/props / sc3_cast
+sc3/props / sc3_lift
+sc3/props / sc3_lift1
+sc3/props sc3_props sc3_sn3_abst
+sc3/props / sc3_repl
+sc3/props / sc3_sn3
+sn3/fwd / sn3_gen_bind
+sn3/fwd / sn3_gen_cflat
+sn3/fwd / sn3_gen_flat
+sn3/fwd / sn3_gen_head
+sn3/fwd / sn3_gen_lift
+sn3/lift1 / sns3_lifts1
+sn3/nf2 / nf2_sn3
+sn3/nf2 / sn3_nf2
+sn3/props / sn3_abbr
+sn3/props / sn3_appl_abbr
+sn3/props / sn3_appl_appl
+sn3/props / sn3_appl_appls
+sn3/props / sn3_appl_beta
+sn3/props / sn3_appl_bind
+sn3/props / sn3_appl_cast
+sn3/props / sn3_appl_lref
+sn3/props / sn3_appls_abbr
+sn3/props / sn3_appls_beta
+sn3/props / sn3_appls_bind
+sn3/props / sn3_appls_cast
+sn3/props / sn3_appls_lref
+sn3/props / sn3_beta
+sn3/props / sn3_bind
+sn3/props / sn3_cast
+sn3/props / sn3_cdelta
+sn3/props / sn3_cflat
+sn3/props / sn3_change
+sn3/props / sn3_cpr3_trans
+sn3/props / sn3_gen_def
+sn3/props / sn3_lift
+sn3/props / sn3_pr2_intro
+sn3/props / sn3_pr3_trans
+sn3/props / sn3_shift
+sn3/props / sns3_lifts
+s/props / minus_s_s
+s/props / s_arith0
+s/props / s_arith1
+s/props / s_inc
+s/props / s_inj
+s/props / s_le
+s/props / s_lt
+s/props / s_minus
+s/props / s_plus
+s/props / s_plus_sym
+s/props / s_S
+sty0/fwd / sty0_gen_appl
+sty0/fwd / sty0_gen_bind
+sty0/fwd / sty0_gen_cast
+sty0/fwd / sty0_gen_lref
+sty0/fwd / sty0_gen_sort
+sty0/props / sty0_correct
+sty0/props / sty0_lift
+sty1/cnt / sty1_cnt
+sty1/props / sty1_abbr
+sty1/props / sty1_appl
+sty1/props / sty1_bind
+sty1/props / sty1_cast2
+sty1/props / sty1_correct
+sty1/props / sty1_lift
+sty1/props / sty1_trans
+subst0/dec / dnf_dec
+subst0/dec / dnf_dec2
+subst0/fwd / subst0_gen_head
+subst0/fwd / subst0_gen_lift_false
+subst0/fwd / subst0_gen_lift_ge
+subst0/fwd / subst0_gen_lift_lt
+subst0/fwd / subst0_gen_lref
+subst0/fwd / subst0_gen_sort
+subst0/props / subst0_lift_ge
+subst0/props / subst0_lift_ge_s
+subst0/props / subst0_lift_ge_S
+subst0/props / subst0_lift_lt
+subst0/props / subst0_refl
+subst0/subst0 / subst0_confluence_eq
+subst0/subst0 / subst0_confluence_lift
+subst0/subst0 / subst0_confluence_neq
+subst0/subst0 / subst0_subst0
+subst0/subst0 / subst0_subst0_back
+subst0/subst0 / subst0_trans
+subst0/tlt / subst0_tlt
+subst0/tlt / subst0_tlt_head
+subst0/tlt / subst0_weight_le
+subst0/tlt / subst0_weight_lt
+subst1/fwd / subst1_gen_head
+subst1/fwd / subst1_gen_lift_eq
+subst1/fwd / subst1_gen_lift_ge
+subst1/fwd / subst1_gen_lift_lt
+subst1/fwd / subst1_gen_lref
+subst1/fwd / subst1_gen_sort
+subst1/props / subst1_ex
+subst1/props / subst1_head
+subst1/props / subst1_lift_ge
+subst1/props / subst1_lift_lt
+subst1/props / subst1_lift_S
+subst1/subst1 / subst1_confluence_eq
+subst1/subst1 / subst1_confluence_lift
+subst1/subst1 / subst1_confluence_neq
+subst1/subst1 / subst1_subst1
+subst1/subst1 / subst1_subst1_back
+subst1/subst1 / subst1_trans
+subst/fwd / subst_head
+subst/fwd / subst_lref_eq
+subst/fwd / subst_lref_gt
+subst/fwd / subst_lref_lt
+subst/fwd / subst_sort
+subst/props / subst_lift_SO
+subst/props / subst_subst0
+T/dec / abst_dec
+T/dec / bind_dec_not
+T/dec / binder_dec
+T/dec / term_dec
+T/dec terms_props bind_dec
+T/dec terms_props flat_dec
+T/dec terms_props kind_dec
+tlist/props / tcons_tapp_ex
+tlist/props / theads_tapp
+tlist/props / tlist_ind_rev
+tlist/props / tslt_wf_ind
+tlist/props tslt_wf q_ind
+tlt/props / tlt_head_dx
+tlt/props / tlt_head_sx
+tlt/props / tlt_trans
+tlt/props / tlt_wf_ind
+tlt/props tlt_wf q_ind
+tlt/props / wadd_le
+tlt/props / wadd_lt
+tlt/props / wadd_O
+tlt/props / weight_add_O
+tlt/props / weight_add_S
+tlt/props / weight_eq
+tlt/props / weight_le
+T/props / not_abbr_abst
+T/props / not_abbr_void
+T/props / not_abst_void
+T/props / not_void_abst
+T/props / thead_x_y_y
+T/props / tweight_lt
+ty3/arity / ty3_arity
+ty3/arity_props / ty3_acyclic
+ty3/arity_props / ty3_predicative
+ty3/arity_props / ty3_repellent
+ty3/arity_props / ty3_sn3
+ty3/dec / ty3_inference
+ty3/fsubst0 / ty3_csubst0
+ty3/fsubst0 / ty3_fsubst0
+ty3/fsubst0 / ty3_subst0
+ty3/fwd / ty3_gen_appl
+ty3/fwd / ty3_gen_bind
+ty3/fwd / ty3_gen_cast
+ty3/fwd / ty3_gen_lref
+ty3/fwd / ty3_gen_sort
+ty3/fwd / tys3_gen_cons
+ty3/fwd / tys3_gen_nil
+ty3/fwd_nf2 / ty3_gen_appl_nf2
+ty3/fwd_nf2 / ty3_inv_appls_lref_nf2
+ty3/fwd_nf2 / ty3_inv_lref_lref_nf2
+ty3/fwd_nf2 / ty3_inv_lref_nf2
+ty3/fwd_nf2 / ty3_inv_lref_nf2_pc3
+ty3/nf2 ty3_nf2_gen ty3_nf2_inv_abst_aux
+ty3/nf2 / ty3_nf2_inv_abst
+ty3/nf2 / ty3_nf2_inv_abst_premise_csort
+ty3/nf2 / ty3_nf2_inv_all
+ty3/nf2 / ty3_nf2_inv_sort
+ty3/pr3 / ty3_sred_pr0
+ty3/pr3 / ty3_sred_pr1
+ty3/pr3 / ty3_sred_pr2
+ty3/pr3 / ty3_sred_pr3
+ty3/pr3 / ty3_sred_wcpr0_pr0
+ty3/pr3_props / ty3_cred_pr2
+ty3/pr3_props / ty3_cred_pr3
+ty3/pr3_props / ty3_gen_lift
+ty3/pr3_props / ty3_sconv
+ty3/pr3_props / ty3_sconv_pc3
+ty3/pr3_props / ty3_sred_back
+ty3/pr3_props / ty3_tred
+ty3/props / ty3_correct
+ty3/props / ty3_gen_abst_abst
+ty3/props / ty3_getl_subst0
+ty3/props / ty3_lift
+ty3/props / ty3_typecheck
+ty3/props / ty3_unique
+ty3/sty0 / ty3_sty0
+ty3/subst1 / ty3_gen_cabbr
+ty3/subst1 / ty3_gen_cvoid
+wcpr0/fwd / wcpr0_gen_head
+wcpr0/fwd / wcpr0_gen_sort
+wcpr0/getl / wcpr0_drop
+wcpr0/getl / wcpr0_drop_back
+wcpr0/getl / wcpr0_getl
+wcpr0/getl / wcpr0_getl_back
+wf3/clear / clear_wf3_trans
+wf3/clear / wf3_clear_conf
+wf3/fwd / wf3_gen_bind1
+wf3/fwd / wf3_gen_flat1
+wf3/fwd / wf3_gen_head2
+wf3/fwd / wf3_gen_sort1
+wf3/getl / getl_wf3_trans
+wf3/getl / wf3_getl_conf
+wf3/props / ty3_shift1
+wf3/props / wf3_idem
+wf3/props / wf3_mono
+wf3/props / wf3_total
+wf3/props / wf3_ty3
+wf3/ty3 / wf3_pc3_conf
+wf3/ty3 / wf3_pr2_conf
+wf3/ty3 / wf3_pr3_conf
+wf3/ty3 / wf3_ty3_conf

diff --git a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
index dcb49f2ce168a1768de1fb831014a2bce79cbf36..ca83c049aa5ac5381d95770a2eac309786a7fac3 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
+++ b/matita/matita/contribs/lambda_delta/basic_2/basic_1.txt
@@ -47,9 +47,6 @@ asucc/fwd asucc_gen_head
 cnt/props cnt_lift
 C/props clt_wf__q_ind
 C/props clt_wf_ind
-C/props chead_ctail
-C/props clt_thead (ctail)
-C/props c_tail_ind
 csuba/arity csuba_arity
 csuba/arity csuba_arity_rev
 csuba/arity arity_appls_appl
@@ -103,7 +100,6 @@ csubv/getl csubv_getl_conf_void
 csubv/props csubv_bind_same
 csubv/props csubv_refl
 drop1/props drop1_cons_tail
-drop/props drop_ctail
 ex0/props aplus_gz_le
 ex0/props aplus_gz_ge
 ex0/props next_plus_gz
@@ -132,18 +128,10 @@ leq/props leq_trans
 leq/props leq_ahead_false_1
 leq/props leq_ahead_false_2
 lift1/fwd lift1_cons_tail
-
-# check #############################################################
-
-lift1/fwd lifts1_flat
 lift1/fwd lifts1_nil
 lift1/fwd lifts1_cons
-lift1/props lift1_free
 lift/props thead_x_lift_y_y
 lift/props lifts_tapp
-
-# waiting ####################################################################
-
 lift/props lifts_inj
 llt/props lweight_repl
 llt/props llt_repl
@@ -156,8 +144,6 @@ 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
@@ -165,15 +151,9 @@ 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/pr3 nf2_pr3_unfold
-nf2/pr3 nf2_pr3_confluence
-
 nf2/props nfs2_tapp
 nf2/props nf2_appls_lref
-
 pc1/props pc1_pr0_r
 pc1/props pc1_pr0_x
 pc1/props pc1_refl
@@ -184,7 +164,6 @@ 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
@@ -232,9 +211,6 @@ pc3/wcpr0 pc3_wcpr0__pc3_wcpr0_t_aux
 pc3/wcpr0 pc3_wcpr0_t
 pc3/wcpr0 pc3_wcpr0
 pr0/fwd pr0_gen_void
-
-# check #############################################################
-
 pr0/dec nf0_dec
 pr0/subst1 pr0_subst1_back
 pr0/subst1 pr0_subst1_fwd
@@ -246,30 +222,13 @@ pr1/props pr1_head_1
 pr1/props pr1_head_2
 pr1/props pr1_comp
 pr1/props pr1_eta
-pr2/clen pr2_gen_ctail
 pr2/fwd pr2_gen_void
-pr2/props pr2_ctail
 pr2/subst1 pr2_gen_cabbr
 pr3/fwd pr3_gen_void
 pr3/pr1 pr3_pr1
-
-pr3/pr3 pr3_strip
-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_eta
-pr3/subst1 pr3_subst1
 pr3/subst1 pr3_gen_cabbr
-sn3/props sn3_cpr3_trans
-
-sn3/props sn3_shift
-sn3/props sn3_change
-sn3/props sn3_gen_def
-sn3/props sn3_cdelta
 sn3/props sns3_lifts
-
 sty0/fwd sty0_gen_sort
 sty0/fwd sty0_gen_lref
 sty0/fwd sty0_gen_bind

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma
new file mode 100644 (file)
index 0000000..22d7ea9
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe.ma
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/computation/cprs.ma".
+include "basic_2/computation/csn.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
+
+definition cpe: lenv → relation term ≝
+                λL,T1,T2. L ⊢ T1 ➡* T2 ∧ L ⊢ 𝐍[T2].
+
+interpretation "context-sensitive parallel evaluation (term)"
+   'PEval L T1 T2 = (cpe L T1 T2).
+
+(* Basic_properties *********************************************************)
+
+(* Basic_1: was: nf2_sn3 *)
+lemma cpe_csn: ∀L,T1. L ⊢ ⬇* T1 → ∃T2. L ⊢ T1 ➡* 𝐍[T2].
+#L #T1 #H @(csn_ind … H) -T1
+#T1 #_ #IHT1
+elim (cnf_dec L T1) /3 width=3/
+* #T #H1T1 #H2T1
+elim (IHT1 … H1T1 H2T1) -IHT1 -H2T1 #T2 * /4 width=3/
+qed.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma
new file mode 100644 (file)
index 0000000..2c3b8b8
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cpe_cpe.ma
@@ -0,0 +1,28 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/computation/cprs_cprs.ma".
+include "basic_2/computation/cpe.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
+
+(* Main properties *********************************************************)
+
+(* Basic_1: was: nf2_pr3_confluence *)
+theorem cpe_mono: ∀L,T,T1. L ⊢ T ➡* 𝐍[T1] → ∀T2. L ⊢ T ➡* 𝐍[T2] → T1 = T2.
+#L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2
+elim (cprs_conf … H1T1 … H1T2) -T #T #HT1
+>(cprs_inv_cnf1 … HT1 H2T1) -T1 #HT2
+>(cprs_inv_cnf1 … HT2 H2T2) -T2 //
+qed-.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
index 5ea230f9b91af1b7d17eda7d453a2779ea36a605..6314894c255b75f7f33a1e5acfcdc4ff6e509604 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs.ma
@@ -60,6 +60,7 @@ lemma cprs_lsubs_conf: ∀L1,T1,T2. L1 ⊢ T1 ➡* T2 →
 /3 width=3/
 qed.
 
+(* Basic_1: was only: pr3_thin_dx *)
 lemma cprs_flat_dx: ∀I,L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L ⊢ T1 ➡* T2 →
                     L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
 #I #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind … HT12) -T2 /3 width=1/
@@ -86,13 +87,15 @@ elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ *
 #W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
 qed-.
 
+(* Basic_1: was: nf2_pr3_unfold *)
 lemma cprs_inv_cnf1: ∀L,T,U. L ⊢ T ➡* U → L ⊢ 𝐍[T] → T = U.
 #L #T #U #H @(cprs_ind_dx … H) -T //
 #T0 #T #H1T0 #_ #IHT #H2T0
 lapply (H2T0 … H1T0) -H1T0 #H destruct /2 width=1/
 qed-.
 
-(* Basic_1: removed theorems 6:
+(* Basic_1: removed theorems 10:
    clear_pr3_trans pr3_cflat pr3_gen_bind
+   pr3_head_1 pr3_head_2 pr3_head_21 pr3_head_12
    pr3_iso_appl_bind pr3_iso_appls_appl_bind pr3_iso_appls_bind
 *)

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
index ca3fe09da3316f6e9c6066f10f4beb06710cc0d9..518c2bd07295a88765cbe26ed0a2785cfaf8971e 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_cprs.ma
@@ -40,6 +40,11 @@ lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T
 lapply (lcpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/
 qed.
 
+(* Basic_1: was: pr3_strip *)
+lemma cprs_strip: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡ T2 →
+                  ∃∃T0. L ⊢ T1 ➡ T0 & L ⊢ T2 ➡* T0.
+/3 width=3/ qed.
+
 (* Advanced inversion lemmas ************************************************)
 
 (* Basic_1: was pr3_gen_appl *)

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma
new file mode 100644 (file)
index 0000000..8859a46
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/cprs_ltpr.ma
@@ -0,0 +1,32 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/reducibility/cpr_ltpr.ma".
+include "basic_2/computation/cprs.ma".
+
+(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+
+(* Properties concerning parallel unfold on terms ***************************)
+
+(* Basic_1: was only: pr3_subst1 *)
+lemma cprs_tpss_ltpr: ∀L1,T1,U1,d,e. L1 ⊢ T1 [d, e] ▶* U1 →
+                      ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 →
+                      ∃∃U2. L2 ⊢ U1 ➡* U2 & L2 ⊢ T2 [d, e] ▶* U2.
+#L1 #T1 #U1 #d #e #HTU1 #L2 #HL12 #T2 #HT12 elim HT12 -T2
+[ #T2 #HT12
+  elim (cpr_tpss_ltpr … HL12 … HT12 … HTU1) -L1 -T1 /3 width=3/
+| #T #T2 #_ #HT2 * #U #HU1 #HTU
+  elim (cpr_tpss_ltpr … HT2 … HTU) -L1 -T // /3 width=3/
+]
+qed.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
index 14655cdee69972365b0c8ab50c60713a3a661f92..27c79d1b609ec080c0a3356353306429d915784d 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn.ma
@@ -82,8 +82,9 @@ qed.
 lemma csn_fwd_flat_dx: ∀I,L,V,T. L ⊢ ⬇* ⓕ{I} V. T → L ⊢ ⬇* T.
 /2 width=5/ qed-.
 
-(* Basic_1: removed theorems 10:
-            sn3_gen_cflat sn3_cflat
+(* Basic_1: removed theorems 14:
+            sn3_cdelta
+           sn3_gen_cflat sn3_cflat sn3_cpr3_trans sn3_shift sn3_change
            sn3_appl_cast sn3_appl_beta sn3_appl_lref sn3_appl_abbr
            sn3_appl_appls sn3_bind sn3_appl_bind sn3_appls_bind
 *)

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma
index 530fde74c2271de0fef1592f602df1aa7cb5cd16..c32947631c92ef7d6512d20109905835f9233f76 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_cprs.ma
@@ -88,17 +88,6 @@ qed.
 lemma csn_cprs_trans: ∀L,T1. L ⊢ ⬇* T1 → ∀T2. L ⊢ T1 ➡* T2 → L ⊢ ⬇* T2.
 /4 width=3/ qed.
 
-(* Basic_1: was: nf2_sn3 *)
-lemma csn_cwn: ∀L,T1. L ⊢ ⬇* T1 →
-               ∃∃T2. L ⊢ T1 ➡* T2 & L ⊢ 𝐍[T2].
-#L #T1 #H elim H -T1 #T1 #_ #IHT1
-elim (cnf_dec L T1)
-[ -IHT1 /2 width=3/
-| * #T2 #HLT12 #HT12
-  elim (IHT1 T2 ? ?) -IHT1 // /2 width=1/ -HT12 /3 width=3/
-]
-qed.
-
 (* Main eliminators *********************************************************)
 
 lemma csn_ind_cprs: ∀L. ∀R:predicate term.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
index b658f9bc81cdc70114e21f63145dff10a3088510..93e22f77afe392ca40be237d6061d0b57041fe87 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/computation/csn_lift.ma
@@ -88,6 +88,17 @@ elim (eq_false_inv_tpair_dx … H2) -H2
 ]
 qed.
 
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was: sn3_gen_def *)
+lemma csn_inv_lref_abbr: ∀L,K,V,i. ⇩[0, i] L ≡ K. ⓓV → L ⊢ ⬇* #i → K ⊢ ⬇* V.
+#L #K #V #i #HLK #Hi
+elim (lift_total V 0 (i+1)) #V0 #HV0
+lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
+@(csn_inv_lift … H0LK … HV0) -H0LK
+@(csn_cpr_trans … Hi) -Hi /2 width=6/
+qed-.
+
 (* Main properties **********************************************************)
 
 theorem csn_acp: acp cpr (eq …) (csn …).

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
index dc2c643b96873915348ede02dd29f38941044464..ba94738a85847b3a9327fd17d492797210605299 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv.ma
@@ -36,3 +36,5 @@ interpretation "abbreviation (local environment)"
 
 interpretation "abstraction (local environment)"
    'DxAbst L T = (LPair L Abst T).
+
+(* Basic_1: removed theorems 2: chead_ctail c_tail_ind *)

diff --git a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
index bc8ffce87e77e97eb79f151d4c0b69d3940ffc3d..990b5c5d07639c7d2060638967778e39e130461a 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/grammar/lenv_weight.ma
@@ -24,4 +24,5 @@ let rec lw L ≝ match L with
 
 interpretation "weight (local environment)" 'Weight L = (lw L).
 
-(* Basic_1: removed theorems 2: clt_cong clt_head *)
+(* Basic_1: removed theorems 2: clt_cong clt_head clt_thead *)
+(* Basic_1: note: clt_thead should be renamed clt_ctail *)

diff --git a/matita/matita/contribs/lambda_delta/basic_2/notation.ma b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
index a9fca999c050e096e09b2b90f9e619d5dfcc01c0..ce9a370e29af537dfad8993acb1ab9983a693a1a 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/notation.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/notation.ma
@@ -146,6 +146,10 @@ notation "hvbox( ⇩ [ d , break e ] break L1 ≡ break L2 )"
    non associative with precedence 45
    for @{ 'RDrop $d $e $L1 $L2 }.
 
+notation "hvbox( L ⊢ break ⌘ [ T ] ≡ break k )"
+   non associative with precedence 45
+   for @{ 'ICM $L $T $k }.
+
 notation "hvbox( T1 break [ d , break e ] ▶ break T2 )"
    non associative with precedence 45
    for @{ 'PSubst $T1 $d $e $T2 }.
@@ -274,6 +278,10 @@ notation "hvbox( L1 ⊢ ➡* break L2 )"
    non associative with precedence 45
    for @{ 'CPRedStar $L1 $L2 }.
 
+notation "hvbox( L ⊢ break term 90 T1 ➡* break 𝐍 [ T2 ] )"
+   non associative with precedence 45
+   for @{ 'PEval $L $T1 $T2 }.
+
 notation "hvbox( ⬇ * T  )"
    non associative with precedence 45
    for @{ 'SN $T }.

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
index b97150df76d30ee9f422bf4eafc08d91e18bca95..00647e43ce09636f76efdb0e9f4c7c883644840f 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cnf.ma
@@ -30,6 +30,7 @@ lemma cnf_sort: ∀L,k. L ⊢ 𝐍[⋆k].
 >(cpr_inv_sort1 … H) //
 qed.
 
+(* Basic_1: was: nf2_dec *)
 axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨
                ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → False).
 

diff --git a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
index fdbc9458fc00e636bf53c677803bf2a6f40559cc..953145592afe77e010941f053f3c60db33cde01c 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/reducibility/cpr.ma
@@ -107,8 +107,9 @@ elim (tpr_inv_cast1 … H) -H /3 width=3/
 elim (tpss_inv_flat1 … HU2) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /4 width=5/
 qed-.
 
-(* Basic_1: removed theorems 4: 
+(* Basic_1: removed theorems 6: 
             pr2_head_2 pr2_cflat pr2_gen_cflat clear_pr2_trans
+           pr2_gen_ctail pr2_ctail
    Basic_1: removed local theorems 3:
             pr2_free_free pr2_free_delta pr2_delta_delta
 *)

diff --git a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
index e667c7cde14f83e07ea49bcf135663d1d324e621..3dfc3563906caeb81ffd56ea44b0221bd07869b2 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/substitution/ldrop.ma
@@ -211,8 +211,8 @@ lemma ldrop_fwd_O1_length: ∀L1,L2,e. ⇩[0, e] L1 ≡ L2 → |L2| = |L1| - e.
 ]
 qed-.
 
-(* Basic_1: removed theorems 49:
-            drop_skip_flat
+(* Basic_1: removed theorems 50:
+            drop_ctail 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

diff --git a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma
index b757b9cb781cda0eda6a1cb12860aac44e4927f6..1690c9f6639c772281fabc0a70da8e29a0c5660c 100644 (file)
--- a/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma
+++ b/matita/matita/contribs/lambda_delta/basic_2/unfold/lifts_vector.ma
@@ -29,6 +29,7 @@ interpretation "generic relocation (vector)"
 
 (* Basic inversion lemmas ***************************************************)
 
+(* Basic_1: was: lifts1_flat (left to right) *)
 lemma lifts_inv_applv1: ∀V1s,U1,T2,des. ⇧*[des] Ⓐ V1s. U1 ≡ T2 →
                         ∃∃V2s,U2. ⇧*[des] V1s ≡ V2s & ⇧*[des] U1 ≡ U2 &
                                   T2 = Ⓐ V2s. U2.
@@ -44,6 +45,7 @@ qed-.
 
 (* Basic properties *********************************************************)
 
+(* Basic_1: was: lifts1_flat (right to left) *)
 lemma lifts_applv: ∀V1s,V2s,des. ⇧*[des] V1s ≡ V2s →
                    ∀T1,T2. ⇧*[des] T1 ≡ T2 →
                    ⇧*[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.

diff --git a/matita/matita/contribs/lambda_delta/orig.sh b/matita/matita/contribs/lambda_delta/orig.sh
new file mode 100644 (file)
index 0000000..83b1fa1
--- /dev/null
+++ b/matita/matita/contribs/lambda_delta/orig.sh
@@ -0,0 +1,4 @@
+F=`find $1 -name "*.ma" -or -name "*.txt"` 
+while read A A A; do
+   if grep -q "$A" $F; then true; else echo $A; fi
+done

diff --git a/matita/matita/lib/basics/star.ma b/matita/matita/lib/basics/star.ma
index bac2e771c23672b73fa9d936dc5fac913d3ac461..bff1aaeef80042a2ae2e838317d0c5ed5c858a58 100644 (file)
--- a/matita/matita/lib/basics/star.ma
+++ b/matita/matita/lib/basics/star.ma
@@ -191,3 +191,10 @@ lemma TC_star_ind_dx: ∀A,R. reflexive A R →
 #A #R #HR #a2 #P #Ha2 #H #a1 #Ha12
 @(TC_star_ind_dx_aux … HR … Ha2 H … Ha12) //
 qed-.
+
+definition Conf3: ∀A. relation A → relation A → Prop ≝ λA,S,R.
+                  ∀a,a1. S a1 a → ∀a2. R a1 a2 → S a2 a.
+
+lemma TC_Conf3: ∀A,S,R. Conf3 A S R → Conf3 A S (TC … R).
+#A #S #R #HSR #a #a1 #Ha1 #a2 #H elim H -a2 /2 width=3/
+qed.

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 98e9f1e61c8c8c05b6ec0739d1adb78a05b454e6..b276fe4bb0360e08f08492d90cdd859fdc6e9e8c 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1503,6 +1503,7 @@ let load_predefined_virtuals () =
 ;;
 
 let predefined_classes = [
+ ["#"; "⌘"; ];
  ["-"; "÷"; "⊢"; ];
  ["="; "≃"; "≈"; "≝"; "≡"; "≅"; "≐"; "≑"; ];  
  ["→"; "⇝"; "⇾"; "⤍"; "⤏"; "⤳"; ] ;