update in ground_2, static_2, basic_2, apps_2, alpha_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / dynamic / cnv_cpms_conf.ma

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 f5c38f1981abbe4aba87d822d81c9ce56501a284..a91fff202d984955fabf05baa787b44ea93cdc68 100644 (file)
--- 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,13 +20,13 @@ 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):
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpm_trans_lpr h a G L T) →
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpms_conf_lpr h a G L T) →
-     â¦\83G0,L0â¦\84 ⊢ T0 ![h,a] →
-     â\88\80n1,T1. â¦\83G0,L0â¦\84 ⊢ T0 ➡*[n1,h] T1 → T0 ≛ T1 →
-     â\88\80n2,T2. â¦\83G0,L0â¦\84 ⊢ T0 ➡*[n2,h] T2 → T0 ≛ T2 →
-     â\88\80L1. â¦\83G0,L0â¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G0,L0â¦\84 ⊢ ➡[h] L2 →
-     â\88\83â\88\83T. â¦\83G0,L1â¦\84 â\8a¢ T1 â\9e¡*[n2-n1,h] T & â¦\83G0,L2â¦\84 ⊢ T2 ➡*[n1-n2,h] T.
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpm_trans_lpr h a G L T) →
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpms_conf_lpr h a G L T) →
+     â\9dªG0,L0â\9d« ⊢ T0 ![h,a] →
+     â\88\80n1,T1. â\9dªG0,L0â\9d« ⊢ T0 ➡*[n1,h] T1 → T0 ≛ T1 →
+     â\88\80n2,T2. â\9dªG0,L0â\9d« ⊢ T0 ➡*[n2,h] T2 → T0 ≛ T2 →
+     â\88\80L1. â\9dªG0,L0â\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG0,L0â\9d« ⊢ ➡[h] L2 →
+     â\88\83â\88\83T. â\9dªG0,L1â\9d« â\8a¢ T1 â\9e¡*[n2-n1,h] T & â\9dªG0,L2â\9d« ⊢ T2 ➡*[n1-n2,h] T.
 #h #a #G #L0 #T0 #IH2 #IH1 #HT0
 #n1 #T1 #H1T01 #H2T01 #n2 #T2 #H1T02 #H2T02
 #L1 #HL01 #L2 #HL02
@@ -35,12 +35,12 @@ 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):
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpm_trans_lpr h a G L T) →
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpms_conf_lpr h a G L T) →
-     â¦\83G0,L0â¦\84 ⊢ T0 ![h,a] →
-     â\88\80X2. â¦\83G0,L0â¦\84 â\8a¢ T0 â\9e¡[m21,h] X2 â\86\92 (T0 â\89\9b X2 â\86\92 â\8a¥) â\86\92 â\88\80T2. â¦\83G0,L0â¦\84 ⊢ X2 ➡*[m22,h] T2 →
-     â\88\80L1. â¦\83G0,L0â¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G0,L0â¦\84 ⊢ ➡[h] L2 →
-     â\88\83â\88\83T. â¦\83G0,L1â¦\84 â\8a¢ T0 â\9e¡*[m21+m22,h] T& â¦\83G0,L2â¦\84 ⊢ T2 ➡*[h] T.
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpm_trans_lpr h a G L T) →
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpms_conf_lpr h a G L T) →
+     â\9dªG0,L0â\9d« ⊢ T0 ![h,a] →
+     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[m21,h] X2 â\86\92 (T0 â\89\9b X2 â\86\92 â\8a¥) â\86\92 â\88\80T2. â\9dªG0,L0â\9d« ⊢ X2 ➡*[m22,h] T2 →
+     â\88\80L1. â\9dªG0,L0â\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG0,L0â\9d« ⊢ ➡[h] L2 →
+     â\88\83â\88\83T. â\9dªG0,L1â\9d« â\8a¢ T0 â\9e¡*[m21+m22,h] T& â\9dªG0,L2â\9d« ⊢ T2 ➡*[h] T.
 #h #a #G0 #L0 #T0 #m21 #m22 #IH2 #IH1 #H0
 #X2 #HX02 #HnX02 #T2 #HXT2
 #L1 #HL01 #L2 #HL02
