matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_update.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/substitution/lift_eq.ma".
  16 include "delayed_updating/syntax/path_update.ma".
  17 include "delayed_updating/syntax/path_depth.ma".
  18 include "ground/lib/stream_eq_eq.ma".
  19
  20 (* LIFT FOR PATH ***********************************************************)
  21
  22 (* Constructions with update ***********************************************)
  23
  24 axiom arith1 (p,q:pnat) (n:nat):
  25       nrplus (pplus p q) n = pplus p (nrplus q n).
  26
  27 lemma pippo (f) (p) (m:pnat):
  28       ⇂*[ninj (m+⧣p)]f ≗ ⇂*[ninj (m+❘p❘)]↑[p]f.
  29 #f #p @(list_ind_rcons … p) -p [ // ]
  30 #p * [ #n ] #IH #m
  31 [ <update_d_dx <depth_d_dx
  32   <nplus_comm <nrplus_inj_sn <nrplus_inj_dx <arith1
  33   @(stream_eq_trans … (lift_rmap_tls_d_dx …))
  34   @(stream_eq_canc_dx … (IH …)) -IH //
  35 | //
  36 | <update_L_dx <depth_L_dx
  37   <nrplus_succ_dx >nsucc_inj //
  38 | //
  39 | //
  40 ]
  41 qed.