X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Flift_update.ma;h=e30fc9d19b260c4dc06b152d9de4ba91414680eb;hb=62d0f5f2c89830ebe884e6afee91eb68b68790fc;hp=999b0e188cb97d1f018b8a89ce282550bc7ac5b1;hpb=be152b5436a8e1e107684722be834dbe02196d53;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.ma
index 999b0e188..e30fc9d19 100644
--- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.ma
+++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.ma
@@ -21,15 +21,48 @@ include "ground/lib/stream_eq_eq.ma".
 
 (* Constructions with update ***********************************************)
 
-axiom arith1 (p,q:pnat) (n:nat):
-      nrplus (pplus p q) n = pplus p (nrplus q n).
+lemma lift_rmap_pap_le (f1) (f2) (p) (m:pnat) (l:nat):
+      ninj (m+⧣p+l) = ❘p❘ →
+      (↑[p]f1)@❨m❩ = (↑[p]f2)@❨m❩.
+#f1 #f2 #p @(list_ind_rcons … p) -p
+[ #m #l <depth_empty #H0 destruct
+| #p * [ #n ] #IH #m #l
+  [ <update_d_dx <depth_d_dx <lift_rmap_pap_d_dx <lift_rmap_pap_d_dx
+    <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <nrplus_pplus_assoc
+    #H0 <(IH … l) -IH //
+  | /2 width=2 by/
+  | <update_L_dx <depth_L_dx <lift_rmap_L_dx <lift_rmap_L_dx
+    cases m -m // #m
+    <nrplus_succ_sn <nrplus_succ_sn >nsucc_inj #H0
+    <tr_pap_push <tr_pap_push
+    <(IH … l) -IH //
+  | /2 width=2 by/
+  | /2 width=2 by/
+  ]
+]
+qed.
 
-lemma pippo (f) (p) (m:pnat):
+lemma lift_rmap_pap_gt (f) (p) (m):
+      f@❨m+⧣p❩+❘p❘ = (↑[p]f)@❨m+❘p❘❩.
+#f #p @(list_ind_rcons … p) -p [ // ]
+#p * [ #n ] #IH #m
+[ <update_d_dx <depth_d_dx
+  <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <nrplus_pplus_assoc
+  <lift_rmap_pap_d_dx >IH -IH //
+| //
+| <update_L_dx <depth_L_dx
+  <nrplus_succ_dx <nrplus_succ_dx <lift_rmap_L_dx <tr_pap_push //
+| //
+| //
+]
+qed.
+
+lemma lift_rmap_tls_gt (f) (p) (m:pnat):
       ⇂*[ninj (m+⧣p)]f ≗ ⇂*[ninj (m+❘p❘)]↑[p]f.
 #f #p @(list_ind_rcons … p) -p [ // ]
 #p * [ #n ] #IH #m
 [ <update_d_dx <depth_d_dx
-  <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <arith1
+  <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <nrplus_pplus_assoc
   @(stream_eq_trans … (lift_rmap_tls_d_dx …))
   @(stream_eq_canc_dx … (IH …)) -IH //
 | //
@@ -38,4 +71,13 @@ lemma pippo (f) (p) (m:pnat):
 | //
 | //
 ]
-qed.  
+qed.
+
+lemma lift_rmap_tls_eq (f) (p):
+      ⇂*[⧣p]f ≗ ⇂*[↑❘p❘]↑[p]⫯f.
+(*
+#f #p @(list_ind_rcons … p) -p //
+#p * [ #n ] #IH //
+<update_d_dx <depth_d_dx <lift_rmap_d_dx
+@(stream_eq_trans … (tr_tls_compose_uni_dx …))
+*)