X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fpr_compose.ma;h=71a256c103633dbe7cacf85dca2c43f326c72a1a;hb=ad6182251b8192ee7d25c53156afbce35e3715b6;hp=0629472e2f285e126f48da111e62ca4d66470066;hpb=f8b4eb67c2437f7b5174d7dca46e102e0ac0d19d;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
index 0629472e2..71a256c10 100644
--- a/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/pr_compose.ma
@@ -12,9 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/relocation/pr_after.ma".
+include "ground/relocation/pr_after_after.ma".
 
-(* RELATIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************)
+(* FUNCTIONAL COMPOSITION FOR PARTIAL RELOCATION MAPS ***********************)
 
 corec definition pr_compose: pr_map → pr_map → pr_map.
 * * #g2 [ #f1 | * * #g1 ]
@@ -28,7 +28,7 @@ interpretation
   "functional composition (partial relocation maps)"
   'compose f2 f1 = (pr_compose f2 f1).
 
-(* Basic constructions (specific) *******************************************)
+(* Basic constructions ******************************************************)
 
 lemma pr_compose_unfold_refl (f2) (f1): ⫯(f2∘f1) = (⫯f2)∘(⫯f1).
 #f2 #f1
@@ -40,6 +40,7 @@ lemma pr_compose_unfold_push (f2) (f1): ↑(f2∘f1) = (⫯f2)∘(↑f1).
 <(stream_unfold … ((⫯f2)∘(↑f1))) in ⊢ (???%); //
 qed.
 
+(*** compose_next *)
 lemma pr_compose_unfold_next (f2) (f1):
       ↑(f2∘f1) = (↑f2)∘f1.
 #f2 #f1
@@ -48,7 +49,8 @@ qed.
 
 (* Main constructions *******************************************************)
 
-corec theorem pr_after_compose (f2) (f1):
+(*** after_total *)
+corec theorem pr_after_total (f2) (f1):
               f2 ⊚ f1 ≘ f2∘f1.
 cases (pr_map_split_tl f2)*
 [ cases (pr_map_split_tl f1) * ]
@@ -57,3 +59,9 @@ cases (pr_map_split_tl f2)*
 | @pr_after_next /2 width=5 by/
 ]
 qed.
+
+(* Main inversions **********************************************************)
+
+(*** after_inv_total *)
+lemma pr_after_inv_total: ∀f2,f1,f. f2 ⊚ f1 ≘ f → f2 ∘ f1 ≐ f.
+/2 width=4 by pr_after_mono/ qed-.