X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_compose_etc.ma;h=ba3915a973cb55a55a976a80c2336b6f1bc7cd9c;hb=ad6182251b8192ee7d25c53156afbce35e3715b6;hp=663dfc9b68684cd431e14aaffa4630496dae2a0f;hpb=04f2f61dbe017ee5a60fd30ae4b6ef355b6e8be4;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
index 663dfc9b6..ba3915a97 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_compose_etc.ma
@@ -12,46 +12,65 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(*
 include "ground/relocation/pstream_tls.ma".
 include "ground/relocation/pstream_istot.ma".
-include "ground/relocation/rtmap_after.ma".
+*)
+include "ground/arith/pnat_plus.ma".
+include "ground/relocation/pr_after.ma".
+include "ground/relocation/tr_map.ma".
 
 (* Properties on after (specific) *********************************************)
 
-lemma after_O2: ∀f2,f1,f. f2 ⊚ f1 ≘ f →
-                ∀p. p⨮f2 ⊚ ⫯f1 ≘ p⨮f.
+(*** after_O2 *)
+lemma tr_after_push_dx:
+      ∀f2,f1,f. 𝐭❨f2❩ ⊚ f1 ≘ 𝐭❨f❩ →
+      ∀p. 𝐭❨p⨮f2❩ ⊚ ⫯f1 ≘ 𝐭❨p⨮f❩.
 #f2 #f1 #f #Hf #p elim p -p
-/2 width=7 by gr_after_refl, gr_after_next/
+/2 width=7 by pr_after_refl, pr_after_next/
 qed.
 
-lemma after_S2: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f →
-                ∀p2. p2⨮f2 ⊚ ↑p1⨮f1 ≘ (p+p2)⨮f.
+(*** after_S2 *) 
+lemma tr_after_next_dx:
+      ∀f2,f1,f,p1,p. 𝐭❨f2❩ ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨p⨮f❩ →
+      ∀p2. 𝐭❨p2⨮f2❩ ⊚ 𝐭❨↑p1⨮f1❩ ≘ 𝐭❨(p+p2)⨮f❩.
 #f2 #f1 #f #p1 #p #Hf #p2 elim p2 -p2
-/2 width=7 by gr_after_next, gr_after_push/
+/2 width=7 by pr_after_next, pr_after_push/
 qed.
 
-lemma after_apply: ∀p1,f2,f1,f.
-      (⫰*[ninj p1] f2) ⊚ f1 ≘ f → f2 ⊚ p1⨮f1 ≘ f2@❨p1❩⨮f.
+include "ground/lib/stream_tls.ma".
+include "ground/relocation/tr_pap.ma".
+
+(*** after_apply *)
+lemma tr_after_pap:
+      ∀p1,f2,f1,f. 𝐭❨⇂*[ninj p1]f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f❩ →
+      (𝐭❨f2❩) ⊚ 𝐭❨p1⨮f1❩ ≘ 𝐭❨f2＠⧣❨p1❩⨮f❩.
 #p1 elim p1 -p1
-[ * /2 width=1 by after_O2/
+[ * /2 width=1 by tr_after_push_dx/
 | #p1 #IH * #p2 #f2 >nsucc_inj <stream_tls_swap
-  /3 width=1 by after_S2/
+  /3 width=1 by tr_after_next_dx/
 ]
 qed-.
 
-corec lemma after_total_aux: ∀f2,f1,f. f2 ∘ f1 = f → f2 ⊚ f1 ≘ f.
+include "ground/relocation/tr_compose_pn.ma".
+
+(*** after_total_aux *)
+corec fact tr_after_total_aux:
+      ∀f2,f1,f. f2 ∘ f1 = f → 𝐭❨f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f❩.
 * #p2 #f2 * #p1 #f1 * #p #f cases p2 -p2
 [ cases p1 -p1
-  [ #H cases (compose_inv_O2 … H) -H /3 width=7 by gr_after_refl, eq_f2/
-  | #p1 #H cases (compose_inv_S2 … H) -H * -p /3 width=7 by gr_after_push/
+  [ #H cases (tr_compose_inv_push_dx … H) -H /3 width=7 by pr_after_refl, eq_f2/
+  | #p1 #H cases (tr_compose_inv_succ_dx … H) -H * -p /3 width=7 by pr_after_push/
   ]
-| #p2 >gr_next_unfold #H cases (compose_inv_S1 … H) -H * -p >gr_next_unfold
-  /3 width=5 by gr_after_next/
+| #p2 >tr_next_unfold #H cases (tr_compose_inv_next_sn … H) -H * -p
+  /3 width=5 by pr_after_next/
 ]
 qed-.
 
-theorem after_total: ∀f1,f2. f2 ⊚ f1 ≘ f2 ∘ f1.
-/2 width=1 by after_total_aux/ qed.
+(*** after_total *)
+theorem tr_after_total:
+        ∀f1,f2. 𝐭❨f2❩ ⊚ 𝐭❨f1❩ ≘ 𝐭❨f2 ∘ f1❩.
+/2 width=1 by tr_after_total_aux/ qed.
 
 (* Inversion lemmas on after (specific) ***************************************)
 
@@ -89,12 +108,12 @@ lemma after_inv_const: ∀f2,f1,f,p1,p.
 ]
 qed-.
 
-lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≡ f.
+lemma after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≐ f.
 /2 width=4 by gr_after_mono/ qed-.
 
 (* Forward lemmas on after (specific) *****************************************)
 
-lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2@❨p1❩ = p.
+lemma after_fwd_hd: ∀f2,f1,f,p1,p. f2 ⊚ p1⨮f1 ≘ p⨮f → f2＠⧣❨p1❩ = p.
 #f2 #f1 #f #p1 #p #H lapply (gr_after_des_pat ? p1 (𝟏) … H) -H [4:|*: // ]
 /3 width=2 by at_inv_O1, sym_eq/
 qed-.
@@ -109,10 +128,6 @@ lemma after_fwd_tls: ∀f,f1,p1,f2,p2,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
 qed-.
 
 lemma after_inv_apply: ∀f2,f1,f,p2,p1,p. p2⨮f2 ⊚ p1⨮f1 ≘ p⨮f →
-                       (p2⨮f2)@❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
+                       (p2⨮f2)＠⧣❨p1❩ = p ∧ (⫰*[↓p1]f2) ⊚ f1 ≘ f.
 /3 width=3 by after_fwd_tls, after_fwd_hd, conj/ qed-.
 
-(* Properties on apply ******************************************************)
-
-lemma compose_apply (f2) (f1) (i): f2@❨f1@❨i❩❩ = (f2∘f1)@❨i❩.
-/4 width=6 by gr_after_des_pat, at_inv_total, sym_eq/ qed.