X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Farity%2Ffwd.ma;fp=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FBasic-1%2Farity%2Ffwd.ma;h=31fa35f3cdcaa17a0fb202118872d5e3dfe5caf0;hb=de77f79d60ee3c1d30fe03469172950b557441f3;hp=292c4b65bab7d8dc0913805aa2c8a53a493ce02c;hpb=3531d88e2a19cba027b4b882f8dd74bf37283b9c;p=helm.git

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/fwd.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/fwd.ma
index 292c4b65b..31fa35f3c 100644
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/fwd.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Basic-1/arity/fwd.ma
@@ -14,11 +14,11 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "LambdaDelta-1/arity/defs.ma".
+include "Basic-1/arity/defs.ma".
 
-include "LambdaDelta-1/leq/asucc.ma".
+include "Basic-1/leq/asucc.ma".
 
-include "LambdaDelta-1/getl/drop.ma".
+include "Basic-1/getl/drop.ma".
 
 theorem arity_gen_sort:
  \forall (g: G).(\forall (c: C).(\forall (n: nat).(\forall (a: A).((arity g c 
@@ -92,6 +92,9 @@ n))))).(\lambda (a2: A).(\lambda (H3: (leq g a1 a2)).(\lambda (H4: (eq T t
 T).(arity g c0 t0 a1)) H1 (TSort n) H5) in (leq_trans g a2 a1 (leq_sym g a1 
 a2 H3) (ASort O n) (H6 (refl_equal T (TSort n))))))))))))))) c y a H0))) 
 H))))).
+(* COMMENTS
+Initial nodes: 1235
+END *)
 
 theorem arity_gen_lref:
  \forall (g: G).(\forall (c: C).(\forall (i: nat).(\forall (a: A).((arity g c 
@@ -290,6 +293,9 @@ T).(arity g d u a2)))) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl i c0
 (CHead d (Bind Abst) u)))) (\lambda (d: C).(\lambda (u: T).(arity g d u 
 (asucc g a2)))) x0 x1 H10 (arity_repl g x0 x1 (asucc g a1) H11 (asucc g a2) 
 (asucc_repl g a1 a2 H3)))))))) H9)) H8))))))))))))) c y a H0))) H))))).
+(* COMMENTS
+Initial nodes: 3853
+END *)
 
 theorem arity_gen_bind:
  \forall (b: B).((not (eq B b Abst)) \to (\forall (g: G).(\forall (c: 
@@ -459,6 +465,9 @@ b) u) t a0))) (\lambda (x: A).(\lambda (H10: (arity g c0 u x)).(\lambda (H11:
 c0 u a3)) (\lambda (_: A).(arity g (CHead c0 (Bind b) u) t a0)) x H10 
 (arity_repl g (CHead c0 (Bind b) u) t a1 H11 a0 H4))))) H9))))))))))))) c y 
 a2 H1))) H0)))))))).
+(* COMMENTS
+Initial nodes: 3365
+END *)
 
 theorem arity_gen_abst:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (a: 
@@ -680,6 +689,9 @@ A).(\lambda (_: A).(arity g c0 u (asucc g a3)))) (\lambda (_: A).(\lambda
 x2 x3)) (arity_repl g c0 u (asucc g x0) H10 (asucc g x2) (asucc_repl g x0 x2 
 H15)) (arity_repl g (CHead c0 (Bind Abst) u) t x1 H11 x3 H16)) a2 H18))))))) 
 H14)))))))))) H8))))))))))))) c y a H0))) H)))))).
+(* COMMENTS
+Initial nodes: 4265
+END *)
 
 theorem arity_gen_appl:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (a2: 
@@ -802,6 +814,9 @@ t (AHead a3 a0)))) (\lambda (x: A).(\lambda (H9: (arity g c0 u x)).(\lambda
 u a3)) (\lambda (a3: A).(arity g c0 t (AHead a3 a0))) x H9 (arity_repl g c0 t 
 (AHead x a1) H10 (AHead x a0) (leq_head g x x (leq_refl g x) a1 a0 H3)))))) 
 H8))))))))))))) c y a2 H0))) H)))))).
+(* COMMENTS
+Initial nodes: 2277
+END *)
 
 theorem arity_gen_cast:
  \forall (g: G).(\forall (c: C).(\forall (u: T).(\forall (t: T).(\forall (a: 
@@ -912,6 +927,9 @@ a1)) (arity g c0 t a1) (land (arity g c0 u (asucc g a2)) (arity g c0 t a2))
 a1)).(conj (arity g c0 u (asucc g a2)) (arity g c0 t a2) (arity_repl g c0 u 
 (asucc g a1) H9 (asucc g a2) (asucc_repl g a1 a2 H3)) (arity_repl g c0 t a1 
 H10 a2 H3)))) H8))))))))))))) c y a H0))) H)))))).
+(* COMMENTS
+Initial nodes: 2147
+END *)
 
 theorem arity_gen_appls:
  \forall (g: G).(\forall (c: C).(\forall (t: T).(\forall (vs: TList).(\forall 
@@ -934,6 +952,9 @@ a2))).(let H_x \def (H (AHead x a2) H3) in (let H4 \def H_x in (ex_ind A
 (\lambda (a: A).(arity g c t a)) (ex A (\lambda (a: A).(arity g c t a))) 
 (\lambda (x0: A).(\lambda (H5: (arity g c t x0)).(ex_intro A (\lambda (a: 
 A).(arity g c t a)) x0 H5))) H4)))))) H1))))))) vs)))).
+(* COMMENTS
+Initial nodes: 341
+END *)
 
 theorem arity_gen_lift:
  \forall (g: G).(\forall (c1: C).(\forall (t: T).(\forall (a: A).(\forall (h: 
@@ -1136,4 +1157,7 @@ A).(\lambda (_: (arity g c t0 a1)).(\lambda (H2: ((\forall (x: nat).(\forall
 a2)).(\lambda (x: nat).(\lambda (x0: T).(\lambda (H4: (eq T t0 (lift h x 
 x0))).(\lambda (c2: C).(\lambda (H5: (drop h x c c2)).(arity_repl g c2 x0 a1 
 (H2 x x0 H4 c2 H5) a2 H3))))))))))))) c1 y a H0))))) H))))))).
+(* COMMENTS
+Initial nodes: 4693
+END *)