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/reducibility/cpr.ma".
17 (* CONTEXT-SENSITIVE NORMAL TERMS *******************************************)
19 definition cnf: lenv → predicate term ≝ λL. NF … (cpr L) (eq …).
22 "context-sensitive normality (term)"
23 'Normal L T = (cnf L T).
25 (* Basic properties *********************************************************)
27 (* Basic_1: was: nf2_sort *)
28 lemma cnf_sort: ∀L,k. L ⊢ 𝐍[⋆k].
30 >(cpr_inv_sort1 … H) //
33 (* Basic_1: was: nf2_dec *)
34 axiom cnf_dec: ∀L,T1. L ⊢ 𝐍[T1] ∨
35 ∃∃T2. L ⊢ T1 ➡ T2 & (T1 = T2 → ⊥).
37 (* Basic_1: removed theorems 1: nf2_abst_shift *)