uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / sc3 / props.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sc3/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sc3/props.ma
index cd5ce1f7d42e880cd8a98e2cc4c35e211e57c277..e1d90925157134ce6f8f8b5edfe7a210d3415148 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sc3/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/sc3/props.ma
@@ -14,25 +14,25 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/sc3/defs.ma".
+include "Basic-1/sc3/defs.ma".
 
-include "LambdaDelta-1/sn3/lift1.ma".
+include "Basic-1/sn3/lift1.ma".
 
-include "LambdaDelta-1/nf2/lift1.ma".
+include "Basic-1/nf2/lift1.ma".
 
-include "LambdaDelta-1/csuba/arity.ma".
+include "Basic-1/csuba/arity.ma".
 
-include "LambdaDelta-1/arity/lift1.ma".
+include "Basic-1/arity/lift1.ma".
 
-include "LambdaDelta-1/arity/aprem.ma".
+include "Basic-1/arity/aprem.ma".
 
-include "LambdaDelta-1/llt/props.ma".
+include "Basic-1/llt/props.ma".
 
-include "LambdaDelta-1/drop1/getl.ma".
+include "Basic-1/drop1/getl.ma".
 
-include "LambdaDelta-1/drop1/props.ma".
+include "Basic-1/drop1/props.ma".
 
-include "LambdaDelta-1/lift1/props.ma".
+include "Basic-1/lift1/props.ma".
 
 theorem sc3_arity_gen:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (a: A).((sc3 g a c 
@@ -54,6 +54,9 @@ Appl) w (lift1 is t)))))))) (arity g c t (AHead a0 a1)) (\lambda (H3: (arity
 g c t (AHead a0 a1))).(\lambda (_: ((\forall (d: C).(\forall (w: T).((sc3 g 
 a0 d w) \to (\forall (is: PList).((drop1 is d c) \to (sc3 g a1 d (THead (Flat 
 Appl) w (lift1 is t)))))))))).H3)) H2))))))) a)))).
+(* COMMENTS
+Initial nodes: 369
+END *)
 
 theorem sc3_repl:
  \forall (g: G).(\forall (a1: A).(\forall (c: C).(\forall (t: T).((sc3 g a1 c 
@@ -121,6 +124,9 @@ t0)).(\lambda (a5: A).(\lambda (H16: (leq g a4 a5)).(H1 a4 (llt_trans a4 a0
 Appl) w (lift1 is t)) (H6 d w (H1 x0 (llt_repl g a x0 H8 (AHead a a0) 
 (llt_head_sx a a0)) d w H12 a (leq_sym g a x0 H8)) is H13) x1 H9))))))) a3 
 H11))))))) H7))))) H4)))))))))))) a2)) a1)).
+(* COMMENTS
+Initial nodes: 1359
+END *)
 
 theorem sc3_lift:
  \forall (g: G).(\forall (a: A).(\forall (e: C).(\forall (t: T).((sc3 g a e 
@@ -164,6 +170,9 @@ is d0 c)).(let H_y \def (H5 d0 w H6 (PConsTail is h d)) in (eq_ind T (lift1
 (PConsTail is h d) t) (\lambda (t0: T).(sc3 g a1 d0 (THead (Flat Appl) w 
 t0))) (H_y (drop1_cons_tail c e h d H2 is d0 H7)) (lift1 is (lift h d t)) 
 (lift1_cons_tail t h d is))))))))))) H3))))))))))))) a)).
+(* COMMENTS
+Initial nodes: 849
+END *)
 
 theorem sc3_lift1:
  \forall (g: G).(\forall (e: C).(\forall (a: A).(\forall (hds: 
@@ -184,6 +193,9 @@ in (ex2_ind C (\lambda (c2: C).(drop n n0 c c2)) (\lambda (c2: C).(drop1 p c2
 e)) (sc3 g a c (lift n n0 (lift1 p t))) (\lambda (x: C).(\lambda (H3: (drop n 
 n0 c x)).(\lambda (H4: (drop1 p x e)).(sc3_lift g a x (lift1 p t) (H x t H0 
 H4) c n n0 H3)))) H2))))))))))) hds)))).
+(* COMMENTS
+Initial nodes: 289
+END *)
 
 theorem sc3_abbr:
  \forall (g: G).(\forall (a: A).(\forall (vs: TList).(\forall (i: 
@@ -256,6 +268,9 @@ vs)) (lift (S (trans is i)) O (lift1 (ptrans is i) v)) (lift1_free is i v))
 H10) (lift1 is (TLRef i)) (lift1_lref is i)) (lift1 is (THeads (Flat Appl) vs 
 (TLRef i))) (lifts1_flat Appl is (TLRef i) vs)))))) H8))))))))))) 
 H3))))))))))))) a)).