@@ -57,28 +57,28 @@ lapply (cpms_trans … HTY2 … HY2) -Y2 #HT2Y
 qed-.
 
 fact cnv_cpms_conf_lpr_step_tneqx_sub (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) (m22):
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpm_trans_lpr h a G L T) →
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpms_conf_lpr h a G L T) →
-     â¦\83G0,L0â¦\84 ⊢ T0 ![h,a] →
-     â\88\80X1. â¦\83G0,L0â¦\84 â\8a¢ T0 â\9e¡[m11,h] X1 â\86\92 T0 â\89\9b X1 â\86\92 â\88\80T1. â¦\83G0,L0â¦\84 ⊢ X1 ➡*[m12,h] T1 → X1 ≛ T1 →
-     â\88\80X2. â¦\83G0,L0â¦\84 â\8a¢ T0 â\9e¡[m21,h] X2 â\86\92 (T0 â\89\9b X2 â\86\92 â\8a¥) â\86\92 â\88\80T2. â¦\83G0,L0â¦\84 ⊢ X2 ➡*[m22,h] T2 →
-     â\88\80L1. â¦\83G0,L0â¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G0,L0â¦\84 ⊢ ➡[h] L2 →
-     ((â\88\80G,L,T. â¦\83G0,L0,X1â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpm_trans_lpr h a G L T) →
-       (â\88\80G,L,T. â¦\83G0,L0,X1â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpms_conf_lpr h a G L T) →
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpm_trans_lpr h a G L T) →
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpms_conf_lpr h a G L T) →
+     â\9dªG0,L0â\9d« ⊢ T0 ![h,a] →
+     â\88\80X1. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[m11,h] X1 â\86\92 T0 â\89\9b X1 â\86\92 â\88\80T1. â\9dªG0,L0â\9d« ⊢ X1 ➡*[m12,h] T1 → X1 ≛ T1 →
+     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[m21,h] X2 â\86\92 (T0 â\89\9b X2 â\86\92 â\8a¥) â\86\92 â\88\80T2. â\9dªG0,L0â\9d« ⊢ X2 ➡*[m22,h] T2 →
+     â\88\80L1. â\9dªG0,L0â\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG0,L0â\9d« ⊢ ➡[h] L2 →
+     ((â\88\80G,L,T. â\9dªG0,L0,X1â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpm_trans_lpr h a G L T) →
+       (â\88\80G,L,T. â\9dªG0,L0,X1â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpms_conf_lpr h a G L T) →
        ∀m21,m22.
-       â\88\80X2. â¦\83G0,L0â¦\84 ⊢ X1 ➡[m21,h] X2 → (X1 ≛ X2 → ⊥) →
-       â\88\80T2. â¦\83G0,L0â¦\84 ⊢ X2 ➡*[m22,h] T2 →
-       â\88\80L1. â¦\83G0,L0â¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G0,L0â¦\84 ⊢ ➡[h] L2 →
-       â\88\83â\88\83T. â¦\83G0,L1â¦\84 â\8a¢ T1 â\9e¡*[m21+m22-m12,h] T & â¦\83G0,L2â¦\84 ⊢ T2 ➡*[m12-(m21+m22),h]T
+       â\88\80X2. â\9dªG0,L0â\9d« ⊢ X1 ➡[m21,h] X2 → (X1 ≛ X2 → ⊥) →
+       â\88\80T2. â\9dªG0,L0â\9d« ⊢ X2 ➡*[m22,h] T2 →
+       â\88\80L1. â\9dªG0,L0â\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG0,L0â\9d« ⊢ ➡[h] L2 →
+       â\88\83â\88\83T. â\9dªG0,L1â\9d« â\8a¢ T1 â\9e¡*[m21+m22-m12,h] T & â\9dªG0,L2â\9d« ⊢ T2 ➡*[m12-(m21+m22),h]T
      ) →
-     â\88\83â\88\83T. â¦\83G0,L1â¦\84 â\8a¢ T1 â\9e¡*[m21+m22-(m11+m12),h] T & â¦\83G0,L2â¦\84 ⊢ T2 ➡*[m11+m12-(m21+m22),h] T.
+     â\88\83â\88\83T. â\9dªG0,L1â\9d« â\8a¢ T1 â\9e¡*[m21+m22-(m11+m12),h] T & â\9dªG0,L2â\9d« ⊢ T2 ➡*[m11+m12-(m21+m22),h] 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
 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 (â¦\83G0, L0, T0â¦\84 >[h] â¦\83G0, L0, X2â¦\84) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *)
