uri renaming and new nodes count

[helm.git] / helm / software / matita / contribs / LAMBDA-TYPES / Ground-1 / ext / arith.ma

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-1/ext/arith.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-1/ext/arith.ma
index 8be48633f5e4995871da5fa102e540cf5a763dd3..f9796e7fdc19281571ad095946cd7d919dcd6388 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Ground-1/ext/arith.ma
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Ground-1/ext/arith.ma
@@ -14,7 +14,7 @@
 
 (* This file was automatically generated: do not edit *********************)
 
-include "Base-1/preamble.ma".
+include "Ground-1/preamble.ma".
 
 theorem nat_dec:
  \forall (n1: nat).(\forall (n2: nat).(or (eq nat n1 n2) ((eq nat n1 n2) \to 
@@ -55,6 +55,9 @@ Prop).(let H3 \def (f_equal nat nat (\lambda (e: nat).(match e in nat return
 (\lambda (n3: nat).(or (eq nat (S n) n3) ((eq nat (S n) n3) \to (\forall (P0: 
 Prop).P0)))) H0 n H3) in (H4 (refl_equal nat n) P)))))))) (H n0)))) n2)))) 
 n1).
+(* COMMENTS
+Initial nodes: 676
+END *)
 
 theorem simpl_plus_r:
  \forall (n: nat).(\forall (m: nat).(\forall (p: nat).((eq nat (plus m n) 
@@ -65,17 +68,26 @@ theorem simpl_plus_r:
 (n0: nat).(eq nat n0 (plus n p))) (eq_ind_r nat (plus p n) (\lambda (n0: 
 nat).(eq nat n0 (plus n p))) (sym_eq nat (plus n p) (plus p n) (plus_sym n 
 p)) (plus m n) H) (plus n m) (plus_sym n m)))))).
+(* COMMENTS
+Initial nodes: 119
+END *)
 
 theorem minus_Sx_Sy:
  \forall (x: nat).(\forall (y: nat).(eq nat (minus (S x) (S y)) (minus x y)))
 \def
  \lambda (x: nat).(\lambda (y: nat).(refl_equal nat (minus x y))).
+(* COMMENTS
+Initial nodes: 13
+END *)
 
 theorem minus_plus_r:
  \forall (m: nat).(\forall (n: nat).(eq nat (minus (plus m n) n) m))
 \def
  \lambda (m: nat).(\lambda (n: nat).(eq_ind_r nat (plus n m) (\lambda (n0: 
 nat).(eq nat (minus n0 n) m)) (minus_plus n m) (plus m n) (plus_sym m n))).
+(* COMMENTS
+Initial nodes: 45
+END *)
 
 theorem plus_permute_2_in_3:
  \forall (x: nat).(\forall (y: nat).(\forall (z: nat).(eq nat (plus (plus x 
@@ -87,6 +99,9 @@ y) z) (plus (plus x z) y))))
 nat (plus (plus x z) y) (\lambda (n: nat).(eq nat n (plus (plus x z) y))) 
 (refl_equal nat (plus (plus x z) y)) (plus x (plus z y)) (plus_assoc_r x z 
 y)) (plus y z) (plus_sym y z)) (plus (plus x y) z) (plus_assoc_r x y z)))).
+(* COMMENTS
+Initial nodes: 163
+END *)
 
 theorem plus_permute_2_in_3_assoc:
  \forall (n: nat).(\forall (h: nat).(\forall (k: nat).(eq nat (plus (plus n 
@@ -97,6 +112,9 @@ h) k) (plus n (plus k h)))))
 nat (plus (plus n k) h) (\lambda (n0: nat).(eq nat (plus (plus n k) h) n0)) 
 (refl_equal nat (plus (plus n k) h)) (plus n (plus k h)) (plus_assoc_l n k 
 h)) (plus (plus n h) k) (plus_permute_2_in_3 n h k)))).
