| cpx_atom : ∀I,G,L. cpx h g G L (⓪{I}) (⓪{I})
| cpx_sort : ∀G,L,k,l. deg h g k (l+1) → cpx h g G L (⋆k) (⋆(next h k))
| cpx_delta: ∀I,G,L,K,V,V2,W2,i.
- ⇩[0, i] L ≡ K.ⓑ{I}V → cpx h g G K V V2 →
- ⇧[0, i + 1] V2 ≡ W2 → cpx h g G L (#i) W2
+ ⇩[i] L ≡ K.ⓑ{I}V → cpx h g G K V V2 →
+ ⇧[0, i+1] V2 ≡ W2 → cpx h g G L (#i) W2
| cpx_bind : ∀a,I,G,L,V1,V2,T1,T2.
cpx h g G L V1 V2 → cpx h g G (L.ⓑ{I}V1) T1 T2 →
cpx h g G L (ⓑ{a,I}V1.T1) (ⓑ{a,I}V2.T2)
[ //
| /2 width=2 by cpx_sort/
| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12
- elim (lsubr_fwd_drop2_bind … HL12 … HLK1) -HL12 -HLK1 *
+ elim (lsubr_fwd_ldrop2_bind … HL12 … HLK1) -HL12 -HLK1 *
/4 width=7 by cpx_delta, cpx_ti/
|4,9: /4 width=1 by cpx_bind, cpx_beta, lsubr_bind/
|5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/
#h #g * /2 width=1 by cpx_bind, cpx_flat/
qed.
-lemma cpx_delift: ∀h,g,I,G,K,V,T1,L,d. ⇩[0, d] L ≡ (K.ⓑ{I}V) →
+lemma cpx_delift: ∀h,g,I,G,K,V,T1,L,d. ⇩[d] L ≡ (K.ⓑ{I}V) →
∃∃T2,T. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 & ⇧[d, 1] T ≡ T2.
#h #g #I #G #K #V #T1 elim T1 -T1
[ * #i #L #d /2 width=4 by cpx_atom, lift_sort, lift_gref, ex2_2_intro/
]
qed-.
-lemma cpx_append: ∀h,g,G. l_appendable_sn … (cpx h g G).
-#h #g #G #K #T1 #T2 #H elim H -G -K -T1 -T2
-/2 width=3 by cpx_sort, cpx_bind, cpx_flat, cpx_zeta, cpx_tau, cpx_ti, cpx_beta, cpx_theta/
-#I #G #K #K0 #V1 #V2 #W2 #i #HK0 #_ #HVW2 #IHV12 #L
-lapply (ldrop_fwd_length_lt2 … HK0) #H
-@(cpx_delta … I … (L@@K0) V1 … HVW2) //
-@(ldrop_O1_append_sn_le … HK0) /2 width=2 by lt_to_le/ (**) (* /3/ does not work *)
-qed.
-
(* Basic inversion lemmas ***************************************************)
fact cpx_inv_atom1_aux: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → ∀J. T1 = ⓪{J} →
∨∨ T2 = ⓪{J}
| ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k) & J = Sort k
- | ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
- ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+ | ∃∃I,K,V,V2,i. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
+ ⇧[O, i+1] V2 ≡ T2 & J = LRef i.
#G #h #g #L #T1 #T2 * -L -T1 -T2
[ #I #G #L #J #H destruct /2 width=1 by or3_intro0/
| #G #L #k #l #Hkl #J #H destruct /3 width=5 by or3_intro1, ex3_2_intro/
lemma cpx_inv_atom1: ∀h,g,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[h, g] T2 →
∨∨ T2 = ⓪{J}
| ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k) & J = Sort k
- | ∃∃I,K,V,V2,i. ⇩[O, i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
- ⇧[O, i + 1] V2 ≡ T2 & J = LRef i.
+ | ∃∃I,K,V,V2,i. ⇩[i] L ≡ K.ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
+ ⇧[O, i+1] V2 ≡ T2 & J = LRef i.
/2 width=3 by cpx_inv_atom1_aux/ qed-.
lemma cpx_inv_sort1: ∀h,g,G,L,T2,k. ⦃G, L⦄ ⊢ ⋆k ➡[h, g] T2 → T2 = ⋆k ∨
lemma cpx_inv_lref1: ∀h,g,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h, g] T2 →
T2 = #i ∨
- ∃∃I,K,V,V2. ⇩[O, i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
- ⇧[O, i + 1] V2 ≡ T2.
+ ∃∃I,K,V,V2. ⇩[i] L ≡ K. ⓑ{I}V & ⦃G, K⦄ ⊢ V ➡[h, g] V2 &
+ ⇧[O, i+1] V2 ≡ T2.
#h #g #G #L #T2 #i #H
elim (cpx_inv_atom1 … H) -H /2 width=1 by or_introl/ *
[ #k #l #_ #_ #H destruct
| #T2 #_ #_ #H destruct
]
qed-.
-
-lemma cpx_fwd_shift1: ∀h,g,G,L1,L,T1,T. ⦃G, L⦄ ⊢ L1 @@ T1 ➡[h, g] T →
- ∃∃L2,T2. |L1| = |L2| & T = L2 @@ T2.
-#h #g #G #L1 @(lenv_ind_dx … L1) -L1 normalize
-[ #L #T1 #T #HT1
- @(ex2_2_intro … (⋆)) // (**) (* explicit constructor *)
-| #I #L1 #V1 #IH #L #T1 #X
- >shift_append_assoc normalize #H
- elim (cpx_inv_bind1 … H) -H *
- [ #V0 #T0 #_ #HT10 #H destruct
- elim (IH … HT10) -IH -HT10 #L2 #T2 #HL12 #H destruct
- >append_length >HL12 -HL12
- @(ex2_2_intro … (⋆.ⓑ{I}V0@@L2) T2) [ >append_length ] /2 width=3 by refl, trans_eq/ (**) (* explicit constructor *)
- | #T #_ #_ #H destruct
- ]
-]
-qed-.