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_transition/cnr_teqg.ma". (**) (* one dependence *)
17 (* NORMAL TERMS FOR CONTEXT-SENSITIVE R-TRANSITION **************************)
19 (* Properties with context-free sort-irrelevant equivalence for terms *******)
21 (* Basic_1: was: nf2_dec *)
22 (* Basic_2A1: uses: cnr_dec *)
23 lemma cnr_dec_teqx (h) (G) (L):
24 ∀T1. ∨∨ ❨G,L❩ ⊢ ➡𝐍[h,0] T1
25 | ∃∃T2. ❨G,L❩ ⊢ T1 ➡[h,0] T2 & (T1 ≅ T2 → ⊥).
26 /2 width=1 by cnr_dec_teqg/ qed-.