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

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/props.ma
index a801ea1bb..2f0f092f2 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/props.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/nf2/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/nf2/defs.ma".
+include "Basic-1/nf2/defs.ma".
 
-include "LambdaDelta-1/pr2/fwd.ma".
+include "Basic-1/pr2/fwd.ma".
 
 theorem nf2_sort:
  \forall (c: C).(\forall (n: nat).(nf2 c (TSort n)))
@@ -24,6 +24,9 @@ theorem nf2_sort:
  \lambda (c: C).(\lambda (n: nat).(\lambda (t2: T).(\lambda (H: (pr2 c (TSort 
 n) t2)).(eq_ind_r T (TSort n) (\lambda (t: T).(eq T (TSort n) t)) (refl_equal 
 T (TSort n)) t2 (pr2_gen_sort c t2 n H))))).
+(* COMMENTS
+Initial nodes: 55
+END *)
 
 theorem nf2_csort_lref:
  \forall (n: nat).(\forall (i: nat).(nf2 (CSort n) (TLRef i)))
@@ -43,6 +46,9 @@ n) (CHead d (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift
 (lift (S i) O x1))).(eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(eq T 
 (TLRef i) t)) (getl_gen_sort n i (CHead x0 (Bind Abbr) x1) H2 (eq T (TLRef i) 
 (lift (S i) O x1))) t2 H3))))) H1)) H0))))).
+(* COMMENTS
+Initial nodes: 355
+END *)
 
 theorem nf2_abst:
  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (b: B).(\forall (v: 
@@ -64,6 +70,9 @@ x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T (THead
 (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst) u x0 t 
 x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 b v))) t2 H3)))))) 
 H2)))))))))).
+(* COMMENTS
+Initial nodes: 299
+END *)
 
 theorem nf2_abst_shift:
  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (t: T).((nf2 (CHead c 
@@ -83,6 +92,9 @@ b) u0) t x1))))).(eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t0: T).(eq T
 (THead (Bind Abst) u t) t0)) (f_equal3 K T T T THead (Bind Abst) (Bind Abst) 
 u x0 t x1 (refl_equal K (Bind Abst)) (H x0 H4) (H0 x1 (H5 Abst u))) t2 
 H3)))))) H2)))))))).
+(* COMMENTS
+Initial nodes: 295
+END *)
 
 theorem nfs2_tapp:
  \forall (c: C).(\forall (t: T).(\forall (ts: TList).((nfs2 c (TApp ts t)) 
@@ -101,6 +113,9 @@ H4 \def H_x in (land_ind (nfs2 c t1) (nf2 c t) (land (land (nf2 c t0) (nfs2 c
 t1)) (nf2 c t)) (\lambda (H5: (nfs2 c t1)).(\lambda (H6: (nf2 c t)).(conj 
 (land (nf2 c t0) (nfs2 c t1)) (nf2 c t) (conj (nf2 c t0) (nfs2 c t1) H2 H5) 
 H6))) H4))))) H1)))))) ts))).
+(* COMMENTS
+Initial nodes: 295
+END *)
 
 theorem nf2_appls_lref:
  \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (vs: 
@@ -257,6 +272,9 @@ True])])) I (THead (Bind x0) x1 x2) H15) in (False_ind (eq T (THead (Flat
 Appl) t (THeads (Flat Appl) (TCons t1 t3) (TLRef i))) (THead (Bind x0) x5 
 (THead (Flat Appl) (lift (S O) O x4) x3))) H16))))))) t0 H_y H9) t2 
 H10))))))))))))) H7)) H6))))))) H2)))))) vs)))).
+(* COMMENTS
+Initial nodes: 2915
+END *)
 
 theorem nf2_appl_lref:
  \forall (c: C).(\forall (u: T).((nf2 c u) \to (\forall (i: nat).((nf2 c 
@@ -265,6 +283,9 @@ theorem nf2_appl_lref:
  \lambda (c: C).(\lambda (u: T).(\lambda (H: (nf2 c u)).(\lambda (i: 
 nat).(\lambda (H0: (nf2 c (TLRef i))).(let H_y \def (nf2_appls_lref c i H0 
 (TCons u TNil)) in (H_y (conj (nf2 c u) True H I))))))).
+(* COMMENTS
+Initial nodes: 49
+END *)
 
 theorem nf2_lref_abst:
  \forall (c: C).(\forall (e: C).(\forall (u: T).(\forall (i: nat).((getl i c 
@@ -295,6 +316,9 @@ Void \Rightarrow False]) | (Flat _) \Rightarrow False])])) I (CHead x0 (Bind
 Abbr) x1) (getl_mono c (CHead e (Bind Abst) u) i H (CHead x0 (Bind Abbr) x1) 
 H3)) in (False_ind (eq T (TLRef i) (lift (S i) O x1)) H6))) t2 H4))))) H2)) 
 H1)))))))).
+(* COMMENTS
+Initial nodes: 494
+END *)
 
 theorem nf2_lift:
  \forall (d: C).(\forall (t: T).((nf2 d t) \to (\forall (c: C).(\forall (h: 
@@ -311,4 +335,7 @@ T (lift h i t) t0)) (let H_y \def (H x H4) in (let H5 \def (eq_ind_r T x
 (\lambda (t0: T).(pr2 d t t0)) H4 t H_y) in (eq_ind T t (\lambda (t0: T).(eq 
 T (lift h i t) (lift h i t0))) (refl_equal T (lift h i t)) x H_y))) t2 H3)))) 
 H2)))))))))).
+(* COMMENTS
+Initial nodes: 245
+END *)