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".
16 include "Basic_2/reducibility/cpr_lift.ma".
17 include "Basic_2/reducibility/lcpr_cpr.ma".
18 include "Basic_2/computation/cprs_cprs.ma".
20 (* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
22 (* Forward lemmas involving same top term constructor ***********************)
24 lemma cpr_fwd_theta: ∀L,V1,V,T,U. L ⊢ ⓐV1. ⓓV. T ➡ U →
25 ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓV. T ≃ U ∨
27 #L #V1 #V #T #U #H #V2 #HV12
28 elim (cpr_inv_appl1 … H) -H *
29 [ -HV12 #V0 #X #_ #_ #H destruct /2 width=1/
30 | -HV12 #V0 #W #T1 #T2 #_ #_ #H destruct
31 | #V0 #V3 #W1 #W2 #T1 #T2 #HV10 #HW12 #HT12 #HV03 #H1 #H2 destruct
32 lapply (cpr_lift (L.ⓓW1) … HV12 … HV03 … HV10) -V0 -HV12 /2 width=1/ #HV23
33 lapply (lcpr_cpr_trans (L. ⓓW1) … HT12) -HT12 /2 width=1/ #HT12