+(* COMMENTS
+Initial nodes: 119
+END *)
 
 theorem plus_O:
  \forall (x: nat).(\forall (y: nat).((eq nat (plus x y) O) \to (land (eq nat 
@@ -114,12 +132,18 @@ y) O)).(let H2 \def (eq_ind nat (plus (S n) y) (\lambda (e: nat).(match e in
 nat return (\lambda (_: nat).Prop) with [O \Rightarrow False | (S _) 
 \Rightarrow True])) I O H1) in (False_ind (land (eq nat (S n) O) (eq nat y 
 O)) H2)))]) in (H1 (refl_equal nat O))))))) x).
+(* COMMENTS
+Initial nodes: 233
+END *)
 
 theorem minus_Sx_SO:
  \forall (x: nat).(eq nat (minus (S x) (S O)) x)
 \def
  \lambda (x: nat).(eq_ind nat x (\lambda (n: nat).(eq nat n x)) (refl_equal 
 nat x) (minus x O) (minus_n_O x)).
+(* COMMENTS
+Initial nodes: 33
+END *)
 
 theorem eq_nat_dec:
  \forall (i: nat).(\forall (j: nat).(or (not (eq nat i j)) (eq nat i j)))
@@ -139,6 +163,9 @@ nat n n0) (or (not (eq nat (S n) (S n0))) (eq nat (S n) (S n0))) (\lambda
 n) (S n0)) (not_eq_S n n0 H1))) (\lambda (H1: (eq nat n n0)).(or_intror (not 
 (eq nat (S n) (S n0))) (eq nat (S n) (S n0)) (f_equal nat nat S n n0 H1))) (H 
 n0)))) j)))) i).
+(* COMMENTS
+Initial nodes: 401
+END *)
 
 theorem neq_eq_e:
  \forall (i: nat).(\forall (j: nat).(\forall (P: Prop).((((not (eq nat i j)) 
@@ -147,6 +174,9 @@ theorem neq_eq_e:
  \lambda (i: nat).(\lambda (j: nat).(\lambda (P: Prop).(\lambda (H: (((not 
 (eq nat i j)) \to P))).(\lambda (H0: (((eq nat i j) \to P))).(let o \def 
 (eq_nat_dec i j) in (or_ind (not (eq nat i j)) (eq nat i j) P H H0 o)))))).
+(* COMMENTS
+Initial nodes: 61
+END *)
 
 theorem le_false:
  \forall (m: nat).(\forall (n: nat).(\forall (P: Prop).((le m n) \to ((le (S 
@@ -179,12 +209,18 @@ H4)) H2))]) in (H2 (refl_equal nat O)))))) (\lambda (n1: nat).(\lambda (_:
 ((\forall (P: Prop).((le (S n) n1) \to ((le (S n1) (S n)) \to P))))).(\lambda 
 (P: Prop).(\lambda (H1: (le (S n) (S n1))).(\lambda (H2: (le (S (S n1)) (S 
 n))).(H n1 P (le_S_n n n1 H1) (le_S_n (S n1) n H2))))))) n0)))) m).
+(* COMMENTS
+Initial nodes: 409
+END *)
 
 theorem le_Sx_x:
  \forall (x: nat).((le (S x) x) \to (\forall (P: Prop).P))
 \def
  \lambda (x: nat).(\lambda (H: (le (S x) x)).(\lambda (P: Prop).(let H0 \def 
 le_Sn_n in (False_ind P (H0 x H))))).
+(* COMMENTS
+Initial nodes: 23
+END *)
 
 theorem le_n_pred:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (le (pred n) (pred m))))
@@ -193,6 +229,9 @@ theorem le_n_pred:
 (n0: nat).(le (pred n) (pred n0))) (le_n (pred n)) (\lambda (m0: 
 nat).(\lambda (_: (le n m0)).(\lambda (H1: (le (pred n) (pred m0))).(le_trans 
 (pred n) (pred m0) m0 H1 (le_pred_n m0))))) m H))).
+(* COMMENTS
+Initial nodes: 71
+END *)
 
 theorem minus_le:
  \forall (x: nat).(\forall (y: nat).(le (minus x y) x))
