uri renaming and new nodes count

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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/C/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/C/props.ma
index c93aa0f08ec8fbeba2699043682e1cc276b7517d..878abb3bcad5dc03c7927690106fbfed05aefbe3 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/C/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/C/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/C/defs.ma".
+include "Basic-1/C/defs.ma".
 
-include "LambdaDelta-1/T/props.ma".
+include "Basic-1/T/props.ma".
 
 theorem clt_cong:
  \forall (c: C).(\forall (d: C).((clt c d) \to (\forall (k: K).(\forall (t: 
@@ -25,6 +25,9 @@ T).(clt (CHead c k t) (CHead d k t))))))
  \lambda (c: C).(\lambda (d: C).(\lambda (H: (lt (cweight c) (cweight 
 d))).(\lambda (_: K).(\lambda (t: T).(lt_reg_r (cweight c) (cweight d) 
 (tweight t) H))))).
+(* COMMENTS
+Initial nodes: 33
+END *)
 
 theorem clt_head:
  \forall (k: K).(\forall (c: C).(\forall (u: T).(clt c (CHead c k u))))
@@ -33,6 +36,9 @@ theorem clt_head:
 c) O) (\lambda (n: nat).(lt n (plus (cweight c) (tweight u)))) 
 (le_lt_plus_plus (cweight c) (cweight c) O (tweight u) (le_n (cweight c)) 
 (tweight_lt u)) (cweight c) (plus_n_O (cweight c))))).
+(* COMMENTS
+Initial nodes: 69
+END *)
 
 theorem clt_wf__q_ind:
  \forall (P: ((C \to Prop))).(((\forall (n: nat).((\lambda (P0: ((C \to 
@@ -44,6 +50,9 @@ C).((eq nat (cweight c) n) \to (P c))))) in (\lambda (P: ((C \to
 Prop))).(\lambda (H: ((\forall (n: nat).(\forall (c: C).((eq nat (cweight c) 
 n) \to (P c)))))).(\lambda (c: C).(H (cweight c) c (refl_equal nat (cweight 
 c)))))).
+(* COMMENTS
+Initial nodes: 61
+END *)
 
 theorem clt_wf_ind:
  \forall (P: ((C \to Prop))).(((\forall (c: C).(((\forall (d: C).((clt d c) 
@@ -61,6 +70,9 @@ C).(P c0))) (\lambda (n0: nat).(\lambda (H0: ((\forall (m: nat).((lt m n0)
 c1)))))) H0 (cweight c0) H1) in (H c0 (\lambda (d: C).(\lambda (H3: (lt 
 (cweight d) (cweight c0))).(H2 (cweight d) H3 d (refl_equal nat (cweight 
 d))))))))))))) c)))).
+(* COMMENTS
+Initial nodes: 179
+END *)
 
 theorem chead_ctail:
  \forall (c: C).(\forall (t: T).(\forall (k: K).(ex_3 K C T (\lambda (h: 
@@ -85,6 +97,9 @@ c1 k0 t0) (CTail h u d))))))) (ex_3_intro K C T (\lambda (h: K).(\lambda (d:
 C).(\lambda (u: T).(eq C (CHead (CTail x0 x2 x1) k0 t0) (CTail h u d))))) x0 
 (CHead x1 k0 t0) x2 (refl_equal C (CHead (CTail x0 x2 x1) k0 t0))) (CHead c0 
 k t) H1))))) H0))))))))) c).
+(* COMMENTS
+Initial nodes: 395
+END *)
 
 theorem clt_thead:
  \forall (k: K).(\forall (u: T).(\forall (c: C).(clt c (CTail k u c))))
@@ -93,6 +108,9 @@ theorem clt_thead:
 c0 (CTail k u c0))) (\lambda (n: nat).(clt_head k (CSort n) u)) (\lambda (c0: 
 C).(\lambda (H: (clt c0 (CTail k u c0))).(\lambda (k0: K).(\lambda (t: 
 T).(clt_cong c0 (CTail k u c0) H k0 t))))) c))).
+(* COMMENTS
+Initial nodes: 71
+END *)
 
 theorem c_tail_ind:
  \forall (P: ((C \to Prop))).(((\forall (n: nat).(P (CSort n)))) \to 
@@ -115,4 +133,7 @@ x1))).(eq_ind_r C (CTail x0 x2 x1) (\lambda (c2: C).(P c2)) (let H5 \def
 (eq_ind C (CHead c1 k t) (\lambda (c2: C).(\forall (d: C).((clt d c2) \to (P 
 d)))) H2 (CTail x0 x2 x1) H4) in (H0 x1 (H5 x1 (clt_thead x0 x2 x1)) x0 x2)) 
 (CHead c1 k t) H4))))) H3)))))))) c0)) c)))).
+(* COMMENTS
+Initial nodes: 295
+END *)