+cut (â\9dªG0, L0, T0â\9d« >[h] â\9dªG0, L0, X2â\9d«) [ /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
 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
@@ -99,13 +99,13 @@ lapply (cpms_trans … HTZ2 … HZ02) -Z2 <arith_l4 #HT2Z
 qed-.
 
 fact cnv_cpms_conf_lpr_teqx_tneqx_aux (h) (a) (G0) (L0) (T0) (n1) (m21) (m22):
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpm_trans_lpr h a G L T) →
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpms_conf_lpr h a G L T) →
-     â¦\83G0,L0â¦\84 ⊢ T0 ![h,a] →
-     â\88\80T1. â¦\83G0,L0â¦\84 ⊢ T0 ➡*[n1,h] T1 → T0 ≛ T1 →
-     â\88\80X2. â¦\83G0,L0â¦\84 â\8a¢ T0 â\9e¡[m21,h] X2 â\86\92 (T0 â\89\9b X2 â\86\92 â\8a¥) â\86\92 â\88\80T2. â¦\83G0,L0â¦\84 ⊢ X2 ➡*[m22,h] T2 →
-     â\88\80L1. â¦\83G0,L0â¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G0,L0â¦\84 ⊢ ➡[h] L2 →
-     â\88\83â\88\83T. â¦\83G0,L1â¦\84 â\8a¢ T1 â\9e¡*[m21+m22-n1,h] T & â¦\83G0,L2â¦\84 ⊢ T2 ➡*[n1-(m21+m22),h] T.
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpm_trans_lpr h a G L T) →
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpms_conf_lpr h a G L T) →
+     â\9dªG0,L0â\9d« ⊢ T0 ![h,a] →
+     â\88\80T1. â\9dªG0,L0â\9d« ⊢ T0 ➡*[n1,h] T1 → T0 ≛ T1 →
+     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[m21,h] X2 â\86\92 (T0 â\89\9b X2 â\86\92 â\8a¥) â\86\92 â\88\80T2. â\9dªG0,L0â\9d« ⊢ X2 ➡*[m22,h] T2 →
+     â\88\80L1. â\9dªG0,L0â\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG0,L0â\9d« ⊢ ➡[h] L2 →
+     â\88\83â\88\83T. â\9dªG0,L1â\9d« â\8a¢ T1 â\9e¡*[m21+m22-n1,h] T & â\9dªG0,L2â\9d« ⊢ T2 ➡*[n1-(m21+m22),h] 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
@@ -122,20 +122,20 @@ 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):
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpm_trans_lpr h a G L T) →
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpms_conf_lpr h a G L T) →
-     â¦\83G0,L0â¦\84 ⊢ T0 ![h,a] →
-     â\88\80X1. â¦\83G0,L0â¦\84 â\8a¢ T0 â\9e¡[m11,h] X1 â\86\92 (T0 â\89\9b X1 â\86\92 â\8a¥) â\86\92 â\88\80T1. â¦\83G0,L0â¦\84 ⊢ X1 ➡*[m12,h] T1 →
-     â\88\80X2. â¦\83G0,L0â¦\84 â\8a¢ T0 â\9e¡[m21,h] X2 â\86\92 (T0 â\89\9b X2 â\86\92 â\8a¥) â\86\92 â\88\80T2. â¦\83G0,L0â¦\84 ⊢ X2 ➡*[m22,h] T2 →
-     â\88\80L1. â¦\83G0,L0â¦\84 â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â¦\83G0,L0â¦\84 ⊢ ➡[h] L2 →
-     â\88\83â\88\83T. â¦\83G0,L1â¦\84 â\8a¢ T1 â\9e¡*[m21+m22-(m11+m12),h] T & â¦\83G0,L2â¦\84 ⊢ T2 ➡*[m11+m12-(m21+m22),h] T.
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpm_trans_lpr h a G L T) →
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpms_conf_lpr h a G L T) →
+     â\9dªG0,L0â\9d« ⊢ T0 ![h,a] →
+     â\88\80X1. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[m11,h] X1 â\86\92 (T0 â\89\9b X1 â\86\92 â\8a¥) â\86\92 â\88\80T1. â\9dªG0,L0â\9d« ⊢ X1 ➡*[m12,h] T1 →
+     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[m21,h] X2 â\86\92 (T0 â\89\9b X2 â\86\92 â\8a¥) â\86\92 â\88\80T2. â\9dªG0,L0â\9d« ⊢ X2 ➡*[m22,h] T2 →
+     â\88\80L1. â\9dªG0,L0â\9d« â\8a¢ â\9e¡[h] L1 â\86\92 â\88\80L2. â\9dªG0,L0â\9d« ⊢ ➡[h] L2 →
+     â\88\83â\88\83T. â\9dªG0,L1â\9d« â\8a¢ T1 â\9e¡*[m21+m22-(m11+m12),h] T & â\9dªG0,L2â\9d« ⊢ T2 ➡*[m11+m12-(m21+m22),h] 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
 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 (â¦\83G0, L0, T0â¦\84 >[h] â¦\83G0, L0, X1â¦\84) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *)
+cut (â\9dªG0, L0, T0â\9d« >[h] â\9dªG0, L0, X1â\9d«) [ /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
 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
@@ -147,8 +147,8 @@ lapply (cpms_trans … HTZ2 … HZ02) -Z2 <arith_l4 #HT2Z
 qed-.
 
 fact cnv_cpms_conf_lpr_aux (h) (a) (G0) (L0) (T0):
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpm_trans_lpr h a G L T) →
-     (â\88\80G,L,T. â¦\83G0,L0,T0â¦\84 >[h] â¦\83G,L,Tâ¦\84 → IH_cnv_cpms_conf_lpr h a G L T) →
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → IH_cnv_cpm_trans_lpr h a G L T) →
+     (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« >[h] â\9dªG,L,Tâ\9d« → 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