+(* COMMENTS
+Initial nodes: 1563
+END *)
 
 theorem sc3_cast:
  \forall (g: G).(\forall (a: A).(\forall (vs: TList).(\forall (c: C).(\forall 
@@ -368,6 +383,9 @@ H9 is H10) (THeads (Flat Appl) (lifts1 is vs) (lift1 is t)) (lifts1_flat Appl
 is t vs))) (lift1 is (THead (Flat Cast) u t)) (lift1_flat Cast is u t)) 
 (lift1 is (THeads (Flat Appl) vs (THead (Flat Cast) u t))) (lifts1_flat Appl 
 is (THead (Flat Cast) u t) vs))))))))))) H6)))) H3)))))))))))) a)).
+(* COMMENTS
+Initial nodes: 2625
+END *)
 
 theorem sc3_props__sc3_sn3_abst:
  \forall (g: G).(\forall (a: A).(land (\forall (c: C).(\forall (t: T).((sc3 g 
@@ -497,6 +515,9 @@ is vs) t)) a1)) (eq_ind T (lift1 is (THeads (Flat Appl) vs (TLRef i)))
 vs)) (H7 d w H4) (sns3_lifts1 c is d H5 vs H3))) (lift1 is (TLRef i)) 
 (lift1_lref is i)) (lift1 is (THeads (Flat Appl) vs (TLRef i))) (lifts1_flat 
 Appl is (TLRef i) vs))))) H9)))) H6))))))))))))))))))) a)).
+(* COMMENTS
+Initial nodes: 2737
+END *)
 
 theorem sc3_sn3:
  \forall (g: G).(\forall (a: A).(\forall (c: C).(\forall (t: T).((sc3 g a c 
@@ -513,6 +534,9 @@ t0)))))).(\lambda (_: ((\forall (vs: TList).(\forall (i: nat).(\forall (c0:
 C).((arity g c0 (THeads (Flat Appl) vs (TLRef i)) a) \to ((nf2 c0 (TLRef i)) 
 \to ((sns3 c0 vs) \to (sc3 g a c0 (THeads (Flat Appl) vs (TLRef 
 i))))))))))).(H1 c t H))) H0))))))).
+(* COMMENTS
+Initial nodes: 203
+END *)
 
 theorem sc3_abst:
  \forall (g: G).(\forall (a: A).(\forall (vs: TList).(\forall (c: C).(\forall 
@@ -532,6 +556,9 @@ vs (TLRef i))) (\lambda (_: ((\forall (c0: C).(\forall (t: T).((sc3 g a c0 t)
 nat).(\forall (c0: C).((arity g c0 (THeads (Flat Appl) vs0 (TLRef i0)) a) \to 
 ((nf2 c0 (TLRef i0)) \to ((sns3 c0 vs0) \to (sc3 g a c0 (THeads (Flat Appl) 
 vs0 (TLRef i0))))))))))).(H4 vs i c H H0 H1))) H2)))))))))).
+(* COMMENTS
+Initial nodes: 249
+END *)
 
 theorem sc3_bind:
  \forall (g: G).(\forall (b: B).((not (eq B b Abst)) \to (\forall (a1: 
@@ -608,6 +635,9 @@ vs))) (lifts (S O) O (lifts1 is vs)) (lifts1_xhg is vs)) (sc3_lift1 g c a1 is
 d v H3 H8)) (lift1 is (THead (Bind b) v t)) (lift1_bind b is v t)) (lift1 is 
 (THeads (Flat Appl) vs (THead (Bind b) v t))) (lifts1_flat Appl is (THead 
 (Bind b) v t) vs))))))))))) H4)))))))))))) a2))))).
+(* COMMENTS
+Initial nodes: 1797
+END *)
 
 theorem sc3_appl:
  \forall (g: G).(\forall (a1: A).(\forall (a2: A).(\forall (vs: 
@@ -692,4 +722,7 @@ w H3 H8))) (lift1 is (THead (Bind Abst) w t)) (lift1_bind Abst is w t))
 v (THead (Bind Abst) w t))) (lift1 is (THeads (Flat Appl) vs (THead (Flat 
 Appl) v (THead (Bind Abst) w t)))) (lifts1_flat Appl is (THead (Flat Appl) v 
 (THead (Bind Abst) w t)) vs)))))))))) H4)))))))))))))) a2))).
+(* COMMENTS
+Initial nodes: 1901
+END *)