]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/rt_equivalence/cpcs_cpcs.ma
milestone in basic_2
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_equivalence / cpcs_cpcs.ma
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/rt_equivalence/cpcs_lprs.ma".
16
17 (* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
18
19 (* Main properties **********************************************************)
20
21 (* Basic_1: was pc3_t *)
22 theorem cpcs_trans (h) (G) (L): Transitive … (cpcs h G L).
23 #h #G #L #T1 #T #HT1 #T2 @(trans_TC … HT1)
24 qed-.
25
26 theorem cpcs_canc_sn (h) (G) (L): left_cancellable … (cpcs h G L).
27 /3 width=3 by cpcs_trans, cpcs_sym/ qed-.
28
29 theorem cpcs_canc_dx (h) (G) (L): right_cancellable … (cpcs h G L).
30 /3 width=3 by cpcs_trans, cpcs_sym/ qed-.
31
32 (* Advanced properties ******************************************************)
33
34 lemma cpcs_bind1 (h) (G) (L): ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬌*[h] V2 →
35                               ∀I,T1,T2. ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬌*[h] T2 →
36                               ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬌*[h] ⓑ{p,I}V2.T2.
37 /3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed.
38
39 lemma cpcs_bind2 (h) (G) (L): ∀V1,V2. ⦃G, L⦄ ⊢ V1 ⬌*[h] V2 →
40                               ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬌*[h] T2 →
41                               ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬌*[h] ⓑ{p,I}V2.T2.
42 /3 width=3 by cpcs_trans, cpcs_bind_sn, cpcs_bind_dx/ qed.
43
44 (* Advanced properties with r-transition for full local environments ********)
45
46 (* Basic_1: was: pc3_wcpr0 *)
47 lemma lpr_cpcs_conf (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ➡[h] L2 →
48                              ∀T1,T2. ⦃G, L1⦄ ⊢ T1 ⬌*[h] T2 → ⦃G, L2⦄ ⊢ T1 ⬌*[h] T2.
49 #h #G #L1 #L2 #HL12 #T1 #T2 #H elim (cpcs_inv_cprs … H) -H
50 /3 width=5 by cpcs_canc_dx, lpr_cprs_conf/
51 qed-.