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
-PACKAGES = Ground_2 Basic_2 Apps_2
+PACKAGES = ground_2 basic_2 apps_2
all:
(* *)
(**************************************************************************)
-include "Ground_2/tri.ma".
-include "Basic_2/substitution/lift.ma".
-include "Apps_2/functional/notation.ma".
+include "ground_2/tri.ma".
+include "basic_2/substitution/lift.ma".
+include "apps_2/functional/notation.ma".
(* RELOCATION ***************************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_vector.ma".
-include "Basic_2/grammar/genv.ma".
+include "basic_2/grammar/term_vector.ma".
+include "basic_2/grammar/genv.ma".
(* REDUCTION AND TYPE MACHINE ***********************************************)
(* *)
(**************************************************************************)
-include "Apps_2/functional/rtm.ma".
+include "apps_2/functional/rtm.ma".
(* REDUCTION AND TYPE MACHINE ***********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/delift_lift.ma".
-include "Apps_2/functional/lift.ma".
+include "basic_2/unfold/delift_lift.ma".
+include "apps_2/functional/lift.ma".
(* CORE SUBSTITUTION ********************************************************)
+++ /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
-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
-csuba/clear csuba_clear_conf
-csuba/clear csuba_clear_trans
-csuba/drop csuba_drop_abbr
-csuba/drop csuba_drop_abst
-csuba/drop csuba_drop_abst_rev
-csuba/drop csuba_drop_abbr_rev
-csuba/fwd csuba_gen_abbr
-csuba/fwd csuba_gen_void
-csuba/fwd csuba_gen_abst
-csuba/fwd csuba_gen_flat
-csuba/fwd csuba_gen_bind
-csuba/fwd csuba_gen_abst_rev
-csuba/fwd csuba_gen_void_rev
-csuba/fwd csuba_gen_abbr_rev
-csuba/fwd csuba_gen_flat_rev
-csuba/fwd csuba_gen_bind_rev
-csuba/getl csuba_getl_abbr
-csuba/getl csuba_getl_abst
-csuba/getl csuba_getl_abst_rev
-csuba/getl csuba_getl_abbr_rev
-csuba/props csuba_refl
-csubc/arity csubc_arity_conf
-csubc/arity csubc_arity_trans
-csubc/csuba csubc_csuba
-csubc/drop1 drop1_csubc_trans
-csubc/drop drop_csubc_trans
-csubt/clear csubt_clear_conf
-csubt/csuba csubt_csuba
-csubt/drop csubt_drop_flat
-csubt/drop csubt_drop_abbr
-csubt/drop csubt_drop_abst
-csubt/fwd csubt_gen_abbr
-csubt/fwd csubt_gen_abst
-csubt/fwd csubt_gen_flat
-csubt/fwd csubt_gen_bind
-csubt/getl csubt_getl_abbr
-csubt/getl csubt_getl_abst
-csubt/pc3 csubt_pr2
-csubt/pc3 csubt_pc3
-csubt/props csubt_refl
-csubt/ty3 csubt_ty3
-csubt/ty3 csubt_ty3_ld
-csubv/clear csubv_clear_conf
-csubv/clear csubv_clear_conf_void
-csubv/drop csubv_drop_conf
-csubv/getl csubv_getl_conf
-csubv/getl csubv_getl_conf_void
-csubv/props csubv_bind_same
-csubv/props csubv_refl
-drop1/props drop1_cons_tail
-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
-fsubst0/fwd fsubst0_gen_base
-leq/asucc asucc_repl
-leq/asucc asucc_inj
-leq/asucc leq_asucc
-leq/asucc leq_ahead_asucc_false
-leq/asucc leq_asucc_false
-leq/fwd leq_gen_sort1
-leq/fwd leq_gen_head1
-leq/fwd leq_gen_sort2
-leq/fwd leq_gen_head2
-leq/props ahead_inj_snd
-leq/props leq_refl
-leq/props leq_eq
-leq/props leq_sym
-leq/props leq_trans
-leq/props leq_ahead_false_1
-leq/props leq_ahead_false_2
-lift1/fwd lift1_cons_tail
-
-# 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
-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/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
-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 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_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/fwd pr0_gen_void
-
-# check #############################################################
-
-pr0/dec nf0_dec
-pr0/subst1 pr0_subst1_back
-pr0/subst1 pr0_subst1_fwd
-pr1/pr1 pr1_strip
-pr1/pr1 pr1_confluence
-pr1/props pr1_pr0
-pr1/props pr1_t
-pr1/props pr1_head_1
-pr1/props pr1_head_2
-pr1/props pr1_comp
-pr1/props pr1_eta
-pr2/clen pr2_gen_ctail
-pr2/fwd pr2_gen_void
-pr2/props pr2_ctail
-pr2/subst1 pr2_gen_cabbr
-
-pr3/fwd pr3_gen_abst
-pr3/fwd pr3_gen_lref
-pr3/fwd pr3_gen_void
-pr3/fwd pr3_gen_appl
-pr3/fwd pr3_gen_bind
-pr3/iso pr3_iso_appls_abbr
-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/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_flat
-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 sn3_appl_lref
-sn3/props sn3_appl_abbr
-sn3/props sn3_appl_cast
-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_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
-subst/fwd subst_sort
-subst/fwd subst_lref_lt
-subst/fwd subst_lref_eq
-subst/fwd subst_lref_gt
-subst/fwd subst_head
-subst/props subst_lift_SO
-subst/props subst_subst0
-T/dec binder_dec
-T/dec abst_dec
-tlist/props tslt_wf__q_ind
-tlist/props tslt_wf_ind
-tlist/props theads_tapp
-tlist/props tcons_tapp_ex
-tlist/props tlist_ind_rev
-ty3/arity ty3_arity
-ty3/arity_props ty3_predicative
-ty3/arity_props ty3_repellent
-ty3/arity_props ty3_acyclic
-ty3/arity_props ty3_sn3
-ty3/dec ty3_inference
-ty3/fsubst0 ty3_fsubst0
-ty3/fsubst0 ty3_csubst0
-ty3/fsubst0 ty3_subst0
-ty3/fwd ty3_gen_sort
-ty3/fwd ty3_gen_lref
-ty3/fwd ty3_gen_bind
-ty3/fwd ty3_gen_appl
-ty3/fwd ty3_gen_cast
-ty3/fwd tys3_gen_nil
-ty3/fwd tys3_gen_cons
-ty3/fwd_nf2 ty3_gen_appl_nf2
-ty3/fwd_nf2 ty3_inv_lref_nf2_pc3
-ty3/fwd_nf2 ty3_inv_lref_nf2
-ty3/fwd_nf2 ty3_inv_appls_lref_nf2
-ty3/fwd_nf2 ty3_inv_lref_lref_nf2
-ty3/nf2 ty3_nf2_inv_abst_premise_csort
-ty3/nf2 ty3_nf2_inv_all
-ty3/nf2 ty3_nf2_inv_sort
-ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux
-ty3/nf2 ty3_nf2_inv_abst
-ty3/pr3 ty3_sred_wcpr0_pr0
-ty3/pr3 ty3_sred_pr0
-ty3/pr3 ty3_sred_pr1
-ty3/pr3 ty3_sred_pr2
-ty3/pr3 ty3_sred_pr3
-ty3/pr3_props ty3_cred_pr2
-ty3/pr3_props ty3_cred_pr3
-ty3/pr3_props ty3_gen_lift
-ty3/pr3_props ty3_tred
-ty3/pr3_props ty3_sconv_pc3
-ty3/pr3_props ty3_sred_back
-ty3/pr3_props ty3_sconv
-ty3/props ty3_lift
-ty3/props ty3_correct
-ty3/props ty3_unique
-ty3/props ty3_gen_abst_abst
-ty3/props ty3_typecheck
-ty3/props ty3_getl_subst0
-ty3/sty0 ty3_sty0
-ty3/subst1 ty3_gen_cabbr
-ty3/subst1 ty3_gen_cvoid
-wf3/clear wf3_clear_conf
-wf3/clear clear_wf3_trans
-wf3/fwd wf3_gen_sort1
-wf3/fwd wf3_gen_bind1
-wf3/fwd wf3_gen_flat1
-wf3/fwd wf3_gen_head2
-wf3/getl wf3_getl_conf
-wf3/getl getl_wf3_trans
-wf3/props wf3_mono
-wf3/props wf3_total
-wf3/props ty3_shift1
-wf3/props wf3_idem
-wf3/props wf3_ty3
-wf3/ty3 wf3_pr2_conf
-wf3/ty3 wf3_pr3_conf
-wf3/ty3 wf3_pc3_conf
-wf3/ty3 wf3_ty3_conf
-
-# check ######################################################################
--- /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
+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
+csuba/clear csuba_clear_conf
+csuba/clear csuba_clear_trans
+csuba/drop csuba_drop_abbr
+csuba/drop csuba_drop_abst
+csuba/drop csuba_drop_abst_rev
+csuba/drop csuba_drop_abbr_rev
+csuba/fwd csuba_gen_abbr
+csuba/fwd csuba_gen_void
+csuba/fwd csuba_gen_abst
+csuba/fwd csuba_gen_flat
+csuba/fwd csuba_gen_bind
+csuba/fwd csuba_gen_abst_rev
+csuba/fwd csuba_gen_void_rev
+csuba/fwd csuba_gen_abbr_rev
+csuba/fwd csuba_gen_flat_rev
+csuba/fwd csuba_gen_bind_rev
+csuba/getl csuba_getl_abbr
+csuba/getl csuba_getl_abst
+csuba/getl csuba_getl_abst_rev
+csuba/getl csuba_getl_abbr_rev
+csuba/props csuba_refl
+csubc/arity csubc_arity_conf
+csubc/arity csubc_arity_trans
+csubc/csuba csubc_csuba
+csubc/drop1 drop1_csubc_trans
+csubc/drop drop_csubc_trans
+csubt/clear csubt_clear_conf
+csubt/csuba csubt_csuba
+csubt/drop csubt_drop_flat
+csubt/drop csubt_drop_abbr
+csubt/drop csubt_drop_abst
+csubt/fwd csubt_gen_abbr
+csubt/fwd csubt_gen_abst
+csubt/fwd csubt_gen_flat
+csubt/fwd csubt_gen_bind
+csubt/getl csubt_getl_abbr
+csubt/getl csubt_getl_abst
+csubt/pc3 csubt_pr2
+csubt/pc3 csubt_pc3
+csubt/props csubt_refl
+csubt/ty3 csubt_ty3
+csubt/ty3 csubt_ty3_ld
+csubv/clear csubv_clear_conf
+csubv/clear csubv_clear_conf_void
+csubv/drop csubv_drop_conf
+csubv/getl csubv_getl_conf
+csubv/getl csubv_getl_conf_void
+csubv/props csubv_bind_same
+csubv/props csubv_refl
+drop1/props drop1_cons_tail
+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
+fsubst0/fwd fsubst0_gen_base
+leq/asucc asucc_repl
+leq/asucc asucc_inj
+leq/asucc leq_asucc
+leq/asucc leq_ahead_asucc_false
+leq/asucc leq_asucc_false
+leq/fwd leq_gen_sort1
+leq/fwd leq_gen_head1
+leq/fwd leq_gen_sort2
+leq/fwd leq_gen_head2
+leq/props ahead_inj_snd
+leq/props leq_refl
+leq/props leq_eq
+leq/props leq_sym
+leq/props leq_trans
+leq/props leq_ahead_false_1
+leq/props leq_ahead_false_2
+lift1/fwd lift1_cons_tail
+
+# 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
+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/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
+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 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_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/fwd pr0_gen_void
+
+# check #############################################################
+
+pr0/dec nf0_dec
+pr0/subst1 pr0_subst1_back
+pr0/subst1 pr0_subst1_fwd
+pr1/pr1 pr1_strip
+pr1/pr1 pr1_confluence
+pr1/props pr1_pr0
+pr1/props pr1_t
+pr1/props pr1_head_1
+pr1/props pr1_head_2
+pr1/props pr1_comp
+pr1/props pr1_eta
+pr2/clen pr2_gen_ctail
+pr2/fwd pr2_gen_void
+pr2/props pr2_ctail
+pr2/subst1 pr2_gen_cabbr
+
+pr3/fwd pr3_gen_lref
+pr3/fwd pr3_gen_void
+pr3/fwd pr3_gen_bind
+pr3/iso pr3_iso_appls_abbr
+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/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_flat
+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 sn3_appl_lref
+sn3/props sn3_appl_abbr
+sn3/props sn3_appl_cast
+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_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
+subst/fwd subst_sort
+subst/fwd subst_lref_lt
+subst/fwd subst_lref_eq
+subst/fwd subst_lref_gt
+subst/fwd subst_head
+subst/props subst_lift_SO
+subst/props subst_subst0
+T/dec binder_dec
+T/dec abst_dec
+tlist/props tslt_wf__q_ind
+tlist/props tslt_wf_ind
+tlist/props theads_tapp
+tlist/props tcons_tapp_ex
+tlist/props tlist_ind_rev
+ty3/arity ty3_arity
+ty3/arity_props ty3_predicative
+ty3/arity_props ty3_repellent
+ty3/arity_props ty3_acyclic
+ty3/arity_props ty3_sn3
+ty3/dec ty3_inference
+ty3/fsubst0 ty3_fsubst0
+ty3/fsubst0 ty3_csubst0
+ty3/fsubst0 ty3_subst0
+ty3/fwd ty3_gen_sort
+ty3/fwd ty3_gen_lref
+ty3/fwd ty3_gen_bind
+ty3/fwd ty3_gen_appl
+ty3/fwd ty3_gen_cast
+ty3/fwd tys3_gen_nil
+ty3/fwd tys3_gen_cons
+ty3/fwd_nf2 ty3_gen_appl_nf2
+ty3/fwd_nf2 ty3_inv_lref_nf2_pc3
+ty3/fwd_nf2 ty3_inv_lref_nf2
+ty3/fwd_nf2 ty3_inv_appls_lref_nf2
+ty3/fwd_nf2 ty3_inv_lref_lref_nf2
+ty3/nf2 ty3_nf2_inv_abst_premise_csort
+ty3/nf2 ty3_nf2_inv_all
+ty3/nf2 ty3_nf2_inv_sort
+ty3/nf2 ty3_nf2_gen__ty3_nf2_inv_abst_aux
+ty3/nf2 ty3_nf2_inv_abst
+ty3/pr3 ty3_sred_wcpr0_pr0
+ty3/pr3 ty3_sred_pr0
+ty3/pr3 ty3_sred_pr1
+ty3/pr3 ty3_sred_pr2
+ty3/pr3 ty3_sred_pr3
+ty3/pr3_props ty3_cred_pr2
+ty3/pr3_props ty3_cred_pr3
+ty3/pr3_props ty3_gen_lift
+ty3/pr3_props ty3_tred
+ty3/pr3_props ty3_sconv_pc3
+ty3/pr3_props ty3_sred_back
+ty3/pr3_props ty3_sconv
+ty3/props ty3_lift
+ty3/props ty3_correct
+ty3/props ty3_unique
+ty3/props ty3_gen_abst_abst
+ty3/props ty3_typecheck
+ty3/props ty3_getl_subst0
+ty3/sty0 ty3_sty0
+ty3/subst1 ty3_gen_cabbr
+ty3/subst1 ty3_gen_cvoid
+wf3/clear wf3_clear_conf
+wf3/clear clear_wf3_trans
+wf3/fwd wf3_gen_sort1
+wf3/fwd wf3_gen_bind1
+wf3/fwd wf3_gen_flat1
+wf3/fwd wf3_gen_head2
+wf3/getl wf3_getl_conf
+wf3/getl getl_wf3_trans
+wf3/props wf3_mono
+wf3/props wf3_total
+wf3/props ty3_shift1
+wf3/props wf3_idem
+wf3/props wf3_ty3
+wf3/ty3 wf3_pr2_conf
+wf3/ty3 wf3_pr3_conf
+wf3/ty3 wf3_pc3_conf
+wf3/ty3 wf3_ty3_conf
+
+# check ######################################################################
(* *)
(**************************************************************************)
-include "Basic_2/unfold/ldrops.ma".
+include "basic_2/unfold/ldrops.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/lifts_lifts.ma".
-include "Basic_2/unfold/ldrops_ldrops.ma".
-include "Basic_2/static/aaa_lifts.ma".
-include "Basic_2/static/aaa_aaa.ma".
-include "Basic_2/computation/lsubc_ldrops.ma".
+include "basic_2/unfold/lifts_lifts.ma".
+include "basic_2/unfold/ldrops_ldrops.ma".
+include "basic_2/static/aaa_lifts.ma".
+include "basic_2/static/aaa_aaa.ma".
+include "basic_2/computation/lsubc_ldrops.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/aarity.ma".
-include "Basic_2/unfold/gr2_gr2.ma".
-include "Basic_2/unfold/lifts_lift_vector.ma".
-include "Basic_2/unfold/ldrops_ldrop.ma".
-include "Basic_2/computation/acp.ma".
+include "basic_2/grammar/aarity.ma".
+include "basic_2/unfold/gr2_gr2.ma".
+include "basic_2/unfold/lifts_lift_vector.ma".
+include "basic_2/unfold/ldrops_ldrop.ma".
+include "basic_2/computation/acp.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/cpr_lift.ma".
-include "Basic_2/reducibility/cpr_cpr.ma".
-include "Basic_2/reducibility/lcpr_cpr.ma".
-include "Basic_2/computation/cprs_lcpr.ma".
+include "basic_2/reducibility/cpr_lift.ma".
+include "basic_2/reducibility/cpr_cpr.ma".
+include "basic_2/reducibility/lcpr_cpr.ma".
+include "basic_2/computation/cprs_lcpr.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/ltpr_tps.ma".
-include "Basic_2/reducibility/cpr_ltpss.ma".
-include "Basic_2/reducibility/lcpr.ma".
-include "Basic_2/computation/cprs.ma".
+include "basic_2/reducibility/ltpr_tps.ma".
+include "basic_2/reducibility/cpr_ltpss.ma".
+include "basic_2/reducibility/lcpr.ma".
+include "basic_2/computation/cprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
(* *)
(**************************************************************************)
-include "Basic_2/computation/cprs_cprs.ma".
-include "Basic_2/computation/lcprs_lcprs.ma".
+include "basic_2/computation/cprs_cprs.ma".
+include "basic_2/computation/lcprs_lcprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/cpr_lift.ma".
-include "Basic_2/computation/cprs.ma".
+include "basic_2/reducibility/cpr_lift.ma".
+include "basic_2/computation/cprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was: pr3_gen_abst *)
+lemma cprs_inv_abst1: ∀I,W,L,V1,T1,U2. L ⊢ ⓛV1. T1 ➡* U2 →
+ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L. ⓑ{I} W ⊢ T1 ➡* T2 &
+ U2 = ⓛV2. T2.
+#I #W #L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /2 width=5/
+#U #U2 #_ #HU2 * #V #T #HV1 #HT1 #H destruct
+elim (cpr_inv_abst1 … HU2 I W) -HU2 #V2 #T2 #HV2 #HT2 #H destruct /3 width=5/
+qed-.
+
(* Relocation properties ****************************************************)
(* Basic_1: was: pr3_lift *)
-HTU1 #U #U2 #_ #HU2 * #T #HTU #HT1
elim (cpr_inv_lift … HLK … HTU … HU2) -U -HLK /3 width=5/
qed.
+
(* *)
(**************************************************************************)
-include "Basic_2/grammar/tstc.ma".
+include "basic_2/grammar/tstc.ma".
(*
-include "Basic_2/reducibility/cpr_lift.ma".
-include "Basic_2/reducibility/lcpr_cpr.ma".
+include "basic_2/reducibility/cpr_lift.ma".
+include "basic_2/reducibility/lcpr_cpr.ma".
*)
-include "Basic_2/computation/cprs_cprs.ma".
+include "basic_2/computation/cprs_cprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/tstc_vector.ma".
-include "Basic_2/substitution/lift_vector.ma".
-include "Basic_2/computation/cprs_tstc.ma".
+include "basic_2/grammar/tstc_vector.ma".
+include "basic_2/substitution/lift_vector.ma".
+include "basic_2/computation/cprs_tstc.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/cpr.ma".
-include "Basic_2/reducibility/cnf.ma".
+include "basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/cnf.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* *)
(**************************************************************************)
-include "Basic_2/computation/acp_aaa.ma".
-include "Basic_2/computation/csn_lcpr_vector.ma".
+include "basic_2/computation/acp_aaa.ma".
+include "basic_2/computation/csn_lcpr_vector.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/cpr_cpr.ma".
-include "Basic_2/computation/csn.ma".
+include "basic_2/reducibility/cpr_cpr.ma".
+include "basic_2/computation/csn.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* *)
(**************************************************************************)
-include "Basic_2/computation/cprs.ma".
-include "Basic_2/computation/csn.ma".
+include "basic_2/computation/cprs.ma".
+include "basic_2/computation/csn.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/tstc_tstc.ma".
-include "Basic_2/computation/cprs_cprs.ma".
-include "Basic_2/computation/csn_lift.ma".
-include "Basic_2/computation/csn_cpr.ma".
-include "Basic_2/computation/csn_cprs.ma".
+include "basic_2/grammar/tstc_tstc.ma".
+include "basic_2/computation/cprs_cprs.ma".
+include "basic_2/computation/csn_lift.ma".
+include "basic_2/computation/csn_cpr.ma".
+include "basic_2/computation/csn_cprs.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* *)
(**************************************************************************)
-include "Basic_2/computation/acp_cr.ma".
-include "Basic_2/computation/cprs_tstc_vector.ma".
-include "Basic_2/computation/csn_lcpr.ma".
-include "Basic_2/computation/csn_vector.ma".
+include "basic_2/computation/acp_cr.ma".
+include "basic_2/computation/cprs_tstc_vector.ma".
+include "basic_2/computation/csn_lcpr.ma".
+include "basic_2/computation/csn_vector.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/cnf_lift.ma".
-include "Basic_2/computation/acp.ma".
-include "Basic_2/computation/csn.ma".
+include "basic_2/reducibility/cnf_lift.ma".
+include "basic_2/computation/acp.ma".
+include "basic_2/computation/csn.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_vector.ma".
-include "Basic_2/computation/csn.ma".
+include "basic_2/grammar/term_vector.ma".
+include "basic_2/computation/csn.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERM VECTORS **********************)
lemma csnv_inv_cons: ∀L,T,Ts. L ⊢ ⬇* T :: Ts → L ⊢ ⬇* T ∧ L ⊢ ⬇* Ts.
/2 width=3/ qed-.
-include "Basic_2/computation/csn_cpr.ma".
+include "basic_2/computation/csn_cpr.ma".
lemma csn_fwd_applv: ∀L,T,Vs. L ⊢ ⬇* Ⓐ Vs. T → L ⊢ ⬇* Vs ∧ L ⊢ ⬇* T.
#L #T #Vs elim Vs -Vs /2 width=1/
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/lcpr.ma".
+include "basic_2/reducibility/lcpr.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/lcpr_cpr.ma".
-include "Basic_2/computation/cprs.ma".
-include "Basic_2/computation/lcprs.ma".
+include "basic_2/reducibility/lcpr_cpr.ma".
+include "basic_2/computation/cprs.ma".
+include "basic_2/computation/lcprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************)
(* *)
(**************************************************************************)
-include "Basic_2/computation/lcprs_cprs.ma".
+include "basic_2/computation/lcprs_cprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *************)
(* *)
(**************************************************************************)
-include "Basic_2/static/aaa.ma".
-include "Basic_2/computation/acp_cr.ma".
+include "basic_2/static/aaa.ma".
+include "basic_2/computation/acp_cr.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
(* *)
(**************************************************************************)
-include "Basic_2/static/aaa_lift.ma".
-include "Basic_2/computation/acp_cr.ma".
-include "Basic_2/computation/lsubc.ma".
+include "basic_2/static/aaa_lift.ma".
+include "basic_2/computation/acp_cr.ma".
+include "basic_2/computation/lsubc.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
(* *)
(**************************************************************************)
-include "Basic_2/computation/lsubc_ldrop.ma".
+include "basic_2/computation/lsubc_ldrop.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
(* *)
(**************************************************************************)
-include "Basic_2/static/lsuba.ma".
-include "Basic_2/computation/acp_aaa.ma".
+include "basic_2/static/lsuba.ma".
+include "basic_2/computation/acp_aaa.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON TERMS ***************************)
(* *)
(**************************************************************************)
-include "Basic_2/conversion/cpc.ma".
+include "basic_2/conversion/cpc.ma".
(* CONTEXT-SENSITIVE PARALLEL CONVERSION ON TERMS ***************************)
(* *)
(**************************************************************************)
-include "Basic_2/conversion/cpc.ma".
+include "basic_2/conversion/cpc.ma".
(* CONTEXT-SENSITIVE PARALLEL EQUIVALENCE ON TERMS **************************)
* [ suggested invocation to start formal specifications with ]
*)
-include "Ground_2/star.ma".
-include "Basic_2/notation.ma".
+include "ground_2/star.ma".
+include "basic_2/notation.ma".
(* ATOMIC ARITY *************************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/lenv.ma".
+include "basic_2/grammar/lenv.ma".
(* SHIFT OF A CLOSURE *******************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/lenv_weight.ma".
-include "Basic_2/grammar/cl_shift.ma".
+include "basic_2/grammar/lenv_weight.ma".
+include "basic_2/grammar/cl_shift.ma".
(* WEIGHT OF A CLOSURE ******************************************************)
(* *)
(**************************************************************************)
-include "Ground_2/list.ma".
-include "Basic_2/grammar/term.ma".
+include "ground_2/list.ma".
+include "basic_2/grammar/term.ma".
(* GLOBAL ENVIRONMENTS ******************************************************)
(* *)
(**************************************************************************)
-include "Ground_2/arith.ma".
-include "Basic_2/notation.ma".
+include "ground_2/arith.ma".
+include "basic_2/notation.ma".
(* ITEMS ********************************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term.ma".
+include "basic_2/grammar/term.ma".
(* LOCAL ENVIRONMENTS *******************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/lenv.ma".
+include "basic_2/grammar/lenv.ma".
(* LENGTH OF A LOCAL ENVIRONMENT ********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_weight.ma".
-include "Basic_2/grammar/lenv.ma".
+include "basic_2/grammar/term_weight.ma".
+include "basic_2/grammar/lenv.ma".
(* WEIGHT OF A LOCAL ENVIRONMENT ********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/lenv_length.ma".
+include "basic_2/grammar/lenv_length.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR SUBSTITUTION ****************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/item.ma".
+include "basic_2/grammar/item.ma".
(* TERMS ********************************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term.ma".
+include "basic_2/grammar/term.ma".
(* SIMPLE (NEUTRAL) TERMS ***************************************************)
(* *)
(**************************************************************************)
-include "Ground_2/list.ma".
-include "Basic_2/grammar/term.ma".
+include "ground_2/list.ma".
+include "basic_2/grammar/term.ma".
(* TERMS ********************************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term.ma".
+include "basic_2/grammar/term.ma".
(* WEIGHT OF A TERM *********************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_simple.ma".
+include "basic_2/grammar/term_simple.ma".
(* SAME HEAD TERM FORMS *****************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_simple.ma".
+include "basic_2/grammar/term_simple.ma".
(* SAME TOP TERM CONSTRUCTOR ************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/tstc.ma".
+include "basic_2/grammar/tstc.ma".
(* SAME TOP TERM CONSTRUCTOR ************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_vector.ma".
-include "Basic_2/grammar/tstc.ma".
+include "basic_2/grammar/term_vector.ma".
+include "basic_2/grammar/tstc.ma".
(* SAME TOP TERM CONSTRUCTOR ************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/cpr.ma".
(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/cpr_lift.ma".
-include "Basic_2/reducibility/cnf.ma".
+include "basic_2/reducibility/cpr_lift.ma".
+include "basic_2/reducibility/cnf.ma".
(* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/cl_shift.ma".
-include "Basic_2/unfold/tpss.ma".
-include "Basic_2/reducibility/tpr.ma".
+include "basic_2/grammar/cl_shift.ma".
+include "basic_2/unfold/tpss.ma".
+include "basic_2/reducibility/tpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/tpr_tpr.ma".
-include "Basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/tpr_tpr.ma".
+include "basic_2/reducibility/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/tpss_lift.ma".
-include "Basic_2/reducibility/tpr_lift.ma".
-include "Basic_2/reducibility/cpr.ma".
+include "basic_2/unfold/tpss_lift.ma".
+include "basic_2/reducibility/tpr_lift.ma".
+include "basic_2/reducibility/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/tpr_tpss.ma".
-include "Basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/ltpss_tpss.ma".
-include "Basic_2/reducibility/cpr.ma".
+include "basic_2/unfold/ltpss_tpss.ma".
+include "basic_2/reducibility/cpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON TERMS ****************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/ltpss.ma".
-include "Basic_2/reducibility/ltpr.ma".
+include "basic_2/unfold/ltpss.ma".
+include "basic_2/reducibility/ltpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/ltpss_ltpss.ma".
-include "Basic_2/reducibility/cpr.ma".
-include "Basic_2/reducibility/lcpr.ma".
+include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/reducibility/cpr.ma".
+include "basic_2/reducibility/lcpr.ma".
(* CONTEXT-SENSITIVE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS *************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/tpr.ma".
+include "basic_2/reducibility/tpr.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/tpr_lift.ma".
-include "Basic_2/reducibility/ltpr.ma".
+include "basic_2/reducibility/tpr_lift.ma".
+include "basic_2/reducibility/ltpr.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/ltpr_ldrop.ma".
+include "basic_2/reducibility/ltpr_ldrop.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/trf.ma".
+include "basic_2/reducibility/trf.ma".
(* CONTEXT-FREE IRREDUCIBLE TERMS *******************************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/tpr.ma".
+include "basic_2/reducibility/tpr.ma".
(* CONTEXT-FREE NORMAL TERMS ************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/tps_lift.ma".
-include "Basic_2/reducibility/tif.ma".
-include "Basic_2/reducibility/tnf.ma".
+include "basic_2/substitution/tps_lift.ma".
+include "basic_2/reducibility/tif.ma".
+include "basic_2/reducibility/tnf.ma".
(* CONTEXT-FREE NORMAL TERMS ************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/tps.ma".
+include "basic_2/substitution/tps.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/tps_lift.ma".
-include "Basic_2/reducibility/tpr.ma".
+include "basic_2/substitution/tps_lift.ma".
+include "basic_2/reducibility/tpr.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
(* *)
(**************************************************************************)
-include "Basic_2/reducibility/tpr_tpss.ma".
+include "basic_2/reducibility/tpr_tpss.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/ltpss_ltpss.ma".
-include "Basic_2/reducibility/ltpr_ldrop.ma".
+include "basic_2/unfold/ltpss_ltpss.ma".
+include "basic_2/reducibility/ltpr_ldrop.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_simple.ma".
+include "basic_2/grammar/term_simple.ma".
(* CONTEXT-FREE REDUCIBLE TERMS *********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/tshf.ma".
-include "Basic_2/reducibility/tpr.ma".
+include "basic_2/grammar/tshf.ma".
+include "basic_2/reducibility/tpr.ma".
(* CONTEXT-FREE WEAK HEAD NORMAL TERMS **************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/aarity.ma".
-include "Basic_2/substitution/ldrop.ma".
+include "basic_2/grammar/aarity.ma".
+include "basic_2/substitution/ldrop.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/ldrop_ldrop.ma".
-include "Basic_2/static/aaa.ma".
+include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/static/aaa.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/ldrop_ldrop.ma".
-include "Basic_2/static/aaa.ma".
+include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/static/aaa.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/ldrops.ma".
-include "Basic_2/static/aaa_lift.ma".
+include "basic_2/unfold/ldrops.ma".
+include "basic_2/static/aaa_lift.ma".
(* ATONIC ARITY ASSIGNMENT ON TERMS *****************************************)
(* *)
(**************************************************************************)
-include "Basic_2/static/aaa.ma".
+include "basic_2/static/aaa.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
(* *)
(**************************************************************************)
-include "Basic_2/static/aaa_aaa.ma".
-include "Basic_2/static/lsuba_ldrop.ma".
+include "basic_2/static/aaa_aaa.ma".
+include "basic_2/static/lsuba_ldrop.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
(* *)
(**************************************************************************)
-include "Basic_2/static/lsuba.ma".
+include "basic_2/static/lsuba.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
(* *)
(**************************************************************************)
-include "Basic_2/static/lsuba_aaa.ma".
+include "basic_2/static/lsuba_aaa.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
(* *)
(**************************************************************************)
-include "Ground_2/arith.ma".
+include "ground_2/arith.ma".
(* SORT HIERARCHY ***********************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/genv.ma".
+include "basic_2/grammar/genv.ma".
(* GLOBAL ENVIRONMENT SLICING ***********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/gdrop.ma".
+include "basic_2/substitution/gdrop.ma".
(* GLOBAL ENVIRONMENT SLICING ***********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/lenv_weight.ma".
-include "Basic_2/grammar/lsubs.ma".
-include "Basic_2/substitution/lift.ma".
+include "basic_2/grammar/lenv_weight.ma".
+include "basic_2/grammar/lsubs.ma".
+include "basic_2/substitution/lift.ma".
(* LOCAL ENVIRONMENT SLICING ************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/lift_lift.ma".
-include "Basic_2/substitution/ldrop.ma".
+include "basic_2/substitution/lift_lift.ma".
+include "basic_2/substitution/ldrop.ma".
(* DROPPING *****************************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_weight.ma".
-include "Basic_2/grammar/term_simple.ma".
+include "basic_2/grammar/term_weight.ma".
+include "basic_2/grammar/term_simple.ma".
(* BASIC TERM RELOCATION ****************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/lift.ma".
+include "basic_2/substitution/lift.ma".
(* BASIC TERM RELOCATION ****************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/lift_lift.ma".
-include "Basic_2/substitution/lift_vector.ma".
+include "basic_2/substitution/lift_lift.ma".
+include "basic_2/substitution/lift_vector.ma".
(* BASIC TERM VECTOR RELOCATION *********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_vector.ma".
-include "Basic_2/substitution/lift.ma".
+include "basic_2/grammar/term_vector.ma".
+include "basic_2/substitution/lift.ma".
(* BASIC TERM VECTOR RELOCATION *********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/tps.ma".
+include "basic_2/substitution/tps.ma".
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/ltps.ma".
+include "basic_2/substitution/ltps.ma".
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/tps_lift.ma".
-include "Basic_2/substitution/ltps_ldrop.ma".
+include "basic_2/substitution/tps_lift.ma".
+include "basic_2/substitution/ltps_ldrop.ma".
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/cl_weight.ma".
-include "Basic_2/substitution/ldrop.ma".
+include "basic_2/grammar/cl_weight.ma".
+include "basic_2/substitution/ldrop.ma".
(* PARALLEL SUBSTITUTION ON TERMS *******************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/ldrop_ldrop.ma".
-include "Basic_2/substitution/tps.ma".
+include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/substitution/tps.ma".
(* PARTIAL SUBSTITUTION ON TERMS ********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/tps_lift.ma".
+include "basic_2/substitution/tps_lift.ma".
(* PARALLEL SUBSTITUTION ON TERMS *******************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/tpss.ma".
+include "basic_2/unfold/tpss.ma".
(* DELIFT ON TERMS **********************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/tpss_lift.ma".
-include "Basic_2/unfold/delift.ma".
+include "basic_2/unfold/tpss_lift.ma".
+include "basic_2/unfold/delift.ma".
(* DELIFT ON TERMS **********************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_vector.ma".
+include "basic_2/grammar/term_vector.ma".
(* GENERIC RELOCATION WITH PAIRS ********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/gr2.ma".
+include "basic_2/unfold/gr2.ma".
(* GENERIC RELOCATION WITH PAIRS ********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/gr2.ma".
+include "basic_2/unfold/gr2.ma".
(* GENERIC RELOCATION WITH PAIRS ********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/gr2.ma".
+include "basic_2/unfold/gr2.ma".
(* GENERIC RELOCATION WITH PAIRS ********************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/ldrop.ma".
-include "Basic_2/unfold/gr2_minus.ma".
-include "Basic_2/unfold/lifts.ma".
+include "basic_2/substitution/ldrop.ma".
+include "basic_2/unfold/gr2_minus.ma".
+include "basic_2/unfold/lifts.ma".
(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/ldrop_ldrop.ma".
-include "Basic_2/unfold/ldrops.ma".
+include "basic_2/substitution/ldrop_ldrop.ma".
+include "basic_2/unfold/ldrops.ma".
(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/ldrops_ldrop.ma".
+include "basic_2/unfold/ldrops_ldrop.ma".
(* GENERIC LOCAL ENVIRONMENT SLICING ****************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/lift.ma".
-include "Basic_2/unfold/gr2_plus.ma".
+include "basic_2/substitution/lift.ma".
+include "basic_2/unfold/gr2_plus.ma".
(* GENERIC TERM RELOCATION **************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/lift_lift.ma".
-include "Basic_2/unfold/gr2_minus.ma".
-include "Basic_2/unfold/lifts.ma".
+include "basic_2/substitution/lift_lift.ma".
+include "basic_2/unfold/gr2_minus.ma".
+include "basic_2/unfold/lifts.ma".
(* GENERIC TERM RELOCATION **************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/lift_lift_vector.ma".
-include "Basic_2/unfold/lifts_lift.ma".
-include "Basic_2/unfold/lifts_vector.ma".
+include "basic_2/substitution/lift_lift_vector.ma".
+include "basic_2/unfold/lifts_lift.ma".
+include "basic_2/unfold/lifts_vector.ma".
(* GENERIC RELOCATION *******************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/lifts_lift.ma".
+include "basic_2/unfold/lifts_lift.ma".
(* GENERIC RELOCATION *******************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/lift_vector.ma".
-include "Basic_2/unfold/lifts.ma".
+include "basic_2/substitution/lift_vector.ma".
+include "basic_2/unfold/lifts.ma".
(* GENERIC TERM VECTOR RELOCATION *******************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/ltps.ma".
-include "Basic_2/unfold/tpss.ma".
+include "basic_2/substitution/ltps.ma".
+include "basic_2/unfold/tpss.ma".
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/ltps_ldrop.ma".
-include "Basic_2/unfold/ltpss.ma".
+include "basic_2/substitution/ltps_ldrop.ma".
+include "basic_2/unfold/ltpss.ma".
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/ltpss_tpss.ma".
+include "basic_2/unfold/ltpss_tpss.ma".
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
(* *)
(**************************************************************************)
-include "Basic_2/unfold/tpss_ltps.ma".
-include "Basic_2/unfold/ltpss.ma".
+include "basic_2/unfold/tpss_ltps.ma".
+include "basic_2/unfold/ltpss.ma".
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/tps.ma".
+include "basic_2/substitution/tps.ma".
(* PARTIAL UNFOLD ON TERMS **************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/tps_lift.ma".
-include "Basic_2/unfold/tpss.ma".
+include "basic_2/substitution/tps_lift.ma".
+include "basic_2/unfold/tpss.ma".
(* PARTIAL UNFOLD ON TERMS **************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/ltps_tps.ma".
-include "Basic_2/unfold/tpss_tpss.ma".
+include "basic_2/substitution/ltps_tps.ma".
+include "basic_2/unfold/tpss_tpss.ma".
(* PARTIAL UNFOLD ON TERMS **************************************************)
(* *)
(**************************************************************************)
-include "Basic_2/substitution/tps_tps.ma".
-include "Basic_2/unfold/tpss_lift.ma".
+include "basic_2/substitution/tps_tps.ma".
+include "basic_2/unfold/tpss_lift.ma".
(* PARTIAL UNFOLD ON TERMS **************************************************)
(**************************************************************************)
include "arithmetics/nat.ma".
-include "Ground_2/star.ma".
+include "ground_2/star.ma".
(* ARITHMETICAL PROPERTIES **************************************************)
(* *)
(**************************************************************************)
-include "Ground_2/arith.ma".
+include "ground_2/arith.ma".
(* LISTS ********************************************************************)
(**************************************************************************)
include "basics/star.ma".
-include "Ground_2/xoa_props.ma".
-include "Ground_2/notation.ma".
+include "ground_2/xoa_props.ma".
+include "ground_2/notation.ma".
(* PROPERTIES OF RELATIONS **************************************************)
(* *)
(**************************************************************************)
-include "Ground_2/arith.ma".
+include "ground_2/arith.ma".
(* TRICOTOMY FUNCTION *******************************************************)
-->
</section>
<section name="xoa">
- <key name="output_dir">contribs/lambda_delta/Ground_2/</key>
+ <key name="output_dir">contribs/lambda_delta/ground_2/</key>
<key name="objects">xoa</key>
<key name="notations">xoa_notation</key>
<key name="include">basics/pts.ma</key>
(* *)
(**************************************************************************)
-include "Ground_2/xoa_notation.ma".
-include "Ground_2/xoa.ma".
+include "ground_2/xoa_notation.ma".
+include "ground_2/xoa.ma".
lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
#A0 #P0 #P1 * /2 width=3/
projects / helm.git / commitdiff