include "basic_2/rt_computation/cpms_cpms.ma".
include "basic_2/rt_equivalence/cpes.ma".
-include "basic_2/dynamic/cnv_aaa.ma".
+include "basic_2/dynamic/cnv.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
(* Properties with t-bound rt-equivalence for terms *************************)
-lemma cnv_appl_cpes (a) (h) (G) (L):
- ∀n. (a = Ⓣ → n ≤ 1) →
- â\88\80V. â¦\83G, Lâ¦\84 â\8a¢ V ![a, h] â\86\92 â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ T ![a, h] →
- â\88\80W. â¦\83G, Lâ¦\84 ⊢ V ⬌*[h,1,0] W →
- â\88\80p,U. â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡*[n, h] â\93\9b{p}W.U â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\93\90V.T ![a, h].
-#a #h #G #L #n #Hn #V #HV #T #HT #W *
+lemma cnv_appl_cpes (h) (a) (G) (L):
+ ∀n. ad a n →
+ â\88\80V. â\9dªG,Lâ\9d« â\8a¢ V ![h,a] â\86\92 â\88\80T. â\9dªG,Lâ\9d« â\8a¢ T ![h,a] →
+ â\88\80W. â\9dªG,Lâ\9d« ⊢ V ⬌*[h,1,0] W →
+ â\88\80p,U. â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] â\93\9b[p]W.U â\86\92 â\9dªG,Lâ\9d« â\8a¢ â\93\90V.T ![h,a].
+#h #a #G #L #n #Hn #V #HV #T #HT #W *
/4 width=11 by cnv_appl, cpms_cprs_trans, cpms_bind/
qed.
-lemma cnv_cast_cpes (a) (h) (G) (L):
- â\88\80U. â¦\83G, Lâ¦\84 â\8a¢ U ![a, h] →
- â\88\80T. â¦\83G, Lâ¦\84 â\8a¢ T ![a, h] â\86\92 â¦\83G, Lâ¦\84 â\8a¢ U â¬\8c*[h,0,1] T â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\93\9dU.T ![a, h].
-#a #h #G #L #U #HU #T #HT * /2 width=3 by cnv_cast/
+lemma cnv_cast_cpes (h) (a) (G) (L):
+ â\88\80U. â\9dªG,Lâ\9d« â\8a¢ U ![h,a] →
+ â\88\80T. â\9dªG,Lâ\9d« â\8a¢ T ![h,a] â\86\92 â\9dªG,Lâ\9d« â\8a¢ U â¬\8c*[h,0,1] T â\86\92 â\9dªG,Lâ\9d« â\8a¢ â\93\9dU.T ![h,a].
+#h #a #G #L #U #HU #T #HT * /2 width=3 by cnv_cast/
qed.
(* Inversion lemmas with t-bound rt-equivalence for terms *******************)
-lemma cnv_inv_appl_cpes (a) (h) (G) (L):
- â\88\80V,T. â¦\83G, Lâ¦\84 â\8a¢ â\93\90V.T ![a, h] →
- ∃∃n,p,W,U. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
- â¦\83G, Lâ¦\84 â\8a¢ V â¬\8c*[h,1,0] W & â¦\83G, Lâ¦\84 â\8a¢ T â\9e¡*[n, h] â\93\9b{p}W.U.
-#a #h #G #L #V #T #H
+lemma cnv_inv_appl_cpes (h) (a) (G) (L):
+ â\88\80V,T. â\9dªG,Lâ\9d« â\8a¢ â\93\90V.T ![h,a] →
+ ∃∃n,p,W,U. ad a n & ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
+ â\9dªG,Lâ\9d« â\8a¢ V â¬\8c*[h,1,0] W & â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] â\93\9b[p]W.U.
+#h #a #G #L #V #T #H
elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
/3 width=7 by cpms_div, ex5_4_intro/
qed-.
-lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L):
- ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
- ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
- ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
-#a #h #G #L #V #T #H
-elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
-/3 width=7 by cpms_div, ex5_4_intro/
-qed-.
-
-lemma cnv_inv_appl_true_cpes (h) (G) (L):
- ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h] →
- ∃∃p,W,U. ⦃G,L⦄ ⊢ V ![h] & ⦃G,L⦄ ⊢ T ![h] &
- ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[1,h] ⓛ{p}W.U.
-#h #G #L #V #T #H
-elim (cnv_inv_appl_SO_cpes … H) -H #n #p #W #U #Hn
->Hn -n [| // ] #HV #HT #HVW #HTU
-/2 width=5 by ex4_3_intro/
-qed-.
-
-lemma cnv_inv_cast_cpes (a) (h) (G) (L):
- ∀U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] →
- ∧∧ ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T.
-#a #h #G #L #U #T #H
+lemma cnv_inv_cast_cpes (h) (a) (G) (L):
+ ∀U,T. ❪G,L❫ ⊢ ⓝU.T ![h,a] →
+ ∧∧ ❪G,L❫ ⊢ U ![h,a] & ❪G,L❫ ⊢ T ![h,a] & ❪G,L❫ ⊢ U ⬌*[h,0,1] T.
+#h #a #G #L #U #T #H
elim (cnv_inv_cast … H) -H
/3 width=3 by cpms_div, and3_intro/
qed-.
(* Eliminators with t-bound rt-equivalence for terms ************************)
-lemma cnv_ind_cpes (a) (h) (Q:relation3 genv lenv term):
+lemma cnv_ind_cpes (h) (a) (Q:relation3 genv lenv term):
(∀G,L,s. Q G L (⋆s)) →
- (â\88\80I,G,K,V. â¦\83G,Kâ¦\84 â\8a¢ V![a,h] â\86\92 Q G K V â\86\92 Q G (K.â\93\91{I}V) (#O)) →
- (â\88\80I,G,K,i. â¦\83G,Kâ¦\84 â\8a¢ #i![a,h] â\86\92 Q G K (#i) â\86\92 Q G (K.â\93\98{I}) (#(↑i))) →
- (â\88\80p,I,G,L,V,T. â¦\83G,Lâ¦\84 â\8a¢ V![a,h] â\86\92 â¦\83G,L.â\93\91{I}Vâ¦\84â\8a¢T![a,h] →
- Q G L V →Q G (L.ⓑ{I}V) T →Q G L (ⓑ{p,I}V.T)
+ (â\88\80I,G,K,V. â\9dªG,Kâ\9d« â\8a¢ V![h,a] â\86\92 Q G K V â\86\92 Q G (K.â\93\91[I]V) (#O)) →
+ (â\88\80I,G,K,i. â\9dªG,Kâ\9d« â\8a¢ #i![h,a] â\86\92 Q G K (#i) â\86\92 Q G (K.â\93\98[I]) (#(↑i))) →
+ (â\88\80p,I,G,L,V,T. â\9dªG,Lâ\9d« â\8a¢ V![h,a] â\86\92 â\9dªG,L.â\93\91[I]Vâ\9d«â\8a¢T![h,a] →
+ Q G L V →Q G (L.ⓑ[I]V) T →Q G L (ⓑ[p,I]V.T)
) →
- (∀n,p,G,L,V,W,T,U. (a = Ⓣ → n ≤ 1) → ⦃G,L⦄ ⊢ V![a,h] → ⦃G,L⦄ ⊢ T![a,h] →
- â¦\83G,Lâ¦\84 â\8a¢ V â¬\8c*[h,1,0]W â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] â\93\9b{p}W.U →
+ (∀n,p,G,L,V,W,T,U. ad a n → ❪G,L❫ ⊢ V![h,a] → ❪G,L❫ ⊢ T![h,a] →
+ â\9dªG,Lâ\9d« â\8a¢ V â¬\8c*[h,1,0]W â\86\92 â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] â\93\9b[p]W.U →
Q G L V → Q G L T → Q G L (ⓐV.T)
) →
- (â\88\80G,L,U,T. â¦\83G,Lâ¦\84â\8a¢ U![a,h] â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T![a,h] â\86\92 â¦\83G,Lâ¦\84 ⊢ U ⬌*[h,0,1] T →
+ (â\88\80G,L,U,T. â\9dªG,Lâ\9d«â\8a¢ U![h,a] â\86\92 â\9dªG,Lâ\9d« â\8a¢ T![h,a] â\86\92 â\9dªG,Lâ\9d« ⊢ U ⬌*[h,0,1] T →
Q G L U → Q G L T → Q G L (ⓝU.T)
) →
- â\88\80G,L,T. â¦\83G,Lâ¦\84â\8a¢ T![a,h] → Q G L T.
-#a #h #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #G #L #T #H
+ â\88\80G,L,T. â\9dªG,Lâ\9d«â\8a¢ T![h,a] → Q G L T.
+#h #a #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #G #L #T #H
elim H -G -L -T [5,6: /3 width=7 by cpms_div/ |*: /2 width=1 by/ ]
qed-.