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/rt_transition/cpg_drops.ma".
16 include "basic_2/rt_transition/cpt.ma".
18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-TRANSITION FOR TERMS ****************)
20 (* Properties with generic slicing for local environments *******************)
22 lemma cpt_lifts_sn (h) (n) (G):
23 d_liftable2_sn … lifts (λL. cpt h G L n).
24 #h #n #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1
25 elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1
26 /3 width=5 by ex2_intro/
29 lemma cpt_lifts_bi (h) (n) (G):
30 d_liftable2_bi … lifts (λL. cpt h G L n).
31 #h #n #G #K #T1 #T2 * /3 width=11 by cpg_lifts_bi, ex2_intro/
34 (* Inversion lemmas with generic slicing for local environments *************)
36 lemma cpt_inv_lifts_sn (h) (n) (G):
37 d_deliftable2_sn … lifts (λL. cpt h G L n).
38 #h #n #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1
39 elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1
40 /3 width=5 by ex2_intro/
43 lemma cpt_inv_lifts_bi (h) (n) (G):
44 d_deliftable2_bi … lifts (λL. cpt h G L n).
45 #h #n #G #L #U1 #U2 * /3 width=11 by cpg_inv_lifts_bi, ex2_intro/