X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fsubstitution%2Fprelift_rmap.ma;h=94c358d1ba248d7bf1a2ed739f770495db79d3d7;hb=7008128d354c6e998a87bc2febe9f86ea714869c;hp=de7f40321f9052b9c11878eb7b3ef8177323699d;hpb=a4cacf8e269910184348a037106551dbc8a46fd4;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma index de7f40321..94c358d1b 100644 --- a/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma +++ b/matita/matita/contribs/lambdadelta/delayed_updating/substitution/prelift_rmap.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "delayed_updating/notation/functions/uparrow_2.ma". +include "delayed_updating/notation/functions/righttrianglearrow_2.ma". include "delayed_updating/syntax/label.ma". include "ground/relocation/tr_pn.ma". include "ground/lib/stream_tls.ma". @@ -21,7 +21,7 @@ include "ground/lib/stream_tls.ma". definition prelift_rmap (f) (l): tr_map ≝ match l with -[ label_d n ⇒ ⇂*[n]f +[ label_d k ⇒ ⇂*[k]f | label_m ⇒ f | label_L ⇒ ⫯f | label_A ⇒ f @@ -30,26 +30,26 @@ match l with interpretation "prelift (relocation map)" - 'UpArrow l f = (prelift_rmap f l). + 'RightTriangleArrow f l = (prelift_rmap f l). (* Basic constructions ******************************************************) -lemma prelift_rmap_d (f) (n:pnat): - ⇂*[n]f = ↑[𝗱n]f. +lemma prelift_rmap_d (f) (k:pnat): + ⇂*[k]f = 🠢[f]𝗱k. // qed. lemma prelift_rmap_m (f): - f = ↑[𝗺]f. + f = 🠢[f]𝗺. // qed. lemma prelift_rmap_L (f): - (⫯f) = ↑[𝗟]f. + (⫯f) = 🠢[f]𝗟. // qed. lemma prelift_rmap_A (f): - f = ↑[𝗔]f. + f = 🠢[f]𝗔. // qed. lemma prelift_rmap_S (f): - f = ↑[𝗦]f. + f = 🠢[f]𝗦. // qed.