X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_pushs_tls.ma;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground%2Frelocation%2Ftr_pushs_tls.ma;h=fab5dd3e93f863d2f87bca235adc59f03d580a1a;hb=b05a8a8b1cc518973c30fdbed6a47d7d3ea9d7f0;hp=0000000000000000000000000000000000000000;hpb=d108bcea8ebae11b03e8d8a155dfd3f2eb445127;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/tr_pushs_tls.ma b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pushs_tls.ma new file mode 100644 index 000000000..fab5dd3e9 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/relocation/tr_pushs_tls.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground/relocation/tr_pushs.ma". +include "ground/relocation/tr_pn_hdtl.ma". +include "ground/lib/stream_tls.ma". + +(* ITERATED PUSH FOR TOTAL RELOCATION MAPS **********************************) + +(* Constructions with stream_tls ********************************************) + +lemma tr_tls_pushs (f) (n): + f = ⇂*[n]⫯*[n]f. +#f #n @(nat_ind_succ … n) -n // +#n #IH +