X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Frelocation%2Frtmap_after.ma;h=a28f7b384a76697ad88453e5b109db45731a4b2e;hb=528f8ea107f689d07d060e1d31ba32bf65b4e6ba;hp=fef08518974b72a1862df14594b6d53d4446ad3a;hpb=f215e6c18fbd22a049e6d34cf3bb52b0cabc4d58;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
index fef085189..a28f7b384 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/rtmap_after.ma
@@ -1,3 +1,4 @@
+
 (**************************************************************************)
 (*       ___                                                              *)
 (*      ||M||                                                             *)
@@ -13,7 +14,6 @@
 (**************************************************************************)
 
 include "ground_2/notation/relations/rafter_3.ma".
-include "ground_2/relocation/rtmap_sor.ma".
 include "ground_2/relocation/rtmap_istot.ma".
 
 (* RELOCATION MAP ***********************************************************)
@@ -271,8 +271,10 @@ lemma after_mono_eq: ∀f1,f2,f. f1 ⊚ f2 ≡ f → ∀g1,g2,g. g1 ⊚ g2 ≡ g
 lemma after_tls: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n → 
                  f1 ⊚ f2 ≡ f → ⫱*[n]f1 ⊚ f2 ≡ ⫱*[n]f.
 #n elim n -n //
-#n #IH #f1 #f2 #f #Hf1 #Hf cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ]
-#g1 #Hg1 #H1 cases (after_inv_nxx … Hf … H1) -Hf /2 width=1 by/
+#n #IH #f1 #f2 #f #Hf1 #Hf
+cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ] #g1 #Hg1 #H1
+cases (after_inv_nxx … Hf … H1) -Hf #g #Hg #H0 destruct
+<tls_xn <tls_xn /2 width=1 by/
 qed.
 
 (* Properties on isid *******************************************************)
@@ -335,36 +337,10 @@ qed.
 (* Properties on uni ********************************************************)
 
 lemma after_uni: ∀n1,n2. 𝐔❴n1❵ ⊚ 𝐔❴n2❵ ≡ 𝐔❴n1+n2❵.
-@nat_elim2
-/4 width=5 by after_uni_next2, after_isid_sn, after_isid_dx, after_next/
+@nat_elim2 [3: #n #m <plus_n_Sm ] (**) (* full auto fails *)
+/4 width=5 by after_uni_next2, after_isid_dx, after_isid_sn, after_next/
 qed.
 
-(* Inversion lemmas on sor **************************************************)
-
-lemma sor_isid: ∀f1,f2,f. 𝐈⦃f1⦄ → 𝐈⦃f2⦄ → 𝐈⦃f⦄ → f1 ⋓ f2 ≡ f.
-/4 width=3 by sor_eq_repl_back2, sor_eq_repl_back1, isid_inv_eq_repl/ qed.
-(*
-lemma after_inv_sor: ∀f. 𝐅⦃f⦄ → ∀f2,f1. f2 ⊚ f1 ≡ f → ∀fa,fb. fa ⋓ fb ≡ f →
-                     ∃∃f1a,f1b. f2 ⊚ f1a ≡ fa & f2 ⊚ f1b ≡ fb & f1a ⋓ f1b ≡ f1.
-@isfin_ind
-[ #f #Hf #f2 #f1 #H1f #fa #fb #H2f
-  elim (after_inv_isid3 … H1f) -H1f //
-  elim (sor_inv_isid3 … H2f) -H2f //
-  /3 width=5 by ex3_2_intro, after_isid_sn, sor_isid/
-| #f #_ #IH #f2 #f1 #H1 #fa #fb #H2
-  elim (after_inv_xxp … H1) -H1 [ |*: // ] #g2 #g1 #H1f
-  elim (sor_inv_xxp … H2) -H2 [ |*: // ] #ga #gb #H2f
-  elim (IH … H1f … H2f) -f /3 width=11 by sor_pp, after_refl, ex3_2_intro/
-| #f #_ #IH #f2 #f1 #H1 #fa #fb #H2
-  elim (sor_inv_xxn … H2) -H2 [1,3,4: * |*: // ] #ga #gb #H2f
-  elim (after_inv_xxn … H1) -H1 [1,3,5,7,9,11: * |*: // ] #g2 [1,3,5: #g1 ] #H1f
-  elim (IH … H1f … H2f) -f
-  /3 width=11 by sor_np, sor_pn, sor_nn, after_refl, after_push, after_next, ex3_2_intro/
-  #x1a #x1b #H39 #H40 #H41 #H42 #H43 #H44
-  [ @ex3_2_intro
-    [3: /2 width=7 by after_next/ | skip
-    |5: @H41 | skip  
-*)
 (* Forward lemmas on at *****************************************************)
 
 lemma after_at_fwd: ∀i,i1,f. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f →
@@ -439,10 +415,10 @@ lemma after_uni_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
   elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
   [ #g2 #j1 #Hg2 #H1 #H2 destruct
     elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   | #g2 #Hg2 #H2 destruct
     elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   ]
 ]
 qed.
@@ -475,10 +451,10 @@ lemma after_uni_succ_dx: ∀i2,i1,f2. @⦃i1, f2⦄ ≡ i2 →
   elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
   [ #g2 #j1 #Hg2 #H1 #H2 destruct
     elim (after_inv_pnx … Hf) -Hf [ |*: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   | #g2 #Hg2 #H2 destruct
     elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct
-    /3 width=5 by after_next/
+    <tls_xn /3 width=5 by after_next/
   ]
 ]
 qed.