X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Funwind2%2Funwind_depth.etc;fp=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fdelayed_updating%2Fetc%2Funwind2%2Funwind_depth.etc;h=0000000000000000000000000000000000000000;hb=084fe5719d41ce13be068050fbade488d4a183ee;hp=8715fb514e8de0ce1f23966b39f204d469c350b1;hpb=61bc42e04598a9f5e489c3867af72e700c7fda04;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_depth.etc b/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_depth.etc
deleted file mode 100644
index 8715fb514..000000000
--- a/matita/matita/contribs/lambdadelta/delayed_updating/etc/unwind2/unwind_depth.etc
+++ /dev/null
@@ -1,48 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||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/unwind2/unwind.ma".
-include "delayed_updating/syntax/path_depth.ma".
-include "ground/relocation/tr_id_compose.ma".
-include "ground/relocation/tr_compose_compose.ma".
-include "ground/relocation/tr_compose_pn.ma".
-include "ground/relocation/tr_compose_eq.ma".
-include "ground/relocation/tr_pn_eq.ma".
-include "ground/lib/stream_eq_eq.ma".
-
-(* UNWIND FOR PATH **********************************************************)
-
-(* Constructions with depth *************************************************)
-
-lemma unwind_rmap_decompose (p) (f):
-      ▼[p]f ≗ (⫯*[❘p❘]f)∘(▼[p]𝐢).
-#p @(list_ind_rcons … p) -p
-[ #f <unwind_rmap_empty <unwind_rmap_empty <tr_pushs_zero //
-| #p * [ #n ] #IH #f //
-  [ <unwind_rmap_d_dx <unwind_rmap_d_dx <depth_d_dx
-    @(stream_eq_trans … (tr_compose_assoc …))
-    /2 width=1 by tr_compose_eq_repl/
-  | <unwind_rmap_L_dx <unwind_rmap_L_dx <depth_L_dx
-    <tr_pushs_succ <tr_compose_push_bi
-    /2 width=1 by tr_push_eq_repl/
-  ]
-]
-qed.
-
-lemma unwind_rmap_pap_le (f) (p) (n):
-      (▼[p]𝐢)@❨n❩ < ↑❘p❘ → (▼[p]𝐢)@❨n❩ = (▼[p]f)@❨n❩.
-#f #p #n #Hn
->(tr_pap_eq_repl … (▼[p]f) … (unwind_rmap_decompose …))
-<tr_compose_pap @tr_pap_pushs_le //
-qed.