(**************************************************************************)
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=1 by stream_eq_refl/
+ /3 width=3 by stream_tls_eq_repl, compose_repl_fwd_sn/
| /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ā©)āā[š¢]p) = ā[f](š±nāp).
+ (š±(f@āØnā©)āā[ā*[n]f]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 *********************)