(* Properties based on preservation *****************************************)
lemma cnv_cpms_ntas (h) (a) (G) (L):
- â\88\80T. â¦\83G,Lâ¦\84 â\8a¢ T ![h,a] â\86\92 â\88\80n,U.â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] U â\86\92 â¦\83G,Lâ¦\84 ⊢ T :*[h,a,n] U.
+ â\88\80T. â\9dªG,Lâ\9d« â\8a¢ T ![h,a] â\86\92 â\88\80n,U.â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] U â\86\92 â\9dªG,Lâ\9d« ⊢ T :*[h,a,n] U.
/3 width=4 by ntas_intro, cnv_cpms_trans/ qed.
(* Inversion lemmas based on preservation ***********************************)
lemma ntas_inv_plus (h) (a) (n1) (n2) (G) (L):
- â\88\80T1,T2. â¦\83G,Lâ¦\84 ⊢ T1 :*[h,a,n1+n2] T2 →
- â\88\83â\88\83T0. â¦\83G,Lâ¦\84 â\8a¢ T1 :*[h,a,n1] T0 & â¦\83G,Lâ¦\84 ⊢ T0 :*[h,a,n2] T2.
+ â\88\80T1,T2. â\9dªG,Lâ\9d« ⊢ T1 :*[h,a,n1+n2] T2 →
+ â\88\83â\88\83T0. â\9dªG,Lâ\9d« â\8a¢ T1 :*[h,a,n1] T0 & â\9dªG,Lâ\9d« ⊢ T0 :*[h,a,n2] T2.
#h #a #n1 #n2 #G #L #T1 #T2 * #X0 #HT2 #HT1 #H20 #H10
elim (cpms_inv_plus … H10) -H10 #T0 #H10 #H00
lapply (cnv_cpms_trans … HT1 … H10) #HT0
qed-.
lemma ntas_inv_appl_sn (h) (a) (m) (G) (L) (V) (T):
- â\88\80X. â¦\83G,Lâ¦\84 ⊢ ⓐV.T :*[h,a,m] X →
- â\88¨â\88¨ â\88\83â\88\83n,p,W,U,U0. n â\89¤ m & ad a n & â¦\83G,Lâ¦\84 â\8a¢ V :*[h,a,1] W & â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,n] â\93\9b{p}W.U0 & â¦\83G,L.â\93\9bWâ¦\84 â\8a¢ U0 :*[h,a,m-n] U & â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.â\93\9b{p}W.U â¬\8c*[h] X & â¦\83G,Lâ¦\84 ⊢ X ![h,a]
- | â\88\83â\88\83n,p,W,U,U0. m â\89¤ n & ad a n & â¦\83G,Lâ¦\84 â\8a¢ V :*[h,a,1] W & â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,m] U & â¦\83G,Lâ¦\84 â\8a¢ U :*[h,a,n-m] â\93\9b{p}W.U0 & â¦\83G,Lâ¦\84 â\8a¢ â\93\90V.U â¬\8c*[h] X & â¦\83G,Lâ¦\84 ⊢ X ![h,a].
+ â\88\80X. â\9dªG,Lâ\9d« ⊢ ⓐV.T :*[h,a,m] X →
+ â\88¨â\88¨ â\88\83â\88\83n,p,W,U,U0. n â\89¤ m & ad a n & â\9dªG,Lâ\9d« â\8a¢ V :*[h,a,1] W & â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,n] â\93\9b[p]W.U0 & â\9dªG,L.â\93\9bWâ\9d« â\8a¢ U0 :*[h,a,m-n] U & â\9dªG,Lâ\9d« â\8a¢ â\93\90V.â\93\9b[p]W.U â¬\8c*[h] X & â\9dªG,Lâ\9d« ⊢ X ![h,a]
+ | â\88\83â\88\83n,p,W,U,U0. m â\89¤ n & ad a n & â\9dªG,Lâ\9d« â\8a¢ V :*[h,a,1] W & â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,m] U & â\9dªG,Lâ\9d« â\8a¢ U :*[h,a,n-m] â\93\9b[p]W.U0 & â\9dªG,Lâ\9d« â\8a¢ â\93\90V.U â¬\8c*[h] X & â\9dªG,Lâ\9d« ⊢ X ![h,a].
#h #a #m #G #L #V #T #X
* #X0 #HX #HVT #HX0 #HTX0
elim (cnv_inv_appl … HVT) #n #p #W #U0 #Ha #HV #HT #HVW #HTU0