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/steps/rtc_ist_shift.ma".
16 include "ground_2/steps/rtc_ist_plus.ma".
17 include "ground_2/steps/rtc_ist_max.ma".
18 include "basic_2/notation/relations/pty_6.ma".
19 include "basic_2/rt_transition/cpg.ma".
21 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
23 definition cpt (h) (G) (L) (n): relation2 term term ≝
24 λT1,T2. ∃∃c. 𝐓⦃n,c⦄ & ⦃G,L⦄ ⊢ T1 ⬈[eq …,c,h] T2.
27 "t-bound context-sensitive parallel t-transition (term)"
28 'PTy h n G L T1 T2 = (cpt h G L n T1 T2).
30 (* Basic properties *********************************************************)
32 lemma cpt_ess (h) (G) (L):
33 ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,1] ⋆(⫯[h]s).
34 /2 width=3 by cpg_ess, ex2_intro/ qed.
36 lemma cpt_delta (h) (n) (G) (K):
37 ∀V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 →
38 ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓓV1⦄ ⊢ #0 ⬆[h,n] W2.
40 /3 width=5 by cpg_delta, ex2_intro/
43 lemma cpt_ell (h) (n) (G) (K):
44 ∀V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 →
45 ∀W2. ⇧*[1] V2 ≘ W2 → ⦃G,K.ⓛV1⦄ ⊢ #0 ⬆[h,↑n] W2.
47 /3 width=5 by cpg_ell, ex2_intro, ist_succ/
50 lemma cpt_lref (h) (n) (G) (K):
51 ∀T,i. ⦃G,K⦄ ⊢ #i ⬆[h,n] T → ∀U. ⇧*[1] T ≘ U →
52 ∀I. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬆[h,n] U.
54 /3 width=5 by cpg_lref, ex2_intro/
57 lemma cpt_bind (h) (n) (G) (L):
58 ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 → ∀I,T1,T2. ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2 →
59 ∀p. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆[h,n] ⓑ{p,I}V2.T2.
60 #h #n #G #L #V1 #V2 * #cV #HcV #HV12 #I #T1 #T2 *
61 /3 width=5 by cpg_bind, ist_max_O1, ex2_intro/
64 lemma cpt_appl (h) (n) (G) (L):
65 ∀V1,V2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 →
66 ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ ⓐV1.T1 ⬆[h,n] ⓐV2.T2.
67 #h #n #G #L #V1 #V2 * #cV #HcV #HV12 #T1 #T2 *
68 /3 width=5 by ist_max_O1, cpg_appl, ex2_intro/
71 lemma cpt_cast (h) (n) (G) (L):
72 ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆[h,n] U2 →
73 ∀T1,T2. ⦃G,L⦄ ⊢ T1 ⬆[h,n] T2 → ⦃G,L⦄ ⊢ ⓝU1.T1 ⬆[h,n] ⓝU2.T2.
74 #h #n #G #L #U1 #U2 * #cU #HcU #HU12 #T1 #T2 *
75 /3 width=6 by cpg_cast, ex2_intro/
78 lemma cpt_ee (h) (n) (G) (L):
79 ∀U1,U2. ⦃G,L⦄ ⊢ U1 ⬆[h,n] U2 → ∀T. ⦃G,L⦄ ⊢ ⓝU1.T ⬆[h,↑n] U2.
81 /3 width=3 by cpg_ee, ist_succ, ex2_intro/
84 (* Basic properties *********************************************************)
86 lemma cpt_refl (h) (G) (L): reflexive … (cpt h G L 0).
87 /3 width=3 by cpg_refl, ex2_intro/ qed.
89 (* Advanced properties ******************************************************)
91 lemma cpt_sort (h) (G) (L):
92 ∀n. n ≤ 1 → ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] ⋆((next h)^n s).
94 #n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/