X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_transition%2Fcpt.ma;h=53f9d778d6ee580474db80b1fb81347ce937499d;hp=229c32a96063e5b6eba66848f18891f92a594dd7;hb=bfd440cc2a790741616cae6b375609c6bbdc3b24;hpb=21e6d5cb0c9b6d6a6b9975b78ae752120a969cd6

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma
index 229c32a96..53f9d778d 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpt.ma
@@ -81,11 +81,17 @@ lemma cpt_ee (h) (n) (G) (L):
 /3 width=3 by cpg_ee, ist_succ, ex2_intro/
 qed.
 
-(* Basic properties *********************************************************)
-
 lemma cpt_refl (h) (G) (L): reflexive … (cpt h G L 0).
 /3 width=3 by cpg_refl, ex2_intro/ qed.
 
+(* Advanced properties ******************************************************)
+
+lemma cpt_sort (h) (G) (L):
+      ∀n. n ≤ 1 → ∀s. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] ⋆((next h)^n s).
+#h #G #L * //
+#n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/
+qed.
+
 (* Basic inversion lemmas ***************************************************)
 
 lemma cpt_inv_atom_sn (h) (n) (J) (G) (L):
@@ -109,6 +115,71 @@ elim (cpg_inv_atom1 … H) -H *
 ]
 qed-.
 
+lemma cpt_inv_sort_sn (h) (n) (G) (L) (s):
+      ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] X2 →
+      ∧∧ X2 = ⋆(((next h)^n) s) & n ≤ 1.
+#h #n #G #L #s #X2 * #c #Hc #H
+elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct
+/2 width=1 by conj/
+qed-.
+
+lemma cpt_inv_zero_sn (h) (n) (G) (L):
+      ∀X2. ⦃G,L⦄ ⊢ #0 ⬆[h,n] X2 →
+      ∨∨ ∧∧ X2 = #0 & n = 0
+       | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓓV1
+       | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,m] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓛV1 & n = ↑m.
+#h #n #G #L #X2 * #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
+  /4 width=8 by or3_intro1, ex3_3_intro, ex2_intro/
+| #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
+  elim (ist_inv_plus_SO_dx … H2) -H2 // #m #Hc #H destruct
+  /4 width=8 by or3_intro2, ex4_4_intro, ex2_intro/
+]
+qed-.
+
+lemma cpt_inv_zero_sn_unit (h) (n) (I) (K) (G):
+      ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ⬆[h,n] X2 → ∧∧ X2 = #0 & n = 0.
+#h #n #I #G #K #X2 #H
+elim (cpt_inv_zero_sn … H) -H *
+[ #H1 #H2 destruct /2 width=1 by conj/
+| #Y #X1 #X2 #_ #_ #H destruct
+| #m #Y #X1 #X2 #_ #_ #H destruct
+]
+qed.
+
+lemma cpt_inv_lref_sn (h) (n) (G) (L) (i):
+      ∀X2. ⦃G,L⦄ ⊢ #↑i ⬆[h,n] X2 →
+      ∨∨ ∧∧ X2 = #(↑i) & n = 0
+       | ∃∃I,K,T. ⦃G,K⦄ ⊢ #i ⬆[h,n] T & ⇧*[1] T ≘ X2 & L = K.ⓘ{I}.
+#h #n #G #L #i #X2 * #c #Hc #H elim (cpg_inv_lref1 … H) -H *
+[ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or_introl, conj/
+| #I #K #V2 #HV2 #HVT2 #H destruct
+ /4 width=6 by ex3_3_intro, ex2_intro, or_intror/
+]
+qed-.
+
+lemma cpt_inv_lref_sn_ctop (n) (h) (G) (i):
+      ∀X2. ⦃G,⋆⦄ ⊢ #i ⬆[h,n] X2 → ∧∧ X2 = #i & n = 0.
+#h #n #G * [| #i ] #X2 #H
+[ elim (cpt_inv_zero_sn … H) -H *
+  [ #H1 #H2 destruct /2 width=1 by conj/
+  | #Y #X1 #X2 #_ #_ #H destruct
+  | #m #Y #X1 #X2 #_ #_ #H destruct
+  ]
+| elim (cpt_inv_lref_sn … H) -H *
+  [ #H1 #H2 destruct /2 width=1 by conj/
+  | #Z #Y #X0 #_ #_ #H destruct
+  ]
+]
+qed.
+
+lemma cpt_inv_gref_sn (h) (n) (G) (L) (l):
+      ∀X2. ⦃G,L⦄ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0.
+#h #n #G #L #l #X2 * #c #Hc #H elim (cpg_inv_gref1 … H) -H
+#H1 #H2 destruct /2 width=1 by conj/ 
+qed-.
+
 lemma cpt_inv_bind_sn (h) (n) (p) (I) (G) (L) (V1) (T1):
       ∀X2. ⦃G,L⦄ ⊢ ⓑ{p,I}V1.T1 ⬆[h,n] X2 →
       ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬆[h,0] V2 & ⦃G,L.ⓑ{I}V1⦄ ⊢ T1 ⬆[h,n] T2