matita/matita/contribs/lambdadelta/delayed_updating/unwind1/unwind_depth.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "delayed_updating/unwind1/unwind.ma".
  16 include "delayed_updating/syntax/path_depth.ma".
  17 include "ground/relocation/tr_id_compose.ma".
  18 include "ground/relocation/tr_compose_compose.ma".
  19 include "ground/relocation/tr_compose_pn.ma".
  20 include "ground/relocation/tr_compose_eq.ma".
  21 include "ground/relocation/tr_pn_eq.ma".
  22 include "ground/lib/stream_eq_eq.ma".
  23
  24 (* UNWIND FOR PATH *********************************************************)
  25 (* COMMENT
  26 (* Constructions with depth ************************************************)
  27
  28 lemma unwind_rmap_decompose (p) (f):
  29       ▼[p]f ≗ (▼[p]𝐢)∘(⫯*[❘p❘]f).
  30 #p @(list_ind_rcons … p) -p
  31 [ #f <unwind_rmap_empty <unwind_rmap_empty <tr_pushs_zero //
  32 | #p * [ #n ] #IH #f //
  33   [ <unwind_rmap_d_dx <unwind_rmap_d_dx <depth_d_dx
  34     @(stream_eq_canc_dx … (tr_compose_assoc …))
  35     /2 width=1 by tr_compose_eq_repl/
  36   | <unwind_rmap_L_dx <unwind_rmap_L_dx <depth_L_dx
  37     <tr_pushs_succ <tr_compose_push_bi
  38     /2 width=1 by tr_push_eq_repl/
  39   ]
  40 ]
  41 qed.
  42
  43 lemma unwind_rmap_pap_le (f) (p) (n):
  44       n < ▼❘p❘ → (▼[p]𝐢)＠⧣❨n❩ = (▼[p]f)＠⧣❨n❩.
  45 #f #p #n #Hn
  46 >(tr_pap_eq_repl … (▼[p]f) … (unwind_rmap_decompose …))
  47 <tr_compose_pap <tr_pap_pushs_le //
  48 qed.
  49 *)