(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
definition IH_cnv_cpm_teqx_cpm_trans (h) (a): relation3 genv lenv term ≝
- λG,L,T1. â\9dªG,Lâ\9d« ⊢ T1 ![h,a] →
- â\88\80n1,T. â\9dªG,Lâ\9d« ⊢ T1 ➡[h,n1] T → T1 ≅ T →
- â\88\80n2,T2. â\9dªG,Lâ\9d« ⊢ T ➡[h,n2] T2 →
- â\88\83â\88\83T0. â\9dªG,Lâ\9d« â\8a¢ T1 â\9e¡[h,n2] T0 & â\9dªG,Lâ\9d« ⊢ T0 ➡[h,n1] T2 & T0 ≅ T2.
+ λG,L,T1. â\9d¨G,Lâ\9d© ⊢ T1 ![h,a] →
+ â\88\80n1,T. â\9d¨G,Lâ\9d© ⊢ T1 ➡[h,n1] T → T1 ≅ T →
+ â\88\80n2,T2. â\9d¨G,Lâ\9d© ⊢ T ➡[h,n2] T2 →
+ â\88\83â\88\83T0. â\9d¨G,Lâ\9d© â\8a¢ T1 â\9e¡[h,n2] T0 & â\9d¨G,Lâ\9d© ⊢ T0 ➡[h,n1] T2 & T0 ≅ T2.
(* Transitive properties restricted rt-transition for terms *****************)
fact cnv_cpm_teqx_cpm_trans_sub (h) (a) (G0) (L0) (T0):
- (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« > â\9dªG,L,Tâ\9d« → IH_cnv_cpm_trans_lpr h a G L T) →
- (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« â¬\82+ â\9dªG,L,Tâ\9d« → IH_cnv_cpm_teqx_cpm_trans h a G L T) →
+ (â\88\80G,L,T. â\9d¨G0,L0,T0â\9d© > â\9d¨G,L,Tâ\9d© → IH_cnv_cpm_trans_lpr h a G L T) →
+ (â\88\80G,L,T. â\9d¨G0,L0,T0â\9d© â¬\82+ â\9d¨G,L,Tâ\9d© → IH_cnv_cpm_teqx_cpm_trans h a G L T) →
∀G,L,T1. G0 = G → L0 = L → T0 = T1 → IH_cnv_cpm_teqx_cpm_trans h a G L T1.
#h #a #G0 #L0 #T0 #IH2 #IH1 #G #L * [| * [| * ]]
[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct -G0 -L0 -T0
qed-.
fact cnv_cpm_teqx_cpm_trans_aux (h) (a) (G0) (L0) (T0):
- (â\88\80G,L,T. â\9dªG0,L0,T0â\9d« > â\9dªG,L,Tâ\9d« → IH_cnv_cpm_trans_lpr h a G L T) →
+ (â\88\80G,L,T. â\9d¨G0,L0,T0â\9d© > â\9d¨G,L,Tâ\9d© → IH_cnv_cpm_trans_lpr h a G L T) →
IH_cnv_cpm_teqx_cpm_trans h a G0 L0 T0.
#h #a #G0 #L0 #T0
@(fqup_wf_ind (Ⓣ) … G0 L0 T0) -G0 -L0 -T0 #G0 #L0 #T0 #IH #IH0