X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_computation%2Flpxs_cpxs.ma;h=10831ed7308c2195f552cbdfced23031d96a26f1;hb=730642efca3fb00ca4f8268bd97b0778cff14514;hp=b663f6a6162775dbfd9554b2f4fd572c97bb6d7b;hpb=1604f2ee65c57eefb7c6b3122eab2a9f32e0552d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma
index b663f6a61..10831ed73 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma
@@ -12,15 +12,47 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/rt_computation/lfpxs_cpxs.ma".
-include "basic_2/rt_computation/lfpxs_lpxs.ma".
+include "basic_2/rt_computation/lpxs_lpx.ma".
 
-(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *****************)
+(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************)
 
-(* Properties with uncounted context-sensitive rt-computation for terms *****)
+(* Properties with context-sensitive extended rt-computation for terms ******)
 
-lemma lpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (λ_.lpxs h G).
-/3 width=3 by lfpxs_cpx_trans, lfpxs_lpxs/ qed-.
+(* Basic_2A1: was: cpxs_bind2 *)
+lemma cpxs_bind_dx (h) (G): ∀L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 →
+                            ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h] T2 →
+                            ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2.
+/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed.
 
-lemma lpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (λ_.lpxs h G).
-/3 width=3 by lfpxs_cpxs_trans, lfpxs_lpxs/ qed-.
+(* Inversion lemmas with context-sensitive ext rt-computation for terms *****)
+
+lemma cpxs_inv_abst1 (h) (G): ∀p,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈*[h] U2 →
+                              ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈*[h] T2 &
+                                       U2 = ⓛ{p}V2.T2.
+#h #G #p #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/
+#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct
+elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct
+lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?)
+/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/
+qed-.
+
+lemma cpxs_inv_abbr1 (h) (G): ∀p,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈*[h] U2 →
+                              ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 &
+                                          U2 = ⓓ{p}V2.T2
+                               | ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 & ⬆*[1] U2 ≘ T2 & p = Ⓣ.
+#h #G #p #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/
+#U0 #U2 #_ #HU02 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+  elim (cpx_inv_abbr1 … HU02) -HU02 *
+  [ #V2 #T2 #HV02 #HT02 #H destruct
+    lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?)
+    /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/
+  | #T2 #HT02 #HUT2
+    lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02
+    /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/
+  ]
+| #U1 #HTU1 #HU01 #Hp
+  elim (cpx_lifts_sn … HU02 (Ⓣ) … (L.ⓓV1) … HU01) -U0 /3 width=3 by drops_refl, drops_drop/ #U #HU2 #HU1
+  /4 width=3 by cpxs_strap1, ex3_intro, or_intror/
+]
+qed-.