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 "static_2/static/aaa.ma".
16 include "basic_2/rt_computation/cpts_drops.ma".
18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL T-COMPUTATION FOR TERMS ***************)
20 (* Properties with atomic arity assignment for terms ************************)
22 lemma cpts_total_aaa (h) (G) (L) (T1):
23 ∀A. ❪G,L❫ ⊢ T1 ⁝ A → ∀n. ∃T2. ❪G,L❫ ⊢ T1 ⬆*[h,n] T2.
24 #h #G #L #T1 #A #H elim H -G -L -T1 -A
25 [ #G #L #s #n /3 width=2 by ex_intro/
26 | #I #G #K #V1 #B #_ #IH #n -B
28 [ elim (IH n) -IH #V2 #HV12
29 elim (lifts_total V2 (𝐔❨1❩)) #T2 #HVT2
30 /3 width=4 by cpts_delta, ex_intro/
32 [ /2 width=2 by ex_intro/
33 | #n elim (IH n) -IH #V2 #HV12
34 elim (lifts_total V2 (𝐔❨1❩)) #T2 #HVT2
35 /3 width=4 by cpts_ell, ex_intro/
38 | #I #G #K #A #i #_ #IH #n -A
39 elim (IH n) -IH #T #HT
40 elim (lifts_total T (𝐔❨1❩)) #U #HTU
41 /3 width=4 by cpts_lref, ex_intro/
42 | #p #G #L #V1 #T1 #B #A #_ #_ #IHV #IHT #n -B -A
43 elim (IHV 0) -IHV #V2 #HV12
44 elim (IHT n) -IHT #T2 #HT12
45 /3 width=3 by cpts_bind_dx, ex_intro/
46 | #p #G #L #V1 #T1 #B #A #_ #_ #IHV #IHT #n -B -A
47 elim (IHV 0) -IHV #V2 #HV12
48 elim (IHT n) -IHT #T2 #HT12
49 /3 width=3 by cpts_bind_dx, ex_intro/
50 | #G #L #V1 #T1 #B #A #_ #_ #IHV #IHT #n -B -A
51 elim (IHV 0) -IHV #V2 #HV12
52 elim (IHT n) -IHT #T2 #HT12
53 /3 width=3 by cpts_appl_dx, ex_intro/
54 | #G #L #U1 #T1 #A #_ #_ #IHU #_ #n -A
56 [ /2 width=2 by ex_intro/
57 | #n elim (IHU n) -IHU #U2 #HU12
58 /3 width=3 by cpts_ee, ex_intro/