update in static_2

[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 a818e63479b36946d67322a37bb90195fb760aaa..691ffde904476daef44750474129977314fa1324 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
@@ -23,8 +23,8 @@ fact cnv_cpms_conf_lpr_teqx_teqx_aux (h) (a) (G0) (L0) (T0):
      (∀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] →
-     â\88\80n1,T1. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡*[h,n1] T1 â\86\92 T0 â\89\9b T1 →
-     â\88\80n2,T2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡*[h,n2] T2 â\86\92 T0 â\89\9b T2 →
+     â\88\80n1,T1. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡*[h,n1] T1 â\86\92 T0 â\89\85 T1 →
+     â\88\80n2,T2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡*[h,n2] T2 â\86\92 T0 â\89\85 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
@@ -38,7 +38,7 @@ fact cnv_cpms_conf_lpr_refl_tneqx_sub (h) (a) (G0) (L0) (T0) (m21) (m22):
      (∀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] →
-     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m21] X2 â\86\92 (T0 â\89\9b X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 →
+     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m21] X2 â\86\92 (T0 â\89\85 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
@@ -60,13 +60,13 @@ fact cnv_cpms_conf_lpr_step_tneqx_sub (h) (a) (G0) (L0) (T0) (m11) (m12) (m21) (
      (∀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] →
-     â\88\80X1. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m11] X1 â\86\92 T0 â\89\9b X1 â\86\92 â\88\80T1. â\9dªG0,L0â\9d« â\8a¢ X1 â\9e¡*[h,m12] T1 â\86\92 X1 â\89\9b T1 →
-     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m21] X2 â\86\92 (T0 â\89\9b X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 →
+     â\88\80X1. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m11] X1 â\86\92 T0 â\89\85 X1 â\86\92 â\88\80T1. â\9dªG0,L0â\9d« â\8a¢ X1 â\9e¡*[h,m12] T1 â\86\92 X1 â\89\85 T1 →
+     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m21] X2 â\86\92 (T0 â\89\85 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❫ > ❪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.
-       â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ X1 â\9e¡[h,m21] X2 â\86\92 (X1 â\89\9b X2 → ⊥) →
+       â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ X1 â\9e¡[h,m21] X2 â\86\92 (X1 â\89\85 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
@@ -102,8 +102,8 @@ fact cnv_cpms_conf_lpr_teqx_tneqx_aux (h) (a) (G0) (L0) (T0) (n1) (m21) (m22):
      (∀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] →
-     â\88\80T1. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡*[h,n1] T1 â\86\92 T0 â\89\9b T1 →
-     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m21] X2 â\86\92 (T0 â\89\9b X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 →
+     â\88\80T1. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡*[h,n1] T1 â\86\92 T0 â\89\85 T1 →
+     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m21] X2 â\86\92 (T0 â\89\85 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
@@ -125,8 +125,8 @@ fact cnv_cpms_conf_lpr_tneqx_tneqx_aux (h) (a) (G0) (L0) (T0) (m11) (m12) (m21)
      (∀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] →
-     â\88\80X1. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m11] X1 â\86\92 (T0 â\89\9b X1 → ⊥) → ∀T1. ❪G0,L0❫ ⊢ X1 ➡*[h,m12] T1 →
-     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m21] X2 â\86\92 (T0 â\89\9b X2 → ⊥) → ∀T2. ❪G0,L0❫ ⊢ X2 ➡*[h,m22] T2 →
+     â\88\80X1. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m11] X1 â\86\92 (T0 â\89\85 X1 → ⊥) → ∀T1. ❪G0,L0❫ ⊢ X1 ➡*[h,m12] T1 →
+     â\88\80X2. â\9dªG0,L0â\9d« â\8a¢ T0 â\9e¡[h,m21] X2 â\86\92 (T0 â\89\85 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