matita/matita/contribs/lambdadelta/basic_2A/etc/lsubr/dxprs_lpss.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/sstas_lpss.ma".
  16 include "basic_2/computation/cprs_lpss.ma".
  17 include "basic_2/computation/dxprs.ma".
  18
  19 (* DECOMPOSED EXTENDED PARALLEL COMPUTATION ON TERMS ************************)
  20
  21 (* Properties about sn parallel substitution for local environments *********)
  22
  23 lemma dxprs_lpss_conf: ∀h,g,L1,T,U1. ⦃h, L1⦄ ⊢ T •*➡*[g] U1 → ∀L2. L1 ⊢ ▶* L2 →
  24                        ∃∃U2. ⦃h, L2⦄ ⊢ T •*➡*[g] U2 & L1 ⊢ U1 ▶* U2.
  25 #h #g #L1 #T #U1 * #U #HTU #HU1 #L2 #HL12
  26 elim (sstas_lpss_conf … HTU … HL12) -HTU #U0 #HTU0 #HU0
  27 elim (cprs_cpss_conf … HU1 … HU0) -U #U #HU1 #HU0
  28 elim (cprs_lpss_conf_sn … HU0 … HL12) -HU0 -HL12 #U2 #HU2 #HU02
  29 lapply (cpss_trans … HU1 … HU2) -U /3 width=3/
  30 qed-.
  31
  32 lemma dxprs_cpss_conf: ∀h,g,L,T1,U1. ⦃h, L⦄ ⊢ T1 •*➡*[g] U1 → ∀T2. L ⊢ T1 ▶* T2 →
  33                        ∃∃U2. ⦃h, L⦄ ⊢ T2 •*➡*[g] U2 & L ⊢ U1 ▶* U2.
  34 #h #g #L #T1 #U1 * #W1 #HTW1 #HWU1 #T2 #HT12
  35 elim (sstas_cpss_conf … HTW1 … HT12) -T1 #W2 #HTW2 #HW12
  36 elim (cprs_cpss_conf … HWU1 … HW12) -W1 /3 width=3/
  37 qed-.
  38
  39 lemma dxprs_cpss_lpss_conf: ∀h,g,L1,T1,U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 →
  40                             ∀T2. L1 ⊢ T1 ▶* T2 → ∀L2. L1 ⊢ ▶* L2 →
  41                             ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L1 ⊢ U1 ▶* U2.
  42 #h #g #L1 #T1 #U1 #HTU1 #T2 #HT12 #L2 #HL12
  43 elim (dxprs_cpss_conf … HTU1 … HT12) -T1 #U2 #HTU2 #HU12
  44 elim (dxprs_lpss_conf … HTU2 … HL12) -HTU2 -HL12 #U #HT2U #HU2
  45 lapply (cpss_trans … HU12 … HU2) -U2 /2 width=3/
  46 qed-.