@@ -203,6 +242,9 @@ y) n))) (\lambda (_: nat).(le_n O)) (\lambda (n: nat).(\lambda (H: ((\forall
 nat).(le (minus (S n) n0) (S n))) (le_n (S n)) (\lambda (n0: nat).(\lambda 
 (_: (le (match n0 with [O \Rightarrow (S n) | (S l) \Rightarrow (minus n l)]) 
 (S n))).(le_S (minus n n0) n (H n0)))) y)))) x).
+(* COMMENTS
+Initial nodes: 101
+END *)
 
 theorem le_plus_minus_sym:
  \forall (n: nat).(\forall (m: nat).((le n m) \to (eq nat m (plus (minus m n) 
@@ -211,6 +253,9 @@ n))))
  \lambda (n: nat).(\lambda (m: nat).(\lambda (H: (le n m)).(eq_ind_r nat 
 (plus n (minus m n)) (\lambda (n0: nat).(eq nat m n0)) (le_plus_minus n m H) 
 (plus (minus m n) n) (plus_sym (minus m n) n)))).
+(* COMMENTS
+Initial nodes: 61
+END *)
 
 theorem le_minus_minus:
  \forall (x: nat).(\forall (y: nat).((le x y) \to (\forall (z: nat).((le y z) 
@@ -221,6 +266,9 @@ nat).(\lambda (H0: (le y z)).(simpl_le_plus_l x (minus y x) (minus z x)
 (eq_ind_r nat y (\lambda (n: nat).(le n (plus x (minus z x)))) (eq_ind_r nat 
 z (\lambda (n: nat).(le y n)) H0 (plus x (minus z x)) (le_plus_minus_r x z 
 (le_trans x y z H H0))) (plus x (minus y x)) (le_plus_minus_r x y H))))))).
+(* COMMENTS
+Initial nodes: 117
+END *)
 
 theorem le_minus_plus:
  \forall (z: nat).(\forall (x: nat).((le z x) \to (\forall (y: nat).(eq nat 
@@ -257,6 +305,9 @@ H1))]) in (H1 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: (((le (S
 z0) n) \to (\forall (y: nat).(eq nat (minus (plus n y) (S z0)) (plus (minus n 
 (S z0)) y)))))).(\lambda (H1: (le (S z0) (S n))).(\lambda (y: nat).(H n 
 (le_S_n z0 n H1) y))))) x)))) z).
+(* COMMENTS
+Initial nodes: 603
+END *)
 
 theorem le_minus:
  \forall (x: nat).(\forall (z: nat).(\forall (y: nat).((le (plus x y) z) \to 
@@ -266,6 +317,9 @@ theorem le_minus:
 x y) z)).(eq_ind nat (minus (plus x y) y) (\lambda (n: nat).(le n (minus z 
 y))) (le_minus_minus y (plus x y) (le_plus_r x y) z H) x (minus_plus_r x 
 y))))).
+(* COMMENTS
+Initial nodes: 69
+END *)
 
 theorem le_trans_plus_r:
  \forall (x: nat).(\forall (y: nat).(\forall (z: nat).((le (plus x y) z) \to 
@@ -273,6 +327,9 @@ theorem le_trans_plus_r:
 \def
  \lambda (x: nat).(\lambda (y: nat).(\lambda (z: nat).(\lambda (H: (le (plus 
 x y) z)).(le_trans y (plus x y) z (le_plus_r x y) H)))).
+(* COMMENTS
+Initial nodes: 35
+END *)
 
 theorem lt_x_O:
  \forall (x: nat).((lt x O) \to (\forall (P: Prop).P))
@@ -281,6 +338,9 @@ theorem lt_x_O:
 (le_n_O_eq (S x) H) in (let H0 \def (eq_ind nat O (\lambda (ee: nat).(match 
 ee in nat return (\lambda (_: nat).Prop) with [O \Rightarrow True | (S _) 
 \Rightarrow False])) I (S x) H_y) in (False_ind P H0))))).
+(* COMMENTS
+Initial nodes: 48
+END *)
 
 theorem le_gen_S:
  \forall (m: nat).(\forall (x: nat).((le (S m) x) \to (ex2 nat (\lambda (n: 
@@ -299,6 +359,9 @@ nat n (S n0))) (\lambda (n0: nat).(le m n0))))) (\lambda (H2: (le (S m)
 m0)).(ex_intro2 nat (\lambda (n: nat).(eq nat (S m0) (S n))) (\lambda (n: 
 nat).(le m n)) m0 (refl_equal nat (S m0)) (le_S_n m m0 (le_S (S m) m0 H2)))) 
 x H1 H0))]) in (H0 (refl_equal nat x))))).
