X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpms_conf.ma;h=691ffde904476daef44750474129977314fa1324;hb=b118146b97959e6a6dde18fdd014b8e1e676a2d1;hp=7965bcae14b0a054d111a0be9303d310ca849479;hpb=ca7327c20c6031829fade8bb84a3a1bb66113f54;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma index 7965bcae1..691ffde90 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpms_conf.ma @@ -20,11 +20,11 @@ include "basic_2/dynamic/cnv_cpms_teqx_conf.ma". (* Sub confluence propery with t-bound rt-computation for terms *************) fact cnv_cpms_conf_lpr_teqx_teqx_aux (h) (a) (G0) (L0) (T0): - (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → - (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → ❪G0,L0❫ ⊢ T0 ![h,a] → - ∀n1,T1. ❪G0,L0❫ ⊢ T0 ➡*[h,n1] T1 → T0 ≛ T1 → - ∀n2,T2. ❪G0,L0❫ ⊢ T0 ➡*[h,n2] T2 → T0 ≛ T2 → + ∀n1,T1. ❪G0,L0❫ ⊢ T0 ➡*[h,n1] T1 → T0 ≅ T1 → + ∀n2,T2. ❪G0,L0❫ ⊢ T0 ➡*[h,n2] T2 → T0 ≅ T2 → ∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 → ∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[h,n2-n1] T & ❪G0,L2❫ ⊢ T2 ➡*[h,n1-n2] T. #h #a #G #L0 #T0 #IH2 #IH1 #HT0 @@ -35,10 +35,10 @@ elim (cnv_cpms_teqx_conf_lpr_aux … IH2 IH1 … H1T01 … H1T02 … HL01 … HL qed-. fact cnv_cpms_conf_lpr_refl_tneqx_sub (h) (a) (G0) (L0) (T0) (m21) (m22): - (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → - (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → ❪G0,L0❫ ⊢ T0 ![h,a] → - ∀X2. ❪G0,L0❫ ⊢ T0 ➡[h,m21] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 → + ∀X2. ❪G0,L0❫ ⊢ T0 ➡[h,m21] X2 → (T0 ≅ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 → ∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 → ∃∃T. ❪G0,L1❫ ⊢ T0 ➡*[h,m21+m22] T& ❪G0,L2❫ ⊢ T2 ➡*[h,0] T. #h #a #G0 #L0 #T0 #m21 #m22 #IH2 #IH1 #H0 @@ -47,9 +47,9 @@ fact cnv_cpms_conf_lpr_refl_tneqx_sub (h) (a) (G0) (L0) (T0) (m21) (m22): lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX02 … 0 T0 … L0 … HL01) // [h] ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → - (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → ❪G0,L0❫ ⊢ T0 ![h,a] → - ∀X1. ❪G0,L0❫ ⊢ T0 ➡[h,m11] X1 → T0 ≛ X1 → ∀T1. ❪G0,L0❫ ⊢ X1 ➡*[h,m12] T1 → X1 ≛ T1 → - ∀X2. ❪G0,L0❫ ⊢ T0 ➡[h,m21] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 → + ∀X1. ❪G0,L0❫ ⊢ T0 ➡[h,m11] X1 → T0 ≅ X1 → ∀T1. ❪G0,L0❫ ⊢ X1 ➡*[h,m12] T1 → X1 ≅ T1 → + ∀X2. ❪G0,L0❫ ⊢ T0 ➡[h,m21] X2 → (T0 ≅ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 → ∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 → - ((∀G,L,T. ❪G0,L0,X1❫ >[h] ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → - (∀G,L,T. ❪G0,L0,X1❫ >[h] ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → + ((∀G,L,T. ❪G0,L0,X1❫ > ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,X1❫ > ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → ∀m21,m22. - ∀X2. ❪G0,L0❫ ⊢ X1 ➡[h,m21] X2 → (X1 ≛ X2 → ⊥) → + ∀X2. ❪G0,L0❫ ⊢ X1 ➡[h,m21] X2 → (X1 ≅ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 → ∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 → ∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[h,m21+m22-m12] T & ❪G0,L2❫ ⊢ T2 ➡*[h,m12-(m21+m22)]T @@ -78,8 +78,8 @@ fact cnv_cpms_conf_lpr_step_tneqx_sub (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) ( lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … H1X01 … L0 ?) // #HX1 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … H1X02 … L0 ?) // #HX2 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … H1X01 … H1X02 … L0 … L0) // #Z0 #HXZ10 #HXZ20 -cut (❪G0, L0, T0❫ >[h] ❪G0, L0, X2❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *) -lapply (fpbg_fpbs_trans ?? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=2 by cpms_fwd_fpbs/ ] #H2fpbg +cut (❪G0, L0, T0❫ > ❪G0, L0, X2❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *) +lapply (fpbg_fpbs_trans ? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ20 … L0 ?) // #HZ0 elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02 elim (teqx_dec X1 Z0) #H2XZ @@ -99,11 +99,11 @@ lapply (cpms_trans … HTZ2 … HZ02) -Z2 [h] ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → - (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → ❪G0,L0❫ ⊢ T0 ![h,a] → - ∀T1. ❪G0,L0❫ ⊢ T0 ➡*[h,n1] T1 → T0 ≛ T1 → - ∀X2. ❪G0,L0❫ ⊢ T0 ➡[h,m21] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 → + ∀T1. ❪G0,L0❫ ⊢ T0 ➡*[h,n1] T1 → T0 ≅ T1 → + ∀X2. ❪G0,L0❫ ⊢ T0 ➡[h,m21] X2 → (T0 ≅ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 → ∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 → ∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[h,m21+m22-n1] T & ❪G0,L2❫ ⊢ T2 ➡*[h,n1-(m21+m22)] T. #h #a #G0 #L0 #T0 #n1 #m21 #m22 #IH2 #IH1 #HT0 @@ -122,11 +122,11 @@ generalize in match IH1; generalize in match IH2; qed-. fact cnv_cpms_conf_lpr_tneqx_tneqx_aux (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) (m22): - (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → - (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → ❪G0,L0❫ ⊢ T0 ![h,a] → - ∀X1. ❪G0,L0❫ ⊢ T0 ➡[h,m11] X1 → (T0 ≛ X1 → ⊥) → ∀T1. ❪G0,L0❫ ⊢ X1 ➡*[h,m12] T1 → - ∀X2. ❪G0,L0❫ ⊢ T0 ➡[h,m21] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 → + ∀X1. ❪G0,L0❫ ⊢ T0 ➡[h,m11] X1 → (T0 ≅ X1 → ⊥) → ∀T1. ❪G0,L0❫ ⊢ X1 ➡*[h,m12] T1 → + ∀X2. ❪G0,L0❫ ⊢ T0 ➡[h,m21] X2 → (T0 ≅ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 → ∀L1. ❪G0,L0❫ ⊢ ➡[h,0] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h,0] L2 → ∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[h,m21+m22-(m11+m12)] T & ❪G0,L2❫ ⊢ T2 ➡*[h,m11+m12-(m21+m22)] T. #h #a #G0 #L0 #T0 #m11 #m12 #m21 #m22 #IH2 #IH1 #H0 @@ -135,11 +135,11 @@ fact cnv_cpms_conf_lpr_tneqx_tneqx_aux (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX01 … L0 ?) // #HX1 lapply (cnv_cpm_trans_lpr_aux … IH1 IH2 … HX02 … L0 ?) // #HX2 elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX01 … HX02 … L0 … L0) // #Z0 #HXZ10 #HXZ20 -cut (❪G0, L0, T0❫ >[h] ❪G0, L0, X1❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *) -lapply (fpbg_fpbs_trans ?? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=2 by cpms_fwd_fpbs/ ] #H2fpbg +cut (❪G0, L0, T0❫ > ❪G0, L0, X1❫) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *) +lapply (fpbg_fpbs_trans ? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=3 by cpms_fwd_fpbs/ ] #H2fpbg lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ10 … L0 ?) // #HZ0 elim (IH1 … HXT1 … HXZ10 … L1 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT1 -HXZ10 #Z1 #HTZ1 #HZ01 -elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02 +elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=3 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02 elim (IH1 … HZ01 … HZ02 L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02 lapply (cpms_trans … HTZ1 … HZ01) -Z1 [h] ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → - (∀G,L,T. ❪G0,L0,T0❫ >[h] ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpm_trans_lpr h a G L T) → + (∀G,L,T. ❪G0,L0,T0❫ > ❪G,L,T❫ → IH_cnv_cpms_conf_lpr h a G L T) → ∀G,L,T. G0 = G → L0 = L → T0 = T → IH_cnv_cpms_conf_lpr h a G L T. #h #a #G #L #T #IH2 #IH1 #G0 #L0 #T0 #HG #HL #HT #HT0 #n1 #T1 #HT01 #n2 #T2 #HT02 #L1 #HL01 #L2 #HL02 destruct