(**************************************************************************)
include "basic_2/notation/relations/preditnormal_4.ma".
(**************************************************************************)
include "basic_2/notation/relations/preditnormal_4.ma".
include "basic_2/rt_computation/cpms.ma".
(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
definition cnuw (h) (G) (L): predicate term ≝
include "basic_2/rt_computation/cpms.ma".
(* NORMAL TERMS FOR T-UNUNBOUND WHD RT-TRANSITION ***************************)
definition cnuw (h) (G) (L): predicate term ≝
- λT1. â\88\80n,T2. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡*[h,n] T2 â\86\92 T1 â\89\85 T2.
+ λT1. â\88\80n,T2. â\9d¨G,Lâ\9d© â\8a¢ T1 â\9e¡*[h,n] T2 â\86\92 T1 â\89\83 T2.
#h #G #L #l1 #n #X #H
elim (cpms_inv_gref1 … H) -H #H #_ destruct //
qed.
(* Basic_inversion lemmas ***************************************************)
#h #G #L #l1 #n #X #H
elim (cpms_inv_gref1 … H) -H #H #_ destruct //
qed.
(* Basic_inversion lemmas ***************************************************)
#h * #G #L #V #H
elim (lifts_total V (𝐔❨1❩)) #W #HVW
[ lapply (H 0 W ?) [ /3 width=3 by cpm_cpms, cpm_delta/ ]
| lapply (H 1 W ?) [ /3 width=3 by cpm_cpms, cpm_ell/ ]
] -H #HW
#h * #G #L #V #H
elim (lifts_total V (𝐔❨1❩)) #W #HVW
[ lapply (H 0 W ?) [ /3 width=3 by cpm_cpms, cpm_delta/ ]
| lapply (H 1 W ?) [ /3 width=3 by cpm_cpms, cpm_ell/ ]
] -H #HW
qed-.
(* Basic forward lemmas *****************************************************)
lemma cnuw_fwd_appl (h) (G) (L):
qed-.
(* Basic forward lemmas *****************************************************)
lemma cnuw_fwd_appl (h) (G) (L):
- â\88\80V,T. â\9dªG,Lâ\9d« â\8a¢ â\9e¡ð\9d\90\8dð\9d\90\96*[h] â\93\90V.T â\86\92 â\9dªG,Lâ\9d« ⊢ ➡𝐍𝐖*[h] T.
+ â\88\80V,T. â\9d¨G,Lâ\9d© â\8a¢ â\9e¡ð\9d\90\8dð\9d\90\96*[h] â\93\90V.T â\86\92 â\9d¨G,Lâ\9d© ⊢ ➡𝐍𝐖*[h] T.