(**************************************************************************) (* ___ *) (* ||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/cpds_cpds.ma". include "basic_2/dynamic/snv_aaa.ma". include "basic_2/dynamic/snv_cpcs.ma". include "basic_2/dynamic/lsubsv_lstas.ma". (* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) (* Properties on sn parallel reduction for local environments ***************) fact lstas_cpr_lpr_aux: ∀h,g,G0,L0,T0. (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_snv_cpx_lpx h g G1 L1 T1) → (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_da_cpr_lpr h g G1 L1 T1) → (∀G1,L1,T1. ⦃G0, L0, T0⦄ >≡[h, g] ⦃G1, L1, T1⦄ → IH_lstas_cpr_lpr h g G1 L1 T1) → ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_lstas_cpr_lpr h g G1 L1 T1. #h #g #G0 #L0 #T0 #IH3 #IH2 #IH1 #G1 #L1 * * [|||| * ] [ #k #_ #_ #_ #_ #l1 #l2 #_ #_ #X2 #H2 #X3 #H3 #L2 #_ -IH3 -IH2 -IH1 >(lstas_inv_sort1 … H2) -X2 >(cpr_inv_sort1 … H3) -X3 /2 width=3 by ex2_intro/ | #i #HG0 #HL0 #HT0 #H1 #l1 #l2 @(nat_ind_plus … l2) -l2 [ #_ | #l2 #_ #Hl21 ] #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH3 [ lapply (lstas_inv_O … H2) -H2 #H destruct -IH1 -H1 -l1 /4 width=5 by lpr_cpcs_conf, cpr_cpcs_dx, ex2_intro/ ] elim (snv_inv_lref … H1) -H1 #I0 #K0 #X0 #HK0 #HX0 elim (da_inv_lref … Hl1) -Hl1 * #K1 [ #V1 | #W1 #l0 ] #HLK1 [ #HVl1 | #HWl1 #H destruct ] lapply (ldrop_mono … HK0 … HLK1) -HK0 #H destruct elim (lstas_inv_lref1 … H2) -H2 * #K0 #V0 #W0 [2,4: #X0 ] #HK0 [1,2: #_ -X0 ] #HVW0 #HX2 lapply (ldrop_mono … HK0 … HLK1) -HK0 #H destruct [ lapply (le_plus_to_le_r … Hl21) -Hl21 #Hl21 ] lapply (fqup_lref … G1 … HLK1) #HKV1 elim (lpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 elim (lpr_inv_pair1 … H) -H #K2 [ #W2 | #V2 ] #HK12 [ #HW12 | #HV12 ] #H destruct lapply (ldrop_fwd_drop2 … HLK2) #H2 elim (cpr_inv_lref1 … H3) -H3 [1,3: #H destruct -HLK1 |2,4: * #K0 #V0 #X0 #H #HVX0 #HX0 lapply (ldrop_mono … H … HLK1) -H -HLK1 #H destruct ] [ lapply (IH2 … HWl1 … HW12 … HK12) /2 width=1 by fqup_fpbg/ -IH2 #H elim (da_inv_sta … H) -H elim (IH1 … HWl1 … HVW0 … HW12 … HK12) -IH1 -HVW0 /2 width=1 by fqup_fpbg/ #V2 #HWV2 #HV2 elim (lift_total V2 0 (i+1)) /3 width=12 by cpcs_lift, lstas_ldec, ex2_intro/ | elim (IH1 … HVl1 … HVW0 … HV12 … HK12) -IH1 -HVl1 -HVW0 -HV12 -HK12 -IH2 /2 width=1 by fqup_fpbg/ #W2 #HVW2 #HW02 elim (lift_total W2 0 (i+1)) /4 width=12 by cpcs_lift, lstas_ldef, ex2_intro/ | elim (IH1 … HVl1 … HVW0 … HVX0 … HK12) -IH1 -HVl1 -HVW0 -HVX0 -HK12 -IH2 -V2 /2 width=1 by fqup_fpbg/ -l1 #W2 #HXW2 #HW02 elim (lift_total W2 0 (i+1)) /3 width=12 by cpcs_lift, lstas_lift, ex2_intro/ ] | #p #_ #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 elim (snv_inv_gref … H1) | #a #I #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct -IH3 -IH2 elim (snv_inv_bind … H1) -H1 #_ #HT1 lapply (da_inv_bind … Hl1) -Hl1 #Hl1 elim (lstas_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct elim (cpr_inv_bind1 … H3) -H3 * [ #V2 #T2 #HV12 #HT12 #H destruct elim (IH1 … Hl1 … HTU1 … HT12 (L2.ⓑ{I}V2)) -IH1 -Hl1 -HTU1 -HT12 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 /4 width=5 by cpcs_bind2, lpr_cpr_conf, lstas_bind, ex2_intro/ | #T3 #HT13 #HXT3 #H1 #H2 destruct elim (IH1 … Hl1 … HTU1 … HT13 (L2.ⓓV1)) -IH1 -Hl1 -HTU1 -HT13 /2 width=1 by fqup_fpbg, lpr_pair/ -T1 -HL12 #U3 #HTU3 #HU13 elim (lstas_inv_lift1 … HTU3 L2 … HXT3) -T3 /5 width=8 by cpcs_cpr_strap1, cpcs_bind1, cpr_zeta, ldrop_drop, ex2_intro/ ] | #V1 #T1 #HG0 #HL0 #HT0 #H1 #l1 #l2 #Hl21 #Hl1 #X2 #H2 #X3 #H3 #L2 #HL12 destruct elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #Hl0 #HVW1 #HW10 #HTU10 lapply (da_inv_flat … Hl1) -Hl1 #Hl1 elim (lstas_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct elim (cpr_inv_appl1 … H3) -H3 * [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2 elim (IH1 … Hl1 … HTU1 … HT12 … HL12) -IH1 -Hl1 -HTU1 /4 width=5 by fqup_fpbg, cpcs_flat, lpr_cpr_conf, lstas_appl, ex2_intro/ | #b #V2 #W2 #W3 #T2 #T3 #HV12 #HW23 #HT23 #H1 #H2 destruct elim (snv_inv_bind … HT1) -HT1 #HW2 #HT2 lapply (da_inv_bind … Hl1) -Hl1 #Hl1 elim (lstas_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct elim (cpds_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW20 #_ #H destruct lapply (cprs_div … HW10 … HW20) -W0 #HW12 lapply (da_sta_conf … HVW1 … Hl0)