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 "ground_2/lib/star.ma".
16 include "basic_2/notation/relations/pconvstar_5.ma".
17 include "basic_2/rt_conversion/cpc.ma".
19 (* CONTEXT-SENSITIVE PARALLEL R-EQUIVALENCE FOR TERMS ***********************)
21 definition cpcs (h) (G): relation3 lenv term term ≝
24 interpretation "context-sensitive parallel r-equivalence (term)"
25 'PConvStar h G L T1 T2 = (cpcs h G L T1 T2).
27 (* Basic eliminators ********************************************************)
29 (* Basic_2A1: was: cpcs_ind_dx *)
30 lemma cpcs_ind_sn (h) (G) (L) (T2):
31 ∀Q:predicate term. Q T2 →
32 (∀T1,T. ❪G,L❫ ⊢ T1 ⬌[h] T → ❪G,L❫ ⊢ T ⬌*[h] T2 → Q T → Q T1) →
33 ∀T1. ❪G,L❫ ⊢ T1 ⬌*[h] T2 → Q T1.
34 normalize /3 width=6 by TC_star_ind_dx/
37 (* Basic_2A1: was: cpcs_ind *)
38 lemma cpcs_ind_dx (h) (G) (L) (T1):
39 ∀Q:predicate term. Q T1 →
40 (∀T,T2. ❪G,L❫ ⊢ T1 ⬌*[h] T → ❪G,L❫ ⊢ T ⬌[h] T2 → Q T → Q T2) →
41 ∀T2. ❪G,L❫ ⊢ T1 ⬌*[h] T2 → Q T2.
42 normalize /3 width=6 by TC_star_ind/
45 (* Basic properties *********************************************************)
47 (* Basic_1: was: pc3_refl *)
48 lemma cpcs_refl (h) (G): c_reflexive … (cpcs h G).
49 /2 width=1 by inj/ qed.
51 (* Basic_1: was: pc3_s *)
52 lemma cpcs_sym (h) (G) (L): symmetric … (cpcs h G L).
53 #h #G #L @TC_symmetric
54 /2 width=1 by cpc_sym/
57 lemma cpc_cpcs (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T1 ⬌[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
58 /2 width=1 by inj/ qed.
60 (* Basic_2A1: was: cpcs_strap2 *)
61 lemma cpcs_step_sn (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌[h] T →
62 ∀T2. ❪G,L❫ ⊢ T ⬌*[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
63 normalize /2 width=3 by TC_strap/
66 (* Basic_2A1: was: cpcs_strap1 *)
67 lemma cpcs_step_dx (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌*[h] T →
68 ∀T2. ❪G,L❫ ⊢ T ⬌[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
69 normalize /2 width=3 by step/
72 (* Basic_1: was: pc3_pr2_r *)
73 lemma cpr_cpcs_dx (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T1 ➡[h,0] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
74 /3 width=1 by cpc_cpcs, or_introl/ qed.
76 (* Basic_1: was: pc3_pr2_x *)
77 lemma cpr_cpcs_sn (h) (G) (L): ∀T1,T2. ❪G,L❫ ⊢ T2 ➡[h,0] T1 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
78 /3 width=1 by cpc_cpcs, or_intror/ qed.
80 (* Basic_1: was: pc3_pr2_u *)
81 (* Basic_2A1: was: cpcs_cpr_strap2 *)
82 lemma cpcs_cpr_step_sn (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ➡[h,0] T → ∀T2. ❪G,L❫ ⊢ T ⬌*[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
83 /3 width=3 by cpcs_step_sn, or_introl/ qed-.
85 (* Basic_2A1: was: cpcs_cpr_strap1 *)
86 lemma cpcs_cpr_step_dx (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌*[h] T →
87 ∀T2. ❪G,L❫ ⊢ T ➡[h,0] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
88 /3 width=3 by cpcs_step_dx, or_introl/ qed-.
90 lemma cpcs_cpr_div (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ⬌*[h] T →
91 ∀T2. ❪G,L❫ ⊢ T2 ➡[h,0] T → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
92 /3 width=3 by cpcs_step_dx, or_intror/ qed-.
94 lemma cpr_div (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T1 ➡[h,0] T →
95 ∀T2. ❪G,L❫ ⊢ T2 ➡[h,0] T → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
96 /3 width=3 by cpr_cpcs_dx, cpcs_step_dx, or_intror/ qed-.
98 (* Basic_1: was: pc3_pr2_u2 *)
99 lemma cpcs_cpr_conf (h) (G) (L): ∀T1,T. ❪G,L❫ ⊢ T ➡[h,0] T1 →
100 ∀T2. ❪G,L❫ ⊢ T ⬌*[h] T2 → ❪G,L❫ ⊢ T1 ⬌*[h] T2.
101 /3 width=3 by cpcs_step_sn, or_intror/ qed-.
103 (* Basic_1: removed theorems 9:
104 clear_pc3_trans pc3_ind_left
105 pc3_head_1 pc3_head_2 pc3_head_12 pc3_head_21
106 pc3_pr2_fqubst0 pc3_pr2_fqubst0_back pc3_fqubst0
107 pc3_gen_abst pc3_gen_abst_shift
109 (* Basic_1: removed local theorems 6:
110 pc3_left_pr3 pc3_left_trans pc3_left_sym pc3_left_pc3 pc3_pc3_left