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_computation/cpms_aaa.ma".
16 include "basic_2/rt_equivalence/cpes.ma".
18 (* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-EQUIVALENCE FOR TERMS **************)
20 (* Properties with atomic arity assignment on terms *************************)
22 (* Basic_2A1: uses: scpes_refl *)
23 lemma cpes_refl_aaa (h) (n):
24 ∀G,L,T,A. ❨G,L❩ ⊢ T ⁝ A → ❨G,L❩ ⊢ T ⬌*[h,n,n] T.
26 elim (cpms_total_aaa h … n … HA) #U #HTU
27 /2 width=3 by cpms_div/
30 (* Main inversion lemmas with atomic arity assignment on terms **************)
32 (* Basic_2A1: uses: scpes_aaa_mono *)
33 theorem cpes_aaa_mono (h) (n1) (n2):
34 ∀G,L,T1,T2. ❨G,L❩ ⊢ T1 ⬌*[h,n1,n2] T2 →
35 ∀A1. ❨G,L❩ ⊢ T1 ⁝ A1 → ∀A2. ❨G,L❩ ⊢ T2 ⁝ A2 → A1 = A2.
36 #h #n1 #n2 #G #L #T1 #T2 * #T #HT1 #HT2 #A1 #HA1 #A2 #HA2
37 lapply (cpms_aaa_conf … HA1 … HT1) -T1 #HA1
38 lapply (cpms_aaa_conf … HA2 … HT2) -T2 #HA2
39 lapply (aaa_mono … HA1 … HA2) -L -T //