X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Fnlibrary%2FPTS%2Fgpts.ma;h=9af90225239158d425d63dd8cd90d8b2fbc2b1a7;hb=bf7be462a06e739b39af20f72362857e849a2aa0;hp=9a53cc00f4d771aad41d00ceca43d5e6a87d4460;hpb=471987d6759c57e40fb89d435345cf654dc4aa39;p=helm.git

diff --git a/helm/software/matita/nlibrary/PTS/gpts.ma b/helm/software/matita/nlibrary/PTS/gpts.ma
index 9a53cc00f..9af902252 100644
--- a/helm/software/matita/nlibrary/PTS/gpts.ma
+++ b/helm/software/matita/nlibrary/PTS/gpts.ma
@@ -177,92 +177,8 @@ ntheorem substitution_tj:
        nrewrite > (delift (lift N O O) A1 O O O ??); //;
        nnormalize in Heq; ndestruct;/2/;
     ##|#H; #L; #N1; #Heq; nnormalize in Heq;
-       #tjN1; nnormalize; ndestruct;          
-    ncheck( let clause_829:
- ∀x1947: ?.
-  ∀x1948: ?.
-   ∀x1949: ?.
-    ∀x1950: ?.
-     ∀x1951: ?.
-      eq T (lift (subst x1947 (plus x1948 x1949) x1950) x1949 x1951)
-        (subst (lift x1947 x1949 x1951) (plus x1948 (plus x1949 x1951))
-          x1950)
- ≝ λx1947:?.
-      λx1948:?.
-       λx1949:?.
-        λx1950:?.
-         λx1951:?.
-          rewrite_l nat (plus (plus x1948 x1949) x1951)
-            (λx:nat.
-              eq T (lift (subst x1947 (plus x1948 x1949) x1950) x1949 x1951)
-                (subst (lift x1947 x1949 x1951) x x1950))
-            (lift_subst_ijk x1950 x1947 x1951 x1948 x1949)
-            (plus x1948 (plus x1949 x1951))
-            (associative_plus x1948 x1949 x1951) in
- let clause_60: ∀x156: ?. eq nat (S x156) (plus x156 (S O))
-  ≝ λx156:?.
-       rewrite_r nat (plus x156 O) (λx:nat. eq nat (S x) (plus x156 (S O)))
-         (plus_n_Sm x156 O) x156 (plus_n_O x156) in
-  let clause_996 :
-   eq Type
-     (TJ (cons T (subst ? ? ?) ?) (Rel O)
-       (subst (lift ? O (S O)) (plus ? (S O)) ?))
-     (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
-       (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))
-   ≝ rewrite_l nat (S (length T L))
-         (λx:nat.
-           eq Type
-             (TJ
-               (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
-               (Rel O) (subst (lift H O (S O)) x N1))
-             (TJ
-               (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
-               (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
-         (refl Type
-           (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
-             (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
-         (plus (length T L) (S O)) (clause_60 (length T L)) in
-   let clause_995:
-    eq Type
-      (TJ (cons T (subst ? ? ?) ?) (Rel O)
-        (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?))
-      (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
-        (Rel O) (subst (lift H O (S O)) (S (length T L)) N1))
-    ≝ rewrite_l nat (S O)
-          (λx:nat.
-            eq Type
-              (TJ (cons T (subst ? ? ?) ?) (Rel O)
-                (subst (lift ? O (S O)) (plus ? x) ?))
-              (TJ
-                (cons T (subst H (length T L) N1)
-                  (append T (substl L N1) G1)) (Rel O)
-                (subst (lift H O (S O)) (S (length T L)) N1))) clause_996
-          (plus O (S O)) (plus_O_n (S O)) in
-    rewrite_r T
-      (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?)
-      (λx:T.
-        eq Type
-          (TJ (cons T (subst ? (plus ? O) ?) ?) (Rel O) x)
-          (TJ (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
-            (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
-      (rewrite_l nat ?
-        (λx:nat.
-          eq Type
-            (TJ (cons T (subst ? x ?) ?) (Rel O)
-              (subst (lift ? O (S O)) (plus ? (plus O (S O))) ?))
-            (TJ
-              (cons T (subst H (length T L) N1) (append T (substl L N1) G1))
-              (Rel O) (subst (lift H O (S O)) (S (length T L)) N1)))
-        clause_995 (plus ? O) (plus_n_O ?))
-      (lift (subst ? (plus ? O) ?) O (S O))
-      (clause_829 ? ? O ? (S O))
-).
-       napplyS start;
-       (* napplyS start; *)
-       (* napplyS start non va *)
-       ncut (S (length T L) = ((length T L)+0+1)); ##[//##] #Heq;
-       ncheck start.
-       napplyS start;/2/; 
+       #tjN1; nnormalize; ndestruct;             
+       napplyS start; /2/;
     ##]
   ##|#G; #P; #Q; #R; #i; #tjP; #tjR; #Hind1; #Hind2;
      #G1; #D; #N; ncases D; nnormalize;
@@ -279,21 +195,23 @@ ntheorem substitution_tj:
     ##[/2/;
     ##|ncut (S (length T D) = (length T D)+1); ##[//##] #Heq1;
        nrewrite < Heq1; 
-       napply (Hind2 ? (P::D));//;
+       napply (Hind2 ? (P::D));nnormalize;//;
     ##]
   ##|#G; #P; #Q; #R; #S; #tjP; #tjS; #Hind1; #Hind2;
+     #G1; #D; #N; #Heq; #tjN; nnormalize in Hind1 ⊢ %;
+     nrewrite > (plus_n_O (length ? D)) in ⊢ (? ? ? (? ? % ?));
+     nrewrite > (subst_lemma R S N ? 0);
+     napplyS app; /2/;
+  ##|#G; #P; #Q; #R; #i; #tjR; #tjProd; #Hind1; #Hind2;
      #G1; #D; #N; #Heq; #tjN; nnormalize;
-     ncheck (
-             (subst (subst_aux  S (length T  D)  N)
-               (subst_aux  R (length T  D)  N))
-      ).
-     napplyS (app (substl D N@G1) (subst_aux P (length T D) N) A (subst_aux R (length T D) N) (subst_aux S (length T D) N) ?).
-     nlapply (subst_lemma R S N (length ? D) 0); #sl;
-     nrewrite < (plus_n_O ?) in sl; #sl;
-     nrewrite > sl;
-     nauto demod;
-     napply app; nnormalize in Hind1;/2/;
+     napplyS abs; 
+      ##[nnormalize in Hind2; /2/;
+      ##|(* napplyS (Hind1 G1 (P::D) N ? tjN); sistemare *)
+       ngeneralize in match (Hind1 G1 (P::D) N ? tjN); 
+        ##[#H; nnormalize in H; napplyS H;##|nnormalize; //##]
+      ##|##]
   ##|
+