X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Funwind3%2Funwind_structure_depth.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Funwind3%2Funwind_structure_depth.etc;h=fdb7d781be5ffdb610bdb88b4c83c7c4fa49f48b;hb=2c68dcfee2c3fe819c8f92a9609620a85909ce8a;hp=0000000000000000000000000000000000000000;hpb=eba13527cf74de399b7e5b958901962666d4cd25;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure_depth.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure_depth.etc new file mode 100644 index 000000000..fdb7d781b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind3/unwind_structure_depth.etc @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "delayed_updating/unwind3/unwind.ma". +include "delayed_updating/syntax/path_structure.ma". +include "delayed_updating/syntax/path_depth.ma". +include "ground/arith/nat_pred_succ.ma". + +(* UNWIND FOR PATH *********************************************************) + +(* Basic constructions with structure and depth ****************************) + +lemma unwind_rmap_structure (p) (f): + (⫯*[❘p❘]f) = ▼[⊗p]f. +#p elim p -p // +* [ #n ] #p #IH #f // +[