matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt_cpt.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/rt_transition/cpt_drops.ma".
  16 include "basic_2/rt_transition/cpt_fqu.ma".
  17
  18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
  19
  20 (* Main properties **********************************************************)
  21
  22 theorem cpt_n_O_trans (h) (n) (G) (L) (T0):
  23         ∀T1. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T0 →
  24         ∀T2. ⦃G,L⦄ ⊢ T0 ⬆[h,0] T2 → ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2.
  25 #h #n #G #L #T0 #T1 #H
  26 @(cpt_ind … H) -H
  27 [ #I #G #L #X2 #HX2 //
  28 | #G #L #s #X2 #HX2
  29   elim (cpt_inv_sort_sn_iter … HX2) -HX2 #H #_ destruct //
  30 | #n #G #K #V1 #V0 #W0 #_ #IH #HVW0 #W2 #HW02
  31   elim (cpt_inv_lifts_sn … HW02 (Ⓣ) … K … HVW0) -W0
  32   [| /3 width=1 by drops_refl, drops_drop/ ] #V2 #HVW2 #HV02
  33   /3 width=3 by cpt_delta/
  34 | #n #G #K #W1 #W0 #V0 #_ #IH #HWV0 #V2 #HV02
  35   elim (cpt_inv_lifts_sn … HV02 (Ⓣ) … K … HWV0) -V0
  36   [| /3 width=1 by drops_refl, drops_drop/ ] #W2 #HWV2 #HW02
  37   /3 width=3 by cpt_ell/
  38 | #n #I #G #K #T0 #U0 #i #_ #IH #HTU0 #U2 #HU02
  39   elim (cpt_inv_lifts_sn … HU02 (Ⓣ) … K … HTU0) -U0
  40   [| /3 width=1 by drops_refl, drops_drop/ ] #T2 #HTU2 #HT02
  41   /3 width=3 by cpt_lref/
  42 | #n #p #I #G #L #V1 #V0 #T1 #T0 #_ #_ #IHV #IHT #X2 #HX2
  43   elim (cpt_inv_bind_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
  44   @cpt_bind
  45   [ /2 width=1 by/
  46   | @IHT
  47   ]
  48 | #n #G #L #V1 #V0 #T1 #T0 #_ #_ #IHV #IHT #X2 #HX2
  49   elim (cpt_inv_appl_sn … HX2) -HX2 #V2 #T2 #HV02 #HT02 #H destruct
  50   /3 width=1 by cpt_appl/
  51 | #n #G #L #V1 #V0 #T1 #T0 #_ #_ #IHV #IHT #X2 #HX2
  52   elim (cpt_inv_cast_sn … HX2) -HX2 *
  53   [ #V2 #T2 #HV02 #HT02 #H destruct /3 width=1 by cpt_cast/
  54   | #m #_ #H destruct
  55   ]
  56 | #n #G #L #V1 #V0 #T1 #_ #IH #V2 #HV02
  57   /3 width=1 by cpt_ee/
  58 ]
  59
  60
  61
  62