qed.
lemma cpm_ell: ∀n,h,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 →
- â¬\86*[1] V2 â\89\98 W2 â\86\92 â¦\83G, K.â\93\9bV1â¦\84 â\8a¢ #0 â\9e¡[⫯n, h] W2.
+ â¬\86*[1] V2 â\89\98 W2 â\86\92 â¦\83G, K.â\93\9bV1â¦\84 â\8a¢ #0 â\9e¡[â\86\91n, h] W2.
#n #h #G #K #V1 #V2 #W2 *
/3 width=5 by cpg_ell, ex2_intro, isrt_succ/
qed.
lemma cpm_lref: ∀n,h,I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T →
- â¬\86*[1] T â\89\98 U â\86\92 â¦\83G, K.â\93\98{I}â¦\84 â\8a¢ #⫯i ➡[n, h] U.
+ â¬\86*[1] T â\89\98 U â\86\92 â¦\83G, K.â\93\98{I}â¦\84 â\8a¢ #â\86\91i ➡[n, h] U.
#n #h #I #G #K #T #U #i *
/3 width=5 by cpg_lref, ex2_intro/
qed.
/3 width=3 by cpg_eps, isrt_plus_O2, ex2_intro/
qed.
-lemma cpm_ee: â\88\80n,h,G,L,V1,V2,T. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[n, h] V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.T â\9e¡[⫯n, h] V2.
+lemma cpm_ee: â\88\80n,h,G,L,V1,V2,T. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[n, h] V2 â\86\92 â¦\83G, Lâ¦\84 â\8a¢ â\93\9dV1.T â\9e¡[â\86\91n, h] V2.
#n #h #G #L #V1 #V2 #T *
/3 width=3 by cpg_ee, isrt_succ, ex2_intro/
qed.
| ∃∃K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 & ⬆*[1] V2 ≘ T2 &
L = K.ⓓV1 & J = LRef 0
| ∃∃k,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[k, h] V2 & ⬆*[1] V2 ≘ T2 &
- L = K.â\93\9bV1 & J = LRef 0 & n = ⫯k
+ L = K.â\93\9bV1 & J = LRef 0 & n = â\86\91k
| ∃∃I,K,T,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T & ⬆*[1] T ≘ T2 &
- L = K.â\93\98{I} & J = LRef (⫯i).
+ L = K.â\93\98{I} & J = LRef (â\86\91i).
#n #h #J #G #L #T2 * #c #Hc #H elim (cpg_inv_atom1 … H) -H *
[ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or5_intro0, conj/
| #s #H1 #H2 #H3 destruct /4 width=3 by isrt_inv_01, or5_intro1, ex3_intro/
| ∃∃K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 & ⬆*[1] V2 ≘ T2 &
L = K.ⓓV1
| ∃∃k,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[k, h] V2 & ⬆*[1] V2 ≘ T2 &
- L = K.â\93\9bV1 & n = ⫯k.
+ L = K.â\93\9bV1 & n = â\86\91k.
#n #h #G #L #T2 * #c #Hc #H elim (cpg_inv_zero1 … H) -H *
[ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or3_intro0, conj/
| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
]
qed-.
-lemma cpm_inv_lref1: â\88\80n,h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #⫯i ➡[n, h] T2 →
- â\88¨â\88¨ T2 = #(⫯i) ∧ n = 0
+lemma cpm_inv_lref1: â\88\80n,h,G,L,T2,i. â¦\83G, Lâ¦\84 â\8a¢ #â\86\91i ➡[n, h] T2 →
+ â\88¨â\88¨ T2 = #(â\86\91i) ∧ n = 0
| ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ➡[n, h] T & ⬆*[1] T ≘ T2 & L = K.ⓘ{I}.
#n #h #G #L #T2 #i * #c #Hc #H elim (cpg_inv_lref1 … H) -H *
[ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or_introl, conj/
∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[n, h] V2 & ⦃G, L⦄ ⊢ U1 ➡[n, h] T2 &
U2 = ⓝV2.T2
| ⦃G, L⦄ ⊢ U1 ➡[n, h] U2
- | â\88\83â\88\83k. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[k, h] U2 & n = ⫯k.
+ | â\88\83â\88\83k. â¦\83G, Lâ¦\84 â\8a¢ V1 â\9e¡[k, h] U2 & n = â\86\91k.
#n #h #G #L #V1 #U1 #U2 * #c #Hc #H elim (cpg_inv_cast1 … H) -H *
[ #cV #cT #V2 #T2 #HV12 #HT12 #HcVT #H1 #H2 destruct
elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct