uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / arity / pr3.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/pr3.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/pr3.ma
index b56a8945a05500e3259140626a7a7eab992bb64a..f8952088ee20470060d56e69f6d2f49c20307b3e 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/pr3.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/pr3.ma
@@ -14,17 +14,17 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/csuba/arity.ma".
+include "Basic-1/csuba/arity.ma".
 
-include "LambdaDelta-1/pr3/defs.ma".
+include "Basic-1/pr3/defs.ma".
 
-include "LambdaDelta-1/pr1/defs.ma".
+include "Basic-1/pr1/defs.ma".
 
-include "LambdaDelta-1/wcpr0/getl.ma".
+include "Basic-1/wcpr0/getl.ma".
 
-include "LambdaDelta-1/pr0/fwd.ma".
+include "Basic-1/pr0/fwd.ma".
 
-include "LambdaDelta-1/arity/subst0.ma".
+include "Basic-1/arity/subst0.ma".
 
 theorem arity_sred_wcpr0_pr0:
  \forall (g: G).(\forall (c1: C).(\forall (t1: T).(\forall (a: A).((arity g 
@@ -570,6 +570,9 @@ c2) \to (\forall (t2: T).((pr0 t t2) \to (arity g c2 t2 a1))))))).(\lambda
 (a2: A).(\lambda (H2: (leq g a1 a2)).(\lambda (c2: C).(\lambda (H3: (wcpr0 c 
 c2)).(\lambda (t2: T).(\lambda (H4: (pr0 t t2)).(arity_repl g c2 t2 a1 (H1 c2 
 H3 t2 H4) a2 H2)))))))))))) c1 t1 a H))))).
+(* COMMENTS
+Initial nodes: 10246
+END *)
 
 theorem arity_sred_wcpr0_pr1:
  \forall (t1: T).(\forall (t2: T).((pr1 t1 t2) \to (\forall (g: G).(\forall 
@@ -589,6 +592,9 @@ a))))))))).(\lambda (g: G).(\lambda (c1: C).(\lambda (a: A).(\lambda (H3:
 (arity g c1 t4 a)).(\lambda (c2: C).(\lambda (H4: (wcpr0 c1 c2)).(H2 g c2 a 
 (arity_sred_wcpr0_pr0 g c1 t4 a H3 c2 H4 t3 H0) c2 (wcpr0_refl 
 c2)))))))))))))) t1 t2 H))).
+(* COMMENTS
+Initial nodes: 213
+END *)
 
 theorem arity_sred_pr2:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall 
@@ -606,6 +612,9 @@ t4)).(\lambda (t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (g:
 G).(\lambda (a: A).(\lambda (H3: (arity g c0 t3 a)).(arity_subst0 g c0 t4 a 
 (arity_sred_wcpr0_pr0 g c0 t3 a H3 c0 (wcpr0_refl c0) t4 H1) d u i H0 t 
 H2)))))))))))))) c t1 t2 H)))).
+(* COMMENTS
+Initial nodes: 205
+END *)
 
 theorem arity_sred_pr3:
  \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr3 c t1 t2) \to (\forall 
@@ -620,4 +629,7 @@ T).(\lambda (t4: T).(\lambda (H0: (pr2 c t4 t3)).(\lambda (t5: T).(\lambda
 t3 a) \to (arity g c t5 a)))))).(\lambda (g: G).(\lambda (a: A).(\lambda (H3: 
 (arity g c t4 a)).(H2 g a (arity_sred_pr2 c t4 t3 H0 g a H3))))))))))) t1 t2 
 H)))).
+(* COMMENTS
+Initial nodes: 151
+END *)