]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/basic_2/etc/cpue/cnu.etc
update in static_2 and basic_2 for the article
[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc / cpue / cnu.etc
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 include "basic_2/notation/relations/preditnormal_4.ma".
16 include "static_2/syntax/tueq.ma".
17 include "basic_2/rt_transition/cpm.ma".
18
19 (* NORMAL TERMS FOR T-UNUNBOUND RT-TRANSITION *******************************)
20
21 definition cnu (h) (G) (L): predicate term ≝
22            λT1. ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≅ T2.
23
24 interpretation
25    "normality for t-unbound context-sensitive parallel rt-transition (term)"
26    'PRedITNormal h G L T = (cnu h G L T).
27
28 (* Basic properties *********************************************************)
29
30 lemma cnu_sort (h) (G) (L): ∀s. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃⋆s⦄.
31 #h #G #L #s1 #n #X #H
32 elim (cpm_inv_sort1 … H) -H #H #_ destruct //
33 qed.
34
35 lemma cnu_ctop (h) (G): ∀i. ⦃G,⋆⦄ ⊢ ⥲[h] 𝐍⦃#i⦄.
36 #h #G * [| #i ] #n #X #H
37 [ elim (cpm_inv_zero1 … H) -H *
38   [ #H #_ destruct //
39   | #Y #X1 #X2 #_ #_ #H destruct
40   | #m #Y #X1 #X2 #_ #_ #H destruct
41   ]
42 | elim (cpm_inv_lref1 … H) -H *
43   [ #H #_ destruct //
44   | #Z #Y #X0 #_ #_ #H destruct
45   ]
46 ]
47 qed.
48
49 lemma cnu_zero (h) (G) (L): ∀I. ⦃G,L.ⓤ{I}⦄ ⊢ ⥲[h] 𝐍⦃#0⦄.
50 #h #G #L #I #n #X #H 
51 elim (cpm_inv_zero1 … H) -H *
52 [ #H #_ destruct //
53 | #Y #X1 #X2 #_ #_ #H destruct
54 | #m #Y #X1 #X2 #_ #_ #H destruct
55 ]
56 qed.
57
58 lemma cnu_gref (h) (G) (L): ∀l. ⦃G,L⦄ ⊢ ⥲[h] 𝐍⦃§l⦄.
59 #h #G #L #l1 #n #X #H
60 elim (cpm_inv_gref1 … H) -H #H #_ destruct //
61 qed.