update in ground

+ additions on tr_pap

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
index 59256fbbb2cfab01c61153504911eb5fea8a6881..34f7ca78c6b2c35bfeeae99931221c160e0bbf20 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_id_pap.ma
@@ -12,8 +12,8 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground/relocation/tr_pap.ma".
-include "ground/relocation/tr_id.ma".
+include "ground/relocation/tr_pap_pushs.ma".
+include "ground/relocation/tr_id_pushs.ma".
 
 (* IDENTITY ELEMENT FOR TOTAL RELOCATION MAPS *******************************)
 
@@ -21,6 +21,6 @@ include "ground/relocation/tr_id.ma".
 
 lemma tr_pap_id (p):
       p = 𝐢@❨p❩.
-#p elim p -p //
-#p #IH <tr_id_unfold <tr_pap_succ //
+#p >(tr_pushs_id p)
+/2 width=1 by tr_pap_pushs_le/
 qed.

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma
index 65cb40105072455c645d23178671263486846082..c3cacbbd493457421174fc3d189b578489dff511 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pap.ma
@@ -14,6 +14,8 @@
 
 include "ground/relocation/tr_pap_pat.ma".
 
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
 (* Main inversions **********************************************************)
 
 (*** apply_inj *)

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
index 96eaa241f056e7d273d31dde50d4bf36ef1e02b7..ce4a0aa3229524ca1dd505e53dc7840538f5bcb7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pn.ma
@@ -17,6 +17,12 @@ include "ground/relocation/tr_pap.ma".
 
 (* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
 
+(* Constructions with tr_push ***********************************************)
+
+lemma tr_pap_push (f):
+      ∀i. ↑(f@❨i❩) = (⫯f)@❨↑i❩.
+// qed.
+
 (* Constructions with tr_next ***********************************************)
 
 (*** apply_S2 *)

diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma
new file mode 100644 (file)
index 0000000..6fe65c8
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pap_pushs.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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 "ground/arith/pnat_lt.ma".
+include "ground/relocation/tr_pushs.ma".
+include "ground/relocation/tr_pap_pn.ma".
+
+(* POSITIVE APPLICATION FOR TOTAL RELOCATION MAPS ***************************)
+
+(* Constructions with tr_pushs **********************************************)
+
+lemma tr_pap_pushs_le (n) (p) (f):
+      p < ↑n → p = (⫯*[n]f)@❨p❩.
+#n @(nat_ind_succ … n) -n
+[ #p #f #H0
+  elim (plt_inv_unit_dx … H0)
+| #n #IH *
+  [ #f #H0 <tr_pushs_succ //
+  | #p #f <npsucc_succ #H0
+    lapply (plt_inv_succ_bi … H0) -H0 #H0
+    lapply (IH … f H0) -IH -H0 #H0
+    <tr_pushs_succ <tr_pap_push //
+  ]
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
index 71470225eb9e2cff8ea465af5b3931b6a3992b98..05ba00fe433c991a9ff89ecacfb7e5344d9cdb5b 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
+++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl
@@ -33,7 +33,7 @@ table {
           [ "tr_uni ( 𝐮❨?❩ )" * ]
           [ "tr_id ( 𝐢 ) " "tr_id_pushs" "tr_id_pap" * ]
           [ "tr_compose ( ?∘? )" "tr_compose_pn" * ]
-          [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pap" * ]
+          [ "tr_pap ( ?@❨?❩ )" "tr_pap_eq" "tr_pap_pat" "tr_pap_pn" "tr_pap_pushs" "tr_pap_pap" * ]
           [ "tr_pushs ( ⫯*[?]? )" * ]
           [ "tr_pn ( ⫯? ) ( ↑? )" "tr_pn_hdtl" "tr_pn_tls" * ]
           [ "tr_map ( 𝐭❨?❩ )" "tr_eq" "tr_nexts" "tr_pat" "tr_ist" * ]