(* *)
(**************************************************************************)
-include "basic_2/notation/relations/normal_5.ma".
+include "basic_2/notation/relations/prednormal_5.ma".
include "basic_2/reduction/cnr.ma".
include "basic_2/reduction/cpx.ma".
-(* CONTEXT-SENSITIVE EXTENDED NORMAL TERMS **********************************)
+(* NORMAL TERMS FOR CONTEXT-SENSITIVE EXTENDED REDUCTION ********************)
definition cnx: ∀h. sd h → relation3 genv lenv term ≝
λh,g,G,L. NF … (cpx h g G L) (eq …).
interpretation
- "context-sensitive extended normality (term)"
- 'Normal h g L T = (cnx h g L T).
+ "normality for context-sensitive extended reduction (term)"
+ 'PRedNormal h g L T = (cnx h g L T).
(* Basic inversion lemmas ***************************************************)
lemma cnx_inv_sort: ∀h,g,G,L,k. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃⋆k⦄ → deg h g k 0.
#h #g #G #L #k #H elim (deg_total h g k)
#l @(nat_ind_plus … l) -l // #l #_ #Hkl
-lapply (H (⋆(next h k)) ?) -H /2 width=2 by cpx_sort/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
+lapply (H (⋆(next h k)) ?) -H /2 width=2 by cpx_st/ -L -l #H destruct -H -e0 (**) (* destruct does not remove some premises *)
lapply (next_lt h k) >e1 -e1 #H elim (lt_refl_false … H)
qed-.
]
qed-.
-lemma cnx_inv_tau: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓝV.T⦄ → ⊥.
+lemma cnx_inv_eps: ∀h,g,G,L,V,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃ⓝV.T⦄ → ⊥.
#h #g #G #L #V #T #H lapply (H T ?) -H
-/2 width=4 by cpx_tau, discr_tpair_xy_y/
+/2 width=4 by cpx_eps, discr_tpair_xy_y/
qed-.
(* Basic forward lemmas *****************************************************)