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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/drop.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/drop.ma
index 507560f88..e4404e137 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/drop.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/getl/drop.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/getl/props.ma".
+include "Basic-1/getl/props.ma".
 
-include "LambdaDelta-1/clear/drop.ma".
+include "Basic-1/clear/drop.ma".
 
 theorem getl_drop:
  \forall (b: B).(\forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (h: 
@@ -59,6 +59,9 @@ n) O (CHead c0 k t) e)))).(\lambda (H1: (getl (S n) (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) (getl_gen_S k c0 (CHead e (Bind b) u) t 
 n H1)) (r k (S n)) (r_S k n)) t)))) h)))))))) c)).
+(* COMMENTS
+Initial nodes: 827
+END *)
 
 theorem getl_drop_conf_lt:
  \forall (b: B).(\forall (c: C).(\forall (c0: C).(\forall (u: T).(\forall (i: 
@@ -329,6 +332,9 @@ T).(\lambda (e0: C).(getl (S i0) (CHead x1 k x2) (CHead e0 (Bind b) v))))
 h d x3)) (getl_head k i0 x1 (CHead x4 (Bind b) x3) H23 x2) H24) u H22)))))))) 
 H21)))))) e H11))))))))) (drop_gen_skip_l c0 e t h (plus (S i0) d) k 
 H9))))))) i H1 H7 IHx)))) k0 H5 H6))))))) x H3 H4)))) H2)))))))))))))) c)).
+(* COMMENTS
+Initial nodes: 6137
+END *)
 
 theorem getl_drop_conf_ge:
  \forall (i: nat).(\forall (a: C).(\forall (c: C).((getl i c a) \to (\forall 
@@ -342,6 +348,9 @@ in (ex2_ind C (\lambda (e0: C).(drop i O c e0)) (\lambda (e0: C).(clear e0
 a)) (getl (minus i h) e a) (\lambda (x: C).(\lambda (H3: (drop i O c 
 x)).(\lambda (H4: (clear x a)).(getl_intro (minus i h) e a x (drop_conf_ge i 
 x c H3 e h d H0 H1) H4)))) H2)))))))))).
+(* COMMENTS
+Initial nodes: 141
+END *)
 
 theorem getl_conf_ge_drop:
  \forall (b: B).(\forall (c1: C).(\forall (e: C).(\forall (u: T).(\forall (i: 
@@ -355,6 +364,9 @@ nat).(\lambda (H: (getl i c1 (CHead e (Bind b) u))).(\lambda (c2: C).(\lambda
 u i H) c2 (S O) i H0 (eq_ind_r nat (plus (S O) i) (\lambda (n: nat).(le n (S 
 i))) (le_n (S i)) (plus i (S O)) (plus_sym i (S O)))) i (minus_Sx_SO i)) in 
 H3)))))))).
+(* COMMENTS
+Initial nodes: 151
+END *)
 
 theorem getl_drop_conf_rev:
  \forall (j: nat).(\forall (e1: C).(\forall (e2: C).((drop j O e1 e2) \to 
@@ -366,6 +378,9 @@ c2 (CHead e2 (Bind b) v2)) \to (ex2 C (\lambda (c1: C).(drop j O c1 c2))
 e2)).(\lambda (b: B).(\lambda (c2: C).(\lambda (v2: T).(\lambda (i: 
 nat).(\lambda (H0: (getl i c2 (CHead e2 (Bind b) v2))).(drop_conf_rev j e1 e2 
 H c2 (S i) (getl_drop b c2 e2 v2 i H0)))))))))).
+(* COMMENTS
+Initial nodes: 69
+END *)
 
 theorem drop_getl_trans_lt:
  \forall (i: nat).(\forall (d: nat).((lt i d) \to (\forall (c1: C).(\forall 
@@ -399,6 +414,9 @@ c1 (CHead e1 (Bind b) (lift h (minus d (S i)) v)))) (\lambda (e1: C).(drop h
 (minus d (S i)) e1 e2)) x1 (getl_intro i c1 (CHead x1 (Bind b) (lift h (minus 
 d (S i)) v)) x0 H5 H9) H10)))) H8)))))) (drop_trans_le i d (le_S_n i d (le_S 
 (S i) d H)) c1 c2 h H0 x H3))))) H2)))))))))))).
+(* COMMENTS
+Initial nodes: 627
+END *)
 
 theorem drop_getl_trans_le:
  \forall (i: nat).(\forall (d: nat).((le i d) \to (\forall (c1: C).(\forall 
@@ -424,6 +442,9 @@ e2)))) (\lambda (x0: C).(\lambda (H6: (drop i O c1 x0)).(\lambda (H7: (drop h
 O c1 e0))) (\lambda (e0: C).(\lambda (e1: C).(drop h (minus d i) e0 e1))) 
 (\lambda (_: C).(\lambda (e1: C).(clear e1 e2))) x0 x H6 H7 H4)))) H5))))) 
 H2)))))))))).
+(* COMMENTS
+Initial nodes: 323
+END *)
 
 theorem drop_getl_trans_ge:
  \forall (i: nat).(\forall (c1: C).(\forall (c2: C).(\forall (d: 
@@ -437,6 +458,9 @@ C).(\lambda (H0: (getl i c2 e2)).(\lambda (H1: (le d i)).(let H2 \def
 (\lambda (e: C).(clear e e2)) (getl (plus i h) c1 e2) (\lambda (x: 
 C).(\lambda (H3: (drop i O c2 x)).(\lambda (H4: (clear x e2)).(getl_intro 
 (plus i h) c1 e2 x (drop_trans_ge i c1 c2 d h H x H3 H1) H4)))) H2)))))))))).
+(* COMMENTS
+Initial nodes: 137
+END *)
 
 theorem getl_drop_trans:
  \forall (c1: C).(\forall (c2: C).(\forall (h: nat).((getl h c1 c2) \to 
@@ -484,4 +508,7 @@ n)) O (CHead c2 (Flat f) t) e2))))))).(\lambda (H0: (getl (S n) (CHead c2
 (Flat f) t) c3)).(\lambda (e2: C).(\lambda (i: nat).(\lambda (H1: (drop (S i) 
 O c3 e2)).(drop_drop (Flat f) (plus i (S n)) c2 e2 (IHc c3 (S n) (getl_gen_S 
 (Flat f) c2 c3 t n H0) e2 i H1) t))))))) h))))) k)))) c1).
+(* COMMENTS
+Initial nodes: 953
+END *)