include "basic_2/notation/relations/degree_6.ma".
include "basic_2/grammar/genv.ma".
-include "basic_2/relocation/ldrop.ma".
+include "basic_2/substitution/drop.ma".
include "basic_2/static/sd.ma".
(* DEGREE ASSIGNMENT FOR TERMS **********************************************)
(* activate genv *)
inductive da (h:sh) (g:sd h): relation4 genv lenv term nat ≝
| da_sort: ∀G,L,k,l. deg h g k l → da h g G L (⋆k) l
-| da_ldef: â\88\80G,L,K,V,i,l. â\87©[i] L ≡ K.ⓓV → da h g G K V l → da h g G L (#i) l
-| da_ldec: â\88\80G,L,K,W,i,l. â\87©[i] L ≡ K.ⓛW → da h g G K W l → da h g G L (#i) (l+1)
+| da_ldef: â\88\80G,L,K,V,i,l. â¬\87[i] L ≡ K.ⓓV → da h g G K V l → da h g G L (#i) l
+| da_ldec: â\88\80G,L,K,W,i,l. â¬\87[i] L ≡ K.ⓛW → da h g G K W l → da h g G L (#i) (l+1)
| da_bind: ∀a,I,G,L,V,T,l. da h g G (L.ⓑ{I}V) T l → da h g G L (ⓑ{a,I}V.T) l
| da_flat: ∀I,G,L,V,T,l. da h g G L T l → da h g G L (ⓕ{I}V.T) l
.
/2 width=5 by da_inv_sort_aux/ qed-.
fact da_inv_lref_aux: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀j. T = #j →
- (â\88\83â\88\83K,V. â\87©[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
- (â\88\83â\88\83K,W,l0. â\87©[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 &
+ (â\88\83â\88\83K,V. â¬\87[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
+ (â\88\83â\88\83K,W,l0. â¬\87[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 &
l = l0 + 1
).
#h #g #G #L #T #l * -G -L -T -l
qed-.
lemma da_inv_lref: ∀h,g,G,L,j,l. ⦃G, L⦄ ⊢ #j ▪[h, g] l →
- (â\88\83â\88\83K,V. â\87©[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
- (â\88\83â\88\83K,W,l0. â\87©[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 & l = l0+1).
+ (â\88\83â\88\83K,V. â¬\87[j] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ▪[h, g] l) ∨
+ (â\88\83â\88\83K,W,l0. â¬\87[j] L ≡ K.ⓛW & ⦃G, K⦄ ⊢ W ▪[h, g] l0 & l = l0+1).
/2 width=3 by da_inv_lref_aux/ qed-.
fact da_inv_gref_aux: ∀h,g,G,L,T,l. ⦃G, L⦄ ⊢ T ▪[h, g] l → ∀p0. T = §p0 → ⊥.