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-.