X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Fty3%2Fnf2.ma;h=47b675663abb30e2bbe04bcca816d2431ed552f0;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=0c23d2956a4d062ca0ad009b96891303e293ee20;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/nf2.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/nf2.ma
index 0c23d2956..47b675663 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/nf2.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/ty3/nf2.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/ty3/arity.ma".
+include "Basic-1/ty3/arity.ma".
 
-include "LambdaDelta-1/pc3/nf2.ma".
+include "Basic-1/pc3/nf2.ma".
 
-include "LambdaDelta-1/nf2/arity.ma".
+include "Basic-1/nf2/arity.ma".
 
 definition ty3_nf2_inv_abst_premise:
  C \to (T \to (T \to Prop))
@@ -37,6 +37,9 @@ theorem ty3_nf2_inv_abst_premise_csort:
 wi))).(\lambda (vs: TList).(\lambda (_: (pc3 (CSort m) (THeads (Flat Appl) vs 
 (lift (S i) O wi)) (THead (Bind Abst) w u))).(getl_gen_sort m i (CHead d 
 (Bind Abst) wi) H False))))))))).
+(* COMMENTS
+Initial nodes: 85
+END *)
 
 theorem ty3_nf2_inv_all:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (u: T).((ty3 g c t 
@@ -60,6 +63,9 @@ i))))) (\lambda (ws: TList).(\lambda (_: nat).(nfs2 c ws))) (\lambda (_:
 TList).(\lambda (i: nat).(nf2 c (TLRef i)))))) (\lambda (x: A).(\lambda (H2: 
 (arity g c t x)).(\lambda (_: (arity g c u (asucc g x))).(arity_nf2_inv_all g 
 c t x H2 H0)))) H1)))))))).
+(* COMMENTS
+Initial nodes: 233
+END *)
 
 theorem ty3_nf2_inv_sort:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (m: nat).((ty3 g c t 
@@ -172,6 +178,9 @@ x1)) (THeads (Flat Appl) ws (TLRef i))))) (\lambda (ws: TList).(\lambda (_:
 nat).(nfs2 c ws))) (\lambda (_: TList).(\lambda (i: nat).(nf2 c (TLRef i)))) 
 x0 x1 (refl_equal T (THeads (Flat Appl) x0 (TLRef x1))) H4 H5)) t H3))))))) 
 H2)) H1)))))))).
+(* COMMENTS
+Initial nodes: 2045
+END *)
 
 theorem ty3_nf2_gen__ty3_nf2_inv_abst_aux:
  \forall (c: C).(\forall (w1: T).(\forall (u1: T).((ty3_nf2_inv_abst_premise 
@@ -192,6 +201,9 @@ wi))).(\lambda (vs: TList).(\lambda (H2: (pc3 c (THeads (Flat Appl) vs (lift
 (THeads (Flat Appl) vs (lift (S i) O wi))) (pc3_thin_dx c (THeads (Flat Appl) 
 vs (lift (S i) O wi)) (THead (Bind Abst) w2 u2) H2 t Appl) (THead (Bind Abst) 
 w1 u1) H0))))))))))))))).
+(* COMMENTS
+Initial nodes: 271
+END *)
 
 theorem ty3_nf2_inv_abst:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (w: T).(\forall (u: 
@@ -454,4 +466,7 @@ Abst) x) v x2))) (\lambda (v: T).(\lambda (_: T).(nf2 (CHead c (Bind Abst) x)
 v)))) H23)))))) t1 H18))))))) H17))))))))) (ty3_gen_appl g c t0 (THeads (Flat 
 Appl) t1 (TLRef x1)) (THead (Bind Abst) x x2) H12))))))))) x0)) H10)) H9)) t 
 H5))))))) H4)) H3))))))))))).
+(* COMMENTS
+Initial nodes: 5333
+END *)