matita/matita/contribs/lambdadelta/delayed_updating/unwind/unwind1_rmap_tail.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/unwind/unwind1_rmap.ma".
  16 include "delayed_updating/syntax/path_tail_depth.ma".
  17 include "delayed_updating/syntax/path_height.ma".
  18
  19 (* BASIC UNWIND MAP FOR PATH ************************************************)
  20
  21 include "ground/relocation/tr_uni_pap.ma".
  22 include "ground/relocation/tr_compose_pap.ma".
  23 include "ground/relocation/tr_pap_pn.ma".
  24 include "ground/notation/functions/applysucc_2.ma".
  25 include "ground/arith/nat_plus_rplus.ma".
  26 include "ground/arith/nat_pred_succ.ma".
  27
  28 definition tr_nap (f) (l:nat): nat ≝
  29            ↓(f@❨↑l❩).
  30
  31 interpretation
  32   "functional non-negative application (total relocation maps)"
  33   'ApplySucc f l = (tr_nap f l).
  34
  35 lemma tr_nap_unfold (f) (l):
  36       ↓(f@❨↑l❩) = f@↑❨l❩.
  37 // qed.
  38
  39 lemma tr_compose_nap (f2) (f1) (l):
  40       f2@↑❨f1@↑❨l❩❩ = (f2∘f1)@↑❨l❩.
  41 #f2 #f1 #l
  42 <tr_nap_unfold <tr_nap_unfold <tr_nap_unfold
  43 <tr_compose_pap <npsucc_pred //
  44 qed.
  45
  46 lemma tr_uni_nap (n) (m):
  47       m + n = 𝐮❨n❩@↑❨m❩.
  48 #n #m
  49 <tr_nap_unfold
  50 <tr_uni_pap <nrplus_npsucc_sn //
  51 qed.
  52
  53 lemma tr_nap_push (f):
  54       ∀l. ↑(f@↑❨l❩) = (⫯f)@↑❨↑l❩.
  55 #f #l
  56 <tr_nap_unfold <tr_nap_unfold
  57 <tr_pap_push <pnpred_psucc //
  58 qed.
  59
  60 (****)
  61
  62 lemma unwind1_rmap_labels_L (n):
  63       (𝐢) = ▶(𝗟∗∗n).
  64 #n @(nat_ind_succ … n) -n //
  65 #n #IH
  66 <labels_succ <unwind1_rmap_L_sn //
  67 qed.
  68
  69 lemma unwind1_rmap_tail (p) (n):
  70       n + ♯(↳[n]p) = (▶↳[n]p)@↑❨n❩.
  71 #p elim p -p //
  72 #l #p #IH #n @(nat_ind_succ … n) -n //
  73 #n #_ cases l [ #m ]
  74 [ <unwind1_rmap_d_sn <tail_d_sn <height_d_sn
  75   <nplus_assoc >IH -IH <tr_compose_nap //
  76 | <unwind1_rmap_m_sn <tail_m_sn <height_m_sn //
  77 | <unwind1_rmap_L_sn <tail_L_sn <height_L_sn
  78   <tr_nap_push <npred_succ //
  79 | <unwind1_rmap_A_sn <tail_A_sn <height_A_sn //
  80 | <unwind1_rmap_S_sn <tail_S_sn <height_S_sn //
  81 ]
  82 qed.