X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_preserve_sub.ma;h=76ff1a2a1c7d69d12bae7f37c2ef4984b820da6b;hb=e23331eef5817eaa6c5e1c442d1d6bbb18650573;hp=b9b06348d6a8a49ab7a81739a5f3c0c9d3436405;hpb=ca7327c20c6031829fade8bb84a3a1bb66113f54;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma index b9b06348d..76ff1a2a1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_sub.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/rt_transition/lpr.ma". include "basic_2/rt_computation/cpms_fpbg.ma". include "basic_2/dynamic/cnv.ma". @@ -20,39 +21,39 @@ include "basic_2/dynamic/cnv.ma". (* Inductive premises for the preservation results **************************) definition IH_cnv_cpm_trans_lpr (h) (a): relation3 genv lenv term ≝ - λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] → - ∀n,T2. ❪G,L1❫ ⊢ T1 ➡[h,n] T2 → - ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a]. + λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] → + ∀n,T2. ❪G,L1❫ ⊢ T1 ➡[h,n] T2 → + ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a]. definition IH_cnv_cpms_trans_lpr (h) (a): relation3 genv lenv term ≝ - λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] → - ∀n,T2. ❪G,L1❫ ⊢ T1 ➡*[h,n] T2 → - ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a]. + λG,L1,T1. ❪G,L1❫ ⊢ T1 ![h,a] → + ∀n,T2. ❪G,L1❫ ⊢ T1 ➡*[h,n] T2 → + ∀L2. ❪G,L1❫ ⊢ ➡[h,0] L2 → ❪G,L2❫ ⊢ T2 ![h,a]. definition IH_cnv_cpm_conf_lpr (h) (a): relation3 genv lenv term ≝ - λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → - ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 → - ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → - ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. + λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → + ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 → + ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → + ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. definition IH_cnv_cpms_strip_lpr (h) (a): relation3 genv lenv term ≝ - λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → - ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 → - ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → - ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. + λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → + ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡[h,n2] T2 → + ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → + ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. definition IH_cnv_cpms_conf_lpr (h) (a): relation3 genv lenv term ≝ - λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → - ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡*[h,n2] T2 → - ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → - ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. + λG,L0,T0. ❪G,L0❫ ⊢ T0 ![h,a] → + ∀n1,T1. ❪G,L0❫ ⊢ T0 ➡*[h,n1] T1 → ∀n2,T2. ❪G,L0❫ ⊢ T0 ➡*[h,n2] T2 → + ∀L1. ❪G,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G,L0❫ ⊢ ➡[h,0] L2 → + ∃∃T. ❪G,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G,L2❫ ⊢ T2 ➡*[h,n1-n2] T. (* Auxiliary properties for preservation ************************************) fact cnv_cpms_trans_lpr_sub (h) (a): ∀G0,L0,T0. - (∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) → - ∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpms_trans_lpr h a G1 L1 T1. + (∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpm_trans_lpr h a G1 L1 T1) → + ∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpms_trans_lpr h a G1 L1 T1. #h #a #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H @(cpms_ind_dx … H) -n -T2 /3 width=7 by fpbg_cpms_trans/ @@ -60,12 +61,12 @@ qed-. fact cnv_cpm_conf_lpr_sub (h) (a): ∀G0,L0,T0. - (∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) → - ∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpm_conf_lpr h a G1 L1 T1. + (∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) → + ∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpm_conf_lpr h a G1 L1 T1. /3 width=8 by cpm_cpms/ qed-. fact cnv_cpms_strip_lpr_sub (h) (a): ∀G0,L0,T0. - (∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) → - ∀G1,L1,T1. ❪G0,L0,T0❫ >[h] ❪G1,L1,T1❫ → IH_cnv_cpms_strip_lpr h a G1 L1 T1. + (∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpms_conf_lpr h a G1 L1 T1) → + ∀G1,L1,T1. ❪G0,L0,T0❫ > ❪G1,L1,T1❫ → IH_cnv_cpms_strip_lpr h a G1 L1 T1. /3 width=8 by cpm_cpms/ qed-.