X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Fgr_tls.ma;h=6b52f797142e07007f2f7864fe3cf1714d1066b3;hb=8bbe582d87984526f40182c4409cbfd43108cb79;hp=6d2ddc203c9475c5c671b0a37500bf986b6ba825;hpb=55c768d7e45babb300b5010463ba3196a68f1bbe;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma index 6d2ddc203..6b52f7971 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/gr_tls.ma @@ -12,33 +12,33 @@ (* *) (**************************************************************************) -include "ground/notation/functions/droppreds_2.ma". +include "ground/notation/functions/downspoonstar_2.ma". include "ground/lib/stream_tls.ma". include "ground/relocation/gr_tl.ma". -(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ***********************************************************) +(* ITERATED TAIL FOR GENERIC RELOCATION MAPS ********************************) (*** tls *) -definition gr_tls (n) (f:gr_map) ≝ ⫰*[n]f. +definition gr_tls (n) (f:gr_map) ≝ ⇂*[n]f. interpretation "iterated tail (generic relocation maps)" - 'DropPreds n f = (gr_tls n f). + 'DownSpoonStar n f = (gr_tls n f). -(* Basic properties (specific) *********************************************************) +(* Basic constructions (specific) *******************************************) (*** tls_O *) -lemma gr_tls_zero (f): f = ⫱*[𝟎] f. +lemma gr_tls_zero (f): f = ⫰*[𝟎] f. // qed. (*** tls_swap *) -lemma gr_tls_tl (n) (f): ⫱⫱*[n] f = ⫱*[n] ⫱f. +lemma gr_tls_tl (n) (f): ⫰⫰*[n] f = ⫰*[n] ⫰f. /2 width=1 by stream_tls_tl/ qed. (*** tls_S *) -lemma gr_tls_succ (n) (f): ⫱⫱*[n] f = ⫱*[↑n] f. +lemma gr_tls_succ (n) (f): ⫰⫰*[n] f = ⫰*[↑n] f. /2 width=1 by stream_tls_succ/ qed. (*** tls_xn *) -lemma gr_tls_swap (n) (f): ⫱*[n] ⫱f = ⫱*[↑n] f. +lemma gr_tls_swap (n) (f): ⫰*[n] ⫰f = ⫰*[↑n] f. // qed.