X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpm_trans.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpm_trans.ma;h=2d9f53b9c3aa455c64c80a8a88c6857047d31a8c;hb=93768d9ebc0e3c8e3bcd69571d7a635cb1a16b29;hp=0000000000000000000000000000000000000000;hpb=b634a816745cf8a9a7ad14650d088232c8ee1a1a;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma new file mode 100644 index 000000000..2d9f53b9c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma @@ -0,0 +1,129 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_computation/cpms_fpbg.ma". +include "basic_2/rt_computation/cprs_cprs.ma". +include "basic_2/rt_computation/lprs_cpms.ma". +include "basic_2/dynamic/cnv_drops.ma". +include "basic_2/dynamic/cnv_etc.ma". +include "basic_2/dynamic/lsubv_cnv.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Properties with context-free parallel reduction for local environments *****) + +fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ → + ∀G0,L0,T0. + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) → + (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) → + ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_trans_lpr a h G1 L1 T1. +#a #h #o #Ha #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 * * [|||| * ] +[ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct -IH2 -IH1 -H1 + elim (cpm_inv_sort1 … H2) -H2 * #H1 #H2 destruct // +| #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2 + elim (cnv_inv_lref_drops … H1) -H1 #I #K1 #V1 #HLK1 #HV1 + elim (lpr_drops_conf … HLK1 … HL12) -HL12 // #Y #H #HLK2 + elim (lpr_inv_pair_sn … H) -H #K2 #V2 #HK12 #HV12 #H destruct + lapply (fqup_lref (Ⓣ) … G1 … HLK1) #HKL + elim (cpm_inv_lref1_drops … H2) -H2 * + [ #H1 #H2 destruct -HLK1 /4 width=7 by fqup_fpbg, cnv_lref_drops/ + | #K0 #V0 #W0 #H #HVW0 #W0 -HV12 + lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct + lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/ + | #n #K0 #V0 #W0 #H #HVW0 #W0 #H destruct -HV12 + lapply (drops_mono … H … HLK1) -HLK1 -H #H destruct + lapply (drops_isuni_fwd_drop2 … HLK2) -HLK2 /4 width=7 by fqup_fpbg, cnv_lifts/ + ] +| #l #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2 -IH1 + elim (cnv_inv_gref … H1) +| #p #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2 + elim (cnv_inv_bind … H1) -H1 #HV1 #HT1 + elim (cpm_inv_bind1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct /4 width=9 by fqup_fpbg, cnv_bind, lpr_pair/ + | #T2 #HT12 #HXT2 #H1 #H2 destruct -HV1 + /4 width=11 by fqup_fpbg, cnv_inv_lifts, lpr_pair, drops_refl, drops_drop/ + ] +| #V1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct + elim (cnv_inv_appl … H1) -H1 #n #p #W1 #U1 #Hn #HV1 #HT1 #HVW1 #HTU1 + elim (cpm_inv_appl1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct + lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2 + lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2 + elim (cnv_cpms_strip_lpr_far … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12 + eq_minus_O // #W0 #H1 #H2 -IH2 -IH1 -L1 -W1 -T1 -U1 + lapply (cprs_trans … HXW21 … H1) -XW1 #H1 + lapply (cpms_trans … HXT21 … H2) -XT1