+(* COMMENTS
+Initial nodes: 261
+END *)
 
 theorem lt_x_plus_x_Sy:
  \forall (x: nat).(\forall (y: nat).(lt x (plus x (S y))))
@@ -306,6 +369,9 @@ theorem lt_x_plus_x_Sy:
  \lambda (x: nat).(\lambda (y: nat).(eq_ind_r nat (plus (S y) x) (\lambda (n: 
 nat).(lt x n)) (le_S_n (S x) (S (plus y x)) (le_n_S (S x) (S (plus y x)) 
 (le_n_S x (plus y x) (le_plus_r y x)))) (plus x (S y)) (plus_sym x (S y)))).
+(* COMMENTS
+Initial nodes: 83
+END *)
 
 theorem simpl_lt_plus_r:
  \forall (p: nat).(\forall (n: nat).(\forall (m: nat).((lt (plus n p) (plus m 
@@ -316,6 +382,9 @@ n p) (plus m p))).(simpl_lt_plus_l n m p (let H0 \def (eq_ind nat (plus n p)
 (\lambda (n0: nat).(lt n0 (plus m p))) H (plus p n) (plus_sym n p)) in (let 
 H1 \def (eq_ind nat (plus m p) (\lambda (n0: nat).(lt (plus p n) n0)) H0 
 (plus p m) (plus_sym m p)) in H1)))))).
+(* COMMENTS
+Initial nodes: 101
+END *)
 
 theorem minus_x_Sy:
  \forall (x: nat).(\forall (y: nat).((lt y x) \to (eq nat (minus x y) (S 
@@ -341,6 +410,9 @@ n0))) (refl_equal nat (S n)) (minus n O) (minus_n_O n))) (\lambda (n0:
 nat).(\lambda (_: (((lt n0 (S n)) \to (eq nat (minus (S n) n0) (S (minus (S 
 n) (S n0))))))).(\lambda (H1: (lt (S n0) (S n))).(let H2 \def (le_S_n (S n0) 
 n H1) in (H n0 H2))))) y)))) x).
+(* COMMENTS
+Initial nodes: 383
+END *)
 
 theorem lt_plus_minus:
  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus x (minus 
@@ -348,6 +420,9 @@ y (S x)))))))
 \def
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_plus_minus (S 
 x) y H))).
+(* COMMENTS
+Initial nodes: 19
+END *)
 
 theorem lt_plus_minus_r:
  \forall (x: nat).(\forall (y: nat).((lt x y) \to (eq nat y (S (plus (minus y 
@@ -356,6 +431,9 @@ theorem lt_plus_minus_r:
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(eq_ind_r nat 
 (plus x (minus y (S x))) (\lambda (n: nat).(eq nat y (S n))) (lt_plus_minus x 
 y H) (plus (minus y (S x)) x) (plus_sym (minus y (S x)) x)))).
+(* COMMENTS
+Initial nodes: 69
+END *)
 
 theorem minus_x_SO:
  \forall (x: nat).((lt O x) \to (eq nat x (S (minus x (S O)))))
@@ -363,6 +441,9 @@ theorem minus_x_SO:
  \lambda (x: nat).(\lambda (H: (lt O x)).(eq_ind nat (minus x O) (\lambda (n: 
 nat).(eq nat x n)) (eq_ind nat x (\lambda (n: nat).(eq nat x n)) (refl_equal 
 nat x) (minus x O) (minus_n_O x)) (S (minus x (S O))) (minus_x_Sy x O H))).
+(* COMMENTS
+Initial nodes: 77
+END *)
 
 theorem le_x_pred_y:
  \forall (y: nat).(\forall (x: nat).((lt x y) \to (le x (pred y))))
@@ -380,6 +461,9 @@ True])) I O H1) in (False_ind ((le (S x) m) \to (le x O)) H2)) H0))]) in (H0
 (refl_equal nat O))))) (\lambda (n: nat).(\lambda (_: ((\forall (x: nat).((lt 
 x n) \to (le x (pred n)))))).(\lambda (x: nat).(\lambda (H0: (lt x (S 
 n))).(le_S_n x n H0))))) y).
