1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "basic_2/substitution/lpss_cpss.ma".
16 include "basic_2/reduction/lpr_lpss.ma".
17 include "basic_2/computation/cprs.ma".
19 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
21 (* Properties on parallel substitution for terms ****************************)
23 (* Basic_1: was: pr3_subst1 *)
24 lemma cprs_cpss_conf: ∀L,T0,T1. L ⊢ T0 ➡* T1 → ∀T2. L ⊢ T0 ▶* T2 →
25 ∃∃T. L ⊢ T1 ▶* T & L ⊢ T2 ➡* T.
26 #L @TC_strip1 /2 width=3 by cpr_cpss_conf/ qed-. (**) (* auto /3 width=3/ fails because a δ-expansion gets in the way *)
28 (* Properties on sn parallel substitution for local environments ************)
30 lemma cprs_lpss_conf_dx: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ▶* L1 →
31 ∃∃T. L1 ⊢ T1 ▶* T & L1 ⊢ T0 ➡* T.
32 #L0 #T0 #T1 #H elim H -T1
34 elim (cpr_lpss_conf_dx … HT01 … HL01) -L0 /3 width=3/
35 | #T #T1 #_ #HT1 #IHT0 #L1 #HL01
36 elim (IHT0 … HL01) #T2 #HT2 #HT02
37 elim (cpr_lpss_conf_dx … HT1 … HL01) -L0 #T3 #HT13 #HT3
38 elim (cpr_cpss_conf … HT3 … HT2) -T #T #HT3 #HT2
39 lapply (cpss_trans … HT13 … HT3) -T3
40 lapply (cprs_strap1 … HT02 … HT2) -T2 /2 width=3/
44 lemma cprs_lpss_conf_sn: ∀L0,T0,T1. L0 ⊢ T0 ➡* T1 → ∀L1. L0 ⊢ ▶* L1 →
45 ∃∃T. L0 ⊢ T1 ▶* T & L1 ⊢ T0 ➡* T.
46 #L0 #T0 #T1 #HT01 #L1 #HL01
47 elim (cprs_lpss_conf_dx … HT01 … HL01) -HT01 #T #HT1
48 lapply (lpss_cpss_trans … HL01 … HT1) -HT1 /2 width=3/