X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fdrop%2Fprops.ma;h=ac802b1050b1348561db1eeb1f875fcbe2f1244a;hb=a88be1ca42c0969dbab9a5c76240f5931df876d9;hp=a0744633e65274ecac4bf95e63a5a2bde6f746d4;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop/props.ma
index a0744633e..ac802b105 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/drop/props.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/drop/fwd.ma".
+include "Basic-1/drop/fwd.ma".
 
-include "LambdaDelta-1/lift/props.ma".
+include "Basic-1/lift/props.ma".
 
-include "LambdaDelta-1/r/props.ma".
+include "Basic-1/r/props.ma".
 
 theorem drop_skip_bind:
  \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h 
@@ -29,6 +29,9 @@ d c e) \to (\forall (b: B).(\forall (u: T).(drop h (S d) (CHead c (Bind b)
 (H: (drop h d c e)).(\lambda (b: B).(\lambda (u: T).(eq_ind nat (r (Bind b) 
 d) (\lambda (n: nat).(drop h (S d) (CHead c (Bind b) (lift h n u)) (CHead e 
 (Bind b) u))) (drop_skip (Bind b) h d c e H u) d (refl_equal nat d)))))))).
+(* COMMENTS
+Initial nodes: 95
+END *)
 
 theorem drop_skip_flat:
  \forall (h: nat).(\forall (d: nat).(\forall (c: C).(\forall (e: C).((drop h 
@@ -40,6 +43,9 @@ f) (lift h (S d) u)) (CHead e (Flat f) u))))))))
 f) d) (\lambda (n: nat).(drop h (S d) (CHead c (Flat f) (lift h n u)) (CHead 
 e (Flat f) u))) (drop_skip (Flat f) h d c e H u) (S d) (refl_equal nat (S 
 d))))))))).
+(* COMMENTS
+Initial nodes: 101
+END *)
 
 theorem drop_S:
  \forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (h: 
@@ -81,6 +87,9 @@ k t) e)))).(\lambda (H1: (drop (S n) O (CHead c0 k t) (CHead e (Bind b)
 u))).(drop_drop k (S n) c0 e (eq_ind_r nat (S (r k n)) (\lambda (n0: 
 nat).(drop n0 O c0 e)) (H e u (r k n) (drop_gen_drop k c0 (CHead e (Bind b) 
 u) t n H1)) (r k (S n)) (r_S k n)) t)))) h)))))))) c)).
+(* COMMENTS
+Initial nodes: 807
+END *)
 
 theorem drop_ctail:
  \forall (c1: C).(\forall (c2: C).(\forall (d: nat).(\forall (h: nat).((drop 
@@ -136,6 +145,9 @@ T).(drop h (S n) (CTail k0 u (CHead c2 k t0)) (CTail k0 u (CHead x0 k x1))))
 (drop_skip k h n (CTail k0 u c2) (CTail k0 u x0) (IHc x0 (r k n) h H3 k0 u) 
 x1) t H2)) c3 H1))))))) (drop_gen_skip_l c2 c3 t h n k H0)))))))) d))))))) 
 c1).
+(* COMMENTS
+Initial nodes: 1211
+END *)
 
 theorem drop_mono:
  \forall (c: C).(\forall (x1: C).(\forall (d: nat).(\forall (h: nat).((drop h 
@@ -202,6 +214,9 @@ x3))) (f_equal3 C K T C CHead x4 x0 k k x3 x3 (sym_eq C x0 x4 (H x0 (r k n) h
 H5 x4 H8)) (refl_equal K k) (refl_equal T x3)) x5 (lift_inj x5 x3 h (r k n) 
 H11))))) x1 H6)) x2 H3)))))) (drop_gen_skip_l c0 x1 t h n k H1))))))) 
 (drop_gen_skip_l c0 x2 t h n k H2)))))))) d))))))) c).
+(* COMMENTS
+Initial nodes: 1539
+END *)
 
 theorem drop_conf_lt:
  \forall (k: K).(\forall (i: nat).(\forall (u: T).(\forall (c0: C).(\forall 
@@ -334,6 +349,9 @@ k d) c0 e0))) x2 x3 H6 (drop_drop (Flat f) i0 x0 (CHead x3 k x2) H7 x1)
 H8)))))) (H0 (drop_gen_drop (Flat f) c1 (CHead c0 k u) t i0 H1) x0 h d H5)) e 
 H3)))))) (drop_gen_skip_l c1 e t h (plus (S i0) d) (Flat f) H2))))))))) 
 k0)))) c)))))) i)).
+(* COMMENTS
+Initial nodes: 2972
+END *)
 
 theorem drop_conf_ge:
  \forall (i: nat).(\forall (a: C).(\forall (c: C).((drop i O c a) \to 
@@ -448,6 +466,9 @@ x1) a)) (drop_drop (Flat f) (minus i0 h) x0 a H9 x1) (minus (S i0) h)
 (minus_Sn_m i0 h (le_trans_plus_r d0 h i0 (le_S_n (plus d0 h) i0 H5))))) e 
 H6)))))) (drop_gen_skip_l c0 e t h d0 (Flat f) H4)))))) d H2 H3))))))))) 
 k)))) c))))) i).
+(* COMMENTS
+Initial nodes: 2726
+END *)
 
 theorem drop_conf_rev:
  \forall (j: nat).(\forall (e1: C).(\forall (e2: C).((drop j O e1 e2) \to 
@@ -504,6 +525,9 @@ C).(drop (S j0) O c1 c2)) (\lambda (c1: C).(drop i (S j0) c1 (CHead e2 (Flat
 f) t))) (CHead x (Flat f) (lift i (r (Flat f) j0) t)) (drop_drop (Flat f) j0 
 x c2 H3 (lift i (r (Flat f) j0) t)) (drop_skip (Flat f) i j0 x e2 H4 t))))) 
 H2))))) k (drop_gen_drop k e2 e3 t j0 H))))))))))) e1)))) j).
+(* COMMENTS
+Initial nodes: 1154
+END *)
 
 theorem drop_trans_le:
  \forall (i: nat).(\forall (d: nat).((le i d) \to (\forall (c1: C).(\forall 
@@ -616,6 +640,9 @@ i0)) x e2)).(ex_intro2 C (\lambda (e1: C).(drop (S i0) O (CHead c2 (Flat f)
 i0)) e1 e2)) x (drop_drop (Flat f) i0 c2 x H6 (lift h (r (Flat f) d0) x1)) 
 H7)))) (IHc x0 h H4 e2 (drop_gen_drop (Flat f) x0 e2 x1 i0 H5))) t H3))))))) 
 (drop_gen_skip_l c2 c3 t h d0 (Flat f) H0))))))))) k)))) c1))))) d)))) i).
+(* COMMENTS
+Initial nodes: 2453
+END *)
 
 theorem drop_trans_ge:
  \forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (d: 
@@ -704,4 +731,7 @@ F).(\lambda (H8: (drop h (r (Flat f) d0) c2 x0)).(\lambda (H9: (drop (r (Flat
 f) i0) O x0 e2)).(IHc x0 (r (Flat f) d0) h H8 e2 H9 H1)))) k H4 
 (drop_gen_drop k x0 e2 x1 i0 H6)) (lift h (r k d0) x1)) t H3))))))))) 
 (drop_gen_skip_l c2 c3 t h d0 k H))))))))) d))))))) c1)))) i).
+(* COMMENTS
+Initial nodes: 2020
+END *)