+(* COMMENTS
+Initial nodes: 189
+END *)
 
 theorem lt_le_minus:
  \forall (x: nat).(\forall (y: nat).((lt x y) \to (le x (minus y (S O)))))
@@ -387,6 +471,9 @@ theorem lt_le_minus:
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(le_minus x y (S 
 O) (eq_ind_r nat (plus (S O) x) (\lambda (n: nat).(le n y)) H (plus x (S O)) 
 (plus_sym x (S O)))))).
+(* COMMENTS
+Initial nodes: 57
+END *)
 
 theorem lt_le_e:
  \forall (n: nat).(\forall (d: nat).(\forall (P: Prop).((((lt n d) \to P)) 
@@ -395,6 +482,9 @@ theorem lt_le_e:
  \lambda (n: nat).(\lambda (d: nat).(\lambda (P: Prop).(\lambda (H: (((lt n 
 d) \to P))).(\lambda (H0: (((le d n) \to P))).(let H1 \def (le_or_lt d n) in 
 (or_ind (le d n) (lt n d) P H0 H H1)))))).
+(* COMMENTS
+Initial nodes: 49
+END *)
 
 theorem lt_eq_e:
  \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) 
@@ -403,6 +493,9 @@ theorem lt_eq_e:
  \lambda (x: nat).(\lambda (y: nat).(\lambda (P: Prop).(\lambda (H: (((lt x 
 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (le x 
 y)).(or_ind (lt x y) (eq nat x y) P H H0 (le_lt_or_eq x y H1))))))).
+(* COMMENTS
+Initial nodes: 59
+END *)
 
 theorem lt_eq_gt_e:
  \forall (x: nat).(\forall (y: nat).(\forall (P: Prop).((((lt x y) \to P)) 
@@ -412,6 +505,9 @@ theorem lt_eq_gt_e:
 y) \to P))).(\lambda (H0: (((eq nat x y) \to P))).(\lambda (H1: (((lt y x) 
 \to P))).(lt_le_e x y P H (\lambda (H2: (le y x)).(lt_eq_e y x P H1 (\lambda 
 (H3: (eq nat y x)).(H0 (sym_eq nat y x H3))) H2)))))))).
+(* COMMENTS
+Initial nodes: 79
+END *)
 
 theorem lt_gen_xS:
  \forall (x: nat).(\forall (n: nat).((lt x (S n)) \to (or (eq nat x O) (ex2 
@@ -428,6 +524,9 @@ nat).(\lambda (H0: (lt (S n) (S n0))).(or_intror (eq nat (S n) O) (ex2 nat
 (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt m n0))) 
 (ex_intro2 nat (\lambda (m: nat).(eq nat (S n) (S m))) (\lambda (m: nat).(lt 
 m n0)) n (refl_equal nat (S n)) (le_S_n (S n) n0 H0))))))) x).
+(* COMMENTS
+Initial nodes: 243
+END *)
 
 theorem le_lt_false:
  \forall (x: nat).(\forall (y: nat).((le x y) \to ((lt y x) \to (\forall (P: 
@@ -435,6 +534,9 @@ Prop).P))))
 \def
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (le x y)).(\lambda (H0: (lt 
 y x)).(\lambda (P: Prop).(False_ind P (le_not_lt x y H H0)))))).
+(* COMMENTS
+Initial nodes: 31
+END *)
 
 theorem lt_neq:
  \forall (x: nat).(\forall (y: nat).((lt x y) \to (not (eq nat x y))))
@@ -442,6 +544,9 @@ theorem lt_neq:
  \lambda (x: nat).(\lambda (y: nat).(\lambda (H: (lt x y)).(\lambda (H0: (eq 
 nat x y)).(let H1 \def (eq_ind nat x (\lambda (n: nat).(lt n y)) H y H0) in 
 (lt_n_n y H1))))).
