theory of relocation updated .....

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc
new file mode 100644 (file)
index 0000000..d7356d0
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_drops.etc
@@ -0,0 +1,23 @@
+lemma pippo: ∀L1,L2,t1. ⬇*[Ⓕ, t1] L1 ≡ L2 → ∀t2. ⬇*[Ⓕ, t2] L1 ≡ L2 →
+|t1| + ∥t2∥ = ∥t1∥ + |t2|.
+#L1 #L2 #t1 #H elim H -L1 -L2 -t1
+[ #t1 #Ht1 #t2 #H elim (drops_inv_atom1 … H) -H
+  #_ #Ht2 >Ht1 -Ht1 // >Ht2 -Ht2 //
+| #I #L1 #L2 #V #t1 #_ #IH #t2 #H normalize 
+
+lemma drop_conf_div: ∀I1,L,K,V1,m1. ⬇[m1] L ≡ K.ⓑ{I1}V1 →
+                     ∀I2,V2,m2. ⬇[m2] L ≡ K.ⓑ{I2}V2 →
+                     ∧∧ m1 = m2 & I1 = I2 & V1 = V2.
+#I1 #L #K #V1 #m1 #HLK1 #I2 #V2 #m2 #HLK2
+elim (yle_split m1 m2) #H
+elim (yle_inv_plus_sn … H) -H #m #Hm
+[ lapply (drop_conf_ge … HLK1 … HLK2 … Hm ?)
+| lapply (drop_conf_ge … HLK2 … HLK1 … Hm ?)
+] -HLK1 -HLK2 // #HK
+lapply (drop_fwd_length … HK) #H
+elim (discr_yplus_x_xy … H) -H
+[1,3: #H elim (ylt_yle_false (|K.ⓑ{I1}V1|) (∞)) // ]
+#H destruct
+lapply (drop_inv_O2 … HK) -HK #H destruct
+/2 width=1 by and3_intro/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drop.ma
deleted file mode 100644 (file)
index 2bf29c6..0000000
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drop.ma
+++ /dev/null
@@ -1,35 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-include "basic_2/substitution/drop_drop.ma".
-include "basic_2/multiple/drops.ma".
-
-(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
-
-(* Properties concerning basic local environment slicing ********************)
-
-lemma drops_drop_trans: ∀L1,L,cs. ⬇*[Ⓕ, cs] L1 ≡ L → ∀L2,i. ⬇[i] L ≡ L2 →
-                        ∃∃L0,cs0,i0. ⬇[i0] L1 ≡ L0 & ⬇*[Ⓕ, cs0] L0 ≡ L2 &
-                                      @⦃i, cs⦄ ≡ i0 & cs ▭ i ≡ cs0.
-#L1 #L #cs #H elim H -L1 -L -cs
-[ /2 width=7 by drops_nil, minuss_nil, at_nil, ex4_3_intro/
-| #L1 #L0 #L #cs #l #m #_ #HL0 #IHL0 #L2 #i #HL2
-  elim (ylt_split i l) #Hil
-  [ elim (drop_trans_le … HL0 … HL2) -L /2 width=2 by ylt_fwd_le/
-    #L #HL0 #HL2 elim (IHL0 … HL0) -L0 /3 width=7 by drops_cons, minuss_lt, at_lt, ex4_3_intro/
-  | lapply (drop_trans_ge … HL0 … HL2 ?) -L // #HL02
-    elim (IHL0 … HL02) -L0 /3 width=7 by minuss_ge, at_ge, ex4_3_intro/
-  ]
-]
-qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
index 0ca46fa3c40120ad5e70fc5917055f1f4205c5cf..6a66289bd6f28f6e56ad0222650fc5bb080d59f7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma
@@ -16,7 +16,7 @@ include "ground_2/relocation/trace_isid.ma".
 include "basic_2/notation/relations/rliftstar_3.ma".
 include "basic_2/grammar/term.ma".
 
-(* GENERIC TERM RELOCATION **************************************************)
+(* GENERIC RELOCATION FOR TERMS *********************************************)
 
 (* Basic_1: includes:
             lift_sort lift_lref_lt lift_lref_ge lift_bind lift_flat
@@ -334,11 +334,11 @@ lemma is_lifts_dec: ∀T2,t. Decidable (∃T1. ⬆*[t] T1 ≡ T2).
 ]
 qed-.
 
-(* Basic_2A1: removed theorems 17:
-              lifts_inv_nil lifts_inv_cons lifts_total
+(* Basic_2A1: removed theorems 14:
+              lifts_inv_nil lifts_inv_cons
               lift_inv_Y1 lift_inv_Y2 lift_inv_lref_Y1 lift_inv_lref_Y2 lift_lref_Y lift_Y1
               lift_lref_lt_eq lift_lref_ge_eq lift_lref_plus lift_lref_pred
-              lift_lref_ge_minus lift_lref_ge_minus_eq lift_total lift_refl
+              lift_lref_ge_minus lift_lref_ge_minus_eq
 *)
 (* Basic_1: removed theorems 8:
             lift_lref_gt            

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
index b0e32002ce5738d92ef709814daacf5bfaecf195..3ac75012cc86b1de7c8f05cdee166f85af863c39 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/relocation/lifts.ma".
 
-(* GENERIC RELOCATION *******************************************************)
+(* GENERIC RELOCATION FOR TERMS *********************************************)
 
 (* Main properties **********************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma
index fb5953c267baa16fb83b74c28aa49544e1c792be..c1a088ee5d5c77bd67ab1967232936525ccdcbbf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts_vector.ma
@@ -15,7 +15,7 @@
 include "basic_2/relocation/lifts_lifts.ma".
 include "basic_2/relocation/lifts_vector.ma".
 
-(* GENERIC TERM VECTOR RELOCATION *******************************************)
+(* GENERIC RELOCATION FOR TERM VECTORS *************************************)
 
 (* Main properties **********************************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma
index 389f724d2322d6c340a9db7ff1bb53337f59660f..ae73703f7c4ff3e909dd3ffa296fa059ed8370da 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_simple.ma
@@ -15,7 +15,7 @@
 include "basic_2/grammar/term_simple.ma".
 include "basic_2/relocation/lifts.ma".
 
-(* GENERIC TERM RELOCATION **************************************************)
+(* GENERIC RELOCATION FOR TERMS *********************************************)
 
 (* Forward lemmas on simple terms *******************************************)
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
index 89ead4cf50755db4171137ffa791ea3ff2a8b2b7..159e9d869975b709c964da321294b1b2f752d59b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma
@@ -15,7 +15,7 @@
 include "basic_2/grammar/term_vector.ma".
 include "basic_2/relocation/lifts.ma".
 
-(* GENERIC TERM VECTOR RELOCATION *******************************************)
+(* GENERIC RELOCATION FOR TERM VECTORS *************************************)
 
 (* Basic_2A1: includes: liftv_nil liftv_cons *)
 inductive liftsv (t:trace) : relation (list term) ≝

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma
index 17952bba8b3029c231d27420bd08e1fda9127088..ace77ad27fba59cddc85c3dd473986d59c919a8b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_weight.ma
@@ -15,7 +15,7 @@
 include "basic_2/grammar/term_weight.ma".
 include "basic_2/relocation/lifts.ma".
 
-(* GENERIC TERM RELOCATION **************************************************)
+(* GENERIC RELOCATION FOR TERMS *********************************************)
 
 (* Forward lemmas on weight for terms ***************************************)