X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_cpms_conf.ma;h=7965bcae14b0a054d111a0be9303d310ca849479;hp=a91fff202d984955fabf05baa787b44ea93cdc68;hb=ca7327c20c6031829fade8bb84a3a1bb66113f54;hpb=25c634037771dff0138e5e8e3d4378183ff49b86 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 a91fff202..7965bcae1 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 @@ -23,10 +23,10 @@ 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) → ❪G0,L0❫ ⊢ T0 ![h,a] → - ∀n1,T1. ❪G0,L0❫ ⊢ T0 ➡*[n1,h] T1 → T0 ≛ T1 → - ∀n2,T2. ❪G0,L0❫ ⊢ T0 ➡*[n2,h] T2 → T0 ≛ T2 → - ∀L1. ❪G0,L0❫ ⊢ ➡[h] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h] L2 → - ∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[n2-n1,h] T & ❪G0,L2❫ ⊢ T2 ➡*[n1-n2,h] T. + ∀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 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #H1T02 #H2T02 #L1 #HL01 #L2 #HL02 @@ -38,9 +38,9 @@ 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) → ❪G0,L0❫ ⊢ T0 ![h,a] → - ∀X2. ❪G0,L0❫ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[m22,h] T2 → - ∀L1. ❪G0,L0❫ ⊢ ➡[h] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h] L2 → - ∃∃T. ❪G0,L1❫ ⊢ T0 ➡*[m21+m22,h] T& ❪G0,L2❫ ⊢ T2 ➡*[h] T. + ∀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 #X2 #HX02 #HnX02 #T2 #HXT2 #L1 #HL01 #L2 #HL02 @@ -60,18 +60,18 @@ fact cnv_cpms_conf_lpr_step_tneqx_sub (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) ( (∀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) → ❪G0,L0❫ ⊢ T0 ![h,a] → - ∀X1. ❪G0,L0❫ ⊢ T0 ➡[m11,h] X1 → T0 ≛ X1 → ∀T1. ❪G0,L0❫ ⊢ X1 ➡*[m12,h] T1 → X1 ≛ T1 → - ∀X2. ❪G0,L0❫ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[m22,h] T2 → - ∀L1. ❪G0,L0❫ ⊢ ➡[h] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h] L2 → + ∀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) → ∀m21,m22. - ∀X2. ❪G0,L0❫ ⊢ X1 ➡[m21,h] X2 → (X1 ≛ X2 → ⊥) → - ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[m22,h] T2 → - ∀L1. ❪G0,L0❫ ⊢ ➡[h] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h] L2 → - ∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[m21+m22-m12,h] T & ❪G0,L2❫ ⊢ T2 ➡*[m12-(m21+m22),h]T + ∀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 ) → - ∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[m21+m22-(m11+m12),h] T & ❪G0,L2❫ ⊢ T2 ➡*[m11+m12-(m21+m22),h] T. + ∃∃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 #HT0 #X1 #H1X01 #H2X01 #T1 #H1XT1 #H2XT1 #X2 #H1X02 #H2X02 #T2 #HXT2 #L1 #HL01 #L2 #HL02 #IH @@ -102,10 +102,10 @@ fact cnv_cpms_conf_lpr_teqx_tneqx_aux (h) (a) (G0) (L0) (T0) (n1) (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) → ❪G0,L0❫ ⊢ T0 ![h,a] → - ∀T1. ❪G0,L0❫ ⊢ T0 ➡*[n1,h] T1 → T0 ≛ T1 → - ∀X2. ❪G0,L0❫ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[m22,h] T2 → - ∀L1. ❪G0,L0❫ ⊢ ➡[h] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h] L2 → - ∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[m21+m22-n1,h] T & ❪G0,L2❫ ⊢ T2 ➡*[n1-(m21+m22),h] T. + ∀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 #T1 #H1T01 #H2T01 generalize in match m22; generalize in match m21; -m21 -m22 @@ -125,10 +125,10 @@ fact cnv_cpms_conf_lpr_tneqx_tneqx_aux (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) (∀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) → ❪G0,L0❫ ⊢ T0 ![h,a] → - ∀X1. ❪G0,L0❫ ⊢ T0 ➡[m11,h] X1 → (T0 ≛ X1 → ⊥) → ∀T1. ❪G0,L0❫ ⊢ X1 ➡*[m12,h] T1 → - ∀X2. ❪G0,L0❫ ⊢ T0 ➡[m21,h] X2 → (T0 ≛ X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[m22,h] T2 → - ∀L1. ❪G0,L0❫ ⊢ ➡[h] L1 → ∀L2. ❪G0,L0❫ ⊢ ➡[h] L2 → - ∃∃T. ❪G0,L1❫ ⊢ T1 ➡*[m21+m22-(m11+m12),h] T & ❪G0,L2❫ ⊢ T2 ➡*[m11+m12-(m21+m22),h] T. + ∀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 #X1 #HX01 #HnX01 #T1 #HXT1 #X2 #HX02 #HnX02 #T2 #HXT2 #L1 #HL01 #L2 #HL02