matita/matita/contribs/lambdadelta/basic_2A/etc/cpr/ltpss_sn_tps.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/unfold/ltpss_sn_ldrop.ma".
  16
  17 (* SN PARALLEL UNFOLD ON LOCAL ENVIRONMENTS *********************************)
  18
  19 (* Properties concerning partial substitution on terms **********************)
  20
  21 lemma ltpss_sn_tps_conf_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
  22                             ∀L1,d1,e1. L0 ⊢ ▶* [d1, e1] L1 → d1 + e1 ≤ d2 →
  23                             L1 ⊢ T2 ▶ [d2, e2] U2.
  24 #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
  25 [ //
  26 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL01 #Hde1d2
  27   lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
  28   lapply (ltpss_sn_ldrop_conf_ge … HL01 … HLK0 ?) -L0 // /2 width=4/
  29 | #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL01 #Hde1d2
  30   @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_sn_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
  31 | /3 width=4/
  32 ]
  33 qed.
  34
  35 lemma ltpss_sn_tps_trans_ge: ∀L0,T2,U2,d2,e2. L0 ⊢ T2 ▶ [d2, e2] U2 →
  36                              ∀L1,d1,e1. L1 ⊢ ▶* [d1, e1] L0 → d1 + e1 ≤ d2 →
  37                              L1 ⊢ T2 ▶ [d2, e2] U2.
  38 #L0 #T2 #U2 #d2 #e2 #H elim H -L0 -T2 -U2 -d2 -e2
  39 [ //
  40 | #L0 #K0 #V0 #W0 #i2 #d2 #e2 #Hdi2 #Hide2 #HLK0 #HVW0 #L1 #d1 #e1 #HL10 #Hde1d2
  41   lapply (transitive_le … Hde1d2 Hdi2) -Hde1d2 #Hde1i2
  42   lapply (ltpss_sn_ldrop_trans_ge … HL10 … HLK0 ?) -L0 // /2 width=4/
  43 | #L0 #a #I #V2 #W2 #T2 #U2 #d2 #e2 #_ #_ #IHVW2 #IHTU2 #L1 #d1 #e1 #HL10 #Hde1d2
  44   @tps_bind [ /2 width=4/ | @IHTU2 -IHTU2 -IHVW2 [3: /2 by ltpss_sn_tpss1/ |1,2: skip | /2 width=1/ ] ] (**) (* explicit constructor *)
  45 | /3 width=4/
  46 ]
  47 qed.