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/grammar/tstc.ma".
17 include "basic_2/reducibility/cpr_lift.ma".
18 include "basic_2/reducibility/lcpr_cpr.ma".
20 include "basic_2/computation/cprs_cprs.ma".
22 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
24 (* Forward lemmas involving same top term constructor ***********************)
26 lemma cpr_fwd_beta: ∀L,V,W,T,U. L ⊢ ⓐV. ⓛW. T ➡ U →
27 ⓐV. ⓛW. T ≃ U ∨ L ⊢ ⓓV. T ➡* U.
29 elim (cpr_inv_appl1 … H) -H *
30 [ #V0 #X #_ #_ #H destruct /2 width=1/
31 | #V0 #W0 #T1 #T2 #HV0 #HT12 #H1 #H2 destruct
32 lapply (lcpr_cpr_trans (L. ⓓV) … HT12) -HT12 /2 width=1/ /3 width=1/
33 | #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #H destruct
37 lemma cpr_fwd_theta: ∀L,V1,V,T,U. L ⊢ ⓐV1. ⓓV. T ➡ U →
38 ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓV. T ≃ U ∨
40 #L #V1 #V #T #U #H #V2 #HV12
41 elim (cpr_inv_appl1 … H) -H *
42 [ -HV12 #V0 #X #_ #_ #H destruct /2 width=1/
43 | -HV12 #V0 #W #T1 #T2 #_ #_ #H destruct
44 | #V0 #V3 #W1 #W2 #T1 #T2 #HV10 #HW12 #HT12 #HV03 #H1 #H2 destruct
45 lapply (cpr_lift (L.ⓓW1) … HV12 … HV03 … HV10) -V0 -HV12 /2 width=1/ #HV23
46 lapply (lcpr_cpr_trans (L. ⓓW1) … HT12) -HT12 /2 width=1/ #HT12
51 lemma cprs_fwd_tau: ∀L,W,T,U. L ⊢ ⓣW. T ➡* U →
52 ⓣW. T ≃ U ∨ L ⊢ T ➡* U.
54 elim (cprs_inv_cast1 … H) -H /2 width=1/ *
55 #W0 #T0 #_ #_ #H destruct /2 width=1/