From f1c1453b618f8028476d0f473e314e5a9492f30b Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 12 Oct 2011 12:01:06 +0000
Subject: [PATCH] theory of ltpss completed!

---
 .../lambda_delta/Basic_2/unfold/ltpss_drop.ma | 142 ++++++------------
 1 file changed, 42 insertions(+), 100 deletions(-)

diff --git a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_drop.ma b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_drop.ma
index 6b45b4628..10ef14016 100644
--- a/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_drop.ma
+++ b/matita/matita/contribs/lambda_delta/Basic_2/unfold/ltpss_drop.ma
@@ -11,122 +11,64 @@
 (*        v         GNU General Public License Version 2                  *)
 (*                                                                        *)
 (**************************************************************************)
-(*
-include "Basic_2/substitution/ltps.ma".
 
-(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
+include "Basic_2/substitution/ltps_drop.ma".
+include "Basic_2/unfold/ltpss.ma".
 
-lemma ltps_drop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
-                         ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
-                         d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
-#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H //
-| //
-| normalize #K0 #K1 #I #V0 #V1 #e1 #_ #_ #IHK01 #L2 #e2 #H #He12
-  lapply (plus_le_weak … He12) #He2
-  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
-  lapply (IHK01 … HK0L2 ?) -IHK01 HK0L2 /2/
-| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2
-  lapply (plus_le_weak … Hd1e2) #He2
-  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
-  lapply (IHK01 … HK0L2 ?) -IHK01 HK0L2 /2/
-]
-qed.
+(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
 
-lemma ltps_drop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
+lemma ltpss_drop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
                           ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
                           d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
-#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H //
-| //
-| normalize #K1 #K0 #I #V1 #V0 #e1 #_ #_ #IHK10 #L2 #e2 #H #He12
-  lapply (plus_le_weak … He12) #He2
-  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
-  lapply (IHK10 … HK0L2 ?) -IHK10 HK0L2 /2/
-| #K0 #K1 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2
-  lapply (plus_le_weak … Hd1e2) #He2
-  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
-  lapply (IHK10 … HK0L2 ?) -IHK10 HK0L2 /2/
-]
+#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 /3 width=6/
 qed.
 
-lemma ltps_drop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
-                         ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
-                         ∃∃L. L2 [0, d1 + e1 - e2] ≫ L & ↓[0, e2] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
-| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
-  lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2;
-  lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/
-| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #_ #He21
-  lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2
-  [ destruct -IHK01 He21 e2 L2 <minus_n_O /3/
-  | -HK01 HV01 <minus_le_minus_minus_comm //
-    elim (IHK01 … HK0L2 ? ?) -IHK01 HK0L2 /3/
-  ]
-| #K0 #K1 #I #V0 #V1 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK01 #L2 #e2 #H #Hd1e2 #He2de1
-  lapply (plus_le_weak … Hd1e2) #He2
-  <minus_le_minus_minus_comm //
-  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
-  elim (IHK01 … HK0L2 ? ?) -IHK01 HK0L2 /3/
-]
+lemma ltpss_drop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
+                           ∀L2,e2. ↓[0, e2] L0 ≡ L2 →
+                           d1 + e1 ≤ e2 → ↓[0, e2] L1 ≡ L2.
+#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 /3 width=6/
 qed.
 
-lemma ltps_drop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
+lemma ltpss_drop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
                           ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
