matita/matita/contribs/lambdadelta/basic_2/etc_new/cpy/cpy_nlift.etc

   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 "basic_2/substitution/lift_neg.ma".
  16 include "basic_2/substitution/lift_lift.ma".
  17 include "basic_2/substitution/cpy.ma".
  18
  19 (* CONTEXT-SENSITIVE EXTENDED ORDINARY SUBSTITUTION FOR TERMS ***************)
  20
  21 (* Inversion lemmas on negated relocation ***********************************)
  22
  23 lemma cpy_fwd_nlift2_ge: ∀G,L,U1,U2,l,m. ⦃G, L⦄ ⊢ U1 ▶[l, m] U2 →
  24                          ∀i. l ≤ i → (∀T2. ⬆[i, 1] T2 ≡ U2 → ⊥) →
  25                          (∀T1. ⬆[i, 1] T1 ≡ U1 → ⊥) ∨
  26                          ∃∃I,K,W,j. l ≤ yinj j & j < i & ⬇[j]L ≡ K.ⓑ{I}W &
  27                                     (∀V. ⬆[⫰(i-j), 1] V ≡ W → ⊥) & (∀T1. ⬆[j, 1] T1 ≡ U1 → ⊥).
  28 #G #L #U1 #U2 #l #m #H elim H -G -L -U1 -U2 -l -m
  29 [ /3 width=2 by or_introl/
  30 | #I #G #L #K #V #W #j #l #m #Hlj #Hjlm #HLK #HVW #i #Hli #HnW
  31   elim (ylt_split j i) #Hij
  32   [ @or_intror @(ex5_4_intro … HLK) // -HLK
  33     [ #X #HXV elim (lift_trans_le … HXV … HVW ?) -V // #Y #HXY
  34       <yminus_succ2 <yplus_inj >yplus_SO2 >ymax_pre_sn /2 width=2 by ylt_fwd_le_succ1/
  35     | -HnW /3 width=7 by lift_inv_lref2_be, ylt_inj/
  36     ]
  37   | elim (lift_split … HVW i j) -HVW //
  38     #X #_ #H elim HnW -HnW //
  39   ]
  40 | #a #I #G #L #W1 #W2 #U1 #U2 #l #m #_ #_ #IHW12 #IHU12 #i #Hli #H elim (nlift_inv_bind … H) -H
  41   [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
  42     [ /4 width=9 by nlift_bind_sn, or_introl/
  43     | * /5 width=9 by nlift_bind_sn, ex5_4_intro, or_intror/
  44     ]
  45   | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 /2 width=1 by yle_succ/
  46     [ /4 width=9 by nlift_bind_dx, or_introl/
  47     | * #J #K #W #j #Hlj elim (yle_inv_succ1 … Hlj) -Hlj #Hlj #Hj
  48       <Hj >yminus_succ #Hji #HLK #HnW
  49       lapply (drop_inv_drop1_lt … HLK ?) /2 width=1 by ylt_O/ -HLK #HLK
  50       <yminus_SO2 in Hlj; #Hlj #H4
  51       @or_intror @(ex5_4_intro … HLK) (**) (* explicit constructors *)
  52       /3 width=9 by nlift_bind_dx, ylt_pred, ylt_inj/
  53     ]
  54   ]
  55 | #I #G #L #W1 #W2 #U1 #U2 #l #m #_ #_ #IHW12 #IHU12 #i #Hli #H elim (nlift_inv_flat … H) -H
  56   [ #HnW2 elim (IHW12 … HnW2) -IHW12 -HnW2 -IHU12 //
  57     [ /4 width=9 by nlift_flat_sn, or_introl/
  58     | * /5 width=9 by nlift_flat_sn, ex5_4_intro, or_intror/
  59     ]
  60   | #HnU2 elim (IHU12 … HnU2) -IHU12 -HnU2 -IHW12 //
  61     [ /4 width=9 by nlift_flat_dx, or_introl/
  62     | * /5 width=9 by nlift_flat_dx, ex5_4_intro, or_intror/
  63   ]
  64 ]
  65 qed-.