+(* COMMENTS
+Initial nodes: 43
+END *)
 
 theorem arith0:
  \forall (h2: nat).(\forall (d2: nat).(\forall (n: nat).((le (plus d2 h2) n) 
@@ -457,6 +562,9 @@ h2) (\lambda (n0: nat).(le n0 (minus (plus n h1) h2))) (le_minus_minus h2
 (le_plus_plus (plus d2 h2) n h1 h1 H (le_n h1)))) (plus h2 d2) (plus_sym h2 
 d2)) (plus h2 (plus d2 h1)) (plus_assoc_l h2 d2 h1))) (plus d2 h1) 
 (minus_plus h2 (plus d2 h1))))))).
+(* COMMENTS
+Initial nodes: 235
+END *)
 
 theorem O_minus:
  \forall (x: nat).(\forall (y: nat).((le x y) \to (eq nat (minus x y) O)))
@@ -476,6 +584,9 @@ H3))))) (le_gen_S x0 O H0))) (\lambda (n: nat).(\lambda (_: (((le (S x0) n)
 \to (eq nat (match n with [O \Rightarrow (S x0) | (S l) \Rightarrow (minus x0 
 l)]) O)))).(\lambda (H1: (le (S x0) (S n))).(H n (le_S_n x0 n H1))))) y)))) 
 x).
+(* COMMENTS
+Initial nodes: 252
+END *)
 
 theorem minus_minus:
  \forall (z: nat).(\forall (x: nat).(\forall (y: nat).((le z x) \to ((le z y) 
@@ -517,6 +628,9 @@ y0)))))).(\lambda (H: (le (S z0) (S x0))).(\lambda (H0: (le (S z0) (S
 y0))).(\lambda (H1: (eq nat (minus (S x0) (S z0)) (minus (S y0) (S 
 z0)))).(f_equal nat nat S x0 y0 (IH x0 y0 (le_S_n z0 x0 H) (le_S_n z0 y0 H0) 
 H1))))))) y)))) x)))) z).
+(* COMMENTS
+Initial nodes: 751
+END *)
 
 theorem plus_plus:
  \forall (z: nat).(\forall (x1: nat).(\forall (x2: nat).(\forall (y1: 
@@ -592,6 +706,9 @@ z0))).(\lambda (H0: (le (S x4) (S z0))).(\lambda (H1: (eq nat (plus (minus z0
 x2) y1) (plus (minus z0 x4) y2))).(f_equal nat nat S (plus x2 y2) (plus x4 
 y1) (IH x2 x4 y1 y2 (le_S_n x2 z0 H) (le_S_n x4 z0 H0) H1))))))))) x3)))) 
 x1)))) z).
+(* COMMENTS
+Initial nodes: 1495
+END *)
 
 theorem le_S_minus:
  \forall (d: nat).(\forall (h: nat).(\forall (n: nat).((le (plus d h) n) \to 
@@ -602,6 +719,9 @@ d h) n)).(let H0 \def (le_trans d (plus d h) n (le_plus_l d h) H) in (let H1
 \def (eq_ind nat n (\lambda (n0: nat).(le d n0)) H0 (plus (minus n h) h) 
 (le_plus_minus_sym h n (le_trans h (plus d h) n (le_plus_r d h) H))) in (le_S 
 d (minus n h) (le_minus d n h H))))))).
+(* COMMENTS
+Initial nodes: 107
+END *)
 
 theorem lt_x_pred_y:
  \forall (x: nat).(\forall (y: nat).((lt x (pred y)) \to (lt (S x) y)))
@@ -611,4 +731,7 @@ n)) \to (lt (S x) n))) (\lambda (H: (lt x O)).(lt_x_O x H (lt (S x) O)))
 (\lambda (n: nat).(\lambda (_: (((lt x (pred n)) \to (lt (S x) n)))).(\lambda 
 (H0: (lt x n)).(le_S_n (S (S x)) (S n) (le_n_S (S (S x)) (S n) (le_n_S (S x) 
 n H0)))))) y)).
+(* COMMENTS
+Initial nodes: 103
+END *)