matita/matita/contribs/lambda_delta/basic_2/unfold/ltpsss_tps.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 "basic_2/unfold/ltpss_tps.ma".
  16 include "basic_2/unfold/ltpsss.ma".
  17
  18 (* ITERATED PARTIAL UNFOLD ON LOCAL ENVIRONMENTS ****************************)
  19
  20 (* Properties concerning partial substitution on terms **********************)
  21
  22 lemma ltpsss_tps_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ▶** L0 →
  23                            ∀T2,U2,d2,e2. L0 ⊢ T2 [d2, e2] ▶ U2 →
  24                            d1 + e1 ≤ d2 → L1 ⊢ T2 [d2, e2] ▶ U2.
  25 #L1 #L0 #d1 #e1 #H @(ltpsss_ind … H) -L0 //
  26 #L #L0 #_ #HL0 #IHL #T2 #U2 #d2 #e2 #HTU2 #Hde1d2
  27 lapply (ltpss_tps_trans_ge … HTU2 … HL0 ?) -HL0 -HTU2 // /2 width=1/
  28 qed.
  29
  30 lemma ltpsss_tps_conf_ge: ∀L0,L1,T2,U2,d1,e1,d2,e2. d1 + e1 ≤ d2 →
  31                           L0 ⊢ T2 [d2, e2] ▶ U2 → L0 [d1, e1] ▶** L1 →
  32                           L1 ⊢ T2 [d2, e2] ▶ U2.
  33 #L0 #L1 #T2 #U2 #d1 #e1 #d2 #e2 #Hde1d2 #HTU2 #H @(ltpsss_ind … H) -L1 //
  34 -HTU2 #L #L1 #_ #HL1 #IHL
  35 lapply (ltpss_tps_conf_ge … IHL … HL1 ?) -HL1 -IHL //
  36 qed.