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/computation/cprs_cprs.ma".
16 include "basic_2/computation/cpre.ma".
18 (* CONTEXT-SENSITIVE PARALLEL EVALUATION ON TERMS **************************)
20 (* Main properties *********************************************************)
22 (* Basic_1: was: nf2_pr3_confluence *)
23 theorem cpre_mono: ∀G,L,T,T1. ⦃G, L⦄ ⊢ T ➡* 𝐍⦃T1⦄ → ∀T2. ⦃G, L⦄ ⊢ T ➡* 𝐍⦃T2⦄ → T1 = T2.
24 #G #L #T #T1 * #H1T1 #H2T1 #T2 * #H1T2 #H2T2
25 elim (cprs_conf … H1T1 … H1T2) -T #T #HT1
26 >(cprs_inv_cnr1 … HT1 H2T1) -T1 #HT2
27 >(cprs_inv_cnr1 … HT2 H2T2) -T2 //