(* Properties with t-bound context-sensitive rt-computarion for terms *******)
lemma lprs_cpms_trans (h) (n) (G) (T1:term) (T2:term):
- â\88\80L2. â\9dªG,L2â\9d« ⊢ T1 ➡*[h,n] T2 →
- â\88\80L1. â\9dªG,L1â\9d« â\8a¢ â\9e¡*[h,0] L2 â\86\92 â\9dªG,L1â\9d« ⊢ T1 ➡*[h,n] T2.
+ â\88\80L2. â\9d¨G,L2â\9d© ⊢ T1 ➡*[h,n] T2 →
+ â\88\80L1. â\9d¨G,L1â\9d© â\8a¢ â\9e¡*[h,0] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ T1 ➡*[h,n] T2.
#h #n #G #T1 #T2 #L2 #HT12 #L1 #H
@(lprs_ind_sn … H) -L1
/2 width=3 by lpr_cpms_trans/
qed-.
lemma lprs_cpm_trans (h) (n) (G) (T1:term) (T2:term):
- â\88\80L2. â\9dªG,L2â\9d« ⊢ T1 ➡[h,n] T2 →
- â\88\80L1. â\9dªG,L1â\9d« â\8a¢ â\9e¡*[h,0] L2 â\86\92 â\9dªG,L1â\9d« ⊢ T1 ➡*[h,n] T2.
+ â\88\80L2. â\9d¨G,L2â\9d© ⊢ T1 ➡[h,n] T2 →
+ â\88\80L1. â\9d¨G,L1â\9d© â\8a¢ â\9e¡*[h,0] L2 â\86\92 â\9d¨G,L1â\9d© ⊢ T1 ➡*[h,n] T2.
/3 width=3 by lprs_cpms_trans, cpm_cpms/ qed-.
(* Basic_2A1: includes cprs_bind2 *)
lemma cpms_bind_alt (h) (n) (G) (L):
- â\88\80V1,V2. â\9dªG,Lâ\9d« ⊢ V1 ➡*[h,0] V2 →
- â\88\80I,T1,T2. â\9dªG,L.â\93\91[I]V2â\9d« ⊢ T1 ➡*[h,n] T2 →
- â\88\80p. â\9dªG,Lâ\9d« ⊢ ⓑ[p,I]V1.T1 ➡*[h,n] ⓑ[p,I]V2.T2.
+ â\88\80V1,V2. â\9d¨G,Lâ\9d© ⊢ V1 ➡*[h,0] V2 →
+ â\88\80I,T1,T2. â\9d¨G,L.â\93\91[I]V2â\9d© ⊢ T1 ➡*[h,n] T2 →
+ â\88\80p. â\9d¨G,Lâ\9d© ⊢ ⓑ[p,I]V1.T1 ➡*[h,n] ⓑ[p,I]V2.T2.
/4 width=5 by lprs_cpms_trans, lprs_pair, cpms_bind/ qed.
(* Inversion lemmas with t-bound context-sensitive rt-computarion for terms *)
(* Basic_2A1: includes: cprs_inv_abst1 *)
(* Basic_2A1: uses: scpds_inv_abst1 *)
lemma cpms_inv_abst_sn (h) (n) (G) (L):
- â\88\80p,V1,T1,X2. â\9dªG,Lâ\9d« ⊢ ⓛ[p]V1.T1 ➡*[h,n] X2 →
- â\88\83â\88\83V2,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â\9e¡*[h,0] V2 & â\9dªG,L.â\93\9bV1â\9d« ⊢ T1 ➡*[h,n] T2 & X2 = ⓛ[p]V2.T2.
+ â\88\80p,V1,T1,X2. â\9d¨G,Lâ\9d© ⊢ ⓛ[p]V1.T1 ➡*[h,n] X2 →
+ â\88\83â\88\83V2,T2. â\9d¨G,Lâ\9d© â\8a¢ V1 â\9e¡*[h,0] V2 & â\9d¨G,L.â\93\9bV1â\9d© ⊢ T1 ➡*[h,n] T2 & X2 = ⓛ[p]V2.T2.
#h #n #G #L #p #V1 #T1 #X2 #H
@(cpms_ind_dx … H) -X2 /2 width=5 by ex3_2_intro/
#n1 #n2 #X #X2 #_ * #V #T #HV1 #HT1 #H1 #H2 destruct
qed-.
lemma cpms_inv_abst_sn_cprs (h) (n) (p) (G) (L) (W):
- â\88\80T,X. â\9dªG,Lâ\9d« ⊢ ⓛ[p]W.T ➡*[h,n] X →
- â\88\83â\88\83U. â\9dªG,L.â\93\9bWâ\9d«â\8a¢ T â\9e¡*[h,n] U & â\9dªG,Lâ\9d« ⊢ ⓛ[p]W.U ➡*[h,0] X.
+ â\88\80T,X. â\9d¨G,Lâ\9d© ⊢ ⓛ[p]W.T ➡*[h,n] X →
+ â\88\83â\88\83U. â\9d¨G,L.â\93\9bWâ\9d©â\8a¢ T â\9e¡*[h,n] U & â\9d¨G,Lâ\9d© ⊢ ⓛ[p]W.U ➡*[h,0] X.
#h #n #p #G #L #W #T #X #H
elim (cpms_inv_abst_sn … H) -H #W0 #U #HW0 #HTU #H destruct
@(ex2_intro … HTU) /2 width=1 by cpms_bind/
(* Basic_2A1: includes: cprs_inv_abst *)
lemma cpms_inv_abst_bi (h) (n) (p1) (p2) (G) (L):
- â\88\80W1,W2,T1,T2. â\9dªG,Lâ\9d« ⊢ ⓛ[p1]W1.T1 ➡*[h,n] ⓛ[p2]W2.T2 →
- â\88§â\88§ p1 = p2 & â\9dªG,Lâ\9d« â\8a¢ W1 â\9e¡*[h,0] W2 & â\9dªG,L.â\93\9bW1â\9d« ⊢ T1 ➡*[h,n] T2.
+ â\88\80W1,W2,T1,T2. â\9d¨G,Lâ\9d© ⊢ ⓛ[p1]W1.T1 ➡*[h,n] ⓛ[p2]W2.T2 →
+ â\88§â\88§ p1 = p2 & â\9d¨G,Lâ\9d© â\8a¢ W1 â\9e¡*[h,0] W2 & â\9d¨G,L.â\93\9bW1â\9d© ⊢ T1 ➡*[h,n] T2.
#h #n #p1 #p2 #G #L #W1 #W2 #T1 #T2 #H
elim (cpms_inv_abst_sn … H) -H #W #T #HW1 #HT1 #H destruct
/2 width=1 by and3_intro/
(* Basic_1: was pr3_gen_abbr *)
(* Basic_2A1: includes: cprs_inv_abbr1 *)
lemma cpms_inv_abbr_sn_dx (h) (n) (G) (L):
- â\88\80p,V1,T1,X2. â\9dªG,Lâ\9d« ⊢ ⓓ[p]V1.T1 ➡*[h,n] X2 →
- â\88¨â\88¨ â\88\83â\88\83V2,T2. â\9dªG,Lâ\9d« â\8a¢ V1 â\9e¡*[h,0] V2 & â\9dªG,L.â\93\93V1â\9d« ⊢ T1 ➡*[h,n] T2 & X2 = ⓓ[p]V2.T2
- | â\88\83â\88\83T2. â\9dªG,L.â\93\93V1â\9d« ⊢ T1 ➡*[h,n] T2 & ⇧[1] X2 ≘ T2 & p = Ⓣ.
+ â\88\80p,V1,T1,X2. â\9d¨G,Lâ\9d© ⊢ ⓓ[p]V1.T1 ➡*[h,n] X2 →
+ â\88¨â\88¨ â\88\83â\88\83V2,T2. â\9d¨G,Lâ\9d© â\8a¢ V1 â\9e¡*[h,0] V2 & â\9d¨G,L.â\93\93V1â\9d© ⊢ T1 ➡*[h,n] T2 & X2 = ⓓ[p]V2.T2
+ | â\88\83â\88\83T2. â\9d¨G,L.â\93\93V1â\9d© ⊢ T1 ➡*[h,n] T2 & ⇧[1] X2 ≘ T2 & p = Ⓣ.
#h #n #G #L #p #V1 #T1 #X2 #H
@(cpms_ind_dx … H) -X2 -n /3 width=5 by ex3_2_intro, or_introl/
#n1 #n2 #X #X2 #_ * *
(* Basic_2A1: uses: scpds_inv_abbr_abst *)
lemma cpms_inv_abbr_abst (h) (n) (G) (L):
- â\88\80p1,p2,V1,W2,T1,T2. â\9dªG,Lâ\9d« ⊢ ⓓ[p1]V1.T1 ➡*[h,n] ⓛ[p2]W2.T2 →
- â\88\83â\88\83T. â\9dªG,L.â\93\93V1â\9d« ⊢ T1 ➡*[h,n] T & ⇧[1] ⓛ[p2]W2.T2 ≘ T & p1 = Ⓣ.
+ â\88\80p1,p2,V1,W2,T1,T2. â\9d¨G,Lâ\9d© ⊢ ⓓ[p1]V1.T1 ➡*[h,n] ⓛ[p2]W2.T2 →
+ â\88\83â\88\83T. â\9d¨G,L.â\93\93V1â\9d© ⊢ T1 ➡*[h,n] T & ⇧[1] ⓛ[p2]W2.T2 ≘ T & p1 = Ⓣ.
#h #n #G #L #p1 #p2 #V1 #W2 #T1 #T2 #H
elim (cpms_inv_abbr_sn_dx … H) -H *
[ #V #T #_ #_ #H destruct