X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fnext_plus%2Fprops.ma;h=2f42fc60e194d4ba9ce08945248e1ca78dd21f2a;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=258c3a711bacce875591a3b84bc4df205d0f9e68;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma b/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma
index 258c3a711..2f42fc60e 100644
--- a/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma
+++ b/matita/matita/contribs/lambdadelta/basic_1/next_plus/props.ma
@@ -14,9 +14,9 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Basic-1/next_plus/defs.ma".
+include "basic_1/next_plus/defs.ma".
 
-theorem next_plus_assoc:
+lemma next_plus_assoc:
  \forall (g: G).(\forall (n: nat).(\forall (h1: nat).(\forall (h2: nat).(eq 
 nat (next_plus g (next_plus g n h1) h2) (next_plus g n (plus h1 h2))))))
 \def
@@ -35,11 +35,8 @@ n0)) n1) (next g (next_plus g n (plus n0 n1))))).(eq_ind nat (S (plus n0 n1))
 n1)) (next g (next_plus g n n2)))) (f_equal nat nat (next g) (next_plus g 
 (next g (next_plus g n n0)) n1) (next g (next_plus g n (plus n0 n1))) H0) 
 (plus n0 (S n1)) (plus_n_Sm n0 n1)))) h2)))) h1))).
-(* COMMENTS
-Initial nodes: 351
-END *)
 
-theorem next_plus_next:
+lemma next_plus_next:
  \forall (g: G).(\forall (n: nat).(\forall (h: nat).(eq nat (next_plus g 
 (next g n) h) (next g (next_plus g n h)))))
 \def
@@ -47,11 +44,8 @@ theorem next_plus_next:
 g n (plus (S O) h)) (\lambda (n0: nat).(eq nat n0 (next g (next_plus g n 
 h)))) (refl_equal nat (next g (next_plus g n h))) (next_plus g (next_plus g n 
 (S O)) h) (next_plus_assoc g n (S O) h)))).
-(* COMMENTS
-Initial nodes: 87
-END *)
 
-theorem next_plus_lt:
+lemma next_plus_lt:
  \forall (g: G).(\forall (h: nat).(\forall (n: nat).(lt n (next_plus g (next 
 g n) h))))
 \def
@@ -62,7 +56,4 @@ g n0) n))))).(\lambda (n0: nat).(eq_ind nat (next_plus g (next g (next g n0))
 n) (\lambda (n1: nat).(lt n0 n1)) (lt_trans n0 (next g n0) (next_plus g (next 
 g (next g n0)) n) (next_lt g n0) (H (next g n0))) (next g (next_plus g (next 
 g n0) n)) (next_plus_next g (next g n0) n))))) h)).
-(* COMMENTS
-Initial nodes: 153
-END *)