-                          ∃∃L. L [0, d1 + e1 - e2] ≫ L2 & ↓[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
-| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
-  lapply (le_n_O_to_eq … He2) -He2 #H destruct -e2;
-  lapply (drop_inv_refl … HL2) -HL2 #H destruct -L2 /2/
-| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #_ #He21
-  lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2
-  [ destruct -IHK10 He21 e2 L2 <minus_n_O /3/
-  | -HK10 HV10 <minus_le_minus_minus_comm //
-    elim (IHK10 … HK0L2 ? ?) -IHK10 HK0L2 /3/
-  ]
-| #K1 #K0 #I #V1 #V0 #d1 #e1 >plus_plus_comm_23 #_ #_ #IHK10 #L2 #e2 #H #Hd1e2 #He2de1
-  lapply (plus_le_weak … Hd1e2) #He2
-  <minus_le_minus_minus_comm //
-  lapply (drop_inv_drop1 … H ?) -H // #HK0L2
-  elim (IHK10 … HK0L2 ? ?) -IHK10 HK0L2 /3/
+                          ∃∃L. L2 [0, d1 + e1 - e2] ≫* L & ↓[0, e2] L1 ≡ L.
+#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
+[ /2/
+| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
+  elim (IHL … HL02 Hd1e2 He2de1) -L0 #L0 #HL20 #HL0
+  elim (ltps_drop_conf_be … HL1 … HL0 Hd1e2 He2de1) -L /3/
 ]
 qed.
 
-lemma ltps_drop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
-                         ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
-                         ∃∃L. L2 [d1 - e2, e1] ≫ L & ↓[0, e2] L1 ≡ L.
-#L0 #L1 #d1 #e1 #H elim H -H L0 L1 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
-| /2/
-| normalize #K0 #K1 #I #V0 #V1 #e1 #HK01 #HV01 #_ #L2 #e2 #H #He2
-  lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2;
-  lapply (drop_inv_refl … H) -H #H destruct -L2 /3/
-| #K0 #K1 #I #V0 #V1 #d1 #e1 #HK01 #HV01 #IHK01 #L2 #e2 #H #He2d1
-  lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2
-  [ destruct -IHK01 He2d1 e2 L2 <minus_n_O /3/
-  | -HK01 HV01 <minus_le_minus_minus_comm //
-    elim (IHK01 … HK0L2 ?) -IHK01 HK0L2 /3/
-  ]
+lemma ltpss_drop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
+                           ∀L2,e2. ↓[0, e2] L0 ≡ L2 → d1 ≤ e2 → e2 ≤ d1 + e1 →
+                           ∃∃L. L [0, d1 + e1 - e2] ≫* L2 & ↓[0, e2] L1 ≡ L.
+#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
+[ /2/
+| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
+  elim (ltps_drop_trans_be … HL0 … HL02 Hd1e2 He2de1) -L0 #L0 #HL02 #HL0
+  elim (IHL … HL0 Hd1e2 He2de1) -L /3/
 ]
 qed.
 
-lemma ltps_drop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
+lemma ltpss_drop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
                           ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
-                          ∃∃L. L [d1 - e2, e1] ≫ L2 & ↓[0, e2] L1 ≡ L.
-#L1 #L0 #d1 #e1 #H elim H -H L1 L0 d1 e1
-[ #d1 #e1 #L2 #e2 #H >(drop_inv_atom1 … H) -H /2/
-| /2/
-| normalize #K1 #K0 #I #V1 #V0 #e1 #HK10 #HV10 #_ #L2 #e2 #H #He2
-  lapply (le_n_O_to_eq … He2) -He2 #He2 destruct -e2;
-  lapply (drop_inv_refl … H) -H #H destruct -L2 /3/
-| #K1 #K0 #I #V1 #V0 #d1 #e1 #HK10 #HV10 #IHK10 #L2 #e2 #H #He2d1
-  lapply (drop_inv_O1 … H) -H * * #He2 #HK0L2
-  [ destruct -IHK10 He2d1 e2 L2 <minus_n_O /3/
-  | -HK10 HV10 <minus_le_minus_minus_comm //
-    elim (IHK10 … HK0L2 ?) -IHK10 HK0L2 /3/
-  ]
+                          ∃∃L. L2 [d1 - e2, e1] ≫* L & ↓[0, e2] L1 ≡ L.
+#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
+[ /2/
+| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1
+  elim (IHL … HL02 He2d1) -L0 #L0 #HL20 #HL0
+  elim (ltps_drop_conf_le … HL1 … HL0 He2d1) -L /3/
+]
+qed.
+
+lemma ltpss_drop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
+                           ∀L2,e2. ↓[0, e2] L0 ≡ L2 → e2 ≤ d1 →
+                           ∃∃L. L [d1 - e2, e1] ≫* L2 & ↓[0, e2] L1 ≡ L.
+#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
+[ /2/
+| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1
+  elim (ltps_drop_trans_le … HL0 … HL02 He2d1) -L0 #L0 #HL02 #HL0
+  elim (IHL … HL0 He2d1) -L /3/
 ]
 qed.
-*)
-- 
2.39.2