uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Basic-1 / nf2 / fwd.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/fwd.ma
index e212a16dbf8cddf60882ca9512ab8d9f02d88db2..9138ff2fad1005ab9cccb7cbd15b973b191b7b0a 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/fwd.ma
@@ -14,13 +14,13 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/nf2/defs.ma".
+include "Basic-1/nf2/defs.ma".
 
-include "LambdaDelta-1/pr2/clen.ma".
+include "Basic-1/pr2/clen.ma".
 
-include "LambdaDelta-1/subst0/dec.ma".
+include "Basic-1/subst0/dec.ma".
 
-include "LambdaDelta-1/T/props.ma".
+include "Basic-1/T/props.ma".
 
 theorem nf2_gen_lref:
  \forall (c: C).(\forall (d: C).(\forall (u: T).(\forall (i: nat).((getl i c 
@@ -32,6 +32,9 @@ c (TLRef i) t2) \to (eq T (TLRef i) t2))))).(\lambda (P:
 Prop).(lift_gen_lref_false (S i) O i (le_O_n i) (le_n (plus O (S i))) u (H0 
 (lift (S i) O u) (pr2_delta c d u i H (TLRef i) (TLRef i) (pr0_refl (TLRef 
 i)) (lift (S i) O u) (subst0_lref u i))) P))))))).
+(* COMMENTS
+Initial nodes: 129
+END *)
 
 theorem nf2_gen_abst:
  \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Bind Abst) u 
@@ -55,6 +58,9 @@ _ t0) \Rightarrow t0])) (THead (Bind Abst) u t) (THead (Bind Abst) u t2) (H
 H_y))) in (let H2 \def (eq_ind_r T t2 (\lambda (t0: T).(pr2 (CHead c (Bind 
 Abst) u) t t0)) H0 t H1) in (eq_ind T t (\lambda (t0: T).(eq T t t0)) 
 (refl_equal T t) t2 H1))))))))).
+(* COMMENTS
+Initial nodes: 353
+END *)
 
 theorem nf2_gen_cast:
  \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Flat Cast) u 
@@ -63,6 +69,9 @@ t)) \to (\forall (P: Prop).P))))
  \lambda (c: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H: (nf2 c (THead 
 (Flat Cast) u t))).(\lambda (P: Prop).(thead_x_y_y (Flat Cast) u t (H t 
 (pr2_free c (THead (Flat Cast) u t) t (pr0_tau t t (pr0_refl t) u))) P))))).
+(* COMMENTS
+Initial nodes: 65
+END *)
 
 theorem nf2_gen_beta:
  \forall (c: C).(\forall (u: T).(\forall (v: T).(\forall (t: T).((nf2 c 
@@ -79,6 +88,9 @@ Prop).(let H0 \def (eq_ind T (THead (Flat Appl) u (THead (Bind Abst) v t))
 Abbr) u t) (pr2_free c (THead (Flat Appl) u (THead (Bind Abst) v t)) (THead 
 (Bind Abbr) u t) (pr0_beta v u u (pr0_refl u) t t (pr0_refl t))))) in 
 (False_ind P H0))))))).
+(* COMMENTS
+Initial nodes: 183
+END *)
 
 theorem nf2_gen_flat:
  \forall (f: F).(\forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c 
@@ -97,6 +109,9 @@ u t2)).(let H1 \def (f_equal T T (\lambda (e: T).(match e in T return
 \Rightarrow t | (TLRef _) \Rightarrow t | (THead _ _ t0) \Rightarrow t0])) 
 (THead (Flat f) u t) (THead (Flat f) u t2) (H (THead (Flat f) u t2) 
 (pr2_head_2 c u t t2 (Flat f) (pr2_cflat c t t2 H0 f u)))) in H1)))))))).
+(* COMMENTS
+Initial nodes: 251
+END *)
 
 theorem nf2_gen__nf2_gen_aux:
  \forall (b: B).(\forall (x: T).(\forall (u: T).(\forall (d: nat).((eq T 
@@ -157,6 +172,9 @@ H4 (Bind b) H6) in (let H8 \def (eq_ind T (lift (S O) d (THead (Bind b) t
 t0)) (\lambda (t1: T).(eq T t1 t0)) H7 (THead (Bind b) (lift (S O) d t) (lift 
 (S O) (S d) t0)) (lift_bind b t t0 (S O) d)) in (H0 (lift (S O) d t) (S d) H8 
 P)))))) H3)) H2))))))))))) x)).
+(* COMMENTS
+Initial nodes: 935
+END *)
 
 theorem nf2_gen_abbr:
  \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Bind Abbr) u 
@@ -182,6 +200,9 @@ O x))).(let H3 \def (eq_ind T t (\lambda (t0: T).(\forall (t2: T).((pr2 c
 (lift (S O) O x) H2) in (nf2_gen__nf2_gen_aux Abbr x u O (H3 x (pr2_free c 
 (THead (Bind Abbr) u (lift (S O) O x)) x (pr0_zeta Abbr not_abbr_abst x x 
 (pr0_refl x) u))) P))) H1))) H0))))))).
+(* COMMENTS
+Initial nodes: 511
+END *)
 
 theorem nf2_gen_void:
  \forall (c: C).(\forall (u: T).(\forall (t: T).((nf2 c (THead (Bind Void) u 
@@ -193,4 +214,7 @@ Void) u (lift (S O) O t)) t2))))).(\lambda (P: Prop).(nf2_gen__nf2_gen_aux
 Void t u O (H t (pr2_free c (THead (Bind Void) u (lift (S O) O t)) t 
 (pr0_zeta Void (sym_not_eq B Abst Void not_abst_void) t t (pr0_refl t) u))) 
 P))))).
+(* COMMENTS
+Initial nodes: 121
+END *)