rec definition lift_rmap (f) (p) on p: tr_map ≝
match p with
[ list_empty ⇒ f
-| list_lcons l q ⇒ ↑[l](lift_rmap f q)
+| list_lcons l q ⇒ 🠢[lift_rmap f q]l
].
interpretation
"lift (relocation map)"
- 'UpArrow p f = (lift_rmap f p).
+ 'RightTriangleArrow f p = (lift_rmap f p).
(* Basic constructions ******************************************************)
lemma lift_rmap_empty (f):
- f = ↑[𝐞]f.
+ f = 🠢[f]𝐞.
// qed.
lemma lift_rmap_rcons (f) (p) (l):
- ↑[l]↑[p]f = ↑[p◖l]f.
+ 🠢[🠢[f]p]l = 🠢[f](p◖l).
// qed.
lemma lift_rmap_d_dx (f) (p) (k:pnat):
- ⇂*[k](↑[p]f) = ↑[p◖𝗱k]f.
+ ⇂*[k](🠢[f]p) = 🠢[f](p◖𝗱k).
// qed.
lemma lift_rmap_m_dx (f) (p):
- ↑[p]f = ↑[p◖𝗺]f.
+ 🠢[f]p = 🠢[f](p◖𝗺).
// qed.
lemma lift_rmap_L_dx (f) (p):
- (⫯↑[p]f) = ↑[p◖𝗟]f.
+ (⫯🠢[f]p) = 🠢[f](p◖𝗟).
// qed.
lemma lift_rmap_A_dx (f) (p):
- ↑[p]f = ↑[p◖𝗔]f.
+ 🠢[f]p = 🠢[f](p◖𝗔).
// qed.
lemma lift_rmap_S_dx (f) (p):
- ↑[p]f = ↑[p◖𝗦]f.
+ 🠢[f]p = 🠢[f](p◖𝗦).
// qed.
(* Constructions with path_append *******************************************)
lemma lift_rmap_append (p) (q) (f):
- ↑[q]↑[p]f = ↑[p●q]f.
+ 🠢[🠢[f]p]q = 🠢[f](p●q).
#p #q elim q -q //
qed.
(* Constructions with path_lcons ********************************************)
lemma lift_rmap_lcons (f) (p) (l):
- ↑[p]↑[l]f = ↑[l◗p]f.
+ 🠢[🠢[f]l]p = 🠢[f](l◗p).
// qed.
lemma lift_rmap_d_sn (f) (p) (k:pnat):
- ↑[p](⇂*[k]f) = ↑[𝗱k◗p]f.
+ 🠢[⇂*[k]f]p = 🠢[f](𝗱k◗p).
// qed.
lemma lift_rmap_m_sn (f) (p):
- ↑[p]f = ↑[𝗺◗p]f.
+ 🠢[f]p = 🠢[f](𝗺◗p).
// qed.
lemma lift_rmap_L_sn (f) (p):
- ↑[p](⫯f) = ↑[𝗟◗p]f.
+ 🠢[⫯f]p = 🠢[f](𝗟◗p).
// qed.
lemma lift_rmap_A_sn (f) (p):
- ↑[p]f = ↑[𝗔◗p]f.
+ 🠢[f]p = 🠢[f](𝗔◗p).
// qed.
lemma lift_rmap_S_sn (f) (p):
- ↑[p]f = ↑[𝗦◗p]f.
+ 🠢[f]p = 🠢[f](𝗦◗p).
// qed.