(**************************************************************************)
include "delayed_updating/substitution/lift.ma".
-(*
-include "ground/relocation/tr_uni_compose.ma".
-include "ground/relocation/tr_compose_compose.ma".
-include "ground/relocation/tr_compose_eq.ma".
-*)
include "ground/relocation/tr_pap_eq.ma".
include "ground/relocation/tr_pn_eq.ma".
-include "ground/lib/stream_tls_eq.ma".
(* LIFT FOR PATH ***********************************************************)
#k1 #k2 #Hk #f1 #f2 #Hf
[ <lift_empty <lift_empty /2 width=1 by/
| <lift_d_sn <lift_d_sn <(tr_pap_eq_repl ā¦ Hf)
- /3 width=3 by stream_tls_eq_repl, compose_repl_fwd_sn/
+ /3 width=1 by stream_eq_refl/
| /3 width=1 by/
| /3 width=1 by tr_push_eq_repl/
| /3 width=1 by/
qed.
lemma lift_path_d_sn (f) (p) (n):
- (š±(f@āØnā©)āā[ā*[n]f]p) = ā[f](š±nāp).
+ (š±(f@āØnā©)āā[š¢]p) = ā[f](š±nāp).
// qed.
lemma lift_path_m_sn (f) (p):
lemma lift_path_S_sn (f) (p):
(š¦āā[f]p) = ā[f](š¦āp).
// qed.
+
+lemma lift_path_id (p):
+ p = ā[š¢]p.
+#p elim p -p //
+* [ #n ] #p #IH //
+[ <lift_path_d_sn //
+| <lift_path_L_sn //
+]
+qed.
+
+lemma lift_path_append (p2) (p1) (f):
+ (ā[f]p1)ā(ā[ā[p1]f]p2) = ā[f](p1āp2).
+#p2 #p1 elim p1 -p1 //
+* [ #n1 ] #p1 #IH #f
+[ <lift_path_d_sn <lift_path_d_sn <IH //
+| <lift_path_m_sn <lift_path_m_sn <IH //
+| <lift_path_L_sn <lift_path_L_sn <IH //
+| <lift_path_A_sn <lift_path_A_sn <IH //
+| <lift_path_S_sn <lift_path_S_sn <IH //
+]
+qed.
+
+lemma lift_path_d_dx (n) (p) (f):
+ (ā[f]p)āš±((ā[p]f)@āØnā©) = ā[f](pāš±n).
+#n #p #f <lift_path_append //
+qed.
+
+lemma lift_path_m_dx (p) (f):
+ (ā[f]p)āšŗ = ā[f](pāšŗ).
+#p #f <lift_path_append //
+qed.
+
+lemma lift_path_L_dx (p) (f):
+ (ā[f]p)āš = ā[f](pāš).
+#p #f <lift_path_append //
+qed.
+
+lemma lift_path_A_dx (p) (f):
+ (ā[f]p)āš = ā[f](pāš).
+#p #f <lift_path_append //
+qed.
+
+lemma lift_path_S_dx (p) (f):
+ (ā[f]p)āš¦ = ā[f](pāš¦).
+#p #f <lift_path_append //
+qed.
+
(* COMMENT
(* Advanced constructions with proj_rmap and stream_tls *********************)