include "delayed_updating/syntax/path_balanced.ma".
include "delayed_updating/syntax/path_depth.ma".
include "delayed_updating/notation/relations/black_rightarrow_df_4.ma".
-include "ground/arith/nat_rplus.ma".
include "ground/xoa/ex_1_2.ma".
include "ground/xoa/and_4.ma".
@(subset_eq_canc_dx … (lift_term_after …))
@lift_term_eq_repl_sn -t1
@(stream_eq_trans … (tr_compose_uni_dx …))
+ @tr_compose_eq_repl
(*
>nrplus_inj_dx <tr_pap_plus
*)
(* *)
(**************************************************************************)
-include "ground/relocation/tr_compose.ma".
-include "ground/relocation/tr_uni.ma".
+include "ground/relocation/tr_compose_pap.ma".
+include "ground/relocation/tr_uni_pap.ma".
include "delayed_updating/syntax/path.ma".
include "delayed_updating/notation/functions/uparrow_4.ma".
include "delayed_updating/notation/functions/uparrow_2.ma".
↑[p]f = ↑[p◖𝗦]f.
// qed.
+lemma lift_rmap_pap_d_dx (f) (p) (n) (m):
+ ↑[p]f@❨m+n❩ = ↑[p◖𝗱n]f@❨m❩.
+#f #p #n #m
+<lift_rmap_d_dx <tr_compose_pap <tr_uni_pap //
+qed.
+
(* Advanced eliminations with path ******************************************)
lemma path_ind_lift (Q:predicate …):
include "delayed_updating/substitution/lift.ma".
include "delayed_updating/syntax/path_depth.ma".
-include "ground/relocation/tr_pushs.ma".
+include "ground/relocation/tr_id_compose.ma".
+include "ground/relocation/tr_compose_compose.ma".
+include "ground/relocation/tr_compose_pn.ma".
+include "ground/relocation/tr_compose_eq.ma".
+include "ground/relocation/tr_pn_eq.ma".
+include "ground/lib/stream_eq_eq.ma".
(* LIFT FOR PATH ***********************************************************)
-(* Basic constructions with depth ******************************************)
+(* Constructions with depth ************************************************)
-lemma pippo (p) (f):
- (⫯*[❘p❘]f) ∘ (↑[p]𝐢) = ↑[p]f.
-#p elim p -p
-[ #f <lift_rmap_empty <lift_rmap_empty <tr_pushs_zero
-| * [ #n ] #p #IH #f //
- <lift_rmap_d_sn <lift_rmap_d_sn <depth_d_sn
- @(trans_eq … (IH …)) -IH
-
+lemma lift_rmap_decompose (p) (f):
+ ↑[p]f ≗ (⫯*[❘p❘]f)∘(↑[p]𝐢).
+#p @(list_ind_rcons … p) -p
+[ #f <lift_rmap_empty <lift_rmap_empty <tr_pushs_zero //
+| #p * [ #n ] #IH #f //
+ [ <lift_rmap_d_dx <lift_rmap_d_dx <depth_d_dx
+ @(stream_eq_trans … (tr_compose_assoc …))
+ /2 width=1 by tr_compose_eq_repl/
+ | <lift_rmap_L_dx <lift_rmap_L_dx <depth_L_dx
+ <tr_pushs_succ <tr_compose_push_bi
+ /2 width=1 by tr_push_eq_repl/
+ ]
+]
+qed.
include "delayed_updating/substitution/lift.ma".
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_depth.ma".
-include "ground/relocation/tr_pushs.ma".
include "ground/arith/nat_pred_succ.ma".
(* LIFT FOR PATH ***********************************************************)
(* 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 //
| //
| //
| //
]
-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 …))
+*)