- ldrop is now drop as in basic_1

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / computation / cpxs_cpxs.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
index 9e6cfcd24f842e178c7e2e56a6bc032c3a6e5aef..a19c92545b1444d26c54dd6479a4c43a264b2fe7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpxs.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "basic_2/reduction/lpx_ldrop.ma".
+include "basic_2/reduction/lpx_drop.ma".
 include "basic_2/computation/cpxs_lift.ma".
 
 (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
@@ -96,13 +96,13 @@ qed-.
 lemma lpx_cpx_trans: ∀h,g,G. s_r_transitive … (cpx h g G) (λ_.lpx h g G).
 #h #g #G #L2 #T1 #T2 #HT12 elim HT12 -G -L2 -T1 -T2
 [ /2 width=3 by/
-| /3 width=2 by cpx_cpxs, cpx_sort/
+| /3 width=2 by cpx_cpxs, cpx_st/
 | #I #G #L2 #K2 #V0 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV02 #L1 #HL12
-  elim (lpx_ldrop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
+  elim (lpx_drop_trans_O1 … HL12 … HLK2) -L2 #X #HLK1 #H
   elim (lpx_inv_pair2 … H) -H #K1 #V1 #HK12 #HV10 #H destruct
   /4 width=7 by cpxs_delta, cpxs_strap2/
 |4,9: /4 width=1 by cpxs_beta, cpxs_bind, lpx_pair/
-|5,7,8: /3 width=1 by cpxs_flat, cpxs_ti, cpxs_tau/
+|5,7,8: /3 width=1 by cpxs_flat, cpxs_ct, cpxs_eps/
 | /4 width=3 by cpxs_zeta, lpx_pair/
 | /4 width=3 by cpxs_theta, cpxs_strap1, lpx_pair/
 ]
@@ -126,13 +126,13 @@ lemma cpxs_bind2_dx: ∀h,g,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h, g] V2 →
 
 (* Properties on supclosure *************************************************)
 
-lemma fqu_cpxs_trans_neq: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\83 ⦃G2, L2, T2⦄ →
+lemma fqu_cpxs_trans_neq: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90 ⦃G2, L2, T2⦄ →
                           ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → (T2 = U2 → ⊥) →
-                          â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, g] U1 & T1 = U1 â\86\92 â\8a¥ & â¦\83G1, L1, U1â¦\84 â\8a\83 ⦃G2, L2, U2⦄.
+                          â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, g] U1 & T1 = U1 â\86\92 â\8a¥ & â¦\83G1, L1, U1â¦\84 â\8a\90 ⦃G2, L2, U2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
 [ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1)
   #U2 #HVU2 @(ex3_intro … U2)
-  [1,3: /3 width=7 by fqu_drop, cpxs_delta, ldrop_pair, ldrop_drop/
+  [1,3: /3 width=7 by fqu_drop, cpxs_delta, drop_pair, drop_drop/
   | #H destruct /2 width=7 by lift_inv_lref2_be/
   ]
 | #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T))
@@ -154,9 +154,9 @@ lemma fqu_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2,
 ]
 qed-.
 
-lemma fquq_cpxs_trans_neq: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\83⸮ ⦃G2, L2, T2⦄ →
+lemma fquq_cpxs_trans_neq: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90⸮ ⦃G2, L2, T2⦄ →
                            ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → (T2 = U2 → ⊥) →
-                           â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, g] U1 & T1 = U1 â\86\92 â\8a¥ & â¦\83G1, L1, U1â¦\84 â\8a\83⸮ ⦃G2, L2, U2⦄.
+                           â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, g] U1 & T1 = U1 â\86\92 â\8a¥ & â¦\83G1, L1, U1â¦\84 â\8a\90⸮ ⦃G2, L2, U2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12
 [ #H12 elim (fqu_cpxs_trans_neq … H12 … HTU2 H) -T2
   /3 width=4 by fqu_fquq, ex3_intro/
@@ -164,9 +164,9 @@ lemma fquq_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃
 ]
 qed-.
 
-lemma fqup_cpxs_trans_neq: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\83+ ⦃G2, L2, T2⦄ →
+lemma fqup_cpxs_trans_neq: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90+ ⦃G2, L2, T2⦄ →
                            ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → (T2 = U2 → ⊥) →
-                           â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, g] U1 & T1 = U1 â\86\92 â\8a¥ & â¦\83G1, L1, U1â¦\84 â\8a\83+ ⦃G2, L2, U2⦄.
+                           â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, g] U1 & T1 = U1 â\86\92 â\8a¥ & â¦\83G1, L1, U1â¦\84 â\8a\90+ ⦃G2, L2, U2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1
 [ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpxs_trans_neq … H12 … HTU2 H) -T2
   /3 width=4 by fqu_fqup, ex3_intro/
@@ -176,9 +176,9 @@ lemma fqup_cpxs_trans_neq: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2
 ]
 qed-.
 
-lemma fqus_cpxs_trans_neq: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\83* ⦃G2, L2, T2⦄ →
+lemma fqus_cpxs_trans_neq: â\88\80h,g,G1,G2,L1,L2,T1,T2. â¦\83G1, L1, T1â¦\84 â\8a\90* ⦃G2, L2, T2⦄ →
                            ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡*[h, g] U2 → (T2 = U2 → ⊥) →
-                           â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, g] U1 & T1 = U1 â\86\92 â\8a¥ & â¦\83G1, L1, U1â¦\84 â\8a\83* ⦃G2, L2, U2⦄.
+                           â\88\83â\88\83U1. â¦\83G1, L1â¦\84 â\8a¢ T1 â\9e¡*[h, g] U1 & T1 = U1 â\86\92 â\8a¥ & â¦\83G1, L1, U1â¦\84 â\8a\90* ⦃G2, L2, U2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12
 [ #H12 elim (fqup_cpxs_trans_neq … H12 … HTU2 H) -T2
   /3 width=4 by fqup_fqus, ex3_intro/