(* This file was automatically generated: do not edit *********************)
-include "LambdaDelta-1/next_plus/defs.ma".
+include "Basic-1/next_plus/defs.ma".
theorem next_plus_assoc:
\forall (g: G).(\forall (n: nat).(\forall (h1: nat).(\forall (h2: nat).(eq
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:
\forall (g: G).(\forall (n: nat).(\forall (h: nat).(eq nat (next_plus g
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:
\forall (g: G).(\forall (h: nat).(\forall (n: nat).(lt n (next_plus g (next
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 *)