matita/matita/contribs/lambdadelta/apps_2/functional/flifts_flifts_basic.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 "apps_2/functional/flifts_flifts.ma".
  16 include "apps_2/functional/flifts_basic.ma".
  17
  18 (* BASIC FUNCTIONAL RELOCATION **********************************************)
  19
  20 (* Main properties **********************************************************)
  21
  22 theorem flifts_basic_swap (T) (d1) (d2) (h1) (h2):
  23                           d2 ≤ d1 → ↑[d2,h2]↑[d1,h1]T = ↑[h2+d1,h1]↑[d2,h2]T.
  24 /3 width=1 by flifts_comp, basic_swap/ qed-.
  25 (*
  26 lemma flift_join: ∀e1,e2,T. ⬆[e1, e2] ↑[0, e1] T ≡ ↑[0, e1 + e2] T.
  27 #e1 #e2 #T
  28 lapply (flift_lift T 0 (e1+e2)) #H
  29 elim (lift_split … H e1 e1) -H // #U #H
  30 >(flift_inv_lift … H) -H //
  31 qed.
  32 *)