update in basic_2 and in web site

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / cpce / cpce_lpr.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_lpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_lpr.etc
new file mode 100644 (file)
index 0000000..f0a3a15
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpce/cpce_lpr.etc
@@ -0,0 +1,42 @@
+include "basic_2/rt_transition/lpr.ma".
+include "basic_2/rt_conversion/lpce.ma".
+include "basic_2/dynamic/cnv_preserve.ma".
+
+lemma cpce_cpm_conf_lpce_lpr (a) (h) (n) (G):
+      ∀L1,T1. ⦃G,L1⦄ ⊢ T1 ![a,h] →
+      ∀U1. ⦃G,L1⦄ ⊢ T1 ⬌η[h] U1 → ∀K1. ⦃G,L1⦄ ⊢ ⬌η[h] K1 →
+      ∀T2. ⦃G,L1⦄ ⊢ T1 ➡[n,h] T2 → ∀L2. ⦃G,L1⦄ ⊢ ➡[h] L2 →
+      ∃∃K2,U2.  ⦃G,K1⦄ ⊢ ➡[h] K2 & ⦃G,L2⦄ ⊢ ⬌η[h] K2 & ⦃G,K2⦄ ⊢ U1 ➡[n,h] U2 & ⦃G,L2⦄ ⊢ T2 ⬌η[h] U2.
+#a #h #n #G #L1 #T1 #HT1
+letin o ≝ (sd_O h)
+lapply (cnv_fwd_fsb … o … HT1) -HT1 #H
+@(fsb_ind_fpbg … H) -G -L1 -T1 #G #L1 #T1 #_ #IH
+#U1 
+
+#H elim H -G -L1 -T1 -U1
+[ #G #L1 elim L1 -L1 [| #L1 #I1 #IH ] #s #K1 #HLK1 #X2 #HX2 #Y2 #HY2
+  elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn destruct
+  [ lapply (lpr_inv_atom_sn … HY2) -HY2 #H destruct
+    lapply (lpce_inv_atom_sn … HLK1) -HLK1 #H destruct
+    /3 width=6 by cpce_sort, cpm_sort, ex4_2_intro/
+  | elim (lpr_inv_bind_sn … HY2) -HY2 #I2 #L2 #HL12 #HI12 #H destruct
+    elim (lpce_inv_bind_sn … HLK1) -HLK1 #J1 #K0 #HLK1 #HIJ1 #H destruct
+    elim (IH s ? HLK1 (⋆((next h)^n s)) … HL12) -IH -HLK1 -HL12
+    [| /2 width=1 by cpm_sort/ ] #K2 #U2 #HK12 #HLK2 #H1s #H2s
+
+| #G #L1 #s elim L1 -L1
+  [ #Y2 #HY2 #X2 #HX2 #K1 #HLK1
+    lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
+    /3 width=6 by cpce_sort, ex4_2_intro/
+  | #L1 #I1 #IH #Y2 #HY2 #X2 #HX2 #K1 #HLK1
+    lapply (cpce_inv_sort_sn … HX2) -HX2 #H destruct
+
+    
+| #n #G #K1 #V1 #V2 #X1 #HV12 #_ #HX1 #X2 #HX2 #Y2 #HY2
+  elim (lpr_inv_pair_sn … HY2) -HY2 #K2 #W1 #HK12 #HVW1 #H destruct
+  lapply (cpce_inv_ldef_sn … HX2) -HX2 #H destruct
+  elim (lifts_total W1 (𝐔❴1❵)) #X2 #HX2
+  @(ex2_intro … X2) [ @(cpm_delta … HX2) /3 width=5 by _/
+  
+  /3 width=3 by cpce_ldef, ex2_intro/
+  | 
\ No newline at end of file