- advances towards strong normalization

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / relocation / drops.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
index e18b10a1a5faf7e6a591545871bf8780844902ba..0a21cd1d7a6e99674dcf144484e010aba6c58c29 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma
@@ -38,26 +38,39 @@ interpretation "uniform slicing (local environment)"
 interpretation "generic slicing (local environment)"
    'RDropStar b f L1 L2 = (drops b f L1 L2).
 
-definition d_liftable1: relation2 lenv term → predicate bool ≝
-                        λR,b. ∀f,L,K. ⬇*[b, f] L ≡ K →
-                        ∀T,U. ⬆*[f] T ≡ U → R K T → R L U.
+definition d_liftable1: predicate (relation2 lenv term) ≝
+                        λR. ∀K,T. R K T → ∀b,f,L. ⬇*[b, f] L ≡ K →
+                        ∀U. ⬆*[f] T ≡ U → R L U.
 
-definition d_liftable2: predicate (lenv → relation term) ≝
-                        λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K →
-                        ∀U1. ⬆*[f] T1 ≡ U1 → 
-                        ∃∃U2. ⬆*[f] T2 ≡ U2 & R L U1 U2.
+definition d_deliftable1: predicate (relation2 lenv term) ≝
+                          λR. ∀L,U. R L U → ∀b,f,K. ⬇*[b, f] L ≡ K →
+                          ∀T. ⬆*[f] T ≡ U → R K T.
+
+definition d_liftable2_sn: predicate (lenv → relation term) ≝
+                           λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K →
+                           ∀U1. ⬆*[f] T1 ≡ U1 → 
+                           ∃∃U2. ⬆*[f] T2 ≡ U2 & R L U1 U2.
 
 definition d_deliftable2_sn: predicate (lenv → relation term) ≝
                              λR. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⬇*[b, f] L ≡ K →
                              ∀T1. ⬆*[f] T1 ≡ U1 →
                              ∃∃T2. ⬆*[f] T2 ≡ U2 & R K T1 T2.
 
+definition d_liftable2_bi: predicate (lenv → relation term) ≝
+                           λR. ∀K,T1,T2. R K T1 T2 → ∀b,f,L. ⬇*[b, f] L ≡ K →
+                           ∀U1. ⬆*[f] T1 ≡ U1 → 
+                           ∀U2. ⬆*[f] T2 ≡ U2 → R L U1 U2.
+
+definition d_deliftable2_bi: predicate (lenv → relation term) ≝
+                             λR. ∀L,U1,U2. R L U1 U2 → ∀b,f,K. ⬇*[b, f] L ≡ K →
+                             ∀T1. ⬆*[f] T1 ≡ U1 →
+                             ∀T2. ⬆*[f] T2 ≡ U2 → R K T1 T2.
+
 definition co_dropable_sn: predicate (rtmap → relation lenv) ≝
                            λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ →
                            ∀f2,L2. R f2 L1 L2 → ∀f1. f ~⊚ f1 ≡ f2 →
                            ∃∃K2. R f1 K1 K2 & ⬇*[b, f] L2 ≡ K2.
 
-
 definition co_dropable_dx: predicate (rtmap → relation lenv) ≝
                            λR. ∀f2,L1,L2. R f2 L1 L2 →
                            ∀b,f,K2. ⬇*[b, f] L2 ≡ K2 → 𝐔⦃f⦄ →
@@ -271,7 +284,7 @@ lemma drops_inv_pair2_isuni_next: ∀b,f,I,K,V,L1. 𝐔⦃f⦄ → ⬇*[b, ⫯f]
 [ #H elim (isid_inv_next … H) -H //
 | /2 width=5 by ex2_3_intro/
 ]
-qed-. 
+qed-.
 
 fact drops_inv_TF_aux: ∀f,L1,L2. ⬇*[Ⓕ, f] L1 ≡ L2 → 𝐔⦃f⦄ →
                        ∀I,K,V. L2 = K.ⓑ{I}V →